Sections / Section 17: Welfare, Trade, Applications / inequalityAversion

Inequality Aversion

defprovedMacroeconomics

Documentation

Lean 4 Proof

def inequalityAversion (ρ : ℝ) : ℝ := 1 - ρ

Dependency Graph

Used by

lower_rho_more_averse complementarity_alignment surplus_loss_is_welfare_loss no_tradeoff_welfare_interpretation curvature_is_aversion_times_diversity

Location

thesis/CESProofs/Applications/SocialWelfare.lean:48

Module Section

CES as Atkinson Social Welfare Function

In the same file

crraUtility atkinsonSWF atkinsonIndex ces_is_atkinson_swf curvature_is_aversion_times_diversity lower_rho_more_averse no_tradeoff_welfare_interpretation atkinson_index_zero_at_equality atkinson_index_nonneg_equal_weights atkinsonIndex_nonneg_equal_weights utilitarian_at_rho_one rawlsian_limit upstream_reform_pareto damping_no_distributional_conflict surplus_loss_is_welfare_loss complementarity_alignment