Documentation

Lean 4 Proof

def marginalProductL (A α ρ K L : ℝ) : ℝ :=
  A * (1 - α) * L ^ (ρ - 1) * (cesInner α ρ K L) ^ ((1 - ρ) / ρ)

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:54

Module Section

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

In the same file