Additive utility for pairs

This is Scott 1964, Theorem 3.1.

noncomputable def Scott1964.MeasurementStructures.pairVector {A : Type u} {A' : Type v} (x : A) (x' : A') : A ⊕ A' → ℝ

The incidence vector of a pair, with one coordinate in each summand.

Equations

• Scott1964.MeasurementStructures.pairVector x x' = Pi.single (Sum.inl x) 1 + Pi.single (Sum.inr x') 1

theorem Scott1964.MeasurementStructures.pairVector_injective {A : Type u} {A' : Type v} : Function.Injective (Function.uncurry pairVector)

theorem Scott1964.MeasurementStructures.pairVector_sum_eq_permutations {A : Type u} {A' : Type v} {ι : Type u_1} [Fintype ι] (x y : ι → A) (x' y' : ι → A') (h : ∑ i : ι, pairVector (x i) (x' i) = ∑ i : ι, pairVector (y i) (y' i)) : ∃ (π : Equiv.Perm ι) (σ : Equiv.Perm ι), (∀ (i : ι), y i = x (π i)) ∧ ∀ (i : ι), y' i = x' (σ i)

Equality of sums of incidence vectors gives the two independent permutations of coordinates used in condition (2_V).

def Scott1964.MeasurementStructures.RealizableUtilityPair {A : Type u} {A' : Type v} (V : A → A' → A → A' → Prop) : Prop

A relation on pairs is represented by the sum of two utility functions.

Equations

• Scott1964.MeasurementStructures.RealizableUtilityPair V = ∃ (f : A → ℝ) (f' : A' → ℝ), ∀ (x : A) (x' : A') (y : A) (y' : A'), V x x' y y' ↔ f x + f' x' ≥ f y + f' y'

def Scott1964.MeasurementStructures.PairTotal {A : Type u} {A' : Type v} (V : A → A' → A → A' → Prop) : Prop

Scott 1964, condition (1_V).

Equations

• Scott1964.MeasurementStructures.PairTotal V = ∀ (x : A) (x' : A') (y : A) (y' : A'), V x x' y y' ∨ V y y' x x'

def Scott1964.MeasurementStructures.PairPermutation {A : Type u} {A' : Type v} (V : A → A' → A → A' → Prop) : Prop

Scott 1964, condition (2_V), indexed at length n + 1 so that the distinguished index 0 always exists.

Equations

• One or more equations did not get rendered due to their size.

theorem Scott1964.MeasurementStructures.PairPermutation.transitive {A : Type u} {A' : Type v} {V : A → A' → A → A' → Prop} (hV : PairPermutation V) (p q r : A × A') : V p.1 p.2 q.1 q.2 → V q.1 q.2 r.1 r.2 → V p.1 p.2 r.1 r.2

Scott's observation following (2_V): the permutation condition already implies transitivity.

theorem Scott1964.MeasurementStructures.RealizableUtilityPair.total {A : Type u} {A' : Type v} {V : A → A' → A → A' → Prop} (hV : RealizableUtilityPair V) : PairTotal V

theorem Scott1964.MeasurementStructures.RealizableUtilityPair.permutation {A : Type u} {A' : Type v} {V : A → A' → A → A' → Prop} (hV : RealizableUtilityPair V) : PairPermutation V

theorem Scott1964.MeasurementStructures.RealizableUtilityPair.necessary {A : Type u} {A' : Type v} {V : A → A' → A → A' → Prop} (hV : RealizableUtilityPair V) : PairTotal V ∧ PairPermutation V

theorem Scott1964.MeasurementStructures.theorem_3_1 {A : Type u} {A' : Type v} [Finite A] [Finite A'] (V : A → A' → A → A' → Prop) : RealizableUtilityPair V ↔ PairTotal V ∧ PairPermutation V

Scott 1964, Theorem 3.1 (additive utility for pairs). The result also holds when either coordinate type is empty.