EconCSLib.Foundation.Utility.Basic

Risk attitudes and their characterizations.

Main definitions

• IsAffineUtility — utility function of the form u(x) = a·x + b
• IsRiskNeutral — utility preserves expected values
• IsLinearUtility — utility linear over lottery mixtures

Main results

• IsAffineUtility.isRiskNeutral — affine utility → risk neutral [MSZ 2.27]
• IsRiskNeutral.isAffine — risk neutral → affine utility [MSZ 2.27]

References

• [MSZ] Chapter 2, Definitions 2.24–2.27

Risk attitudes

def IsAffineUtility {𝕜 : Type u_1} [Field 𝕜] (u : 𝕜 → 𝕜) : Prop

A utility function is affine (linear + constant): u(x) = a·x + b. An agent with an affine utility function is risk neutral. [MSZ 2.24]

Equations

• IsAffineUtility u = ∃ (a : 𝕜) (b : 𝕜), ∀ (x : 𝕜), u x = a * x + b

def IsRiskNeutral {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {I : Type u_2} [Fintype I] (u : 𝕜 → 𝕜) : Prop

Risk neutrality for lotteries over a finite index set I: u(∑ pᵢ·xᵢ) = ∑ pᵢ·u(xᵢ). Equivalent to u being affine. [MSZ 2.27]

Equations

• IsRiskNeutral u = ∀ (p : ↑(stdSimplex 𝕜 I)) (x : I → 𝕜), u (wsum p x) = wsum p (u ∘ x)

theorem IsAffineUtility.isRiskNeutral {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] {u : 𝕜 → 𝕜} (h : IsAffineUtility u) : IsRiskNeutral u

An affine utility function is risk neutral. [MSZ 2.27, easy direction]

theorem IsRiskNeutral.isAffine {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [Nontrivial I] {u : 𝕜 → 𝕜} (h : IsRiskNeutral u) : IsAffineUtility u

Risk neutrality implies affine utility. [MSZ 2.27, hard direction] Requires |I| ≥ 2 so that non-trivial distributions exist.