Documentation

Lean 4 Proof

theorem herfindahl_increases_on_exit {H a_m : ℝ}
    (ha_pos : 0 < a_m) (ha_lt : a_m < 1)
    (hH_pos : 0 < H) (_hH_lt : H < 1)
    (ha_small : a_m < 2 * H / (1 + H)) :
    H < postExitHerfindahl H a_m := by
  simp only [postExitHerfindahl]
  have h1am_pos : (0 : ℝ) < 1 - a_m := by linarith
  rw [lt_div_iff₀ (sq_pos_of_pos h1am_pos)]
  -- Need: H · (1-aₘ)² < H - aₘ²
  -- i.e., H - H·(1-aₘ)² < aₘ²... no, rearrange:
  -- H·(1-aₘ)² < H - aₘ²
  -- H·(1 - 2aₘ + aₘ²) < H - aₘ²
  -- H - 2H·aₘ + H·aₘ² < H - aₘ²
  -- -2H·aₘ + H·aₘ² < -aₘ²
  -- aₘ²(H+1) < 2H·aₘ
  -- aₘ(H+1) < 2H  (divide by aₘ > 0)
  -- aₘ < 2H/(1+H)  ✓
  have hH1_pos : 0 < 1 + H := by linarith
  have ha_clear : a_m * (1 + H) < 2 * H := by
    rwa [lt_div_iff₀ hH1_pos] at ha_small
  nlinarith [sq_nonneg a_m, sq_nonneg (1 - a_m), mul_pos ha_pos hH_pos]

Dependency Graph

Location

thesis/CESProofs/Applications/HeterogeneousFirms.lean:90

Module Section

Heterogeneous Firms and the Melitz Connection

In the same file