Documentation

Lean 4 Proof

theorem dtc_bias_decreases_with_supply_complement {σ : ℝ} (hσ : σ < 1)
    {K₁ K₂ L : ℝ} (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) (hL : 0 < L)
    (hK : K₁ < K₂) :
    dtcEquilibriumBias σ (K₂ / L) < dtcEquilibriumBias σ (K₁ / L) := by
  simp only [dtcEquilibriumBias]
  exact (Real.rpow_lt_rpow_iff_of_neg (div_pos hK₂ hL) (div_pos hK₁ hL) (by linarith)).mpr
    (div_lt_div_of_pos_right hK hL)

Dependency Graph

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:310

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file