EconCSLib.Foundation.Utility.AffineTransform

Positive affine transformations of utility functions and their properties.

Main definitions

• IsPositiveAffineOf — v is a positive affine transform of u

Main results

• IsPositiveAffineOf.preserves_le — positive affine transform preserves ≤
• IsPositiveAffineOf.preserves_representation — if u represents ≤, so does a·u + b
• IsPositiveAffineOf.symm — positive affine transform is invertible [MSZ Ex 2.19]

References

• [MSZ] Chapter 2, Theorem 2.22

def IsPositiveAffineOf {X : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] (u v : X → 𝕜) : Prop

v is a positive affine transformation of u: v(x) = a · u(x) + b with a > 0. Two utility functions related by a positive affine transform represent the same preference. [MSZ 2.22]

Equations

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

theorem IsPositiveAffineOf.refl {X : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (u : X → 𝕜) : IsPositiveAffineOf u u

Positive affine transformation is reflexive (identity: a=1, b=0).

theorem IsPositiveAffineOf.trans {X : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {u v w : X → 𝕜} (h₁ : IsPositiveAffineOf u v) (h₂ : IsPositiveAffineOf v w) : IsPositiveAffineOf u w

Positive affine transformation is transitive.

theorem IsPositiveAffineOf.preserves_le {X : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {u v : X → 𝕜} (h : IsPositiveAffineOf u v) (x y : X) : u x ≤ u y ↔ v x ≤ v y

A positive affine transform preserves the order: u x ≤ u y ↔ v x ≤ v y.

theorem IsPositiveAffineOf.preserves_representation {X : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Preorder X] {u v : X → 𝕜} (h : IsPositiveAffineOf u v) (hrep : RepresentsPreference u) : RepresentsPreference v

If u represents a preference, so does any positive affine transform. [MSZ 2.22]

theorem IsPositiveAffineOf.symm {X : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {u v : X → 𝕜} (h : IsPositiveAffineOf u v) : IsPositiveAffineOf v u

Positive affine transformation is symmetric (invertible). [MSZ Ex 2.19] If v(x) = a·u(x) + b with a > 0, then u(x) = (1/a)·v(x) + (-b/a).