feat(Data/Set/Dissipate): Introduce dissipate s x := ⋂ y ≤ x, s y (#33975)

Introduce Dissipate s x := ⋂ y ≤ x, s y (Data/Set/Dissipate), which is parallel to Data/Set/Accumulate and provide some API for it. 

This will be used for compact systems in another PR. 

This PR continues the work from #25899.

Co-authored-by: pfaffelh <p.p@stochastik.uni-freiburg.de>
Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

Author: pfaffelh

Mathlib.lean

@@ -4047,6 +4047,7 @@ public import Mathlib.Data.Set.Constructions
 public import Mathlib.Data.Set.Countable
 public import Mathlib.Data.Set.Defs
 public import Mathlib.Data.Set.Disjoint
+public import Mathlib.Data.Set.Dissipate
 public import Mathlib.Data.Set.Enumerate
 public import Mathlib.Data.Set.Equitable
 public import Mathlib.Data.Set.Finite.Basic

Mathlib/Data/Set/Accumulate.lean

@@ -3,25 +3,25 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
+
 module
 
 public import Mathlib.Data.Nat.Lattice
-public import Mathlib.Data.Set.Lattice
 public import Mathlib.Order.PartialSups
 
 /-!
 # Accumulate
 
-The function `accumulate` takes a set `s` and returns `⋃ y ≤ x, s y`.
+The function `accumulate` takes `s : α → Set β` with `LE α` and returns `⋃ y ≤ x, s y`.
+It is related to `dissipate s := ⋂ y ≤ x, s y`.
 
-This is closely related to the function `partialSups`, although these two functions have
+`accumulate` is closely related to the function `partialSups`, although these two functions have
 slightly different typeclass assumptions and API. `partialSups_eq_accumulate` shows
 that they coincide on `ℕ`.
 -/
 
 @[expose] public section
 
-
 variable {α β : Type*} {s : α → Set β}
 
 namespace Set
@@ -52,11 +52,13 @@ theorem accumulate_subset_accumulate [Preorder α] {x y} (h : x ≤ y) :
     accumulate s x ⊆ accumulate s y :=
   monotone_accumulate h
 
+@[simp]
 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
 
+@[simp]
 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]

Mathlib/Data/Set/Dissipate.lean

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2026 Peter Pfaffelhuber. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Peter Pfaffelhuber
+-/
+
+module
+
+public import Mathlib.Data.Set.Accumulate
+
+/-!
+# Dissipate
+
+The function `dissipate` takes `s : α → Set β` with `LE α` and returns `⋂ y ≤ x, s y`.
+It is related to `accumulate s := ⋃ y ≤ x, s y`.
+
+-/
+
+@[expose] public section
+
+variable {α β : Type*} {s : α → Set β}
+
+namespace Set
+
+/-- `dissipate s` is the intersection of `s y` for `y ≤ x`. -/
+def dissipate [LE α] (s : α → Set β) (x : α) : Set β :=
+  ⋂ y ≤ x, s y
+
+theorem dissipate_def [LE α] {x : α} : dissipate s x = ⋂ y ≤ x, s y := rfl
+
+@[simp]
+theorem mem_dissipate [LE α] {x : α} {z : β} : z ∈ dissipate s x ↔ ∀ y ≤ x, z ∈ s y := by
+  simp [dissipate_def]
+
+theorem dissipate_subset [LE α] {x y : α} (hy : y ≤ x) : dissipate s x ⊆ s y :=
+  biInter_subset_of_mem hy
+
+theorem iInter_subset_dissipate [LE α] (x : α) : ⋂ i, s i ⊆ dissipate s x := by
+  simp only [dissipate, subset_iInter_iff]
+  exact fun x h ↦ iInter_subset_of_subset x fun ⦃a⦄ a ↦ a
+
+theorem antitone_dissipate [Preorder α] : Antitone (dissipate s) :=
+  fun _ _ hab ↦ biInter_subset_biInter_left fun _ hz => le_trans hz hab
+
+@[gcongr]
+theorem dissipate_subset_dissipate [Preorder α] {x y} (h : y ≤ x) :
+    dissipate s x ⊆ dissipate s y :=
+  antitone_dissipate h
+
+@[simp]
+theorem biInter_dissipate [Preorder α] {s : α → Set β} {x : α} :
+    ⋂ y, ⋂ (_ : y ≤ x), dissipate s y = dissipate s x := by
+  apply Subset.antisymm
+  · apply iInter_mono fun z y hy ↦ ?_
+    simp only [mem_iInter, mem_dissipate] at *
+    exact fun h ↦ hy h z le_rfl
+  · simp only [subset_iInter_iff]
+    exact fun i j ↦ dissipate_subset_dissipate j
+
+@[simp]
+theorem iInter_dissipate [Preorder α] : ⋂ x, dissipate s x = ⋂ x, s x := by
+  apply Subset.antisymm <;> simp_rw [subset_def, dissipate_def, mem_iInter]
+  · exact fun z h x' ↦ h x' x' le_rfl
+  · exact fun z h x' y hy ↦ h y
+
+@[simp]
+lemma dissipate_bot [PartialOrder α] [OrderBot α] (s : α → Set β) : dissipate s ⊥ = s ⊥ := by
+  simp [dissipate_def]
+
+@[simp]
+lemma dissipate_zero_nat (s : ℕ → Set β) : dissipate s 0 = s 0 := by
+  simp [dissipate_def]
+
+open Nat
+
+@[simp]
+theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) :
+  dissipate s (n + 1) = (dissipate s n) ∩ s (n + 1) := by
+  ext x
+  simp_all only [dissipate_def, mem_iInter, mem_inter_iff]
+  grind
+
+end Set

Mathlib/MeasureTheory/Measure/MeasuredSets.lean

@@ -114,7 +114,7 @@ lemma exists_measure_symmDiff_lt_of_generateFrom_isSetRing [IsFiniteMeasure μ]
       have fC n : Set.accumulate f n ∈ C := hC.accumulate_mem (fun n ↦ DC (by simp [hf])) n
       have : Tendsto (fun n ↦ μ (Set.accumulate f n)ᶜ) atTop (𝓝 0) := by
         have : ⋃₀ D = ⋃ n, Set.accumulate f n := by simp [hf, iUnion_accumulate]
-        rw [show (⋃₀ D)ᶜ = ⋂ n, (Set.accumulate f n)ᶜ by simp [this]] at hD
+        rw [show (⋃₀ D)ᶜ = ⋂ n, (Set.accumulate f n)ᶜ by simp [this, accumulate]] at hD
         rw [← hD]
         apply tendsto_measure_iInter_atTop (fun i ↦ ?_)
           (fun i j hij ↦ by simpa using monotone_accumulate hij) ⟨0, by simp⟩