From df68816c3c7e13a50d951094f39a11dd221a7b5e Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Fri, 8 May 2026 09:09:49 -0400
Subject: [PATCH 01/24] update

---
 .../Integral/FinMeasAdditive.lean             |  50 +++++
 Mathlib/MeasureTheory/Integral/SetToL1.lean   |  51 +++++
 .../MeasureTheory/VectorMeasure/Basic.lean    |  11 ++
 .../MeasureTheory/VectorMeasure/Integral.lean | 174 ++++++++++++++++--
 4 files changed, 269 insertions(+), 17 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
index e492295f3a9e7f..dc12d039116d00 100644
--- a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
+++ b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
@@ -68,6 +68,16 @@ theorem add (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive μ T') :
   simp only [hT s t hs ht hμs hμt hst, hT' s t hs ht hμs hμt hst, Pi.add_apply]
   abel
 
+theorem add_measure {ν : Measure α} (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive ν T') :
+    FinMeasAdditive (μ + ν) (T + T') := by
+  intro s t hms hmt hs ht hst
+  have hμs : μ s ≠ ∞ := ((Measure.le_add_right le_rfl s).trans_lt hs.lt_top).ne
+  have hμt : μ t ≠ ∞ := ((Measure.le_add_right le_rfl t).trans_lt ht.lt_top).ne
+  have hνs : ν s ≠ ∞ := ((Measure.le_add_left le_rfl s).trans_lt hs.lt_top).ne
+  have hνt : ν t ≠ ∞ := ((Measure.le_add_left le_rfl t).trans_lt ht.lt_top).ne
+  simp [hT s t hms hmt hμs hμt hst, hT' s t hms hmt hνs hνt hst]
+  abel
+
 theorem smul [DistribSMul 𝕜 β] (hT : FinMeasAdditive μ T) (c : 𝕜) :
     FinMeasAdditive μ fun s => c • T s := fun s t hs ht hμs hμt hst => by
   simp [hT s t hs ht hμs hμt hst]
@@ -166,6 +176,11 @@ theorem add (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditi
   rw [Pi.add_apply, add_mul]
   exact (norm_add_le _ _).trans (add_le_add (hT.2 s hs hμs) (hT'.2 s hs hμs))
 
+theorem mono_bound (hT : DominatedFinMeasAdditive μ T C) (hCC' : C ≤ C') :
+    DominatedFinMeasAdditive μ T C' :=
+  ⟨hT.1, fun s hs hμs =>
+    (hT.2 s hs hμs).trans (mul_le_mul_of_nonneg_right hCC' measureReal_nonneg)⟩
+
 theorem smul [SeminormedAddGroup 𝕜] [DistribSMul 𝕜 β] [IsBoundedSMul 𝕜 β]
     (hT : DominatedFinMeasAdditive μ T C) (c : 𝕜) :
     DominatedFinMeasAdditive μ (fun s => c • T s) (‖c‖ * C) := by
@@ -185,6 +200,21 @@ theorem of_measure_le {μ' : Measure α} (h : μ ≤ μ') (hT : DominatedFinMeas
       gcongr
       exact hμ's.ne
 
+theorem add_measure {C' : ℝ} (μ ν : Measure α)
+    (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive ν T' C') :
+    DominatedFinMeasAdditive (μ + ν) (T + T') (max C C') := by
+  refine ⟨hT.1.add_measure hT'.1, fun s hs hsf ↦ ?_⟩
+  have hμs : μ s < ∞ := (Measure.le_add_right le_rfl s).trans_lt hsf
+  have hνs : ν s < ∞ := (Measure.le_add_left le_rfl s).trans_lt hsf
+  rw [Pi.add_apply, measureReal_add_apply hμs.ne hνs.ne, mul_add]
+  calc
+    ‖T s + T' s‖ ≤ ‖T s‖ + ‖T' s‖ := norm_add_le _ _
+    _ ≤ C * μ.real s + C' * ν.real s := add_le_add (hT.2 s hs hμs) (hT'.2 s hs hνs)
+    _ ≤ max C C' * μ.real s + max C C' * ν.real s := by
+      gcongr
+      · exact le_max_left C C'
+      · exact le_max_right C C'
+
 theorem add_measure_right {_ : MeasurableSpace α} (μ ν : Measure α)
     (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) : DominatedFinMeasAdditive (μ + ν) T C :=
   of_measure_le (Measure.le_add_right le_rfl) hT hC
@@ -193,6 +223,26 @@ theorem add_measure_left {_ : MeasurableSpace α} (μ ν : Measure α)
     (hT : DominatedFinMeasAdditive ν T C) (hC : 0 ≤ C) : DominatedFinMeasAdditive (μ + ν) T C :=
   of_measure_le (Measure.le_add_left le_rfl) hT hC
 
+theorem finsetSum_measure {ι} {_ : MeasurableSpace α} (s : Finset ι) (μ : ι → Measure α)
+    (T : ι → Set α → β) (C : ι → ℝ)
+    (hT : ∀ i, DominatedFinMeasAdditive (μ i) (T i) (C i)) :
+    DominatedFinMeasAdditive (∑ i ∈ s, μ i) (∑ i ∈ s, T i)
+      (∑ i ∈ s, max (C i) 0) := by
+  classical
+  induction s using Finset.induction_on with
+  | empty =>
+      simpa using (zero (0 : Measure α) (β := β) (C := 0) le_rfl)
+  | insert i s his ih =>
+      have h_nonneg : 0 ≤ ∑ j ∈ s, max (C j) 0 :=
+        Finset.sum_nonneg fun j _ => le_max_right _ _
+      have hle : max (C i) (∑ j ∈ s, max (C j) 0) ≤
+          ∑ j ∈ insert i s, max (C j) 0 := by
+        rw [Finset.sum_insert his]
+        exact max_le ((le_max_left _ _).trans (le_add_of_nonneg_right h_nonneg))
+          (le_add_of_nonneg_left (le_max_right _ _))
+      simpa [Finset.sum_insert, his] using
+        ((hT i).add_measure (μ i) (∑ j ∈ s, μ j) ih).mono_bound hle
+
 theorem of_smul_measure {c : ℝ≥0∞} (hc_ne_top : c ≠ ∞) (hT : DominatedFinMeasAdditive (c • μ) T C) :
     DominatedFinMeasAdditive μ T (c.toReal * C) := by
   have h : ∀ s, MeasurableSet s → c • μ s = ∞ → μ s = ∞ := by
diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean
index fb257b16c4850e..a2c27024e349e8 100644
--- a/Mathlib/MeasureTheory/Integral/SetToL1.lean
+++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean
@@ -980,6 +980,57 @@ theorem setToFun_congr_measure_of_add_left {μ' : Measure α}
   rw [one_smul]
   exact Measure.le_add_left le_rfl
 
+theorem setToFun_add_measure {ν : Measure α} (hTμ : DominatedFinMeasAdditive μ T C)
+    (hTν : DominatedFinMeasAdditive ν T' C') (hμ : Integrable f μ) (hν : Integrable f ν) :
+    setToFun (μ + ν) (T + T') (hTμ.add_measure μ ν hTν) f =
+      setToFun μ T hTμ f + setToFun ν T' hTν f := by
+  have hfi := hμ.add_measure hν
+  have hTμ_add : DominatedFinMeasAdditive (μ + ν) T (max C 0) :=
+    (hTμ.mono_bound (le_max_left C 0)).of_measure_le (Measure.le_add_right le_rfl)
+      (le_max_right C 0)
+  have hTν_add : DominatedFinMeasAdditive (μ + ν) T' (max C' 0) :=
+    (hTν.mono_bound (le_max_left C' 0)).of_measure_le (Measure.le_add_left le_rfl)
+      (le_max_right C' 0)
+  calc
+    setToFun (μ + ν) (T + T') (hTμ.add_measure μ ν hTν) f =
+        setToFun (μ + ν) (T + T') (hTμ_add.add hTν_add) f :=
+      setToFun_congr_left _ _ rfl f
+    _ = setToFun (μ + ν) T hTμ_add f + setToFun (μ + ν) T' hTν_add f :=
+      setToFun_add_left hTμ_add hTν_add f
+    _ = setToFun μ T hTμ f + setToFun ν T' hTν f := by
+      rw [setToFun_congr_measure_of_add_right hTμ_add hTμ f hfi,
+        setToFun_congr_measure_of_add_left hTν_add hTν f hfi]
+
+theorem setToFun_finsetSum_measure {ι} (s : Finset ι) {μs : ι → Measure α}
+    {Ts : ι → Set α → E →L[ℝ] F} {Cs : ι → ℝ}
+    (hTs : ∀ i, DominatedFinMeasAdditive (μs i) (Ts i) (Cs i))
+    (hf : ∀ i ∈ s, Integrable f (μs i)) :
+    setToFun (∑ i ∈ s, μs i) (∑ i ∈ s, Ts i)
+        (DominatedFinMeasAdditive.finsetSum_measure s μs Ts Cs hTs) f =
+      ∑ i ∈ s, setToFun (μs i) (Ts i) (hTs i) f := by
+  classical
+  induction s using Finset.induction_on with
+  | empty =>
+      exact setToFun_zero_left
+  | insert i s his ih =>
+      have hrest : Integrable f (∑ j ∈ s, μs j) :=
+        integrable_finsetSum_measure.2 fun j hj => hf j (Finset.mem_insert_of_mem hj)
+      have h_add : DominatedFinMeasAdditive (∑ j ∈ insert i s, μs j) (∑ j ∈ insert i s, Ts j)
+          (max (Cs i) (∑ j ∈ s, max (Cs j) 0)) := by
+        simpa [Finset.sum_insert, his] using
+          ((hTs i).add_measure (μs i) (∑ j ∈ s, μs j)
+            (DominatedFinMeasAdditive.finsetSum_measure s μs Ts Cs hTs))
+      calc
+        setToFun (∑ j ∈ insert i s, μs j) (∑ j ∈ insert i s, Ts j)
+            (DominatedFinMeasAdditive.finsetSum_measure (insert i s) μs Ts Cs hTs) f =
+            setToFun (∑ j ∈ insert i s, μs j) (∑ j ∈ insert i s, Ts j) h_add f :=
+          setToFun_congr_left _ _ rfl f
+        _ = ∑ j ∈ insert i s, setToFun (μs j) (Ts j) (hTs j) f := by
+          simpa [Finset.sum_insert, his, ih fun j hj => hf j (Finset.mem_insert_of_mem hj)] using
+            setToFun_add_measure (hTs i)
+              (DominatedFinMeasAdditive.finsetSum_measure s μs Ts Cs hTs)
+              (hf i (Finset.mem_insert_self i s)) hrest
+
 theorem setToFun_top_smul_measure (hT : DominatedFinMeasAdditive (∞ • μ) T C) (f : α → E) :
     setToFun (∞ • μ) T hT f = 0 := by
   refine setToFun_measure_zero' hT fun s _ hμs => ?_
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
index e45965e0dbc9f6..b60d0c6cbb9019 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
@@ -282,6 +282,17 @@ instance instZero : Zero (VectorMeasure α M) :=
 instance instInhabited : Inhabited (VectorMeasure α M) :=
   ⟨0⟩
 
+@[nontriviality]
+lemma apply_eq_zero_of_isEmpty [IsEmpty α] (μ : VectorMeasure α M) (s : Set α) :
+    μ s = 0 := by
+  simp [eq_empty_of_isEmpty s]
+
+instance instSubsingleton [IsEmpty α] : Subsingleton (VectorMeasure α M) :=
+  ⟨fun μ ν => by ext1 s _; rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]⟩
+
+theorem eq_zero_of_isEmpty [IsEmpty α] (μ : VectorMeasure α M) : μ = 0 :=
+  Subsingleton.elim μ 0
+
 @[simp]
 theorem coe_zero : ⇑(0 : VectorMeasure α M) = 0 := rfl
 
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
index 201814264e89b9..faa3da2ead410c 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
@@ -63,7 +63,7 @@ public section
 
 open Set MeasureTheory VectorMeasure ContinuousLinearMap
 
-variable {X E F G : Type*} {mX : MeasurableSpace X}
+variable {ι X E F G : Type*} {mX : MeasurableSpace X}
   [NormedAddCommGroup E] [NormedSpace ℝ E]
   [NormedAddCommGroup F] [NormedSpace ℝ F]
   [NormedAddCommGroup G] [NormedSpace ℝ G]
@@ -134,61 +134,201 @@ noncomputable def integral (μ : VectorMeasure X F) (f : X → E) (B : E →L[
   else 0
 
 @[inherit_doc integral]
-notation3 "∫ᵛ "(...)", "r:60:(scoped f => f)" ∂["B:70"; "μ:70"]" => integral μ r B
+notation3 "∫ᵛ "(...)", "r:60:(scoped f => f)" ∂["B:65"; "μ:65"]" => integral μ r B
 
 /-- The special case of the pairing integral where the pairing is just the scalar multiplication by
 `ℝ` on `F` and `f` is real-valued. The resulting integral is `F`-valued.-/
 notation3 "∫ᵛ "(...)", "r:60:(scoped f => f)" ∂•"μ:70 => integral μ r (lsmul ℝ ℝ)
 
-variable {μ : VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G}
+variable {f g : X → E} {μ ν : VectorMeasure X F} {B C : E →L[ℝ] F →L[ℝ] G}
 
-theorem integral_fun_add {f g : X → E} (hf : μ.Integrable f B) (hg : μ.Integrable g B) :
+@[simp]
+theorem transpose_zero_vectorMeasure (B : E →L[ℝ] F →L[ℝ] G) :
+    (0 : VectorMeasure X F).transpose B = 0 := by
+  simp [transpose]
+
+@[simp]
+theorem transpose_zero_cbm (μ : VectorMeasure X F) :
+    μ.transpose (0 : E →L[ℝ] F →L[ℝ] G) = 0 := by
+  ext
+  simp [transpose]
+
+@[simp]
+theorem transpose_smul (c : ℝ) (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) :
+    μ.transpose (c • B) = c • (μ.transpose B) := by
+  ext
+  simp [transpose]
+
+section Function
+
+theorem integral_undef (h : ¬ μ.Integrable f B) :
+    ∫ᵛ x, f x ∂[B; μ] = 0 := by
+  by_cases hG : CompleteSpace G
+  · simp [integral, setToFun_undef _ h]
+  · simp [integral, hG]
+
+@[simp]
+theorem integral_zero : ∫ᵛ _, 0 ∂[B; μ] = 0 := by
+  by_cases hG : CompleteSpace G
+  · simp only [integral, hG]
+    exact setToFun_zero (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
+  · simp [integral, hG]
+
+theorem integral_congr_ae (h : f =ᵐ[(μ.transpose B).variation] g) :
+    ∫ᵛ x, f x ∂[B; μ] = ∫ᵛ x, g x ∂[B; μ] := by
+  by_cases hG : CompleteSpace G
+  · simp only [integral, hG]
+    exact setToFun_congr_ae (dominatedFinMeasAdditive_cbmApplyMeasure μ B) h
+  · simp [integral, hG]
+
+theorem integral_eq_zero_of_ae (hf : f =ᵐ[(μ.transpose B).variation] 0) :
+    ∫ᵛ x, f x ∂[B; μ] = 0 := by
+  simp [integral_congr_ae hf]
+
+theorem integral_fun_add (hf : μ.Integrable f B) (hg : μ.Integrable g B) :
     ∫ᵛ x, f x + g x ∂[B; μ] = ∫ᵛ x, f x ∂[B; μ] + ∫ᵛ x, g x ∂[B; μ] := by
   by_cases hG : CompleteSpace G
   · simp only [integral, hG]
     exact setToFun_add (dominatedFinMeasAdditive_cbmApplyMeasure μ B) hf hg
   · simp [integral, hG]
 
-theorem integral_add {f g : X → E} (hf : μ.Integrable f B) (hg : μ.Integrable g B) :
+theorem integral_add (hf : μ.Integrable f B) (hg : μ.Integrable g B) :
     ∫ᵛ x, (f + g) x ∂[B; μ] = ∫ᵛ x, f x ∂[B; μ] + ∫ᵛ x, g x ∂[B; μ] := integral_fun_add hf hg
 
-variable (μ B) in
+theorem integral_finsetSum (s : Finset ι) {f : ι → X → E}
+    (hf : ∀ i ∈ s, μ.Integrable (f i) B) :
+    ∫ᵛ x, ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ x, f i x ∂[B; μ] := by
+  by_cases hG : CompleteSpace G
+  · simp only [integral, hG]
+    exact setToFun_finsetSum (dominatedFinMeasAdditive_cbmApplyMeasure μ B) s hf
+  · simp [integral, hG]
+
+variable (f μ B) in
 @[integral_simps]
-theorem integral_fun_neg (f : X → E) :
+theorem integral_fun_neg :
     ∫ᵛ x, -f x ∂[B; μ]= -∫ᵛ x, f x ∂[B; μ] := by
   by_cases hG : CompleteSpace G
   · simp only [integral, hG, ↓reduceDIte, transpose_eq_cbmApplyMeasure]
     exact setToFun_neg (dominatedFinMeasAdditive_cbmApplyMeasure μ B) f
   · simp [integral, hG]
 
-variable (μ B) in
+variable (f μ B) in
 @[integral_simps]
-theorem integral_neg (f : X → E) :
-    ∫ᵛ x, (-f) x ∂[B; μ] = -∫ᵛ x, f x ∂[B; μ] := integral_fun_neg μ B f
+theorem integral_neg :
+    ∫ᵛ x, (-f) x ∂[B; μ] = -∫ᵛ x, f x ∂[B; μ] := integral_fun_neg f μ B
 
-theorem integral_fun_sub {f g : X → E} (hf : μ.Integrable f B) (hg : μ.Integrable g B) :
+theorem integral_fun_sub (hf : μ.Integrable f B) (hg : μ.Integrable g B) :
     ∫ᵛ x, f x - g x ∂[B; μ] = ∫ᵛ x, f x ∂[B; μ] - ∫ᵛ x, g x ∂[B; μ] := by
   by_cases hG : CompleteSpace G
   · simp only [integral, hG]
     exact setToFun_sub (dominatedFinMeasAdditive_cbmApplyMeasure μ B) hf hg
   · simp [integral, hG]
 
-theorem integral_sub {f g : X → E} (hf : μ.Integrable f B) (hg : μ.Integrable g B) :
+theorem integral_sub (hf : μ.Integrable f B) (hg : μ.Integrable g B) :
     ∫ᵛ x, (f - g) x ∂[B; μ] = ∫ᵛ x, f x ∂[B; μ] - ∫ᵛ x, g x ∂[B; μ] := integral_fun_sub hf hg
 
-variable (μ B) in
+variable (f μ B) in
 @[integral_simps]
-theorem integral_fun_smul (c : ℝ) (f : X → E) :
+theorem integral_fun_smul (c : ℝ) :
     ∫ᵛ x, c • f x ∂[B; μ] = c • ∫ᵛ x, f x ∂[B; μ] := by
   by_cases hG : CompleteSpace G
   · simp only [integral, hG]
     exact setToFun_smul (dominatedFinMeasAdditive_cbmApplyMeasure μ B) (by simp) c f
   · simp [integral, hG]
 
-variable (μ B) in
+variable (f μ B) in
+@[integral_simps]
+theorem integral_smul (c : ℝ) :
+    ∫ᵛ x, (c • f) x ∂[B; μ] = c • ∫ᵛ x, f x ∂[B; μ] := integral_fun_smul f μ B c
+
+end Function
+
+section VectorMeasure
+
+variable (f μ B) in
+@[simp]
+theorem integral_zero_vectorMeasure :
+    ∫ᵛ x, f x ∂[B; (0 : VectorMeasure X F)] = 0 := by
+  by_cases hG : CompleteSpace G
+  · simp only [integral, hG]
+    refine setToFun_measure_zero (dominatedFinMeasAdditive_cbmApplyMeasure 0 B) ?_
+    simp [variation_zero]
+  · simp [integral, hG]
+
+lemma integral_of_isEmpty [IsEmpty X] : ∫ᵛ x, f x ∂[B; μ] = 0 := by simp [eq_zero_of_isEmpty]
+
+theorem integral_add_vectorMeasure (hμ : μ.Integrable f B) (hν : ν.Integrable f B) :
+    ∫ᵛ x, f x ∂[B; μ + ν] = ∫ᵛ x, f x ∂[B; μ] + ∫ᵛ x, f x ∂[B; ν] := by
+  by_cases hG : CompleteSpace G
+  · simp only [integral, hG]
+    sorry
+  · simp [integral, hG]
+
+theorem integral_finsetSum_vectorMeasure {μ : ι → VectorMeasure X F}
+    {s : Finset ι} (hf : ∀ i ∈ s, (μ i).Integrable f B) :
+    ∫ᵛ x, f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ x, f x ∂[B; μ i] := by
+  sorry
+
+variable (f μ B) in
+@[integral_simps]
+theorem integral_neg_vectorMeasure :
+    ∫ᵛ x, f x ∂[B; -μ] = -∫ᵛ x, f x ∂[B; μ] := sorry
+
+theorem integral_sub_vectorMeasure (hμ : μ.Integrable f B) (hν : ν.Integrable f B) :
+    ∫ᵛ x, f x ∂[B; μ - ν] = ∫ᵛ x, f x ∂[B; μ] - ∫ᵛ x, f x ∂[B; ν] := by
+  by_cases hG : CompleteSpace G
+  · simp only [integral, hG]
+    sorry
+  · simp [integral, hG]
+
+theorem integral_smul_vectorMeasure (c : ℝ) :
+    ∫ᵛ x, f x ∂[B; c • μ] = c • ∫ᵛ x, f x ∂[B; μ] := by
+  by_cases hG : CompleteSpace G
+  · simp only [integral, hG]
+    sorry
+  · simp [integral, hG]
+
+end VectorMeasure
+
+section cbm
+
+variable (f μ) in
+@[simp]
+theorem integral_zero_cbm :
+    ∫ᵛ x, f x ∂[(0 : E →L[ℝ] F →L[ℝ] G); μ] = 0 := by
+  simp [integral]
+
+theorem integral_add_cbm (hB : μ.Integrable f B) (hC : μ.Integrable f C) :
+    ∫ᵛ x, f x ∂[B + C; μ] = ∫ᵛ x, f x ∂[B; μ] + ∫ᵛ x, f x ∂[C; μ] := by
+  by_cases hG : CompleteSpace G
+  · simp [integral, hG]
+    sorry
+  · simp [integral, hG]
+
+theorem integral_finsetSum_cbm {B : ι → E →L[ℝ] F →L[ℝ] G}
+    {s : Finset ι} (hf : ∀ i ∈ s, μ.Integrable f (B i)) :
+    ∫ᵛ x, f x ∂[∑ i ∈ s, B i; μ] = ∑ i ∈ s, ∫ᵛ x, f x ∂[B i; μ] := by
+  sorry
+
 @[integral_simps]
-theorem integral_smul (c : ℝ) (f : X → E) :
-    ∫ᵛ x, (c • f) x ∂[B; μ] = c • ∫ᵛ x, f x ∂[B; μ] := integral_fun_smul μ B c f
+theorem integral_neg_cbm :
+    ∫ᵛ x, f x ∂[-B; μ] = -∫ᵛ x, f x ∂[B; μ] := sorry
+
+theorem integral_sub_cbm (hB : μ.Integrable f B) (hC : μ.Integrable f C) :
+    ∫ᵛ x, f x ∂[B - C; μ] = ∫ᵛ x, f x ∂[B; μ] - ∫ᵛ x, f x ∂[C; μ] := by
+  by_cases hG : CompleteSpace G
+  · simp only [integral, hG]
+    sorry
+  · simp [integral, hG]
+
+theorem integral_smul_cbm (c : ℝ) :
+    ∫ᵛ x, f x ∂[c • B; μ] = c • ∫ᵛ x, f x ∂[B; μ] := by
+  by_cases hG : CompleteSpace G
+  · simp only [integral, hG]
+    sorry
+  · simp [integral, hG]
+
+end cbm
 
 end VectorMeasure
 

From b3d214db3755a2c1152c378099e4715e0f33b8ce Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Fri, 8 May 2026 14:56:57 -0400
Subject: [PATCH 02/24] update

---
 Mathlib/MeasureTheory/Integral/SetToL1.lean   | 47 +------------------
 .../MeasureTheory/VectorMeasure/Integral.lean | 10 +++-
 .../VectorMeasure/Variation/Basic.lean        |  7 +++
 3 files changed, 16 insertions(+), 48 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean
index a2c27024e349e8..0ab8147381aeb9 100644
--- a/Mathlib/MeasureTheory/Integral/SetToL1.lean
+++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean
@@ -984,52 +984,7 @@ theorem setToFun_add_measure {ν : Measure α} (hTμ : DominatedFinMeasAdditive
     (hTν : DominatedFinMeasAdditive ν T' C') (hμ : Integrable f μ) (hν : Integrable f ν) :
     setToFun (μ + ν) (T + T') (hTμ.add_measure μ ν hTν) f =
       setToFun μ T hTμ f + setToFun ν T' hTν f := by
-  have hfi := hμ.add_measure hν
-  have hTμ_add : DominatedFinMeasAdditive (μ + ν) T (max C 0) :=
-    (hTμ.mono_bound (le_max_left C 0)).of_measure_le (Measure.le_add_right le_rfl)
-      (le_max_right C 0)
-  have hTν_add : DominatedFinMeasAdditive (μ + ν) T' (max C' 0) :=
-    (hTν.mono_bound (le_max_left C' 0)).of_measure_le (Measure.le_add_left le_rfl)
-      (le_max_right C' 0)
-  calc
-    setToFun (μ + ν) (T + T') (hTμ.add_measure μ ν hTν) f =
-        setToFun (μ + ν) (T + T') (hTμ_add.add hTν_add) f :=
-      setToFun_congr_left _ _ rfl f
-    _ = setToFun (μ + ν) T hTμ_add f + setToFun (μ + ν) T' hTν_add f :=
-      setToFun_add_left hTμ_add hTν_add f
-    _ = setToFun μ T hTμ f + setToFun ν T' hTν f := by
-      rw [setToFun_congr_measure_of_add_right hTμ_add hTμ f hfi,
-        setToFun_congr_measure_of_add_left hTν_add hTν f hfi]
-
-theorem setToFun_finsetSum_measure {ι} (s : Finset ι) {μs : ι → Measure α}
-    {Ts : ι → Set α → E →L[ℝ] F} {Cs : ι → ℝ}
-    (hTs : ∀ i, DominatedFinMeasAdditive (μs i) (Ts i) (Cs i))
-    (hf : ∀ i ∈ s, Integrable f (μs i)) :
-    setToFun (∑ i ∈ s, μs i) (∑ i ∈ s, Ts i)
-        (DominatedFinMeasAdditive.finsetSum_measure s μs Ts Cs hTs) f =
-      ∑ i ∈ s, setToFun (μs i) (Ts i) (hTs i) f := by
-  classical
-  induction s using Finset.induction_on with
-  | empty =>
-      exact setToFun_zero_left
-  | insert i s his ih =>
-      have hrest : Integrable f (∑ j ∈ s, μs j) :=
-        integrable_finsetSum_measure.2 fun j hj => hf j (Finset.mem_insert_of_mem hj)
-      have h_add : DominatedFinMeasAdditive (∑ j ∈ insert i s, μs j) (∑ j ∈ insert i s, Ts j)
-          (max (Cs i) (∑ j ∈ s, max (Cs j) 0)) := by
-        simpa [Finset.sum_insert, his] using
-          ((hTs i).add_measure (μs i) (∑ j ∈ s, μs j)
-            (DominatedFinMeasAdditive.finsetSum_measure s μs Ts Cs hTs))
-      calc
-        setToFun (∑ j ∈ insert i s, μs j) (∑ j ∈ insert i s, Ts j)
-            (DominatedFinMeasAdditive.finsetSum_measure (insert i s) μs Ts Cs hTs) f =
-            setToFun (∑ j ∈ insert i s, μs j) (∑ j ∈ insert i s, Ts j) h_add f :=
-          setToFun_congr_left _ _ rfl f
-        _ = ∑ j ∈ insert i s, setToFun (μs j) (Ts j) (hTs j) f := by
-          simpa [Finset.sum_insert, his, ih fun j hj => hf j (Finset.mem_insert_of_mem hj)] using
-            setToFun_add_measure (hTs i)
-              (DominatedFinMeasAdditive.finsetSum_measure s μs Ts Cs hTs)
-              (hf i (Finset.mem_insert_self i s)) hrest
+  sorry
 
 theorem setToFun_top_smul_measure (hT : DominatedFinMeasAdditive (∞ • μ) T C) (f : α → E) :
     setToFun (∞ • μ) T hT f = 0 := by
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
index faa3da2ead410c..2ffc1fa499275e 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
@@ -324,8 +324,14 @@ theorem integral_sub_cbm (hB : μ.Integrable f B) (hC : μ.Integrable f C) :
 theorem integral_smul_cbm (c : ℝ) :
     ∫ᵛ x, f x ∂[c • B; μ] = c • ∫ᵛ x, f x ∂[B; μ] := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG]
-    sorry
+  · simp only [integral, hG, ↓reduceDIte, transpose_smul, coe_smul, ← setToFun_smul_left,
+      Real.norm_eq_abs, mul_one]
+    refine setToFun_congr_measure (ENNReal.ofReal |c|) (ENNReal.ofReal |c|)⁻¹
+      ?_ ?_ ?_ ?_ _ _ f
+    · sorry
+    · sorry
+    · sorry
+    · sorry
   · simp [integral, hG]
 
 end cbm
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
index e37a6277de2df1..59db0aaa8778a4 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
@@ -6,6 +6,7 @@ Authors: Oliver Butterley, Yoh Tanimoto
 module
 
 public import Mathlib.MeasureTheory.VectorMeasure.Variation.Defs
+public import Mathlib.Analysis.Normed.Module.Basic
 
 /-!
 # Properties of variation
@@ -111,6 +112,12 @@ variable (μ) in
 @[simp]
 lemma variation_neg : (-μ).variation = μ.variation := by simp [variation]
 
+variable [NormedSpace ℝ V]
+
+theorem variation_smul (c : ℝ) :
+    (c • μ).variation = ENNReal.ofReal |c| • μ.variation := by
+  sorry
+
 end NormedAddCommGroup
 
 end MeasureTheory.VectorMeasure

From 82d428f243b960906847336da73a76585e2bd473 Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Fri, 8 May 2026 15:23:55 -0400
Subject: [PATCH 03/24] Update FinMeasAdditive.lean

---
 .../Integral/FinMeasAdditive.lean             | 29 +++++--------------
 1 file changed, 8 insertions(+), 21 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
index dc12d039116d00..e1e6e8d6f8455f 100644
--- a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
+++ b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
@@ -176,11 +176,6 @@ theorem add (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditi
   rw [Pi.add_apply, add_mul]
   exact (norm_add_le _ _).trans (add_le_add (hT.2 s hs hμs) (hT'.2 s hs hμs))
 
-theorem mono_bound (hT : DominatedFinMeasAdditive μ T C) (hCC' : C ≤ C') :
-    DominatedFinMeasAdditive μ T C' :=
-  ⟨hT.1, fun s hs hμs =>
-    (hT.2 s hs hμs).trans (mul_le_mul_of_nonneg_right hCC' measureReal_nonneg)⟩
-
 theorem smul [SeminormedAddGroup 𝕜] [DistribSMul 𝕜 β] [IsBoundedSMul 𝕜 β]
     (hT : DominatedFinMeasAdditive μ T C) (c : 𝕜) :
     DominatedFinMeasAdditive μ (fun s => c • T s) (‖c‖ * C) := by
@@ -223,25 +218,17 @@ theorem add_measure_left {_ : MeasurableSpace α} (μ ν : Measure α)
     (hT : DominatedFinMeasAdditive ν T C) (hC : 0 ≤ C) : DominatedFinMeasAdditive (μ + ν) T C :=
   of_measure_le (Measure.le_add_left le_rfl) hT hC
 
-theorem finsetSum_measure {ι} {_ : MeasurableSpace α} (s : Finset ι) (μ : ι → Measure α)
-    (T : ι → Set α → β) (C : ι → ℝ)
-    (hT : ∀ i, DominatedFinMeasAdditive (μ i) (T i) (C i)) :
-    DominatedFinMeasAdditive (∑ i ∈ s, μ i) (∑ i ∈ s, T i)
-      (∑ i ∈ s, max (C i) 0) := by
+theorem finsetSum_measure {ι} {s : Finset ι} (hs : s.Nonempty) (μ : ι → Measure α)
+    (T : ι → Set α → β) (C : ι → ℝ) (hT : ∀ i, DominatedFinMeasAdditive (μ i) (T i) (C i)) :
+    DominatedFinMeasAdditive (∑ i ∈ s, μ i) (∑ i ∈ s, T i) (s.sup' hs C) := by
   classical
   induction s using Finset.induction_on with
-  | empty =>
-      simpa using (zero (0 : Measure α) (β := β) (C := 0) le_rfl)
+  | empty => grind
   | insert i s his ih =>
-      have h_nonneg : 0 ≤ ∑ j ∈ s, max (C j) 0 :=
-        Finset.sum_nonneg fun j _ => le_max_right _ _
-      have hle : max (C i) (∑ j ∈ s, max (C j) 0) ≤
-          ∑ j ∈ insert i s, max (C j) 0 := by
-        rw [Finset.sum_insert his]
-        exact max_le ((le_max_left _ _).trans (le_add_of_nonneg_right h_nonneg))
-          (le_add_of_nonneg_left (le_max_right _ _))
-      simpa [Finset.sum_insert, his] using
-        ((hT i).add_measure (μ i) (∑ j ∈ s, μ j) ih).mono_bound hle
+    by_cases hs' : s.Nonempty
+    · simpa [Finset.sum_insert, his, Finset.sup'_insert hs' C] using
+        (hT i).add_measure (μ i) (∑ j ∈ s, μ j) (ih hs')
+    · simp_all
 
 theorem of_smul_measure {c : ℝ≥0∞} (hc_ne_top : c ≠ ∞) (hT : DominatedFinMeasAdditive (c • μ) T C) :
     DominatedFinMeasAdditive μ T (c.toReal * C) := by

From c73ee93ea4ba96aa91d609de0d43257d5c847758 Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Fri, 8 May 2026 22:11:36 -0400
Subject: [PATCH 04/24] update

---
 .../Integral/FinMeasAdditive.lean             |  73 +++++++---
 Mathlib/MeasureTheory/Integral/SetToL1.lean   |  41 +++++-
 .../MeasureTheory/VectorMeasure/Basic.lean    |   4 +
 .../MeasureTheory/VectorMeasure/Integral.lean | 129 ++++++++++++++----
 4 files changed, 197 insertions(+), 50 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
index e1e6e8d6f8455f..f4c861c65afe6d 100644
--- a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
+++ b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
@@ -58,25 +58,13 @@ def FinMeasAdditive {β} [AddMonoid β] {_ : MeasurableSpace α} (μ : Measure 
 
 namespace FinMeasAdditive
 
-variable {β : Type*} [AddCommMonoid β] {T T' : Set α → β}
+variable {β : Type*} {T T' : Set α → β}
 
-theorem zero : FinMeasAdditive μ (0 : Set α → β) := fun _ _ _ _ _ _ _ => by simp
+section AddMonoid
 
-theorem add (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive μ T') :
-    FinMeasAdditive μ (T + T') := by
-  intro s t hs ht hμs hμt hst
-  simp only [hT s t hs ht hμs hμt hst, hT' s t hs ht hμs hμt hst, Pi.add_apply]
-  abel
+variable [AddMonoid β]
 
-theorem add_measure {ν : Measure α} (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive ν T') :
-    FinMeasAdditive (μ + ν) (T + T') := by
-  intro s t hms hmt hs ht hst
-  have hμs : μ s ≠ ∞ := ((Measure.le_add_right le_rfl s).trans_lt hs.lt_top).ne
-  have hμt : μ t ≠ ∞ := ((Measure.le_add_right le_rfl t).trans_lt ht.lt_top).ne
-  have hνs : ν s ≠ ∞ := ((Measure.le_add_left le_rfl s).trans_lt hs.lt_top).ne
-  have hνt : ν t ≠ ∞ := ((Measure.le_add_left le_rfl t).trans_lt ht.lt_top).ne
-  simp [hT s t hms hmt hμs hμt hst, hT' s t hms hmt hνs hνt hst]
-  abel
+theorem zero : FinMeasAdditive μ (0 : Set α → β) := fun _ _ _ _ _ _ _ => by simp
 
 theorem smul [DistribSMul 𝕜 β] (hT : FinMeasAdditive μ T) (c : 𝕜) :
     FinMeasAdditive μ fun s => c • T s := fun s t hs ht hμs hμt hst => by
@@ -112,6 +100,28 @@ theorem map_empty_eq_zero {β} [AddCancelMonoid β] {T : Set α → β} (hT : Fi
   nth_rw 1 [← add_zero (T ∅)] at hT
   exact (add_left_cancel hT).symm
 
+end AddMonoid
+
+section AddCommMonoid
+
+variable [AddCommMonoid β]
+
+theorem add (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive μ T') :
+    FinMeasAdditive μ (T + T') := by
+  intro s t hs ht hμs hμt hst
+  simp only [hT s t hs ht hμs hμt hst, hT' s t hs ht hμs hμt hst, Pi.add_apply]
+  abel
+
+theorem add_measure {ν : Measure α} (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive ν T') :
+    FinMeasAdditive (μ + ν) (T + T') := by
+  intro s t hms hmt hs ht hst
+  have hμs : μ s ≠ ∞ := ((Measure.le_add_right le_rfl s).trans_lt hs.lt_top).ne
+  have hμt : μ t ≠ ∞ := ((Measure.le_add_right le_rfl t).trans_lt ht.lt_top).ne
+  have hνs : ν s ≠ ∞ := ((Measure.le_add_left le_rfl s).trans_lt hs.lt_top).ne
+  have hνt : ν t ≠ ∞ := ((Measure.le_add_left le_rfl t).trans_lt ht.lt_top).ne
+  simp [hT s t hms hmt hμs hμt hst, hT' s t hms hmt hνs hνt hst]
+  abel
+
 theorem map_iUnion_fin_meas_set_eq_sum (T : Set α → β) (T_empty : T ∅ = 0)
     (h_add : FinMeasAdditive μ T) {ι} (S : ι → Set α) (sι : Finset ι)
     (hS_meas : ∀ i, MeasurableSet (S i)) (hSp : ∀ i ∈ sι, μ (S i) ≠ ∞)
@@ -140,6 +150,19 @@ theorem map_iUnion_fin_meas_set_eq_sum (T : Set α → β) (T_empty : T ∅ = 0)
     rw [← hai] at hi
     exact has hi
 
+end AddCommMonoid
+
+theorem neg [AddGroup β] (hT : FinMeasAdditive μ T) :
+    FinMeasAdditive μ (-T) := by
+  intro s t hs ht hμs hμt hst
+  have h_comm : T s + T t = T t + T s := by
+    rw [← hT s t hs ht hμs hμt hst, ← hT t s ht hs hμt hμs hst.symm, union_comm]
+  simp_all [Pi.neg_apply, hT s t hs ht hμs hμt hst, neg_add_rev]
+
+theorem sub [AddCommGroup β] (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive μ T') :
+    FinMeasAdditive μ (T - T') :=
+  sub_eq_add_neg T T' ▸ hT.add hT'.neg
+
 end FinMeasAdditive
 
 /-- A `FinMeasAdditive` set function whose norm on every set is less than the measure of the
@@ -170,12 +193,22 @@ theorem eq_zero {β : Type*} [NormedAddCommGroup β] {T : Set α → β} {C : 
     T s = 0 :=
   eq_zero_of_measure_zero hT hs (by simp only [Measure.coe_zero, Pi.zero_apply])
 
+theorem max_zero (hT : DominatedFinMeasAdditive μ T C) :
+    DominatedFinMeasAdditive μ T (max C 0) :=
+  ⟨hT.1, fun s hs hμs => (hT.2 s hs hμs).trans <|
+    mul_le_mul_of_nonneg_right (le_max_left C 0) measureReal_nonneg⟩
+
 theorem add (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') :
     DominatedFinMeasAdditive μ (T + T') (C + C') := by
   refine ⟨hT.1.add hT'.1, fun s hs hμs => ?_⟩
   rw [Pi.add_apply, add_mul]
   exact (norm_add_le _ _).trans (add_le_add (hT.2 s hs hμs) (hT'.2 s hs hμs))
 
+theorem neg (hT : DominatedFinMeasAdditive μ T C) :
+    DominatedFinMeasAdditive μ (-T) C := by
+  refine ⟨hT.1.neg, fun s hs hμs => ?_⟩
+  simpa only [Pi.neg_apply, norm_neg] using hT.2 s hs hμs
+
 theorem smul [SeminormedAddGroup 𝕜] [DistribSMul 𝕜 β] [IsBoundedSMul 𝕜 β]
     (hT : DominatedFinMeasAdditive μ T C) (c : 𝕜) :
     DominatedFinMeasAdditive μ (fun s => c • T s) (‖c‖ * C) := by
@@ -210,6 +243,11 @@ theorem add_measure {C' : ℝ} (μ ν : Measure α)
       · exact le_max_left C C'
       · exact le_max_right C C'
 
+theorem sub_measure {C' : ℝ} (μ ν : Measure α)
+    (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive ν T' C') :
+    DominatedFinMeasAdditive (μ + ν) (T - T') (max C C') :=
+  sub_eq_add_neg T T' ▸ hT.add_measure μ ν hT'.neg
+
 theorem add_measure_right {_ : MeasurableSpace α} (μ ν : Measure α)
     (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) : DominatedFinMeasAdditive (μ + ν) T C :=
   of_measure_le (Measure.le_add_right le_rfl) hT hC
@@ -226,8 +264,7 @@ theorem finsetSum_measure {ι} {s : Finset ι} (hs : s.Nonempty) (μ : ι → Me
   | empty => grind
   | insert i s his ih =>
     by_cases hs' : s.Nonempty
-    · simpa [Finset.sum_insert, his, Finset.sup'_insert hs' C] using
-        (hT i).add_measure (μ i) (∑ j ∈ s, μ j) (ih hs')
+    · simpa [his, Finset.sup'_insert hs' C] using (hT i).add_measure (μ i) (∑ j ∈ s, μ j) (ih hs')
     · simp_all
 
 theorem of_smul_measure {c : ℝ≥0∞} (hc_ne_top : c ≠ ∞) (hT : DominatedFinMeasAdditive (c • μ) T C) :
diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean
index 0ab8147381aeb9..13b7cdbe7c925d 100644
--- a/Mathlib/MeasureTheory/Integral/SetToL1.lean
+++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean
@@ -744,6 +744,10 @@ theorem setToFun_neg (hT : DominatedFinMeasAdditive μ T C) (f : α → E) :
   · rw [setToFun_undef hT hf, setToFun_undef hT, neg_zero]
     rwa [← integrable_neg_iff] at hf
 
+theorem setToFun_neg' (hT : DominatedFinMeasAdditive μ T C) (f : α → E) :
+    setToFun μ (-T) hT.neg f = -setToFun μ T hT f := by
+  simpa using setToFun_smul_left' hT hT.neg (-1) (by simp) f
+
 theorem setToFun_sub (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ)
     (hg : Integrable g μ) : setToFun μ T hT (f - g) = setToFun μ T hT f - setToFun μ T hT g := by
   rw [sub_eq_add_neg, sub_eq_add_neg, setToFun_add hT hf hg.neg, setToFun_neg hT g]
@@ -983,8 +987,41 @@ theorem setToFun_congr_measure_of_add_left {μ' : Measure α}
 theorem setToFun_add_measure {ν : Measure α} (hTμ : DominatedFinMeasAdditive μ T C)
     (hTν : DominatedFinMeasAdditive ν T' C') (hμ : Integrable f μ) (hν : Integrable f ν) :
     setToFun (μ + ν) (T + T') (hTμ.add_measure μ ν hTν) f =
-      setToFun μ T hTμ f + setToFun ν T' hTν f := by
-  sorry
+      setToFun μ T hTμ f + setToFun ν T' hTν f :=
+  have hTμ_add : DominatedFinMeasAdditive (μ + ν) T (max C 0) :=
+    hTμ.max_zero.add_measure_right μ ν (le_max_right C 0)
+  have hTν_add : DominatedFinMeasAdditive (μ + ν) T' (max C' 0) :=
+    hTν.max_zero.add_measure_left μ ν (le_max_right C' 0)
+  calc
+    _ = setToFun (μ + ν) T hTμ_add f + setToFun (μ + ν) T' hTν_add f :=
+      setToFun_add_left hTμ_add hTν_add f
+    _ = setToFun μ T hTμ f + setToFun ν T' hTν f := by
+      rw [setToFun_congr_measure_of_add_right hTμ_add hTμ f (hμ.add_measure hν),
+        setToFun_congr_measure_of_add_left hTν_add hTν f (hμ.add_measure hν)]
+
+theorem setToFun_sub_measure {ν : Measure α} (hTμ : DominatedFinMeasAdditive μ T C)
+    (hTν : DominatedFinMeasAdditive ν T' C') (hμ : Integrable f μ) (hν : Integrable f ν) :
+    setToFun (μ + ν) (T - T') (hTμ.sub_measure μ ν hTν) f =
+      setToFun μ T hTμ f - setToFun ν T' hTν f := by
+  simp [sub_eq_add_neg, setToFun_add_measure hTμ hTν.neg hμ hν, setToFun_neg' hTν]
+
+theorem setToFun_finsetSum_measure {ι} {s : Finset ι} (hs : s.Nonempty)
+    {μs : ι → Measure α} {Ts : ι → Set α → E →L[ℝ] F} {Cs : ι → ℝ}
+    (hTs : ∀ i, DominatedFinMeasAdditive (μs i) (Ts i) (Cs i))
+    (hf : ∀ i ∈ s, Integrable f (μs i)) :
+    setToFun (∑ i ∈ s, μs i) (∑ i ∈ s, Ts i)
+      (DominatedFinMeasAdditive.finsetSum_measure hs μs Ts Cs hTs) f =
+      ∑ i ∈ s, setToFun (μs i) (Ts i) (hTs i) f := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => grind
+  | insert i s his ih =>
+    by_cases hs' : s.Nonempty
+    · simpa [his, ih hs' fun j hj => hf j (Finset.mem_insert_of_mem hj)] using
+        setToFun_add_measure (hTs i) (DominatedFinMeasAdditive.finsetSum_measure hs' μs Ts Cs hTs)
+        (hf i (s.mem_insert_self i))
+        (integrable_finsetSum_measure.2 fun j hj => hf j (Finset.mem_insert_of_mem hj))
+    · simp_all
 
 theorem setToFun_top_smul_measure (hT : DominatedFinMeasAdditive (∞ • μ) T C) (f : α → E) :
     setToFun (∞ • μ) T hT f = 0 := by
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
index b60d0c6cbb9019..3a0e8232af8761 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
@@ -325,6 +325,10 @@ def coeFnAddMonoidHom : VectorMeasure α M →+ Set α → M where
   map_zero' := coe_zero
   map_add' := coe_add
 
+@[simp]
+theorem coe_finsetSum {ι} (I : Finset ι) (v : ι → VectorMeasure α M) :
+    ⇑(∑ i ∈ I, v i) = ∑ i ∈ I, ⇑(v i) := map_sum coeFnAddMonoidHom v I
+
 end AddCommMonoid
 
 section AddCommGroup
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
index 2ffc1fa499275e..09311fb73cabb4 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
@@ -154,8 +154,54 @@ theorem transpose_zero_cbm (μ : VectorMeasure X F) :
   simp [transpose]
 
 @[simp]
-theorem transpose_smul (c : ℝ) (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) :
-    μ.transpose (c • B) = c • (μ.transpose B) := by
+theorem transpose_add_vectorMeasure (μ ν : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) :
+    (μ + ν).transpose B = μ.transpose B + ν.transpose B := by
+  simp [transpose]
+
+@[simp]
+theorem transpose_add_cbm (μ : VectorMeasure X F) (B C : E →L[ℝ] F →L[ℝ] G) :
+    μ.transpose (B + C) = μ.transpose B + μ.transpose C := by
+  ext
+  simp [transpose]
+
+@[simp]
+theorem transpose_finsetSum_vectorMeasure (μ : ι → VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G)
+    (s : Finset ι) :
+    (∑ i ∈ s, μ i).transpose B = ∑ i ∈ s, (μ i).transpose B := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp
+  | insert i s his ih => simp [Finset.sum_insert, his, ih]
+
+@[simp]
+theorem transpose_finsetSum_cbm (μ : VectorMeasure X F) (B : ι → E →L[ℝ] F →L[ℝ] G) (s : Finset ι) :
+    μ.transpose (∑ i ∈ s, B i) = ∑ i ∈ s, μ.transpose (B i) := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp
+  | insert i s his ih => simp [Finset.sum_insert, his, ih]
+
+@[simp]
+theorem transpose_neg_vectorMeasure (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) :
+    (-μ).transpose B = - (μ.transpose B) := by
+  ext
+  simp [transpose]
+
+@[simp]
+theorem transpose_neg_cbm (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) :
+    μ.transpose (-B) = - (μ.transpose B) := by
+  ext
+  simp [transpose]
+
+@[simp]
+theorem transpose_sub_vectorMeasure (μ ν : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) :
+    (μ - ν).transpose B = μ.transpose B - ν.transpose B := by
+  ext
+  simp [transpose]
+
+@[simp]
+theorem transpose_sub_cbm (μ : VectorMeasure X F) (B C : E →L[ℝ] F →L[ℝ] G) :
+    μ.transpose (B - C) = μ.transpose B - μ.transpose C := by
   ext
   simp [transpose]
 
@@ -260,31 +306,46 @@ lemma integral_of_isEmpty [IsEmpty X] : ∫ᵛ x, f x ∂[B; μ] = 0 := by simp
 theorem integral_add_vectorMeasure (hμ : μ.Integrable f B) (hν : ν.Integrable f B) :
     ∫ᵛ x, f x ∂[B; μ + ν] = ∫ᵛ x, f x ∂[B; μ] + ∫ᵛ x, f x ∂[B; ν] := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG]
+  · simp only [integral, hG, ↓reduceDIte, transpose_add_vectorMeasure, coe_add,
+      transpose_eq_cbmApplyMeasure, ← setToFun_add_measure
+      (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
+      (dominatedFinMeasAdditive_cbmApplyMeasure ν B) hμ hν]
+    refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f
+      (hμ.add_measure hν)).symm
     sorry
   · simp [integral, hG]
 
 theorem integral_finsetSum_vectorMeasure {μ : ι → VectorMeasure X F}
     {s : Finset ι} (hf : ∀ i ∈ s, (μ i).Integrable f B) :
     ∫ᵛ x, f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ x, f x ∂[B; μ i] := by
-  sorry
+  by_cases hG : CompleteSpace G
+  · by_cases! hs : s.Nonempty
+    · simp only [integral, hG, ↓reduceDIte, transpose_finsetSum_vectorMeasure, coe_finsetSum,
+        transpose_eq_cbmApplyMeasure, ← setToFun_finsetSum_measure hs
+        (fun i ↦ dominatedFinMeasAdditive_cbmApplyMeasure (μ i) B) hf]
+      refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f
+        (integrable_finsetSum_measure.2 hf)).symm
+      sorry
+    · simp_all
+  · simp [integral, hG]
 
 variable (f μ B) in
 @[integral_simps]
 theorem integral_neg_vectorMeasure :
-    ∫ᵛ x, f x ∂[B; -μ] = -∫ᵛ x, f x ∂[B; μ] := sorry
+    ∫ᵛ x, f x ∂[B; -μ] = -∫ᵛ x, f x ∂[B; μ] := by
+  by_cases hG : CompleteSpace G
+  · simp [integral, hG, ← setToFun_neg']
+  · simp [integral, hG]
 
 theorem integral_sub_vectorMeasure (hμ : μ.Integrable f B) (hν : ν.Integrable f B) :
     ∫ᵛ x, f x ∂[B; μ - ν] = ∫ᵛ x, f x ∂[B; μ] - ∫ᵛ x, f x ∂[B; ν] := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG]
-    sorry
-  · simp [integral, hG]
-
-theorem integral_smul_vectorMeasure (c : ℝ) :
-    ∫ᵛ x, f x ∂[B; c • μ] = c • ∫ᵛ x, f x ∂[B; μ] := by
-  by_cases hG : CompleteSpace G
-  · simp only [integral, hG]
+  · simp only [integral, hG, ↓reduceDIte, transpose_sub_vectorMeasure, coe_sub,
+      transpose_eq_cbmApplyMeasure, ← setToFun_sub_measure
+      (dominatedFinMeasAdditive_cbmApplyMeasure μ B) (dominatedFinMeasAdditive_cbmApplyMeasure ν B)
+      hμ hν]
+    refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f
+       (hμ.add_measure hν)).symm
     sorry
   · simp [integral, hG]
 
@@ -301,39 +362,47 @@ theorem integral_zero_cbm :
 theorem integral_add_cbm (hB : μ.Integrable f B) (hC : μ.Integrable f C) :
     ∫ᵛ x, f x ∂[B + C; μ] = ∫ᵛ x, f x ∂[B; μ] + ∫ᵛ x, f x ∂[C; μ] := by
   by_cases hG : CompleteSpace G
-  · simp [integral, hG]
+  · simp only [integral, hG, ↓reduceDIte, transpose_add_cbm, coe_add, transpose_eq_cbmApplyMeasure,
+      ← setToFun_add_measure (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
+      (dominatedFinMeasAdditive_cbmApplyMeasure μ C) hB hC]
+    refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f
+      (hB.add_measure hC)).symm
     sorry
   · simp [integral, hG]
 
 theorem integral_finsetSum_cbm {B : ι → E →L[ℝ] F →L[ℝ] G}
     {s : Finset ι} (hf : ∀ i ∈ s, μ.Integrable f (B i)) :
     ∫ᵛ x, f x ∂[∑ i ∈ s, B i; μ] = ∑ i ∈ s, ∫ᵛ x, f x ∂[B i; μ] := by
-  sorry
+  by_cases hG : CompleteSpace G
+  · by_cases! hs : s.Nonempty
+    · simp only [integral, hG, ↓reduceDIte, transpose_finsetSum_cbm, coe_finsetSum,
+        transpose_eq_cbmApplyMeasure, ← setToFun_finsetSum_measure hs
+        (fun i ↦ dominatedFinMeasAdditive_cbmApplyMeasure μ (B i)) hf]
+      refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f
+        (integrable_finsetSum_measure.2 hf)).symm
+      sorry
+    · simp_all
+  · simp [integral, hG]
 
 @[integral_simps]
 theorem integral_neg_cbm :
-    ∫ᵛ x, f x ∂[-B; μ] = -∫ᵛ x, f x ∂[B; μ] := sorry
+    ∫ᵛ x, f x ∂[-B; μ] = -∫ᵛ x, f x ∂[B; μ] := by
+  by_cases hG : CompleteSpace G
+  · simp [integral, hG, ← setToFun_neg']
+  · simp [integral, hG]
 
 theorem integral_sub_cbm (hB : μ.Integrable f B) (hC : μ.Integrable f C) :
     ∫ᵛ x, f x ∂[B - C; μ] = ∫ᵛ x, f x ∂[B; μ] - ∫ᵛ x, f x ∂[C; μ] := by
   by_cases hG : CompleteSpace G
-  · simp only [integral, hG]
+  · simp only [integral, hG, ↓reduceDIte, transpose_sub_cbm, coe_sub,
+      transpose_eq_cbmApplyMeasure, ← setToFun_sub_measure
+      (dominatedFinMeasAdditive_cbmApplyMeasure μ B) (dominatedFinMeasAdditive_cbmApplyMeasure μ C)
+      hB hC]
+    refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f
+       (hB.add_measure hC)).symm
     sorry
   · simp [integral, hG]
 
-theorem integral_smul_cbm (c : ℝ) :
-    ∫ᵛ x, f x ∂[c • B; μ] = c • ∫ᵛ x, f x ∂[B; μ] := by
-  by_cases hG : CompleteSpace G
-  · simp only [integral, hG, ↓reduceDIte, transpose_smul, coe_smul, ← setToFun_smul_left,
-      Real.norm_eq_abs, mul_one]
-    refine setToFun_congr_measure (ENNReal.ofReal |c|) (ENNReal.ofReal |c|)⁻¹
-      ?_ ?_ ?_ ?_ _ _ f
-    · sorry
-    · sorry
-    · sorry
-    · sorry
-  · simp [integral, hG]
-
 end cbm
 
 end VectorMeasure

From fa70a41c5d04cff6eb6d7719d78a40df1c4b43ad Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Fri, 8 May 2026 22:14:18 -0400
Subject: [PATCH 05/24] Update Basic.lean

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

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
index 59db0aaa8778a4..e37a6277de2df1 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
@@ -6,7 +6,6 @@ Authors: Oliver Butterley, Yoh Tanimoto
 module
 
 public import Mathlib.MeasureTheory.VectorMeasure.Variation.Defs
-public import Mathlib.Analysis.Normed.Module.Basic
 
 /-!
 # Properties of variation
@@ -112,12 +111,6 @@ variable (μ) in
 @[simp]
 lemma variation_neg : (-μ).variation = μ.variation := by simp [variation]
 
-variable [NormedSpace ℝ V]
-
-theorem variation_smul (c : ℝ) :
-    (c • μ).variation = ENNReal.ofReal |c| • μ.variation := by
-  sorry
-
 end NormedAddCommGroup
 
 end MeasureTheory.VectorMeasure

From caa8ff87c021f49fd2c0b6d6eb4ac8b23f72f41d Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Fri, 8 May 2026 22:15:07 -0400
Subject: [PATCH 06/24] Update Integral.lean

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

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
index 09311fb73cabb4..6e4ff40e11e53c 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Yoh Tanimoto. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yoh Tanimoto
+Authors: Yoh Tanimoto, Yongxi Lin
 -/
 module
 

From 8a9255b32e091dc0d5360d224e809e8ec3c32ff2 Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Fri, 8 May 2026 22:21:24 -0400
Subject: [PATCH 07/24] Update Basic.lean

---
 .../MeasureTheory/VectorMeasure/Variation/Basic.lean | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
index e37a6277de2df1..09cf46d3708fd5 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
@@ -100,7 +100,7 @@ end Basic
 
 section NormedAddCommGroup
 
-variable [NormedAddCommGroup V] {μ : VectorMeasure X V}
+variable [NormedAddCommGroup V] {μ ν : VectorMeasure X V}
 
 theorem norm_measure_le_variation {E : Set X} (hE : μ.variation E ≠ ∞ := by finiteness) :
     ‖μ E‖ ≤ μ.variation.real E := by
@@ -111,6 +111,16 @@ variable (μ) in
 @[simp]
 lemma variation_neg : (-μ).variation = μ.variation := by simp [variation]
 
+lemma variation_add_le : (μ + ν).variation ≤ μ.variation + ν.variation := by
+  sorry
+
+lemma variation_sub_le : (μ - ν).variation ≤ μ.variation + ν.variation := by
+  grw [sub_eq_add_neg, variation_add_le, variation_neg]
+
+lemma variation_finsetSum_le {ι} (s : Finset ι) (μ : ι → VectorMeasure X V) :
+    (∑ i ∈ s, μ i).variation ≤ ∑ i ∈ s, (μ i).variation := by
+  sorry
+
 end NormedAddCommGroup
 
 end MeasureTheory.VectorMeasure

From 876d7340652fa2500f2849c52e14b540236b12ce Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Fri, 8 May 2026 22:49:21 -0400
Subject: [PATCH 08/24] finishes proof

---
 .../MeasureTheory/VectorMeasure/Integral.lean | 36 +++++++++----------
 .../VectorMeasure/Variation/Basic.lean        | 16 +++++++--
 2 files changed, 32 insertions(+), 20 deletions(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
index 6e4ff40e11e53c..20b936b6e460db 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
@@ -310,9 +310,9 @@ theorem integral_add_vectorMeasure (hμ : μ.Integrable f B) (hν : ν.Integrabl
       transpose_eq_cbmApplyMeasure, ← setToFun_add_measure
       (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
       (dominatedFinMeasAdditive_cbmApplyMeasure ν B) hμ hν]
-    refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f
-      (hμ.add_measure hν)).symm
-    sorry
+    refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f ?_).symm
+    · simpa using variation_add_le
+    · exact hμ.add_measure hν
   · simp [integral, hG]
 
 theorem integral_finsetSum_vectorMeasure {μ : ι → VectorMeasure X F}
@@ -323,9 +323,9 @@ theorem integral_finsetSum_vectorMeasure {μ : ι → VectorMeasure X F}
     · simp only [integral, hG, ↓reduceDIte, transpose_finsetSum_vectorMeasure, coe_finsetSum,
         transpose_eq_cbmApplyMeasure, ← setToFun_finsetSum_measure hs
         (fun i ↦ dominatedFinMeasAdditive_cbmApplyMeasure (μ i) B) hf]
-      refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f
-        (integrable_finsetSum_measure.2 hf)).symm
-      sorry
+      refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f ?_).symm
+      · simpa using variation_finsetSum_le s _
+      · exact integrable_finsetSum_measure.2 hf
     · simp_all
   · simp [integral, hG]
 
@@ -344,9 +344,9 @@ theorem integral_sub_vectorMeasure (hμ : μ.Integrable f B) (hν : ν.Integrabl
       transpose_eq_cbmApplyMeasure, ← setToFun_sub_measure
       (dominatedFinMeasAdditive_cbmApplyMeasure μ B) (dominatedFinMeasAdditive_cbmApplyMeasure ν B)
       hμ hν]
-    refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f
-       (hμ.add_measure hν)).symm
-    sorry
+    refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f ?_).symm
+    · simpa using variation_sub_le
+    · exact hμ.add_measure hν
   · simp [integral, hG]
 
 end VectorMeasure
@@ -365,9 +365,9 @@ theorem integral_add_cbm (hB : μ.Integrable f B) (hC : μ.Integrable f C) :
   · simp only [integral, hG, ↓reduceDIte, transpose_add_cbm, coe_add, transpose_eq_cbmApplyMeasure,
       ← setToFun_add_measure (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
       (dominatedFinMeasAdditive_cbmApplyMeasure μ C) hB hC]
-    refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f
-      (hB.add_measure hC)).symm
-    sorry
+    refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f ?_).symm
+    · simpa using variation_add_le
+    · exact hB.add_measure hC
   · simp [integral, hG]
 
 theorem integral_finsetSum_cbm {B : ι → E →L[ℝ] F →L[ℝ] G}
@@ -378,9 +378,9 @@ theorem integral_finsetSum_cbm {B : ι → E →L[ℝ] F →L[ℝ] G}
     · simp only [integral, hG, ↓reduceDIte, transpose_finsetSum_cbm, coe_finsetSum,
         transpose_eq_cbmApplyMeasure, ← setToFun_finsetSum_measure hs
         (fun i ↦ dominatedFinMeasAdditive_cbmApplyMeasure μ (B i)) hf]
-      refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f
-        (integrable_finsetSum_measure.2 hf)).symm
-      sorry
+      refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f ?_).symm
+      · simpa using variation_finsetSum_le s _
+      · exact integrable_finsetSum_measure.2 hf
     · simp_all
   · simp [integral, hG]
 
@@ -398,9 +398,9 @@ theorem integral_sub_cbm (hB : μ.Integrable f B) (hC : μ.Integrable f C) :
       transpose_eq_cbmApplyMeasure, ← setToFun_sub_measure
       (dominatedFinMeasAdditive_cbmApplyMeasure μ B) (dominatedFinMeasAdditive_cbmApplyMeasure μ C)
       hB hC]
-    refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f
-       (hB.add_measure hC)).symm
-    sorry
+    refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f ?_).symm
+    · simpa using variation_sub_le
+    · exact hB.add_measure hC
   · simp [integral, hG]
 
 end cbm
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
index 09cf46d3708fd5..e4b0f92a010b26 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean
@@ -112,14 +112,26 @@ variable (μ) in
 lemma variation_neg : (-μ).variation = μ.variation := by simp [variation]
 
 lemma variation_add_le : (μ + ν).variation ≤ μ.variation + ν.variation := by
-  sorry
+  refine Measure.le_iff.2 fun s hs ↦ ?_
+  simp only [variation_apply, preVariation_apply, Measure.add_apply, ennrealToMeasure_apply hs,
+    ennrealPreVariation_apply, preVariationFun, hs, ↓reduceDIte]
+  refine iSup_le fun P ↦ ?_
+  calc
+  _ ≤ ∑ p ∈ P.parts, (‖μ p‖ₑ + ‖ν p‖ₑ) := Finset.sum_le_sum fun p _ ↦ enorm_add_le (μ p) (ν p)
+  _ = (∑ p ∈ P.parts, ‖μ p‖ₑ) + ∑ p ∈ P.parts, ‖ν p‖ₑ := by rw [Finset.sum_add_distrib]
+  _ ≤ _ := add_le_add (le_iSup_of_le P le_rfl) (le_iSup_of_le P le_rfl)
 
 lemma variation_sub_le : (μ - ν).variation ≤ μ.variation + ν.variation := by
   grw [sub_eq_add_neg, variation_add_le, variation_neg]
 
 lemma variation_finsetSum_le {ι} (s : Finset ι) (μ : ι → VectorMeasure X V) :
     (∑ i ∈ s, μ i).variation ≤ ∑ i ∈ s, (μ i).variation := by
-  sorry
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp
+  | insert i s his ih =>
+    simpa [Finset.sum_insert his] using
+      variation_add_le.trans (add_le_add_right ih ((μ i).variation))
 
 end NormedAddCommGroup
 

From 345914ecde32795e9721f137eb8c6f778d12ed68 Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Sun, 17 May 2026 08:57:40 -0400
Subject: [PATCH 09/24] Update FinMeasAdditive.lean

---
 .../Integral/FinMeasAdditive.lean             | 20 +++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
index f4c861c65afe6d..07fac9ec65166b 100644
--- a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
+++ b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
@@ -74,6 +74,16 @@ theorem of_eq_top_imp_eq_top {μ' : Measure α} (h : ∀ s, MeasurableSet s →
     (hT : FinMeasAdditive μ T) : FinMeasAdditive μ' T := fun s t hs ht hμ's hμ't hst =>
   hT s t hs ht (mt (h s hs) hμ's) (mt (h t ht) hμ't) hst
 
+theorem add_right_measure {ν : Measure α} (hT : FinMeasAdditive μ T) :
+    FinMeasAdditive (μ + ν) T :=
+  hT.of_eq_top_imp_eq_top fun s _ hμs =>
+    top_unique <| hμs.symm.trans_le (Measure.le_add_right le_rfl s)
+
+theorem add_left_measure {ν : Measure α} (hT : FinMeasAdditive μ T) :
+    FinMeasAdditive (ν + μ) T :=
+  hT.of_eq_top_imp_eq_top fun s _ hμs =>
+    top_unique <| hμs.symm.trans_le (Measure.le_add_left le_rfl s)
+
 theorem of_smul_measure {c : ℝ≥0∞} (hc_ne_top : c ≠ ∞) (hT : FinMeasAdditive (c • μ) T) :
     FinMeasAdditive μ T := by
   refine of_eq_top_imp_eq_top (fun s _ hμs => ?_) hT
@@ -113,14 +123,8 @@ theorem add (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive μ T') :
   abel
 
 theorem add_measure {ν : Measure α} (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive ν T') :
-    FinMeasAdditive (μ + ν) (T + T') := by
-  intro s t hms hmt hs ht hst
-  have hμs : μ s ≠ ∞ := ((Measure.le_add_right le_rfl s).trans_lt hs.lt_top).ne
-  have hμt : μ t ≠ ∞ := ((Measure.le_add_right le_rfl t).trans_lt ht.lt_top).ne
-  have hνs : ν s ≠ ∞ := ((Measure.le_add_left le_rfl s).trans_lt hs.lt_top).ne
-  have hνt : ν t ≠ ∞ := ((Measure.le_add_left le_rfl t).trans_lt ht.lt_top).ne
-  simp [hT s t hms hmt hμs hμt hst, hT' s t hms hmt hνs hνt hst]
-  abel
+    FinMeasAdditive (μ + ν) (T + T') :=
+  hT.add_right_measure.add (hT'.add_left_measure)
 
 theorem map_iUnion_fin_meas_set_eq_sum (T : Set α → β) (T_empty : T ∅ = 0)
     (h_add : FinMeasAdditive μ T) {ι} (S : ι → Set α) (sι : Finset ι)

From a8fe7e5e0cf2ffa2dc4eca6748b1fc20af2cf729 Mon Sep 17 00:00:00 2001
From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com>
Date: Sun, 24 May 2026 16:41:10 -0400
Subject: [PATCH 10/24] Apply suggestion from @EtienneC30

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
---
 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 1bdcfd8bc37e3e..c94fec09694a7b 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
@@ -288,7 +288,7 @@ lemma apply_eq_zero_of_isEmpty [IsEmpty α] (μ : VectorMeasure α M) (s : Set 
   simp [eq_empty_of_isEmpty s]
 
 instance instSubsingleton [IsEmpty α] : Subsingleton (VectorMeasure α M) :=
-  ⟨fun μ ν => by ext1 s _; rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]⟩
+  ⟨fun μ ν => by ext; rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]⟩
 
 theorem eq_zero_of_isEmpty [IsEmpty α] (μ : VectorMeasure α M) : μ = 0 :=
   Subsingleton.elim μ 0

From 36297d30c9a6794c30f6676d38035852e712a884 Mon Sep 17 00:00:00 2001
From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com>
Date: Sun, 24 May 2026 16:41:24 -0400
Subject: [PATCH 11/24] Apply suggestion from @EtienneC30

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
---
 Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
index 66d80474630fa3..4ba0eb54e10527 100644
--- a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
+++ b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
@@ -161,7 +161,7 @@ theorem neg [AddGroup β] (hT : FinMeasAdditive μ T) :
   intro s t hs ht hμs hμt hst
   have h_comm : T s + T t = T t + T s := by
     rw [← hT s t hs ht hμs hμt hst, ← hT t s ht hs hμt hμs hst.symm, union_comm]
-  simp_all [Pi.neg_apply, hT s t hs ht hμs hμt hst, neg_add_rev]
+  simp_all [hT s t hs ht hμs hμt hst, neg_add_rev]
 
 theorem sub [AddCommGroup β] (hT : FinMeasAdditive μ T) (hT' : FinMeasAdditive μ T') :
     FinMeasAdditive μ (T - T') :=

From da471eccaf1f163a6f3cd4e2bc0f2e6451f2c5fe Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Sun, 24 May 2026 16:47:56 -0400
Subject: [PATCH 12/24] nontriviality

---
 Mathlib/MeasureTheory/Measure/MeasureSpace.lean | 1 +
 Mathlib/MeasureTheory/VectorMeasure/Basic.lean  | 3 ++-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index dfdbb0f4299ba0..a01264c58a03f6 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -853,6 +853,7 @@ lemma apply_eq_zero_of_isEmpty [IsEmpty α] {_ : MeasurableSpace α} (μ : Measu
 instance instSubsingleton [IsEmpty α] {m : MeasurableSpace α} : Subsingleton (Measure α) :=
   ⟨fun μ ν => by ext1 s _; rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]⟩
 
+@[nontriviality]
 theorem eq_zero_of_isEmpty [IsEmpty α] {_m : MeasurableSpace α} (μ : Measure α) : μ = 0 :=
   Subsingleton.elim μ 0
 
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
index c94fec09694a7b..4974567cc92ada 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
@@ -287,9 +287,10 @@ lemma apply_eq_zero_of_isEmpty [IsEmpty α] (μ : VectorMeasure α M) (s : Set 
     μ s = 0 := by
   simp [eq_empty_of_isEmpty s]
 
-instance instSubsingleton [IsEmpty α] : Subsingleton (VectorMeasure α M) :=
+instance [IsEmpty α] : Subsingleton (VectorMeasure α M) :=
   ⟨fun μ ν => by ext; rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]⟩
 
+@[nontriviality]
 theorem eq_zero_of_isEmpty [IsEmpty α] (μ : VectorMeasure α M) : μ = 0 :=
   Subsingleton.elim μ 0
 

From fd50c1d3d2440ccb796e0cbe1da17f11784393e4 Mon Sep 17 00:00:00 2001
From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com>
Date: Sun, 24 May 2026 16:54:45 -0400
Subject: [PATCH 13/24] Apply suggestion from @EtienneC30

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
---
 Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
index 4ba0eb54e10527..d400e6c0382463 100644
--- a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
+++ b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
@@ -209,9 +209,8 @@ theorem add (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditi
   exact (norm_add_le _ _).trans (add_le_add (hT.2 s hs hμs) (hT'.2 s hs hμs))
 
 theorem neg (hT : DominatedFinMeasAdditive μ T C) :
-    DominatedFinMeasAdditive μ (-T) C := by
-  refine ⟨hT.1.neg, fun s hs hμs => ?_⟩
-  simpa only [Pi.neg_apply, norm_neg] using hT.2 s hs hμs
+    DominatedFinMeasAdditive μ (-T) C :=
+  ⟨hT.1.neg, fun s hs hμs => by simpa using hT.2 s hs hμs⟩
 
 theorem smul [SeminormedAddGroup 𝕜] [DistribSMul 𝕜 β] [IsBoundedSMul 𝕜 β]
     (hT : DominatedFinMeasAdditive μ T C) (c : 𝕜) :

From d161eaf9636c22629c8ee0a4d0adfc86ac8a1074 Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Sun, 24 May 2026 17:23:17 -0400
Subject: [PATCH 14/24] Finset.Nonempty.cons_induction

---
 .../Integral/FinMeasAdditive.lean             | 11 ++++------
 Mathlib/MeasureTheory/Integral/SetToL1.lean   | 22 +++++++++----------
 2 files changed, 14 insertions(+), 19 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
index 4ba0eb54e10527..e1b17f2ab6174d 100644
--- a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
+++ b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
@@ -263,13 +263,10 @@ theorem add_measure_left {_ : MeasurableSpace α} (μ ν : Measure α)
 theorem finsetSum_measure {ι} {s : Finset ι} (hs : s.Nonempty) (μ : ι → Measure α)
     (T : ι → Set α → β) (C : ι → ℝ) (hT : ∀ i, DominatedFinMeasAdditive (μ i) (T i) (C i)) :
     DominatedFinMeasAdditive (∑ i ∈ s, μ i) (∑ i ∈ s, T i) (s.sup' hs C) := by
-  classical
-  induction s using Finset.induction_on with
-  | empty => grind
-  | insert i s his ih =>
-    by_cases hs' : s.Nonempty
-    · simpa [his, Finset.sup'_insert hs' C] using (hT i).add_measure (μ i) (∑ j ∈ s, μ j) (ih hs')
-    · simp_all
+  induction hs using Finset.Nonempty.cons_induction with
+  | singleton i => simp_all
+  | @cons i s his hs' ih =>
+    simpa [his, Finset.sup'_cons hs' C] using (hT i).add_measure (μ i) (∑ j ∈ s, μ j) ih
 
 theorem of_smul_measure {c : ℝ≥0∞} (hc_ne_top : c ≠ ∞) (hT : DominatedFinMeasAdditive (c • μ) T C) :
     DominatedFinMeasAdditive μ T (c.toReal * C) := by
diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean
index 695049e418ee1b..222ac5d6da2ceb 100644
--- a/Mathlib/MeasureTheory/Integral/SetToL1.lean
+++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean
@@ -1103,8 +1103,9 @@ theorem setToFun_add_measure {ν : Measure α} (hTμ : DominatedFinMeasAdditive
   have hTν_add : DominatedFinMeasAdditive (μ + ν) T' (max C' 0) :=
     hTν.max_zero.add_measure_left μ ν (le_max_right C' 0)
   calc
-    _ = setToFun (μ + ν) T hTμ_add f + setToFun (μ + ν) T' hTν_add f :=
-      setToFun_add_left hTμ_add hTν_add f
+    setToFun (μ + ν) (T + T') (hTμ.add_measure μ ν hTν) f =
+      setToFun (μ + ν) T hTμ_add f + setToFun (μ + ν) T' hTν_add f :=
+        setToFun_add_left hTμ_add hTν_add f
     _ = setToFun μ T hTμ f + setToFun ν T' hTν f := by
       rw [setToFun_congr_measure_of_add_right hTμ_add hTμ f (hμ.add_measure hν),
         setToFun_congr_measure_of_add_left hTν_add hTν f (hμ.add_measure hν)]
@@ -1122,16 +1123,13 @@ theorem setToFun_finsetSum_measure {ι} {s : Finset ι} (hs : s.Nonempty)
     setToFun (∑ i ∈ s, μs i) (∑ i ∈ s, Ts i)
       (DominatedFinMeasAdditive.finsetSum_measure hs μs Ts Cs hTs) f =
       ∑ i ∈ s, setToFun (μs i) (Ts i) (hTs i) f := by
-  classical
-  induction s using Finset.induction_on with
-  | empty => grind
-  | insert i s his ih =>
-    by_cases hs' : s.Nonempty
-    · simpa [his, ih hs' fun j hj => hf j (Finset.mem_insert_of_mem hj)] using
-        setToFun_add_measure (hTs i) (DominatedFinMeasAdditive.finsetSum_measure hs' μs Ts Cs hTs)
-        (hf i (s.mem_insert_self i))
-        (integrable_finsetSum_measure.2 fun j hj => hf j (Finset.mem_insert_of_mem hj))
-    · simp_all
+  induction hs using Finset.Nonempty.cons_induction with
+  | singleton i => simp
+  | @cons i s his hs' ih =>
+    simpa [his, ih fun j hj => hf j (Finset.mem_cons_of_mem hj)] using
+      setToFun_add_measure (hTs i) (DominatedFinMeasAdditive.finsetSum_measure hs' μs Ts Cs hTs)
+      (hf i (Finset.mem_cons_self i s))
+      (integrable_finsetSum_measure.2 fun j hj => hf j (Finset.mem_cons_of_mem hj))
 
 theorem setToFun_top_smul_measure (hT : DominatedFinMeasAdditive (∞ • μ) T C) (f : α → E) :
     setToFun (∞ • μ) T hT f = 0 := by

From 893ac2bde613ca831ac0c8543044fc2170617875 Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Sun, 24 May 2026 18:06:49 -0400
Subject: [PATCH 15/24] address comment

---
 .../Integral/FinMeasAdditive.lean              |  7 +++----
 Mathlib/MeasureTheory/Integral/SetToL1.lean    | 18 +++++++++---------
 2 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
index 37412e28161eaa..6fac9a1fe55d27 100644
--- a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
+++ b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
@@ -197,10 +197,9 @@ theorem eq_zero {β : Type*} [NormedAddCommGroup β] {T : Set α → β} {C : 
     T s = 0 :=
   eq_zero_of_measure_zero hT hs (by simp only [Measure.coe_zero, Pi.zero_apply])
 
-theorem max_zero (hT : DominatedFinMeasAdditive μ T C) :
-    DominatedFinMeasAdditive μ T (max C 0) :=
-  ⟨hT.1, fun s hs hμs => (hT.2 s hs hμs).trans <|
-    mul_le_mul_of_nonneg_right (le_max_left C 0) measureReal_nonneg⟩
+theorem le (hT : DominatedFinMeasAdditive μ T C) (hC : C ≤ C') :
+    DominatedFinMeasAdditive μ T C' :=
+  ⟨hT.1, fun s hs hμs => (hT.2 s hs hμs).trans <| mul_le_mul_of_nonneg_right hC measureReal_nonneg⟩
 
 theorem add (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') :
     DominatedFinMeasAdditive μ (T + T') (C + C') := by
diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean
index 222ac5d6da2ceb..1020f6879b8d51 100644
--- a/Mathlib/MeasureTheory/Integral/SetToL1.lean
+++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean
@@ -1099,9 +1099,9 @@ theorem setToFun_add_measure {ν : Measure α} (hTμ : DominatedFinMeasAdditive
     setToFun (μ + ν) (T + T') (hTμ.add_measure μ ν hTν) f =
       setToFun μ T hTμ f + setToFun ν T' hTν f :=
   have hTμ_add : DominatedFinMeasAdditive (μ + ν) T (max C 0) :=
-    hTμ.max_zero.add_measure_right μ ν (le_max_right C 0)
+    (hTμ.le (le_max_left C 0)).add_measure_right μ ν (le_max_right C 0)
   have hTν_add : DominatedFinMeasAdditive (μ + ν) T' (max C' 0) :=
-    hTν.max_zero.add_measure_left μ ν (le_max_right C' 0)
+    (hTν.le (le_max_left C' 0)).add_measure_left μ ν (le_max_right C' 0)
   calc
     setToFun (μ + ν) (T + T') (hTμ.add_measure μ ν hTν) f =
       setToFun (μ + ν) T hTμ_add f + setToFun (μ + ν) T' hTν_add f :=
@@ -1117,17 +1117,17 @@ theorem setToFun_sub_measure {ν : Measure α} (hTμ : DominatedFinMeasAdditive
   simp [sub_eq_add_neg, setToFun_add_measure hTμ hTν.neg hμ hν, setToFun_neg' hTν]
 
 theorem setToFun_finsetSum_measure {ι} {s : Finset ι} (hs : s.Nonempty)
-    {μs : ι → Measure α} {Ts : ι → Set α → E →L[ℝ] F} {Cs : ι → ℝ}
-    (hTs : ∀ i, DominatedFinMeasAdditive (μs i) (Ts i) (Cs i))
-    (hf : ∀ i ∈ s, Integrable f (μs i)) :
-    setToFun (∑ i ∈ s, μs i) (∑ i ∈ s, Ts i)
-      (DominatedFinMeasAdditive.finsetSum_measure hs μs Ts Cs hTs) f =
-      ∑ i ∈ s, setToFun (μs i) (Ts i) (hTs i) f := by
+    {μ : ι → Measure α} {T : ι → Set α → E →L[ℝ] F} {C : ι → ℝ}
+    (hTs : ∀ i, DominatedFinMeasAdditive (μ i) (T i) (C i))
+    (hf : ∀ i ∈ s, Integrable f (μ i)) :
+    setToFun (∑ i ∈ s, μ i) (∑ i ∈ s, T i)
+      (DominatedFinMeasAdditive.finsetSum_measure hs μ T C hTs) f =
+      ∑ i ∈ s, setToFun (μ i) (T i) (hTs i) f := by
   induction hs using Finset.Nonempty.cons_induction with
   | singleton i => simp
   | @cons i s his hs' ih =>
     simpa [his, ih fun j hj => hf j (Finset.mem_cons_of_mem hj)] using
-      setToFun_add_measure (hTs i) (DominatedFinMeasAdditive.finsetSum_measure hs' μs Ts Cs hTs)
+      setToFun_add_measure (hTs i) (DominatedFinMeasAdditive.finsetSum_measure hs' μ T C hTs)
       (hf i (Finset.mem_cons_self i s))
       (integrable_finsetSum_measure.2 fun j hj => hf j (Finset.mem_cons_of_mem hj))
 

From dc41fb6487a4ff5318fb78ac0477da9871ff6e80 Mon Sep 17 00:00:00 2001
From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com>
Date: Tue, 26 May 2026 10:17:37 -0400
Subject: [PATCH 16/24] Update
 Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
---
 Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
index 6fac9a1fe55d27..f59dfd6d9bf24e 100644
--- a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
+++ b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
@@ -197,7 +197,7 @@ theorem eq_zero {β : Type*} [NormedAddCommGroup β] {T : Set α → β} {C : 
     T s = 0 :=
   eq_zero_of_measure_zero hT hs (by simp only [Measure.coe_zero, Pi.zero_apply])
 
-theorem le (hT : DominatedFinMeasAdditive μ T C) (hC : C ≤ C') :
+theorem of_le (hT : DominatedFinMeasAdditive μ T C) (hC : C ≤ C') :
     DominatedFinMeasAdditive μ T C' :=
   ⟨hT.1, fun s hs hμs => (hT.2 s hs hμs).trans <| mul_le_mul_of_nonneg_right hC measureReal_nonneg⟩
 

From ab8b3def637e23a85343e112d4f9f644aaff0510 Mon Sep 17 00:00:00 2001
From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com>
Date: Tue, 26 May 2026 10:17:51 -0400
Subject: [PATCH 17/24] Update
 Mathlib/MeasureTheory/VectorMeasure/Integral.lean

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
---
 Mathlib/MeasureTheory/VectorMeasure/Integral.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
index 20b936b6e460db..dd96c4b446ace7 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
@@ -396,8 +396,8 @@ theorem integral_sub_cbm (hB : μ.Integrable f B) (hC : μ.Integrable f C) :
   by_cases hG : CompleteSpace G
   · simp only [integral, hG, ↓reduceDIte, transpose_sub_cbm, coe_sub,
       transpose_eq_cbmApplyMeasure, ← setToFun_sub_measure
-      (dominatedFinMeasAdditive_cbmApplyMeasure μ B) (dominatedFinMeasAdditive_cbmApplyMeasure μ C)
-      hB hC]
+        (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
+        (dominatedFinMeasAdditive_cbmApplyMeasure μ C) hB hC]
     refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f ?_).symm
     · simpa using variation_sub_le
     · exact hB.add_measure hC

From 4d206f0563a76fbed84a58209e3f6a99a148bb64 Mon Sep 17 00:00:00 2001
From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com>
Date: Tue, 26 May 2026 10:18:01 -0400
Subject: [PATCH 18/24] Update
 Mathlib/MeasureTheory/VectorMeasure/Integral.lean

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
---
 Mathlib/MeasureTheory/VectorMeasure/Integral.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
index dd96c4b446ace7..fb60e130b8a154 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
@@ -377,7 +377,7 @@ theorem integral_finsetSum_cbm {B : ι → E →L[ℝ] F →L[ℝ] G}
   · by_cases! hs : s.Nonempty
     · simp only [integral, hG, ↓reduceDIte, transpose_finsetSum_cbm, coe_finsetSum,
         transpose_eq_cbmApplyMeasure, ← setToFun_finsetSum_measure hs
-        (fun i ↦ dominatedFinMeasAdditive_cbmApplyMeasure μ (B i)) hf]
+          (fun i ↦ dominatedFinMeasAdditive_cbmApplyMeasure μ (B i)) hf]
       refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f ?_).symm
       · simpa using variation_finsetSum_le s _
       · exact integrable_finsetSum_measure.2 hf

From 6bd29bf32700679df1a682cbc69e152b1446b41d Mon Sep 17 00:00:00 2001
From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com>
Date: Tue, 26 May 2026 10:18:12 -0400
Subject: [PATCH 19/24] Update
 Mathlib/MeasureTheory/VectorMeasure/Integral.lean

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
---
 Mathlib/MeasureTheory/VectorMeasure/Integral.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
index fb60e130b8a154..ec62c183ce4f61 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
@@ -364,7 +364,7 @@ theorem integral_add_cbm (hB : μ.Integrable f B) (hC : μ.Integrable f C) :
   by_cases hG : CompleteSpace G
   · simp only [integral, hG, ↓reduceDIte, transpose_add_cbm, coe_add, transpose_eq_cbmApplyMeasure,
       ← setToFun_add_measure (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
-      (dominatedFinMeasAdditive_cbmApplyMeasure μ C) hB hC]
+        (dominatedFinMeasAdditive_cbmApplyMeasure μ C) hB hC]
     refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f ?_).symm
     · simpa using variation_add_le
     · exact hB.add_measure hC

From 0c19b006a53ac6d9a521f682651f0dc24ab8995e Mon Sep 17 00:00:00 2001
From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com>
Date: Tue, 26 May 2026 10:18:25 -0400
Subject: [PATCH 20/24] Update
 Mathlib/MeasureTheory/VectorMeasure/Integral.lean

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
---
 Mathlib/MeasureTheory/VectorMeasure/Integral.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
index ec62c183ce4f61..9cc5907b6ca515 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
@@ -342,8 +342,8 @@ theorem integral_sub_vectorMeasure (hμ : μ.Integrable f B) (hν : ν.Integrabl
   by_cases hG : CompleteSpace G
   · simp only [integral, hG, ↓reduceDIte, transpose_sub_vectorMeasure, coe_sub,
       transpose_eq_cbmApplyMeasure, ← setToFun_sub_measure
-      (dominatedFinMeasAdditive_cbmApplyMeasure μ B) (dominatedFinMeasAdditive_cbmApplyMeasure ν B)
-      hμ hν]
+        (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
+        (dominatedFinMeasAdditive_cbmApplyMeasure ν B) hμ hν]
     refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f ?_).symm
     · simpa using variation_sub_le
     · exact hμ.add_measure hν

From 69b3ac3d858d6af8dc28f831a0db64877d85cb5c Mon Sep 17 00:00:00 2001
From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com>
Date: Tue, 26 May 2026 10:18:37 -0400
Subject: [PATCH 21/24] Update
 Mathlib/MeasureTheory/VectorMeasure/Integral.lean

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
---
 Mathlib/MeasureTheory/VectorMeasure/Integral.lean | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
index 9cc5907b6ca515..5561f1e7650d2a 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
@@ -294,12 +294,7 @@ section VectorMeasure
 variable (f μ B) in
 @[simp]
 theorem integral_zero_vectorMeasure :
-    ∫ᵛ x, f x ∂[B; (0 : VectorMeasure X F)] = 0 := by
-  by_cases hG : CompleteSpace G
-  · simp only [integral, hG]
-    refine setToFun_measure_zero (dominatedFinMeasAdditive_cbmApplyMeasure 0 B) ?_
-    simp [variation_zero]
-  · simp [integral, hG]
+    ∫ᵛ x, f x ∂[B; (0 : VectorMeasure X F)] = 0 := by simp [integral]
 
 lemma integral_of_isEmpty [IsEmpty X] : ∫ᵛ x, f x ∂[B; μ] = 0 := by simp [eq_zero_of_isEmpty]
 

From de377433f1da97cf2b2d6bfccb6a8eed9c26c927 Mon Sep 17 00:00:00 2001
From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com>
Date: Tue, 26 May 2026 10:18:50 -0400
Subject: [PATCH 22/24] Update
 Mathlib/MeasureTheory/VectorMeasure/Integral.lean

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
---
 Mathlib/MeasureTheory/VectorMeasure/Integral.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
index 5561f1e7650d2a..d843f2c8c7e10f 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
@@ -317,7 +317,7 @@ theorem integral_finsetSum_vectorMeasure {μ : ι → VectorMeasure X F}
   · by_cases! hs : s.Nonempty
     · simp only [integral, hG, ↓reduceDIte, transpose_finsetSum_vectorMeasure, coe_finsetSum,
         transpose_eq_cbmApplyMeasure, ← setToFun_finsetSum_measure hs
-        (fun i ↦ dominatedFinMeasAdditive_cbmApplyMeasure (μ i) B) hf]
+          (fun i ↦ dominatedFinMeasAdditive_cbmApplyMeasure (μ i) B) hf]
       refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f ?_).symm
       · simpa using variation_finsetSum_le s _
       · exact integrable_finsetSum_measure.2 hf

From b7058ab5a45f0004a903fadda3b5adb076e73379 Mon Sep 17 00:00:00 2001
From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com>
Date: Tue, 26 May 2026 10:19:01 -0400
Subject: [PATCH 23/24] Update
 Mathlib/MeasureTheory/VectorMeasure/Integral.lean

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
---
 Mathlib/MeasureTheory/VectorMeasure/Integral.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
index d843f2c8c7e10f..0eeaf32ac5d4ee 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean
@@ -303,8 +303,8 @@ theorem integral_add_vectorMeasure (hμ : μ.Integrable f B) (hν : ν.Integrabl
   by_cases hG : CompleteSpace G
   · simp only [integral, hG, ↓reduceDIte, transpose_add_vectorMeasure, coe_add,
       transpose_eq_cbmApplyMeasure, ← setToFun_add_measure
-      (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
-      (dominatedFinMeasAdditive_cbmApplyMeasure ν B) hμ hν]
+        (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
+        (dominatedFinMeasAdditive_cbmApplyMeasure ν B) hμ hν]
     refine (setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f ?_).symm
     · simpa using variation_add_le
     · exact hμ.add_measure hν

From 0606ced1254974e67f6d71cd3a53e69b664c3354 Mon Sep 17 00:00:00 2001
From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com>
Date: Tue, 26 May 2026 10:23:56 -0400
Subject: [PATCH 24/24] fix

---
 Mathlib/MeasureTheory/Integral/SetToL1.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean
index 1020f6879b8d51..29c764ef2269ca 100644
--- a/Mathlib/MeasureTheory/Integral/SetToL1.lean
+++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean
@@ -1099,9 +1099,9 @@ theorem setToFun_add_measure {ν : Measure α} (hTμ : DominatedFinMeasAdditive
     setToFun (μ + ν) (T + T') (hTμ.add_measure μ ν hTν) f =
       setToFun μ T hTμ f + setToFun ν T' hTν f :=
   have hTμ_add : DominatedFinMeasAdditive (μ + ν) T (max C 0) :=
-    (hTμ.le (le_max_left C 0)).add_measure_right μ ν (le_max_right C 0)
+    (hTμ.of_le (le_max_left C 0)).add_measure_right μ ν (le_max_right C 0)
   have hTν_add : DominatedFinMeasAdditive (μ + ν) T' (max C' 0) :=
-    (hTν.le (le_max_left C' 0)).add_measure_left μ ν (le_max_right C' 0)
+    (hTν.of_le (le_max_left C' 0)).add_measure_left μ ν (le_max_right C' 0)
   calc
     setToFun (μ + ν) (T + T') (hTμ.add_measure μ ν hTν) f =
       setToFun (μ + ν) T hTμ_add f + setToFun (μ + ν) T' hTν_add f :=