Equal Productivity Minimizes H

theorem proved Curvature Roles

Documentation

Lean 4 Proof

theorem equal_productivity_minimizes_H (hJ : 0 < J) :
    herfindahlIndex J (fun _ : Fin J => (1 / ↑J : ℝ)) = 1 / ↑J :=
  herfindahl_equal_weights hJ

Dependency Graph

Location

thesis/CESProofs/Applications/HeterogeneousFirms.lean:147

Module Section

Heterogeneous Firms and the Melitz Connection

In the same file

firmContribution exitThreshold postExitHerfindahl exit_when_contribution_below_cost friction_raises_exit_threshold complementarity_compresses_ratio herfindahl_increases_on_exit curvature_decreases_on_exit extensive_margin_curvature_loss concentration_amplifies_exit cascade_exit_feedback melitz_ces_equivalence