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.

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 oscillationWithin.

Tags

oscillation, oscillationWithin

noncomputable def oscillation {E : Type u} {F : Type v} [PseudoEMetricSpace F] [TopologicalSpace E] (f : E → F) (x : E) : ENNReal

The oscillation of f : E → F at x.

Equations

• oscillation f x = ⨅ S ∈ Filter.map f (nhds x), EMetric.diam S

noncomputable def oscillationWithin {E : Type u} {F : Type v} [PseudoEMetricSpace F] [TopologicalSpace E] (f : E → F) (D : Set E) (x : E) : ENNReal

The oscillation of f : E → F within D at x.

Equations

• oscillationWithin f D x = ⨅ S ∈ Filter.map f (nhdsWithin x D), EMetric.diam S

theorem oscillationWithin_nhds_eq_oscillation {E : Type u} {F : Type v} [PseudoEMetricSpace F] [TopologicalSpace E] (f : E → F) (D : Set E) (x : E) (hD : D ∈ nhds x) : oscillationWithin f D x = oscillation f x

The oscillation of f at x within a neighborhood D of x is equal to oscillation f x

@[deprecated oscillationWithin_nhds_eq_oscillation (since := "2025-05-22")]

theorem oscillationWithin_nhd_eq_oscillation {E : Type u} {F : Type v} [PseudoEMetricSpace F] [TopologicalSpace E] (f : E → F) (D : Set E) (x : E) (hD : D ∈ nhds x) : oscillationWithin f D x = oscillation f x

Alias of oscillationWithin_nhds_eq_oscillation.

---

The oscillation of f at x within a neighborhood D of x is equal to oscillation f x

theorem oscillationWithin_univ_eq_oscillation {E : Type u} {F : Type v} [PseudoEMetricSpace F] [TopologicalSpace E] (f : E → F) (x : E) : oscillationWithin f Set.univ x = oscillation f x

The oscillation of f at x within univ is equal to oscillation f x

theorem ContinuousWithinAt.oscillationWithin_eq_zero {E : Type u} {F : Type v} [PseudoEMetricSpace F] [TopologicalSpace E] {f : E → F} {D : Set E} {x : E} (hf : ContinuousWithinAt f D x) : oscillationWithin f D x = 0

theorem ContinuousAt.oscillation_eq_zero {E : Type u} {F : Type v} [PseudoEMetricSpace F] [TopologicalSpace E] {f : E → F} {x : E} (hf : ContinuousAt f x) : oscillation f x = 0

theorem OscillationWithin.eq_zero_iff_continuousWithinAt {E : Type u} {F : Type v} [PseudoEMetricSpace F] [TopologicalSpace E] (f : E → F) {D : Set E} {x : E} (xD : x ∈ D) : oscillationWithin f D x = 0 ↔ ContinuousWithinAt f D x

The oscillation within D of f at x ∈ D is 0 if and only if ContinuousWithinAt f D x.

theorem Oscillation.eq_zero_iff_continuousAt {E : Type u} {F : Type v} [PseudoEMetricSpace F] [TopologicalSpace E] (f : E → F) (x : E) : oscillation f x = 0 ↔ ContinuousAt f x

The oscillation of f at x is 0 if and only if f is continuous at x.

theorem IsCompact.uniform_oscillationWithin {E : Type u} {F : Type v} [PseudoEMetricSpace F] [PseudoEMetricSpace E] {K : Set E} {f : E → F} {D : Set E} {ε : ENNReal} (comp : IsCompact K) (hK : ∀ x ∈ K, oscillationWithin f D x < ε) : ∃ δ > 0, ∀ x ∈ K, EMetric.diam (f '' (EMetric.ball x (ENNReal.ofReal δ) ∩ D)) ≤ ε

If oscillationWithin f D x < ε at every x in a compact set K, then there exists δ > 0 such that the oscillation of f on ball x δ ∩ D is less than ε for every x in K.

theorem IsCompact.uniform_oscillation {E : Type u} {F : Type v} [PseudoEMetricSpace F] [PseudoEMetricSpace E] {K : Set E} (comp : IsCompact K) {f : E → F} {ε : ENNReal} (hK : ∀ x ∈ K, oscillation f x < ε) : ∃ δ > 0, ∀ x ∈ K, EMetric.diam (f '' EMetric.ball x (ENNReal.ofReal δ)) ≤ ε

If oscillation f x < ε at every x in a compact set K, then there exists δ > 0 such that the oscillation of f on ball x δ is less than ε for every x in K.