Finitely additive probabilities on Boolean algebras

Scott's probabilities are real-valued and finitely additive. This file deliberately does not use Mathlib's countably additive MeasureTheory.Measure: the source works with an arbitrary Boolean algebra and only finite disjoint unions.

structure Scott1964.MeasurementStructures.IsProbability {B : Type u} [BooleanAlgebra B] (μ : B → ℝ) : Prop

A normalized finitely additive probability on a Boolean algebra.

• bot : μ ⊥ = 0
• top : μ ⊤ = 1
• additive (x y : B) : Disjoint x y → μ (x ⊔ y) = μ x + μ y
• nonnegative (x : B) : 0 ≤ μ x

structure Scott1964.MeasurementStructures.IsSignedCharge {B : Type u} [BooleanAlgebra B] (μ : B → ℝ) : Prop

A finitely additive signed charge. Unlike IsProbability, no nonnegativity or normalization is imposed.

• bot : μ ⊥ = 0
• additive (x y : B) : Disjoint x y → μ (x ⊔ y) = μ x + μ y

theorem Scott1964.MeasurementStructures.IsProbability.isSignedCharge {B : Type u} [BooleanAlgebra B] {μ : B → ℝ} (hμ : IsProbability μ) : IsSignedCharge μ

Forgetting positivity and normalization preserves finite additivity.

def Scott1964.MeasurementStructures.IsNonnegative {B : Type u} (μ : B → ℝ) : Prop

Nonnegativity of a finitely additive set function.

Equations

• Scott1964.MeasurementStructures.IsNonnegative μ = ∀ (x : B), 0 ≤ μ x

def Scott1964.MeasurementStructures.IsFinitelyAdditiveProbability {B : Type u} [BooleanAlgebra B] (μ : B → ℝ) : Prop

Compatibility name for a finitely additive probability.

Equations

• Scott1964.MeasurementStructures.IsFinitelyAdditiveProbability μ = Scott1964.MeasurementStructures.IsProbability μ

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

A qualitative ordering is represented exactly by a normalized additive function.

Equations

• Scott1964.MeasurementStructures.RealizableProbability R = ∃ (μ : B → ℝ), Scott1964.MeasurementStructures.IsProbability μ ∧ ∀ (x y : B), R x y ↔ μ x ≥ μ y

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

A qualitative relation is represented by a finitely additive signed charge, with no normalization or positivity requirement.

Equations

• Scott1964.MeasurementStructures.RealizableSignedCharge R = ∃ (μ : B → ℝ), Scott1964.MeasurementStructures.IsSignedCharge μ ∧ ∀ (x y : B), R x y ↔ μ x ≥ μ y

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

A probability representation is also a signed-charge representation.

def Scott1964.MeasurementStructures.StrictlyPreferred {B : Type u} (R : B → B → Prop) (x y : B) : Prop

Scott's strict notation: x ≻ y means that y is not weakly preferred to x.

Equations

• Scott1964.MeasurementStructures.StrictlyPreferred R x y = ¬R y x

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

Scott 1964, condition (1_B): the certain event is strictly above the null event.

Equations

• Scott1964.MeasurementStructures.ProbNontrivial R = (R ⊤ ⊥ ∧ ¬R ⊥ ⊤)

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

Scott 1964, condition (2_B): every event is at least as likely as null.

Equations

• Scott1964.MeasurementStructures.ProbNonneg R = ∀ (x : B), R x ⊥

def Scott1964.MeasurementStructures.ProbTotal {B : Type u} (R : B → B → Prop) : Prop

Scott 1964, condition (3_B): qualitative probabilities are comparable.

Equations

• Scott1964.MeasurementStructures.ProbTotal R = ∀ (x y : B), R x y ∨ R y x

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

Scott 1964, condition (4_B). The equality says that every atom occurs equally often on the two sides.

Equations

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

def Scott1964.MeasurementStructures.ProbTransitive {B : Type u} (R : B → B → Prop) : Prop

Transitivity, de Finetti's condition (iv).

Equations

• Scott1964.MeasurementStructures.ProbTransitive R = ∀ ⦃x y z : B⦄, R x y → R y z → R x z

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

Invariance under adjoining one event disjoint from both sides, de Finetti's condition (v).

Equations

• Scott1964.MeasurementStructures.ProbDisjointUnionInvariant R = ∀ ⦃x y z : B⦄, Disjoint z x → Disjoint z y → (R x y ↔ R (x ⊔ z) (y ⊔ z))

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

De Finetti's five qualitative-probability axioms. Condition (i) is literally ¬ R ⊥ ⊤; it does not include Scott's additional R ⊤ ⊥ conjunct from (1_B).

• nontrivial : ¬R ⊥ ⊤
• bottom (x : B) : R x ⊥
• total : ProbTotal R
• transitive : ProbTransitive R
• disjointUnionInvariant : ProbDisjointUnionInvariant R

theorem Scott1964.MeasurementStructures.IsProbability.compl {B : Type u} [BooleanAlgebra B] {μ : B → ℝ} (hμ : IsProbability μ) (x : B) : μ xᶜ = 1 - μ x

theorem Scott1964.MeasurementStructures.IsSignedCharge.mono_of_nonnegative {B : Type u} [BooleanAlgebra B] {μ : B → ℝ} (hμ : IsSignedCharge μ) (hn : IsNonnegative μ) ⦃x y : B⦄ (hxy : x ≤ y) : μ x ≤ μ y

A nonnegative signed charge is monotone on events.

theorem Scott1964.MeasurementStructures.IsProbability.mono {B : Type u} [BooleanAlgebra B] {μ : B → ℝ} (hμ : IsProbability μ) ⦃x y : B⦄ (hxy : x ≤ y) : μ x ≤ μ y

theorem Scott1964.MeasurementStructures.IsProbability.le_one {B : Type u} [BooleanAlgebra B] {μ : B → ℝ} (hμ : IsProbability μ) (x : B) : μ x ≤ 1

theorem Scott1964.MeasurementStructures.RealizableProbability.nonnegative {B : Type u} [BooleanAlgebra B] {R : B → B → Prop} (hR : RealizableProbability R) : ∃ (μ : B → ℝ), IsFinitelyAdditiveProbability μ ∧ ∀ (x y : B), R x y ↔ μ x ≥ μ y

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

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

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

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

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