Documentation

Lean 4 Proof

theorem dtcPremium_complement_regime {α σ : ℝ}
    (hα : 0 < α) (hα1 : α < 1) (hσ : σ < 2)
    {K₁ K₂ L : ℝ} (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) (hL : 0 < L)
    (hK : K₁ < K₂) :
    (α / (1 - α)) * (K₂ / L) ^ (σ - 2) <
    (α / (1 - α)) * (K₁ / L) ^ (σ - 2) := by
  have hα_rat : 0 < α / (1 - α) := div_pos hα (by linarith)
  apply mul_lt_mul_of_pos_left _ hα_rat
  have hσ2 : σ - 2 < 0 := by linarith
  exact (Real.rpow_lt_rpow_iff_of_neg (div_pos hK₂ hL) (div_pos hK₁ hL) hσ2).mpr
    (div_lt_div_of_pos_right hK hL)

Dependency Graph

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:224

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file