Documentation

Lean 4 Proof

theorem relativeWage_pos {α ρ A_K K A_L L : ℝ}
    (hα : 0 < α) (hα1 : α < 1)
    (hAK : 0 < A_K) (hAL : 0 < A_L) (hK : 0 < K) (hL : 0 < L) :
    0 < relativeWageDTC α ρ A_K K A_L L := by
  simp only [relativeWageDTC]
  apply mul_pos
  · apply mul_pos
    · exact div_pos hα (by linarith)
    · exact rpow_pos_of_pos (div_pos hAK hAL) ρ
  · exact rpow_pos_of_pos (div_pos hK hL) (ρ - 1)

Dependency Graph

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:166

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file