Finite qualitative probability

This file isolates the last step of Scott's proof: a separating functional on atom vectors is normalized to a finitely additive probability.

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

Linear-functional representation of a qualitative relation on event characteristic vectors.

Equations

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

noncomputable def Scott1964.MeasurementStructures.atomWeightFunctional {B : Type u} [BooleanAlgebra B] [Fintype B] (μ : B → ℝ) : ({ a : B // IsAtom a } → ℝ) →ₗ[ℝ] ℝ

Integration of atom vectors against arbitrary real-valued atom weights.

Equations

• Scott1964.MeasurementStructures.atomWeightFunctional μ = { toFun := fun (v : { a : B // IsAtom a } → ℝ) => ∑ a : { a : B // IsAtom a }, v a * μ ↑a, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Scott1964.MeasurementStructures.atomWeightFunctional_apply {B : Type u} [BooleanAlgebra B] [Fintype B] (μ : B → ℝ) (v : { a : B // IsAtom a } → ℝ) : (atomWeightFunctional μ) v = ∑ a : { a : B // IsAtom a }, v a * μ ↑a

theorem Scott1964.MeasurementStructures.atomWeightFunctional_atomVector_signed {B : Type u} [BooleanAlgebra B] [Fintype B] {μ : B → ℝ} (hμ : IsSignedCharge μ) (x : B) : (atomWeightFunctional μ) (atomVector x) = μ x

Atom-weight integration also recovers an arbitrary signed charge.

theorem Scott1964.MeasurementStructures.atomWeightFunctional_atomVector {B : Type u} [BooleanAlgebra B] [Fintype B] {μ : B → ℝ} (hμ : IsProbability μ) (x : B) : (atomWeightFunctional μ) (atomVector x) = μ x

theorem Scott1964.MeasurementStructures.RealizableSignedCharge.atomLinearRepresentation {B : Type u} [BooleanAlgebra B] [Finite B] {R : B → B → Prop} (hR : RealizableSignedCharge R) : AtomLinearRepresentation R

theorem Scott1964.MeasurementStructures.RealizableProbability.atomLinearRepresentation {B : Type u} [BooleanAlgebra B] [Finite B] {R : B → B → Prop} (hR : RealizableProbability R) : AtomLinearRepresentation R

theorem Scott1964.MeasurementStructures.signedCharge_of_atomLinearRepresentation {B : Type u} [BooleanAlgebra B] {R : B → B → Prop} (hR : AtomLinearRepresentation R) : RealizableSignedCharge R

A linear representation on atom vectors induces a signed charge directly. No division by the charge of ⊤ is needed.

theorem Scott1964.MeasurementStructures.probability_of_atomLinearRepresentation {B : Type u} [BooleanAlgebra B] {R : B → B → Prop} (hR : AtomLinearRepresentation R) (hnt : ProbNontrivial R) (hn : ProbNonneg R) : RealizableProbability R

A nondegenerate atom-functional representation normalizes to a finitely additive probability without changing any comparisons.

theorem Scott1964.MeasurementStructures.nonnegative_probability_of_atomLinearRepresentation {B : Type u} [BooleanAlgebra B] {R : B → B → Prop} (hR : AtomLinearRepresentation R) (hnt : ProbNontrivial R) (hn : ProbNonneg R) : ∃ (μ : B → ℝ), IsFinitelyAdditiveProbability μ ∧ ∀ (x y : B), R x y ↔ μ x ≥ μ y

Condition (2_B) makes the normalized signed measure nonnegative.

theorem Scott1964.MeasurementStructures.AtomLinearRepresentation.cancellation {B : Type u} [BooleanAlgebra B] {R : B → B → Prop} (hR : AtomLinearRepresentation R) (n : ℕ) (x y : Fin (n + 1) → B) : (∀ (a : B), IsAtom a → (∑ i : Fin (n + 1), if a ≤ x i then 1 else 0) = ∑ i : Fin (n + 1), if a ≤ y i then 1 else 0) → (∀ (i : Fin (n + 1)), i ≠ finHead n → R (x i) (y i)) → R (y (finHead n)) (x (finHead n))

Every atom-functional representation satisfies Scott's cancellation scheme. This is the easy direction of the finite separation theorem.

theorem Scott1964.MeasurementStructures.AtomLinearRepresentation.probCancellation {B : Type u} [BooleanAlgebra B] {R : B → B → Prop} (hR : AtomLinearRepresentation R) : ProbCancellation R

theorem Scott1964.MeasurementStructures.ProbCancellation.of_atomVector_sum {B : Type u} [BooleanAlgebra B] {R : B → B → Prop} (hR : ProbCancellation R) (n : ℕ) (x y : Fin (n + 1) → B) (hsum : ∑ i : Fin (n + 1), atomVector (x i) = ∑ i : Fin (n + 1), atomVector (y i)) (hweak : ∀ (i : Fin (n + 1)), i ≠ finHead n → R (x i) (y i)) : R (y (finHead n)) (x (finHead n))

The atom-count formulation can equivalently be supplied as an equality of sums of characteristic vectors.

theorem Scott1964.MeasurementStructures.ProbCancellation.refl {B : Type u} [BooleanAlgebra B] {R : B → B → Prop} (hR : ProbCancellation R) (x : B) : R x x

Scott cancellation alone implies reflexivity.

theorem Scott1964.MeasurementStructures.ProbCancellation.transitive {B : Type u} [BooleanAlgebra B] {R : B → B → Prop} (hR : ProbCancellation R) : ProbTransitive R

Scott cancellation implies de Finetti transitivity.

theorem Scott1964.MeasurementStructures.ProbCancellation.disjointUnionInvariant {B : Type u} [BooleanAlgebra B] {R : B → B → Prop} (hR : ProbCancellation R) : ProbDisjointUnionInvariant R

Scott cancellation gives both directions of de Finetti's invariance under adjoining a common disjoint event.

Reduction to Scott's explicit §1 relation theorem

noncomputable def Scott1964.MeasurementStructures.eventOfAtomVector {B : Type u} [BooleanAlgebra B] (v : { a : B // IsAtom a } → ℝ) : B

The event represented by an atom vector in the range of atomVector. Outside that range its value is immaterial.

Equations

• Scott1964.MeasurementStructures.eventOfAtomVector v = if h : ∃ (x : B), Scott1964.MeasurementStructures.atomVector x = v then Classical.choose h else ⊥

@[simp]

theorem Scott1964.MeasurementStructures.eventOfAtomVector_atomVector {B : Type u} [BooleanAlgebra B] [Finite B] (x : B) : eventOfAtomVector (atomVector x) = x

def Scott1964.MeasurementStructures.AtomVectorRelation {B : Type u} [BooleanAlgebra B] (R : B → B → Prop) (u v : { a : B // IsAtom a } → ℝ) : Prop

The relation transported from events to their characteristic vectors.

Equations

• Scott1964.MeasurementStructures.AtomVectorRelation R u v = R (Scott1964.MeasurementStructures.eventOfAtomVector u) (Scott1964.MeasurementStructures.eventOfAtomVector v)

@[simp]

theorem Scott1964.MeasurementStructures.atomVectorRelation_atomVectors {B : Type u} [BooleanAlgebra B] [Finite B] (R : B → B → Prop) (x y : B) : AtomVectorRelation R (atomVector x) (atomVector y) ↔ R x y

theorem Scott1964.MeasurementStructures.atomVector_range_finite {B : Type u} [BooleanAlgebra B] [Finite B] : (Set.range atomVector).Finite

theorem Scott1964.MeasurementStructures.atomVector_range_rational {B : Type u} [BooleanAlgebra B] : LinearInequalities.IsRationalSet (Set.range atomVector)

theorem Scott1964.MeasurementStructures.atomVectorRelation_complete {B : Type u} [BooleanAlgebra B] [Finite B] {R : B → B → Prop} (hR : ProbTotal R) : LinearInequalities.RelationComplete (Set.range atomVector) (AtomVectorRelation R)

theorem Scott1964.MeasurementStructures.atomVectorRelation_sequenceCancellation {B : Type u} [BooleanAlgebra B] [Finite B] {R : B → B → Prop} (hR : ProbCancellation R) : LinearInequalities.RelationSequenceCancellation (Set.range atomVector) (AtomVectorRelation R)

theorem Scott1964.MeasurementStructures.atomLinearRepresentation_of_relationRealizable {B : Type u} [BooleanAlgebra B] [Finite B] {R : B → B → Prop} (hreal : LinearInequalities.RelationRealizable (Set.range atomVector) (AtomVectorRelation R)) : AtomLinearRepresentation R

theorem Scott1964.MeasurementStructures.atomLinearRepresentation_of_total_cancellation {B : Type u} [BooleanAlgebra B] [Finite B] {R : B → B → Prop} (htotal : ProbTotal R) (hcancel : ProbCancellation R) : AtomLinearRepresentation R

Scott's (3_B) and (4_B) produce a linear representation on atom vectors, without any positivity or nondegeneracy assumptions.

theorem Scott1964.MeasurementStructures.RealizableProbability.probCancellation {B : Type u} [BooleanAlgebra B] [Finite B] {R : B → B → Prop} (hR : RealizableProbability R) : ProbCancellation R

theorem Scott1964.MeasurementStructures.RealizableProbability.finiteNecessary {B : Type u} [BooleanAlgebra B] [Finite B] {R : B → B → Prop} (hR : RealizableProbability R) : ProbNontrivial R ∧ ProbNonneg R ∧ ProbTotal R ∧ ProbCancellation R

theorem Scott1964.MeasurementStructures.RealizableSignedCharge.finiteNecessary {B : Type u} [BooleanAlgebra B] [Finite B] {R : B → B → Prop} (hR : RealizableSignedCharge R) : ProbTotal R ∧ ProbCancellation R

theorem Scott1964.MeasurementStructures.scott_p15_signed_charge {B : Type u} [BooleanAlgebra B] [Finite B] (R : B → B → Prop) : RealizableSignedCharge R ↔ ProbTotal R ∧ ProbCancellation R

Scott's p.15 signed-measure claim: (3_B) and (4_B) are exactly the conditions for representation by a finitely additive signed charge.

theorem Scott1964.MeasurementStructures.scott_p15_signed_charge_vector {B : Type u} [BooleanAlgebra B] [Finite B] (R : B → B → Prop) : RealizableSignedCharge R ↔ ProbTotal R ∧ ProbVectorCancellation R

Scott's p.15 claim with literal vector-sum cancellation (4_B).

theorem Scott1964.MeasurementStructures.probability_of_finite_axioms {B : Type u} [BooleanAlgebra B] [Finite B] {R : B → B → Prop} (hnt : ProbNontrivial R) (hn : ProbNonneg R) (htotal : ProbTotal R) (hcancel : ProbCancellation R) : RealizableProbability R

theorem Scott1964.MeasurementStructures.theorem_4_1 {B : Type u} [BooleanAlgebra B] [Finite B] (R : B → B → Prop) : RealizableProbability R ↔ ProbNontrivial R ∧ ProbNonneg R ∧ ProbTotal R ∧ ProbCancellation R

Scott 1964, Theorem 4.1 (subjective probability).

theorem Scott1964.MeasurementStructures.theorem_4_1_vector {B : Type u} [BooleanAlgebra B] [Finite B] (R : B → B → Prop) : RealizableProbability R ↔ ProbNontrivial R ∧ ProbNonneg R ∧ ProbTotal R ∧ ProbVectorCancellation R

Scott 1964, Theorem 4.1, with (4_B) stated literally as equality of sums of atom vectors.