Prove2Me

The LpL^p norm of a translation difference of a C1C^1 function is bounded by ∣h∣ ∥Dg∥Lp|h|\,\|Dg\|_{L^p}

Proved
CauchyRiemannIndex.eLpNorm_translate_sub_le

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

measure-theoryreal-analysissobolev-spaces

Let 1≤p<∞1\le p<\infty, let FF be a real Banach space, let g:Rm→Fg:\mathbb R^m\to F be continuously differentiable, and let h∈Rmh\in\mathbb R^m. Then

(∫Rm∣g(x+h)−g(x)∣p dx)1/p  ≤  ∣h∣ (∫Rm∥Dg(x)∥p dx)1/p,\Big(\int_{\mathbb R^m}\big|g(x+h)-g(x)\big|^p\,dx\Big)^{1/p}\;\le\;|h|\,\Big(\int_{\mathbb R^m}\|Dg(x)\|^p\,dx\Big)^{1/p},

where ∥Dg(x)∥\|Dg(x)\| is the operator norm of the derivative of gg at xx.

This is the standard modulus-of-continuity bound for translations in LpL^p in terms of the gradient. It gives equicontinuity of translations, uniformly over families with bounded W1,pW^{1,p} norm, and is used for compactness statements for Sobolev-bounded families. No integrability of gg or DgDg is assumed; the right-hand side may be infinite.

Formalization Note. pp is in ℝ≥0∞; norms are written with eLpNorm for Lebesgue measure on EuclideanSpace ℝ (Fin m), ∣h∣|h| is ENNReal.ofReal ‖h‖, DgDg is fderiv ℝ g and C1C^1 is ContDiff ℝ 1.

Preamble
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Formal statement
namespace CauchyRiemannIndex

open MeasureTheory
open scoped ENNReal NNReal

/-- For `1 ≤ p < ∞` and a `C¹` map `g : ℝᵐ → F` into a Banach space, the `Lᵖ` norm of the
translation difference `x ↦ g (x + h) - g x` is at most `|h|` times the `Lᵖ` norm of `|Dg|`. -/
theorem eLpNorm_translate_sub_le {m : ℕ} {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    [CompleteSpace F] (p : ℝ≥0∞) (hp : 1 ≤ p) (hp' : p ≠ ⊤)
    (g : EuclideanSpace ℝ (Fin m) → F) (hg : ContDiff ℝ 1 g) (h : EuclideanSpace ℝ (Fin m)) :
    eLpNorm (fun x => g (x + h) - g x) p volume ≤
      ENNReal.ofReal ‖h‖ * eLpNorm (fun x => ‖fderiv ℝ g x‖) p volume := by
  sorry

end CauchyRiemannIndex
Source
C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 4, p. 74 (the compact inclusion used after Lemma 4.13); standard Sobolev space theory, e.g. H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Springer 2011, Proposition 9.3 and Theorem 9.16

View graph