mathlib3 documentation

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 #

Main statements #

Disintegration of measures on α × ℝ #

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
Instances for probability_theory.cond_kernel_real

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.

@[irreducible]

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

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 ρ.

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) :
∫⁻ (a : α), ((ρ.cond_kernel) a) {x : Ω | (a, x) s} ρ.fst = ρ s
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) :
∫⁻ (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} [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) :
∫⁻ (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} [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) :
∫⁻ (a : α) in s, ∫⁻ (ω : Ω), f (a, ω) (ρ.cond_kernel) a ρ.fst = ∫⁻ (x : α × Ω) in s ×ˢ set.univ, f x ρ
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) :
∫⁻ (a : α), ∫⁻ (ω : Ω) in t, f (a, ω) (ρ.cond_kernel) a ρ.fst = ∫⁻ (x : α × Ω) in set.univ ×ˢ t, f x ρ
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 ρ) :
(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} [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) ρ) :
(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} [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) ρ) :
(a : α) in s, (ω : Ω), f (a, ω) (ρ.cond_kernel) a ρ.fst = (x : α × Ω) in s ×ˢ set.univ, f x ρ
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) ρ) :
(a : α), (ω : Ω) in t, f (a, ω) (ρ.cond_kernel) a ρ.fst = (x : α × Ω) in set.univ ×ˢ t, f x ρ

Integrability #

We place these lemmas in the measure_theory namespace to enable dot notation.

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)