Complementarity Compresses Ratio

theorem proved Curvature Roles

Documentation

Lean 4 Proof

theorem complementarity_compresses_ratio {ρ₁ ρ₂ x : ℝ}
    (hρ : ρ₁ < ρ₂) (hx : 1 < x) :
    x ^ ρ₁ < x ^ ρ₂ :=
  rpow_lt_rpow_of_exponent_lt (by linarith) hρ

Dependency Graph

Location

thesis/CESProofs/Applications/HeterogeneousFirms.lean:75

Module Section

Heterogeneous Firms and the Melitz Connection

In the same file

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