Basic API for qualitative probabilities

On any Boolean algebra the axioms let a disjoint common context cancel and let disjoint comparisons merge. On sets, a qualitative probability pulls back along preimages (Set.preimage f ⁻¹'o r) and, when the range is not null, along images of an injection.

Main statements

• rel_sup_sup_right_iff, rel_sup_sup_right, rel_sup_sup: context cancellation and merging.
• isQualitativeProbability_image: pulling back along the image of an injection.
• not_isQualitativeProbability_of_isEmpty: an empty carrier has no qualitative probability.
• exists_not_rel_empty_singleton: a finite carrier has a non-null atom.

theorem ComparativeProbability.rel_sup_sup_right_iff {α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [IsQualitativeAdditive r] {a b c : α} (hca : Disjoint c a) (hcb : Disjoint c b) : r (a ⊔ c) (b ⊔ c) ↔ r a b

A common context c disjoint from both sides cancels, so a ⊔ c ≿ b ⊔ c ↔ a ≿ b.

theorem ComparativeProbability.rel_sup_sup_right {α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [IsQualitativeAdditive r] {a b c : α} (h : r a b) (hca : Disjoint c a) (hcb : Disjoint c b) : r (a ⊔ c) (b ⊔ c)

theorem ComparativeProbability.rel_sup_sup {α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [IsQualitativeAdditive r] [IsTrans α r] {a₁ b₁ a₂ b₂ : α} (h₁ : r a₁ b₁) (h₂ : r a₂ b₂) (ha : Disjoint a₁ a₂) (hb : Disjoint b₁ b₂) : r (a₁ ⊔ a₂) (b₁ ⊔ b₂)

Two comparisons with disjoint left parts and disjoint right parts merge into their joins, even with cross overlaps. The proof adds context to each side, passes through b₁ ⊔ a₂, and restores the pivot a₂ ⊓ b₁ by additivity.

Qualitative probabilities on sets

theorem ComparativeProbability.rel_empty {W : Type u_2} {r : Set W → Set W → Prop} [IsLikelihoodMono r] (A : Set W) : r A ∅

Every set is at least as likely as ∅.

theorem ComparativeProbability.not_rel_empty_univ {W : Type u_2} {r : Set W → Set W → Prop} [IsNontrivial r] : ¬r ∅ Set.univ

The whole space is strictly more likely than ∅.

instance ComparativeProbability.instIsQualitativeProbabilitySetPreimagePreimage {α : Type u_1} {W : Type u_2} {r : Set W → Set W → Prop} [IsQualitativeProbability r] (f : W → α) : IsQualitativeProbability (Set.preimage f ⁻¹'o r)

A qualitative probability pulls back along preimages, comparing sets by their preimages.

theorem ComparativeProbability.isQualitativeProbability_image {α : Type u_1} {W : Type u_2} {r : Set W → Set W → Prop} [IsQualitativeProbability r] {f : α → W} (hf : Function.Injective f) (hnt : ¬r ∅ (Set.range f)) : IsQualitativeProbability (Set.image f ⁻¹'o r)

A qualitative probability pulls back along the image of an injection f, comparing sets by their images, when the range of f is not null.

theorem ComparativeProbability.not_isQualitativeProbability_of_isEmpty {W : Type u_2} [IsEmpty W] (r : Set W → Set W → Prop) : ¬IsQualitativeProbability r

An empty carrier has no qualitative probability, since there ∅ = Set.univ.

theorem ComparativeProbability.exists_not_rel_empty_singleton {W : Type u_2} [Fintype W] (r : Set W → Set W → Prop) [IsQualitativeProbability r] : ∃ (i : W), ¬r ∅ {i}

On a finite carrier some atom is not null, since were every singleton at most as likely as ∅, so would be Set.univ.