Sections / Section 13: Hierarchical Architecture / herfindahl_equal_weights

Herfindahl Equal Weights

theoremprovedHierarchy

Documentation

Lean 4 Proof

theorem herfindahl_equal_weights (J : ℕ) (hJ : 0 < J) :
    herfindahlIndex (equalWeights J) = 1 / (J : ℝ) := by
  simp only [herfindahlIndex, equalWeights]
  simp only [Finset.sum_const, Finset.card_fin, nsmul_eq_mul]
  field_simp

Dependency Graph

Used by

equal_productivity_minimizes_H herfindahl_entry_decrease_index

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:41

Module Section

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

In the same file

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