Sections / Section 13: Hierarchical Architecture / equalWeights

Equal Weights

defprovedHierarchy

Documentation

Lean 4 Proof

def equalWeights (J : ℕ) : Fin J → ℝ := fun _ => (1 : ℝ) / J

Dependency Graph

Used by

herfindahl_entry_decrease_index herfindahl_equal_weights

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:33

Module Section

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

In the same file

herfindahlIndex 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