Smooth functions and analytic functions on perfect sets

DefinitionPerfect sets of real numbers#✓fully proved

A set \(s \subseteq \mathbb{R}\) is perfect if it is closed, nonempty, and has no isolated points: every \(x \in s\) lies in the closure of \(s \setminus \{x\}\).

def IsPerfectSet (s : Set ℝ) : Prop :=
  IsClosed s ∧ s.Nonempty ∧ ∀ x ∈ s, x ∈ closure (s \ {x})

Used by 1

Used byUlam's problem on analytic agreement on a perfect set

DefinitionUlam's problem on analytic agreement on a perfect set#✓fully proved

Ulam's Problem 17.1 from the Scottish Book: for every continuous f on [0, 1], do there exist a perfect set C in [0, 1] and an analytic function φ with f x = φ x for every x ∈ C? The claim is stated for C ^ ∞ functions, which is the case refuted by Zahorski's construction.

def ScottishBookProblem17Point1Claim : Prop :=
  ∀ (f : ℝ → ℝ), ContDiff ℝ ⊤ f →
    ∃ (C : Set ℝ) (φ : ℝ → ℝ), IsPerfectSet C ∧ C ⊆ Set.Icc (0 : ℝ) 1 ∧
      AnalyticOn ℝ φ (Set.Icc (0 : ℝ) 1) ∧ ∀ x ∈ C, f x = φ x

Uses 1 · Used by 1

Statement usesPerfect sets of real numbers

Used byZahorski's negative answer to Ulam's perfect set problem

TheoremZahorski's negative answer to Ulam's perfect set problem#●ready to prove

Problem 17.1 is false: the answer is negative. Source: S. Ulam, Problem 17.1 of the Scottish Book; Z. Zahorski gave a negative answer by constructing a C ^ ∞ function that agrees with every real-analytic function on at most finitely many points, so no nonempty perfect set C can work for it: Z. Zahorski, "Sur l'ensemble des points singuliers d'une fonction d'une variable reelle admettant les derivees de tous les ordres", Fund. Math. 34 (1947), 183-245. The 2026 survey "90+ years of the Scottish Book" (arXiv:2603.27867) confirms the negative solution.

theorem_wanted continuousFunctionPerfectAnalytic_refuted : ¬ ScottishBookProblem17Point1Claim

Uses 1

Statement usesUlam's problem on analytic agreement on a perfect set

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.