Documentation

Lean 4 Proof

theorem dtc_bias_invariant_cobbDouglas {K L : ℝ} (_hK : 0 < K) (_hL : 0 < L) :
    dtcEquilibriumBias 1 (K / L) = 1 := by
  simp only [dtcEquilibriumBias]
  rw [show (1 : ℝ) - 1 = 0 from by ring]
  exact rpow_zero _

Dependency Graph

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:322

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file