L² translation estimate

For a continuously differentiable, compactly supported f : ℝⁿ → ℝ, the L² norm of the difference between f and its translate f(· + h) is controlled by the displacement ‖h‖ and the L² norm of the gradient: ∫ x, (f (x + h) - f x) ^ 2 ≤ ‖h‖ ^ 2 * ∫ x, ‖fderiv ℝ f x‖ ^ 2.

This is the gradient-to-L² translation estimate, the equicontinuity input to the Fréchet-Kolmogorov precompactness criterion and hence to the Rellich-Kondrachov compact embedding.

The argument writes f (x + h) - f x = ∫ t in 0..1, (fderiv ℝ f (x + t • h)) h by the fundamental theorem of calculus along the segment t ↦ x + t • h, squares through the one-variable Cauchy-Schwarz bound on [0, 1] (MeasureTheory.sq_intervalIntegral_le), integrates over x, swaps the order of integration (Tonelli, the integrand being a continuous function supported in a bounded slab), and uses translation invariance of the Lebesgue integral to collapse the inner translate back to the gradient integral.

Main results

• MeasureTheory.integral_sq_sub_translation_le: the L² translation estimate.

theorem MeasureTheory.integral_sq_sub_translation_le {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : ContDiff ℝ 1 f) (hfc : HasCompactSupport f) (h : EuclideanSpace ℝ (Fin n)) : ∫ (x : EuclideanSpace ℝ (Fin n)), (f (x + h) - f x) ^ 2 ≤ ‖h‖ ^ 2 * ∫ (x : EuclideanSpace ℝ (Fin n)), ‖fderiv ℝ f x‖ ^ 2

L² translation estimate. For a continuously differentiable, compactly supported f : ℝⁿ → ℝ, ∫ x, (f (x + h) - f x) ^ 2 ≤ ‖h‖ ^ 2 * ∫ x, ‖fderiv ℝ f x‖ ^ 2.