Documentation

Lean 4 Proof

theorem cesGame_classification :
    -- ρ ≤ 0: complete complementarity, losing one player is catastrophic
    (∀ ρ : ℝ, ρ ≤ 0 → cesGameCriticalRatio ρ = 0) ∧
    -- ρ > 0: partial substitutability, nonzero payoff from unilateral action
    (∀ ρ : ℝ, 0 < ρ → 0 < cesGameCriticalRatio ρ) := by
  constructor
  · intro ρ hρ
    simp [cesGameCriticalRatio, show ¬(ρ > 0) by linarith]
  · intro ρ hρ
    exact (cesGameCriticalRatio_bounds hρ).1

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/Strategic.lean:125

Module Section

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

In the same file