Documentation

Lean 4 Proof

theorem dtcPremium_strong_substitute_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 : 0 < σ - 2 := by linarith
  exact rpow_lt_rpow (le_of_lt (div_pos hK₁ hL))
    (div_lt_div_of_pos_right hK hL) hσ2

Dependency Graph

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:240

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file