Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:216

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file