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

Capital Share

defprovedMacroeconomicskey theorem

Documentation

Lean 4 Proof

def capitalShare (α ρ K L : ℝ) : ℝ :=
  α * K ^ ρ / cesInner α ρ K L

Dependency Graph

Used by

capitalShare_eq_one_sub_laborShare factorShare_slope_is_rho mpk_eq_capitalShare_times_ypk solowSteadyState_capitalShare capitalShare_lt_one factorShare_identity_augmented capitalShare_cobbDouglas goldenRule_savings_eq_capitalShare goldenRule_cobbDouglas capitalShare_eq_factorShare factorShare_identity capitalShare_factorAugmented solowGoldenRule_savings factorShare_identity_cobbDouglas capitalShare_plus_laborShare capitalShare_pos cleanShare_rises_with_relative_input_substitute cleanEnergyShare shares_sum_one_factorAugmented

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:60

Module Section

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

In the same file

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