From b2c7702b6e9901d28bf974eeaa40f82af5bfd5b4 Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Wed, 20 May 2026 15:59:10 +0200
Subject: [PATCH 01/12] cherry pick

---
 .../MeasureTheory/VectorMeasure/Basic.lean    |  45 +++++-
 .../VectorMeasure/Variation/Basic.lean        | 131 +++++++++++++++++-
 2 files changed, 164 insertions(+), 12 deletions(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
index e45965e0dbc9f6..b6e7f34f44d294 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
@@ -123,6 +123,14 @@ theorem ext_iff (v w : VectorMeasure α M) : v = w ↔ ∀ i : Set α, Measurabl
 theorem ext {s t : VectorMeasure α M} (h : ∀ i : Set α, MeasurableSet i → s i = t i) : s = t :=
   (ext_iff s t).2 h
 
+@[nontriviality]
+lemma apply_eq_zero_of_isEmpty [IsEmpty α] (v : VectorMeasure α M) (s : Set α) :
+    v s = 0 := by
+  rw [eq_empty_of_isEmpty s, empty]
+
+instance instSubsingleton [IsEmpty α] : Subsingleton (VectorMeasure α M) :=
+  ⟨fun μ ν => by ext1 s _; rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]⟩
+
 variable [Countable β] {v : VectorMeasure α M} {f : β → Set α}
 
 theorem hasSum_of_disjoint_iUnion (hm : ∀ i, MeasurableSet (f i)) (hd : Pairwise (Disjoint on f)) :
@@ -287,6 +295,9 @@ theorem coe_zero : ⇑(0 : VectorMeasure α M) = 0 := rfl
 
 theorem zero_apply (i : Set α) : (0 : VectorMeasure α M) i = 0 := rfl
 
+theorem eq_zero_of_isEmpty [IsEmpty α] (v : VectorMeasure α M) : v = 0 :=
+  Subsingleton.elim v 0
+
 variable [ContinuousAdd M]
 
 /-- The sum of two vector measure is a vector measure. -/
@@ -408,6 +419,10 @@ def dirac (x : β) (v : M) : VectorMeasure β M where
 @[simp] lemma dirac_apply_of_notMem (hx : x ∉ s) : dirac x v s = 0 := by
   simp [dirac, hx]
 
+@[simp] lemma dirac_zero : dirac x (0 : M) = 0 := by
+  ext s hs
+  simp [dirac]
+
 end Dirac
 
 end VectorMeasure
@@ -631,17 +646,21 @@ end ContinuousAdd
 section Module
 
 variable {R : Type*} [Semiring R] [Module R M] [Module R N]
-variable [ContinuousAdd M] [ContinuousAdd N] [ContinuousConstSMul R M] [ContinuousConstSMul R N]
+
+variable [ContinuousConstSMul R M] [ContinuousConstSMul R N]
+
+theorem mapRange_smul {v : VectorMeasure α M} {f : M →ₗ[R] N} (hf : Continuous f) {c : R} :
+    (c • v).mapRange f.toAddMonoidHom hf = c • (v.mapRange f.toAddMonoidHom hf) := by
+  ext; simp
+
+variable [ContinuousAdd M] [ContinuousAdd N]
 
 /-- Given a continuous linear map `f : M → N`, `mapRangeₗ` is the linear map mapping the
 vector measure `v` on `M` to the vector measure `f ∘ v` on `N`. -/
 def mapRangeₗ (f : M →ₗ[R] N) (hf : Continuous f) : VectorMeasure α M →ₗ[R] VectorMeasure α N where
   toFun v := v.mapRange f.toAddMonoidHom hf
   map_add' _ _ := mapRange_add hf
-  map_smul' := by
-    intros
-    ext
-    simp
+  map_smul' _ _ := mapRange_smul hf
 
 end Module
 
@@ -649,7 +668,7 @@ end
 
 open Classical in
 /-- The restriction of a vector measure on some set. -/
