feat: vector measures associated to functions of bounded variation

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -89,7 +89,11 @@ theorem prod_pair [DecidableEq ι] {a b : ι} (h : a ≠ b) :
     (∏ x ∈ ({a, b} : Finset ι), f x) = f a * f b := by
   rw [prod_insert (notMem_singleton.2 h), prod_singleton]
 
-@[to_additive (attr := simp)]
+/-- If a function is injective on a finset, products over the original finset or its image coincide.
+See also `prod_image_of_pairwise_eq_one` for a version with weaker assumptions. -/
+@[to_additive (attr := simp) /-- If a function is injective on a finset, sums over the original
+finset or its image coincide.
+See also `sum_image_of_pairwise_eq_zero` for a version with weaker assumptions. -/]
 theorem prod_image [DecidableEq ι] {s : Finset κ} {g : κ → ι} :
     Set.InjOn g s → ∏ x ∈ s.image g, f x = ∏ x ∈ s, f (g x) :=
   fold_image
@@ -210,7 +214,12 @@ lemma prod_sum_eq_prod_toLeft_mul_prod_toRight (s : Finset (ι ⊕ κ)) (f : ι
 theorem prod_sumElim (s : Finset ι) (t : Finset κ) (f : ι → M) (g : κ → M) :
     ∏ x ∈ s.disjSum t, Sum.elim f g x = (∏ x ∈ s, f x) * ∏ x ∈ t, g x := by simp
 
-@[to_additive]
+/-- Given a finite family of pairwise disjoint finsets, the product over their union is the product
+of the products over the sets.
+See also `prod_biUnion_of_pairwise_eq_one` for a version with weaker assumptions. -/
+@[to_additive /-- Given a finite family of pairwise disjoint finsets, the sum over their union is
+the sum of the sums over the sets.
+See also `sum_biUnion_of_pairwise_eq_zero` for a version with weaker assumptions. -/]
 theorem prod_biUnion [DecidableEq ι] {s : Finset κ} {t : κ → Finset ι}
     (hs : Set.PairwiseDisjoint (↑s) t) : ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i := by
   rw [← disjiUnion_eq_biUnion _ _ hs, prod_disjiUnion]
@@ -784,6 +793,26 @@ lemma prod_mul_eq_prod_mul_of_exists {s : Finset ι} {f : ι → M} {b₁ b₂ :
   simp only [mem_erase, ne_eq, not_true_eq_false, false_and, not_false_eq_true, prod_insert]
   rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]
 
+@[to_additive]
+theorem prod_biUnion_of_pairwise_eq_one [DecidableEq ι] {s : Finset κ} {t : κ → Finset ι}
+    (hs : (s : Set κ).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1) :
+    ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i := by
+  classical
+  let t' k := (t k).filter (fun i ↦ f i ≠ 1)
+  have : ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s.biUnion t', f x := by
+    apply prod_congr_of_eq_on_inter
+    · simp +contextual; grind
+    · simp +contextual; grind
+    · simp
+  rw [this, prod_biUnion]; swap
+  · intro i hi j hj hij a hai haj k hk
+    have hki : k ∈ t' i := hai hk
+    have hkj : k ∈ t' j := haj hk
+    simp only [ne_eq, mem_filter, t'] at hki hkj
+    exact (hki.2 (hs hi hj hij k (by grind) )).elim
+  apply Finset.prod_congr rfl (fun i hi ↦ ?_)
+  exact prod_filter_ne_one (t i)
+
 @[to_additive]
 lemma prod_filter_of_pairwise_eq_one [DecidableEq ι] {f : κ → ι} {g : ι → M} {n : κ} {I : Finset κ}
     (hn : n ∈ I) (hf : (I : Set κ).Pairwise fun i j ↦ f i = f j → g (f i) = 1) :

Mathlib/Analysis/Normed/Group/Basic.lean

@@ -419,7 +419,7 @@ abbrev GroupNorm.toNormedCommGroup [CommGroup E] (f : GroupNorm E) : NormedCommG
 section SeminormedGroup
 
 variable [SeminormedGroup E] [SeminormedGroup F] [SeminormedGroup G] {s : Set E}
-  {a a₁ a₂ b c : E} {r r₁ r₂ : ℝ}
+  {a a₁ a₂ b c d : E} {r r₁ r₂ : ℝ}
 
 @[to_additive]
 theorem dist_eq_norm_div (a b : E) : dist a b = ‖a / b‖ :=
@@ -495,6 +495,11 @@ theorem norm_mul_le_of_le' (h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r
 @[to_additive norm_add₃_le /-- **Triangle inequality** for the norm. -/]
 lemma norm_mul₃_le' : ‖a * b * c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ := norm_mul_le_of_le' (norm_mul_le' _ _) le_rfl
 
+/-- **Triangle inequality** for the norm. -/
+@[to_additive norm_add₄_le /-- **Triangle inequality** for the norm. -/]
+lemma norm_mul₄_le' : ‖a * b * c * d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖ :=
+    norm_mul_le_of_le' norm_mul₃_le' le_rfl
+
 @[to_additive]
 lemma norm_div_le_norm_div_add_norm_div (a b c : E) : ‖a / c‖ ≤ ‖a / b‖ + ‖b / c‖ := by
   simpa only [dist_eq_norm_div] using dist_triangle a b c
@@ -979,6 +984,19 @@ variable {E : Type*} [TopologicalSpace E] [ESeminormedMonoid E]
 @[to_additive enorm_add_le]
 lemma enorm_mul_le' (a b : E) : ‖a * b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ := ESeminormedMonoid.enorm_mul_le a b
 
+@[to_additive enorm_add_le_of_le]
+theorem enorm_mul_le_of_le' {r₁ r₂ : ℝ≥0∞} {a₁ a₂ : E}
+    (h₁ : ‖a₁‖ₑ ≤ r₁) (h₂ : ‖a₂‖ₑ ≤ r₂) : ‖a₁ * a₂‖ₑ ≤ r₁ + r₂ :=
+  (enorm_mul_le' a₁ a₂).trans <| add_le_add h₁ h₂
+
+@[to_additive enorm_add₃_le]
+lemma enorm_mul₃_le' {a b c : E} : ‖a * b * c‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ :=
+  enorm_mul_le_of_le' (enorm_mul_le' _ _) le_rfl
+
+@[to_additive enorm_add₄_le]
+lemma enorm_mul₄_le' {a b c d : E} : ‖a * b * c * d‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ + ‖d‖ₑ :=
+  enorm_mul_le_of_le' enorm_mul₃_le' le_rfl
+
 end ESeminormedMonoid
 
 section ENormedMonoid

Mathlib/Data/Set/SymmDiff.lean

@@ -17,7 +17,7 @@ assert_not_exists RelIso
 namespace Set
 
 universe u
-variable {α : Type u} {a : α} {s t u : Set α}
+variable {α : Type u} {a : α} {s t u v : Set α}
 
 open scoped symmDiff
 
@@ -50,4 +50,19 @@ theorem subset_symmDiff_union_symmDiff_left (h : Disjoint s t) : u ⊆ s ∆ u 
 theorem subset_symmDiff_union_symmDiff_right (h : Disjoint t u) : s ⊆ s ∆ t ∪ s ∆ u :=
   h.le_symmDiff_sup_symmDiff_right
 
+lemma union_symmDiff_subset : (s ∪ t) ∆ u ⊆ s ∆ u ∪ t ∆ u := by
+  intro x hx
+  simp only [Set.mem_symmDiff, Set.mem_union] at hx ⊢
+  grind
+
+lemma symmDiff_union_subset : s ∆ (t ∪ u) ⊆ s ∆ t ∪ s ∆ u := by
+  intro x hx
+  simp only [Set.mem_symmDiff, Set.mem_union] at hx ⊢
+  grind
+
+lemma union_symmDiff_union_subset : (s ∪ t) ∆ (u ∪ v) ⊆ s ∆ u ∪ t ∆ v := by
+  intro x hx
+  simp only [Set.mem_symmDiff, Set.mem_union] at hx ⊢
+  grind
+
 end Set

Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean

@@ -115,7 +115,7 @@ section ProjectiveFamilyContent
 cylinders, by setting `projectiveFamilyContent s = P I S` for `s = cylinder I S`, where `I` is
 a finite set of indices and `S` is a measurable set in `Π i : I, α i`. -/
 noncomputable def projectiveFamilyContent (hP : IsProjectiveMeasureFamily P) :
-    AddContent (measurableCylinders α) :=
+    AddContent ℝ≥0∞ (measurableCylinders α) :=
   isSetRing_measurableCylinders.addContent_of_union (projectiveFamilyFun P)
     (projectiveFamilyFun_empty hP) (projectiveFamilyFun_union hP)