diff --git a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
index 538cd8f0eefad9..f59dfd6d9bf24e 100644
--- a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
+++ b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
@@ -58,15 +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 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
@@ -76,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
@@ -102,6 +110,22 @@ 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') :=
+  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 ι)
     (hS_meas : ∀ i, MeasurableSet (S i)) (hSp : ∀ i ∈ sι, μ (S i) ≠ ∞)
@@ -130,6 +154,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 [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
@@ -160,12 +197,20 @@ 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 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⟩
+
 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 :=
+  ⟨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 : 𝕜) :
     DominatedFinMeasAdditive μ (fun s => c • T s) (‖c‖ * C) := by
@@ -185,6 +230,26 @@ 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 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
@@ -193,6 +258,14 @@ 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 {ι} {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
+  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
   have h : ∀ s, MeasurableSet s → c • μ s = ∞ → μ s = ∞ := by
diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean
index d76247acbc2e38..29c764ef2269ca 100644
--- a/Mathlib/MeasureTheory/Integral/SetToL1.lean
+++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean
@@ -776,6 +776,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]
@@ -1090,6 +1094,43 @@ 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 :=
+  have hTμ_add : DominatedFinMeasAdditive (μ + ν) T (max 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ν.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 :=
+        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)
+    {μ : ι → 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' μ 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))
+
 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/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 4cf20ddf8f1627..4974567cc92ada 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
@@ -282,6 +282,18 @@ 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 [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
+
 @[simp]
 theorem coe_zero : ⇑(0 : VectorMeasure α M) = 0 := rfl
 
@@ -314,6 +326,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 201814264e89b9..0eeaf32ac5d4ee 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
 
@@ -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,271 @@ 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_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]
+
+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 : ℝ) (f : X → E) :
-    ∫ᵛ x, (c • f) x ∂[B; μ] = c • ∫ᵛ x, f x ∂[B; μ] := integral_fun_smul μ B c f
+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 simp [integral]
+
+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, ↓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 ?_).symm
+    · simpa using variation_add_le
+    · exact hμ.add_measure hν
+  · 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
+  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 ?_).symm
+      · simpa using variation_finsetSum_le s _
+      · exact integrable_finsetSum_measure.2 hf
+    · simp_all
+  · simp [integral, hG]
+
+variable (f μ B) in
+@[integral_simps]
+theorem integral_neg_vectorMeasure :
+    ∫ᵛ 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, ↓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 ?_).symm
+    · simpa using variation_sub_le
+    · exact hμ.add_measure hν
+  · 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 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 ?_).symm
+    · simpa using variation_add_le
+    · exact hB.add_measure hC
+  · 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
+  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 ?_).symm
+      · simpa using variation_finsetSum_le s _
+      · exact integrable_finsetSum_measure.2 hf
+    · simp_all
+  · simp [integral, hG]
+
+@[integral_simps]
+theorem integral_neg_cbm :
+    ∫ᵛ 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, ↓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 ?_).symm
+    · simpa using variation_sub_le
+    · exact hB.add_measure hC
+  · simp [integral, hG]
+
+end cbm
 
 end VectorMeasure