Documentation

Lean 4 Proof

def netReturnOnCapital (A α ρ K L δ : ℝ) : ℝ :=
  marginalProductK A α ρ K L - δ

Dependency Graph

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:466

Module Section

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

In the same file