Conditional probability

Lemmas on mathlib's conditional measure μ[|s] that mathlib does not state: monotonicity in the conditioning event, real-valued forms, pushforwards and products, invariance under scaling with the composition of two Bayesian updates, and conditioning on nested events up to null sets. [UPSTREAM] candidates for Mathlib/Probability/ConditionalProbability.lean.

Evaluation lemmas for conditionals

theorem ProbabilityTheory.cond_le_cond_of_subset {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {u₁ u₂ e : Set Ω} (hu₁ : MeasurableSet u₁) (hu₂ : MeasurableSet u₂) (hsub : u₂ ⊆ u₁) (hent : e ∩ u₁ ⊆ u₂) : μ[e | u₁] ≤ μ[e | u₂]

Conditioning on a subset that sheds only worlds outside e can only raise the conditional probability of e.

theorem ProbabilityTheory.cond_real_apply {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {s : Set Ω} (hs : MeasurableSet s) (e : Set Ω) : μ[|s].real e = μ.real (s ∩ e) / μ.real s

The conditional as a ratio of real-valued masses.

Pushforwards and products

theorem ProbabilityTheory.cond_map {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} {f : Ω → Ω'} (hf : AEMeasurable f μ) {s : Set Ω'} (hs : MeasurableSet s) : (MeasureTheory.Measure.map f μ)[|s] = MeasureTheory.Measure.map f μ[|f ⁻¹' s]

Conditioning a pushforward on a set is pushing forward the conditional on its preimage.

theorem ProbabilityTheory.cond_prod_preimage_fst {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (ν : MeasureTheory.Measure Ω') [MeasureTheory.IsProbabilityMeasure ν] (s : Set Ω) : (μ.prod ν)[|Prod.fst ⁻¹' s] = μ[|s].prod ν

Conditioning a product on an event of its first coordinate conditions the first factor.

Sequential conditioning

Conditioning is scale-invariant, so two Bayesian updates compose: reweighting by f, normalizing, reweighting by g and normalizing again is one reweighting by f * g.

theorem ProbabilityTheory.cond_smul {Ω : Type u_1} [MeasurableSpace Ω] {c : ENNReal} (hc0 : c ≠ 0) (hc : c ≠ ⊤) (μ : MeasureTheory.Measure Ω) (s : Set Ω) : (c • μ)[|s] = μ[|s]

Conditioning is invariant under scaling the measure by a positive finite constant.

theorem ProbabilityTheory.cond_univ_withDensity_mul {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {f g : Ω → ENNReal} (hf : Measurable f) (hg : Measurable g) (hfin : (μ.withDensity f) Set.univ ≠ ⊤) : ((μ.withDensity f)[|Set.univ].withDensity g)[|Set.univ] = (μ.withDensity (f * g))[|Set.univ]

Normalizing after reweighting by f and again after reweighting by g is normalizing once after reweighting by f * g, so two Bayesian updates compose.

Nested events

Conditioning sees an event only up to a null set, so conditioning on an event almost contained in another is conditioning the conditional, and the two conditionals are then comparable.

theorem ProbabilityTheory.cond_congr_set {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {s t : Set Ω} (h : s =ᵐ[μ] t) : μ[|s] = μ[|t]

theorem ProbabilityTheory.cond_cond_of_ae_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {s t : Set Ω} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasurableSet s) (ht : MeasurableSet t) (hst : s ≤ᵐ[μ] t) : μ[|t][|s] = μ[|s]

Conditioning on an event almost contained in another is conditioning the conditional.

theorem ProbabilityTheory.cond_absolutelyContinuous_cond_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {s t : Set Ω} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasurableSet s) (ht : MeasurableSet t) : μ[|s].AbsolutelyContinuous μ[|t] ↔ s ≤ᵐ[μ] t

One conditional is absolutely continuous with respect to another exactly when the first event is almost contained in the second.