Documentation

Lean 4 Proof

theorem concentration_amplifies_exit {ρ H₁ H₂ δ : ℝ}
    (_hρ : ρ < 1) (hH : H₁ < H₂) (hδ : 0 < δ) (_hH₁ : 0 < 1 - H₁)
    (hH₂ : 0 < 1 - H₂) :
    -- Proportional curvature loss is larger when H is higher:
    -- δ/(1-H₂) > δ/(1-H₁) because 1-H₂ < 1-H₁
    δ / (1 - H₁) < δ / (1 - H₂) := by
  apply div_lt_div_of_pos_left hδ hH₂ (by linarith)

Dependency Graph

Location

thesis/CESProofs/Applications/HeterogeneousFirms.lean:160

Module Section

Heterogeneous Firms and the Melitz Connection

In the same file