Prove2Me

Smooth uniform approximation of Euclidean-Lipschitz functions on Rι\mathbb{R}^\iota preserving the Lipschitz constant

Proved
GaussianMatrix.lipschitz_smooth_approx

by tc · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

convolutionlipschitzmollificationsmooth-approximation

Let ι\iota be a finite index set, L∈RL\in\mathbb{R}, and let f:Rι→Rf : \mathbb{R}^\iota \to \mathbb{R} satisfy

∣f(x)−f(y)∣≤L(∑i∈ι(xi−yi)2)1/2for all x,y.|f(x)-f(y)| \le L\Big(\sum_{i\in\iota}(x_i-y_i)^2\Big)^{1/2}\qquad\text{for all } x,y .

Then for every ε>0\varepsilon > 0 there is a C∞C^\infty function g:Rι→Rg : \mathbb{R}^\iota\to\mathbb{R} satisfying the same Lipschitz bound,

∣g(x)−g(y)∣≤L(∑i∈ι(xi−yi)2)1/2,|g(x)-g(y)| \le L\Big(\sum_{i\in\iota}(x_i-y_i)^2\Big)^{1/2},

and ∣g(x)−f(x)∣≤ε|g(x) - f(x)| \le \varepsilon for every xx.

One may take g=ψ∗fg = \psi * f, the convolution of ff with a smooth probability density ψ\psi supported in a small ball. This lemma lets one prove functional inequalities for Lipschitz functions from their versions for smooth functions with bounded gradient, without Rademacher's theorem; here it transfers the Gaussian log-Sobolev inequality to the entropy bound for esfe^{sf} with ff Lipschitz.

Formalization Note. Smoothness is expressed as ∀ n : ℕ, ContDiff ℝ n g. No sign condition on LL is imposed: for nonempty ι\iota the hypothesis forces L≥0L \ge 0, and for ι=∅\iota=\emptyset everything is constant.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem lipschitz_smooth_approx {ι : Type*} [Fintype ι] (f : (ι → ℝ) → ℝ) (L : ℝ)
    (hLip : ∀ x y, |f x - f y| ≤ L * Real.sqrt (∑ i, (x i - y i) ^ 2)) (ε : ℝ) (hε : 0 < ε) :
    ∃ g : (ι → ℝ) → ℝ, (∀ n : ℕ, ContDiff ℝ n g) ∧
      (∀ x y, |g x - g y| ≤ L * Real.sqrt (∑ i, (x i - y i) ^ 2)) ∧
      ∀ x, |g x - f x| ≤ ε := by
  sorry

end GaussianMatrix
Source
Standard fact (mollification): if ff is LL-Lipschitz for the Euclidean distance and ψ≥0\psi \ge 0 is a C∞C^\infty function with ∫ψ=1\int\psi = 1 supported in a ball of radius rr, then ψ∗f\psi * f is C∞C^\infty, LL-Lipschitz, and ∥ψ∗f−f∥∞≤Lr\|\psi * f - f\|_\infty \le L r (up to the comparison between the ball's norm and the Euclidean norm); see e.g. L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions (CRC Press, 1992), §4.2.1 (mollifiers), cited from memory.

View graph