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

Escort Distribution

defprovedFoundations

Documentation

Lean 4 Proof

def escortDistribution (J : ℕ) (q : ℝ) (x : Fin J → ℝ) (j : Fin J) : ℝ :=
  (x j) ^ q / ∑ k : Fin J, (x k) ^ q

Dependency Graph

Used by

logit_escort_identity escortDistribution_hod_zero ten_views_one_object escort_logit_bridge factorShare_escort_identity factorShare_eq_escort escortDistribution_is_shareFunction logit_is_ces_at_q_one escort_symmetric_eq_uniform qExpectation_eq_factorShare_weighted

Location

thesis/CESProofs/Applications/Economics.lean:177

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 factorShare_eq_escort escort_symmetric_eq_uniform qExpectation_eq_factorShare_weighted gainsFromVariety gainsFromVariety_eq_scaling_ratio gainsFromVariety_gt_one gainsFromVariety_eq_trade_gains