Documentation

Lean 4 Proof

theorem dtc_bias_increases_with_supply_substitute {σ : ℝ} (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 rpow_lt_rpow (le_of_lt (div_pos hK₁ hL))
    (div_lt_div_of_pos_right hK hL) (by linarith)

Dependency Graph

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:299

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file