Documentation

Mathlib.Probability.Kernel.CondDistrib

Regular conditional probability distribution #

We define the regular conditional probability distribution of Y : α → Ω given X : α → β, where Ω is a standard Borel space. This is a kernel β Ω such that for almost all a, condDistrib evaluated at X a and a measurable set s is equal to the conditional expectation μ⟦Y ⁻¹' s | mβ.comap X⟧ evaluated at a.

μ⟦Y ⁻¹' s | mβ.comap X⟧ maps a measurable set s to a function α → ℝ≥0∞, and for all s that map is unique up to a μ-null set. For all a, the map from sets to ℝ≥0∞ that we obtain that way verifies some of the properties of a measure, but in general the fact that the μ-null set depends on s can prevent us from finding versions of the conditional expectation that combine into a true measure. The standard Borel space assumption on Ω allows us to do so.

The case Y = X = id is developed in more detail in Probability/Kernel/Condexp.lean: here X is understood as a map from Ω with a sub-σ-algebra m to Ω with its default σ-algebra and the conditional distribution defines a kernel associated with the conditional expectation with respect to m.

Main definitions #

Main statements #

@[irreducible]
noncomputable def ProbabilityTheory.condDistrib {α : Type u_5} {β : Type u_6} {Ω : Type u_7} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] :
{x : MeasurableSpace α} → [inst : MeasurableSpace β] → (αΩ) → (αβ) → (μ : MeasureTheory.Measure α) → [inst_1 : MeasureTheory.IsFiniteMeasure μ] → { x // x ProbabilityTheory.kernel β Ω }

Regular conditional probability distribution: kernel associated with the conditional expectation of Y given X. For almost all a, condDistrib Y X μ evaluated at X a and a measurable set s is equal to the conditional expectation μ⟦Y ⁻¹' s | mβ.comap X⟧ a. It also satisfies the equality μ[(fun a => f (X a, Y a)) | mβ.comap X] =ᵐ[μ] fun a => ∫ y, f (X a, y) ∂(condDistrib Y X μ (X a)) for all integrable functions f.

Instances For
    theorem ProbabilityTheory.condDistrib_def {α : Type u_5} {β : Type u_6} {Ω : Type u_7} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] :
    ∀ {x : MeasurableSpace α} [inst : MeasurableSpace β] (Y : αΩ) (X : αβ) (μ : MeasureTheory.Measure α) [inst_1 : MeasureTheory.IsFiniteMeasure μ], ProbabilityTheory.condDistrib Y X μ = MeasureTheory.Measure.condKernel (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)
    theorem ProbabilityTheory.measurable_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {s : Set Ω} (hs : MeasurableSet s) :
    Measurable fun a => ↑(↑(ProbabilityTheory.condDistrib Y X μ) (X a)) s
    theorem MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {f : β × ΩF} (hY : AEMeasurable Y) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) :
    ((∀ᵐ (a : β) ∂MeasureTheory.Measure.map X μ, MeasureTheory.Integrable fun ω => f (a, ω)) MeasureTheory.Integrable fun a => ∫ (ω : Ω), f (a, ω)↑(ProbabilityTheory.condDistrib Y X μ) a) MeasureTheory.Integrable f
    theorem MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {f : β × ΩF} [NormedSpace F] [CompleteSpace F] (hY : AEMeasurable Y) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) :
    MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y)↑(ProbabilityTheory.condDistrib Y X μ) x) (MeasureTheory.Measure.map X μ)
    theorem MeasureTheory.AEStronglyMeasurable.integral_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {f : β × ΩF} [NormedSpace F] [CompleteSpace F] (hX : AEMeasurable X) (hY : AEMeasurable Y) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) :
    MeasureTheory.AEStronglyMeasurable (fun a => ∫ (y : Ω), f (X a, y)↑(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
    theorem ProbabilityTheory.aestronglyMeasurable'_integral_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {f : β × ΩF} [NormedSpace F] [CompleteSpace F] (hX : AEMeasurable X) (hY : AEMeasurable Y) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) :
    MeasureTheory.AEStronglyMeasurable' (MeasurableSpace.comap X ) (fun a => ∫ (y : Ω), f (X a, y)↑(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
    theorem ProbabilityTheory.integrable_toReal_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {s : Set Ω} (hX : AEMeasurable X) (hs : MeasurableSet s) :
    theorem MeasureTheory.Integrable.condDistrib_ae_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {f : β × ΩF} (hY : AEMeasurable Y) (hf_int : MeasureTheory.Integrable f) :
    ∀ᵐ (b : β) ∂MeasureTheory.Measure.map X μ, MeasureTheory.Integrable fun ω => f (b, ω)
    theorem MeasureTheory.Integrable.condDistrib_ae {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {f : β × ΩF} (hX : AEMeasurable X) (hY : AEMeasurable Y) (hf_int : MeasureTheory.Integrable f) :
    ∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable fun ω => f (X a, ω)
    theorem MeasureTheory.Integrable.integral_norm_condDistrib_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {f : β × ΩF} (hY : AEMeasurable Y) (hf_int : MeasureTheory.Integrable f) :
    MeasureTheory.Integrable fun x => ∫ (y : Ω), f (x, y)↑(ProbabilityTheory.condDistrib Y X μ) x
    theorem MeasureTheory.Integrable.integral_norm_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {f : β × ΩF} (hX : AEMeasurable X) (hY : AEMeasurable Y) (hf_int : MeasureTheory.Integrable f) :
    MeasureTheory.Integrable fun a => ∫ (y : Ω), f (X a, y)↑(ProbabilityTheory.condDistrib Y X μ) (X a)
    theorem MeasureTheory.Integrable.norm_integral_condDistrib_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {f : β × ΩF} [NormedSpace F] [CompleteSpace F] (hY : AEMeasurable Y) (hf_int : MeasureTheory.Integrable f) :
    MeasureTheory.Integrable fun x => ∫ (y : Ω), f (x, y)↑(ProbabilityTheory.condDistrib Y X μ) x
    theorem MeasureTheory.Integrable.norm_integral_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {f : β × ΩF} [NormedSpace F] [CompleteSpace F] (hX : AEMeasurable X) (hY : AEMeasurable Y) (hf_int : MeasureTheory.Integrable f) :
    MeasureTheory.Integrable fun a => ∫ (y : Ω), f (X a, y)↑(ProbabilityTheory.condDistrib Y X μ) (X a)
    theorem MeasureTheory.Integrable.integral_condDistrib_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {f : β × ΩF} [NormedSpace F] [CompleteSpace F] (hY : AEMeasurable Y) (hf_int : MeasureTheory.Integrable f) :
    MeasureTheory.Integrable fun x => ∫ (y : Ω), f (x, y)↑(ProbabilityTheory.condDistrib Y X μ) x
    theorem MeasureTheory.Integrable.integral_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {f : β × ΩF} [NormedSpace F] [CompleteSpace F] (hX : AEMeasurable X) (hY : AEMeasurable Y) (hf_int : MeasureTheory.Integrable f) :
    MeasureTheory.Integrable fun a => ∫ (y : Ω), f (X a, y)↑(ProbabilityTheory.condDistrib Y X μ) (X a)
    theorem ProbabilityTheory.set_lintegral_preimage_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {s : Set Ω} {t : Set β} (hX : Measurable X) (hY : AEMeasurable Y) (hs : MeasurableSet s) (ht : MeasurableSet t) :
    ∫⁻ (a : α) in X ⁻¹' t, ↑(↑(ProbabilityTheory.condDistrib Y X μ) (X a)) sμ = μ (X ⁻¹' t Y ⁻¹' s)
    theorem ProbabilityTheory.set_lintegral_condDistrib_of_measurableSet {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {s : Set Ω} (hX : Measurable X) (hY : AEMeasurable Y) (hs : MeasurableSet s) {t : Set α} (ht : MeasurableSet t) :
    ∫⁻ (a : α) in t, ↑(↑(ProbabilityTheory.condDistrib Y X μ) (X a)) sμ = μ (t Y ⁻¹' s)
    theorem ProbabilityTheory.condDistrib_ae_eq_condexp {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {s : Set Ω} (hX : Measurable X) (hY : Measurable Y) (hs : MeasurableSet s) :

    For almost every a : α, the condDistrib Y X μ kernel applied to X a and a measurable set s is equal to the conditional expectation of the indicator of Y ⁻¹' s.

    theorem ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib' {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {f : β × ΩF} [NormedSpace F] [CompleteSpace F] (hX : Measurable X) (hY : AEMeasurable Y) (hf_int : MeasureTheory.Integrable f) :
    (MeasureTheory.condexp (MeasurableSpace.comap X ) μ fun a => f (X a, Y a)) =ᶠ[MeasureTheory.Measure.ae μ] fun a => ∫ (y : Ω), f (X a, y)↑(ProbabilityTheory.condDistrib Y X μ) (X a)

    The conditional expectation of a function f of the product (X, Y) is almost everywhere equal to the integral of y ↦ f(X, y) against the condDistrib kernel.

    theorem ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib₀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {f : β × ΩF} [NormedSpace F] [CompleteSpace F] (hX : Measurable X) (hY : AEMeasurable Y) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) (hf_int : MeasureTheory.Integrable fun a => f (X a, Y a)) :
    (MeasureTheory.condexp (MeasurableSpace.comap X ) μ fun a => f (X a, Y a)) =ᶠ[MeasureTheory.Measure.ae μ] fun a => ∫ (y : Ω), f (X a, y)↑(ProbabilityTheory.condDistrib Y X μ) (X a)

    The conditional expectation of a function f of the product (X, Y) is almost everywhere equal to the integral of y ↦ f(X, y) against the condDistrib kernel.

    theorem ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} {f : β × ΩF} [NormedSpace F] [CompleteSpace F] (hX : Measurable X) (hY : AEMeasurable Y) (hf : MeasureTheory.StronglyMeasurable f) (hf_int : MeasureTheory.Integrable fun a => f (X a, Y a)) :
    (MeasureTheory.condexp (MeasurableSpace.comap X ) μ fun a => f (X a, Y a)) =ᶠ[MeasureTheory.Measure.ae μ] fun a => ∫ (y : Ω), f (X a, y)↑(ProbabilityTheory.condDistrib Y X μ) (X a)

    The conditional expectation of a function f of the product (X, Y) is almost everywhere equal to the integral of y ↦ f(X, y) against the condDistrib kernel.

    theorem ProbabilityTheory.condexp_ae_eq_integral_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : αβ} {Y : αΩ} {mβ : MeasurableSpace β} [NormedSpace F] [CompleteSpace F] (hX : Measurable X) (hY : AEMeasurable Y) {f : ΩF} (hf : MeasureTheory.StronglyMeasurable f) (hf_int : MeasureTheory.Integrable fun a => f (Y a)) :
    (MeasureTheory.condexp (MeasurableSpace.comap X ) μ fun a => f (Y a)) =ᶠ[MeasureTheory.Measure.ae μ] fun a => ∫ (y : Ω), f y↑(ProbabilityTheory.condDistrib Y X μ) (X a)

    The conditional expectation of Y given X is almost everywhere equal to the integral ∫ y, y ∂(condDistrib Y X μ (X a)).

    theorem MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_mk {β : Type u_2} {mβ : MeasurableSpace β} {Ω : Type u_5} {F : Type u_6} {mΩ : MeasurableSpace Ω} (X : Ωβ) {μ : MeasureTheory.Measure Ω} [TopologicalSpace F] {f : ΩF} (hf : MeasureTheory.AEStronglyMeasurable f μ) :
    MeasureTheory.AEStronglyMeasurable (fun x => f x.snd) (MeasureTheory.Measure.map (fun ω => (X ω, ω)) μ)
    theorem MeasureTheory.Integrable.comp_snd_map_prod_mk {β : Type u_2} {F : Type u_4} [NormedAddCommGroup F] {mβ : MeasurableSpace β} {Ω : Type u_5} {mΩ : MeasurableSpace Ω} (X : Ωβ) {μ : MeasureTheory.Measure Ω} {f : ΩF} (hf_int : MeasureTheory.Integrable f) :
    MeasureTheory.Integrable fun x => f x.snd
    theorem ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prod_mk_iff {β : Type u_2} {mβ : MeasurableSpace β} {Ω : Type u_5} {F : Type u_6} :
    ∀ {x : MeasurableSpace Ω} [inst : TopologicalSpace F] {X : Ωβ} {μ : MeasureTheory.Measure Ω}, Measurable X∀ {f : ΩF}, MeasureTheory.AEStronglyMeasurable (fun x => f x.snd) (MeasureTheory.Measure.map (fun ω => (X ω, ω)) μ) MeasureTheory.AEStronglyMeasurable f μ
    theorem ProbabilityTheory.integrable_comp_snd_map_prod_mk_iff {β : Type u_2} {F : Type u_4} [NormedAddCommGroup F] {mβ : MeasurableSpace β} {Ω : Type u_5} :
    ∀ {x : MeasurableSpace Ω} {X : Ωβ} {μ : MeasureTheory.Measure Ω}, Measurable X∀ {f : ΩF}, (MeasureTheory.Integrable fun x => f x.snd) MeasureTheory.Integrable f