Documentation

Lean 4 Proof

theorem herfindahl_merger_formula {a_i a_j : ℝ} :
    (a_i + a_j) ^ 2 - a_i ^ 2 - a_j ^ 2 = 2 * a_i * a_j := by
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:90

Module Section

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

In the same file