generalize oscillation

Author: lua-vr

Mathlib/Analysis/Oscillation.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 James Sundstrom. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: James Sundstrom
+Authors: James Sundstrom, Lua Viana Reis
 -/
 module
 
@@ -12,10 +12,10 @@ public import Mathlib.Topology.EMetricSpace.Diam
 /-!
 # Oscillation
 
-In this file we define the oscillation of a function `f: E → F` at a point `x` of `E`. (`E` is
-required to be a TopologicalSpace and `F` a PseudoEMetricSpace.) The oscillation of `f` at `x` is
-defined to be the infimum of `diam f '' N` for all neighborhoods `N` of `x`. We also define
-`oscillationWithin f D x`, which is the oscillation at `x` of `f` restricted to `D`.
+In this file we define the oscillation of a function `f: E → F` along a filter `l` of `E`. (`F` is
+required to be a PseudoEMetricSpace.) The oscillation of `f` at `l` is
+defined to be the infimum of `diam f '' N` for all sets `N` in `l`. We also define
+`oscillationWithin f D l`, which is the oscillation at `l` of `f` restricted to `D`.
 
 We also prove some simple facts about oscillation, most notably that the oscillation of `f`
 at `x` is 0 if and only if `f` is continuous at `x`, with versions for both `oscillation` and
@@ -28,20 +28,29 @@ oscillation, oscillationWithin
 
 @[expose] public section
 
-open Topology Metric Set ENNReal
+open Topology Metric Set ENNReal Filter
 
 universe u v
 
 variable {E : Type u} {F : Type v} [PseudoEMetricSpace F]
 
+/-- The oscillation of `f : E → F` along `l`. -/
+noncomputable def oscillation (f : E → F) (l : Filter E) : ENNReal :=
+  ⨅ S ∈ l.map f, ediam S
+
 /-- The oscillation of `f : E → F` at `x`. -/
-noncomputable def oscillation [TopologicalSpace E] (f : E → F) (x : E) : ENNReal :=
-  ⨅ S ∈ (𝓝 x).map f, ediam S
+noncomputable def oscillationAt [TopologicalSpace E] (f : E → F) (x : E) : ENNReal :=
+  oscillation f (𝓝 x)
+
+/-- The oscillation of `f : E → F` within `D` along `l`. -/
+noncomputable def oscillationWithin (f : E → F) (D : Set E) (l : Filter E) :
+    ENNReal :=
+  oscillation f (l ⊓ 𝓟 D)
 
 /-- The oscillation of `f : E → F` within `D` at `x`. -/
-noncomputable def oscillationWithin [TopologicalSpace E] (f : E → F) (D : Set E) (x : E) :
+noncomputable def oscillationWithinAt [TopologicalSpace E] (f : E → F) (D : Set E) (x : E) :
     ENNReal :=
-  ⨅ S ∈ (𝓝[D] x).map f, ediam S
+  oscillationWithin f D (𝓝 x)
 
 /-- The oscillation of `f` at `x` within a neighborhood `D` of `x` is equal to `oscillation f x` -/
 theorem oscillationWithin_nhds_eq_oscillation [TopologicalSpace E] (f : E → F) (D : Set E) (x : E)