Disintegration of measures on product spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Let ρ be a finite measure on α × Ω, where Ω is a standard Borel space. In mathlib terms, Ω
verifies [nonempty Ω] [topological_space Ω] [polish_space Ω] [measurable_space Ω] [borel_space Ω].
Then there exists a kernel ρ.cond_kernel : kernel α Ω such that for any measurable set
s : set (α × Ω), ρ s = ∫⁻ a, ρ.cond_kernel a {x | (a, x) ∈ s} ∂ρ.fst.
In terms of kernels, ρ.cond_kernel is such that for any measurable space γ, we
have a disintegration of the constant kernel from γ with value ρ:
kernel.const γ ρ = (kernel.const γ ρ.fst) ⊗ₖ (kernel.prod_mk_left γ (cond_kernel ρ)),
where ρ.fst is the marginal measure of ρ on α. In particular,
ρ = ((kernel.const unit ρ.fst) ⊗ₖ (kernel.prod_mk_left unit (cond_kernel ρ))) ().
In order to obtain a disintegration for any standard Borel space, we use that these spaces embed
measurably into ℝ: it then suffices to define a suitable kernel for Ω = ℝ. In the real case,
we define a conditional kernel by taking for each a : α the measure associated to the Stieltjes
function cond_cdf ρ a (the conditional cumulative distribution function).
Main definitions #
measure_theory.measure.cond_kernel ρ : kernel α Ω: conditional kernel described above.
Main statements #
probability_theory.lintegral_cond_kernel:∫⁻ a, ∫⁻ ω, f (a, ω) ∂(ρ.cond_kernel a) ∂ρ.fst = ∫⁻ x, f x ∂ρprobability_theory.lintegral_cond_kernel_mem:∫⁻ a, ρ.cond_kernel a {x | (a, x) ∈ s} ∂ρ.fst = ρ sprobability_theory.kernel.const_eq_comp_prod:kernel.const γ ρ = (kernel.const γ ρ.fst) ⊗ₖ (kernel.prod_mk_left γ ρ.cond_kernel)probability_theory.measure_eq_comp_prod:ρ = ((kernel.const unit ρ.fst) ⊗ₖ (kernel.prod_mk_left unit ρ.cond_kernel)) ()
Disintegration of measures on α × ℝ #
noncomputable
def
probability_theory.cond_kernel_real
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ)) :
Conditional measure on the second space of the product given the value on the first, as a
kernel. Use the more general cond_kernel.
Equations
- probability_theory.cond_kernel_real ρ = ⟨λ (a : α), (probability_theory.cond_cdf ρ a).measure, _⟩
Instances for probability_theory.cond_kernel_real
@[protected, instance]
def
probability_theory.cond_kernel_real.is_markov_kernel
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ)) :
theorem
probability_theory.cond_kernel_real_Iic
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
(a : α)
(x : ℝ) :
⇑(⇑(probability_theory.cond_kernel_real ρ) a) (set.Iic x) = ennreal.of_real (⇑(probability_theory.cond_cdf ρ a) x)
theorem
probability_theory.set_lintegral_cond_kernel_real_Iic
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
(x : ℝ)
{s : set α}
(hs : measurable_set s) :
theorem
probability_theory.set_lintegral_cond_kernel_real_univ
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
{s : set α}
(hs : measurable_set s) :
theorem
probability_theory.lintegral_cond_kernel_real_univ
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ)) :
theorem
probability_theory.set_lintegral_cond_kernel_real_prod
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
{s : set α}
(hs : measurable_set s)
{t : set ℝ}
(ht : measurable_set t) :
theorem
probability_theory.lintegral_cond_kernel_real_mem
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
{s : set (α × ℝ)}
(hs : measurable_set s) :
theorem
probability_theory.kernel.const_eq_comp_prod_real
{α : Type u_1}
{mα : measurable_space α}
(γ : Type u_2)
[measurable_space γ]
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ] :
theorem
probability_theory.measure_eq_comp_prod_real
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ] :
theorem
probability_theory.lintegral_cond_kernel_real
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
{f : α × ℝ → ennreal}
(hf : measurable f) :
theorem
probability_theory.ae_cond_kernel_real_eq_one
{α : Type u_1}
{mα : measurable_space α}
(ρ : measure_theory.measure (α × ℝ))
[measure_theory.is_finite_measure ρ]
{s : set ℝ}
(hs : measurable_set s)
(hρ : ⇑ρ {x : α × ℝ | x.snd ∈ sᶜ} = 0) :
Disintegration of measures on Polish Borel spaces #
Since every standard Borel space embeds measurably into ℝ, we can generalize the disintegration
property on ℝ to all these spaces.
theorem
probability_theory.exists_cond_kernel
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
(ρ : measure_theory.measure (α × Ω))
[measure_theory.is_finite_measure ρ]
(γ : Type u_3)
[measurable_space γ] :
Existence of a conditional kernel. Use the definition cond_kernel to get that kernel.
@[irreducible]
noncomputable
def
measure_theory.measure.cond_kernel
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
(ρ : measure_theory.measure (α × Ω))
[measure_theory.is_finite_measure ρ] :
Conditional kernel of a measure on a product space: a Markov kernel such that
ρ = ((kernel.const unit ρ.fst) ⊗ₖ (kernel.prod_mk_left unit ρ.cond_kernel)) ()
(see probability_theory.measure_eq_comp_prod).
Equations
- ρ.cond_kernel = _.some
Instances for measure_theory.measure.cond_kernel
theorem
probability_theory.cond_kernel_def
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
(ρ : measure_theory.measure (α × Ω))
[measure_theory.is_finite_measure ρ] :
ρ.cond_kernel = _.some
@[protected, instance]
def
probability_theory.measure_theory.measure.cond_kernel.is_markov_kernel
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
(ρ : measure_theory.measure (α × Ω))
[measure_theory.is_finite_measure ρ] :
theorem
probability_theory.kernel.const_unit_eq_comp_prod
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
(ρ : measure_theory.measure (α × Ω))
[measure_theory.is_finite_measure ρ] :
theorem
probability_theory.measure_eq_comp_prod
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
(ρ : measure_theory.measure (α × Ω))
[measure_theory.is_finite_measure ρ] :
Disintegration of finite product measures on α × Ω, where Ω is Polish Borel. Such a
measure can be written as the composition-product of the constant kernel with value ρ.fst
(marginal measure over α) and a Markov kernel from α to Ω. We call that Markov kernel
probability_theory.cond_kernel ρ.
theorem
probability_theory.kernel.const_eq_comp_prod
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
(γ : Type u_3)
[measurable_space γ]
(ρ : measure_theory.measure (α × Ω))
[measure_theory.is_finite_measure ρ] :
Disintegration of constant kernels. A constant kernel on a product space α × Ω, where Ω
is Polish Borel, can be written as the composition-product of the constant kernel with value ρ.fst
(marginal measure over α) and a Markov kernel from α to Ω. We call that Markov kernel
probability_theory.cond_kernel ρ.
theorem
probability_theory.lintegral_cond_kernel_mem
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
(ρ : measure_theory.measure (α × Ω))
[measure_theory.is_finite_measure ρ]
{s : set (α × Ω)}
(hs : measurable_set s) :
theorem
probability_theory.set_lintegral_cond_kernel_eq_measure_prod
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
(ρ : measure_theory.measure (α × Ω))
[measure_theory.is_finite_measure ρ]
{s : set α}
(hs : measurable_set s)
{t : set Ω}
(ht : measurable_set t) :
theorem
probability_theory.lintegral_cond_kernel
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
(ρ : measure_theory.measure (α × Ω))
[measure_theory.is_finite_measure ρ]
{f : α × Ω → ennreal}
(hf : measurable f) :
theorem
probability_theory.set_lintegral_cond_kernel
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
(ρ : measure_theory.measure (α × Ω))
[measure_theory.is_finite_measure ρ]
{f : α × Ω → ennreal}
(hf : measurable f)
{s : set α}
(hs : measurable_set s)
{t : set Ω}
(ht : measurable_set t) :
theorem
probability_theory.set_lintegral_cond_kernel_univ_right
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
(ρ : measure_theory.measure (α × Ω))
[measure_theory.is_finite_measure ρ]
{f : α × Ω → ennreal}
(hf : measurable f)
{s : set α}
(hs : measurable_set s) :
theorem
probability_theory.set_lintegral_cond_kernel_univ_left
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
(ρ : measure_theory.measure (α × Ω))
[measure_theory.is_finite_measure ρ]
{f : α × Ω → ennreal}
(hf : measurable f)
{t : set Ω}
(ht : measurable_set t) :
theorem
measure_theory.ae_strongly_measurable.integral_cond_kernel
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
{E : Type u_3}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ρ : measure_theory.measure (α × Ω)}
[measure_theory.is_finite_measure ρ]
{f : α × Ω → E}
(hf : measure_theory.ae_strongly_measurable f ρ) :
measure_theory.ae_strongly_measurable (λ (x : α), ∫ (y : Ω), f (x, y) ∂⇑(ρ.cond_kernel) x) ρ.fst
theorem
probability_theory.integral_cond_kernel
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
{E : Type u_3}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ρ : measure_theory.measure (α × Ω)}
[measure_theory.is_finite_measure ρ]
{f : α × Ω → E}
(hf : measure_theory.integrable f ρ) :
theorem
probability_theory.set_integral_cond_kernel
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
{E : Type u_3}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ρ : measure_theory.measure (α × Ω)}
[measure_theory.is_finite_measure ρ]
{f : α × Ω → E}
{s : set α}
(hs : measurable_set s)
{t : set Ω}
(ht : measurable_set t)
(hf : measure_theory.integrable_on f (s ×ˢ t) ρ) :
theorem
probability_theory.set_integral_cond_kernel_univ_right
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
{E : Type u_3}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ρ : measure_theory.measure (α × Ω)}
[measure_theory.is_finite_measure ρ]
{f : α × Ω → E}
{s : set α}
(hs : measurable_set s)
(hf : measure_theory.integrable_on f (s ×ˢ set.univ) ρ) :
theorem
probability_theory.set_integral_cond_kernel_univ_left
{α : Type u_1}
{mα : measurable_space α}
{Ω : Type u_2}
[topological_space Ω]
[polish_space Ω]
[measurable_space Ω]
[borel_space Ω]
[nonempty Ω]
{E : Type u_3}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ρ : measure_theory.measure (α × Ω)}
[measure_theory.is_finite_measure ρ]
{f : α × Ω → E}
{t : set Ω}
(ht : measurable_set t)
(hf : measure_theory.integrable_on f (set.univ ×ˢ t) ρ) :
Integrability #
We place these lemmas in the measure_theory namespace to enable dot notation.
theorem
measure_theory.ae_strongly_measurable.ae_integrable_cond_kernel_iff
{α : Type u_1}
{Ω : Type u_2}
{F : Type u_4}
{mα : measurable_space α}
[measurable_space Ω]
[topological_space Ω]
[borel_space Ω]
[polish_space Ω]
[nonempty Ω]
[normed_add_comm_group F]
{ρ : measure_theory.measure (α × Ω)}
[measure_theory.is_finite_measure ρ]
{f : α × Ω → F}
(hf : measure_theory.ae_strongly_measurable f ρ) :
(∀ᵐ (a : α) ∂ρ.fst, measure_theory.integrable (λ (ω : Ω), f (a, ω)) (⇑(ρ.cond_kernel) a)) ∧ measure_theory.integrable (λ (a : α), ∫ (ω : Ω), ‖f (a, ω)‖ ∂⇑(ρ.cond_kernel) a) ρ.fst ↔ measure_theory.integrable f ρ
theorem
measure_theory.integrable.cond_kernel_ae
{α : Type u_1}
{Ω : Type u_2}
{F : Type u_4}
{mα : measurable_space α}
[measurable_space Ω]
[topological_space Ω]
[borel_space Ω]
[polish_space Ω]
[nonempty Ω]
[normed_add_comm_group F]
{ρ : measure_theory.measure (α × Ω)}
[measure_theory.is_finite_measure ρ]
{f : α × Ω → F}
(hf_int : measure_theory.integrable f ρ) :
∀ᵐ (a : α) ∂ρ.fst, measure_theory.integrable (λ (ω : Ω), f (a, ω)) (⇑(ρ.cond_kernel) a)
theorem
measure_theory.integrable.integral_norm_cond_kernel
{α : Type u_1}
{Ω : Type u_2}
{F : Type u_4}
{mα : measurable_space α}
[measurable_space Ω]
[topological_space Ω]
[borel_space Ω]
[polish_space Ω]
[nonempty Ω]
[normed_add_comm_group F]
{ρ : measure_theory.measure (α × Ω)}
[measure_theory.is_finite_measure ρ]
{f : α × Ω → F}
(hf_int : measure_theory.integrable f ρ) :
measure_theory.integrable (λ (x : α), ∫ (y : Ω), ‖f (x, y)‖ ∂⇑(ρ.cond_kernel) x) ρ.fst
theorem
measure_theory.integrable.norm_integral_cond_kernel
{α : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mα : measurable_space α}
[measurable_space Ω]
[topological_space Ω]
[borel_space Ω]
[polish_space Ω]
[nonempty Ω]
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ρ : measure_theory.measure (α × Ω)}
[measure_theory.is_finite_measure ρ]
{f : α × Ω → E}
(hf_int : measure_theory.integrable f ρ) :
measure_theory.integrable (λ (x : α), ‖∫ (y : Ω), f (x, y) ∂⇑(ρ.cond_kernel) x‖) ρ.fst
theorem
measure_theory.integrable.integral_cond_kernel
{α : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mα : measurable_space α}
[measurable_space Ω]
[topological_space Ω]
[borel_space Ω]
[polish_space Ω]
[nonempty Ω]
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ρ : measure_theory.measure (α × Ω)}
[measure_theory.is_finite_measure ρ]
{f : α × Ω → E}
(hf_int : measure_theory.integrable f ρ) :
measure_theory.integrable (λ (x : α), ∫ (y : Ω), f (x, y) ∂⇑(ρ.cond_kernel) x) ρ.fst