Documentation

Lean 4 Proof

def factorAugmentedInner (α ρ A_K K A_L L : ℝ) : ℝ :=
  α * (A_K * K) ^ ρ + (1 - α) * (A_L * L) ^ ρ

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:31

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file