Documentation

Lean 4 Proof

theorem cesGameCriticalRatio_bounds {ρ : ℝ} (hρ : 0 < ρ) :
    0 < cesGameCriticalRatio ρ ∧ cesGameCriticalRatio ρ < 1 := by
  rw [cesGameCriticalRatio_eq ρ hρ]
  constructor
  · positivity
  · apply rpow_lt_one_of_one_lt_of_neg (by norm_num : (1:ℝ) < 2)
    exact neg_neg_of_pos (div_pos one_pos hρ)

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/Strategic.lean:109

Module Section

Strategic independence of CES (Paper 1, Sections 7-8):

In the same file