Documentation

Lean 4 Proof

theorem mpk_linear (A α K L : ℝ) :
    marginalProductK A α 1 K L = A * α := by
  simp only [marginalProductK, cesInner]
  simp [rpow_zero, rpow_one]

Dependency Graph

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:422

Module Section

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

In the same file