feat(MeasureTheory): the integral of a vector-valued function against a vector measure is additive (leanprover-community#30230)

Add some basic lemmas about the integral of a vector measure. This PR specifically focuses on the additivity of the integral.

Created with the help of Codex.

Author: CoolRmal

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

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 => ?_

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
 

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