Post Exit Herfindahl

def proved Curvature Roles

Documentation

Lean 4 Proof

def postExitHerfindahl (H a_m : ℝ) : ℝ :=
  (H - a_m ^ 2) / (1 - a_m) ^ 2

Dependency Graph

Used by

herfindahl_increases_on_exit

Location

thesis/CESProofs/Applications/HeterogeneousFirms.lean:36

Module Section

Heterogeneous Firms and the Melitz Connection

In the same file

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