Strong continuity of translations in finite-p Sobolev norms

Proved

HunterPDE.Sobolev.sobolevNorm_translation_small

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

sobolev-spacestranslationweak-derivatives

Let $k\ge0$ , $1\le p<\infty$ , and $f\in W^{k,p}(\mathbb R^n)$ . Translations are continuous at the identity in the Sobolev norm:

\forall\varepsilon>0\;\exists r>0\;\forall a,\quad |a|<r\Longrightarrow \|f-\tau_a f\|_{W^{k,p}(\mathbb R^n)}<\varepsilon,\qquad \tau_a f(x)=f(x-a).

The tolerance may be an extended nonnegative real. The norm uses every weak derivative through order $k$ . The finite-p assumption is essential for general Sobolev functions. This assertion imposes no support or boundary hypothesis.

Preamble

import Definitions.Def_HunterPDE_Sobolev_SobolevSpace
open MeasureTheory HunterPDE.Sobolev
open scoped ENNReal
set_option autoImplicit false

Formal statement

theorem HunterPDE.Sobolev.sobolevNorm_translation_small {n k : ℕ} {p : ENNReal}
    (hp : 1 ≤ p) (hp' : p ≠ ∞)
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : MemW k p Set.univ f)
    (ε : ENNReal) (hε : 0 < ε) :
    ∃ r : ℝ, 0 < r ∧ ∀ a : EuclideanSpace ℝ (Fin n), ‖a‖ < r →
      sobolevNorm k p Set.univ (f - (fun x => f (x - a))) < ε := by sorry

Source

Strong Lp continuity of translations applied to the finitely many weak derivatives in Definition 3.23. J. K. Hunter, Notes on Partial Differential Equations, revised 6/18/2014, https://www.math.ucdavis.edu/~hunter/pdes/ch3.pdf, printed pp.58–60 (Sobolev norm and approximation) and p.73 (translation/mollification outline after Theorem 3.44). The epsilon-delta statement is the whole-space arbitrary-order analytic ingredient of that outline.

View graph