Documentation

Lean 4 Proof

theorem factorAugmentedInner_pos {α ρ A_K K A_L L : ℝ}
    (hα : 0 < α) (hα1 : α < 1)
    (hAK : 0 < A_K) (hK : 0 < K) (hAL : 0 < A_L) (hL : 0 < L) :
    0 < factorAugmentedInner α ρ A_K K A_L L := by
  rw [factorAugmentedInner_eq_cesInner]
  exact cesInner_pos hα hα1 (mul_pos hAK hK) (mul_pos hAL hL)

Dependency Graph

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:82

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file