# 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

The oscillation of `f : E → F`

at `x`

.

## Equations

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

## Instances For

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

The oscillation of `f`

at `x`

within a neighborhood `D`

of `x`

is equal to `oscillation f x`

The oscillation of `f`

at `x`

within `univ`

is equal to `oscillation f x`

The oscillation within `D`

of `f`

at `x ∈ D`

is 0 if and only if `ContinuousWithinAt f D x`

.

The oscillation of `f`

at `x`

is 0 if and only if `f`

is continuous at `x`

.

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`

.

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`

.