Documentation

Lean 4 Proof

theorem sectoral_recession_ordering {J : ℕ} (hJ : 2 ≤ J)
    {ρ1 ρ2 : ℝ} (hρ1 : ρ1 < 1) (hρ2 : ρ2 < 1) (hρ : ρ1 < ρ2)
    {c d_sq : ℝ} (hc : 0 < c) (hd : 0 < d_sq) :
    criticalFriction J ρ1 c d_sq < criticalFriction J ρ2 c d_sq :=
  complementary_goods_more_fragile hJ hρ1 hρ2 hρ hc hd

Dependency Graph

Location

thesis/CESProofs/Potential/MacroApplications.lean:142

Module Section

Macroeconomic Applications of the CES Potential

In the same file