Smooth periodic functions are uniformly dense in continuous periodic functions

Proved

CauchyRiemannIndex.exists_contDiff_periodic_approx

by Mazecto · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

approximationperiodic-functionssmooth-functions

Let $f:\mathbb{R}\to\mathbb{R}$ be continuous and $1$ -periodic, and let $\varepsilon>0$ . Then there is a $C^\infty$ , $1$ -periodic function $g:\mathbb{R}\to\mathbb{R}$ with $|g(t)-f(t)|\le\varepsilon$ for all $t\in\mathbb{R}$ .

This lets continuous loops on $S^1=\mathbb{R}/\mathbb{Z}$ (moduli, arguments, coefficients) be replaced by smooth loops that are uniformly close, for instance in deformation arguments for asymptotic operators.

Formalization Note Smoothness is ContDiff ℝ ∞ g; periodicity is Function.Periodic g 1.

Preamble

import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.Algebra.Ring.Periodic

Formal statement

namespace CauchyRiemannIndex

open scoped ContDiff

/-- A continuous `1`-periodic real function is uniformly approximated, to any `ε > 0`, by a
smooth `1`-periodic function. -/
theorem exists_contDiff_periodic_approx (f : ℝ → ℝ) (hf : Continuous f)
    (hper : Function.Periodic f 1) (ε : ℝ) (hε : 0 < ε) :
    ∃ g : ℝ → ℝ, ContDiff ℝ ∞ g ∧ Function.Periodic g 1 ∧ ∀ t, |g t - f t| ≤ ε := by
  sorry

end CauchyRiemannIndex

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 5, §5.8, pp. 102-103

View graph