Sections / Section 13: Hierarchical Architecture / equalWeightH

Equal Weight H

defprovedHierarchy

Documentation

Lean 4 Proof

def equalWeightH (J : ℕ) : ℝ := 1 / (J : ℝ)

Dependency Graph

Used by

herfindahl_entry_change herfindahl_entry_decrease

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:53

Module Section

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

In the same file

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