Qualitative probability orders: basic API #

Consequences of the axioms on any Boolean algebra (disjoint common context cancels; disjoint comparisons merge), and the transport operations on set-carriers: pullback along an injection (comap) and along an equivalence (transport).

Main statements #

QualitativeProbability.sup_le_sup_iff_right, sup_le_sup_right, sup_le_sup.
QualitativeProbability.comap, transport, elim0.

Consequences of the axioms #

source

theorem ComparativeProbability.QualitativeProbability.sup_le_sup_iff_right {α : Type u_1} [BooleanAlgebra α] (sys : QualitativeProbability α) {a b c : α} (hca : Disjoint c a) (hcb : Disjoint c b) :

sys.le (a ⊔ c) (b ⊔ c) ↔ sys.le a b

Disjoint common context cancels: a ⊔ c ≼ b ⊔ c ↔ a ≼ b for c disjoint from both.

source

theorem ComparativeProbability.QualitativeProbability.sup_le_sup_right {α : Type u_1} [BooleanAlgebra α] (sys : QualitativeProbability α) {a b c : α} (h : sys.le a b) (hca : Disjoint c a) (hcb : Disjoint c b) :

sys.le (a ⊔ c) (b ⊔ c)

source

theorem ComparativeProbability.QualitativeProbability.sup_le_sup {α : Type u_1} [BooleanAlgebra α] (sys : QualitativeProbability α) {a₁ b₁ a₂ b₂ : α} (h₁ : sys.le a₁ b₁) (h₂ : sys.le a₂ b₂) (ha : Disjoint a₁ a₂) (hb : Disjoint b₁ b₂) :

sys.le (a₁ ⊔ a₂) (b₁ ⊔ b₂)

Two comparisons with disjoint left parts and disjoint right parts merge into their joins, even with cross overlaps: add context to each side, transit through b₁ ⊔ a₂, then restore the pivot a₂ ⊓ b₁ by additivity.

Transport on set carriers #

source

def ComparativeProbability.QualitativeProbability.comap {α : Type u_1} {W : Type u_2} (f : α → W) (hf : Function.Injective f) (sys : QualitativeProbability (Set W)) (hnt : ¬sys.le (Set.range f) ∅) :

QualitativeProbability (Set α)

Pull back a qualitative probability order along an injection: α-sets compare via their images. Non-triviality requires a witness and must be supplied.

Equations

ComparativeProbability.QualitativeProbability.comap f hf sys hnt = { le := fun (A B : Set α) => sys.le (f '' A) (f '' B), mono' := ⋯, nonTrivial := ⋯, total := ⋯, trans' := ⋯, additive := ⋯ }