Qualitative probability orders

A qualitative probability order on a Boolean algebra α — de Finetti's axioms for "at most as likely as": total, transitive, monotone, non-trivial, and qualitatively additive (a ≼ b ↔ a \\ b ≼ b \\ a). The relation is stored as le and stated in ≤-vocabulary; the literature's ≿ is the derived ge, mathlib's GE.ge pattern, with scoped notation a ≼[sys] b / a ≿[sys] b.

Main definitions

• QualitativeProbability — the bundled order, with ge, refl, mono, trans, bot_le, le_top.

[UPSTREAM] candidate for Mathlib/Order/Probability/: order theory with a probabilistic reading — no measures occur; the representation theory lives in the sibling files (Content.lean, Scott.lean, Representability.lean, Completeness.lean).

References

[kraft-pratt-seidenberg-1959]

The order

structure ComparativeProbability.QualitativeProbability (α : Type u_1) [BooleanAlgebra α] : Type u_1

A qualitative probability order on a Boolean algebra α: total, transitive, monotone, non-trivial, and qualitatively additive — the standard base system for comparative probability since de Finetti. Every such order on a finite carrier is represented by a qualitatively additive measure (exists_qualAddMeasure_repr), but by a finitely additive one only below five atoms ([kraft-pratt-seidenberg-1959]; Completeness.lean). Reflexivity and ⊥ ≼ a are consequences of monotonicity (refl, bot_le), not fields.

• le : α → α → Prop

  The "at most as likely as" relation.

• mono' (a b : α) : a ≤ b → self.le a b

  Monotonicity: a ≤ b → a ≼ b. Use the lemma mono.

• nonTrivial : ¬self.le ⊤ ⊥

  Non-triviality: ⊤ is not at most as likely as ⊥.

• total (a b : α) : self.le a b ∨ self.le b a

  Totality: any two elements are comparable.

• trans' (a b c : α) : self.le a b → self.le b c → self.le a c

  Transitivity. Use the lemma trans.

• additive (a b : α) : self.le a b ↔ self.le (a \ b) (b \ a)

  Qualitative additivity: a ≼ b ↔ a \ b ≼ b \ a.

def ComparativeProbability.QualitativeProbability.ge {α : Type u_1} [BooleanAlgebra α] (sys : QualitativeProbability α) (a b : α) : Prop

sys.ge a b (a ≿ b): a is at least as likely as b — the converse of le, mathlib's GE.ge pattern. This is the relation the logic layer (Logic/ComparativeProbability/) and the literature read.

Equations

• sys.ge a b = sys.le b a

def ComparativeProbability.QualitativeProbability.«term_≼[_]_» : Lean.TrailingParserDescr

The "at most as likely as" relation.

Equations

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

def ComparativeProbability.QualitativeProbability.«term_≿[_]_» : Lean.TrailingParserDescr

sys.ge a b (a ≿ b): a is at least as likely as b — the converse of le, mathlib's GE.ge pattern. This is the relation the logic layer (Logic/ComparativeProbability/) and the literature read.

Equations

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

@[simp]

theorem ComparativeProbability.QualitativeProbability.ge_iff_le {α : Type u_1} [BooleanAlgebra α] (sys : QualitativeProbability α) {a b : α} : sys.ge a b ↔ sys.le b a

theorem ComparativeProbability.QualitativeProbability.mono {α : Type u_1} [BooleanAlgebra α] (sys : QualitativeProbability α) {a b : α} (h : a ≤ b) : sys.le a b

Monotonicity.

theorem ComparativeProbability.QualitativeProbability.trans {α : Type u_1} [BooleanAlgebra α] (sys : QualitativeProbability α) {a b c : α} (hab : sys.le a b) (hbc : sys.le b c) : sys.le a c

Transitivity.

theorem ComparativeProbability.QualitativeProbability.refl {α : Type u_1} [BooleanAlgebra α] (sys : QualitativeProbability α) (a : α) : sys.le a a

Reflexivity, from monotonicity.

theorem ComparativeProbability.QualitativeProbability.bot_le {α : Type u_1} [BooleanAlgebra α] (sys : QualitativeProbability α) (a : α) : sys.le ⊥ a

theorem ComparativeProbability.QualitativeProbability.le_top {α : Type u_1} [BooleanAlgebra α] (sys : QualitativeProbability α) (a : α) : sys.le a ⊤