Lean declarations

def IsAffineUtility EconCSLib @ cef01c7, EconCSLib.Foundation.Utility.Basic

def IsAffineUtility (u : 𝕜 → 𝕜) : Prop :=
  ∃ (a b : 𝕜), ∀ x, u x = a * x + b

def IsRiskNeutral EconCSLib @ cef01c7, EconCSLib.Foundation.Utility.Basic

def IsRiskNeutral {I : Type*} [Fintype I] (u : 𝕜 → 𝕜) : Prop :=
  ∀ (p : stdSimplex 𝕜 I) (x : I → 𝕜),
    u (wsum p x) = wsum p (u ∘ x)

theorem IsAffineUtility.isRiskNeutral EconCSLib @ cef01c7, EconCSLib.Foundation.Utility.Basic
An affine utility function is risk neutral. [MSZ 2.27, easy direction]
```
theorem IsAffineUtility.isRiskNeutral {I : Type*} [Fintype I] {u : 𝕜 → 𝕜}
    (h : IsAffineUtility u) : IsRiskNeutral (I := I) u
```

theorem IsRiskNeutral.isAffine EconCSLib @ cef01c7, EconCSLib.Foundation.Utility.Basic

theorem IsRiskNeutral.isAffine {I : Type*} [Fintype I] [Nontrivial I] {u : 𝕜 → 𝕜}
    (h : IsRiskNeutral (I := I) u) : IsAffineUtility u

Modules: EconCSLib.Foundation.Utility.Basic

Risk Neutrality

A utility function over monetary outcomes is risk neutral when evaluating the expected monetary payoff first and then applying utility gives the same result as taking the expectation of utility: $$ u\left(\sum_i p_i x_i\right)=\sum_i p_i u(x_i). $$

In the finite setting, this is equivalent to $u$ being affine: $$ u(x)=a x+b. $$

Proof

Sketch

The affine-to-risk-neutral direction follows by distributing the affine formula through the finite weighted sum. For the reverse direction, use two-outcome lotteries to derive preservation of all convex combinations, then recover the affine formula from the values of $u(0)$ and $u(1)$.

References

[MSZ, Chapter 2, Definitions 2.24-2.27] Maschler, Solan, and Zamir, Game Theory. Risk attitudes and risk neutrality.