Documentation

Lean 4 Proof

theorem rawlsian_limit :
    -- lim_{ρ→-∞} (Σ aᵢ cᵢ^ρ)^{1/ρ} = min_i(cᵢ)
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Applications/SocialWelfare.lean:178

Module Section

CES as Atkinson Social Welfare Function

In the same file