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. The results below can be proved for oscillation by observing that both functions are continuous.

Equations

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

theorem toNNReal_le_ENNReal (b : ENNReal) (ε : NNReal) (this : b ≤ ↑ε) : b.toNNReal ≤ ε

theorem coincide_osc {X : Type} {Y : Type} [MetricSpace X] [MetricSpace Y] (f : X → Y) (x : X) : oscillation' f x = oscillation f x

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.