Radon-Nikodym derivative and Lebesgue decomposition for kernels #
theorem
MeasureTheory.Measure.absolutelyContinuous_compProd_left_iff
{α : Type u_1}
{γ : Type u_2}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α γ}
[MeasureTheory.SFinite μ]
[MeasureTheory.SFinite ν]
[ProbabilityTheory.IsFiniteKernel κ]
[∀ (a : α), NeZero (κ a)]
:
(μ.compProd κ).AbsolutelyContinuous (ν.compProd κ) ↔ μ.AbsolutelyContinuous ν
theorem
MeasureTheory.Measure.mutuallySingular_compProd_left
{α : Type u_1}
{γ : Type u_2}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(hμν : μ.MutuallySingular ν)
(κ : ProbabilityTheory.Kernel α γ)
(η : ProbabilityTheory.Kernel α γ)
:
(μ.compProd κ).MutuallySingular (ν.compProd η)
theorem
MeasureTheory.Measure.mutuallySingular_of_mutuallySingular_compProd
{α : Type u_1}
{γ : Type u_2}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α γ}
{η : ProbabilityTheory.Kernel α γ}
{ξ : MeasureTheory.Measure α}
[MeasureTheory.SFinite μ]
[MeasureTheory.SFinite ν]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
(h : (μ.compProd κ).MutuallySingular (ν.compProd η))
(hμ : ξ.AbsolutelyContinuous μ)
(hν : ξ.AbsolutelyContinuous ν)
:
∀ᵐ (x : α) ∂ξ, (κ x).MutuallySingular (η x)
theorem
MeasureTheory.Measure.mutuallySingular_compProd_iff_of_same_right
{α : Type u_1}
{γ : Type u_2}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α γ)
[ProbabilityTheory.IsFiniteKernel κ]
[hκ : ∀ (x : α), NeZero (κ x)]
:
(μ.compProd κ).MutuallySingular (ν.compProd κ) ↔ μ.MutuallySingular ν
theorem
MeasureTheory.Measure.absolutelyContinuous_of_add_of_mutuallySingular
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν₁ : MeasureTheory.Measure α}
{ν₂ : MeasureTheory.Measure α}
(h_ms : μ.MutuallySingular ν₂)
(h : μ.AbsolutelyContinuous (ν₁ + ν₂))
:
μ.AbsolutelyContinuous ν₁
theorem
MeasureTheory.Measure.absolutelyContinuous_compProd_of_compProd
{α : Type u_1}
{γ : Type u_2}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α γ}
{η : ProbabilityTheory.Kernel α γ}
[MeasureTheory.SFinite ν]
[ProbabilityTheory.IsSFiniteKernel η]
(hμν : μ.AbsolutelyContinuous ν)
(hκη : (μ.compProd κ).AbsolutelyContinuous (μ.compProd η))
:
(μ.compProd κ).AbsolutelyContinuous (ν.compProd η)
theorem
MeasureTheory.Measure.absolutelyContinuous_compProd_of_compProd'
{α : Type u_1}
{γ : Type u_2}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α γ}
{η : ProbabilityTheory.Kernel α γ}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
(hκη : (μ.compProd κ).AbsolutelyContinuous (ν.compProd η))
:
(μ.compProd κ).AbsolutelyContinuous (μ.compProd η)
theorem
MeasureTheory.Measure.absolutelyContinuous_compProd_iff'
{α : Type u_1}
{γ : Type u_2}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α γ}
{η : ProbabilityTheory.Kernel α γ}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
[∀ (x : α), NeZero (κ x)]
:
theorem
MeasureTheory.Measure.mutuallySingular_compProd_right
{α : Type u_1}
{γ : Type u_2}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
[MeasurableSpace.CountableOrCountablyGenerated α γ]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
{κ : ProbabilityTheory.Kernel α γ}
{η : ProbabilityTheory.Kernel α γ}
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(hκη : ∀ᵐ (a : α) ∂μ, (κ a).MutuallySingular (η a))
:
(μ.compProd κ).MutuallySingular (ν.compProd η)
theorem
MeasureTheory.Measure.mutuallySingular_compProd_right'
{α : Type u_1}
{γ : Type u_2}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
[MeasurableSpace.CountableOrCountablyGenerated α γ]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
{κ : ProbabilityTheory.Kernel α γ}
{η : ProbabilityTheory.Kernel α γ}
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(hκη : ∀ᵐ (a : α) ∂ν, (κ a).MutuallySingular (η a))
:
(μ.compProd κ).MutuallySingular (ν.compProd η)
theorem
MeasureTheory.Measure.mutuallySingular_compProd_iff_of_same_left
{α : Type u_1}
{γ : Type u_2}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
[MeasurableSpace.CountableOrCountablyGenerated α γ]
(μ : MeasureTheory.Measure α)
[MeasureTheory.SFinite μ]
(κ : ProbabilityTheory.Kernel α γ)
(η : ProbabilityTheory.Kernel α γ)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
(μ.compProd κ).MutuallySingular (μ.compProd η) ↔ ∀ᵐ (a : α) ∂μ, (κ a).MutuallySingular (η a)
theorem
MeasureTheory.Measure.absolutelyContinuous_kernel_of_compProd
{α : Type u_1}
{γ : Type u_2}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α γ}
{η : ProbabilityTheory.Kernel α γ}
[MeasurableSpace.CountableOrCountablyGenerated α γ]
[MeasureTheory.SFinite μ]
[MeasureTheory.SFinite ν]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(h : (μ.compProd κ).AbsolutelyContinuous (ν.compProd η))
:
∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)
theorem
MeasureTheory.Measure.absolutelyContinuous_compProd_iff
{α : Type u_1}
{γ : Type u_2}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α γ}
{η : ProbabilityTheory.Kernel α γ}
[MeasurableSpace.CountableOrCountablyGenerated α γ]
[MeasureTheory.SFinite μ]
[MeasureTheory.SFinite ν]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[∀ (a : α), NeZero (κ a)]
:
theorem
MeasureTheory.Measure.absolutelyContinuous_compProd_right_iff
{α : Type u_1}
{γ : Type u_2}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
[MeasurableSpace.CountableOrCountablyGenerated α γ]
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α γ}
{η : ProbabilityTheory.Kernel α γ}
[MeasureTheory.SFinite μ]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
(μ.compProd κ).AbsolutelyContinuous (μ.compProd η) ↔ ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)
theorem
ProbabilityTheory.Kernel.absolutelyContinuous_compProd_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
:
∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace γ}
[inst : MeasurableSpace.CountableOrCountablyGenerated β γ] {κ₁ η₁ : ProbabilityTheory.Kernel α β}
{κ₂ η₂ : ProbabilityTheory.Kernel (α × β) γ} [inst : ProbabilityTheory.IsSFiniteKernel κ₁]
[inst : ProbabilityTheory.IsSFiniteKernel η₁] [inst : ProbabilityTheory.IsFiniteKernel κ₂]
[inst : ProbabilityTheory.IsFiniteKernel η₂] (a : α) [inst : ∀ (b : β), NeZero (κ₂ (a, b))],
((κ₁.compProd κ₂) a).AbsolutelyContinuous ((η₁.compProd η₂) a) ↔ (κ₁ a).AbsolutelyContinuous (η₁ a) ∧ ∀ᵐ (b : β) ∂κ₁ a, (κ₂ (a, b)).AbsolutelyContinuous (η₂ (a, b))