Herfindahl Entry Change

theorem proved Hierarchy

Documentation

Lean 4 Proof

theorem herfindahl_entry_change (J : ℕ) (hJ : 0 < J) :
    equalWeightH (J + 1) - equalWeightH J < 0 := by
  linarith [herfindahl_entry_decrease J hJ]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:77

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_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