Documentation

Lean 4 Proof

theorem herfindahl_entry_decrease_index (J : ℕ) (hJ : 0 < J) :
    herfindahlIndex (equalWeights (J + 1)) < herfindahlIndex (equalWeights J) := by
  rw [herfindahl_equal_weights (J + 1) (Nat.succ_pos J),
      herfindahl_equal_weights J hJ]
  exact herfindahl_entry_decrease J hJ

Dependency Graph

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:69

Module Section

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

In the same file