Extensive Margin Curvature Loss

theorem proved Curvature Roles

Documentation

Lean 4 Proof

theorem extensive_margin_curvature_loss {ρ H H' : ℝ}
    (hρ : ρ < 1) (hH : H < H') :
    0 < (1 - ρ) * (H' - H) :=
  mul_pos (by linarith) (by linarith)

Dependency Graph

Location

thesis/CESProofs/Applications/HeterogeneousFirms.lean:134

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 equal_productivity_minimizes_H concentration_amplifies_exit cascade_exit_feedback melitz_ces_equivalence