Measures, qualitatively additive contents, and the orders they induce

A probability measure μ on a space in which every event is measurable orders events by A ≿ B ↔ μ B ≤ μ A (Measure.inducedGe). A qualitatively additive measure (QualAddMeasure) need not add over disjoint unions: it fixes the comparison of two events only through their differences. A probability measure is a qualitatively additive measure through its real values μ.real (Measure.toQualAdd), and each kind induces a qualitative probability order.

Main definitions

• QualAddMeasure: qualitatively additive contents, applied as functions m A.
• QualAddMeasure.ofRepr: a normalized function representing a qualitative probability.
• MeasureTheory.Measure.inducedGe: the order a measure induces.
• MeasureTheory.Measure.toQualAdd: a probability measure as a qualitatively additive measure.

Implementation notes

Events are arbitrary subsets, so the carrier is a DiscreteMeasurableSpace, as every finite type with measurable singletons is. A qualitatively additive measure is not a measure, so it stays a structure valued in an ordered field.

Qualitatively additive measures

structure ComparativeProbability.QualAddMeasure (K : Type u_1) [Field K] [LinearOrder K] [IsStrictOrderedRing K] (W : Type u_2) : Type (max u_1 u_2)

A qualitatively additive measure on subsets of W need not add over disjoint unions; it satisfies only the weaker qualitative additivity μ(A) ≥ μ(B) ↔ μ(A \ B) ≥ μ(B \ A). Every qualitative probability order on a finite carrier is represented by one (exists_qualAddMeasure_repr).

• toFun : Set W → K

  toFun A is the measure of A. Apply the measure itself, m A.

• nonneg' (A : Set W) : 0 ≤ self.toFun A

  Every event has nonnegative measure. Use the lemma nonneg.

• empty' : self.toFun ∅ = 0

  The impossible proposition has measure zero. Use the lemma mu_empty.

• total' : self.toFun Set.univ = 1

  The sure event has measure one. Use the lemma total.

• qualAdd' (A B : Set W) : self.toFun A ≤ self.toFun B ↔ self.toFun (A \ B) ≤ self.toFun (B \ A)

  Two events compare as their differences do. Use the lemma qualAdd.

@[instance_reducible]

instance ComparativeProbability.QualAddMeasure.instFunLikeSet {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} : FunLike (QualAddMeasure K W) (Set W) K

Equations

• ComparativeProbability.QualAddMeasure.instFunLikeSet = { coe := ComparativeProbability.QualAddMeasure.toFun, coe_injective := ⋯ }

@[simp]

