Documentation

Lean 4 Proof

theorem merger_reduces_curvature {ρ a_i a_j : ℝ}
    (hρ : ρ < 1) (hi : 0 < a_i) (hj : 0 < a_j) :
    -- Curvature change from merger: ΔK = -(1-ρ)·ΔH = -(1-ρ)·2aᵢaⱼ < 0
    (1 - ρ) * (2 * a_i * a_j) > 0 := by
  apply mul_pos (by linarith) (by positivity)

Dependency Graph

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:144

Module Section

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

In the same file