Documentation

Lean 4 Proof

theorem multiple_equilibria_lower_root {ρ κ : ℝ}
    (_hρ : ρ < 1) (hκ_pos : 0 < κ) (hκ_small : κ < (1 - ρ) / 4) :
    ∃ J_low : ℝ, 1 ≤ J_low ∧ J_low ≤ 2 ∧ perCapitaSurplus J_low ρ = κ := by
  have h_at_1 : perCapitaSurplus 1 ρ = 0 := perCapitaSurplus_at_one ρ
  have h_at_2 : perCapitaSurplus 2 ρ = (1 - ρ) / 4 := perCapitaSurplus_at_two ρ
  -- π_K(1) = 0 ≤ κ ≤ (1-ρ)/4 = π_K(2)
  have hκ_mem : κ ∈ Set.Icc (perCapitaSurplus 1 ρ) (perCapitaSurplus 2 ρ) := by
    rw [h_at_1, h_at_2]; exact ⟨le_of_lt hκ_pos, le_of_lt hκ_small⟩
  -- Continuity of π_K on [1, 2]
  have hcont : ContinuousOn (fun x => perCapitaSurplus x ρ) (Set.Icc 1 2) := by
    simp only [perCapitaSurplus]
    apply ContinuousOn.div
    · exact continuousOn_const.mul (continuousOn_id.sub continuousOn_const)
    · exact continuousOn_id.pow 2
    · intro x hx; exact ne_of_gt (pow_pos (by linarith [hx.1]) 2)
  obtain ⟨J_low, ⟨hJ_ge, hJ_le⟩, hJ_eq⟩ :=
    intermediate_value_Icc (by norm_num : (1:ℝ) ≤ 2) hcont hκ_mem
  exact ⟨J_low, hJ_ge, hJ_le, hJ_eq⟩

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Equilibria.lean:118

Module Section

Paper 1c, Section 3: The Participation Game

In the same file