Documentation

Lean 4 Proof

theorem upstream_reform_pareto :
    -- Reducing σ_{n-1} raises K_eff_n without redistribution
    -- → Pareto improving under any ε > 0
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Applications/SocialWelfare.lean:194

Module Section

CES as Atkinson Social Welfare Function

In the same file