Continuity, regularity and functional equations

Fine structure of real functions: Blumberg's theorem, continuous nowhere-differentiable functions (Weierstrass, Takagi), the rising sun lemma, approximate continuity, midpoint convexity, and the Cauchy, exponential and almost-additive functional equations including Hyers–Ulam stability.

TheoremA continuous nowhere differentiable function#✓fully proved

There exists a continuous function \(f : \mathbb{R} \to \mathbb{R}\) that is differentiable at no point of \(\mathbb{R}\).

theorem exists_continuous_nowhere_differentiable :
    ∃ f : C(ℝ, ℝ), ∀ x, ¬ DifferentiableAt ℝ f x
Sources
  • K. Weierstrass, 1872 lecture; P. du Bois-Reymond, J. Reine Angew. Math. 79 (1875), 21-37, DOI 10.1515/crll.1875.79.21.

TheoremA strict liminf gap at every finite value forces countably many finite values#●ready to prove

Let \(f : [0,1] \to [0,\infty]\) be such that for every \(y \in [0,1]\) with \(f(y) \ne \infty\),

\[ \liminf_{x \to y,\ x \ne y} f(x) > f(y), \]

where \(x\) ranges over \([0,1]\). Then the set \(\{y\in[0,1] : f(y) < \infty\}\) is countable.

public theorem_wanted countable_setOf_lt_top_of_lt_liminf
    (f : Set.Icc (0 : ℝ) 1 → ENNReal)
    (hgap : ∀ y : Set.Icc (0 : ℝ) 1,
      f y ≠ (⊤ : ENNReal) →
        Filter.liminf f (nhdsWithin y ({y}ᶜ)) > f y) :
    Set.Countable {y : Set.Icc (0 : ℝ) 1 | f y < (⊤ : ENNReal)}
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Real functions; Functions of one variable), problem ma_proofbench_l2_32.

TheoremBlumberg's theorem#✓fully proved

For every function \(f : \mathbb{R} \to \mathbb{R}\) there is a dense set \(D \subseteq \mathbb{R}\) such that the restriction of \(f\) to \(D\) is continuous.

theorem blumberg_theorem : ∀ f : ℝ → ℝ, ∃ D : Set ℝ, Dense D ∧ ContinuousOn f D
Sources
  • https://en.wikipedia.org/wiki/Blumberg_theorem.

TheoremContinuous midpoint-convex functions are convex#●ready to prove

Let \(a < b\) be real numbers and let \(\varphi : \mathbb{R} \to \mathbb{R}\) be continuous on \((a, b)\) and satisfy \(\varphi\bigl(\frac{x+y}{2}\bigr) \le \frac{\varphi(x) + \varphi(y)}{2}\) for all \(x, y \in (a, b)\). Then \(\varphi\) is convex on \((a, b)\).

public theorem_wanted convexOn_Ioo_of_continuousOn_of_midpoint_le
    {a b : ℝ} (hab : a < b) (φ : ℝ → ℝ)
    (hcont : ContinuousOn φ (Set.Ioo a b))
    (hmiddle :
      ∀ ⦃x⦄, x ∈ Set.Ioo a b → ∀ ⦃y⦄, y ∈ Set.Ioo a b →
        φ ((x + y) / 2) ≤ (φ x + φ y) / 2) :
    ConvexOn ℝ (Set.Ioo a b) φ
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_61.

TheoremDiscontinuous subadditive multiplicative functions on \(\mathbb{C}\)#●ready to prove

There is a function \(\varphi : \mathbb{C} \to \mathbb{R}\) that is not continuous, satisfies \(\varphi(x) \ge 0\) for all \(x \in \mathbb{C}\), is not identically \(0\) and not identically \(1\), and satisfies \(\varphi(x + y) \le \varphi(x) + \varphi(y)\) and \(\varphi(xy) = \varphi(x)\varphi(y)\) for all \(x, y \in \mathbb{C}\).

This answers Problem 39 of the Scottish Book (Auerbach), which notes that the continuous functions with these properties are exactly \(\varphi(x) = |x|^\alpha\) with \(0 < \alpha \le 1\) and asks whether discontinuous ones exist. Mazur's answer is \(\varphi(x) = |f(x)|\) for a discontinuous field automorphism \(f\) of \(\mathbb{C}\).

theorem_wanted exists_discontinuous_subadditive_multiplicative :
    ∃ φ : ℂ → ℝ, ¬ Continuous φ ∧ (∀ x, 0 ≤ φ x) ∧
      ¬ (∀ x, φ x = 0) ∧ ¬ (∀ x, φ x = 1) ∧
      (∀ x y, φ (x + y) ≤ φ x + φ y) ∧ (∀ x y, φ (x * y) = φ x * φ y)
Sources
  • H. Auerbach, Problem 39 of the Scottish Book; addendum of S. Mazur, 10 April 1937, in the Scottish Book, via Lebesgue's theorem on the existence of a discontinuous automorphism of ℂ (Kamke); see the commentary in R. D. Mauldin (ed.), The Scottish Book, 2nd ed. (Birkhäuser, 2015).

TheoremIsolated points of a graph are countable#●ready to prove

Let \(E \subseteq \mathbb{R}^n\), let \(f : \mathbb{R}^n \to \mathbb{R}^n\), and let \(F\) be the set of \(x\in E\) for which there is a sequence \((x_k)\) in \(E\setminus\{x\}\) with \(x_k \to x\) and \(f(x_k) \to f(x)\). Then \(E \setminus F\) is countable.

public theorem_wanted countable_diff_setOf_exists_seq_tendsto_and_tendsto_apply
    {n : ℕ}
    (E F : Set (EuclideanSpace ℝ (Fin n)))
    (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hF : ∀ x : EuclideanSpace ℝ (Fin n),
      x ∈ F ↔
        x ∈ E ∧
        ∃ xk : ℕ → EuclideanSpace ℝ (Fin n),
          (∀ k : ℕ, xk k ∈ E ∧ xk k ≠ x) ∧
          Filter.Tendsto xk Filter.atTop (nhds x) ∧
          Filter.Tendsto (fun k : ℕ => f (xk k)) Filter.atTop (nhds (f x))) :
    Set.Countable (E \ F)
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Real functions; Functions of several variables), problem ma_proofbench_l2_63.

TheoremSteinhaus's periodization problem (Scottish Book Problem 181)#●ready to prove

There is a continuous function \(f : \mathbb{R} \to \mathbb{R}\) with \(f(x) > 0\) for every real \(x\) such that, for every real \(x\), the series \(\sum_{n \in \mathbb{Z}} f(x + n)\) converges and its sum is \(1\).

theorem_wanted steinhaus181_periodization_one :
    ∃ f : ℝ → ℝ, Continuous f ∧ (∀ x, 0 < f x) ∧
      ∀ x, tsum (fun n : ℤ => f (x + (n : ℝ))) = 1
Sources
  • H. Steinhaus, Problem 181 of the Scottish Book; the addendum Ad 181 records that the Gaussian (1 / √π) exp (-x ^ 2) does not have the property, while Mazur's note gives a construction, taking a positive continuous g with finite periodization and dividing g by that periodization (e.g. g(x) = exp (-x ^ 2)). See the commentary in R. D. Mauldin (ed.), The Scottish Book, 2nd ed. (Birkhäuser, 2015).
2 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.