Documentation

Lean 4 Proof

theorem twoFactorCES_linear (A α K L : ℝ) :
    twoFactorCES A α 1 K L = A * (α * K + (1 - α) * L) := by
  simp only [twoFactorCES, cesInner]
  simp [rpow_one]

Dependency Graph

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:416

Module Section

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

In the same file