-def restrict (v : VectorMeasure α M) (i : Set α) : VectorMeasure α M :=
+@[no_expose] def restrict (v : VectorMeasure α M) (i : Set α) : VectorMeasure α M :=
   if hi : MeasurableSet i then
     { measureOf' := fun s => if MeasurableSet s then v (s ∩ i) else 0
       empty' := by simp
@@ -690,6 +709,20 @@ theorem restrict_zero {i : Set α} : (0 : VectorMeasure α M).restrict i = 0 :=
     rw [restrict_apply 0 hi hj, zero_apply, zero_apply]
   · exact dif_neg hi
 
+theorem restrict_dirac {s : Set α} {x : α} {m : M} (hs : MeasurableSet s) [Decidable (x ∈ s)] :
+    (VectorMeasure.dirac x m).restrict s = if x ∈ s then VectorMeasure.dirac x m else 0 := by
+  classical
+  ext t ht
+  simp only [hs, ht, restrict_apply]
+  split_ifs with has <;> simp [dirac, ht, ht.inter hs, has]
+
+@[simp]
+theorem restrict_singleton {a : α} : v.restrict {a} = VectorMeasure.dirac a (v {a}) := by
+  by_cases h : MeasurableSet {a}
+  · ext1 s hs
+    by_cases ha : a ∈ s <;> simp [*, restrict_apply]
+  · simp [restrict, h]
+
 section ContinuousAdd
 
 variable [ContinuousAdd M]
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
index 3722e32704c756..3a2b5e5063a48c 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
@@ -5,6 +5,8 @@ Authors: Oliver Butterley, Yoh Tanimoto
 -/
 module
 
+public import Mathlib.Analysis.Normed.Module.Basic
+public import Mathlib.MeasureTheory.Measure.Dirac
 public import Mathlib.MeasureTheory.VectorMeasure.Variation.Defs
 
 /-!
@@ -30,7 +32,7 @@ such vector-valued measures.
 
 public section
 
-open Finset
+open Finset Set
 open scoped ENNReal
 
 namespace MeasureTheory.VectorMeasure
@@ -41,7 +43,6 @@ section Basic
 
 variable [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] {μ ν : VectorMeasure X V}
 
-@[simp]
 lemma variation_apply (μ : VectorMeasure X V) (s : Set X) :
     μ.variation s = preVariation (‖μ ·‖ₑ) (isSigmaSubadditiveSetFun_enorm μ) (by simp) s := rfl
 
@@ -96,14 +97,15 @@ lemma absolutelyContinuous (μ : VectorMeasure X V) : μ ≪ᵥ μ.ennrealVariat
     grw [enorm_measure_le_variation, ← ennrealVariation_apply _ hsm, hs]
   · exact μ.not_measurable' hsm
 
-lemma variation_le_of_forall_enorm_le {m : Measure X} (h : ∀ E, MeasurableSet E → ‖μ E‖ₑ ≤ m E) :
-    μ.variation ≤ m := by
-  refine Measure.le_intro fun s hs _ => ?_
+lemma variation_apply_le_of_forall_enorm_le {m : Measure X} {s : Set X} (hs : MeasurableSet s)
+    (h : ∀ E, MeasurableSet E → E ⊆ s → ‖μ E‖ₑ ≤ m E) :
+    μ.variation s ≤ m s := by
   simp only [variation_apply, preVariation, ennrealToMeasure_apply hs, ennrealPreVariation_apply,
     preVariationFun, hs, dite_true, iSup_le_iff]
   intro i
   calc
-    ∑ x ∈ i.parts, ‖μ x‖ₑ ≤ ∑ x ∈ i.parts, m x := Finset.sum_le_sum (fun s hs => h s s.property)
+    ∑ x ∈ i.parts, ‖μ x‖ₑ ≤ ∑ x ∈ i.parts, m x := Finset.sum_le_sum
+        (fun s hs => h s s.property (i.le hs))
     _ = m (i.parts.sup Subtype.val) := by
       rw [sup_set_eq_biUnion]
       refine (MeasureTheory.measure_biUnion_finset ?_ fun b _ => b.property).symm
@@ -113,6 +115,10 @@ lemma variation_le_of_forall_enorm_le {m : Measure X} (h : ∀ E, MeasurableSet
       rw [sup_set_eq_biUnion]
       exact measure_mono <| Set.iUnion₂_subset fun _ hp => Subtype.coe_le_coe.mpr (i.le hp)
 
+lemma variation_le_of_forall_enorm_le {m : Measure X} (h : ∀ E, MeasurableSet E → ‖μ E‖ₑ ≤ m E) :
+    μ.variation ≤ m :=
+  Measure.le_intro fun _ hs _ => variation_apply_le_of_forall_enorm_le hs (fun E hE _ ↦ h E hE)
+
 lemma variation_add_le [ContinuousAdd V] : variation (μ + ν) ≤ variation μ + variation ν := by
   refine variation_le_of_forall_enorm_le fun E _ => ?_
   calc
@@ -129,6 +135,91 @@ lemma variation_finsetSum_le [ContinuousAdd V] {ι} (s : Finset ι) (μ : ι →
     simpa [Finset.sum_insert his] using
       variation_add_le.trans (add_le_add_right ih ((μ i).variation))
 
+lemma variation_apply_eq_zero {μ : VectorMeasure X V} {s : Set X} (hs : MeasurableSet s) :
+    μ.variation s = 0 ↔ ∀ t, t ⊆ s → MeasurableSet t → μ t = 0 := by
+  refine ⟨fun h t hts ht ↦ ?_, fun h ↦ ?_⟩
+  · apply enorm_eq_zero.1
+    apply le_antisymm ?_ zero_le
+    rw [← h]
+    apply (enorm_measure_le_variation _ _).trans (measure_mono hts)
+  · apply le_antisymm ?_ zero_le
+    change μ.variation s ≤ (0 : Measure X) s
+    apply variation_apply_le_of_forall_enorm_le hs (fun t ht hts ↦ ?_)
+    simp [h t hts ht]
+
+@[simp] lemma variation_eq_zero {μ : VectorMeasure X V} :
+    μ.variation = 0 ↔ μ = 0 := by
+  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
+  ext s hs
+  apply enorm_eq_zero.1
+  apply le_antisymm ?_ (by simp)
+  grw [enorm_measure_le_variation]
+  simp [h]
+
+lemma variation_restrict (μ : VectorMeasure X V) {s : Set X} (hs : MeasurableSet s) :
+    (μ.restrict s).variation = μ.variation.restrict s := by
+  apply le_antisymm
+  · apply variation_le_of_forall_enorm_le (fun t ht ↦ ?_)
+    simp only [ht, Measure.restrict_apply, VectorMeasure.restrict_apply, hs]
+    apply enorm_measure_le_variation
+  · apply Measure.le_iff.2 (fun t ht ↦ ?_)
+    simp only [ht, Measure.restrict_apply]
+    calc μ.variation (t ∩ s)
+    _ ≤ (μ.restrict s).variation (t ∩ s) := by
+      apply variation_apply_le_of_forall_enorm_le (ht.inter hs) (fun u u_meas hu ↦ ?_)
+      have : μ u = μ.restrict s u := by
+        rw [VectorMeasure.restrict_apply _ hs u_meas]
+        congr
+        grind
+      rw [this]
+      apply enorm_measure_le_variation
+    _ ≤ (μ.restrict s).variation t := by
+      gcongr
+      exact Set.inter_subset_left
+
+lemma variation_restrict_le (μ : VectorMeasure X V) (s : Set X) :
+    (μ.restrict s).variation ≤ μ.variation.restrict s := by
+  by_cases hs : MeasurableSet s
+  · simp [variation_restrict μ hs]
+  · simp only [restrict_not_measurable _ hs, variation_zero, Measure.zero_le]
+
+lemma variation_map_le {Y : Type*} [MeasurableSpace Y] {φ : X → Y} :
+   (μ.map φ).variation ≤ Measure.map φ μ.variation := by
+  by_cases hφ : Measurable φ; swap
+  · simp [VectorMeasure.map, hφ, Measure.zero_le]
+  apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)
+  simp only [Measure.map_apply hφ hs]
+  apply le_trans ?_ (enorm_measure_le_variation _ _)
+  simp [VectorMeasure.map_apply _ hφ hs]
+
+theorem _root_.MeasurableEmbedding.variation_map {Y : Type*} [MeasurableSpace Y] {φ : X → Y}
+    (hφ : MeasurableEmbedding φ) :
+    (μ.map φ).variation = μ.variation.map φ := by
+  apply le_antisymm variation_map_le ?_
+  apply Measure.le_iff.2 (fun s hs ↦ ?_)
+  simp only [hφ.measurable, hs, Measure.map_apply]
+  have : (μ.map φ).variation s = (μ.map φ).variation (s ∩ range φ) := by
+    nth_rw 1 [← inter_union_diff s (range φ)]
+    have : (μ.map φ).variation (s \ range φ) = 0 := by
+      apply (variation_apply_eq_zero (hs.diff hφ.measurableSet_range)).2 (fun t ht t_meas ↦ ?_)
+      have : φ ⁻¹' t = ∅ := by grind
+      simp [map_apply, t_meas, hφ.measurable, this]
+    rw [measure_union (by grind) (hs.diff hφ.measurableSet_range), this, add_zero]
+  rw [this, ← hφ.comap_preimage]
+  apply variation_le_of_forall_enorm_le (fun t ht ↦ ?_)
+  simp only [hφ.comap_apply]
+  apply le_trans ?_ (enorm_measure_le_variation _ _)
+  rw [map_apply _ hφ.measurable (hφ.measurableSet_image.2 ht), preimage_image_eq _ hφ.injective]
+
+@[simp] lemma variation_dirac (x : X) (v : V) :
+    (VectorMeasure.dirac x v).variation = ‖v‖ₑ • Measure.dirac x := by
+  apply le_antisymm
+  · apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)
+    by_cases hx : x ∈ s <;> simp [hs, hx]
+  · apply Measure.le_iff.2 (fun s hs ↦ ?_)
+    apply le_trans ?_ (enorm_measure_le_variation _ _)
+    by_cases hx : x ∈ s <;> simp [hs, hx]
+
 end Basic
 
 section NormedAddCommGroup
@@ -147,6 +238,34 @@ lemma variation_neg : (-μ).variation = μ.variation := by simp [variation]
 lemma variation_sub_le : (μ - ν).variation ≤ μ.variation + ν.variation := by
   grw [sub_eq_add_neg, variation_add_le, variation_neg]
 
+private lemma variation_smul_le {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 V] {c : 𝕜} :
+    (c • μ).variation ≤ ‖c‖₊ • μ.variation := by
+  apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)
+  simp only [coe_smul, Pi.smul_apply, enorm_smul, Measure.smul_apply, Measure.nnreal_smul_coe_apply]
+  grw [enorm_measure_le_variation]
+  exact le_rfl
+
+lemma variation_smul {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 V] {c : 𝕜} :
+    (c • μ).variation = ‖c‖₊ • μ.variation := by
+  apply le_antisymm variation_smul_le ?_
+  rcases eq_or_ne c 0 with rfl | hc
+  · simp
+  calc ‖c‖₊ • μ.variation
+  _ = ‖c‖₊ • (c⁻¹ • (c • μ)).variation := by simp [smul_smul, inv_mul_cancel₀ hc]
+  _ ≤ ‖c‖₊ • ‖c⁻¹‖₊ • (c • μ).variation := by
+    gcongr
+    exact variation_smul_le
+  _ = (c • μ).variation := by
+    simp [smul_smul, mul_inv_cancel₀ (nnnorm_ne_zero_iff.mpr hc)]
+
+instance [Finite X] : IsFiniteMeasure μ.variation := by
+  classical
+  let : Fintype X := Fintype.ofFinite X
+  constructor
+  simp only [variation_apply, preVariation_apply, MeasurableSet.univ, ennrealToMeasure_apply,
+    ennrealPreVariation_apply, preVariationFun, ↓reduceDIte, ← sup_univ_eq_ciSup]
+  exact (Finset.sup_lt_iff (by simp)).2 (fun b hb ↦ by simp [ENNReal.sum_lt_top, enorm_lt_top])
+
 end NormedAddCommGroup
 
 end MeasureTheory.VectorMeasure

