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

Dtc Equilibrium Bias

defprovedMacroeconomics

Documentation

Lean 4 Proof

def dtcEquilibriumBias (σ K_L_ratio : ℝ) : ℝ :=
  K_L_ratio ^ (σ - 1)

Dependency Graph

Used by

dtc_bias_invariant_cobbDouglas dtc_bias_increases_with_supply_substitute dtc_bias_decreases_with_supply_complement

Location

thesis/CESProofs/Macro/DirectedTechnicalChange.lean:59

Module Section

Directed Technical Change Extension (Acemoglu 2002)

In the same file

factorAugmentedInner factorAugmentedCES mpkFactorAugmented mplFactorAugmented relativeWageDTC skillPremiumExponent factorAugmentedInner_eq_cesInner factorAugmentedCES_eq_twoFactorCES factorAugmentedInner_pos factorAugmentedCES_crs euler_factorAugmented rpow_succ_pred relativeWage_formula relativeWage_pos dtcPremium_exponent dtcPremium_threshold_sigma_2 dtcPremium_complement_regime dtcPremium_strong_substitute_regime capitalShare_factorAugmented laborShare_factorAugmented