Documentation

Lean 4 Proof

theorem antitrust_preserves_curvature {ρ H₁ H₂ : ℝ}
    (hρ : ρ < 1) (hH12 : H₁ < H₂) (hH1 : 0 ≤ H₁) (hH2 : H₂ < 1) :
    -- K_eff at low H₁ > K_eff at high H₂
    (1 - ρ) * (1 - H₁) > (1 - ρ) * (1 - H₂) := by
  apply mul_lt_mul_of_pos_left _ (by linarith)
  linarith

Dependency Graph

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:153

Module Section

Herfindahl Dynamics: Entry, Exit, and Merger Effects on Concentration

In the same file