# 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

source
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

Instances For

source
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

Instances For

source
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`

source
@[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`

source
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`

source
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
source
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
source
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`.

source
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`.

source
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`.

source
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`.