chore: lower case Accumulate (#32871)

`Accumulate` is a function constructing a `Set`. Per our naming rules, it should be lower-case. The current upper case is probably a consequence of the migration script from Lean 3 to Lean 4, which had issues with the casing of Set-valued functions. This PR changes it to lower case.

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/Data/Set/Accumulate.lean

@@ -12,7 +12,7 @@ public import Mathlib.Order.PartialSups
 /-!
 # Accumulate
 
-The function `Accumulate` takes a set `s` and returns `⋃ y ≤ x, s y`.
+The function `accumulate` takes a set `s` and returns `⋃ y ≤ x, s y`.
 
 This is closely related to the function `partialSups`, although these two functions have
 slightly different typeclass assumptions and API. `partialSups_eq_accumulate` shows
@@ -26,64 +26,66 @@ variable {α β : Type*} {s : α → Set β}
 
 namespace Set
 
-/-- `Accumulate s` is the union of `s y` for `y ≤ x`. -/
-def Accumulate [LE α] (s : α → Set β) (x : α) : Set β :=
+/-- `accumulate s` is the union of `s y` for `y ≤ x`. -/
+def accumulate [LE α] (s : α → Set β) (x : α) : Set β :=
   ⋃ y ≤ x, s y
 
-theorem accumulate_def [LE α] {x : α} : Accumulate s x = ⋃ y ≤ x, s y :=
+@[deprecated (since := "2025-12-14")] alias Accumulate := accumulate
+
+theorem accumulate_def [LE α] {x : α} : accumulate s x = ⋃ y ≤ x, s y :=
   rfl
 
 @[simp]
-theorem mem_accumulate [LE α] {x : α} {z : β} : z ∈ Accumulate s x ↔ ∃ y ≤ x, z ∈ s y := by
+theorem mem_accumulate [LE α] {x : α} {z : β} : z ∈ accumulate s x ↔ ∃ y ≤ x, z ∈ s y := by
   simp_rw [accumulate_def, mem_iUnion₂, exists_prop]
 
-theorem subset_accumulate [Preorder α] {x : α} : s x ⊆ Accumulate s x := fun _ => mem_biUnion le_rfl
+theorem subset_accumulate [Preorder α] {x : α} : s x ⊆ accumulate s x := fun _ => mem_biUnion le_rfl
 
-theorem accumulate_subset_iUnion [LE α] (x : α) : Accumulate s x ⊆ ⋃ i, s i :=
+theorem accumulate_subset_iUnion [LE α] (x : α) : accumulate s x ⊆ ⋃ i, s i :=
   (biUnion_subset_biUnion_left (subset_univ _)).trans_eq (biUnion_univ _)
 
-theorem monotone_accumulate [Preorder α] : Monotone (Accumulate s) := fun _ _ hxy =>
+theorem monotone_accumulate [Preorder α] : Monotone (accumulate s) := fun _ _ hxy =>
   biUnion_subset_biUnion_left fun _ hz => le_trans hz hxy
 
 @[gcongr]
 theorem accumulate_subset_accumulate [Preorder α] {x y} (h : x ≤ y) :
-    Accumulate s x ⊆ Accumulate s y :=
+    accumulate s x ⊆ accumulate s y :=
   monotone_accumulate h
 
-theorem biUnion_accumulate [Preorder α] (x : α) : ⋃ y ≤ x, Accumulate s y = ⋃ y ≤ x, s y := by
+theorem biUnion_accumulate [Preorder α] (x : α) : ⋃ y ≤ x, accumulate s y = ⋃ y ≤ x, s y := by
   apply Subset.antisymm
   · exact iUnion₂_subset fun y hy => monotone_accumulate hy
   · exact iUnion₂_mono fun y _ => subset_accumulate
 
-theorem iUnion_accumulate [Preorder α] : ⋃ x, Accumulate s x = ⋃ x, s x := by
+theorem iUnion_accumulate [Preorder α] : ⋃ x, accumulate s x = ⋃ x, s x := by
   apply Subset.antisymm
   · simp only [subset_def, mem_iUnion, exists_imp, mem_accumulate]
     intro z x x' ⟨_, hz⟩
     exact ⟨x', hz⟩
   · exact iUnion_mono fun i => subset_accumulate
 
 @[simp]
-lemma accumulate_bot [PartialOrder α] [OrderBot α] (s : α → Set β) : Accumulate s ⊥ = s ⊥ := by
+lemma accumulate_bot [PartialOrder α] [OrderBot α] (s : α → Set β) : accumulate s ⊥ = s ⊥ := by
   simp [Set.accumulate_def]
 
 @[simp]
-lemma accumulate_zero_nat (s : ℕ → Set β) : Accumulate s 0 = s 0 := by
+lemma accumulate_zero_nat (s : ℕ → Set β) : accumulate s 0 = s 0 := by
   simp [accumulate_def]
 
 open Function in
 theorem disjoint_accumulate [Preorder α] (hs : Pairwise (Disjoint on s)) {i j : α} (hij : i < j) :
-    Disjoint (Accumulate s i) (s j) := by
+    Disjoint (accumulate s i) (s j) := by
   apply disjoint_left.2 (fun x hx ↦ ?_)
-  simp only [Accumulate, mem_iUnion, exists_prop] at hx
+  simp only [accumulate, mem_iUnion, exists_prop] at hx
   rcases hx with ⟨k, hk, hx⟩
   exact disjoint_left.1 (hs (hk.trans_lt hij).ne) hx
 
 theorem accumulate_succ (u : ℕ → Set α) (n : ℕ) :
-    Accumulate u (n + 1) = Accumulate u n ∪ u (n + 1) := biUnion_le_succ u n
+    accumulate u (n + 1) = accumulate u n ∪ u (n + 1) := biUnion_le_succ u n
 
 lemma partialSups_eq_accumulate (f : ℕ → Set α) :
-    partialSups f = Accumulate f := by
+    partialSups f = accumulate f := by
   ext n
-  simp [partialSups_eq_sup_range, Accumulate, Nat.lt_succ_iff]
+  simp [partialSups_eq_sup_range, accumulate, Nat.lt_succ_iff]
 
 end Set

Mathlib/MeasureTheory/Measure/AddContent.lean

@@ -352,7 +352,7 @@ lemma addContent_diff_of_ne_top (m : AddContent C) (hC : IsSetRing C)
 
 lemma addContent_accumulate (m : AddContent C) (hC : IsSetRing C)
     {s : ℕ → Set α} (hs_disj : Pairwise (Disjoint on s)) (hsC : ∀ i, s i ∈ C) (n : ℕ) :
-      m (Set.Accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i) := by
+      m (Set.accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i) := by
   induction n with
   | zero => simp
   | succ n hn =>
@@ -396,7 +396,7 @@ theorem addContent_iUnion_eq_sum_of_tendsto_zero (hC : IsSetRing C) (m : AddCont
     (h_disj : Pairwise (Disjoint on f)) :
     m (⋃ i, f i) = ∑' i, m (f i) := by
   -- We use the continuity of `m` at `∅` on the sequence `n ↦ (⋃ i, f i) \ (set.accumulate f n)`
-  let s : ℕ → Set α := fun n ↦ (⋃ i, f i) \ Set.Accumulate f n
+  let s : ℕ → Set α := fun n ↦ (⋃ i, f i) \ Set.accumulate f n
   have hCs n : s n ∈ C := hC.diff_mem hUf (hC.accumulate_mem hf n)
   have h_tendsto : Tendsto (fun n ↦ m (s n)) atTop (𝓝 0) := by
     refine hm_tendsto hCs ?_ ?_
@@ -428,7 +428,7 @@ theorem tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum (hC : IsSet
       (disjoint_disjointed f)]
   have h n : m (f n) = ∑ i ∈ range (n + 1), m (disjointed f i) := by
     nth_rw 1 [← addContent_accumulate _ hC (disjoint_disjointed f) (hC.disjointed_mem hf),
-    ← hf_mono.partialSups_eq, ← partialSups_disjointed, partialSups_eq_biSup, Accumulate]
+    ← hf_mono.partialSups_eq, ← partialSups_disjointed, partialSups_eq_biSup, accumulate]
     rfl
   simp_rw [h]
   refine (tendsto_add_atTop_iff_nat (f := (fun k ↦ ∑ i ∈ range k, m (disjointed f i))) 1).2 ?_

Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

@@ -177,7 +177,7 @@ theorem apply_union_le (μ : FiniteMeasure Ω) {s₁ s₂ : Set Ω} : μ (s₁ 
 sets is the limit of the measures of the partial unions. -/
 protected lemma tendsto_measure_iUnion_accumulate {ι : Type*} [Preorder ι]
     [IsCountablyGenerated (atTop : Filter ι)] {μ : FiniteMeasure Ω} {f : ι → Set Ω} :
-    Tendsto (fun i ↦ μ (Accumulate f i)) atTop (𝓝 (μ (⋃ i, f i))) := by
+    Tendsto (fun i ↦ μ (accumulate f i)) atTop (𝓝 (μ (⋃ i, f i))) := by
   simpa [← ennreal_coeFn_eq_coeFn_toMeasure]
     using tendsto_measure_iUnion_accumulate (μ := μ.toMeasure) (ι := ι)
 

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -496,7 +496,7 @@ theorem _root_.Antitone.measure_iUnion [Preorder ι] [IsCodirectedOrder ι]
 (not necessarily measurable) sets is the supremum of the measures of the partial unions. -/
 theorem measure_iUnion_eq_iSup_accumulate [Preorder ι] [IsDirectedOrder ι]
     [(atTop : Filter ι).IsCountablyGenerated] {f : ι → Set α} :
-    μ (⋃ i, f i) = ⨆ i, μ (Accumulate f i) := by
+    μ (⋃ i, f i) = ⨆ i, μ (accumulate f i) := by
   rw [← iUnion_accumulate]
   exact monotone_accumulate.measure_iUnion
 
@@ -590,7 +590,7 @@ sets is the limit of the measures of the partial unions. -/
 theorem tendsto_measure_iUnion_accumulate {α ι : Type*}
     [Preorder ι] [IsCountablyGenerated (atTop : Filter ι)]
     {_ : MeasurableSpace α} {μ : Measure α} {f : ι → Set α} :
-    Tendsto (fun i ↦ μ (Accumulate f i)) atTop (𝓝 (μ (⋃ i, f i))) := by
+    Tendsto (fun i ↦ μ (accumulate f i)) atTop (𝓝 (μ (⋃ i, f i))) := by
   refine .of_neBot_imp fun h ↦ ?_
   have := (atTop_neBot_iff.1 h).2
   rw [measure_iUnion_eq_iSup_accumulate]

Mathlib/MeasureTheory/Measure/Portmanteau.lean

@@ -795,7 +795,7 @@ lemma ProbabilityMeasure.exists_lt_measure_biUnion_of_isOpen
     simp [← hT, hr]
   rcases T_count.exists_eq_range this with ⟨f, hf⟩
   have G_eq : G = ⋃ n, f n := by simp [← hT, hf]
-  have : Tendsto (fun i ↦ ν (Accumulate f i)) atTop (𝓝 (ν (⋃ i, f i))) :=
+  have : Tendsto (fun i ↦ ν (accumulate f i)) atTop (𝓝 (ν (⋃ i, f i))) :=
     (ENNReal.tendsto_toNNReal_iff (by simp) (by simp)).2 tendsto_measure_iUnion_accumulate
   rw [← G_eq] at this
   rcases ((tendsto_order.1 this).1 r hr).exists with ⟨n, hn⟩

Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

@@ -204,7 +204,7 @@ theorem apply_union_le (μ : ProbabilityMeasure Ω) {s₁ s₂ : Set Ω} : μ (s
 sets is the limit of the measures of the partial unions. -/
 protected lemma tendsto_measure_iUnion_accumulate {ι : Type*} [Preorder ι]
     [IsCountablyGenerated (atTop : Filter ι)] {μ : ProbabilityMeasure Ω} {f : ι → Set Ω} :
-    Tendsto (fun i ↦ μ (Accumulate f i)) atTop (𝓝 (μ (⋃ i, f i))) := by
+    Tendsto (fun i ↦ μ (accumulate f i)) atTop (𝓝 (μ (⋃ i, f i))) := by
   simpa [← ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.tendsto_coe]
     using tendsto_measure_iUnion_accumulate (μ := μ.toMeasure)
 

Mathlib/MeasureTheory/Measure/SeparableMeasure.lean

@@ -272,7 +272,7 @@ theorem Measure.MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite (h𝒜 : I
   measurable s hs := hgen ▸ measurableSet_generateFrom hs
   approx s ms hμs ε ε_pos := by
     -- We use partial unions of (Sₙ) to get a monotone family spanning `X`.
-    let T := Accumulate S.set
+    let T := accumulate S.set
     have T_mem (n) : T n ∈ 𝒜 := by
       simpa using h𝒜.biUnion_mem {k | k ≤ n}.toFinset (fun k _ ↦ S.set_mem k)
     have T_finite (n) : μ (T n) < ∞ := by

Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean

@@ -117,7 +117,7 @@ def Measure.toFiniteSpanningSetsIn (μ : Measure α) [h : SigmaFinite μ] :
   measure using `Classical.choose`. This definition satisfies monotonicity in addition to all other
   properties in `SigmaFinite`. -/
 def spanningSets (μ : Measure α) [SigmaFinite μ] (i : ℕ) : Set α :=
-  Accumulate μ.toFiniteSpanningSetsIn.set i
+  accumulate μ.toFiniteSpanningSetsIn.set i
 
 theorem monotone_spanningSets (μ : Measure α) [SigmaFinite μ] : Monotone (spanningSets μ) :=
   monotone_accumulate

Mathlib/MeasureTheory/SetSemiring.lean

@@ -523,7 +523,7 @@ theorem iInter_le_mem (hC : IsSetRing C) {s : ℕ → Set α} (hs : ∀ n, s n 
   | succ n hn => rw [biInter_le_succ]; exact hC.inter_mem hn (hs _)
 
 theorem accumulate_mem (hC : IsSetRing C) {s : ℕ → Set α} (hs : ∀ i, s i ∈ C) (n : ℕ) :
-    Accumulate s n ∈ C := by
+    accumulate s n ∈ C := by
   induction n with
   | zero => simp [hs 0]
   | succ n hn => rw [accumulate_succ]; exact hC.union_mem hn (hs _)

Mathlib/Topology/Compactness/Compact.lean

@@ -458,7 +458,7 @@ theorem Finset.isCompact_biUnion (s : Finset ι) {f : ι → Set X} (hf : ∀ i
   s.finite_toSet.isCompact_biUnion hf
 
 theorem isCompact_accumulate {K : ℕ → Set X} (hK : ∀ n, IsCompact (K n)) (n : ℕ) :
-    IsCompact (Accumulate K n) :=
+    IsCompact (accumulate K n) :=
   (finite_le_nat n).isCompact_biUnion fun k _ => hK k
 
 theorem Set.Finite.isCompact_sUnion {S : Set (Set X)} (hf : S.Finite) (hc : ∀ s ∈ S, IsCompact s) :