Documentation

Lean 4 Proof

def cesInner (α ρ K L : ℝ) : ℝ := α * K ^ ρ + (1 - α) * L ^ ρ

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:31

Module Section

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

In the same file