Documentation

Lean 4 Proof

def crraUtility (c ρ : ℝ) : ℝ := c ^ ρ / ρ

Dependency Graph

Location

thesis/CESProofs/Applications/SocialWelfare.lean:33

Module Section

CES as Atkinson Social Welfare Function

In the same file