Documentation

Lean 4 Proof

theorem dtcPremium_threshold_sigma_2 {α K L : ℝ}
    (_hK : 0 < K) (_hL : 0 < L) :
    (α / (1 - α)) * (K / L) ^ ((2 : ℝ) - 2) = α / (1 - α) := by
  rw [show (2 : ℝ) - 2 = 0 from by ring]
  simp [rpow_zero]

Dependency Graph

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:214

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file