Documentation

Lean 4 Proof

theorem folkThreshold_valid {ρ : ℝ}
    (hρ0 : 0 < ρ) (hρ1 : ρ < 1)
    {c : ℝ} (hc : 0 < c) (hJ : 2 ≤ J) :
    0 < folkThreshold J ρ c ∧
    folkThreshold J ρ c < 1 := by
  unfold folkThreshold
  have hg : 0 < deviationGain J ρ c := by
    unfold deviationGain
    exact div_pos (by linarith) (mul_pos
      (mul_pos (by norm_num) (by exact_mod_cast
        (by omega : 0 < J))) hc)
  have hp := knockoutPunishment_pos hρ0 hρ1 hc hJ
  exact ⟨div_pos hg (by linarith),
    (div_lt_one (by linarith)).mpr (by linarith)⟩

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:302

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file