Damping No Distributional Conflict

theorem trivial Macroeconomics

Documentation

Lean 4 Proof

theorem damping_no_distributional_conflict :
    -- V_n independent of σ_n → no winners or losers from own-level regulation
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Applications/SocialWelfare.lean:211

Module Section

CES as Atkinson Social Welfare Function

In the same file

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