Sections / Section 8: Applied Economics -- Elasticity, Demand, Trade / elasticityOfSubstitution

Elasticity Of Substitution

defprovedFoundationskey theorem

Documentation

Lean 4 Proof

def elasticityOfSubstitution (ρ : ℝ) : ℝ := 1 / (1 - ρ)

Dependency Graph

Used by

sigma_gt_one curvatureK_eq_sigma trade_elasticity_eq_variety_exponent sigma_rho_inverse curvatureK_eq_via_sigma sigma_two_factor gainsFromVariety_eq_trade_gains dualExponent_eq_sigma curvatureK_mul_sigma sigma_pos sigma_eq_one_div sigma_substitutes cesPriceIndex_eq_sigma capital_labor_demand_ratio

Location

thesis/CESProofs/Applications/Economics.lean:52

Module Section

Economics extensions for CES formalization:

In the same file

sigma_pos sigma_gt_one sigma_eq_one_div sigma_rho_inverse curvatureK_eq_sigma dualExponent_eq_sigma sigma_substitutes factorShare factorShare_nonneg factorShare_sum_eq_one factorShare_symmetric_uniform factorShare_le_one escortDistribution factorShare_eq_escort escort_symmetric_eq_uniform qExpectation_eq_factorShare_weighted gainsFromVariety gainsFromVariety_eq_scaling_ratio gainsFromVariety_gt_one gainsFromVariety_eq_trade_gains