Documentation

Lean 4 Proof

theorem threshold_lt_half {ρ : ℝ} (hρ : 1 < ρ) :
    stabilityThreshold ρ < 1 / 2 := by
  unfold stabilityThreshold
  rw [div_lt_div_iff₀ (by linarith : (0:ℝ) < 2 * ρ) (by norm_num : (0:ℝ) < 2)]
  nlinarith

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:223

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file