Atkinson Swf

def proved Macroeconomics

Documentation

Lean 4 Proof

def atkinsonSWF (J : ℕ) (a : Fin J → ℝ) (ρ : ℝ) (c : Fin J → ℝ) : ℝ :=
  cesFun J a ρ c

Dependency Graph

Used by

atkinsonIndex atkinson_index_zero_at_equality ces_is_atkinson_swf utilitarian_at_rho_one

Location

thesis/CESProofs/Applications/SocialWelfare.lean:37

Module Section

CES as Atkinson Social Welfare Function

In the same file

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