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

CES Price Index

defprovedFoundations

Documentation

Lean 4 Proof

def cesPriceIndex (J : ℕ) (ρ : ℝ) (p : Fin J → ℝ) : ℝ :=
  unnormCES J (dualExponent ρ) p

Dependency Graph

Used by

shephards_lemma ces_demand_adding_up cesPriceIndex_def cesUnitCost cesDemand_adding_up cesPriceIndex_eq_sigma

Location

thesis/CESProofs/Applications/Economics.lean:504

Module Section

Economics extensions for CES formalization:

In the same file

elasticityOfSubstitution 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