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 : m ≤ mΩ)
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (fun (x : Ω × Ω) => f x.2) (Measure.map (fun (ω : Ω) => (id ω, id ω)) μ)
theorem
MeasureTheory.Integrable.comp_snd_map_prod_id
{Ω : Type u_1}
{F : Type u_2}
{m mΩ : MeasurableSpace Ω}
{μ : Measure Ω}
{f : Ω → F}
[NormedAddCommGroup F]
(hf : Integrable f μ)
:
Integrable (fun (x : Ω × Ω) => f x.2) (Measure.map (fun (ω : Ω) => (id ω, 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
- ProbabilityTheory.condExpKernel μ m = if _h : Nonempty Ω then (ProbabilityTheory.condDistrib id id μ).comap id ⋯ else 0
Instances For
theorem
ProbabilityTheory.condExpKernel_def
{Ω : Type u_3}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(m : MeasurableSpace Ω)
:
theorem
ProbabilityTheory.condExpKernel_eq
{Ω : Type u_1}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
[h : Nonempty Ω]
(m : MeasurableSpace Ω)
:
theorem
ProbabilityTheory.condExpKernel_apply_eq_condDistrib
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[Nonempty Ω]
{ω : Ω}
:
instance
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 : m ≤ mΩ)
:
(μ.trim hm).compProd (condExpKernel μ m) = MeasureTheory.Measure.map (fun (ω : Ω) => (id ω, id ω)) μ
theorem
ProbabilityTheory.condExpKernel_comp_trim
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hm : m ≤ mΩ)
:
theorem
ProbabilityTheory.measurable_condExpKernel
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
(hs : MeasurableSet s)
:
Measurable fun (ω : Ω) => ((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 (ω : Ω) => ((condExpKernel μ m) ω) s
theorem
MeasureTheory.StronglyMeasurable.integral_condExpKernel'
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ F]
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (ω : Ω) => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω
theorem
MeasureTheory.StronglyMeasurable.integral_condExpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ F]
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (ω : Ω) => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω
theorem
MeasureTheory.AEStronglyMeasurable.integral_condExpKernel
{Ω : Type u_1}
{F : Type u_2}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ F]
(hf : AEStronglyMeasurable f μ)
:
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 Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ F]
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ
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 : m ≤ mΩ)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
∀ᵐ (ω : Ω) ∂μ.trim hm, f =ᵐ[(condExpKernel μ m) ω] MeasureTheory.AEStronglyMeasurable.mk f hf
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 μ)
:
∀ᵐ (ω : Ω) ∂μ, Integrable f ((ProbabilityTheory.condExpKernel μ m) ω)
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 (ω : Ω) => ∫ (y : Ω), ‖f y‖ ∂(ProbabilityTheory.condExpKernel μ m) ω) μ
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 ℝ F]
(hf_int : Integrable f μ)
:
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 Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ F]
(hf_int : Integrable f μ)
:
Integrable (fun (ω : Ω) => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω) μ
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 (ω : Ω) => ((condExpKernel μ m) ω).real s) μ
theorem
ProbabilityTheory.condExpKernel_ae_eq_condExp'
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.condExpKernel_ae_eq_condExp
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hm : m ≤ mΩ)
{s : Set Ω}
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.condExpKernel_ae_eq_trim_condExp
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hm : m ≤ mΩ)
{s : Set Ω}
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.condDistrib_apply_ae_eq_condExpKernel_map
{Ω : Type u_1}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{β : Type u_3}
{γ : Type u_4}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[StandardBorelSpace β]
[Nonempty β]
{X : Ω → β}
{Y : Ω → γ}
(hX : Measurable X)
(hY : Measurable Y)
{s : Set β}
(hs : MeasurableSet s)
:
(fun (a : Ω) => ((condDistrib X Y μ) (Y a)) s) =ᵐ[μ] fun (a : Ω) =>
(((condExpKernel μ (MeasurableSpace.comap Y mγ)).map X) a) s
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 ℝ F]
[CompleteSpace F]
(hf_int : MeasureTheory.Integrable f μ)
:
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 ℝ F]
[CompleteSpace F]
(hm : m ≤ mΩ)
(hf_int : MeasureTheory.Integrable f μ)
:
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 ℝ F]
[CompleteSpace F]
(hm : m ≤ mΩ)
(hf : MeasureTheory.StronglyMeasurable f)
(hf_int : MeasureTheory.Integrable f μ)
:
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 ℝ F]
[CompleteSpace F]
(hm : m ≤ mΩ)
(hf_int : MeasureTheory.Integrable f μ)
:
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 ℝ F]
[CompleteSpace F]
(hs : MeasurableSet s)
{f : Ω → F}
(hf : MeasureTheory.Integrable f μ)
:
theorem
ProbabilityTheory.condExp_set_generateFrom_singleton
{Ω : Type u_1}
[mΩ : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s t : Set Ω}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
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)
:
∀ᵐ (ω : Ω) ∂μ.restrict s, ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]