Documentation

Lean 4 Proof

theorem factorShare_identity_cobbDouglas {α K L : ℝ}
    (_hα : 0 < α) (_hα1 : α < 1) (hK : 0 < K) (hL : 0 < L) :
    Real.log (laborShare α 0 K L / capitalShare α 0 K L) =
    Real.log ((1 - α) / α) := by
  rw [laborShare_cobbDouglas (ne_of_gt hK) (ne_of_gt hL),
      capitalShare_cobbDouglas (ne_of_gt hK) (ne_of_gt hL)]

Dependency Graph

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:551

Module Section

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

In the same file