Documentation

Lean 4 Proof

theorem universal_stability_complements {ρ : ℝ} (hρ0 : 0 < ρ) (hρ : ρ < 1)
    (sj : ℝ) (hs_nn : 0 ≤ sj) (_hs_le : sj ≤ 1) :
    isLocallyStable ρ sj := by
  unfold isLocallyStable
  have h1 : 1 - 2 * sj ≤ 1 := by linarith
  have h2 : ρ * (1 - 2 * sj) ≤ ρ := by nlinarith
  linarith

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:178

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file