Friction Raises Exit Threshold

theorem proved Curvature Roles

Documentation

Lean 4 Proof

theorem friction_raises_exit_threshold {T₁ T₂ c : ℝ}
    (hT : T₁ < T₂) (hc : 0 < c) :
    exitThreshold T₁ c < exitThreshold T₂ c := by
  simp only [exitThreshold]
  exact mul_lt_mul_of_pos_right hT hc

Dependency Graph

Location

thesis/CESProofs/Applications/HeterogeneousFirms.lean:57

Module Section

Heterogeneous Firms and the Melitz Connection

In the same file

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