Documentation

Lean 4 Proof

theorem threshold_neg_complements {ρ : ℝ}
    (hρ0 : 0 < ρ) (hρ1 : ρ < 1) :
    stabilityThreshold ρ < 0 := by
  unfold stabilityThreshold
  exact div_neg_of_neg_of_pos (by linarith) (by linarith)

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:208

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file