Disintegration of measures on product spaces #
Let ρ be a finite measure on α × Ω, where Ω is a standard Borel space. In mathlib terms, Ω
verifies [Nonempty Ω] [MeasurableSpace Ω] [StandardBorelSpace Ω].
Then there exists a kernel ρ.condKernel : kernel α Ω such that for any measurable set
s : Set (α × Ω), ρ s = ∫⁻ a, ρ.condKernel a {x | (a, x) ∈ s} ∂ρ.fst.
In terms of kernels, ρ.condKernel is such that for any measurable space γ, we
have a disintegration of the constant kernel from γ with value ρ:
kernel.const γ ρ = (kernel.const γ ρ.fst) ⊗ₖ (kernel.prodMkLeft γ (condKernel ρ)),
where ρ.fst is the marginal measure of ρ on α. In particular, ρ = ρ.fst ⊗ₘ ρ.condKernel.
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 condCDF ρ a (the conditional cumulative distribution function).
Main definitions #
MeasureTheory.Measure.condKernel ρ : kernel α Ω: conditional kernel described above.
Main statements #
ProbabilityTheory.lintegral_condKernel:∫⁻ a, ∫⁻ ω, f (a, ω) ∂(ρ.condKernel a) ∂ρ.fst = ∫⁻ x, f x ∂ρProbabilityTheory.lintegral_condKernel_mem:∫⁻ a, ρ.condKernel a {x | (a, x) ∈ s} ∂ρ.fst = ρ sProbabilityTheory.kernel.const_eq_compProd:kernel.const γ ρ = (kernel.const γ ρ.fst) ⊗ₖ (kernel.prodMkLeft γ ρ.condKernel)ProbabilityTheory.measure_eq_compProd:ρ = ρ.fst ⊗ₘ ρ.condKernelProbabilityTheory.eq_condKernel_of_measure_eq_compProd: a.e. uniqueness ofcondKernel
Disintegration of measures on α × ℝ #
noncomputable def
ProbabilityTheory.condKernelReal
{α : Type u_1}
{mα : MeasurableSpace α}
(ρ : MeasureTheory.Measure (α × ℝ))
:
Conditional measure on the second space of the product given the value on the first, as a
kernel. Use the more general condKernel.
Equations
- ProbabilityTheory.condKernelReal ρ = { val := fun (a : α) => StieltjesFunction.measure (ProbabilityTheory.condCDF ρ a), property := ⋯ }
Instances For
instance
ProbabilityTheory.instIsMarkovKernelRealMeasurableSpaceCondKernelReal
{α : Type u_1}
{mα : MeasurableSpace α}
(ρ : MeasureTheory.Measure (α × ℝ))
:
Equations
- ⋯ = ⋯
theorem
ProbabilityTheory.condKernelReal_Iic
{α : Type u_1}
{mα : MeasurableSpace α}
(ρ : MeasureTheory.Measure (α × ℝ))
(a : α)
(x : ℝ)
:
↑↑((ProbabilityTheory.condKernelReal ρ) a) (Set.Iic x) = ENNReal.ofReal (↑(ProbabilityTheory.condCDF ρ a) x)
theorem
ProbabilityTheory.set_lintegral_condKernelReal_Iic
{α : Type u_1}
{mα : MeasurableSpace α}
(ρ : MeasureTheory.Measure (α × ℝ))
[MeasureTheory.IsFiniteMeasure ρ]
(x : ℝ)
{s : Set α}
(hs : MeasurableSet s)
:
∫⁻ (a : α) in s, ↑↑((ProbabilityTheory.condKernelReal ρ) a) (Set.Iic x) ∂MeasureTheory.Measure.fst ρ = ↑↑ρ (s ×ˢ Set.Iic x)
theorem
ProbabilityTheory.set_lintegral_condKernelReal_univ
{α : Type u_1}
{mα : MeasurableSpace α}
(ρ : MeasureTheory.Measure (α × ℝ))
{s : Set α}
(hs : MeasurableSet s)
:
∫⁻ (a : α) in s, ↑↑((ProbabilityTheory.condKernelReal ρ) a) Set.univ ∂MeasureTheory.Measure.fst ρ = ↑↑ρ (s ×ˢ Set.univ)
theorem
ProbabilityTheory.lintegral_condKernelReal_univ
{α : Type u_1}
{mα : MeasurableSpace α}
(ρ : MeasureTheory.Measure (α × ℝ))
:
∫⁻ (a : α), ↑↑((ProbabilityTheory.condKernelReal ρ) a) Set.univ ∂MeasureTheory.Measure.fst ρ = ↑↑ρ Set.univ
theorem
ProbabilityTheory.set_lintegral_condKernelReal_prod
{α : Type u_1}
{mα : MeasurableSpace α}
(ρ : MeasureTheory.Measure (α × ℝ))
[MeasureTheory.IsFiniteMeasure ρ]
{s : Set α}
(hs : MeasurableSet s)
{t : Set ℝ}
(ht : MeasurableSet t)
:
∫⁻ (a : α) in s, ↑↑((ProbabilityTheory.condKernelReal ρ) a) t ∂MeasureTheory.Measure.fst ρ = ↑↑ρ (s ×ˢ t)
theorem
ProbabilityTheory.lintegral_condKernelReal_mem
{α : Type u_1}
{mα : MeasurableSpace α}
(ρ : MeasureTheory.Measure (α × ℝ))
[MeasureTheory.IsFiniteMeasure ρ]
{s : Set (α × ℝ)}
(hs : MeasurableSet s)
:
∫⁻ (a : α), ↑↑((ProbabilityTheory.condKernelReal ρ) a) {x : ℝ | (a, x) ∈ s} ∂MeasureTheory.Measure.fst ρ = ↑↑ρ s
theorem
ProbabilityTheory.kernel.const_eq_compProd_real
{α : Type u_1}
{mα : MeasurableSpace α}
(γ : Type u_2)
[MeasurableSpace γ]
(ρ : MeasureTheory.Measure (α × ℝ))
[MeasureTheory.IsFiniteMeasure ρ]
:
theorem
ProbabilityTheory.measure_eq_compProd_real
{α : Type u_1}
{mα : MeasurableSpace α}
(ρ : MeasureTheory.Measure (α × ℝ))
[MeasureTheory.IsFiniteMeasure ρ]
:
theorem
ProbabilityTheory.lintegral_condKernelReal
{α : Type u_1}
{mα : MeasurableSpace α}
(ρ : MeasureTheory.Measure (α × ℝ))
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × ℝ → ENNReal}
(hf : Measurable f)
:
∫⁻ (a : α), ∫⁻ (y : ℝ), f (a, y) ∂(ProbabilityTheory.condKernelReal ρ) a ∂MeasureTheory.Measure.fst ρ = ∫⁻ (x : α × ℝ), f x ∂ρ
theorem
ProbabilityTheory.ae_condKernelReal_eq_one
{α : Type u_1}
{mα : MeasurableSpace α}
(ρ : MeasureTheory.Measure (α × ℝ))
[MeasureTheory.IsFiniteMeasure ρ]
{s : Set ℝ}
(hs : MeasurableSet s)
(hρ : ↑↑ρ {x : α × ℝ | x.2 ∈ sᶜ} = 0)
:
∀ᵐ (a : α) ∂MeasureTheory.Measure.fst ρ, ↑↑((ProbabilityTheory.condKernelReal ρ) a) s = 1
Disintegration of measures on standard Borel spaces #
Since every standard Borel space embeds measurably into ℝ, we can generalize the disintegration
property on ℝ to all these spaces.
theorem
ProbabilityTheory.exists_cond_kernel
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
(γ : Type u_3)
[MeasurableSpace γ]
:
Existence of a conditional kernel. Use the definition condKernel to get that kernel.
@[irreducible]
noncomputable def
MeasureTheory.Measure.condKernel
{α : Type u_3}
{mα : MeasurableSpace α}
{Ω : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
:
↥(ProbabilityTheory.kernel α Ω)
Conditional kernel of a measure on a product space: a Markov kernel such that
ρ = ρ.fst ⊗ₘ ρ.condKernel (see ProbabilityTheory.measure_eq_compProd).
Instances For
theorem
MeasureTheory.Measure.condKernel_def
{α : Type u_3}
{mα : MeasurableSpace α}
{Ω : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
:
theorem
ProbabilityTheory.condKernel_def
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
:
instance
ProbabilityTheory.instIsMarkovKernelCondKernel
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
:
Equations
- ⋯ = ⋯
theorem
ProbabilityTheory.kernel.const_unit_eq_compProd
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
:
theorem
ProbabilityTheory.measure_eq_compProd
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
:
Disintegration of finite product measures on α × Ω, where Ω is standard 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
ProbabilityTheory.condKernel ρ.
theorem
ProbabilityTheory.kernel.const_eq_compProd
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(γ : Type u_3)
[MeasurableSpace γ]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
:
Disintegration of constant kernels. A constant kernel on a product space α × Ω, where Ω
is standard 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 ProbabilityTheory.condKernel ρ.
theorem
ProbabilityTheory.condKernel_apply_of_ne_zero_of_measurableSet
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSingletonClass α]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{x : α}
(hx : ↑↑(MeasureTheory.Measure.fst ρ) {x} ≠ 0)
{s : Set Ω}
(hs : MeasurableSet s)
:
↑↑((MeasureTheory.Measure.condKernel ρ) x) s = (↑↑(MeasureTheory.Measure.fst ρ) {x})⁻¹ * ↑↑ρ ({x} ×ˢ s)
Auxiliary lemma for condKernel_apply_of_ne_zero.
theorem
ProbabilityTheory.condKernel_apply_of_ne_zero
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasurableSingletonClass α]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{x : α}
(hx : ↑↑(MeasureTheory.Measure.fst ρ) {x} ≠ 0)
(s : Set Ω)
:
↑↑((MeasureTheory.Measure.condKernel ρ) x) s = (↑↑(MeasureTheory.Measure.fst ρ) {x})⁻¹ * ↑↑ρ ({x} ×ˢ s)
If the singleton {x} has non-zero mass for ρ.fst, then for all s : Set Ω,
ρ.condKernel x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s) .
theorem
ProbabilityTheory.lintegral_condKernel_mem
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
{s : Set (α × Ω)}
(hs : MeasurableSet s)
:
∫⁻ (a : α), ↑↑((MeasureTheory.Measure.condKernel ρ) a) {x : Ω | (a, x) ∈ s} ∂MeasureTheory.Measure.fst ρ = ↑↑ρ s
theorem
ProbabilityTheory.set_lintegral_condKernel_eq_measure_prod
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
{s : Set α}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
:
∫⁻ (a : α) in s, ↑↑((MeasureTheory.Measure.condKernel ρ) a) t ∂MeasureTheory.Measure.fst ρ = ↑↑ρ (s ×ˢ t)
theorem
ProbabilityTheory.lintegral_condKernel
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → ENNReal}
(hf : Measurable f)
:
∫⁻ (a : α), ∫⁻ (ω : Ω), f (a, ω) ∂(MeasureTheory.Measure.condKernel ρ) a ∂MeasureTheory.Measure.fst ρ = ∫⁻ (x : α × Ω), f x ∂ρ
theorem
ProbabilityTheory.set_lintegral_condKernel
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → ENNReal}
(hf : Measurable f)
{s : Set α}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
:
∫⁻ (a : α) in s, ∫⁻ (ω : Ω) in t, f (a, ω) ∂(MeasureTheory.Measure.condKernel ρ) a ∂MeasureTheory.Measure.fst ρ = ∫⁻ (x : α × Ω) in s ×ˢ t, f x ∂ρ
theorem
ProbabilityTheory.set_lintegral_condKernel_univ_right
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → ENNReal}
(hf : Measurable f)
{s : Set α}
(hs : MeasurableSet s)
:
∫⁻ (a : α) in s, ∫⁻ (ω : Ω), f (a, ω) ∂(MeasureTheory.Measure.condKernel ρ) a ∂MeasureTheory.Measure.fst ρ = ∫⁻ (x : α × Ω) in s ×ˢ Set.univ, f x ∂ρ
theorem
ProbabilityTheory.set_lintegral_condKernel_univ_left
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → ENNReal}
(hf : Measurable f)
{t : Set Ω}
(ht : MeasurableSet t)
:
∫⁻ (a : α), ∫⁻ (ω : Ω) in t, f (a, ω) ∂(MeasureTheory.Measure.condKernel ρ) a ∂MeasureTheory.Measure.fst ρ = ∫⁻ (x : α × Ω) in Set.univ ×ˢ t, f x ∂ρ
theorem
MeasureTheory.AEStronglyMeasurable.integral_condKernel
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → E}
(hf : MeasureTheory.AEStronglyMeasurable f ρ)
:
MeasureTheory.AEStronglyMeasurable (fun (x : α) => ∫ (y : Ω), f (x, y) ∂(MeasureTheory.Measure.condKernel ρ) x)
(MeasureTheory.Measure.fst ρ)
theorem
ProbabilityTheory.integral_condKernel
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → E}
(hf : MeasureTheory.Integrable f ρ)
:
∫ (a : α), ∫ (x : Ω), f (a, x) ∂(MeasureTheory.Measure.condKernel ρ) a ∂MeasureTheory.Measure.fst ρ = ∫ (ω : α × Ω), f ω ∂ρ
theorem
ProbabilityTheory.set_integral_condKernel
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → E}
{s : Set α}
(hs : MeasurableSet s)
{t : Set Ω}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ t) ρ)
:
∫ (a : α) in s, ∫ (ω : Ω) in t, f (a, ω) ∂(MeasureTheory.Measure.condKernel ρ) a ∂MeasureTheory.Measure.fst ρ = ∫ (x : α × Ω) in s ×ˢ t, f x ∂ρ
theorem
ProbabilityTheory.set_integral_condKernel_univ_right
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → E}
{s : Set α}
(hs : MeasurableSet s)
(hf : MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) ρ)
:
∫ (a : α) in s, ∫ (ω : Ω), f (a, ω) ∂(MeasureTheory.Measure.condKernel ρ) a ∂MeasureTheory.Measure.fst ρ = ∫ (x : α × Ω) in s ×ˢ Set.univ, f x ∂ρ
theorem
ProbabilityTheory.set_integral_condKernel_univ_left
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → E}
{t : Set Ω}
(ht : MeasurableSet t)
(hf : MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ρ)
:
∫ (a : α), ∫ (ω : Ω) in t, f (a, ω) ∂(MeasureTheory.Measure.condKernel ρ) a ∂MeasureTheory.Measure.fst ρ = ∫ (x : α × Ω) in Set.univ ×ˢ t, f x ∂ρ
Uniqueness #
This section will prove that the conditional kernel is unique almost everywhere.
theorem
ProbabilityTheory.eq_condKernel_of_measure_eq_compProd'
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
(κ : ↥(ProbabilityTheory.kernel α Ω))
[ProbabilityTheory.IsSFiniteKernel κ]
(hκ : ρ = MeasureTheory.Measure.compProd (MeasureTheory.Measure.fst ρ) κ)
{s : Set Ω}
(hs : MeasurableSet s)
:
∀ᵐ (x : α) ∂MeasureTheory.Measure.fst ρ, ↑↑(κ x) s = ↑↑((MeasureTheory.Measure.condKernel ρ) x) s
A s-finite kernel which satisfy the disintegration property of the given measure ρ is almost
everywhere equal to the disintegration kernel of ρ when evaluated on a measurable set.
This theorem in the case of finite kernels is weaker than eq_condKernel_of_measure_eq_compProd
which asserts that the kernels are equal almost everywhere and not just on a given measurable
set.
theorem
ProbabilityTheory.eq_condKernel_of_measure_eq_compProd_real
{α : Type u_1}
{mα : MeasurableSpace α}
(ρ : MeasureTheory.Measure (α × ℝ))
[MeasureTheory.IsFiniteMeasure ρ]
(κ : ↥(ProbabilityTheory.kernel α ℝ))
[ProbabilityTheory.IsFiniteKernel κ]
(hκ : ρ = MeasureTheory.Measure.compProd (MeasureTheory.Measure.fst ρ) κ)
:
∀ᵐ (x : α) ∂MeasureTheory.Measure.fst ρ, κ x = (MeasureTheory.Measure.condKernel ρ) x
theorem
ProbabilityTheory.eq_condKernel_of_measure_eq_compProd
{α : Type u_1}
{mα : MeasurableSpace α}
{Ω : Type u_2}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
(ρ : MeasureTheory.Measure (α × Ω))
[MeasureTheory.IsFiniteMeasure ρ]
(κ : ↥(ProbabilityTheory.kernel α Ω))
[ProbabilityTheory.IsFiniteKernel κ]
(hκ : ρ = MeasureTheory.Measure.compProd (MeasureTheory.Measure.fst ρ) κ)
:
∀ᵐ (x : α) ∂MeasureTheory.Measure.fst ρ, κ x = (MeasureTheory.Measure.condKernel ρ) x
A finite kernel which satisfies the disintegration property is almost everywhere equal to the disintegration kernel.
Integrability #
We place these lemmas in the MeasureTheory namespace to enable dot notation.
theorem
MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff
{α : Type u_1}
{Ω : Type u_2}
{F : Type u_4}
{mα : MeasurableSpace α}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → F}
(hf : MeasureTheory.AEStronglyMeasurable f ρ)
:
(∀ᵐ (a : α) ∂MeasureTheory.Measure.fst ρ,
MeasureTheory.Integrable (fun (ω : Ω) => f (a, ω)) ((MeasureTheory.Measure.condKernel ρ) a)) ∧ MeasureTheory.Integrable (fun (a : α) => ∫ (ω : Ω), ‖f (a, ω)‖ ∂(MeasureTheory.Measure.condKernel ρ) a)
(MeasureTheory.Measure.fst ρ) ↔ MeasureTheory.Integrable f ρ
theorem
MeasureTheory.Integrable.condKernel_ae
{α : Type u_1}
{Ω : Type u_2}
{F : Type u_4}
{mα : MeasurableSpace α}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → F}
(hf_int : MeasureTheory.Integrable f ρ)
:
∀ᵐ (a : α) ∂MeasureTheory.Measure.fst ρ,
MeasureTheory.Integrable (fun (ω : Ω) => f (a, ω)) ((MeasureTheory.Measure.condKernel ρ) a)
theorem
MeasureTheory.Integrable.integral_norm_condKernel
{α : Type u_1}
{Ω : Type u_2}
{F : Type u_4}
{mα : MeasurableSpace α}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → F}
(hf_int : MeasureTheory.Integrable f ρ)
:
MeasureTheory.Integrable (fun (x : α) => ∫ (y : Ω), ‖f (x, y)‖ ∂(MeasureTheory.Measure.condKernel ρ) x)
(MeasureTheory.Measure.fst ρ)
theorem
MeasureTheory.Integrable.norm_integral_condKernel
{α : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mα : MeasurableSpace α}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → E}
(hf_int : MeasureTheory.Integrable f ρ)
:
MeasureTheory.Integrable (fun (x : α) => ‖∫ (y : Ω), f (x, y) ∂(MeasureTheory.Measure.condKernel ρ) x‖)
(MeasureTheory.Measure.fst ρ)
theorem
MeasureTheory.Integrable.integral_condKernel
{α : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mα : MeasurableSpace α}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ρ : MeasureTheory.Measure (α × Ω)}
[MeasureTheory.IsFiniteMeasure ρ]
{f : α × Ω → E}
(hf_int : MeasureTheory.Integrable f ρ)
:
MeasureTheory.Integrable (fun (x : α) => ∫ (y : Ω), f (x, y) ∂(MeasureTheory.Measure.condKernel ρ) x)
(MeasureTheory.Measure.fst ρ)