Fractals and the monadic second order theory of one successor

by PHILIPP HIERONYMI ERIK WALSBERG

Oscillation

Let f : (X, dX) → (Y, dY ) be a function between metric spaces. The oscillation of f at x ∈ X is the supremum of all δ ≥ 0 such that for every ε > 0 there are y,z ∈ X such that dX(x, y) < ε, dX(x,z) < ε and dY (f(y), f(z)) > δ . . Recall that f is continuous at x if and only if the oscillation of f at x is zero.

noncomputable def oscillation {X : Type} {Y : Type} [MetricSpace X] [MetricSpace Y] (f : X → Y) (x : X) : ENNReal

Equations

• oscillation f x = sSup {δ : ENNReal | ∀ ε > 0, ∃ (y : X) (z : X), edist x y < ε ∧ edist x z < ε ∧ edist (f y) (f z) > δ}

theorem oscillation_const {c : ℝ} {x : ℝ} : oscillation (fun (x : ℝ) => c) x = 0

The oscillation of a constant c is 0 at any x.

theorem oscillation_id {x : ℝ} : oscillation (fun (x : ℝ) => x) x = 0

The oscillation of the identity is 0 at any x.