Herfindahl Merger Max At Equal Split

theorem proved Hierarchy

Documentation

Lean 4 Proof

theorem herfindahl_merger_max_at_equal_split {s : ℝ} (hs : 0 < s)
    {a_i : ℝ} (ha_i : 0 < a_i) (ha_lt : a_i < s) :
    2 * a_i * (s - a_i) ≤ s ^ 2 / 2 := by
  nlinarith [sq_nonneg (a_i - s / 2)]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:103

Module Section

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

In the same file

herfindahlIndex equalWeights herfindahl_equal_weights equalWeightH herfindahl_entry_decrease herfindahl_entry_decrease_index herfindahl_entry_change herfindahl_merger_formula herfindahl_merger_increase herfindahl_exit_increases curvature_decreasing_in_H merger_reduces_curvature antitrust_preserves_curvature entry_term_negative merger_term_positive merger_dominance_condition