Documentation

Lean 4 Proof

theorem laborShare_factorAugmented {α ρ A_K K A_L L : ℝ} :
    laborShare α ρ (A_K * K) (A_L * L) =
    (1 - α) * (A_L * L) ^ ρ / factorAugmentedInner α ρ A_K K A_L L := rfl

Dependency Graph

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:264

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file