A modern reconstruction of the infinite probability theorem

Scott's published 1964 paper states and proves the finite theorem, then only announces an unstated infinite extension. The result below adapts Kelley's method and is not presented as Scott's unpublished theorem.

Weak comparisons generate a closed cone in the universal event span, expressed here by its continuous dual polar. The additional generalized Kelley condition gives a countable cover of the strict comparisons by closed convex upper sets. This adapts the countable-cover/separation method of J. L. Kelley, Measures on Boolean Algebras (1959), but the event-span formulation, condition, and theorem statement are not attributed to Kelley. The real Hahn--Banach theorem in HahnBanach.lean, through KelleyCover.exists_combined_separator, then supplies one functional which is nonnegative on every weak comparison and positive on every strict comparison.

noncomputable def Scott1964.MeasurementStructures.Probability.Infinite.comparisonVector (B : Type u) [BooleanAlgebra B] (x y : B) : ↥(EventSpan B)

The signed event-span vector associated with the comparison of x to y.

Equations

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

noncomputable def Scott1964.MeasurementStructures.Probability.Infinite.weakComparisonCone {B : Type u} [BooleanAlgebra B] (R : B → B → Prop) : ProperCone ℝ ↥(EventSpan B)

The closed weak-comparison cone, defined as the intersection of all closed dual half-spaces which contain the declared weak comparisons.

Equations

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

theorem Scott1964.MeasurementStructures.Probability.Infinite.mem_weakComparisonCone_iff {B : Type u} [BooleanAlgebra B] {R : B → B → Prop} {v : ↥(EventSpan B)} : v ∈ weakComparisonCone R ↔ ∀ (L : StrongDual ℝ ↥(EventSpan B)), (∀ (x y : B), R x y → 0 ≤ L (comparisonVector B x y)) → 0 ≤ L v

theorem Scott1964.MeasurementStructures.Probability.Infinite.comparisonVector_mem_weakComparisonCone {B : Type u} [BooleanAlgebra B] {R : B → B → Prop} {x y : B} (hxy : R x y) : comparisonVector B x y ∈ weakComparisonCone R

def Scott1964.MeasurementStructures.Probability.Infinite.strictComparisonSet {B : Type u} [BooleanAlgebra B] (R : B → B → Prop) : Set ↥(EventSpan B)

The set of vectors corresponding to source-strict comparisons x ≻ y, namely ¬ R y x.

Equations

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

theorem Scott1964.MeasurementStructures.Probability.Infinite.comparisonVector_mem_strictComparisonSet {B : Type u} [BooleanAlgebra B] {R : B → B → Prop} {x y : B} (hxy : StrictlyPreferred R x y) : comparisonVector B x y ∈ strictComparisonSet R

def Scott1964.MeasurementStructures.Probability.Infinite.GeneralizedKelleyCondition {B : Type u} [BooleanAlgebra B] (R : B → B → Prop) : Prop

Concrete generalized Kelley condition used by this reconstruction: strict comparison vectors admit a countable Kelley cover above the closed weak cone.

Equations

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

theorem Scott1964.MeasurementStructures.Probability.Infinite.reconstructed_infinite_theorem_4_1 {B : Type u} [BooleanAlgebra B] (R : B → B → Prop) : RealizableProbability R ↔ ProbNontrivial R ∧ ProbNonneg R ∧ ProbTotal R ∧ GeneralizedKelleyCondition R

If-and-only-if characterization of an infinite analogue of Scott's Theorem 4.1, adapting Kelley's 1959 separation method. It is not an attribution of an unpublished theorem to Scott.