CES Is Atkinson Swf

theorem proved Macroeconomics

Documentation

Lean 4 Proof

theorem ces_is_atkinson_swf (J : ℕ) (a : Fin J → ℝ) (ρ : ℝ) (c : Fin J → ℝ) :
    atkinsonSWF J a ρ c = cesFun J a ρ c := rfl

Dependency Graph

Location

thesis/CESProofs/Applications/SocialWelfare.lean:57

Module Section

CES as Atkinson Social Welfare Function

In the same file

crraUtility atkinsonSWF atkinsonIndex inequalityAversion 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