Sections / Section 14: Macro -- Two-Factor CES, Growth, Tax / marginalProductK

Marginal Product K

defprovedMacroeconomics

Documentation

Lean 4 Proof

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

Dependency Graph

Used by

euler_factorAugmented mpk_eq_capitalShare_times_ypk solowSteadyState_capitalShare euler_two_factor mpRatio goldenRule_savings_eq_capitalShare marginalProductK_pos solowGoldenRule_savings mp_ratio mpkFactorAugmented netReturnOnCapital capital_labor_demand_ratio mpk_linear

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:48

Module Section

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

In the same file

cesInner twoFactorCES marginalProductL capitalShare laborShare capitalOutputRatio cesInner_pos cesInner_nonneg cesInner_scale cesInner_symmetric twoFactorCES_homogDegOne twoFactorCES_pos capitalShare_plus_laborShare capitalShare_pos capitalShare_lt_one laborShare_pos laborShare_lt_one capitalShare_eq_one_sub_laborShare euler_two_factor mpk_eq_capitalShare_times_ypk