Documentation

Lean 4 Proof

theorem multiple_equilibria_upper_root {ρ κ : ℝ}
    (hρ : ρ < 1) (hκ_pos : 0 < κ) (hκ_small : κ < (1 - ρ) / 4) :
    ∃ J_high : ℝ, 2 ≤ J_high ∧ perCapitaSurplus J_high ρ = κ := by
  -- Pick J_large from Part 1
  obtain ⟨_, _, ⟨J_large, hJ_large_gt2, hJ_large_small⟩⟩ :=
    multiple_equilibria_sign_below_peak hρ hκ_pos hκ_small
  have h_at_2 : perCapitaSurplus 2 ρ = (1 - ρ) / 4 := perCapitaSurplus_at_two ρ
  -- κ ∈ [π_K(J_large), π_K(2)]
  have hκ_mem : κ ∈ Set.Icc (perCapitaSurplus J_large ρ) (perCapitaSurplus 2 ρ) := by
    rw [h_at_2]; exact ⟨le_of_lt hJ_large_small, le_of_lt hκ_small⟩
  -- But IVT needs [a,b] with a ≤ b, so use [2, J_large]
  -- and note that κ ∈ Icc (min f(2) f(J_large)) (max f(2) f(J_large))
  -- Since f(2) > κ > f(J_large), κ ∈ Icc f(J_large) f(2)
  -- intermediate_value_Icc on [2, J_large] with κ ∈ [f(J_large), f(2)]
  -- Wait, intermediate_value_Icc gives f(a) to f(b), but we need f(a) > f(b)
  -- Use intermediate_value_Icc which gives κ ∈ Icc (f a) (f b) OR use uIcc version
  -- Actually intermediate_value_Icc works: if κ ∈ Icc (f 2) (f J_large) that's wrong
  -- since f(2) > f(J_large). We need the descending version.
  have hle : (2:ℝ) ≤ J_large := le_of_lt hJ_large_gt2
  have hcont : ContinuousOn (fun x => perCapitaSurplus x ρ) (Set.Icc 2 J_large) := 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)
  -- κ ∈ Icc (f J_large) (f 2), need to map to intermediate_value_Icc
  -- Use the fact that ContinuousOn + connected → image is connected
  -- Simpler: use intermediate_value_uIcc or intermediate_value_Icc with swapped bounds
  -- intermediate_value_Icc : a ≤ b → ContinuousOn f [a,b] → y ∈ [f a, f b] → ∃ x ∈ [a,b], f x = y
  -- Our case: a=2, b=J_large, f(2) > κ > f(J_large)
  -- So κ ∉ [f(2), f(J_large)] but κ ∈ [f(J_large), f(2)]
  -- We can negate f and use IVT, or use IsPreconnected.intermediate_value
  -- Actually Mathlib has intermediate_value_Icc which handles both orderings
  -- Let me check: it requires y ∈ Icc (f a) (f b), so if f a > f b we're stuck
  -- Use -f instead: -f(2) < -κ < -f(J_large), so -κ ∈ [-f(2), -f(J_large)]
  have hcont_neg : ContinuousOn (fun x => -(perCapitaSurplus x ρ)) (Set.Icc 2 J_large) :=
    hcont.neg
  have hκ_neg_mem : -κ ∈ Set.Icc (-(perCapitaSurplus 2 ρ)) (-(perCapitaSurplus J_large ρ)) := by
    constructor
    · linarith [hκ_small, h_at_2]
    · linarith [hJ_large_small]
  obtain ⟨J_high, ⟨hJ_ge, _⟩, hJ_eq⟩ :=
    intermediate_value_Icc hle hcont_neg hκ_neg_mem
  exact ⟨J_high, hJ_ge, by linarith⟩

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Equilibria.lean:140

Module Section

Paper 1c, Section 3: The Participation Game

In the same file