From 1dd1a104324ab698754a2e288b7c6750f7729c34 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Degenne?= <Remydegenne@gmail.com>
Date: Sun, 13 Oct 2024 11:01:00 +0000
Subject: [PATCH] feat(Probability/Kernel): `IsFiniteKernel` instances (#17681)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`IsFiniteKernel` instances for `withDensity η (rnDeriv κ η)` and `singularPart κ η`.
---
 .../MeasureTheory/Decomposition/RadonNikodym.lean |  3 +++
 Mathlib/Probability/Kernel/RadonNikodym.lean      | 15 +++++++++++++++
 2 files changed, 18 insertions(+)

diff --git a/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean b/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
index f2347396e6fc3..83a31d388715d 100644
--- 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
index 9b011fdfed324..9e0392d8f287b 100644
--- 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