Lean 4 Proof

theorem herfindahl_merger_increase {a_i a_j : ℝ} (hi : 0 < a_i) (hj : 0 < a_j) :
    0 < (a_i + a_j) ^ 2 - a_i ^ 2 - a_j ^ 2 := by
  rw [herfindahl_merger_formula]
  positivity

Dependency Graph

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:94

Module Section

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

In the same file