Borel complexity of differentiable functions

DefinitionFunctions differentiable at every point of \((0, 1)\)#✓fully proved

A continuous function \(f \colon (0, 1) \to \mathbb{R}\) has a derivative at every point if for every \(x \in (0, 1)\) the function \(\tilde f \colon \mathbb{R} \to \mathbb{R}\) equal to \(f\) on \((0, 1)\) and to \(0\) outside \((0, 1)\) is differentiable at \(x\). Since \(\tilde f\) agrees with \(f\) near every point of \((0, 1)\), this depends only on \(f\): it says that \(f\) is differentiable at every point of \((0, 1)\).

def HasDerivativeAtEveryPoint (f : C(↥(Set.Ioo (0 : ℝ) 1), ℝ)) : Prop :=
  ∀ x : ℝ, x ∈ Set.Ioo (0 : ℝ) 1 →
    DifferentiableAt ℝ (fun y => if h : y ∈ Set.Ioo (0 : ℝ) 1 then f ⟨y, h⟩ else 0) x

Used by 1

Used byEverywhere differentiable functions do not form a Borel set

TheoremEverywhere differentiable functions do not form a Borel set#●ready to prove

In the space \(C((0, 1))\) of continuous real functions on the open interval \((0, 1)\), with the compact-open topology (uniform convergence on compact subsets), the set of functions that have a derivative at every point of \((0, 1)\) is not a Borel set.

This is Banach's Problem 52 of the Scottish Book. The typescript also records that this class is not an \(F_\sigma\) set, that it is coanalytic, and that the problem was solved by Mazurkiewicz.

theorem_wanted everywhere_differentiable_class_not_borel :
    ¬ MeasurableSet { f : C(↥(Set.Ioo (0 : ℝ) 1), ℝ) | HasDerivativeAtEveryPoint f }

Sources

• S. Banach, Problem 52 of the Scottish Book; solved by Mazurkiewicz, as recorded in typescript Ad 52; see the commentary in R. D. Mauldin (ed.), The Scottish Book, 2nd ed. (Birkhäuser, 2015).

Uses 1

Statement usesFunctions differentiable at every point of \((0, 1)\)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.