# mathlib3documentation

probability.kernel.disintegration

# 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 = ρ s
• probability_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
• = λ (a : α), , _⟩
Instances for probability_theory.cond_kernel_real
@[protected, instance]
theorem probability_theory.cond_kernel_real_Iic {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) (x : ) :
(set.Iic x) =
theorem probability_theory.set_lintegral_cond_kernel_real_Iic {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (x : ) {s : set α} (hs : measurable_set s) :
∫⁻ (a : α) in s, (set.Iic x) ρ.fst = ρ (s ×ˢ set.Iic x)
theorem probability_theory.set_lintegral_cond_kernel_real_prod {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) {s : set α} (hs : measurable_set s) {t : set } (ht : measurable_set t) :
∫⁻ (a : α) in s, ρ.fst = ρ (s ×ˢ t)
theorem probability_theory.lintegral_cond_kernel_real_mem {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) {s : set × )} (hs : measurable_set s) :
∫⁻ (a : α), {x : | (a, x) s} ρ.fst = ρ s
theorem probability_theory.lintegral_cond_kernel_real {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) {f : α × ennreal} (hf : measurable f) :
∫⁻ (a : α), ∫⁻ (y : ), f (a, y) ρ.fst = ∫⁻ (x : α × ), f x ρ
theorem probability_theory.ae_cond_kernel_real_eq_one {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) {s : set } (hs : measurable_set s) (hρ : ρ {x : α × | x.snd s} = 0) :
∀ᵐ (a : α) ρ.fst, = 1

