Documentation

Mathlib.Analysis.Oscillation

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 : EF) (x : E) :

The oscillation of f : E → F at x.

Equations
Instances For
    noncomputable def oscillationWithin {E : Type u} {F : Type v} [PseudoEMetricSpace F] [TopologicalSpace E] (f : EF) (D : Set E) (x : E) :

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

    Equations
    Instances For
      theorem oscillationWithin_nhd_eq_oscillation {E : Type u} {F : Type v} [PseudoEMetricSpace F] [TopologicalSpace E] (f : EF) (D : Set E) (x : E) (hD : D nhds x) :

      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 : EF) (x : E) :

      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 : EF} {D : Set E} {x : E} (hf : ContinuousWithinAt f D x) :
      theorem ContinuousAt.oscillation_eq_zero {E : Type u} {F : Type v} [PseudoEMetricSpace F] [TopologicalSpace E] {f : EF} {x : E} (hf : ContinuousAt f x) :
      theorem OscillationWithin.eq_zero_iff_continuousWithinAt {E : Type u} {F : Type v} [PseudoEMetricSpace F] [TopologicalSpace E] (f : EF) {D : Set E} {x : E} (xD : x D) :

      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 : EF) (x : E) :

      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 : EF} {D : Set E} {ε : ENNReal} (comp : IsCompact K) (hK : xK, oscillationWithin f D x < ε) :
      δ > 0, xK, 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 : EF} {ε : ENNReal} (hK : xK, oscillation f x < ε) :
      δ > 0, xK, 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.