Schwartz functions are Lipschitz and uniformly continuous

Proved

SchwartzSpaceWiki.lipschitz_and_uniformContinuous

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

fourier-analysisschwartz-space

Every $f\in\mathcal{S}(\mathbb{R}^n)$ is Lipschitz continuous on $\mathbb{R}^n$ (there is $K\ge 0$ with $|f(x)-f(y)|\le K|x-y|$ for all $x,y$ ), and hence uniformly continuous on $\mathbb{R}^n$ .

Preamble

import Mathlib
import Definitions.Def_SchwartzSpaceWiki_Defs

open MeasureTheory

Formal statement

namespace SchwartzSpaceWiki

theorem lipschitz_and_uniformContinuous (n : ℕ) (f : Rn n → ℂ) (hf : f ∈ schwartzSpace n) :
    (∃ K : NNReal, LipschitzWith K f) ∧ UniformContinuous f := by sorry

end SchwartzSpaceWiki

Source

Wikipedia, "Schwartz space", revision oldid=1360762580 (https://en.wikipedia.org/w/index.php?title=Schwartz_space&oldid=1360762580), section "Properties — Analytic properties", 4th bullet

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph