Herfindahl Entry Decrease

Documentation

Lean 4 Proof

theorem herfindahl_entry_decrease (J : ℕ) (hJ : 0 < J) :
    equalWeightH (J + 1) < equalWeightH J := by
  simp only [equalWeightH]
  apply div_lt_div_of_pos_left one_pos
  · exact_mod_cast hJ
  · norm_cast
    omega

Dependency Graph

Used by

herfindahl_entry_decrease_index herfindahl_entry_change

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:59

Module Section

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

In the same file

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