Exit When Contribution Below Cost

theorem proved Curvature Roles

Documentation

Lean 4 Proof

theorem exit_when_contribution_below_cost {a x ρ T c : ℝ}
    (h : firmContribution a x ρ < exitThreshold T c) :
    a * x ^ ρ < T * c := h

Dependency Graph

Location

thesis/CESProofs/Applications/HeterogeneousFirms.lean:45

Module Section

Heterogeneous Firms and the Melitz Connection

In the same file

firmContribution exitThreshold postExitHerfindahl 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