Lean declarations

def IsPositiveAffineOf EconCSLib @ cef01c7, EconCSLib.Foundation.Utility.AffineTransform

def IsPositiveAffineOf (u v : X → 𝕜) : Prop :=
  ∃ (a b : 𝕜), 0 < a ∧ ∀ x, v x = a * u x + b

theorem IsPositiveAffineOf.preserves_le EconCSLib @ cef01c7, EconCSLib.Foundation.Utility.AffineTransform
A positive affine transform preserves the order: `u x ≤ u y ↔ v x ≤ v y`.
```
theorem IsPositiveAffineOf.preserves_le {u v : X → 𝕜}
    (h : IsPositiveAffineOf u v) (x y : X) :
    u x ≤ u y ↔ v x ≤ v y
```
theorem IsPositiveAffineOf.preserves_representation EconCSLib @ cef01c7, EconCSLib.Foundation.Utility.AffineTransform
If `u` represents a preference, so does any positive affine transform. [MSZ 2.22]
```
theorem IsPositiveAffineOf.preserves_representation [Preorder X] {u v : X → 𝕜}
    (h : IsPositiveAffineOf u v) (hrep : RepresentsPreference u) :
    RepresentsPreference v where
```

theorem IsPositiveAffineOf.symm EconCSLib @ cef01c7, EconCSLib.Foundation.Utility.AffineTransform

theorem IsPositiveAffineOf.symm {u v : X → 𝕜}
    (h : IsPositiveAffineOf u v) : IsPositiveAffineOf v u

Modules: EconCSLib.Foundation.Utility.AffineTransform

Positive Affine Uniqueness Of Utility

If two expected-utility functions represent the same preference over lotteries, then they differ by a positive affine transformation: $$ v(L)=a u(L)+b \quad\text{with}\quad a>0. $$

Conversely, a positive affine transformation of a representing utility function represents the same preference relation.

Proof

Sketch

The order-preserving direction is immediate from $a>0$. For uniqueness, compare the two representations on degenerate lotteries and use linearity over lotteries to extend the affine relation from outcomes to all lotteries.

The Lean library has the positive-affine relation and its order-preservation and inverse lemmas. The full uniqueness theorem for linear utility functionals is still an open theorem target in EconCSLib/Utility/Lottery.lean.

References

[MSZ, Chapter 2, Thm. 2.22] Maschler, Solan, and Zamir, Game Theory. Uniqueness of expected utility up to positive affine transformation.
[MSZ, Chapter 2, Exercise 2.19] Maschler, Solan, and Zamir, Game Theory. Inverse of a positive affine transformation.