Kernel associated with a conditional expectation #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define condexp_kernel μ m, a kernel from Ω to Ω such that for all integrable functions f,
μ[f | m] =ᵐ[μ] λ ω, ∫ y, f y ∂(condexp_kernel μ 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 #
condexp_kernel μ m: kernel such thatμ[f | m] =ᵐ[μ] λ ω, ∫ y, f y ∂(condexp_kernel μ m ω).
Main statements #
condexp_ae_eq_integral_condexp_kernel:μ[f | m] =ᵐ[μ] λ ω, ∫ y, f y ∂(condexp_kernel μ m ω).
theorem
probability_theory.measurable_id''
{Ω : Type u_1}
{m mΩ : measurable_space Ω}
(hm : m ≤ mΩ) :
theorem
probability_theory.ae_measurable_id''
{Ω : Type u_1}
{m mΩ : measurable_space Ω}
(μ : measure_theory.measure Ω)
(hm : m ≤ mΩ) :
theorem
measure_theory.ae_strongly_measurable.comp_snd_map_prod_id
{Ω : Type u_1}
{F : Type u_2}
{m mΩ : measurable_space Ω}
{μ : measure_theory.measure Ω}
{f : Ω → F}
[topological_space F]
(hm : m ≤ mΩ)
(hf : measure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_strongly_measurable (λ (x : Ω × Ω), f x.snd) (measure_theory.measure.map (λ (ω : Ω), (id ω, id ω)) μ)
theorem
measure_theory.integrable.comp_snd_map_prod_id
{Ω : Type u_1}
{F : Type u_2}
{m mΩ : measurable_space Ω}
{μ : measure_theory.measure Ω}
{f : Ω → F}
[normed_add_comm_group F]
(hm : m ≤ mΩ)
(hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (x : Ω × Ω), f x.snd) (measure_theory.measure.map (λ (ω : Ω), (id ω, id ω)) μ)
@[irreducible]
noncomputable
def
probability_theory.condexp_kernel
{Ω : Type u_1}
[topological_space Ω]
[mΩ : measurable_space Ω]
[polish_space Ω]
[borel_space Ω]
[nonempty Ω]
(μ : measure_theory.measure Ω)
[measure_theory.is_finite_measure μ]
(m : measurable_space Ω) :
Kernel associated with the conditional expectation with respect to a σ-algebra. It satisfies
μ[f | m] =ᵐ[μ] λ ω, ∫ y, f y ∂(condexp_kernel μ 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.
Equations
theorem
probability_theory.measurable_condexp_kernel
{Ω : Type u_1}
[topological_space Ω]
{m : measurable_space Ω}
[mΩ : measurable_space Ω]
[polish_space Ω]
[borel_space Ω]
[nonempty Ω]
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
{s : set Ω}
(hs : measurable_set s) :
measurable (λ (ω : Ω), ⇑(⇑(probability_theory.condexp_kernel μ m) ω) s)
theorem
measure_theory.ae_strongly_measurable.integral_condexp_kernel
{Ω : Type u_1}
{F : Type u_2}
[topological_space Ω]
{m : measurable_space Ω}
[mΩ : measurable_space Ω]
[polish_space Ω]
[borel_space Ω]
[nonempty Ω]
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
[normed_add_comm_group F]
{f : Ω → F}
[normed_space ℝ F]
[complete_space F]
(hm : m ≤ mΩ)
(hf : measure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_strongly_measurable (λ (ω : Ω), ∫ (y : Ω), f y ∂⇑(probability_theory.condexp_kernel μ m) ω) μ
theorem
probability_theory.ae_strongly_measurable'_integral_condexp_kernel
{Ω : Type u_1}
{F : Type u_2}
[topological_space Ω]
{m : measurable_space Ω}
[mΩ : measurable_space Ω]
[polish_space Ω]
[borel_space Ω]
[nonempty Ω]
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
[normed_add_comm_group F]
{f : Ω → F}
[normed_space ℝ F]
[complete_space F]
(hm : m ≤ mΩ)
(hf : measure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_strongly_measurable' m (λ (ω : Ω), ∫ (y : Ω), f y ∂⇑(probability_theory.condexp_kernel μ m) ω) μ
theorem
measure_theory.integrable.condexp_kernel_ae
{Ω : Type u_1}
{F : Type u_2}
[topological_space Ω]
{m : measurable_space Ω}
[mΩ : measurable_space Ω]
[polish_space Ω]
[borel_space Ω]
[nonempty Ω]
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
[normed_add_comm_group F]
{f : Ω → F}
(hm : m ≤ mΩ)
(hf_int : measure_theory.integrable f μ) :
∀ᵐ (ω : Ω) ∂μ, measure_theory.integrable f (⇑(probability_theory.condexp_kernel μ m) ω)
theorem
measure_theory.integrable.integral_norm_condexp_kernel
{Ω : Type u_1}
{F : Type u_2}
[topological_space Ω]
{m : measurable_space Ω}
[mΩ : measurable_space Ω]
[polish_space Ω]
[borel_space Ω]
[nonempty Ω]
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
[normed_add_comm_group F]
{f : Ω → F}
(hm : m ≤ mΩ)
(hf_int : measure_theory.integrable f μ) :
measure_theory.integrable (λ (ω : Ω), ∫ (y : Ω), ‖f y‖ ∂⇑(probability_theory.condexp_kernel μ m) ω) μ
theorem
measure_theory.integrable.norm_integral_condexp_kernel
{Ω : Type u_1}
{F : Type u_2}
[topological_space Ω]
{m : measurable_space Ω}
[mΩ : measurable_space Ω]
[polish_space Ω]
[borel_space Ω]
[nonempty Ω]
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
[normed_add_comm_group F]
{f : Ω → F}
[normed_space ℝ F]
[complete_space F]
(hm : m ≤ mΩ)
(hf_int : measure_theory.integrable f μ) :
measure_theory.integrable (λ (ω : Ω), ‖∫ (y : Ω), f y ∂⇑(probability_theory.condexp_kernel μ m) ω‖) μ
theorem
measure_theory.integrable.integral_condexp_kernel
{Ω : Type u_1}
{F : Type u_2}
[topological_space Ω]
{m : measurable_space Ω}
[mΩ : measurable_space Ω]
[polish_space Ω]
[borel_space Ω]
[nonempty Ω]
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
[normed_add_comm_group F]
{f : Ω → F}
[normed_space ℝ F]
[complete_space F]
(hm : m ≤ mΩ)
(hf_int : measure_theory.integrable f μ) :
measure_theory.integrable (λ (ω : Ω), ∫ (y : Ω), f y ∂⇑(probability_theory.condexp_kernel μ m) ω) μ
theorem
probability_theory.integrable_to_real_condexp_kernel
{Ω : Type u_1}
[topological_space Ω]
{m : measurable_space Ω}
[mΩ : measurable_space Ω]
[polish_space Ω]
[borel_space Ω]
[nonempty Ω]
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
(hm : m ≤ mΩ)
{s : set Ω}
(hs : measurable_set s) :
measure_theory.integrable (λ (ω : Ω), (⇑(⇑(probability_theory.condexp_kernel μ m) ω) s).to_real) μ
theorem
probability_theory.condexp_ae_eq_integral_condexp_kernel
{Ω : Type u_1}
{F : Type u_2}
[topological_space Ω]
{m : measurable_space Ω}
[mΩ : measurable_space Ω]
[polish_space Ω]
[borel_space Ω]
[nonempty Ω]
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
[normed_add_comm_group F]
{f : Ω → F}
[normed_space ℝ F]
[complete_space F]
(hm : m ≤ mΩ)
(hf_int : measure_theory.integrable f μ) :
measure_theory.condexp m μ f =ᵐ[μ] λ (ω : Ω), ∫ (y : Ω), f y ∂⇑(probability_theory.condexp_kernel μ m) ω
The conditional expectation of f with respect to a σ-algebra m is almost everywhere equal to
the integral ∫ y, f y ∂(condexp_kernel μ m ω).