From b975b6d444f34320b9d393dcc2c32d140b55145d Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Wed, 20 May 2026 16:08:39 +0200
Subject: [PATCH 02/12] missing bits

---
 Mathlib/Data/ENNReal/Action.lean                |  6 ++++++
 Mathlib/MeasureTheory/Measure/MeasureSpace.lean |  9 +++++++++
 .../VectorMeasure/Variation/Basic.lean          | 17 +++++++++--------
 3 files changed, 24 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Data/ENNReal/Action.lean b/Mathlib/Data/ENNReal/Action.lean
index d6ba39d13c1c4c..431d6397d5b04d 100644
--- a/Mathlib/Data/ENNReal/Action.lean
+++ b/Mathlib/Data/ENNReal/Action.lean
@@ -104,6 +104,12 @@ instance : PosSMulStrictMono ℝ≥0 ℝ≥0∞ where
 instance : SMulPosMono ℝ≥0 ℝ≥0∞ where
   smul_le_smul_of_nonneg_right _r _ _a _b hab := _root_.mul_le_mul_left (coe_le_coe.2 hab) _
 
+instance : CovariantClass ℝ≥0∞ ℝ≥0∞ (· • ·) (· ≤ ·) :=
+  inferInstanceAs <| CovariantClass ℝ≥0∞ ℝ≥0∞ (· * ·) (· ≤ ·)
+
+instance : CovariantClass ℝ≥0 ℝ≥0∞ (· • ·) (· ≤ ·) :=
+  ⟨fun x x y hxy ↦ by simpa [ENNReal.smul_def] using mul_le_mul_right hxy _⟩
+
 end Actions
 
 end ENNReal
diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index dfdbb0f4299ba0..c15b18d4e60997 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -1079,6 +1079,13 @@ protected theorem le_add_left (h : μ ≤ ν) : μ ≤ ν' + ν := fun s => le_a
 
 protected theorem le_add_right (h : μ ≤ ν) : μ ≤ ν + ν' := fun s => le_add_right (h s)
 
+instance [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] [CovariantClass R ℝ≥0∞ (· • ·) (· ≤ ·)] :
+    CovariantClass R (Measure α) (· • ·) (· ≤ ·) := by
+  constructor
+  intro c μ ν hμν s
+  simp only [smul_apply]
+  gcongr
+
 section sInf
 
 variable {m : Set (Measure α)}
@@ -1494,3 +1501,5 @@ end
 end MeasureTheory
 
 end
+
+set_option linter.style.longFile 1700
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
index 3a2b5e5063a48c..64101ada399576 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
@@ -41,7 +41,8 @@ variable {X V : Type*} {mX : MeasurableSpace X}
 
 section Basic
 
-variable [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] {μ ν : VectorMeasure X V}
+variable [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V]
+  {μ ν : VectorMeasure X V} {s : Set X}
 
 lemma variation_apply (μ : VectorMeasure X V) (s : Set X) :
     μ.variation s = preVariation (‖μ ·‖ₑ) (isSigmaSubadditiveSetFun_enorm μ) (by simp) s := rfl
