feat(MeasureTheory): μ.singularPart (r • ν) = μ.singularPart ν (#8040)

Prove 3 lemmas:
- an instance `MeasurableSMul ℝ≥0 ℝ≥0∞`
- `instance haveLebesgueDecomposition_smul_right (μ ν : Measure α) [HaveLebesgueDecomposition μ ν]
    (r : ℝ≥0) : μ.HaveLebesgueDecomposition (r • ν)`
- `theorem singularPart_smul_right (μ ν : Measure α) (r : ℝ≥0) (hr : r ≠ 0) :
    μ.singularPart (r • ν) = μ.singularPart ν`

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -2101,6 +2101,14 @@ instance instMeasurableInv : MeasurableInv ℝ≥0∞ :=
   ⟨continuous_inv.measurable⟩
 #align ennreal.has_measurable_inv ENNReal.instMeasurableInv
 
+instance : MeasurableSMul ℝ≥0 ℝ≥0∞ where
+  measurable_const_smul := by
+    simp_rw [ENNReal.smul_def]
+    exact fun _ ↦ MeasurableSMul.measurable_const_smul _
+  measurable_smul_const := fun x ↦ by
+    simp_rw [ENNReal.smul_def]
+    exact measurable_coe_nnreal_ennreal.mul_const _
+
 end ENNReal
 
 @[measurability]

Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

@@ -120,6 +120,25 @@ instance haveLebesgueDecomposition_smul (μ ν : Measure α) [HaveLebesgueDecomp
       rfl
 #align measure_theory.measure.have_lebesgue_decomposition_smul MeasureTheory.Measure.haveLebesgueDecomposition_smul
 
+instance haveLebesgueDecomposition_smul_right (μ ν : Measure α) [HaveLebesgueDecomposition μ ν]
+    (r : ℝ≥0) :
+    μ.HaveLebesgueDecomposition (r • ν) where
+  lebesgue_decomposition := by
+    obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν
+    by_cases hr : r = 0
+    · exact ⟨⟨μ, 0⟩, measurable_const, by simp [hr], by simp⟩
+    refine ⟨⟨μ.singularPart ν, r⁻¹ • μ.rnDeriv ν⟩, ?_, ?_, ?_⟩
+    · change Measurable (r⁻¹ • μ.rnDeriv ν)
+      exact hmeas.const_smul _
+    · refine MutuallySingular.mono_ac hsing AbsolutelyContinuous.rfl ?_
+      exact absolutelyContinuous_of_le_smul le_rfl
+    · have : r⁻¹ • rnDeriv μ ν = ((r⁻¹ : ℝ≥0) : ℝ≥0∞) • rnDeriv μ ν := by simp [ENNReal.smul_def]
+      rw [this, withDensity_smul _ hmeas, ENNReal.smul_def r, withDensity_smul_measure,
+        ← smul_assoc, smul_eq_mul, ENNReal.coe_inv hr, ENNReal.inv_mul_cancel, one_smul]
+      · exact hadd
+      · simp [hr]
+      · exact ENNReal.coe_ne_top
+
 @[measurability]
 theorem measurable_rnDeriv (μ ν : Measure α) : Measurable <| μ.rnDeriv ν := by
   by_cases h : HaveLebesgueDecomposition μ ν
@@ -282,6 +301,23 @@ theorem singularPart_smul (μ ν : Measure α) (r : ℝ≥0) :
     exact @Measure.haveLebesgueDecomposition_smul _ _ _ _ hl' _
 #align measure_theory.measure.singular_part_smul MeasureTheory.Measure.singularPart_smul
 
+theorem singularPart_smul_right (μ ν : Measure α) (r : ℝ≥0) (hr : r ≠ 0) :
+    μ.singularPart (r • ν) = μ.singularPart ν := by
+  by_cases hl : HaveLebesgueDecomposition μ ν
+  · refine (eq_singularPart ((measurable_rnDeriv μ ν).const_smul r⁻¹) ?_ ?_).symm
+    · refine (mutuallySingular_singularPart μ ν).mono_ac AbsolutelyContinuous.rfl ?_
+      exact absolutelyContinuous_of_le_smul le_rfl
+    · rw [ENNReal.smul_def r, withDensity_smul_measure, ← withDensity_smul]
+      swap; · exact (measurable_rnDeriv _ _).const_smul _
+      convert haveLebesgueDecomposition_add μ ν
+      ext x
+      simp only [Pi.smul_apply, ne_eq]
+      rw [← ENNReal.smul_def, ← smul_assoc, smul_eq_mul, mul_inv_cancel hr, one_smul]
+  · rw [singularPart, singularPart, dif_neg hl, dif_neg]
+    refine fun hl' => hl ?_
+    rw [← inv_smul_smul₀ hr ν]
+    infer_instance
+
 theorem singularPart_add (μ₁ μ₂ ν : Measure α) [HaveLebesgueDecomposition μ₁ ν]
     [HaveLebesgueDecomposition μ₂ ν] :
     (μ₁ + μ₂).singularPart ν = μ₁.singularPart ν + μ₂.singularPart ν := by