Documentation

Lean 4 Proof

theorem multiple_equilibria_fold {ρ κ : ℝ}
    (hρ : ρ < 1) (hκ_pos : 0 < κ) (hκ_small : κ < (1 - ρ) / 4) :
    ∃ J_low J_high : ℝ,
      1 ≤ J_low ∧ J_low ≤ 2 ∧ 2 ≤ J_high ∧
      perCapitaSurplus J_low ρ = κ ∧ perCapitaSurplus J_high ρ = κ := by
  obtain ⟨J_low, hJl1, hJl2, hJl_eq⟩ := multiple_equilibria_lower_root hρ hκ_pos hκ_small
  obtain ⟨J_high, hJh2, hJh_eq⟩ := multiple_equilibria_upper_root hρ hκ_pos hκ_small
  exact ⟨J_low, J_high, hJl1, hJl2, hJh2, hJl_eq, hJh_eq⟩

Dependency Graph

Location

thesis/CESProofs/EntryExit/Equilibria.lean:191

Module Section

Paper 1c, Section 3: The Participation Game

In the same file