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 : MeasurableSpace Ω}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{f : Ω → F}
[TopologicalSpace F]
(hm : m ≤ mΩ)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.AEStronglyMeasurable (fun (x : Ω × Ω) => f x.2)
(MeasureTheory.Measure.map (fun (ω : Ω) => (id ω, id ω)) μ)
theorem
MeasureTheory.Integrable.comp_snd_map_prod_id
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{f : Ω → F}
[NormedAddCommGroup F]
(hm : m ≤ mΩ)
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (x : Ω × Ω) => f x.2) (MeasureTheory.Measure.map (fun (ω : Ω) => (id ω, id ω)) μ)
theorem
ProbabilityTheory.condexpKernel_def
{Ω : Type u_3}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(m : MeasurableSpace Ω)
:
@[irreducible]
noncomputable def
ProbabilityTheory.condexpKernel
{Ω : Type u_3}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(m : MeasurableSpace Ω)
:
↥(ProbabilityTheory.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Ω.
Instances For
theorem
ProbabilityTheory.condexpKernel_apply_eq_condDistrib
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{ω : Ω}
:
(ProbabilityTheory.condexpKernel μ m) ω = (ProbabilityTheory.condDistrib id id μ) (id ω)
instance
ProbabilityTheory.instIsMarkovKernelCondexpKernel
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
:
Equations
- ⋯ = ⋯
theorem
ProbabilityTheory.measurable_condexpKernel
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
(hs : MeasurableSet s)
:
Measurable fun (ω : Ω) => ↑↑((ProbabilityTheory.condexpKernel μ m) ω) s
theorem
ProbabilityTheory.stronglyMeasurable_condexpKernel
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
(hs : MeasurableSet s)
:
MeasureTheory.StronglyMeasurable fun (ω : Ω) => ↑↑((ProbabilityTheory.condexpKernel μ m) ω) s
theorem
MeasureTheory.AEStronglyMeasurable.integral_condexpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => ∫ (y : Ω), f y ∂(ProbabilityTheory.condexpKernel μ m) ω) μ
theorem
ProbabilityTheory.aestronglyMeasurable'_integral_condexpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.AEStronglyMeasurable' m (fun (ω : Ω) => ∫ (y : Ω), f y ∂(ProbabilityTheory.condexpKernel μ m) ω) μ
theorem
MeasureTheory.Integrable.condexpKernel_ae
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
(hf_int : MeasureTheory.Integrable f μ)
:
∀ᵐ (ω : Ω) ∂μ, MeasureTheory.Integrable f ((ProbabilityTheory.condexpKernel μ m) ω)
theorem
MeasureTheory.Integrable.integral_norm_condexpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
(hf_int : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (ω : Ω) => ∫ (y : Ω), ‖f y‖ ∂(ProbabilityTheory.condexpKernel μ m) ω) μ
theorem
MeasureTheory.Integrable.norm_integral_condexpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hf_int : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (ω : Ω) => ‖∫ (y : Ω), f y ∂(ProbabilityTheory.condexpKernel μ m) ω‖) μ
theorem
MeasureTheory.Integrable.integral_condexpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hf_int : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (ω : Ω) => ∫ (y : Ω), f y ∂(ProbabilityTheory.condexpKernel μ m) ω) μ
theorem
ProbabilityTheory.integrable_toReal_condexpKernel
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
(hs : MeasurableSet s)
:
MeasureTheory.Integrable (fun (ω : Ω) => (↑↑((ProbabilityTheory.condexpKernel μ m) ω) s).toReal) μ
theorem
ProbabilityTheory.condexpKernel_ae_eq_condexp'
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
(hs : MeasurableSet s)
:
(fun (ω : Ω) => (↑↑((ProbabilityTheory.condexpKernel μ m) ω) s).toReal) =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp (m ⊓ mΩ) μ (Set.indicator s fun (ω : Ω) => 1)
theorem
ProbabilityTheory.condexpKernel_ae_eq_condexp
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hm : m ≤ mΩ)
{s : Set Ω}
(hs : MeasurableSet s)
:
(fun (ω : Ω) => (↑↑((ProbabilityTheory.condexpKernel μ m) ω) s).toReal) =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp m μ (Set.indicator s fun (ω : Ω) => 1)
theorem
ProbabilityTheory.condexpKernel_ae_eq_trim_condexp
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hm : m ≤ mΩ)
{s : Set Ω}
(hs : MeasurableSet s)
:
(fun (ω : Ω) =>
(↑↑((ProbabilityTheory.condexpKernel μ m) ω)
s).toReal) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.trim μ hm)] MeasureTheory.condexp m μ (Set.indicator s fun (ω : Ω) => 1)
theorem
ProbabilityTheory.condexp_ae_eq_integral_condexpKernel'
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hf_int : MeasureTheory.Integrable f μ)
:
MeasureTheory.condexp (m ⊓ mΩ) μ f =ᶠ[MeasureTheory.Measure.ae μ] fun (ω : Ω) =>
∫ (y : Ω), f y ∂(ProbabilityTheory.condexpKernel μ m) ω
theorem
ProbabilityTheory.condexp_ae_eq_integral_condexpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hm : m ≤ mΩ)
(hf_int : MeasureTheory.Integrable f μ)
:
MeasureTheory.condexp m μ f =ᶠ[MeasureTheory.Measure.ae μ] fun (ω : Ω) =>
∫ (y : Ω), f y ∂(ProbabilityTheory.condexpKernel μ m) ω
The conditional expectation of f with respect to a σ-algebra m is almost everywhere equal to
the integral ∫ y, f y ∂(condexpKernel μ m ω).