mathlib3documentation

probability.kernel.condexp

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} (hm : m mΩ)  :
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} (hm : m mΩ) (hf : μ) :
measure_theory.integrable (λ (x : Ω × Ω), f x.snd) (measure_theory.measure.map (λ (ω : Ω), (id ω, id ω)) μ)
@[irreducible]
noncomputable def probability_theory.condexp_kernel {Ω : Type u_1} [mΩ : measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] (μ : measure_theory.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} {m : measurable_space Ω} [mΩ : measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] {μ : measure_theory.measure Ω} {s : set Ω} (hs : measurable_set s) :
measurable (λ (ω : Ω), ω) s)
theorem measure_theory.ae_strongly_measurable.integral_condexp_kernel {Ω : Type u_1} {F : Type u_2} {m : measurable_space Ω} [mΩ : measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] {μ : measure_theory.measure Ω} {f : Ω F} [ F] (hm : m mΩ)  :
measure_theory.ae_strongly_measurable (λ (ω : Ω), (y : Ω), f y μ
theorem probability_theory.ae_strongly_measurable'_integral_condexp_kernel {Ω : Type u_1} {F : Type u_2} {m : measurable_space Ω} [mΩ : measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] {μ : measure_theory.measure Ω} {f : Ω F} [ F] (hm : m mΩ)  :
(λ (ω : Ω), (y : Ω), f y μ
theorem measure_theory.integrable.condexp_kernel_ae {Ω : Type u_1} {F : Type u_2} {m : measurable_space Ω} [mΩ : measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] {μ : measure_theory.measure Ω} {f : Ω F} (hm : m mΩ) (hf_int : μ) :
∀ᵐ (ω : Ω) μ,
theorem measure_theory.integrable.integral_norm_condexp_kernel {Ω : Type u_1} {F : Type u_2} {m : measurable_space Ω} [mΩ : measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] {μ : measure_theory.measure Ω} {f : Ω F} (hm : m mΩ) (hf_int : μ) :
measure_theory.integrable (λ (ω : Ω), (y : Ω), f y μ
theorem measure_theory.integrable.norm_integral_condexp_kernel {Ω : Type u_1} {F : Type u_2} {m : measurable_space Ω} [mΩ : measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] {μ : measure_theory.measure Ω} {f : Ω F} [ F] (hm : m mΩ) (hf_int : μ) :
measure_theory.integrable (λ (ω : Ω), (y : Ω), f y ) μ
theorem measure_theory.integrable.integral_condexp_kernel {Ω : Type u_1} {F : Type u_2} {m : measurable_space Ω} [mΩ : measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] {μ : measure_theory.measure Ω} {f : Ω F} [ F] (hm : m mΩ) (hf_int : μ) :
measure_theory.integrable (λ (ω : Ω), (y : Ω), f y μ
theorem probability_theory.integrable_to_real_condexp_kernel {Ω : Type u_1} {m : measurable_space Ω} [mΩ : measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] {μ : measure_theory.measure Ω} (hm : m mΩ) {s : set Ω} (hs : measurable_set s) :
measure_theory.integrable (λ (ω : Ω), ( ω) s).to_real) μ
theorem probability_theory.condexp_ae_eq_integral_condexp_kernel {Ω : Type u_1} {F : Type u_2} {m : measurable_space Ω} [mΩ : measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] {μ : measure_theory.measure Ω} {f : Ω F} [ F] (hm : m mΩ) (hf_int : μ) :
=ᵐ[μ] λ (ω : Ω), (y : Ω), f y

The conditional expectation of f with respect to a σ-algebra m is almost everywhere equal to the integral ∫ y, f y ∂(condexp_kernel μ m ω).