Conditional Probability

This file provides the conditional probability API for probability theory, built on mathlib's conditional expectation infrastructure.

Main Definitions

• condProb μ m A: Conditional probability of event A given σ-algebra m Defined as μ[1_A | m] (conditional expectation of the indicator)

Main Results

• condProb_ae_nonneg_le_one: Conditional probability takes values in [0,1] a.e.
• condProb_integral_eq: Integration property: ∫ P[A|m] over B equals μ(A ∩ B)
• condProb_univ, condProb_empty, condProb_compl: Basic properties

All proofs are complete with no sorries.

Conditional Probability

Note: Many lemmas in this file explicitly include {m₀ : MeasurableSpace Ω} as a parameter to work with multiple measurable space structures on Ω (e.g., m₀, m for conditioning). This makes the section variable [MeasurableSpace Ω] unused for those lemmas, requiring set_option linter.unusedSectionVars false before each affected declaration.

noncomputable def Exchangeability.Probability.condProb {Ω : Type u_1} {m₀ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (m : MeasurableSpace Ω) (A : Set Ω) : Ω → ℝ

Conditional probability of an event A given a σ-algebra m. This is the conditional expectation of the indicator function of A.

We define it using mathlib's condexp applied to the indicator function.

Equations

• Exchangeability.Probability.condProb μ m A = μ[A.indicator fun (x : Ω) => 1|m]

theorem Exchangeability.Probability.condProb_def {Ω : Type u_1} [MeasurableSpace Ω] {m₀ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (m : MeasurableSpace Ω) (A : Set Ω) : condProb μ m A = μ[A.indicator fun (x : Ω) => 1|m]

theorem Exchangeability.Probability.condProb_ae_nonneg_le_one {Ω : Type u_1} [MeasurableSpace Ω] {m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (m : MeasurableSpace Ω) (hm : m ≤ m₀) [MeasureTheory.SigmaFinite (μ.trim hm)] {A : Set Ω} (hA : MeasurableSet A) : ∀ᵐ (ω : Ω) ∂μ, 0 ≤ condProb μ m A ω ∧ condProb μ m A ω ≤ 1

Conditional probability takes values in [0,1] almost everywhere.

theorem Exchangeability.Probability.condProb_ae_bound_one {Ω : Type u_1} [MeasurableSpace Ω] {m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (m : MeasurableSpace Ω) (hm : m ≤ m₀) [MeasureTheory.SigmaFinite (μ.trim hm)] (A : Set Ω) (hA : MeasurableSet A) : ∀ᵐ (ω : Ω) ∂μ, ‖μ[A.indicator fun (x : Ω) => 1|m] ω‖ ≤ 1

Uniform bound: conditional probability is in [0,1] a.e. uniformly over A.

theorem Exchangeability.Probability.condProb_integral_eq {Ω : Type u_1} [MeasurableSpace Ω] {m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (m : MeasurableSpace Ω) (hm : m ≤ m₀) [MeasureTheory.SigmaFinite (μ.trim hm)] {A B : Set Ω} (hA : MeasurableSet A) (hB : MeasurableSet B) : ∫ (ω : Ω) in B, condProb μ m A ω ∂μ = (μ (A ∩ B)).toReal

Conditional probability integrates to the expected measure on sets that are measurable with respect to the conditioning σ-algebra.

@[simp]

theorem Exchangeability.Probability.condProb_univ {Ω : Type u_1} [MeasurableSpace Ω] {m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (m : MeasurableSpace Ω) (hm : m ≤ m₀) [MeasureTheory.SigmaFinite (μ.trim hm)] : condProb μ m Set.univ =ᵐ[μ] fun (x : Ω) => 1

@[simp]

theorem Exchangeability.Probability.condProb_empty {Ω : Type u_1} [MeasurableSpace Ω] {m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (m : MeasurableSpace Ω) (hm : m ≤ m₀) : condProb μ m ∅ =ᵐ[μ] fun (x : Ω) => 0

@[simp]

theorem Exchangeability.Probability.condProb_compl {Ω : Type u_1} [MeasurableSpace Ω] {m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (m : MeasurableSpace Ω) (hm : m ≤ m₀) [MeasureTheory.SigmaFinite (μ.trim hm)] {A : Set Ω} (hA : MeasurableSet A) : condProb μ m Aᶜ =ᵐ[μ] fun (ω : Ω) => 1 - condProb μ m A ω