Documentation

Lean 4 Proof

theorem instability_substitutes {ρ : ℝ} (hρ : 1 < ρ)
    (sj : ℝ) (hs : sj < (ρ - 1) / (2 * ρ)) :
    ¬ isLocallyStable ρ sj := by
  unfold isLocallyStable; push_neg
  have h1 : sj * (2 * ρ) < ρ - 1 := by
    rwa [lt_div_iff₀ (by linarith : (0:ℝ) < 2 * ρ)] at hs
  nlinarith

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:194

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file