Documentation

Lean 4 Proof

theorem curvatureK_sign_classification (hJ : 2 ≤ J) (ρ : ℝ) :
    (ρ < 1 → 0 < curvatureK J ρ) ∧
    (ρ = 1 → curvatureK J ρ = 0) ∧
    (1 < ρ → curvatureK J ρ < 0) := by
  refine ⟨curvatureK_pos hJ, fun h => ?_, fun h => ?_⟩
  · simp [curvatureK, h]
  · unfold curvatureK
    apply div_neg_of_neg_of_pos
    · have : (1 : ℝ) < ↑J := by exact_mod_cast (by omega : 1 < J)
      nlinarith
    · exact_mod_cast (by omega : 0 < J)

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:39

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file