@@ -135,7 +136,7 @@ lemma variation_finsetSum_le [ContinuousAdd V] {ι} (s : Finset ι) (μ : ι →
     simpa [Finset.sum_insert his] using
       variation_add_le.trans (add_le_add_right ih ((μ i).variation))
 
-lemma variation_apply_eq_zero {μ : VectorMeasure X V} {s : Set X} (hs : MeasurableSet s) :
+lemma variation_apply_eq_zero (hs : MeasurableSet s) :
     μ.variation s = 0 ↔ ∀ t, t ⊆ s → MeasurableSet t → μ t = 0 := by
   refine ⟨fun h t hts ht ↦ ?_, fun h ↦ ?_⟩
   · apply enorm_eq_zero.1
@@ -147,7 +148,7 @@ lemma variation_apply_eq_zero {μ : VectorMeasure X V} {s : Set X} (hs : Measura
     apply variation_apply_le_of_forall_enorm_le hs (fun t ht hts ↦ ?_)
     simp [h t hts ht]
 
-@[simp] lemma variation_eq_zero {μ : VectorMeasure X V} :
+@[simp] lemma variation_eq_zero :
     μ.variation = 0 ↔ μ = 0 := by
   refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
   ext s hs
@@ -156,7 +157,7 @@ lemma variation_apply_eq_zero {μ : VectorMeasure X V} {s : Set X} (hs : Measura
   grw [enorm_measure_le_variation]
   simp [h]
 
-lemma variation_restrict (μ : VectorMeasure X V) {s : Set X} (hs : MeasurableSet s) :
+lemma variation_restrict (hs : MeasurableSet s) :
     (μ.restrict s).variation = μ.variation.restrict s := by
   apply le_antisymm
   · apply variation_le_of_forall_enorm_le (fun t ht ↦ ?_)
@@ -177,14 +178,14 @@ lemma variation_restrict (μ : VectorMeasure X V) {s : Set X} (hs : MeasurableSe
       gcongr
       exact Set.inter_subset_left
 
-lemma variation_restrict_le (μ : VectorMeasure X V) (s : Set X) :
+lemma variation_restrict_le :
     (μ.restrict s).variation ≤ μ.variation.restrict s := by
   by_cases hs : MeasurableSet s
-  · simp [variation_restrict μ hs]
+  · simp [variation_restrict hs]
   · simp only [restrict_not_measurable _ hs, variation_zero, Measure.zero_le]
 
 lemma variation_map_le {Y : Type*} [MeasurableSpace Y] {φ : X → Y} :
-   (μ.map φ).variation ≤ Measure.map φ μ.variation := by
+    (μ.map φ).variation ≤ Measure.map φ μ.variation := by
   by_cases hφ : Measurable φ; swap
   · simp [VectorMeasure.map, hφ, Measure.zero_le]
   apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)
@@ -211,7 +212,7 @@ theorem _root_.MeasurableEmbedding.variation_map {Y : Type*} [MeasurableSpace Y]
   apply le_trans ?_ (enorm_measure_le_variation _ _)
   rw [map_apply _ hφ.measurable (hφ.measurableSet_image.2 ht), preimage_image_eq _ hφ.injective]
 
-@[simp] lemma variation_dirac (x : X) (v : V) :
+@[simp] lemma variation_dirac {x : X} {v : V} :
     (VectorMeasure.dirac x v).variation = ‖v‖ₑ • Measure.dirac x := by
   apply le_antisymm
   · apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)

From 2ae7fd6a36067c15b9e0a2b88999ebbb85232250 Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Thu, 21 May 2026 11:49:59 +0200
Subject: [PATCH 03/12] more

---
 .../MeasureTheory/VectorMeasure/Basic.lean    | 19 ++++++++++
 .../VectorMeasure/Variation/Basic.lean        | 37 ++++++++++++++-----
 2 files changed, 47 insertions(+), 9 deletions(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
index b6e7f34f44d294..56e93b0eec11cc 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
@@ -755,6 +755,25 @@ def restrictGm (i : Set α) : VectorMeasure α M →+ VectorMeasure α M where
   map_zero' := restrict_zero
   map_add' _ _ := restrict_add _ _ i
 
+variable [T2Space M] {s t : Set α}
+
+theorem restrict_inter_add_diff (hs : MeasurableSet s) (ht : MeasurableSet t) :
+    v.restrict (s ∩ t) + v.restrict (s \ t) = v.restrict s := by
+  ext1 u hu
+  simp only [add_apply, restrict_apply, hs, hu, hs.inter ht, hs.diff ht]
+  rw [← of_union (by grind) (hu.inter (hs.inter ht)) (hu.inter (hs.diff ht))]
+  congr
+  grind
+
+theorem restrict_union_add_inter (hs : MeasurableSet s) (ht : MeasurableSet t) :
+    v.restrict (s ∪ t) + v.restrict (s ∩ t) = v.restrict s + v.restrict t := by
+  rw [← v.restrict_inter_add_diff (hs.union ht) ht, union_inter_cancel_right, union_diff_right,
+    ← v.restrict_inter_add_diff hs ht, add_comm, ← add_assoc, add_right_comm]
+
+theorem restrict_union (h : Disjoint s t) (hs : MeasurableSet s) (ht : MeasurableSet t) :
+    v.restrict (s ∪ t) = v.restrict s + v.restrict t := by
+  simp [← v.restrict_union_add_inter hs ht, disjoint_iff_inter_eq_empty.mp h]
+
 end ContinuousAdd
 
 section Partition
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
index 64101ada399576..c990b5c514269a 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
@@ -41,8 +41,7 @@ variable {X V : Type*} {mX : MeasurableSpace X}
 
 section Basic
 
-variable [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V]
-  {μ ν : VectorMeasure X V} {s : Set X}
+variable [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] {μ ν : VectorMeasure X V}
 
 lemma variation_apply (μ : VectorMeasure X V) (s : Set X) :
     μ.variation s = preVariation (‖μ ·‖ₑ) (isSigmaSubadditiveSetFun_enorm μ) (by simp) s := rfl
@@ -136,7 +135,7 @@ lemma variation_finsetSum_le [ContinuousAdd V] {ι} (s : Finset ι) (μ : ι →
     simpa [Finset.sum_insert his] using
       variation_add_le.trans (add_le_add_right ih ((μ i).variation))
 
-lemma variation_apply_eq_zero (hs : MeasurableSet s) :
+lemma variation_apply_eq_zero {μ : VectorMeasure X V} {s : Set X} (hs : MeasurableSet s) :
     μ.variation s = 0 ↔ ∀ t, t ⊆ s → MeasurableSet t → μ t = 0 := by
   refine ⟨fun h t hts ht ↦ ?_, fun h ↦ ?_⟩
   · apply enorm_eq_zero.1
@@ -148,7 +147,7 @@ lemma variation_apply_eq_zero (hs : MeasurableSet s) :
     apply variation_apply_le_of_forall_enorm_le hs (fun t ht hts ↦ ?_)
     simp [h t hts ht]
 
-@[simp] lemma variation_eq_zero :
+@[simp] lemma variation_eq_zero {μ : VectorMeasure X V} :
     μ.variation = 0 ↔ μ = 0 := by
   refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
   ext s hs
@@ -157,7 +156,7 @@ lemma variation_apply_eq_zero (hs : MeasurableSet s) :
   grw [enorm_measure_le_variation]
   simp [h]
 
-lemma variation_restrict (hs : MeasurableSet s) :
+lemma variation_restrict (μ : VectorMeasure X V) {s : Set X} (hs : MeasurableSet s) :
     (μ.restrict s).variation = μ.variation.restrict s := by
   apply le_antisymm
   · apply variation_le_of_forall_enorm_le (fun t ht ↦ ?_)
@@ -178,14 +177,19 @@ lemma variation_restrict (hs : MeasurableSet s) :
       gcongr
       exact Set.inter_subset_left
 
-lemma variation_restrict_le :
+lemma variation_restrict_le (μ : VectorMeasure X V) (s : Set X) :
     (μ.restrict s).variation ≤ μ.variation.restrict s := by
   by_cases hs : MeasurableSet s
-  · simp [variation_restrict hs]
+  · simp [variation_restrict μ hs]
   · simp only [restrict_not_measurable _ hs, variation_zero, Measure.zero_le]
 
+instance {s : Set X} [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.restrict s).variation := by
+  constructor
+  grw [variation_restrict_le]
+  exact IsFiniteMeasure.measure_univ_lt_top
+
 lemma variation_map_le {Y : Type*} [MeasurableSpace Y] {φ : X → Y} :
-    (μ.map φ).variation ≤ Measure.map φ μ.variation := by
+   (μ.map φ).variation ≤ Measure.map φ μ.variation := by
   by_cases hφ : Measurable φ; swap
   · simp [VectorMeasure.map, hφ, Measure.zero_le]
   apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)
@@ -193,6 +197,12 @@ lemma variation_map_le {Y : Type*} [MeasurableSpace Y] {φ : X → Y} :
   apply le_trans ?_ (enorm_measure_le_variation _ _)
   simp [VectorMeasure.map_apply _ hφ hs]
 
+instance {Y : Type*} [MeasurableSpace Y] {φ : X → Y} [IsFiniteMeasure μ.variation] :
+    IsFiniteMeasure (μ.map φ).variation := by
+  constructor
+  grw [variation_map_le]
+  exact IsFiniteMeasure.measure_univ_lt_top
+
 theorem _root_.MeasurableEmbedding.variation_map {Y : Type*} [MeasurableSpace Y] {φ : X → Y}
     (hφ : MeasurableEmbedding φ) :
     (μ.map φ).variation = μ.variation.map φ := by
@@ -212,7 +222,7 @@ theorem _root_.MeasurableEmbedding.variation_map {Y : Type*} [MeasurableSpace Y]
   apply le_trans ?_ (enorm_measure_le_variation _ _)
   rw [map_apply _ hφ.measurable (hφ.measurableSet_image.2 ht), preimage_image_eq _ hφ.injective]
 
-@[simp] lemma variation_dirac {x : X} {v : V} :
+@[simp] lemma variation_dirac (x : X) (v : V) :
     (VectorMeasure.dirac x v).variation = ‖v‖ₑ • Measure.dirac x := by
   apply le_antisymm
   · apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)
@@ -259,6 +269,11 @@ lemma variation_smul {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 V] {c :
   _ = (c • μ).variation := by
     simp [smul_smul, mul_inv_cancel₀ (nnnorm_ne_zero_iff.mpr hc)]
 
+instance {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 V] {c : 𝕜} [IsFiniteMeasure μ.variation] :
+    IsFiniteMeasure (c • μ).variation := by
+  simp only [variation_smul]
+  infer_instance
+
 instance [Finite X] : IsFiniteMeasure μ.variation := by
   classical
   let : Fintype X := Fintype.ofFinite X
@@ -267,6 +282,10 @@ instance [Finite X] : IsFiniteMeasure μ.variation := by
     ennrealPreVariation_apply, preVariationFun, ↓reduceDIte, ← sup_univ_eq_ciSup]
   exact (Finset.sup_lt_iff (by simp)).2 (fun b hb ↦ by simp [ENNReal.sum_lt_top, enorm_lt_top])
 
+instance {x : X} {v : V} : IsFiniteMeasure (VectorMeasure.dirac x v).variation := by
+  simp only [variation_dirac, enorm_eq_nnnorm, Measure.coe_nnreal_smul]
+  infer_instance
+
 end NormedAddCommGroup
 
 end MeasureTheory.VectorMeasure

From c8374b46d77a88c5933ee2da03895953ee5325e6 Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Thu, 21 May 2026 11:54:32 +0200
Subject: [PATCH 04/12] oops

---
 .../VectorMeasure/Variation/Basic.lean        | 27 ++++++++++---------
 1 file changed, 14 insertions(+), 13 deletions(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
index c990b5c514269a..97250bbb32c832 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
@@ -41,7 +41,8 @@ variable {X V : Type*} {mX : MeasurableSpace X}
 
 section Basic
 
-variable [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] {μ ν : VectorMeasure X V}
+variable [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V]
+  {μ ν : VectorMeasure X V} {s : Set X}
 
 lemma variation_apply (μ : VectorMeasure X V) (s : Set X) :
     μ.variation s = preVariation (‖μ ·‖ₑ) (isSigmaSubadditiveSetFun_enorm μ) (by simp) s := rfl
@@ -135,7 +136,7 @@ lemma variation_finsetSum_le [ContinuousAdd V] {ι} (s : Finset ι) (μ : ι →
     simpa [Finset.sum_insert his] using
       variation_add_le.trans (add_le_add_right ih ((μ i).variation))
 
-lemma variation_apply_eq_zero {μ : VectorMeasure X V} {s : Set X} (hs : MeasurableSet s) :
+lemma variation_apply_eq_zero (hs : MeasurableSet s) :
     μ.variation s = 0 ↔ ∀ t, t ⊆ s → MeasurableSet t → μ t = 0 := by
   refine ⟨fun h t hts ht ↦ ?_, fun h ↦ ?_⟩
   · apply enorm_eq_zero.1
@@ -147,7 +148,7 @@ lemma variation_apply_eq_zero {μ : VectorMeasure X V} {s : Set X} (hs : Measura
     apply variation_apply_le_of_forall_enorm_le hs (fun t ht hts ↦ ?_)
     simp [h t hts ht]
 
-@[simp] lemma variation_eq_zero {μ : VectorMeasure X V} :
+@[simp] lemma variation_eq_zero :
     μ.variation = 0 ↔ μ = 0 := by
   refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
   ext s hs
@@ -156,7 +157,7 @@ lemma variation_apply_eq_zero {μ : VectorMeasure X V} {s : Set X} (hs : Measura
   grw [enorm_measure_le_variation]
   simp [h]
 
-lemma variation_restrict (μ : VectorMeasure X V) {s : Set X} (hs : MeasurableSet s) :
+lemma variation_restrict (hs : MeasurableSet s) :
     (μ.restrict s).variation = μ.variation.restrict s := by
   apply le_antisymm
   · apply variation_le_of_forall_enorm_le (fun t ht ↦ ?_)
@@ -177,19 +178,21 @@ lemma variation_restrict (μ : VectorMeasure X V) {s : Set X} (hs : MeasurableSe
       gcongr
       exact Set.inter_subset_left
 
-lemma variation_restrict_le (μ : VectorMeasure X V) (s : Set X) :
+lemma variation_restrict_le :
     (μ.restrict s).variation ≤ μ.variation.restrict s := by
   by_cases hs : MeasurableSet s
   · simp [variation_restrict μ hs]
   · simp only [restrict_not_measurable _ hs, variation_zero, Measure.zero_le]
 
-instance {s : Set X} [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.restrict s).variation := by
+instance [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.restrict s).variation := by
   constructor
   grw [variation_restrict_le]
   exact IsFiniteMeasure.measure_univ_lt_top
 
-lemma variation_map_le {Y : Type*} [MeasurableSpace Y] {φ : X → Y} :
-   (μ.map φ).variation ≤ Measure.map φ μ.variation := by
+variable {Y : Type*} [MeasurableSpace Y] {φ : X → Y}
+
+lemma variation_map_le :
+    (μ.map φ).variation ≤ Measure.map φ μ.variation := by
   by_cases hφ : Measurable φ; swap
   · simp [VectorMeasure.map, hφ, Measure.zero_le]
   apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)
@@ -197,14 +200,12 @@ lemma variation_map_le {Y : Type*} [MeasurableSpace Y] {φ : X → Y} :
   apply le_trans ?_ (enorm_measure_le_variation _ _)
   simp [VectorMeasure.map_apply _ hφ hs]
 
-instance {Y : Type*} [MeasurableSpace Y] {φ : X → Y} [IsFiniteMeasure μ.variation] :
-    IsFiniteMeasure (μ.map φ).variation := by
+instance [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.map φ).variation := by
   constructor
   grw [variation_map_le]
   exact IsFiniteMeasure.measure_univ_lt_top
 
-theorem _root_.MeasurableEmbedding.variation_map {Y : Type*} [MeasurableSpace Y] {φ : X → Y}
-    (hφ : MeasurableEmbedding φ) :
+theorem _root_.MeasurableEmbedding.variation_map (hφ : MeasurableEmbedding φ) :
     (μ.map φ).variation = μ.variation.map φ := by
   apply le_antisymm variation_map_le ?_
   apply Measure.le_iff.2 (fun s hs ↦ ?_)
@@ -222,7 +223,7 @@ theorem _root_.MeasurableEmbedding.variation_map {Y : Type*} [MeasurableSpace Y]
   apply le_trans ?_ (enorm_measure_le_variation _ _)
   rw [map_apply _ hφ.measurable (hφ.measurableSet_image.2 ht), preimage_image_eq _ hφ.injective]
 
-@[simp] lemma variation_dirac (x : X) (v : V) :
+@[simp] lemma variation_dirac {x : X} {v : V} :
     (VectorMeasure.dirac x v).variation = ‖v‖ₑ • Measure.dirac x := by
   apply le_antisymm
   · apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)

From ffaf4b9bde728b73793cc3133063086b62d47a59 Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Thu, 21 May 2026 13:12:18 +0200
Subject: [PATCH 05/12] fix

---
 .../MeasureTheory/VectorMeasure/Variation/Basic.lean   | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
index 97250bbb32c832..2c26456642017a 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
@@ -98,7 +98,7 @@ lemma absolutelyContinuous (μ : VectorMeasure X V) : μ ≪ᵥ μ.ennrealVariat
     grw [enorm_measure_le_variation, ← ennrealVariation_apply _ hsm, hs]
   · exact μ.not_measurable' hsm
 
-lemma variation_apply_le_of_forall_enorm_le {m : Measure X} {s : Set X} (hs : MeasurableSet s)
+lemma variation_apply_le_of_forall_enorm_le {m : Measure X} (hs : MeasurableSet s)
     (h : ∀ E, MeasurableSet E → E ⊆ s → ‖μ E‖ₑ ≤ m E) :
     μ.variation s ≤ m s := by
   simp only [variation_apply, preVariation, ennrealToMeasure_apply hs, ennrealPreVariation_apply,
@@ -178,10 +178,9 @@ lemma variation_restrict (hs : MeasurableSet s) :
       gcongr
       exact Set.inter_subset_left
 
-lemma variation_restrict_le :
-    (μ.restrict s).variation ≤ μ.variation.restrict s := by
+lemma variation_restrict_le : (μ.restrict s).variation ≤ μ.variation.restrict s := by
   by_cases hs : MeasurableSet s
-  · simp [variation_restrict μ hs]
+  · simp [variation_restrict hs]
   · simp only [restrict_not_measurable _ hs, variation_zero, Measure.zero_le]
 
 instance [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.restrict s).variation := by
@@ -191,8 +190,7 @@ instance [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.restrict s).variat
 
 variable {Y : Type*} [MeasurableSpace Y] {φ : X → Y}
 
-lemma variation_map_le :
-    (μ.map φ).variation ≤ Measure.map φ μ.variation := by
+lemma variation_map_le : (μ.map φ).variation ≤ Measure.map φ μ.variation := by
   by_cases hφ : Measurable φ; swap
   · simp [VectorMeasure.map, hφ, Measure.zero_le]
   apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)

From b63174b77e62aca687309efd0f545b145b2cdd44 Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Thu, 21 May 2026 14:08:08 +0200
Subject: [PATCH 06/12] more

---
 .../MeasureTheory/VectorMeasure/Basic.lean    | 37 ++++++++++---------
 1 file changed, 20 insertions(+), 17 deletions(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
index 56e93b0eec11cc..b35e41ce32f568 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
@@ -723,6 +723,11 @@ theorem restrict_singleton {a : α} : v.restrict {a} = VectorMeasure.dirac a (v
     by_cases ha : a ∈ s <;> simp [*, restrict_apply]
   · simp [restrict, h]
 
+theorem restrict_restrict {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) :
+    (v.restrict t).restrict s = v.restrict (s ∩ t) := by
+  ext u hu
+  simp [restrict_apply, hs, hu, ht, Set.inter_assoc]
+
 section ContinuousAdd
 
 variable [ContinuousAdd M]
@@ -755,7 +760,21 @@ def restrictGm (i : Set α) : VectorMeasure α M →+ VectorMeasure α M where
   map_zero' := restrict_zero
   map_add' _ _ := restrict_add _ _ i
 
-variable [T2Space M] {s t : Set α}
+end ContinuousAdd
+
+section Partition
+
+variable {M : Type*} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] [ContinuousAdd M]
+variable (v : VectorMeasure α M) {i s t : Set α}
+
+@[simp]
+theorem restrict_add_restrict_compl (hi : MeasurableSet i) :
+    v.restrict i + v.restrict iᶜ = v := by
+  ext A hA
+  rw [add_apply, restrict_apply _ hi hA, restrict_apply _ hi.compl hA,
+    ← of_union _ (hA.inter hi) (hA.inter hi.compl)]
+  · simp
+  · exact disjoint_compl_right.inter_right' A |>.inter_left' A
 
 theorem restrict_inter_add_diff (hs : MeasurableSet s) (ht : MeasurableSet t) :
     v.restrict (s ∩ t) + v.restrict (s \ t) = v.restrict s := by
@@ -774,22 +793,6 @@ theorem restrict_union (h : Disjoint s t) (hs : MeasurableSet s) (ht : Measurabl
     v.restrict (s ∪ t) = v.restrict s + v.restrict t := by
   simp [← v.restrict_union_add_inter hs ht, disjoint_iff_inter_eq_empty.mp h]
 
-end ContinuousAdd
-
-section Partition
-
-variable {M : Type*} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] [ContinuousAdd M]
-variable (v : VectorMeasure α M) {i : Set α}
-
-@[simp]
-theorem restrict_add_restrict_compl (hi : MeasurableSet i) :
-    v.restrict i + v.restrict iᶜ = v := by
-  ext A hA
-  rw [add_apply, restrict_apply _ hi hA, restrict_apply _ hi.compl hA,
-    ← of_union _ (hA.inter hi) (hA.inter hi.compl)]
-  · simp
-  · exact disjoint_compl_right.inter_right' A |>.inter_left' A
-
 end Partition
 
 section Sub

From cb5e43014b31fe475d2796309bd37a72c0bb76bb Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Thu, 21 May 2026 14:09:32 +0200
Subject: [PATCH 07/12] implicit argument

---
 Mathlib/MeasureTheory/VectorMeasure/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
index b35e41ce32f568..b9d5701e7bf005 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
@@ -765,7 +765,7 @@ end ContinuousAdd
 section Partition
 
 variable {M : Type*} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] [ContinuousAdd M]
-variable (v : VectorMeasure α M) {i s t : Set α}
+variable {v : VectorMeasure α M} {i s t : Set α}
 
 @[simp]
 theorem restrict_add_restrict_compl (hi : MeasurableSet i) :

From a3dd73849110542eb2426938410a22b18d2ebbb8 Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Thu, 21 May 2026 14:24:46 +0200
Subject: [PATCH 08/12] fix

---
 .../VectorMeasure/Decomposition/JordanSub.lean           | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Decomposition/JordanSub.lean b/Mathlib/MeasureTheory/VectorMeasure/Decomposition/JordanSub.lean
index 1ab015aac88725..026c666ed2b7ca 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Decomposition/JordanSub.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Decomposition/JordanSub.lean
@@ -76,9 +76,9 @@ theorem sub_toSignedMeasure_eq_toSignedMeasure_sub :
     sub_apply_eq_zero_of_isHahnDecomposition hs
   have h₂' := toSignedMeasure_congr <| restrict_eq_zero.mpr <|
   sub_apply_eq_zero_of_isHahnDecomposition hsc
-  have partition₁ := VectorMeasure.restrict_add_restrict_compl (μ - ν).toSignedMeasure
+  have partition₁ := VectorMeasure.restrict_add_restrict_compl (v := (μ - ν).toSignedMeasure)
     hs.measurableSet
-  have partition₂ := VectorMeasure.restrict_add_restrict_compl (ν - μ).toSignedMeasure
+  have partition₂ := VectorMeasure.restrict_add_restrict_compl (v := (ν - μ).toSignedMeasure)
     hs.measurableSet
   rw [toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hs.measurableSet,
     toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hs.measurableSet.compl]
@@ -86,10 +86,9 @@ theorem sub_toSignedMeasure_eq_toSignedMeasure_sub :
   rw [h₁', h₂] at partition₁
   rw [h₁, h₂'] at partition₂
   simp only [toSignedMeasure_zero, zero_add] at partition₁ partition₂
-  rw [← VectorMeasure.restrict_add_restrict_compl μ.toSignedMeasure hs.measurableSet,
-    ← VectorMeasure.restrict_add_restrict_compl ν.toSignedMeasure hs.measurableSet,
+  rw [← VectorMeasure.restrict_add_restrict_compl (v := μ.toSignedMeasure) hs.measurableSet,
+    ← VectorMeasure.restrict_add_restrict_compl (v := ν.toSignedMeasure) hs.measurableSet,
     ← partition₁, ← partition₂]
-  repeat rw [sub_eq_add_neg]
   abel
 
 /-- The Jordan decomposition associated to the pair of mutually singular measures `μ - ν`

From 7b19a49da99a9189b51f6f91a98f902940d78e1a Mon Sep 17 00:00:00 2001
From: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Sun, 24 May 2026 18:58:09 +0200
Subject: [PATCH 09/12] Apply suggestions from code review

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
---
 .../MeasureTheory/Measure/MeasureSpace.lean   |  9 +++---
 .../MeasureTheory/VectorMeasure/Basic.lean    |  4 +--
 .../VectorMeasure/Variation/Basic.lean        | 32 +++++++------------
 3 files changed, 17 insertions(+), 28 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index c15b18d4e60997..61ace844bbb268 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -1080,11 +1080,10 @@ protected theorem le_add_left (h : μ ≤ ν) : μ ≤ ν' + ν := fun s => le_a
 protected theorem le_add_right (h : μ ≤ ν) : μ ≤ ν + ν' := fun s => le_add_right (h s)
 
 instance [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] [CovariantClass R ℝ≥0∞ (· • ·) (· ≤ ·)] :
-    CovariantClass R (Measure α) (· • ·) (· ≤ ·) := by
-  constructor
-  intro c μ ν hμν s
-  simp only [smul_apply]
-  gcongr
+    CovariantClass R (Measure α) (· • ·) (· ≤ ·) where
+  elim c μ ν hμν s := by
+    simp only [smul_apply]
+    gcongr
 
 section sInf
 
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
index b9d5701e7bf005..3717c58dbb6e82 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
@@ -719,7 +719,7 @@ theorem restrict_dirac {s : Set α} {x : α} {m : M} (hs : MeasurableSet s) [Dec
 @[simp]
 theorem restrict_singleton {a : α} : v.restrict {a} = VectorMeasure.dirac a (v {a}) := by
   by_cases h : MeasurableSet {a}
-  · ext1 s hs
+  · ext s hs
     by_cases ha : a ∈ s <;> simp [*, restrict_apply]
   · simp [restrict, h]
 
@@ -778,7 +778,7 @@ theorem restrict_add_restrict_compl (hi : MeasurableSet i) :
 
 theorem restrict_inter_add_diff (hs : MeasurableSet s) (ht : MeasurableSet t) :
     v.restrict (s ∩ t) + v.restrict (s \ t) = v.restrict s := by
-  ext1 u hu
+  ext u hu
   simp only [add_apply, restrict_apply, hs, hu, hs.inter ht, hs.diff ht]
   rw [← of_union (by grind) (hu.inter (hs.inter ht)) (hu.inter (hs.diff ht))]
   congr
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
index 2c26456642017a..c89776b743ac67 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
@@ -139,12 +139,9 @@ lemma variation_finsetSum_le [ContinuousAdd V] {ι} (s : Finset ι) (μ : ι →
 lemma variation_apply_eq_zero (hs : MeasurableSet s) :
     μ.variation s = 0 ↔ ∀ t, t ⊆ s → MeasurableSet t → μ t = 0 := by
   refine ⟨fun h t hts ht ↦ ?_, fun h ↦ ?_⟩
-  · apply enorm_eq_zero.1
-    apply le_antisymm ?_ zero_le
-    rw [← h]
+  · rw [← enorm_eq_zero, ← le_zero_iff, ← h]
     apply (enorm_measure_le_variation _ _).trans (measure_mono hts)
-  · apply le_antisymm ?_ zero_le
-    change μ.variation s ≤ (0 : Measure X) s
+  · suffices μ.variation s ≤ (0 : Measure X) s by simpa
     apply variation_apply_le_of_forall_enorm_le hs (fun t ht hts ↦ ?_)
     simp [h t hts ht]
 
@@ -154,7 +151,7 @@ lemma variation_apply_eq_zero (hs : MeasurableSet s) :
   ext s hs
   apply enorm_eq_zero.1
   apply le_antisymm ?_ (by simp)
-  grw [enorm_measure_le_variation]
+  grw [← le_zero_iff, enorm_measure_le_variation]
   simp [h]
 
 lemma variation_restrict (hs : MeasurableSet s) :
@@ -181,27 +178,21 @@ lemma variation_restrict (hs : MeasurableSet s) :
 lemma variation_restrict_le : (μ.restrict s).variation ≤ μ.variation.restrict s := by
   by_cases hs : MeasurableSet s
   · simp [variation_restrict hs]
-  · simp only [restrict_not_measurable _ hs, variation_zero, Measure.zero_le]
+  · simp [restrict_not_measurable _ hs, Measure.zero_le]
 
-instance [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.restrict s).variation := by
-  constructor
-  grw [variation_restrict_le]
-  exact IsFiniteMeasure.measure_univ_lt_top
+instance [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.restrict s).variation :=
+  isFiniteMeasure_of_le _ variation_restrict_le
 
 variable {Y : Type*} [MeasurableSpace Y] {φ : X → Y}
 
-lemma variation_map_le : (μ.map φ).variation ≤ Measure.map φ μ.variation := by
+lemma variation_map_le : (μ.map φ).variation ≤ μ.variation.map φ := by
   by_cases hφ : Measurable φ; swap
   · simp [VectorMeasure.map, hφ, Measure.zero_le]
   apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)
-  simp only [Measure.map_apply hφ hs]
-  apply le_trans ?_ (enorm_measure_le_variation _ _)
-  simp [VectorMeasure.map_apply _ hφ hs]
+  simp [VectorMeasure.map_apply _ hφ hs, Measure.map_apply hφ hs, enorm_measure_le_variation]
 
-instance [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.map φ).variation := by
-  constructor
-  grw [variation_map_le]
-  exact IsFiniteMeasure.measure_univ_lt_top
+instance [IsFiniteMeasure μ.variation] : IsFiniteMeasure (μ.map φ).variation :=
+  isFiniteMeasure_of_le _ variation_map_le
 
 theorem _root_.MeasurableEmbedding.variation_map (hφ : MeasurableEmbedding φ) :
     (μ.map φ).variation = μ.variation.map φ := by
@@ -252,8 +243,7 @@ private lemma variation_smul_le {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 
     (c • μ).variation ≤ ‖c‖₊ • μ.variation := by
   apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)
   simp only [coe_smul, Pi.smul_apply, enorm_smul, Measure.smul_apply, Measure.nnreal_smul_coe_apply]
-  grw [enorm_measure_le_variation]
-  exact le_rfl
+  grw [enorm_measure_le_variation, enorm_eq_nnnorm]
 
 lemma variation_smul {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 V] {c : 𝕜} :
     (c • μ).variation = ‖c‖₊ • μ.variation := by

From 36352bffa0abf3ef01f3e33e5780f96f1a138aee Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Sun, 24 May 2026 21:55:58 +0200
Subject: [PATCH 10/12] fix, improve

---
 .../MeasureTheory/VectorMeasure/Basic.lean    | 15 ++++++++
 .../VectorMeasure/Variation/Basic.lean        | 35 +++++++++----------
 2 files changed, 32 insertions(+), 18 deletions(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
index 3717c58dbb6e82..6298a9e6d34382 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
@@ -649,6 +649,7 @@ variable {R : Type*} [Semiring R] [Module R M] [Module R N]
 
 variable [ContinuousConstSMul R M] [ContinuousConstSMul R N]
 
+@[simp]
 theorem mapRange_smul {v : VectorMeasure α M} {f : M →ₗ[R] N} (hf : Continuous f) {c : R} :
     (c • v).mapRange f.toAddMonoidHom hf = c • (v.mapRange f.toAddMonoidHom hf) := by
   ext; simp
@@ -716,6 +717,20 @@ theorem restrict_dirac {s : Set α} {x : α} {m : M} (hs : MeasurableSet s) [Dec
   simp only [hs, ht, restrict_apply]
   split_ifs with has <;> simp [dirac, ht, ht.inter hs, has]
 
+@[simp]
+theorem restrict_dirac_of_mem {s : Set α} {x : α} {m : M} (hs : MeasurableSet s) (hx : x ∈ s) :
+    (VectorMeasure.dirac x m).restrict s = VectorMeasure.dirac x m := by
+  classical
+  simp [restrict_dirac, hs, hx]
+
+@[simp]
+theorem restrict_dirac_of_notMem {s : Set α} {x : α} {m : M} (hx : x ∉ s) :
+    (VectorMeasure.dirac x m).restrict s = 0 := by
+  classical
+  by_cases hs : MeasurableSet s
+  · simp [restrict_dirac, hs, hx]
+  · simp [restrict, hs]
+
 @[simp]
 theorem restrict_singleton {a : α} : v.restrict {a} = VectorMeasure.dirac a (v {a}) := by
   by_cases h : MeasurableSet {a}
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
index c89776b743ac67..1abcebc11dcbbe 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
@@ -146,13 +146,14 @@ lemma variation_apply_eq_zero (hs : MeasurableSet s) :
     simp [h t hts ht]
 
 @[simp] lemma variation_eq_zero :
-    μ.variation = 0 ↔ μ = 0 := by
-  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-  ext s hs
-  apply enorm_eq_zero.1
-  apply le_antisymm ?_ (by simp)
-  grw [← le_zero_iff, enorm_measure_le_variation]
-  simp [h]
+    μ.variation = 0 ↔ μ = 0 where
+  mp h := by
+    ext s hs
+    apply enorm_eq_zero.1
+    apply le_antisymm ?_ (by simp)
+    grw [enorm_measure_le_variation]
+    simp [h]
+  mpr h := by simp [h]
 
 lemma variation_restrict (hs : MeasurableSet s) :
     (μ.restrict s).variation = μ.variation.restrict s := by
@@ -165,10 +166,8 @@ lemma variation_restrict (hs : MeasurableSet s) :
     calc μ.variation (t ∩ s)
     _ ≤ (μ.restrict s).variation (t ∩ s) := by
       apply variation_apply_le_of_forall_enorm_le (ht.inter hs) (fun u u_meas hu ↦ ?_)
-      have : μ u = μ.restrict s u := by
-        rw [VectorMeasure.restrict_apply _ hs u_meas]
-        congr
-        grind
+      have : μ u = μ.restrict s u :=
+        (VectorMeasure.restrict_eq_self _ hs u_meas (hu.trans inter_subset_right)).symm
       rw [this]
       apply enorm_measure_le_variation
     _ ≤ (μ.restrict s).variation t := by
@@ -263,13 +262,13 @@ instance {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 V] {c : 𝕜} [IsFi
   simp only [variation_smul]
   infer_instance
 
-instance [Finite X] : IsFiniteMeasure μ.variation := by
-  classical
-  let : Fintype X := Fintype.ofFinite X
-  constructor
-  simp only [variation_apply, preVariation_apply, MeasurableSet.univ, ennrealToMeasure_apply,
-    ennrealPreVariation_apply, preVariationFun, ↓reduceDIte, ← sup_univ_eq_ciSup]
-  exact (Finset.sup_lt_iff (by simp)).2 (fun b hb ↦ by simp [ENNReal.sum_lt_top, enorm_lt_top])
+instance [Finite X] : IsFiniteMeasure μ.variation where
+  measure_univ_lt_top := by
+    classical
+    let : Fintype X := Fintype.ofFinite X
+    simp only [variation_apply, preVariation_apply, MeasurableSet.univ, ennrealToMeasure_apply,
+      ennrealPreVariation_apply, preVariationFun, ↓reduceDIte, ← sup_univ_eq_ciSup]
+    exact (Finset.sup_lt_iff (by simp)).2 (fun b hb ↦ by simp [ENNReal.sum_lt_top, enorm_lt_top])
 
 instance {x : X} {v : V} : IsFiniteMeasure (VectorMeasure.dirac x v).variation := by
   simp only [variation_dirac, enorm_eq_nnnorm, Measure.coe_nnreal_smul]

From 0cb2b103f6dc3a748c2a6cfc03d7fc7d1d98ff14 Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Sun, 24 May 2026 22:14:22 +0200
Subject: [PATCH 11/12] cleanup

---
 Mathlib/MeasureTheory/VectorMeasure/Basic.lean | 11 -----------
 1 file changed, 11 deletions(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
index 6298a9e6d34382..c5eaba293c89ad 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
@@ -123,14 +123,6 @@ theorem ext_iff (v w : VectorMeasure α M) : v = w ↔ ∀ i : Set α, Measurabl
 theorem ext {s t : VectorMeasure α M} (h : ∀ i : Set α, MeasurableSet i → s i = t i) : s = t :=
   (ext_iff s t).2 h
 
-@[nontriviality]
-lemma apply_eq_zero_of_isEmpty [IsEmpty α] (v : VectorMeasure α M) (s : Set α) :
-    v s = 0 := by
-  rw [eq_empty_of_isEmpty s, empty]
-
-instance instSubsingleton [IsEmpty α] : Subsingleton (VectorMeasure α M) :=
-  ⟨fun μ ν => by ext1 s _; rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]⟩
-
 variable [Countable β] {v : VectorMeasure α M} {f : β → Set α}
 
 theorem hasSum_of_disjoint_iUnion (hm : ∀ i, MeasurableSet (f i)) (hd : Pairwise (Disjoint on f)) :
@@ -295,9 +287,6 @@ theorem coe_zero : ⇑(0 : VectorMeasure α M) = 0 := rfl
 
 theorem zero_apply (i : Set α) : (0 : VectorMeasure α M) i = 0 := rfl
 
-theorem eq_zero_of_isEmpty [IsEmpty α] (v : VectorMeasure α M) : v = 0 :=
-  Subsingleton.elim v 0
-
 variable [ContinuousAdd M]
 
 /-- The sum of two vector measure is a vector measure. -/

From 06cfdd55346d11e8b4420b02588e1ffd18e51962 Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Sat, 30 May 2026 13:56:06 +0200
Subject: [PATCH 12/12] remove useless namespacing

---
 Mathlib/MeasureTheory/VectorMeasure/Basic.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
index c5eaba293c89ad..84d98573283ec5 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
@@ -700,7 +700,7 @@ theorem restrict_zero {i : Set α} : (0 : VectorMeasure α M).restrict i = 0 :=
   · exact dif_neg hi
 
 theorem restrict_dirac {s : Set α} {x : α} {m : M} (hs : MeasurableSet s) [Decidable (x ∈ s)] :
-    (VectorMeasure.dirac x m).restrict s = if x ∈ s then VectorMeasure.dirac x m else 0 := by
+    (dirac x m).restrict s = if x ∈ s then dirac x m else 0 := by
   classical
   ext t ht
   simp only [hs, ht, restrict_apply]
@@ -708,20 +708,20 @@ theorem restrict_dirac {s : Set α} {x : α} {m : M} (hs : MeasurableSet s) [Dec
 
 @[simp]
 theorem restrict_dirac_of_mem {s : Set α} {x : α} {m : M} (hs : MeasurableSet s) (hx : x ∈ s) :
-    (VectorMeasure.dirac x m).restrict s = VectorMeasure.dirac x m := by
+    (dirac x m).restrict s = dirac x m := by
   classical
   simp [restrict_dirac, hs, hx]
 
 @[simp]
 theorem restrict_dirac_of_notMem {s : Set α} {x : α} {m : M} (hx : x ∉ s) :
-    (VectorMeasure.dirac x m).restrict s = 0 := by
+    (dirac x m).restrict s = 0 := by
   classical
   by_cases hs : MeasurableSet s
   · simp [restrict_dirac, hs, hx]
   · simp [restrict, hs]
 
 @[simp]
-theorem restrict_singleton {a : α} : v.restrict {a} = VectorMeasure.dirac a (v {a}) := by
+theorem restrict_singleton {a : α} : v.restrict {a} = dirac a (v {a}) := by
   by_cases h : MeasurableSet {a}
   · ext s hs
     by_cases ha : a ∈ s <;> simp [*, restrict_apply]
@@ -1104,7 +1104,7 @@ theorem trans {u : VectorMeasure α L} {v : VectorMeasure α M} {w : VectorMeasu
   fun _ hs => huv <| hvw hs
 
 theorem zero (v : VectorMeasure α N) : (0 : VectorMeasure α M) ≪ᵥ v :=
-  fun s _ => VectorMeasure.zero_apply s
+  fun s _ => zero_apply s
 
 theorem neg_left {M : Type*} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M]
     {v : VectorMeasure α M} {w : VectorMeasure α N} (h : v ≪ᵥ w) : -v ≪ᵥ w := by