Additive contents and the orders they induce

Finitely additive (FinAddMeasure) and qualitatively additive (QualAddMeasure) probability contents on Set W, valued in an ordered field, and the qualitative probability orders they induce.

Main definitions

• FinAddMeasure, QualAddMeasure — with FunLike application m A, ofFintype (discrete contents), map (pushforward).
• QualAddMeasure.toQualitativeProbability, FinAddMeasure.toQualAdd, FinAddMeasure.toQualitativeProbability.

Implementation notes

The contents are generic over an ordered field K: ℝ gives classical [0,1]-valued measures, ℚ the computable theory. On a finite state space the two agree (rational and real linear feasibility coincide), and only ℚ supports the constructive Farkas (Core/Order/FourierMotzkin.lean) and decide-checked models (Representability.lean) behind the representation theorems. FinAddMeasure mirrors mathlib's MeasureTheory.AddContent interface (FunLike, primed axiom fields with unprimed lemmas); re-founding on AddContent itself would trade the ordered-field axioms for monoid-valued contents over a set system with sUnion side conditions, so the structure stays local. FinAddMeasure.inducedGe is Order.Preimage ⇑m (· ≥ ·).

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

A finitely additive probability measure on subsets of W, valued in an ordered field K. The value type is left generic: instantiate at ℚ for the constructive, decide-able representation theory and at ℝ for classical [0,1]-valued measures (see the module docstring).

The measure applies as a function: m A, via FunLike.

• toFun : Set W → K

  The measure function. Apply the measure itself: m A.

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

  Non-negativity. Use the lemma nonneg.

• additive' (A B : Set W) : Disjoint A B → self.toFun (A ∪ B) = self.toFun A + self.toFun B

  Finite additivity on disjoint sets. Use the lemma additive.

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

  Normalization. Use the lemma total.

@[instance_reducible]

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

Equations

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

@[simp]

theorem ComparativeProbability.FinAddMeasure.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₂ : ∀ (A B : Set W), Disjoint A B → f (A ∪ B) = f A + f B) (h₃ : f Set.univ = 1) : ⇑{ toFun := f, nonneg' := h₁, additive' := h₂, total' := h₃ } = f

@[simp]

theorem ComparativeProbability.FinAddMeasure.toFun_eq_coe {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : FinAddMeasure K W) : m.toFun = ⇑m

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

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

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

theorem ComparativeProbability.FinAddMeasure.additive {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : FinAddMeasure K W) {A B : Set W} (h : Disjoint A B) : m (A ∪ B) = m A + m B

@[simp]

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

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

Measure-induced comparative likelihood A ≿ B ↔ μ(A) ≥ μ(B) — the ≿-reading (QualitativeProbability.ge) consumed by the logic layer; the order itself is toQualitativeProbability.

Equations

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

@[simp]

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

μ(∅) = 0 for any finitely additive measure. Follows from additivity: μ(∅ ∪ ∅) = μ(∅) + μ(∅), but ∅ ∪ ∅ = ∅.

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

Subset monotonicity: A ⊆ B → μ(A) ≤ μ(B).

theorem ComparativeProbability.FinAddMeasure.mu_compl {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : FinAddMeasure K W) (A : Set W) : m A + m Aᶜ = 1

Complement measure: μ(A) + μ(Aᶜ) = 1.

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

Qualitative additivity for a finitely additive measure: splitting A and B into the shared part A ∩ B and the private parts cancels the shared part.

@[simp]

theorem ComparativeProbability.FinAddMeasure.sum_mu_singleton {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : FinAddMeasure K W) (S : Finset W) : ∑ i ∈ S, m {i} = m ↑S

The measure of a finite set is the sum of its singleton measures.

def ComparativeProbability.FinAddMeasure.map {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} {α : Type u_3} (f : W → α) (m : FinAddMeasure K W) : FinAddMeasure K α

Pushforward of a finitely additive measure along a map.

Equations

• ComparativeProbability.FinAddMeasure.map f m = { toFun := fun (A : Set α) => m (f ⁻¹' A), nonneg' := ⋯, additive' := ⋯, total' := ⋯ }

@[simp]

theorem ComparativeProbability.FinAddMeasure.map_apply {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} {α : Type u_3} (f : W → α) (m : FinAddMeasure K W) (A : Set α) : (map f m) A = m (f ⁻¹' A)

noncomputable def ComparativeProbability.FinAddMeasure.ofFintype {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} [Fintype W] (w : W → K) (hw : ∀ (i : W), 0 ≤ w i) (hw1 : ∑ i : W, w i = 1) : FinAddMeasure K W

The discrete measure with weight w i on the atom i (the PMF.ofFintype pattern).

Equations

• ComparativeProbability.FinAddMeasure.ofFintype w hw hw1 = { toFun := fun (A : Set W) => ∑ i : W, if i ∈ A then w i else 0, nonneg' := ⋯, additive' := ⋯, total' := ⋯ }

@[simp]

theorem ComparativeProbability.FinAddMeasure.ofFintype_singleton {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} [Fintype W] (w : W → K) (hw : ∀ (i : W), 0 ≤ w i) (hw1 : ∑ i : W, w i = 1) (i : W) : (ofFintype w hw hw1) {i} = w i

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. Unlike FinAddMeasure, this does NOT require μ(A ∪ B) = μ(A) + μ(B) for disjoint A, B. Instead it requires the weaker qualitative additivity condition: μ(A) ≥ μ(B) ↔ μ(A \ B) ≥ μ(B \ A).

Every qualitative probability order on a finite carrier is represented by one (exists_qualAddMeasure_repr), by an affine renormalisation of the dominated-set count.

• toFun : Set W → K

  The measure function. Apply the measure itself: m A.

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

  Non-negativity. 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

  Normalization. Use the lemma total.

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

  Qualitative additivity. 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 := ⋯ }

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)

Qualitative additivity: μ(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

Measure-induced comparative likelihood A ≿ B ↔ μ(A) ≥ μ(B) (the ≿-reading; see FinAddMeasure.inducedGe).

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

Subset monotonicity: A ⊆ B → μ(A) ≤ μ(B). From qualAdd + μ(∅) = 0 + nonneg.

def ComparativeProbability.QualAddMeasure.toQualitativeProbability {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : QualAddMeasure K W) : QualitativeProbability (Set W)

A qualitatively additive measure induces a qualitative probability order.

Equations

• m.toQualitativeProbability = { le := fun (A B : Set W) => m A ≤ m B, mono' := ⋯, nonTrivial := ⋯, total := ⋯, trans' := ⋯, additive := ⋯ }

def ComparativeProbability.FinAddMeasure.toQualAdd {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : FinAddMeasure K W) : QualAddMeasure K W

Every finitely additive measure is qualitatively additive. Proof: μ(A) = μ(A \ B) + μ(A ∩ B) and μ(B) = μ(B \ A) + μ(A ∩ B), so μ(A) ≥ μ(B) ↔ μ(A \ B) ≥ μ(B \ A).

Equations

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

def ComparativeProbability.FinAddMeasure.toQualitativeProbability {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : FinAddMeasure K W) : QualitativeProbability (Set W)

Every finitely additive measure induces a qualitative probability order, through toQualAdd.

Equations

• m.toQualitativeProbability = m.toQualAdd.toQualitativeProbability