Documentation

Lean 4 Proof

theorem shares_sum_one_factorAugmented {α ρ 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) :
    capitalShare α ρ (A_K * K) (A_L * L) +
    laborShare α ρ (A_K * K) (A_L * L) = 1 :=
  capitalShare_plus_laborShare (ρ := ρ) hα hα1 (mul_pos hAK hK) (mul_pos hAL hL)

Dependency Graph

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:269

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file