Representability of qualitative probability orders

A qualitative probability is representable when a probability measure induces it. Kraft, Pratt and Seidenberg show that every order on at most four atoms is representable and give a five-atom order that is not. This file holds the predicate and the reductions to disjoint comparisons and past a null atom; CancellationFin4.lean derives the cases up to four atoms from Scott cancellation, and Completeness.lean holds the five-atom counterexample and its padding to every larger size.

Main statements

• Representable: the representability predicate on relations.
• reduce_to_disjoint, null_elem_reduce, perm_repr: the reductions.

References

• [KPS59]

def ComparativeProbability.Representable {W : Type u_1} [MeasurableSpace W] (r : Set W → Set W → Prop) : Prop

A relation on events is representable when some probability measure induces it.

Equations

• ComparativeProbability.Representable r = ∃ (μ : MeasureTheory.Measure W), MeasureTheory.IsProbabilityMeasure μ ∧ ∀ (A B : Set W), r A B ↔ μ B ≤ μ A

Reductions

theorem ComparativeProbability.reduce_to_disjoint {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] {r : Set W → Set W → Prop} [IsQualitativeAdditive r] (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (C D : Set W), Disjoint C D → (r C D ↔ μ D ≤ μ C)) (A B : Set W) : r A B ↔ μ B ≤ μ A

Agreement on disjoint pairs suffices for full representability, since additivity reduces every comparison to a disjoint one.

theorem ComparativeProbability.null_removal_disjoint {W : Type u_1} {r : Set W → Set W → Prop} [IsQualitativeProbability r] (j : W) (hj : r ∅ {j}) (C D : Set W) (hdisj : Disjoint C D) : r C D ↔ r (C \ {j}) (D \ {j})

Removing a null element (r ∅ {j}) from both sides of a disjoint comparison preserves it.

theorem ComparativeProbability.null_elem_reduce {n : ℕ} (r : Set (Fin (n + 2)) → Set (Fin (n + 2)) → Prop) [IsQualitativeProbability r] (hn0 : r ∅ {0}) (hnn : ∃ (i : Fin (n + 1)), ¬r ∅ {i.succ}) (sub_repr : ∀ (r' : Set (Fin (n + 1)) → Set (Fin (n + 1)) → Prop), IsQualitativeProbability r' → Representable r') : Representable r

If atom 0 is null in a qualitative probability on Fin (n+2) and some atom is not, representability reduces along Fin.succ to Fin (n+1).

Transport along equivalences

theorem ComparativeProbability.transfer_repr {W : Type u_1} {α : Type u_2} [MeasurableSpace W] [DiscreteMeasurableSpace W] [MeasurableSpace α] [DiscreteMeasurableSpace α] (e : W ≃ α) (r : Set W → Set W → Prop) (μ : MeasureTheory.Measure α) (hm : ∀ (A B : Set α), (Set.preimage ⇑e ⁻¹'o r) A B ↔ μ B ≤ μ A) (A B : Set W) : r A B ↔ (MeasureTheory.Measure.map (⇑e.symm) μ) B ≤ (MeasureTheory.Measure.map (⇑e.symm) μ) A

theorem ComparativeProbability.perm_null_iff {n : ℕ} (σ : Fin n ≃ Fin n) (r : Set (Fin n) → Set (Fin n) → Prop) (j : Fin n) : (Set.preimage ⇑σ ⁻¹'o r) ∅ {j} ↔ r ∅ {σ.symm j}

j is null in the transport of r along σ exactly when σ.symm j is null in r.

theorem ComparativeProbability.perm_repr {W : Type u_1} {α : Type u_2} [MeasurableSpace W] [DiscreteMeasurableSpace W] [MeasurableSpace α] [DiscreteMeasurableSpace α] (σ : W ≃ α) (r : Set W → Set W → Prop) (h : Representable (Set.preimage ⇑σ ⁻¹'o r)) : Representable r

Representability transports backward along any equivalence.