Atom vectors for finite Boolean algebras

Scott identifies an event with its 0/1 characteristic vector on the atoms. The cancellation identity in Theorem 4.1 is equality of sums of these vectors.

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

The real characteristic vector of an event on Boolean atoms.

Equations

• Scott1964.MeasurementStructures.atomVector x a = if ↑a ≤ x then 1 else 0

@[simp]

theorem Scott1964.MeasurementStructures.atomVector_apply {B : Type u} [BooleanAlgebra B] (x : B) (a : { a : B // IsAtom a }) : atomVector x a = if ↑a ≤ x then 1 else 0

theorem Scott1964.MeasurementStructures.atomVector_bot {B : Type u} [BooleanAlgebra B] : atomVector ⊥ = 0

theorem Scott1964.MeasurementStructures.atomVector_top {B : Type u} [BooleanAlgebra B] : atomVector ⊤ = 1

theorem Scott1964.MeasurementStructures.atomVector_sup_of_disjoint {B : Type u} [BooleanAlgebra B] {x y : B} (hxy : Disjoint x y) : atomVector (x ⊔ y) = atomVector x + atomVector y

theorem Scott1964.MeasurementStructures.atomVector_injective {B : Type u} [BooleanAlgebra B] [Finite B] : Function.Injective atomVector

theorem Scott1964.MeasurementStructures.disjoint_atoms_of_ne {B : Type u} [BooleanAlgebra B] (a b : { a : B // IsAtom a }) (hab : a ≠ b) : Disjoint ↑a ↑b

Distinct Boolean atoms are disjoint.

theorem Scott1964.MeasurementStructures.disjoint_atom_finset_sup {B : Type u} [BooleanAlgebra B] (a : { a : B // IsAtom a }) (s : Finset { a : B // IsAtom a }) (ha : a ∉ s) : Disjoint (↑a) (s.sup fun (b : { a : B // IsAtom a }) => ↑b)

theorem Scott1964.MeasurementStructures.IsSignedCharge.finset_sup_atoms {B : Type u} [BooleanAlgebra B] {μ : B → ℝ} (hμ : IsSignedCharge μ) (s : Finset { a : B // IsAtom a }) : μ (s.sup fun (a : { a : B // IsAtom a }) => ↑a) = ∑ a ∈ s, μ ↑a

A signed charge evaluates a supremum of distinct atoms as the sum of their charges.

theorem Scott1964.MeasurementStructures.IsProbability.finset_sup_atoms {B : Type u} [BooleanAlgebra B] {μ : B → ℝ} (hμ : IsProbability μ) (s : Finset { a : B // IsAtom a }) : μ (s.sup fun (a : { a : B // IsAtom a }) => ↑a) = ∑ a ∈ s, μ ↑a

Finite additivity evaluates a supremum of distinct atoms as the sum of their masses.

noncomputable def Scott1964.MeasurementStructures.atomsBelow {B : Type u} [BooleanAlgebra B] [Fintype B] (x : B) : Finset { a : B // IsAtom a }

The atoms below an event.

Equations

• Scott1964.MeasurementStructures.atomsBelow x = {a : { a : B // IsAtom a } | ↑a ≤ x}

theorem Scott1964.MeasurementStructures.sup_atomsBelow {B : Type u} [BooleanAlgebra B] [Fintype B] (x : B) : ((atomsBelow x).sup fun (a : { a : B // IsAtom a }) => ↑a) = x

theorem Scott1964.MeasurementStructures.IsSignedCharge.eq_sum_atoms {B : Type u} [BooleanAlgebra B] [Fintype B] {μ : B → ℝ} (hμ : IsSignedCharge μ) (x : B) : μ x = ∑ a ∈ atomsBelow x, μ ↑a

Every finitely additive signed charge is the sum of its atom charges.

theorem Scott1964.MeasurementStructures.IsProbability.eq_sum_atoms {B : Type u} [BooleanAlgebra B] [Fintype B] {μ : B → ℝ} (hμ : IsProbability μ) (x : B) : μ x = ∑ a ∈ atomsBelow x, μ ↑a

Every finitely additive probability is the sum of its atom masses.

theorem Scott1964.MeasurementStructures.sum_atomVector_eq_iff {B : Type u} [BooleanAlgebra B] (n : ℕ) (x y : Fin n → B) : ∑ i : Fin n, atomVector (x i) = ∑ i : Fin n, atomVector (y i) ↔ ∀ (a : B), IsAtom a → (∑ i : Fin n, if a ≤ x i then 1 else 0) = ∑ i : Fin n, if a ≤ y i then 1 else 0

Pointwise equality of sums of event vectors is exactly Scott's atom-count identity.

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

Scott 1964, literal condition (4_B): cancellation is stated using equality of sums of the characteristic vectors themselves.

Equations

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

theorem Scott1964.MeasurementStructures.probVectorCancellation_iff_probCancellation {B : Type u} [BooleanAlgebra B] {R : B → B → Prop} : ProbVectorCancellation R ↔ ProbCancellation R

The literal vector-sum and atom-count formulations of (4_B) agree.