feat(Probability/Kernel): IsFiniteKernel instances (#17681)

`IsFiniteKernel` instances for `withDensity η (rnDeriv κ η)` and `singularPart κ η`.
leanprover-community · Oct 13, 2024 · 1dd1a10 · 1dd1a10
1 parent 5640128
commit 1dd1a10
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 0 deletions.
diff --git a/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean b/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
@@ -305,6 +305,9 @@ lemma setLIntegral_rnDeriv_le (s : Set α) :
 @[deprecated (since := "2024-06-29")]
 alias set_lintegral_rnDeriv_le := setLIntegral_rnDeriv_le
 
+lemma lintegral_rnDeriv_le : ∫⁻ x, μ.rnDeriv ν x ∂ν ≤ μ Set.univ :=
+  (setLIntegral_univ _).symm ▸ Measure.setLIntegral_rnDeriv_le Set.univ
+
 lemma setLIntegral_rnDeriv' [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) {s : Set α}
     (hs : MeasurableSet s) :
     ∫⁻ x in s, μ.rnDeriv ν x ∂ν = μ s := by

diff --git a/Mathlib/Probability/Kernel/RadonNikodym.lean b/Mathlib/Probability/Kernel/RadonNikodym.lean
@@ -534,4 +534,19 @@ lemma eq_singularPart (h : κ = η.withDensity f + ξ)
 
 end Unique
 
+instance [hκ : IsFiniteKernel κ] [IsFiniteKernel η] :
+    IsFiniteKernel (withDensity η (rnDeriv κ η)) := by
+  refine ⟨hκ.bound, hκ.bound_lt_top, fun a ↦ ?_⟩
+  rw [Kernel.withDensity_apply', setLIntegral_univ]
+  swap; · exact measurable_rnDeriv κ η
+  rw [lintegral_congr_ae rnDeriv_eq_rnDeriv_measure]
+  exact Measure.lintegral_rnDeriv_le.trans (measure_le_bound _ _ _)
+
+instance [hκ : IsFiniteKernel κ] [IsFiniteKernel η] : IsFiniteKernel (singularPart κ η) := by
+  refine ⟨hκ.bound, hκ.bound_lt_top, fun a ↦ ?_⟩
+  have h : withDensity η (rnDeriv κ η) a univ + singularPart κ η a univ = κ a univ := by
+    conv_rhs => rw [← rnDeriv_add_singularPart κ η]
+    simp
+  exact (self_le_add_left _ _).trans (h.le.trans (measure_le_bound _ _ _))
+
 end ProbabilityTheory.Kernel