theorem ComparativeProbability.QualAddMeasure.coe_mk {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (f : Set W → K) (h₁ : ∀ (A : Set W), 0 ≤ f A) (h₂ : f ∅ = 0) (h₃ : f Set.univ = 1) (h₄ : ∀ (A B : Set W), f A ≤ f B ↔ f (A \ B) ≤ f (B \ A)) : ⇑{ toFun := f, nonneg' := h₁, empty' := h₂, total' := h₃, qualAdd' := h₄ } = f

theorem ComparativeProbability.QualAddMeasure.ext {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} {m m' : QualAddMeasure K W} (h : ∀ (A : Set W), m A = m' A) : m = m'

theorem ComparativeProbability.QualAddMeasure.ext_iff {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} {m m' : QualAddMeasure K W} : m = m' ↔ ∀ (A : Set W), m A = m' A

theorem ComparativeProbability.QualAddMeasure.nonneg {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : QualAddMeasure K W) (A : Set W) : 0 ≤ m A

@[simp]

theorem ComparativeProbability.QualAddMeasure.mu_empty {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : QualAddMeasure K W) : m ∅ = 0

@[simp]

theorem ComparativeProbability.QualAddMeasure.total {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : QualAddMeasure K W) : m Set.univ = 1

theorem ComparativeProbability.QualAddMeasure.qualAdd {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : QualAddMeasure K W) (A B : Set W) : m A ≤ m B ↔ m (A \ B) ≤ m (B \ A)

Two events compare as their differences do, μ(A) ≤ μ(B) ↔ μ(A ∖ B) ≤ μ(B ∖ A).

def ComparativeProbability.QualAddMeasure.inducedGe {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : QualAddMeasure K W) (A B : Set W) : Prop

m.inducedGe A B is the comparative likelihood A ≿ B ↔ μ(A) ≥ μ(B) that the measure induces.

Equations

• m.inducedGe A B = (m A ≥ m B)

theorem ComparativeProbability.QualAddMeasure.mu_mono {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : QualAddMeasure K W) {A B : Set W} (h : A ⊆ B) : m A ≤ m B

A qualitatively additive measure is monotone, A ⊆ B → μ(A) ≤ μ(B), by qualitative additivity, μ(∅) = 0 and non-negativity.

instance ComparativeProbability.QualAddMeasure.instIsQualitativeProbabilitySetInducedGe {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : QualAddMeasure K W) : IsQualitativeProbability m.inducedGe

A qualitatively additive measure induces a qualitative probability.

def ComparativeProbability.QualAddMeasure.ofRepr {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} {r : Set W → Set W → Prop} [IsQualitativeProbability r] (f : Set W → K) (hf : ∀ (A B : Set W), r A B ↔ f B ≤ f A) (h0 : f ∅ = 0) (h1 : f Set.univ = 1) : QualAddMeasure K W

A function representing a qualitative probability and normalized to 0 on ∅ and 1 on the whole space is a qualitatively additive measure, nonnegative by monotonicity and qualitatively additive because the order is.

Equations

• ComparativeProbability.QualAddMeasure.ofRepr f hf h0 h1 = { toFun := f, nonneg' := ⋯, empty' := h0, total' := h1, qualAdd' := ⋯ }

theorem ComparativeProbability.QualAddMeasure.inducedGe_ofRepr {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} {r : Set W → Set W → Prop} [IsQualitativeProbability r] (f : Set W → K) (hf : ∀ (A B : Set W), r A B ↔ f B ≤ f A) (h0 : f ∅ = 0) (h1 : f Set.univ = 1) : (ofRepr f hf h0 h1).inducedGe = r

Probability measures

def MeasureTheory.Measure.inducedGe {W : Type u_1} [MeasurableSpace W] (μ : Measure W) (A B : Set W) : Prop

μ.inducedGe A B is the comparative likelihood A ≿ B ↔ μ(A) ≥ μ(B) that the measure induces.

Equations

• μ.inducedGe A B = (μ B ≤ μ A)

theorem MeasureTheory.Measure.inducedGe_iff_real {W : Type u_1} [MeasurableSpace W] (μ : Measure W) [IsFiniteMeasure μ] {A B : Set W} : μ.inducedGe A B ↔ μ.real B ≤ μ.real A

theorem MeasureTheory.Measure.strict_inducedGe_iff_real {W : Type u_1} [MeasurableSpace W] (μ : Measure W) [IsFiniteMeasure μ] {A B : Set W} : ComparativeProbability.Strict μ.inducedGe A B ↔ μ.real B < μ.real A

theorem MeasureTheory.Measure.measure_le_iff_sdiff_le {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] (μ : Measure W) [IsFiniteMeasure μ] (A B : Set W) : μ A ≤ μ B ↔ μ (A \ B) ≤ μ (B \ A)

A finite measure on a discrete space compares two events as it compares their differences, since μ(A) = μ(A \ B) + μ(A ∩ B) and μ(B) = μ(B \ A) + μ(A ∩ B).

noncomputable def MeasureTheory.Measure.toQualAdd {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] (μ : Measure W) [IsProbabilityMeasure μ] : ComparativeProbability.QualAddMeasure ℝ W

A probability measure is qualitatively additive through its real values, since μ(A) = μ(A \ B) + μ(A ∩ B) and μ(B) = μ(B \ A) + μ(A ∩ B).

Equations

• μ.toQualAdd = { toFun := μ.real, nonneg' := ⋯, empty' := ⋯, total' := ⋯, qualAdd' := ⋯ }

@[simp]

theorem MeasureTheory.Measure.toQualAdd_apply {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] (μ : Measure W) [IsProbabilityMeasure μ] (A : Set W) : μ.toQualAdd A = μ.real A

theorem MeasureTheory.Measure.inducedGe_eq_toQualAdd {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] (μ : Measure W) [IsProbabilityMeasure μ] : μ.inducedGe = μ.toQualAdd.inducedGe

instance MeasureTheory.Measure.instIsQualitativeProbabilitySetInducedGe {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] (μ : Measure W) [IsProbabilityMeasure μ] : ComparativeProbability.IsQualitativeProbability μ.inducedGe

A probability measure on a discrete space induces a qualitative probability.