Sections / Section 13: Hierarchical Architecture / herfindahlIndex

Herfindahl Index

defprovedHierarchy

Documentation

Lean 4 Proof

def herfindahlIndex {J : ℕ} (a : Fin J → ℝ) : ℝ :=
  ∑ j, a j ^ 2

Dependency Graph

Used by

Tstar_increasing_in_herfindahl rho_ordering_preserved_general_weights K_deficit_from_concentration rho_ordering_with_herfindahl gen_quadruple_K_pos equal_productivity_minimizes_H herfindahl_entry_decrease_index K_positive_nondegenerate knockout_risk_increases_with_concentration levelHerfindahl generalKeff_nonneg herfindahl_equal_weights K_decreasing_in_herfindahl_sector sectorHerfindahl K_decreasing_in_herfindahl share_variance_eq_H_minus_inv concentration_reduces_max_Keff K_reduction_equal_weights

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:29

Module Section

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

In the same file

equalWeights herfindahl_equal_weights 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