### 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} [polish_space Ω] [borel_space Ω] [nonempty Ω] (ρ : measure_theory.measure × Ω)) (γ : Type u_3)  :

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} [polish_space Ω] [borel_space Ω] [nonempty Ω] (ρ : measure_theory.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
Instances for measure_theory.measure.cond_kernel
theorem probability_theory.cond_kernel_def {α : Type u_1} {mα : measurable_space α} {Ω : Type u_2} [polish_space Ω] [borel_space Ω] [nonempty Ω] (ρ : measure_theory.measure × Ω))  :
@[protected, instance]
theorem probability_theory.measure_eq_comp_prod {α : Type u_1} {mα : measurable_space α} {Ω : Type u_2} [polish_space Ω] [borel_space Ω] [nonempty Ω] (ρ : measure_theory.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} [polish_space Ω] [borel_space Ω] [nonempty Ω] (γ : Type u_3) (ρ : measure_theory.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} [polish_space Ω] [borel_space Ω] [nonempty Ω] (ρ : measure_theory.measure × Ω)) {s : set × Ω)} (hs : measurable_set s) :
∫⁻ (a : α), ((ρ.cond_kernel) a) {x : Ω | (a, x) s} ρ.fst = ρ s
theorem probability_theory.set_lintegral_cond_kernel_eq_measure_prod {α : Type u_1} {mα : measurable_space α} {Ω : Type u_2} [polish_space Ω] [borel_space Ω] [nonempty Ω] (ρ : measure_theory.measure × Ω)) {s : set α} (hs : measurable_set s) {t : set Ω} (ht : measurable_set t) :
∫⁻ (a : α) in s, ((ρ.cond_kernel) a) t ρ.fst = ρ (s ×ˢ t)
theorem probability_theory.lintegral_cond_kernel {α : Type u_1} {mα : measurable_space α} {Ω : Type u_2} [polish_space Ω] [borel_space Ω] [nonempty Ω] (ρ : measure_theory.measure × Ω)) {f : α × Ω ennreal} (hf : measurable f) :
∫⁻ (a : α), ∫⁻ (ω : Ω), f (a, ω) (ρ.cond_kernel) a ρ.fst = ∫⁻ (x : α × Ω), f x ρ
theorem probability_theory.set_lintegral_cond_kernel {α : Type u_1} {mα : measurable_space α} {Ω : Type u_2} [polish_space Ω] [borel_space Ω] [nonempty Ω] (ρ : measure_theory.measure × Ω)) {f : α × Ω ennreal} (hf : measurable f) {s : set α} (hs : measurable_set s) {t : set Ω} (ht : measurable_set t) :
∫⁻ (a : α) in s, ∫⁻ (ω : Ω) in t, f (a, ω) (ρ.cond_kernel) a ρ.fst = ∫⁻ (x : α × Ω) in s ×ˢ t, f x ρ
theorem probability_theory.set_lintegral_cond_kernel_univ_right {α : Type u_1} {mα : measurable_space α} {Ω : Type u_2} [polish_space Ω] [borel_space Ω] [nonempty Ω] (ρ : measure_theory.measure × Ω)) {f : α × Ω ennreal} (hf : measurable f) {s : set α} (hs : measurable_set s) :
∫⁻ (a : α) in s, ∫⁻ (ω : Ω), f (a, ω) (ρ.cond_kernel) a ρ.fst = ∫⁻ (x : α × Ω) in , f x ρ
theorem probability_theory.set_lintegral_cond_kernel_univ_left {α : Type u_1} {mα : measurable_space α} {Ω : Type u_2} [polish_space Ω] [borel_space Ω] [nonempty Ω] (ρ : measure_theory.measure × Ω)) {f : α × Ω ennreal} (hf : measurable f) {t : set Ω} (ht : measurable_set t) :
∫⁻ (a : α), ∫⁻ (ω : Ω) in t, f (a, ω) (ρ.cond_kernel) a ρ.fst = ∫⁻ (x : α × Ω) in , f x ρ
theorem measure_theory.ae_strongly_measurable.integral_cond_kernel {α : Type u_1} {mα : measurable_space α} {Ω : Type u_2} [polish_space Ω] [borel_space Ω] [nonempty Ω] {E : Type u_3} [ E] {ρ : measure_theory.measure × Ω)} {f : α × Ω E}  :
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} [polish_space Ω] [borel_space Ω] [nonempty Ω] {E : Type u_3} [ E] {ρ : measure_theory.measure × Ω)} {f : α × Ω E} (hf : ρ) :
(a : α), (x : Ω), f (a, x) (ρ.cond_kernel) a ρ.fst = (ω : α × Ω), f ω ρ
theorem probability_theory.set_integral_cond_kernel {α : Type u_1} {mα : measurable_space α} {Ω : Type u_2} [polish_space Ω] [borel_space Ω] [nonempty Ω] {E : Type u_3} [ E] {ρ : measure_theory.measure × Ω)} {f : α × Ω E} {s : set α} (hs : measurable_set s) {t : set Ω} (ht : measurable_set t) (hf : (s ×ˢ t) ρ) :
(a : α) in s, (ω : Ω) in t, f (a, ω) (ρ.cond_kernel) a ρ.fst = (x : α × Ω) in s ×ˢ t, f x ρ
theorem probability_theory.set_integral_cond_kernel_univ_right {α : Type u_1} {mα : measurable_space α} {Ω : Type u_2} [polish_space Ω] [borel_space Ω] [nonempty Ω] {E : Type u_3} [ E] {ρ : measure_theory.measure × Ω)} {f : α × Ω E} {s : set α} (hs : measurable_set s) (hf : ρ) :
(a : α) in s, (ω : Ω), f (a, ω) (ρ.cond_kernel) a ρ.fst = (x : α × Ω) in , f x ρ
theorem probability_theory.set_integral_cond_kernel_univ_left {α : Type u_1} {mα : measurable_space α} {Ω : Type u_2} [polish_space Ω] [borel_space Ω] [nonempty Ω] {E : Type u_3} [ E] {ρ : measure_theory.measure × Ω)} {f : α × Ω E} {t : set Ω} (ht : measurable_set t) (hf : ρ) :
(a : α), (ω : Ω) in t, f (a, ω) (ρ.cond_kernel) a ρ.fst = (x : α × Ω) in , f x ρ

### 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 α} [borel_space Ω] [polish_space Ω] [nonempty Ω] {ρ : measure_theory.measure × Ω)} {f : α × Ω F}  :
(∀ᵐ (a : α) ρ.fst, measure_theory.integrable (λ (ω : Ω), f (a, ω)) ((ρ.cond_kernel) a)) measure_theory.integrable (λ (a : α), (ω : Ω), f (a, ω) (ρ.cond_kernel) a) ρ.fst
theorem measure_theory.integrable.cond_kernel_ae {α : Type u_1} {Ω : Type u_2} {F : Type u_4} {mα : measurable_space α} [borel_space Ω] [polish_space Ω] [nonempty Ω] {ρ : measure_theory.measure × Ω)} {f : α × Ω F} (hf_int : ρ) :
∀ᵐ (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 α} [borel_space Ω] [polish_space Ω] [nonempty Ω] {ρ : measure_theory.measure × Ω)} {f : α × Ω F} (hf_int : ρ) :
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 α} [borel_space Ω] [polish_space Ω] [nonempty Ω] [ E] {ρ : measure_theory.measure × Ω)} {f : α × Ω E} (hf_int : ρ) :
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 α} [borel_space Ω] [polish_space Ω] [nonempty Ω] [ E] {ρ : measure_theory.measure × Ω)} {f : α × Ω E} (hf_int : ρ) :
measure_theory.integrable (λ (x : α), (y : Ω), f (x, y) (ρ.cond_kernel) x) ρ.fst