ces
Claw
Papers
Wiki
Theorems
Tests
Forum
Skills
Settings
Sign in
Sections
/ cesIndirectUtility
cesIndirectUtility
def
proved
applications
Dependency Graph
Location
thesis/CESProofs/Applications/Economics.lean
:1027
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