Atkinson Index

def proved Macroeconomics

Documentation

Lean 4 Proof

def atkinsonIndex (J : ℕ) (a c : Fin J → ℝ) (ρ : ℝ) : ℝ :=
  1 - atkinsonSWF J a ρ c / (∑ j : Fin J, a j * c j)

Dependency Graph

Used by

atkinson_index_zero_at_equality

Location

thesis/CESProofs/Applications/SocialWelfare.lean:44

Module Section

CES as Atkinson Social Welfare Function

In the same file

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