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

Two Factor CES

defprovedMacroeconomicskey theorem

Documentation

Lean 4 Proof

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

Dependency Graph

Used by

mpl_eq_laborShare_times_ypl twoFactorCES_eq_cesFun factorAugmentedCES_eq_twoFactorCES mpk_eq_capitalShare_times_ypk solowSteadyState_capitalShare euler_two_factor twoFactorCES_homogDegOne capitalOutputRatio energyCES_eq_twoFactorCES goldenRule_savings_eq_capitalShare twoFactorCES_pos solowGoldenRule_savings twoFactorCES_symmetric energyCES twoFactorCES_linear

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:42

Module Section

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

In the same file

cesInner marginalProductK 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