Conditional-probability toolkit: pushforward, products, full-measure events

Category: 1-Mathlib (CSD-free Mathlib upstream candidates).

Four small lemmas about ProbabilityTheory.cond that Mathlib does not currently provide:

• cond_map — conditioning commutes with pushforward: cond (f_*μ) S = f_* (cond μ (f⁻¹S)).
• cond_prod_prod — conditioning a product measure on a product event conditions the factors independently.
• cond_eq_self — conditioning a probability measure on a full-measure event does nothing.
• cond_finsetSum — Bayes for finite mixtures: conditioning a finite mixture is the posterior-weighted mixture of the conditionings, cond (∑ⱼ cⱼ•μⱼ) S = ∑ⱼ (cⱼ·μⱼ(S) / (∑ₖ cₖ•μₖ)(S)) • cond μⱼ S. The degenerate cases ride the ℝ≥0∞ conventions: zero-mass components drop out of both sides, and a zero-mass (or infinite-mass) mixture makes both sides the zero measure.

Provenance

cond_map/cond_prod_prod/cond_eq_self extracted 2026-08-02 from CsdLean4/RecordLayer/JoinLuders.lean (the degenerate-Lüders conditioning bookkeeping); cond_finsetSum added 2026-08-03 for the outcome-conditioned mixed update (CsdLean4/RecordLayer/MixedLuders.lean). Staged here for upstream. Naming and import discipline track Mathlib idiom; intended target Mathlib.Probability.ConditionalProbability.

theorem ProbabilityTheory.cond_map {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) {f : X → Y} (hf : Measurable f) {S : Set Y} (hS : MeasurableSet S) : (MeasureTheory.Measure.map f μ)[|S] = MeasureTheory.Measure.map f μ[|f ⁻¹' S]

Conditioning commutes with pushforward: cond (f_*μ) S = f_* (cond μ (f⁻¹S)).

theorem ProbabilityTheory.cond_prod_prod {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.SFinite μ] (A : Set X) (B : Set Y) : (μ.prod ν)[|A ×ˢ B] = μ[|A].prod ν[|B]

Conditioning a product on a product event conditions the factors independently.

theorem ProbabilityTheory.cond_eq_self {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] {S : Set X} (hS : MeasurableSet S) (h : μ Sᶜ = 0) : μ[|S] = μ

Conditioning a probability measure on a full-measure event does nothing.

theorem ProbabilityTheory.cond_finsetSum {X : Type u_1} [MeasurableSpace X] {ι : Type u_3} (s : Finset ι) (μ : ι → MeasureTheory.Measure X) [∀ (j : ι), MeasureTheory.IsFiniteMeasure (μ j)] (c : ι → ENNReal) {S : Set X} (hS : MeasurableSet S) : (∑ j ∈ s, c j • μ j)[|S] = ∑ j ∈ s, (c j * (μ j) S / (∑ k ∈ s, c k • μ k) S) • (μ j)[|S]

Bayes for finite mixtures: conditioning a finite mixture of finite measures on an event is the posterior-weighted mixture of the conditioned components — the posterior of component j being its prior weight cⱼ times its likelihood μⱼ S, normalised by the mixture's total mass on S. Zero-mass components contribute zero to both sides, and a zero-mass mixture makes both sides the zero measure, so no positivity hypothesis is needed.