theorem multiple_equilibria_sign_below_peak {ρ κ : ℝ}
(_hρ : ρ < 1) (hκ_pos : 0 < κ) (hκ_small : κ < (1 - ρ) / 4) :
-- (a) At J=1: surplus is 0 < κ, so net payoff is negative
perCapitaSurplus 1 ρ < κ ∧
-- (b) At J=2: surplus exceeds cost
κ < perCapitaSurplus 2 ρ ∧
-- (c) For sufficiently large J: surplus falls below cost again
∃ J_large : ℝ, 2 < J_large ∧ perCapitaSurplus J_large ρ < κ := by
refine ⟨?_, ?_, ?_⟩
· -- (a) π_K(1) = 0 < κ
rw [perCapitaSurplus_at_one]; exact hκ_pos
· -- (b) π_K(2) = (1-ρ)/4 > κ
rw [perCapitaSurplus_at_two]; exact hκ_small
· -- (c) For large J, π_K(J) < κ.
-- π_K(J) = (1-ρ)(J-1)/J² ≤ (1-ρ)/J (since (J-1)/J² ≤ 1/J for J ≥ 1).
-- So pick J_large such that (1-ρ)/J_large < κ.
-- Use J_large = 2(1-ρ)/κ which gives (1-ρ)/J_large = κ/2 < κ.
have h1ρ : 0 < 1 - ρ := by linarith
use 2 * (1 - ρ) / κ
have hκne : κ ≠ 0 := ne_of_gt hκ_pos
constructor
· -- 2(1-ρ)/κ > 2 iff (1-ρ)/κ > 1 iff 1-ρ > κ
rw [show (2:ℝ) * (1 - ρ) / κ = 2 * ((1 - ρ) / κ) from by ring]
have h1 : 1 < (1 - ρ) / κ := by rw [one_lt_div hκ_pos]; linarith
linarith
· -- π_K(2(1-ρ)/κ) < κ
simp only [perCapitaSurplus]
have hJ_pos : 0 < 2 * (1 - ρ) / κ := by positivity
rw [div_lt_iff₀ (sq_pos_of_pos hJ_pos)]
-- Goal: (1-ρ) * (2(1-ρ)/κ - 1) < κ * (2(1-ρ)/κ)²
-- Bound LHS ≤ (1-ρ) * (2(1-ρ)/κ) = 2(1-ρ)²/κ
-- RHS = κ * 4(1-ρ)²/κ² = 4(1-ρ)²/κ
-- So LHS < RHS since 2(1-ρ)²/κ < 4(1-ρ)²/κ
have hJ_sub : 2 * (1 - ρ) / κ - 1 < 2 * (1 - ρ) / κ := by linarith
have hJ_bound : (1 - ρ) * (2 * (1 - ρ) / κ - 1) <
(1 - ρ) * (2 * (1 - ρ) / κ) := by
exact mul_lt_mul_of_pos_left hJ_sub h1ρ
have hsq : (2 * (1 - ρ) / κ) ^ 2 = 4 * (1 - ρ) ^ 2 / κ ^ 2 := by ring
calc (1 - ρ) * (2 * (1 - ρ) / κ - 1)
< (1 - ρ) * (2 * (1 - ρ) / κ) := hJ_bound
_ = 2 * (1 - ρ) ^ 2 / κ := by ring
_ ≤ κ * (2 * (1 - ρ) / κ) ^ 2 := by
rw [hsq]
rw [show κ * (4 * (1 - ρ) ^ 2 / κ ^ 2) =
4 * (1 - ρ) ^ 2 / κ from by field_simp]
apply div_le_div_of_nonneg_right _ hκ_pos.le
linarith [sq_nonneg (1 - ρ)]Paper 1c, Section 3: The Participation Game