Fractals and the monadic second order theory of one successor

PHILIPP HIERONYMI and 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

oscillation was also added to Mathlib in 2024. We should prove that they coincide.

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.