feat: generalize some lemmas using withDensity_apply' (#8383)

@sgouezel added a version of `withDensity_apply` that does not require measurability of the set if the measure is s-finite. This PR uses that result in other files of the library.

For results about `rnDeriv`, I put a prime on the version that assumes measurability of the set and no prime on the version for s-finite measures, as the second one should be the main use case.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: RemyDegenne <Remydegenne@gmail.com>

Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

@@ -320,28 +320,40 @@ lemma set_lintegral_rnDeriv_le (s : Set α) :
     ∫⁻ x in s, μ.rnDeriv ν x ∂ν ≤ μ s :=
   (withDensity_apply_le _ _).trans (Measure.le_iff'.1 (withDensity_rnDeriv_le μ ν) s)
 
-lemma set_lintegral_rnDeriv [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) {s : Set α}
+lemma set_lintegral_rnDeriv' [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) {s : Set α}
     (hs : MeasurableSet s) :
     ∫⁻ x in s, μ.rnDeriv ν x ∂ν = μ s := by
   rw [← withDensity_apply _ hs, Measure.withDensity_rnDeriv_eq _ _ hμν]
 
+lemma set_lintegral_rnDeriv [HaveLebesgueDecomposition μ ν] [SFinite ν]
+    (hμν : μ ≪ ν) (s : Set α) :
+    ∫⁻ x in s, μ.rnDeriv ν x ∂ν = μ s := by
+  rw [← withDensity_apply' _ s, Measure.withDensity_rnDeriv_eq _ _ hμν]
+
 lemma lintegral_rnDeriv [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) :
     ∫⁻ x, μ.rnDeriv ν x ∂ν = μ Set.univ := by
-  rw [← set_lintegral_univ, set_lintegral_rnDeriv hμν MeasurableSet.univ]
+  rw [← set_lintegral_univ, set_lintegral_rnDeriv' hμν MeasurableSet.univ]
 
 lemma integrableOn_toReal_rnDeriv {s : Set α} (hμs : μ s ≠ ∞) :
     IntegrableOn (fun x ↦ (μ.rnDeriv ν x).toReal) s ν := by
   refine integrable_toReal_of_lintegral_ne_top (Measure.measurable_rnDeriv _ _).aemeasurable ?_
   exact ((set_lintegral_rnDeriv_le _).trans_lt hμs.lt_top).ne
 
-lemma set_integral_toReal_rnDeriv_eq_withDensity [SigmaFinite μ]
+lemma set_integral_toReal_rnDeriv_eq_withDensity' [SigmaFinite μ]
     {s : Set α} (hs : MeasurableSet s) :
     ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν) s).toReal := by
   rw [integral_toReal (Measure.measurable_rnDeriv _ _).aemeasurable]
   · rw [ENNReal.toReal_eq_toReal_iff, ← withDensity_apply _ hs]
     simp
   · exact ae_restrict_of_ae (Measure.rnDeriv_lt_top _ _)
 
+lemma set_integral_toReal_rnDeriv_eq_withDensity [SigmaFinite μ] [SFinite ν] (s : Set α) :
+    ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν) s).toReal := by
+  rw [integral_toReal (Measure.measurable_rnDeriv _ _).aemeasurable]
+  · rw [ENNReal.toReal_eq_toReal_iff, ← withDensity_apply' _ s]
+    simp
+  · exact ae_restrict_of_ae (Measure.rnDeriv_lt_top _ _)
+
 lemma set_integral_toReal_rnDeriv_le [SigmaFinite μ] {s : Set α} (hμs : μ s ≠ ∞) :
     ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν ≤ (μ s).toReal := by
   set t := toMeasurable μ s with ht
@@ -353,20 +365,24 @@ lemma set_integral_toReal_rnDeriv_le [SigmaFinite μ] {s : Set α} (hμs : μ s
         · exact integrableOn_toReal_rnDeriv hμt
         · exact ae_of_all _ (by simp)
   _ ≤ (μ t).toReal := by
-        rw [set_integral_toReal_rnDeriv_eq_withDensity ht_m, ENNReal.toReal_le_toReal _ hμt]
+        rw [set_integral_toReal_rnDeriv_eq_withDensity' ht_m, ENNReal.toReal_le_toReal _ hμt]
         · exact withDensity_rnDeriv_le _ _ _ ht_m
         · exact ((withDensity_rnDeriv_le _ _ _ ht_m).trans_lt hμt.lt_top).ne
   _ = (μ s).toReal := by rw [← measure_toMeasurable s]
 
-lemma set_integral_toReal_rnDeriv [SigmaFinite μ] [HaveLebesgueDecomposition μ ν]
+lemma set_integral_toReal_rnDeriv' [SigmaFinite μ] [HaveLebesgueDecomposition μ ν]
     (hμν : μ ≪ ν) {s : Set α} (hs : MeasurableSet s) :
     ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν = (μ s).toReal := by
-  rw [set_integral_toReal_rnDeriv_eq_withDensity hs, Measure.withDensity_rnDeriv_eq _ _ hμν]
-#align measure_theory.measure.with_density_rn_deriv_to_real_eq MeasureTheory.Measure.set_integral_toReal_rnDeriv
+  rw [set_integral_toReal_rnDeriv_eq_withDensity' hs, Measure.withDensity_rnDeriv_eq _ _ hμν]
+#align measure_theory.measure.with_density_rn_deriv_to_real_eq MeasureTheory.Measure.set_integral_toReal_rnDeriv'
+
+lemma set_integral_toReal_rnDeriv [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) (s : Set α) :
+    ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν = (μ s).toReal := by
+  rw [set_integral_toReal_rnDeriv_eq_withDensity s, Measure.withDensity_rnDeriv_eq _ _ hμν]
 
 lemma integral_toReal_rnDeriv [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
     ∫ x, (μ.rnDeriv ν x).toReal ∂ν = (μ Set.univ).toReal := by
-  rw [← integral_univ, set_integral_toReal_rnDeriv hμν MeasurableSet.univ]
+  rw [← integral_univ, set_integral_toReal_rnDeriv hμν Set.univ]
 
 end Measure
 
@@ -380,7 +396,7 @@ theorem withDensityᵥ_rnDeriv_eq (s : SignedMeasure α) (μ : Measure α) [Sigm
     totalVariation_absolutelyContinuous_iff] at h
   · ext1 i hi
     rw [withDensityᵥ_apply (integrable_rnDeriv _ _) hi, rnDeriv, integral_sub,
-      set_integral_toReal_rnDeriv h.1 hi, set_integral_toReal_rnDeriv h.2 hi]
+      set_integral_toReal_rnDeriv h.1 i, set_integral_toReal_rnDeriv h.2 i]
     · conv_rhs => rw [← s.toSignedMeasure_toJordanDecomposition]
       erw [VectorMeasure.sub_apply]
       rw [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi]

Mathlib/Probability/Distributions/Gaussian.lean

@@ -199,14 +199,13 @@ instance instIsProbabilityMeasureGaussianReal (μ : ℝ) (v : ℝ≥0) :
     IsProbabilityMeasure (gaussianReal μ v) where
   measure_univ := by by_cases h : v = 0 <;> simp [gaussianReal_of_var_ne_zero, h]
 
-lemma gaussianReal_apply (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) {s : Set ℝ} (hs : MeasurableSet s) :
+lemma gaussianReal_apply (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) (s : Set ℝ) :
     gaussianReal μ v s = ∫⁻ x in s, gaussianPdf μ v x := by
-  rw [gaussianReal_of_var_ne_zero _ hv, withDensity_apply _ hs]
+  rw [gaussianReal_of_var_ne_zero _ hv, withDensity_apply' _ s]
 
-lemma gaussianReal_apply_eq_integral (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0)
-    {s : Set ℝ} (hs : MeasurableSet s) :
+lemma gaussianReal_apply_eq_integral (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) (s : Set ℝ) :
     gaussianReal μ v s = ENNReal.ofReal (∫ x in s, gaussianPdfReal μ v x) := by
-  rw [gaussianReal_apply _ hv hs, ofReal_integral_eq_lintegral_ofReal]
+  rw [gaussianReal_apply _ hv s, ofReal_integral_eq_lintegral_ofReal]
   · rfl
   · exact (integrable_gaussianPdfReal _ _).restrict
   · exact ae_of_all _ (gaussianPdfReal_nonneg _ _)
@@ -266,7 +265,7 @@ lemma gaussianReal_map_add_const (y : ℝ) :
   ext s' hs'
   rw [MeasurableEquiv.gaussianReal_map_symm_apply hv e he' hs']
   simp only [abs_neg, abs_one, MeasurableEquiv.coe_mk, Equiv.coe_fn_mk, one_mul, ne_eq]
-  rw [gaussianReal_apply_eq_integral _ hv hs']
+  rw [gaussianReal_apply_eq_integral _ hv s']
   simp [gaussianPdfReal_sub _ y, Homeomorph.addRight, ← sub_eq_add_neg]
 
 /-- The map of a Gaussian distribution by addition of a constant is a Gaussian. -/
@@ -296,7 +295,7 @@ lemma gaussianReal_map_const_mul (c : ℝ) :
   ext s' hs'
   rw [MeasurableEquiv.gaussianReal_map_symm_apply hv e he' hs']
   simp only [MeasurableEquiv.coe_mk, Equiv.coe_fn_mk, ne_eq, mul_eq_zero]
-  rw [gaussianReal_apply_eq_integral _ _ hs']
+  rw [gaussianReal_apply_eq_integral _ _ s']
   swap
   · simp only [ne_eq, mul_eq_zero, hv, or_false]
     rw [← NNReal.coe_eq]

Mathlib/Probability/Kernel/Basic.lean

@@ -308,6 +308,9 @@ instance isFiniteKernel_seq (κ : kernel α β) [h : IsSFiniteKernel κ] (n : 
   h.tsum_finite.choose_spec.1 n
 #align probability_theory.kernel.is_finite_kernel_seq ProbabilityTheory.kernel.isFiniteKernel_seq
 
+instance IsSFiniteKernel.sFinite [IsSFiniteKernel κ] (a : α) : SFinite (κ a) :=
+  ⟨⟨fun n ↦ seq κ n a, inferInstance, (measure_sum_seq κ a).symm⟩⟩
+
 instance IsSFiniteKernel.add (κ η : kernel α β) [IsSFiniteKernel κ] [IsSFiniteKernel η] :
     IsSFiniteKernel (κ + η) := by
   refine' ⟨⟨fun n => seq κ n + seq η n, fun n => inferInstance, _⟩⟩

Mathlib/Probability/Kernel/WithDensity.lean

@@ -66,10 +66,10 @@ protected theorem withDensity_apply (κ : kernel α β) [IsSFiniteKernel κ]
   rfl
 #align probability_theory.kernel.with_density_apply ProbabilityTheory.kernel.withDensity_apply
 
-theorem withDensity_apply' (κ : kernel α β) [IsSFiniteKernel κ]
-    (hf : Measurable (Function.uncurry f)) (a : α) {s : Set β} (hs : MeasurableSet s) :
+protected theorem withDensity_apply' (κ : kernel α β) [IsSFiniteKernel κ]
+    (hf : Measurable (Function.uncurry f)) (a : α) (s : Set β) :
     withDensity κ f a s = ∫⁻ b in s, f a b ∂κ a := by
-  rw [kernel.withDensity_apply κ hf, withDensity_apply _ hs]
+  rw [kernel.withDensity_apply κ hf, withDensity_apply' _ s]
 #align probability_theory.kernel.with_density_apply' ProbabilityTheory.kernel.withDensity_apply'
 
 theorem lintegral_withDensity (κ : kernel α β) [IsSFiniteKernel κ]
@@ -117,7 +117,7 @@ theorem withDensity_tsum [Countable ι] (κ : kernel α β) [IsSFiniteKernel κ]
   have h_sum_a : ∀ a, Summable fun n => f n a := fun a => Pi.summable.mpr fun b => ENNReal.summable
   have h_sum : Summable fun n => f n := Pi.summable.mpr h_sum_a
   ext a s hs
-  rw [sum_apply' _ a hs, withDensity_apply' κ _ a hs]
+  rw [sum_apply' _ a hs, kernel.withDensity_apply' κ _ a s]
   swap
   · have : Function.uncurry (∑' n, f n) = ∑' n, Function.uncurry (f n) := by
       ext1 p
@@ -131,7 +131,7 @@ theorem withDensity_tsum [Countable ι] (κ : kernel α β) [IsSFiniteKernel κ]
     rw [tsum_apply h_sum, tsum_apply (h_sum_a a)]
   rw [this, lintegral_tsum fun n => (Measurable.of_uncurry_left (hf n)).aemeasurable]
   congr with n
-  rw [withDensity_apply' _ (hf n) a hs]
+  rw [kernel.withDensity_apply' _ (hf n) a s]
 #align probability_theory.kernel.with_density_tsum ProbabilityTheory.kernel.withDensity_tsum
 
 /-- If a kernel `κ` is finite and a function `f : α → β → ℝ≥0∞` is bounded, then `withDensity κ f`
@@ -141,7 +141,7 @@ theorem isFiniteKernel_withDensity_of_bounded (κ : kernel α β) [IsFiniteKerne
   by_cases hf : Measurable (Function.uncurry f)
   · exact ⟨⟨B * IsFiniteKernel.bound κ, ENNReal.mul_lt_top hB_top (IsFiniteKernel.bound_ne_top κ),
       fun a => by
-        rw [withDensity_apply' κ hf a MeasurableSet.univ]
+        rw [kernel.withDensity_apply' κ hf a Set.univ]
         calc
           ∫⁻ b in Set.univ, f a b ∂κ a ≤ ∫⁻ _ in Set.univ, B ∂κ a := lintegral_mono (hf_B a)
           _ = B * κ a Set.univ := by