feat(MeasureTheory): add singularPart and rnDeriv lemmas (#11883)

Also golf and move `rnDeriv_restrict`.

Author: RemyDegenne

Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

@@ -238,6 +238,11 @@ theorem singularPart_zero (ν : Measure α) : (0 : Measure α).singularPart ν =
   singularPart_eq_zero_of_ac (AbsolutelyContinuous.zero _)
 #align measure_theory.measure.singular_part_zero MeasureTheory.Measure.singularPart_zero
 
+@[simp]
+lemma singularPart_zero_right (μ : Measure α) : μ.singularPart 0 = μ := by
+  conv_rhs => rw [haveLebesgueDecomposition_add μ 0]
+  simp
+
 lemma singularPart_eq_zero (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] :
     μ.singularPart ν = 0 ↔ μ ≪ ν := by
   have h_dec := haveLebesgueDecomposition_add μ ν
@@ -306,6 +311,12 @@ lemma singularPart_eq_self [μ.HaveLebesgueDecomposition ν] : μ.singularPart 
   · conv_rhs => rw [h_dec]
     rw [(withDensity_rnDeriv_eq_zero _ _).mpr h, add_zero]
 
+@[simp]
+lemma singularPart_singularPart (μ ν : Measure α) :
+    (μ.singularPart ν).singularPart ν = μ.singularPart ν := by
+  rw [Measure.singularPart_eq_self]
+  exact Measure.mutuallySingular_singularPart _ _
+
 instance singularPart.instIsFiniteMeasure [IsFiniteMeasure μ] :
     IsFiniteMeasure (μ.singularPart ν) :=
   isFiniteMeasure_of_le μ <| singularPart_le μ ν
@@ -462,6 +473,16 @@ theorem singularPart_add (μ₁ μ₂ ν : Measure α) [HaveLebesgueDecompositio
     ← haveLebesgueDecomposition_add μ₂ ν]
 #align measure_theory.measure.singular_part_add MeasureTheory.Measure.singularPart_add
 
+lemma singularPart_restrict (μ ν : Measure α) [HaveLebesgueDecomposition μ ν]
+    {s : Set α} (hs : MeasurableSet s) :
+    (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s := by
+  refine (Measure.eq_singularPart (f := s.indicator (μ.rnDeriv ν)) ?_ ?_ ?_).symm
+  · exact (μ.measurable_rnDeriv ν).indicator hs
+  · exact (Measure.mutuallySingular_singularPart μ ν).restrict s
+  · ext t
+    rw [withDensity_indicator hs, ← restrict_withDensity hs, ← Measure.restrict_add,
+      ← μ.haveLebesgueDecomposition_add ν]
+
 /-- Given measures `μ` and `ν`, if `s` is a measure mutually singular to `ν` and `f` is a
 measurable function such that `μ = s + fν`, then `f = μ.rnDeriv ν`.
 
@@ -545,6 +566,14 @@ theorem rnDeriv_withDensity (ν : Measure α) [SigmaFinite ν] {f : α → ℝ
   rnDeriv_withDensity₀ ν hf.aemeasurable
 #align measure_theory.measure.rn_deriv_with_density MeasureTheory.Measure.rnDeriv_withDensity
 
+lemma rnDeriv_restrict (μ ν : Measure α) [HaveLebesgueDecomposition μ ν] [SigmaFinite ν]
+    {s : Set α} (hs : MeasurableSet s) :
+    (μ.restrict s).rnDeriv ν =ᵐ[ν] s.indicator (μ.rnDeriv ν) := by
+  refine (eq_rnDeriv (s := (μ.restrict s).singularPart ν)
+    ((measurable_rnDeriv _ _).indicator hs) (mutuallySingular_singularPart _ _) ?_).symm
+  rw [singularPart_restrict _ _ hs, withDensity_indicator hs, ← restrict_withDensity hs,
+    ← Measure.restrict_add, ← μ.haveLebesgueDecomposition_add ν]
+
 /-- The Radon-Nikodym derivative of the restriction of a measure to a measurable set is the
 indicator function of this set. -/
 theorem rnDeriv_restrict_self (ν : Measure α) [SigmaFinite ν] {s : Set α} (hs : MeasurableSet s) :

Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

@@ -189,18 +189,6 @@ lemma rnDeriv_withDensity_right (μ ν : Measure α) [SigmaFinite μ] [SigmaFini
 
 end rnDeriv_withDensity_leftRight
 
-theorem rnDeriv_restrict (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν]
-    {s : Set α} (hs : MeasurableSet s) :
-    (μ.restrict s).rnDeriv ν =ᵐ[ν] s.indicator (μ.rnDeriv ν) := by
-  rw [← withDensity_indicator_one hs]
-  refine (rnDeriv_withDensity_left ?_ ?_ ?_).trans (ae_of_all _ (fun x ↦ ?_))
-  · exact measurable_one.aemeasurable.indicator hs
-  · exact measurable_one.aemeasurable.indicator hs
-  · filter_upwards with x
-    simp only [Set.indicator_apply, Pi.one_apply, ne_eq]
-    split_ifs <;> simp [ENNReal.zero_ne_top]
-  · simp [Set.indicator_apply]
-
 lemma rnDeriv_eq_zero_of_mutuallySingular [SigmaFinite μ] {ν' : Measure α}
     [SigmaFinite ν'] (h : μ ⟂ₘ ν) (hνν' : ν ≪ ν') :
     μ.rnDeriv ν' =ᵐ[ν] 0 := by

Mathlib/MeasureTheory/Measure/MutuallySingular.lean

@@ -151,6 +151,11 @@ theorem smul_nnreal (r : ℝ≥0) (h : ν ⟂ₘ μ) : r • ν ⟂ₘ μ :=
   h.smul r
 #align measure_theory.measure.mutually_singular.smul_nnreal MeasureTheory.Measure.MutuallySingular.smul_nnreal
 
+lemma restrict (h : μ ⟂ₘ ν) (s : Set α) : μ.restrict s ⟂ₘ ν := by
+  refine ⟨h.nullSet, h.measurableSet_nullSet, ?_, h.measure_compl_nullSet⟩
+  rw [Measure.restrict_apply h.measurableSet_nullSet]
+  exact measure_mono_null (Set.inter_subset_left _ _) h.measure_nullSet
+
 end MutuallySingular
 
 lemma eq_zero_of_absolutelyContinuous_of_mutuallySingular {μ ν : Measure α}

Mathlib/MeasureTheory/Measure/Trim.lean

@@ -129,4 +129,10 @@ theorem sigmaFinite_trim_bot_iff : SigmaFinite (μ.trim bot_le) ↔ IsFiniteMeas
   · rwa [trim_measurableSet_eq bot_le MeasurableSet.univ]
 #align measure_theory.sigma_finite_trim_bot_iff MeasureTheory.sigmaFinite_trim_bot_iff
 
+lemma Measure.AbsolutelyContinuous.trim {ν : Measure α} (hμν : μ ≪ ν) (hm : m ≤ m0) :
+    μ.trim hm ≪ ν.trim hm := by
+  refine Measure.AbsolutelyContinuous.mk (fun s hs hsν ↦ ?_)
+  rw [trim_measurableSet_eq hm hs] at hsν ⊢
+  exact hμν hsν
+
 end MeasureTheory

Mathlib/MeasureTheory/Measure/WithDensity.lean

@@ -220,6 +220,13 @@ theorem restrict_withDensity' [SFinite μ] (s : Set α) (f : α → ℝ≥0∞)
   rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply' _ (t ∩ s),
     restrict_restrict ht]
 
+lemma trim_withDensity {m m0 : MeasurableSpace α} {μ : Measure α}
+    (hm : m ≤ m0) {f : α → ℝ≥0∞} (hf : Measurable[m] f) :
+    (μ.withDensity f).trim hm = (μ.trim hm).withDensity f := by
+  refine @Measure.ext _ m _ _ (fun s hs ↦ ?_)
+  rw [withDensity_apply _ hs, restrict_trim _ _ hs, lintegral_trim _ hf, trim_measurableSet_eq _ hs,
+    withDensity_apply _ (hm s hs)]
+
 lemma Measure.MutuallySingular.withDensity {ν : Measure α} {f : α → ℝ≥0∞} (h : μ ⟂ₘ ν) :
     μ.withDensity f ⟂ₘ ν :=
   MutuallySingular.mono_ac h (withDensity_absolutelyContinuous _ _) AbsolutelyContinuous.rfl