Scott's theorem

Scott's representation theorem for qualitative probability on a finite set says that an order on the subsets of a finite W is represented by a probability measure iff it satisfies finite cancellation. A comparison A ≿ B between disjoint sets is a sign vector v : W → SignType, A its positive support and B its negative support, and cancellation (Cancellation) says that whenever a multiset of valid comparisons sums to zero as integer vectors, every comparison in it also holds reversed. This is equivalent to the balanced-sequence form FiniteCancellation of Cancellation.lean (cancellation_iff_finiteCancellation).

The hard direction is linear-programming duality over ℚ (Matrix.farkas), on Fin n and transported along Fintype.equivFin. The weight vectors representing the order form a polyhedron, whose normalized points weight the Dirac measures of a representing measure; it is nonempty unless a Farkas certificate exists, a nonnegative weighting of valid comparisons that sums to zero yet weights a strict one. Clearing denominators turns the certificate into a multiset violating Cancellation.

Main declarations

• posSupport, negSupport, comparisonSum: the sign-vector vocabulary.
• Cancellation: Scott's condition in sign-vector form.
• FiniteCancellation.cancellation, Cancellation.finiteCancellation, cancellation_iff_finiteCancellation: the two forms agree.
• Cancellation.transport: cancellation along an equivalence of carriers.
• cancellation_implies_representable: the Farkas direction.
• representable_iff_cancellation, representable_iff_finiteCancellation: Scott's theorem.
• cancellation_of_null_atom: a null atom reduces cancellation to representability one atom down.

References

• [Sco64]
• [KPS59]

Sign vectors as comparisons

def ComparativeProbability.posSupport {W : Type u_1} (v : W → SignType) : Set W

The positive support of a sign vector is the left side of the comparison.

Equations

• ComparativeProbability.posSupport v = {i : W | v i = 1}

def ComparativeProbability.negSupport {W : Type u_1} (v : W → SignType) : Set W

The negative support of a sign vector is the right side of the comparison.

Equations

• ComparativeProbability.negSupport v = {i : W | v i = -1}

@[simp]

theorem ComparativeProbability.mem_posSupport {W : Type u_1} {v : W → SignType} {i : W} : i ∈ posSupport v ↔ v i = 1

@[simp]

theorem ComparativeProbability.mem_negSupport {W : Type u_1} {v : W → SignType} {i : W} : i ∈ negSupport v ↔ v i = -1

@[simp]

theorem ComparativeProbability.posSupport_neg {W : Type u_1} (v : W → SignType) : posSupport (-v) = negSupport v

@[simp]

theorem ComparativeProbability.negSupport_neg {W : Type u_1} (v : W → SignType) : negSupport (-v) = posSupport v

theorem ComparativeProbability.disjoint_posSupport_negSupport {W : Type u_1} (v : W → SignType) : Disjoint (posSupport v) (negSupport v)

def ComparativeProbability.comparisonSum {W : Type u_1} (M : Multiset (W → SignType)) (i : W) : ℤ

comparisonSum M sums a multiset of sign vectors as an integer vector.

Equations

• ComparativeProbability.comparisonSum M i = (Multiset.map (fun (v : W → SignType) => ↑(v i)) M).sum

@[simp]

theorem ComparativeProbability.comparisonSum_zero {W : Type u_1} (i : W) : comparisonSum 0 i = 0

@[simp]

theorem ComparativeProbability.comparisonSum_cons {W : Type u_1} (v : W → SignType) (M : Multiset (W → SignType)) (i : W) : comparisonSum (v ::ₘ M) i = ↑(v i) + comparisonSum M i

@[simp]

theorem ComparativeProbability.comparisonSum_add {W : Type u_1} (M N : Multiset (W → SignType)) (i : W) : comparisonSum (M + N) i = comparisonSum M i + comparisonSum N i

theorem ComparativeProbability.comparisonSum_coe {W : Type u_1} (L : List (W → SignType)) (i : W) : comparisonSum (↑L) i = (List.map (fun (v : W → SignType) => ↑(v i)) L).sum

Scott's condition

def ComparativeProbability.Cancellation {W : Type u_1} (ge : Set W → Set W → Prop) : Prop

Scott's cancellation condition says that when a multiset of valid comparisons sums to zero as integer vectors, every comparison in it also holds reversed.

Equations

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

theorem ComparativeProbability.Cancellation.transport {W : Type u_1} {α : Type u_2} (e : W ≃ α) {r : Set W → Set W → Prop} (h : Cancellation r) : Cancellation (Set.preimage ⇑e ⁻¹'o r)

Cancellation pulls back along an equivalence of carriers.

theorem ComparativeProbability.FiniteCancellation.cancellation {W : Type u_1} {ge : Set W → Set W → Prop} (h : FiniteCancellation ge) : Cancellation ge

The balanced-sequence form implies the sign-vector form.

theorem ComparativeProbability.Cancellation.finiteCancellation {W : Type u_1} (r : Set W → Set W → Prop) [IsQualitativeProbability r] (h : Cancellation r) : FiniteCancellation r

For a qualitative probability the sign-vector form implies the balanced-sequence form, by normalizing every comparison with additivity.

theorem ComparativeProbability.cancellation_iff_finiteCancellation {W : Type u_1} (r : Set W → Set W → Prop) [IsQualitativeProbability r] : Cancellation r ↔ FiniteCancellation r

The two forms of Scott's condition agree on a qualitative probability.

Weighted cancellation

The Farkas certificate is a rational weighting of comparisons; Cancellation handles it once the weights are cleared to natural multiplicities.

The Farkas direction

Scott's theorem

theorem ComparativeProbability.cancellation_implies_representable {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (r : Set W → Set W → Prop) [IsQualitativeProbability r] (h : Cancellation r) : Representable r

Scott's theorem, hard direction. A qualitative probability on a finite carrier satisfying cancellation is represented by a probability measure.

theorem ComparativeProbability.representable_iff_cancellation {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (r : Set W → Set W → Prop) [IsQualitativeProbability r] : Representable r ↔ Cancellation r

Scott's theorem in sign-vector form.

theorem ComparativeProbability.representable_iff_finiteCancellation {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (r : Set W → Set W → Prop) [IsQualitativeProbability r] : Representable r ↔ FiniteCancellation r

Scott's theorem in balanced-sequence form.

theorem ComparativeProbability.cancellation_of_null_atom {n : ℕ} (r : Set (Fin (n + 2)) → Set (Fin (n + 2)) → Prop) [IsQualitativeProbability r] {j : Fin (n + 2)} (hj : r ∅ {j}) (sub : ∀ (r' : Set (Fin (n + 1)) → Set (Fin (n + 1)) → Prop), IsQualitativeProbability r' → Representable r') : Cancellation r

A null atom and representability one cardinality down yield cancellation, by swapping the null atom to position 0 and applying null_elem_reduce.