Cancellation conditions

A pair of event sequences is balanced when every state lies in equally many events on each side. Finite cancellation, Scott's reformulation of the condition of Kraft, Pratt and Seidenberg, says that when the premise comparisons of a balanced pair hold, the head comparison holds reversed; it characterizes representability by a single additive measure.

Scott.lean proves Scott's theorem in the sign-vector form of the condition and shows the two forms agree (ComparativeProbability.cancellation_iff_finiteCancellation). This file holds the balanced-sequence form and its soundness: the order a finite measure induces, and so every representable qualitative probability order, satisfies finite cancellation.

Main definitions

• BalancedSeqs, FiniteCancellation: balance and finite cancellation.

Main statements

• MeasureTheory.Measure.finiteCancellation, Representable.finiteCancellation: soundness.

References

• [Sco64]
• [KPS59]

noncomputable def ComparativeProbability.seqCount {W : Type u_1} (s : W) (Es : List (Set W)) : ℕ

seqCount s Es counts the events of Es that contain s.

Equations

• ComparativeProbability.seqCount s Es = (List.map (fun (E : Set W) => if s ∈ E then 1 else 0) Es).sum

@[simp]

theorem ComparativeProbability.seqCount_nil {W : Type u_1} (s : W) : seqCount s [] = 0

@[simp]

theorem ComparativeProbability.seqCount_cons {W : Type u_1} (s : W) (E : Set W) (Es : List (Set W)) : seqCount s (E :: Es) = (if s ∈ E then 1 else 0) + seqCount s Es

def ComparativeProbability.BalancedSeqs {W : Type u_1} (Es Fs : List (Set W)) : Prop

Two event sequences are balanced when every state lies in equally many events on the left as on the right.

Equations

• ComparativeProbability.BalancedSeqs Es Fs = ∀ (s : W), ComparativeProbability.seqCount s Es = ComparativeProbability.seqCount s Fs

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

Finite cancellation holds when Y ≿ X for every balanced pair ⟨…, X⟩ / ⟨…, Y⟩ whose premise comparisons all hold. Here prem carries the paired premise events and X, Y are the heads.

Equations

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

Measures satisfy finite cancellation

theorem MeasureTheory.Measure.finiteCancellation {W : Type u_1} [Fintype W] [MeasurableSpace W] [MeasurableSingletonClass W] (μ : Measure W) [IsFiniteMeasure μ] : ComparativeProbability.FiniteCancellation μ.inducedGe

The order a finite measure induces satisfies finite cancellation, since a balanced pair of sequences has equal total measure on its two sides.

theorem ComparativeProbability.Representable.finiteCancellation {W : Type u_1} [Fintype W] [MeasurableSpace W] [MeasurableSingletonClass W] {r : Set W → Set W → Prop} (h : Representable r) : FiniteCancellation r

A representable relation satisfies finite cancellation (the soundness half of Scott's theorem, in balanced-sequence form).