feat: results about subtraction of measures (leanprover-community#35018)

Main results:
* `sub_le_iff_le_add`: for `μ` and `ν` finite measures, `μ - ν ≤ ξ ↔ μ ≤ ξ + ν`.
* `withDensity_sub`: If `μ.withDensity g` is finite, then `μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g`.

Co-authored-by: Remy Degenne <remydegenne@gmail.com>

Author: RemyDegenne

Mathlib.lean

@@ -5206,6 +5206,7 @@ public import Mathlib.MeasureTheory.Measure.Restrict
 public import Mathlib.MeasureTheory.Measure.SeparableMeasure
 public import Mathlib.MeasureTheory.Measure.Stieltjes
 public import Mathlib.MeasureTheory.Measure.Sub
+public import Mathlib.MeasureTheory.Measure.SubFinite
 public import Mathlib.MeasureTheory.Measure.Support
 public import Mathlib.MeasureTheory.Measure.Tight
 public import Mathlib.MeasureTheory.Measure.TightNormed

Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean

@@ -1058,6 +1058,27 @@ lemma rnDeriv_add_of_mutuallySingular (ν₁ ν₂ μ : Measure α)
 
 end rnDeriv
 
+lemma add_sub_of_mutuallySingular {ξ : Measure α} (h : μ ⟂ₘ ξ) : μ + (ν - ξ) = μ + ν - ξ := by
+  let s := h.nullSet
+  have hs : MeasurableSet s := h.measurableSet_nullSet
+  have h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s := by
+    rw [h.restrict_nullSet, restrict_sub_eq_restrict_sub_restrict hs]
+    simp
+  have h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ =
+      μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ := by
+    rw [restrict_sub_eq_restrict_sub_restrict hs.compl, h.restrict_compl_nullSet]
+    simp
+  calc μ + (ν - ξ)
+  _ = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ := by
+    rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs]
+  _ = μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) := by abel
+  _ = (μ.restrict s + ν.restrict s - ξ.restrict s) +
+      (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) := by rw [h_le_s, h_le_s_compl]
+  _ = (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ := by
+      simp [restrict_sub_eq_restrict_sub_restrict hs,
+        restrict_sub_eq_restrict_sub_restrict hs.compl]
+  _ = μ + ν - ξ := by rw [restrict_add_restrict_compl hs]
+
 end Measure
 
 end MeasureTheory

Mathlib/MeasureTheory/Measure/Sub.lean

@@ -35,7 +35,7 @@ Specifically, note that if you have `α = {1,2}`, and `μ {1} = 2`, `μ {2} = 0`
 noncomputable instance instSub {α : Type*} [MeasurableSpace α] : Sub (Measure α) :=
   ⟨fun μ ν => sInf { τ | μ ≤ τ + ν }⟩
 
-variable {α : Type*} {m : MeasurableSpace α} {μ ν : Measure α} {s : Set α}
+variable {α : Type*} {m : MeasurableSpace α} {μ ν ξ : Measure α} {s : Set α}
 
 theorem sub_def : μ - ν = sInf { d | μ ≤ d + ν } := rfl
 
@@ -145,6 +145,16 @@ theorem sub_apply_eq_zero_of_restrict_le_restrict (h_le : μ.restrict s ≤ ν.r
 instance isFiniteMeasure_sub [IsFiniteMeasure μ] : IsFiniteMeasure (μ - ν) :=
   isFiniteMeasure_of_le μ sub_le
 
+/-- See `sub_le_iff_le_add` for the case where both measures are finite, which does not need the
+hypothesis `ν ≤ μ`. -/
+lemma sub_le_iff_le_add_of_le [IsFiniteMeasure ν] (h_le : ν ≤ μ) : μ - ν ≤ ξ ↔ μ ≤ ξ + ν := by
+  refine ⟨fun h ↦ ?_, Measure.sub_le_of_le_add⟩
+  rw [Measure.le_iff] at h ⊢
+  intro s hs
+  specialize h s hs
+  simp only [Measure.coe_add, Pi.add_apply]
+  rwa [Measure.sub_apply hs h_le, tsub_le_iff_right] at h
+
 end Measure
 
 end MeasureTheory

Mathlib/MeasureTheory/Measure/SubFinite.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
+public import Mathlib.MeasureTheory.Measure.Sub
+
+import Mathlib.MeasureTheory.Integral.Lebesgue.Sub
+
+/-!
+# Results about subtraction of finite measures
+
+The content of this file is not placed in `MeasureTheory.Measure.Sub` because it uses tools that are
+not imported in the other file: the Hahn decomposition of finite measures and measures built with
+`withDensity`.
+
+## Main statements
+
+* `sub_le_iff_le_add`: for `μ` and `ν` finite measures, `μ - ν ≤ ξ ↔ μ ≤ ξ + ν`. See also
+  `sub_le_iff_le_add_of_le` for the case where only `ν` is finite, with the additional hypothesis
+  `ν ≤ μ`.
+* `withDensity_sub`: If `μ.withDensity g` is finite, then
+  `μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g`.
+
+-/
+
+@[expose] public section
+
+open scoped ENNReal
+
+namespace MeasureTheory.Measure
+
+variable {α : Type*} {mα : MeasurableSpace α} {μ ν ξ : Measure α}
+
+lemma sub_le_iff_le_add [IsFiniteMeasure μ] [IsFiniteMeasure ν] : μ - ν ≤ ξ ↔ μ ≤ ξ + ν := by
+  refine ⟨fun h ↦ ?_, sub_le_of_le_add⟩
+  obtain ⟨s, hs⟩ := exists_isHahnDecomposition μ ν
+  have h_le_s : μ.restrict s ≤ ξ.restrict s + ν.restrict s :=
+    hs.le_on.trans (Measure.le_add_left le_rfl)
+  have h_le_s_compl : μ.restrict sᶜ ≤ ξ.restrict sᶜ + ν.restrict sᶜ := by
+    refine (sub_le_iff_le_add_of_le hs.ge_on_compl).mp ?_
+    rw [← restrict_sub_eq_restrict_sub_restrict hs.measurableSet.compl]
+    exact restrict_mono subset_rfl h
+  rw [← restrict_add_restrict_compl (μ := μ) hs.measurableSet,
+    ← restrict_add_restrict_compl (μ := ξ) hs.measurableSet,
+    ← restrict_add_restrict_compl (μ := ν) hs.measurableSet]
+  suffices μ.restrict s + μ.restrict sᶜ ≤
+    ξ.restrict s + ν.restrict s + (ξ.restrict sᶜ + ν.restrict sᶜ) from this.trans_eq (by abel)
+  gcongr
+
+lemma withDensity_sub_of_le {f g : α → ℝ≥0∞} [IsFiniteMeasure (μ.withDensity g)]
+    (hg : Measurable g) (hgf : g ≤ᵐ[μ] f) :
+    μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g := by
+  ext s hs
+  rw [sub_apply hs (withDensity_mono hgf), withDensity_apply _ hs, withDensity_apply _ hs,
+    withDensity_apply _ hs, ← lintegral_sub hg _ (ae_restrict_of_ae hgf)]
+  · simp
+  · simp [← withDensity_apply _ hs]
+
+lemma withDensity_sub {f g : α → ℝ≥0∞} [IsFiniteMeasure (μ.withDensity g)]
+    (hf : Measurable f) (hg : Measurable g) :
+    μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g := by
+  refine le_antisymm ?_ ?_
+  · let t := {x | f x ≤ g x}
+    have ht : MeasurableSet t := measurableSet_le hf hg
+    rw [← restrict_add_restrict_compl (μ := μ.withDensity (f - g)) ht,
+      ← restrict_add_restrict_compl (μ := μ.withDensity f - μ.withDensity g) ht]
+    have h_zero : (μ.withDensity (f - g)).restrict t = 0 := by
+      simp only [restrict_eq_zero]
+      rw [withDensity_apply _ ht, lintegral_eq_zero_iff (by fun_prop)]
+      refine ae_restrict_of_forall_mem ht fun x hx ↦ ?_
+      simpa [tsub_eq_zero_iff_le]
+    rw [h_zero, zero_add]
+    suffices (μ.withDensity (f - g)).restrict tᶜ ≤
+      (μ.withDensity f - μ.withDensity g).restrict tᶜ from this.trans (Measure.le_add_left le_rfl)
+    rw [restrict_sub_eq_restrict_sub_restrict ht.compl]
+    simp_rw [restrict_withDensity ht.compl]
+    have : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g) := by
+      rw [← restrict_withDensity ht.compl]
+      infer_instance
+    rw [withDensity_sub_of_le hg]
+    refine ae_restrict_of_forall_mem ht.compl fun x hx ↦ ?_
+    simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le, t] at hx
+    exact hx.le
+  · refine sub_le_of_le_add ?_
+    rw [← withDensity_add_right _ hg]
+    exact withDensity_mono (ae_of_all _ fun x ↦ le_tsub_add)
+
+end MeasureTheory.Measure