Absolute continuity of the composition of measures and kernels #
This file contains some results about the absolute continuity of the composition of measures and
kernels which use an assumption CountableOrCountablyGenerated α β on the measurable spaces.
Results that hold without that assumption are in files about the definitions of compositions and
products, like Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean and
Mathlib/Probability/Kernel/Composition/MeasureComp.lean.
The assumption ensures the measurability of the sets where two kernels are absolutely continuous or mutually singular.
Main statements #
absolutelyContinuous_compProd_iff':μ ⊗ₘ κ ≪ ν ⊗ₘ η ↔ μ ≪ ν ∧ ∀ᵐ a ∂μ, κ a ≪ η a.
theorem
MeasureTheory.Measure.MutuallySingular.compProd_of_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ η : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ ν : Measure α)
(hκη : ∀ᵐ (a : α) ∂μ, (κ a).MutuallySingular (η a))
:
(μ.compProd κ).MutuallySingular (ν.compProd η)
theorem
MeasureTheory.Measure.MutuallySingular.compProd_of_right'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ η : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ ν : Measure α)
(hκη : ∀ᵐ (a : α) ∂ν, (κ a).MutuallySingular (η a))
:
(μ.compProd κ).MutuallySingular (ν.compProd η)
theorem
MeasureTheory.Measure.mutuallySingular_compProd_right_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasurableSpace.CountableOrCountablyGenerated α β]
[SFinite μ]
:
theorem
MeasureTheory.Measure.AbsolutelyContinuous.kernel_of_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasurableSpace.CountableOrCountablyGenerated α β]
[SFinite μ]
(h : (μ.compProd κ).AbsolutelyContinuous (ν.compProd η))
:
∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)
theorem
MeasureTheory.Measure.absolutelyContinuous_compProd_iff'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasurableSpace.CountableOrCountablyGenerated α β]
[SFinite μ]
[SFinite ν]
[∀ (a : α), NeZero (κ a)]
:
(μ.compProd κ).AbsolutelyContinuous (ν.compProd η) ↔ μ.AbsolutelyContinuous ν ∧ ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)
theorem
MeasureTheory.Measure.absolutelyContinuous_compProd_right_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{κ η : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasurableSpace.CountableOrCountablyGenerated α β]
[SFinite μ]
:
(μ.compProd κ).AbsolutelyContinuous (μ.compProd η) ↔ ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)