Smooth Approximation with Uniform Gradient Control

This gives a smooth approximation scheme for a function with Lipschitz gradient.

Let $E$ be a finite-dimensional real inner-product space with its Borel structure. Let $U:E\to\mathbb R$ be $C^1$, and suppose that $\nabla U$ is Lipschitz with constant $G\in[0,\infty)$. Then there exists a sequence $U_k:E\to\mathbb R$ such that:

1. Every $U_k$ is $C^\infty$.
2. For every $k$ and $x\in E$,

3. Every $\nabla U_k$ is Lipschitz with the same constant $G$.
4. For every $x$, $U_k(x)\to U(x)$ as $k\to\infty$.
5. For almost every $x$ with respect to volume measure, $D(\nabla U_k)(x)$ converges to $D(\nabla U)(x)$ as $k\to\infty$.

The sequence is a reusable regularization device preserving the Lipschitz-gradient bound while providing almost-everywhere Hessian convergence.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem exists_contDiff_approx_of_lipschitz_gradient
    {U : E → ℝ} (hU : ContDiff ℝ 1 U) {G : NNReal} (hG : LipschitzWith G (gradient U)) :
    ∃ Uk : ℕ → E → ℝ, (∀ k, ContDiff ℝ ∞ (Uk k)) ∧
      (∀ k x, ‖gradient (Uk k) x - gradient U x‖ ≤ G / ((k : ℝ) + 1)) ∧
      (∀ k, LipschitzWith G (gradient (Uk k))) ∧
      (∀ x, Tendsto (fun k => Uk k x) atTop (𝓝 (U x))) ∧
      (∀ᵐ x ∂(volume : Measure E), Tendsto (fun k => fderiv ℝ (gradient (Uk k)) x) atTop
        (𝓝 (fderiv ℝ (gradient U) x)))

Module navigation

Module: Analysis/Mollification/Hessian.

Supporting theorems: hasFDerivAt_convolution_normed_of_lipschitz, gradient_convolution_normed.

Previous: gradient_convolution_normed.

Source excerpt, lines 268–275 · Frozen source 408915f.