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)