Documentation

Lean 4 Proof

theorem laborShare_cobbDouglas {α K L : ℝ}
    (_hK : K ≠ 0) (_hL : L ≠ 0) :
    laborShare α 0 K L = 1 - α := by
  simp only [laborShare, cesInner, rpow_zero]; ring

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:542

Module Section

Two-Factor CES Production Function (Layer 1 of Macro Extension)

In the same file