# Documentation

Mathlib.Probability.Kernel.Condexp

# Kernel associated with a conditional expectation #

We define condexpKernel μ m, a kernel from Ω to Ω such that for all integrable functions f, μ[f | m] =ᵐ[μ] fun ω => ∫ y, f y ∂(condexpKernel μ m ω).

This kernel is defined if Ω is a standard Borel space. In general, μ⟦s | m⟧ 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 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.

## Main definitions #

• condexpKernel μ m: kernel such that μ[f | m] =ᵐ[μ] fun ω => ∫ y, f y ∂(condexpKernel μ m ω).

## Main statements #

• condexp_ae_eq_integral_condexpKernel: μ[f | m] =ᵐ[μ] fun ω => ∫ y, f y ∂(condexpKernel μ m ω).
theorem MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id {Ω : Type u_1} {F : Type u_2} {m : } {mΩ : } {μ : } {f : ΩF} [] (hm : m ) (hf : ) :
MeasureTheory.AEStronglyMeasurable (fun x => f x.snd) (MeasureTheory.Measure.map (fun ω => (id ω, id ω)) μ)
theorem MeasureTheory.Integrable.comp_snd_map_prod_id {Ω : Type u_1} {F : Type u_2} {m : } {mΩ : } {μ : } {f : ΩF} (hm : m ) (hf : ) :
MeasureTheory.Integrable fun x => f x.snd
theorem ProbabilityTheory.condexpKernel_def {Ω : Type u_3} [] [mΩ : ] [] [] [] (μ : ) (m : ) :
@[irreducible]
noncomputable def ProbabilityTheory.condexpKernel {Ω : Type u_3} [] [mΩ : ] [] [] [] (μ : ) (m : ) :
{ x // }

Kernel associated with the conditional expectation with respect to a σ-algebra. It satisfies μ[f | m] =ᵐ[μ] fun ω => ∫ y, f y ∂(condexpKernel μ m ω). It is defined as the conditional distribution of the identity given the identity, where the second identity is understood as a map from Ω with the σ-algebra mΩ to Ω with σ-algebra m ⊓ mΩ. We use m ⊓ mΩ instead of m to ensure that it is a sub-σ-algebra of mΩ. We then use kernel.comap to get a kernel from m to mΩ instead of from m ⊓ mΩ to mΩ.

Instances For
theorem ProbabilityTheory.condexpKernel_apply_eq_condDistrib {Ω : Type u_1} [] {m : } [mΩ : ] [] [] [] {μ : } {ω : Ω} :
↑() ω = ↑() (id ω)
instance ProbabilityTheory.instIsMarkovKernelCondexpKernel {Ω : Type u_1} [] {m : } [mΩ : ] [] [] [] {μ : } :
theorem ProbabilityTheory.measurable_condexpKernel {Ω : Type u_1} [] {m : } [mΩ : ] [] [] [] {μ : } {s : Set Ω} (hs : ) :
Measurable fun ω => ↑(↑() ω) s
theorem ProbabilityTheory.stronglyMeasurable_condexpKernel {Ω : Type u_1} [] {m : } [mΩ : ] [] [] [] {μ : } {s : Set Ω} (hs : ) :
MeasureTheory.StronglyMeasurable fun ω => ↑(↑() ω) s
theorem MeasureTheory.AEStronglyMeasurable.integral_condexpKernel {Ω : Type u_1} {F : Type u_2} [] {m : } [mΩ : ] [] [] [] {μ : } {f : ΩF} [] [] (hf : ) :
MeasureTheory.AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y↑() ω) μ
theorem ProbabilityTheory.aestronglyMeasurable'_integral_condexpKernel {Ω : Type u_1} {F : Type u_2} [] {m : } [mΩ : ] [] [] [] {μ : } {f : ΩF} [] [] (hf : ) :
MeasureTheory.AEStronglyMeasurable' m (fun ω => ∫ (y : Ω), f y↑() ω) μ
theorem MeasureTheory.Integrable.condexpKernel_ae {Ω : Type u_1} {F : Type u_2} [] {m : } [mΩ : ] [] [] [] {μ : } {f : ΩF} (hf_int : ) :
∀ᵐ (ω : Ω) ∂μ,
theorem MeasureTheory.Integrable.integral_norm_condexpKernel {Ω : Type u_1} {F : Type u_2} [] {m : } [mΩ : ] [] [] [] {μ : } {f : ΩF} (hf_int : ) :
MeasureTheory.Integrable fun ω => ∫ (y : Ω), f y↑() ω
theorem MeasureTheory.Integrable.norm_integral_condexpKernel {Ω : Type u_1} {F : Type u_2} [] {m : } [mΩ : ] [] [] [] {μ : } {f : ΩF} [] [] (hf_int : ) :
MeasureTheory.Integrable fun ω => ∫ (y : Ω), f y↑() ω
theorem MeasureTheory.Integrable.integral_condexpKernel {Ω : Type u_1} {F : Type u_2} [] {m : } [mΩ : ] [] [] [] {μ : } {f : ΩF} [] [] (hf_int : ) :
MeasureTheory.Integrable fun ω => ∫ (y : Ω), f y↑() ω
theorem ProbabilityTheory.integrable_toReal_condexpKernel {Ω : Type u_1} [] {m : } [mΩ : ] [] [] [] {μ : } {s : Set Ω} (hs : ) :
MeasureTheory.Integrable fun ω => ENNReal.toReal (↑(↑() ω) s)
theorem ProbabilityTheory.condexpKernel_ae_eq_condexp' {Ω : Type u_1} [] {m : } [mΩ : ] [] [] [] {μ : } {s : Set Ω} (hs : ) :
(fun ω => ENNReal.toReal (↑(↑() ω) s)) =ᶠ[] MeasureTheory.condexp (m ) μ (Set.indicator s fun ω => 1)
theorem ProbabilityTheory.condexpKernel_ae_eq_condexp {Ω : Type u_1} [] {m : } [mΩ : ] [] [] [] {μ : } (hm : m ) {s : Set Ω} (hs : ) :
(fun ω => ENNReal.toReal (↑(↑() ω) s)) =ᶠ[] MeasureTheory.condexp m μ (Set.indicator s fun ω => 1)
theorem ProbabilityTheory.condexpKernel_ae_eq_trim_condexp {Ω : Type u_1} [] {m : } [mΩ : ] [] [] [] {μ : } (hm : m ) {s : Set Ω} (hs : ) :
(fun ω => ENNReal.toReal (↑(↑() ω) s)) =ᶠ[] MeasureTheory.condexp m μ (Set.indicator s fun ω => 1)
theorem ProbabilityTheory.condexp_ae_eq_integral_condexpKernel' {Ω : Type u_1} {F : Type u_2} [] {m : } [mΩ : ] [] [] [] {μ : } {f : ΩF} [] [] (hf_int : ) :
MeasureTheory.condexp (m ) μ f =ᶠ[] fun ω => ∫ (y : Ω), f y↑() ω
theorem ProbabilityTheory.condexp_ae_eq_integral_condexpKernel {Ω : Type u_1} {F : Type u_2} [] {m : } [mΩ : ] [] [] [] {μ : } {f : ΩF} [] [] (hm : m ) (hf_int : ) :
=ᶠ[] fun ω => ∫ (y : Ω), f y↑() ω

The conditional expectation of f with respect to a σ-algebra m is almost everywhere equal to the integral ∫ y, f y ∂(condexpKernel μ m ω).