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Ω : MeasurableSpace Ω}
{μ : Measure Ω}
{f : Ω → F}
[TopologicalSpace F]
(hm : LE.le m mΩ)
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (fun (x : Prod Ω Ω) => f x.snd) (Measure.map (fun (ω : Ω) => { fst := id ω, snd := id ω }) μ)
theorem
MeasureTheory.Integrable.comp_snd_map_prod_id
{Ω : Type u_1}
{F : Type u_2}
{m mΩ : MeasurableSpace Ω}
{μ : Measure Ω}
{f : Ω → F}
[NormedAddCommGroup F]
(hm : LE.le m mΩ)
(hf : Integrable f μ)
:
Integrable (fun (x : Prod Ω Ω) => f x.snd) (Measure.map (fun (ω : Ω) => { fst := id ω, snd := id ω }) μ)
@[irreducible]
noncomputable def
ProbabilityTheory.condExpKernel
{Ω : Type u_3}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(m : MeasurableSpace Ω)
:
Kernel Ω Ω
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Ω.
Equations
Instances For
theorem
ProbabilityTheory.condExpKernel_def
{Ω : Type u_3}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(m : MeasurableSpace Ω)
:
Eq (condExpKernel μ m) (if _h : Nonempty Ω then (condDistrib id id μ).comap id ⋯ else 0)
@[deprecated ProbabilityTheory.condExpKernel (since := "2025-01-21")]
def
ProbabilityTheory.condexpKernel
{Ω : Type u_3}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(m : MeasurableSpace Ω)
:
Kernel Ω Ω
Alias of ProbabilityTheory.condExpKernel.
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_eq
{Ω : Type u_1}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
[h : Nonempty Ω]
(m : MeasurableSpace Ω)
:
Eq (condExpKernel μ m) ((condDistrib id id μ).comap id ⋯)
@[deprecated ProbabilityTheory.condExpKernel_eq (since := "2025-01-21")]
theorem
ProbabilityTheory.condexpKernel_eq
{Ω : Type u_1}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
[h : Nonempty Ω]
(m : MeasurableSpace Ω)
:
Eq (condExpKernel μ m) ((condDistrib id id μ).comap id ⋯)
Alias of ProbabilityTheory.condExpKernel_eq.
theorem
ProbabilityTheory.condExpKernel_apply_eq_condDistrib
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[Nonempty Ω]
{ω : Ω}
:
Eq (DFunLike.coe (condExpKernel μ m) ω) (DFunLike.coe (condDistrib id id μ) (id ω))
@[deprecated ProbabilityTheory.condExpKernel_apply_eq_condDistrib (since := "2025-01-21")]
theorem
ProbabilityTheory.condexpKernel_apply_eq_condDistrib
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[Nonempty Ω]
{ω : Ω}
:
Eq (DFunLike.coe (condExpKernel μ m) ω) (DFunLike.coe (condDistrib id id μ) (id ω))
Alias of ProbabilityTheory.condExpKernel_apply_eq_condDistrib.
theorem
ProbabilityTheory.instIsMarkovKernelCondExpKernel
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
:
IsMarkovKernel (condExpKernel μ m)
theorem
ProbabilityTheory.compProd_trim_condExpKernel
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hm : LE.le m mΩ)
:
Eq ((μ.trim hm).compProd (condExpKernel μ m))
(MeasureTheory.Measure.map (fun (ω : Ω) => { fst := id ω, snd := id ω }) μ)
theorem
ProbabilityTheory.condExpKernel_comp_trim
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hm : LE.le m mΩ)
:
Eq ((μ.trim hm).bind (DFunLike.coe (condExpKernel μ m))) μ
theorem
ProbabilityTheory.measurable_condExpKernel
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
(hs : MeasurableSet s)
:
Measurable fun (ω : Ω) => DFunLike.coe (DFunLike.coe (condExpKernel μ m) ω) s
@[deprecated ProbabilityTheory.measurable_condExpKernel (since := "2025-01-21")]
theorem
ProbabilityTheory.measurable_condexpKernel
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
(hs : MeasurableSet s)
:
Measurable fun (ω : Ω) => DFunLike.coe (DFunLike.coe (condExpKernel μ m) ω) s
theorem
ProbabilityTheory.stronglyMeasurable_condExpKernel
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
(hs : MeasurableSet s)
:
MeasureTheory.StronglyMeasurable fun (ω : Ω) => DFunLike.coe (DFunLike.coe (condExpKernel μ m) ω) s
@[deprecated ProbabilityTheory.stronglyMeasurable_condExpKernel (since := "2025-01-21")]
theorem
ProbabilityTheory.stronglyMeasurable_condexpKernel
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
(hs : MeasurableSet s)
:
MeasureTheory.StronglyMeasurable fun (ω : Ω) => DFunLike.coe (DFunLike.coe (condExpKernel μ m) ω) s
Alias of ProbabilityTheory.stronglyMeasurable_condExpKernel.
theorem
MeasureTheory.StronglyMeasurable.integral_condExpKernel'
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (ω : Ω) => integral (DFunLike.coe (ProbabilityTheory.condExpKernel μ m) ω) fun (y : Ω) => f y
theorem
MeasureTheory.StronglyMeasurable.integral_condExpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (ω : Ω) => integral (DFunLike.coe (ProbabilityTheory.condExpKernel μ m) ω) fun (y : Ω) => f y
theorem
MeasureTheory.AEStronglyMeasurable.integral_condExpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (fun (ω : Ω) => integral (DFunLike.coe (ProbabilityTheory.condExpKernel μ m) ω) fun (y : Ω) => f y)
μ
@[deprecated MeasureTheory.AEStronglyMeasurable.integral_condExpKernel (since := "2025-01-21")]
theorem
MeasureTheory.AEStronglyMeasurable.integral_condexpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (fun (ω : Ω) => integral (DFunLike.coe (ProbabilityTheory.condExpKernel μ m) ω) fun (y : Ω) => f y)
μ
Alias of MeasureTheory.AEStronglyMeasurable.integral_condExpKernel.
theorem
ProbabilityTheory.aestronglyMeasurable_integral_condExpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.AEStronglyMeasurable
(fun (ω : Ω) => MeasureTheory.integral (DFunLike.coe (condExpKernel μ m) ω) fun (y : Ω) => f y) μ
@[deprecated ProbabilityTheory.aestronglyMeasurable_integral_condExpKernel (since := "2025-01-24")]
theorem
ProbabilityTheory.aestronglyMeasurable'_integral_condExpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.AEStronglyMeasurable
(fun (ω : Ω) => MeasureTheory.integral (DFunLike.coe (condExpKernel μ m) ω) fun (y : Ω) => f y) μ
Alias of ProbabilityTheory.aestronglyMeasurable_integral_condExpKernel.
@[deprecated ProbabilityTheory.aestronglyMeasurable_integral_condExpKernel (since := "2025-01-21")]
theorem
ProbabilityTheory.aestronglyMeasurable'_integral_condexpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.AEStronglyMeasurable
(fun (ω : Ω) => MeasureTheory.integral (DFunLike.coe (condExpKernel μ m) ω) fun (y : Ω) => f y) μ
Alias of ProbabilityTheory.aestronglyMeasurable_integral_condExpKernel.
theorem
ProbabilityTheory.aestronglyMeasurable_trim_condExpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
(hm : LE.le m mΩ)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
Filter.Eventually
(fun (ω : Ω) =>
(MeasureTheory.ae (DFunLike.coe (condExpKernel μ m) ω)).EventuallyEq f (MeasureTheory.AEStronglyMeasurable.mk f hf))
(MeasureTheory.ae (μ.trim hm))
theorem
MeasureTheory.Integrable.condExpKernel_ae
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
(hf_int : Integrable f μ)
:
Filter.Eventually (fun (ω : Ω) => Integrable f (DFunLike.coe (ProbabilityTheory.condExpKernel μ m) ω)) (ae μ)
@[deprecated MeasureTheory.Integrable.condExpKernel_ae (since := "2025-01-21")]
theorem
MeasureTheory.Integrable.condexpKernel_ae
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
(hf_int : Integrable f μ)
:
Filter.Eventually (fun (ω : Ω) => Integrable f (DFunLike.coe (ProbabilityTheory.condExpKernel μ m) ω)) (ae μ)
theorem
MeasureTheory.Integrable.integral_norm_condExpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
(hf_int : Integrable f μ)
:
Integrable
(fun (ω : Ω) => integral (DFunLike.coe (ProbabilityTheory.condExpKernel μ m) ω) fun (y : Ω) => Norm.norm (f y)) μ
@[deprecated MeasureTheory.Integrable.integral_norm_condExpKernel (since := "2025-01-21")]
theorem
MeasureTheory.Integrable.integral_norm_condexpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
(hf_int : Integrable f μ)
:
Integrable
(fun (ω : Ω) => integral (DFunLike.coe (ProbabilityTheory.condExpKernel μ m) ω) fun (y : Ω) => Norm.norm (f y)) μ
Alias of MeasureTheory.Integrable.integral_norm_condExpKernel.
theorem
MeasureTheory.Integrable.norm_integral_condExpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
(hf_int : Integrable f μ)
:
Integrable
(fun (ω : Ω) => Norm.norm (integral (DFunLike.coe (ProbabilityTheory.condExpKernel μ m) ω) fun (y : Ω) => f y)) μ
@[deprecated MeasureTheory.Integrable.norm_integral_condExpKernel (since := "2025-01-21")]
theorem
MeasureTheory.Integrable.norm_integral_condexpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
(hf_int : Integrable f μ)
:
Integrable
(fun (ω : Ω) => Norm.norm (integral (DFunLike.coe (ProbabilityTheory.condExpKernel μ m) ω) fun (y : Ω) => f y)) μ
Alias of MeasureTheory.Integrable.norm_integral_condExpKernel.
theorem
MeasureTheory.Integrable.integral_condExpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
(hf_int : Integrable f μ)
:
Integrable (fun (ω : Ω) => integral (DFunLike.coe (ProbabilityTheory.condExpKernel μ m) ω) fun (y : Ω) => f y) μ
@[deprecated MeasureTheory.Integrable.integral_condExpKernel (since := "2025-01-21")]
theorem
MeasureTheory.Integrable.integral_condexpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
(hf_int : Integrable f μ)
:
Integrable (fun (ω : Ω) => integral (DFunLike.coe (ProbabilityTheory.condExpKernel μ m) ω) fun (y : Ω) => f y) μ
theorem
ProbabilityTheory.integrable_toReal_condExpKernel
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
(hs : MeasurableSet s)
:
MeasureTheory.Integrable (fun (ω : Ω) => (DFunLike.coe (DFunLike.coe (condExpKernel μ m) ω) s).toReal) μ
@[deprecated ProbabilityTheory.integrable_toReal_condExpKernel (since := "2025-01-21")]
theorem
ProbabilityTheory.integrable_toReal_condexpKernel
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
(hs : MeasurableSet s)
:
MeasureTheory.Integrable (fun (ω : Ω) => (DFunLike.coe (DFunLike.coe (condExpKernel μ m) ω) s).toReal) μ
theorem
ProbabilityTheory.condExpKernel_ae_eq_condExp'
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
(hs : MeasurableSet s)
:
(MeasureTheory.ae μ).EventuallyEq (fun (ω : Ω) => (DFunLike.coe (DFunLike.coe (condExpKernel μ m) ω) s).toReal)
(MeasureTheory.condExp (Min.min m mΩ) μ (s.indicator fun (ω : Ω) => 1))
@[deprecated ProbabilityTheory.condExpKernel_ae_eq_condExp' (since := "2025-01-21")]
theorem
ProbabilityTheory.condexpKernel_ae_eq_condexp'
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
(hs : MeasurableSet s)
:
(MeasureTheory.ae μ).EventuallyEq (fun (ω : Ω) => (DFunLike.coe (DFunLike.coe (condExpKernel μ m) ω) s).toReal)
(MeasureTheory.condExp (Min.min m mΩ) μ (s.indicator fun (ω : Ω) => 1))
theorem
ProbabilityTheory.condExpKernel_ae_eq_condExp
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hm : LE.le m mΩ)
{s : Set Ω}
(hs : MeasurableSet s)
:
(MeasureTheory.ae μ).EventuallyEq (fun (ω : Ω) => (DFunLike.coe (DFunLike.coe (condExpKernel μ m) ω) s).toReal)
(MeasureTheory.condExp m μ (s.indicator fun (ω : Ω) => 1))
@[deprecated ProbabilityTheory.condExpKernel_ae_eq_condExp (since := "2025-01-21")]
theorem
ProbabilityTheory.condexpKernel_ae_eq_condexp
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hm : LE.le m mΩ)
{s : Set Ω}
(hs : MeasurableSet s)
:
(MeasureTheory.ae μ).EventuallyEq (fun (ω : Ω) => (DFunLike.coe (DFunLike.coe (condExpKernel μ m) ω) s).toReal)
(MeasureTheory.condExp m μ (s.indicator fun (ω : Ω) => 1))
theorem
ProbabilityTheory.condExpKernel_ae_eq_trim_condExp
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hm : LE.le m mΩ)
{s : Set Ω}
(hs : MeasurableSet s)
:
(MeasureTheory.ae (μ.trim hm)).EventuallyEq
(fun (ω : Ω) => (DFunLike.coe (DFunLike.coe (condExpKernel μ m) ω) s).toReal)
(MeasureTheory.condExp m μ (s.indicator fun (ω : Ω) => 1))
@[deprecated ProbabilityTheory.condExpKernel_ae_eq_trim_condExp (since := "2025-01-21")]
theorem
ProbabilityTheory.condexpKernel_ae_eq_trim_condexp
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hm : LE.le m mΩ)
{s : Set Ω}
(hs : MeasurableSet s)
:
(MeasureTheory.ae (μ.trim hm)).EventuallyEq
(fun (ω : Ω) => (DFunLike.coe (DFunLike.coe (condExpKernel μ m) ω) s).toReal)
(MeasureTheory.condExp m μ (s.indicator fun (ω : Ω) => 1))
Alias of ProbabilityTheory.condExpKernel_ae_eq_trim_condExp.
theorem
ProbabilityTheory.condExp_ae_eq_integral_condExpKernel'
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
[CompleteSpace F]
(hf_int : MeasureTheory.Integrable f μ)
:
(MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp (Min.min m mΩ) μ f) fun (ω : Ω) =>
MeasureTheory.integral (DFunLike.coe (condExpKernel μ m) ω) fun (y : Ω) => f y
@[deprecated ProbabilityTheory.condExp_ae_eq_integral_condExpKernel' (since := "2025-01-21")]
theorem
ProbabilityTheory.condexp_ae_eq_integral_condexpKernel'
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
[CompleteSpace F]
(hf_int : MeasureTheory.Integrable f μ)
:
(MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp (Min.min m mΩ) μ f) fun (ω : Ω) =>
MeasureTheory.integral (DFunLike.coe (condExpKernel μ m) ω) fun (y : Ω) => f y
Alias of ProbabilityTheory.condExp_ae_eq_integral_condExpKernel'.
theorem
ProbabilityTheory.condExp_ae_eq_integral_condExpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
[CompleteSpace F]
(hm : LE.le m mΩ)
(hf_int : MeasureTheory.Integrable f μ)
:
(MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ f) fun (ω : Ω) =>
MeasureTheory.integral (DFunLike.coe (condExpKernel μ m) ω) 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 ω).
@[deprecated ProbabilityTheory.condExp_ae_eq_integral_condExpKernel (since := "2025-01-21")]
theorem
ProbabilityTheory.condexp_ae_eq_integral_condexpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
[CompleteSpace F]
(hm : LE.le m mΩ)
(hf_int : MeasureTheory.Integrable f μ)
:
(MeasureTheory.ae μ).EventuallyEq (MeasureTheory.condExp m μ f) fun (ω : Ω) =>
MeasureTheory.integral (DFunLike.coe (condExpKernel μ m) ω) fun (y : Ω) => f y
Alias of ProbabilityTheory.condExp_ae_eq_integral_condExpKernel.
The conditional expectation of f with respect to a σ-algebra m is almost everywhere equal to
the integral ∫ y, f y ∂(condExpKernel μ m ω).
theorem
ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
[CompleteSpace F]
(hm : LE.le m mΩ)
(hf : MeasureTheory.StronglyMeasurable f)
(hf_int : MeasureTheory.Integrable f μ)
:
(MeasureTheory.ae (μ.trim hm)).EventuallyEq (MeasureTheory.condExp m μ f) fun (ω : Ω) =>
MeasureTheory.integral (DFunLike.coe (condExpKernel μ m) ω) fun (y : Ω) => f y
Auxiliary lemma for condExp_ae_eq_trim_integral_condExpKernel.
theorem
ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace Real F]
[CompleteSpace F]
(hm : LE.le m mΩ)
(hf_int : MeasureTheory.Integrable f μ)
:
(MeasureTheory.ae (μ.trim hm)).EventuallyEq (MeasureTheory.condExp m μ f) fun (ω : Ω) =>
MeasureTheory.integral (DFunLike.coe (condExpKernel μ m) ω) fun (y : Ω) => f y
The conditional expectation of f with respect to a σ-algebra m is
(μ.trim hm)-almost everywhere equal to the integral ∫ y, f y ∂(condExpKernel μ m ω).
Relation between conditional expectation, conditional kernel and the conditional measure. #
theorem
ProbabilityTheory.condExp_generateFrom_singleton
{Ω : Type u_1}
{F : Type u_2}
[mΩ : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
[NormedAddCommGroup F]
[NormedSpace Real F]
[CompleteSpace F]
(hs : MeasurableSet s)
{f : Ω → F}
(hf : MeasureTheory.Integrable f μ)
:
(MeasureTheory.ae (μ.restrict s)).EventuallyEq
(MeasureTheory.condExp (MeasurableSpace.generateFrom (Singleton.singleton s)) μ f) fun (x : Ω) =>
MeasureTheory.integral (cond μ s) fun (x : Ω) => f x
@[deprecated ProbabilityTheory.condExp_generateFrom_singleton (since := "2025-01-21")]
theorem
ProbabilityTheory.condexp_generateFrom_singleton
{Ω : Type u_1}
{F : Type u_2}
[mΩ : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
[NormedAddCommGroup F]
[NormedSpace Real F]
[CompleteSpace F]
(hs : MeasurableSet s)
{f : Ω → F}
(hf : MeasureTheory.Integrable f μ)
:
(MeasureTheory.ae (μ.restrict s)).EventuallyEq
(MeasureTheory.condExp (MeasurableSpace.generateFrom (Singleton.singleton s)) μ f) fun (x : Ω) =>
MeasureTheory.integral (cond μ s) fun (x : Ω) => f x
theorem
ProbabilityTheory.condExp_set_generateFrom_singleton
{Ω : Type u_1}
[mΩ : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s t : Set Ω}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
(MeasureTheory.ae (μ.restrict s)).EventuallyEq
(MeasureTheory.condExp (MeasurableSpace.generateFrom (Singleton.singleton s)) μ (t.indicator fun (ω : Ω) => 1))
fun (x : Ω) => (DFunLike.coe (cond μ s) t).toReal
@[deprecated ProbabilityTheory.condExp_set_generateFrom_singleton (since := "2025-01-21")]
theorem
ProbabilityTheory.condexp_set_generateFrom_singleton
{Ω : Type u_1}
[mΩ : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s t : Set Ω}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
(MeasureTheory.ae (μ.restrict s)).EventuallyEq
(MeasureTheory.condExp (MeasurableSpace.generateFrom (Singleton.singleton s)) μ (t.indicator fun (ω : Ω) => 1))
fun (x : Ω) => (DFunLike.coe (cond μ s) t).toReal
Alias of ProbabilityTheory.condExp_set_generateFrom_singleton.
theorem
ProbabilityTheory.condExpKernel_singleton_ae_eq_cond
{Ω : Type u_1}
[mΩ : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s t : Set Ω}
[StandardBorelSpace Ω]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
Filter.Eventually
(fun (ω : Ω) =>
Eq (DFunLike.coe (DFunLike.coe (condExpKernel μ (MeasurableSpace.generateFrom (Singleton.singleton s))) ω) t)
(DFunLike.coe (cond μ s) t))
(MeasureTheory.ae (μ.restrict s))
@[deprecated ProbabilityTheory.condExpKernel_singleton_ae_eq_cond (since := "2025-01-21")]
theorem
ProbabilityTheory.condexpKernel_singleton_ae_eq_cond
{Ω : Type u_1}
[mΩ : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s t : Set Ω}
[StandardBorelSpace Ω]
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
Filter.Eventually
(fun (ω : Ω) =>
Eq (DFunLike.coe (DFunLike.coe (condExpKernel μ (MeasurableSpace.generateFrom (Singleton.singleton s))) ω) t)
(DFunLike.coe (cond μ s) t))
(MeasureTheory.ae (μ.restrict s))
Alias of ProbabilityTheory.condExpKernel_singleton_ae_eq_cond.