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 Ω}
{μ : 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 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 ω)) μ)
@[irreducible]
noncomputable def
ProbabilityTheory.condexpKernel
{Ω : Type u_3}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(m : MeasurableSpace Ω)
:
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_def
{Ω : Type u_3}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(m : MeasurableSpace Ω)
:
ProbabilityTheory.condexpKernel μ m = if _h : Nonempty Ω then (ProbabilityTheory.condDistrib id id μ).comap id ⋯ else 0
theorem
ProbabilityTheory.condexpKernel_eq
{Ω : Type u_1}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
[h : Nonempty Ω]
(m : MeasurableSpace Ω)
:
ProbabilityTheory.condexpKernel μ m = (ProbabilityTheory.condDistrib id id μ).comap id ⋯
theorem
ProbabilityTheory.condexpKernel_apply_eq_condDistrib
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[Nonempty Ω]
{ω : Ω}
:
(ProbabilityTheory.condexpKernel μ m) ω = (ProbabilityTheory.condDistrib id id μ) (id ω)
instance
ProbabilityTheory.instIsMarkovKernelCondexpKernel
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
:
Equations
- ⋯ = ⋯
theorem
ProbabilityTheory.measurable_condexpKernel
{Ω : Type u_1}
{m : MeasurableSpace Ω}
[mΩ : MeasurableSpace Ω]
[StandardBorelSpace Ω]
{μ : 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 Ω]
{μ : 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 Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ 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 Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ 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 Ω]
{μ : 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 Ω]
{μ : 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 Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ 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 Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ 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 Ω]
{μ : 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 Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set Ω}
(hs : MeasurableSet s)
:
(fun (ω : Ω) => (((ProbabilityTheory.condexpKernel μ m) ω) s).toReal) =ᵐ[μ] MeasureTheory.condexp (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 : m ≤ mΩ)
{s : Set Ω}
(hs : MeasurableSet s)
:
(fun (ω : Ω) => (((ProbabilityTheory.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 : m ≤ mΩ)
{s : Set Ω}
(hs : MeasurableSet s)
:
(fun (ω : Ω) => (((ProbabilityTheory.condexpKernel μ m) ω) s).toReal) =ᵐ[μ.trim hm] MeasureTheory.condexp m μ (s.indicator fun (ω : Ω) => 1)
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 μ)
:
MeasureTheory.condexp (m ⊓ mΩ) μ f =ᵐ[μ] 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 Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
[NormedAddCommGroup F]
{f : Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hm : m ≤ mΩ)
(hf_int : MeasureTheory.Integrable f μ)
:
MeasureTheory.condexp m μ f =ᵐ[μ] 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 ω).
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 μ)
:
MeasureTheory.condexp (MeasurableSpace.generateFrom {s}) μ f =ᵐ[μ.restrict s] fun (x : Ω) =>
∫ (x : Ω), f x ∂ProbabilityTheory.cond μ s
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.condexp (MeasurableSpace.generateFrom {s}) μ (t.indicator fun (ω : Ω) => 1) =ᵐ[μ.restrict s] fun (x : Ω) => ((ProbabilityTheory.cond μ s) t).toReal
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,
((ProbabilityTheory.condexpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = (ProbabilityTheory.cond μ s) t