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

Labor Share

defprovedMacroeconomics

Documentation

Lean 4 Proof

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

Dependency Graph

Used by

capitalShare_eq_one_sub_laborShare laborShare_cobbDouglas mpl_eq_laborShare_times_ypl factorShare_slope_is_rho capitalShare_lt_one factorShare_identity_augmented laborShare_factorAugmented dirtyEnergyShare factorShare_identity factorShare_identity_cobbDouglas laborShare_lt_one laborShare_pos capitalShare_plus_laborShare laborShare_increases_with_kl_ratio_complements shares_sum_one_factorAugmented

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:65

Module Section

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

In the same file

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