Continuity of translation in Lᵖ

An Lᵖ function is close in Lᵖ to its own translates by small vectors. This is the statement the global approximation theorem shifts on: a function is moved into the domain by a small translation, and the shift has to be small in the norm the approximation is measured in.

Mathlib has the two halves and not the statement. Translation is measure preserving, so it is an Lᵖ isometry, and the continuous compactly supported functions are dense in Lᵖ (MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le). Between them the usual three-term argument runs: approximate, translate the approximant, and pay twice for the approximation.

For a continuous compactly supported g the translate estimate is uniform continuity together with one compact set containing the support of every difference g(· + h) - g with ‖h‖ ≤ 1, so the sup bound converts to an Lᵖ bound against the measure of that set.

Main declarations

• EllipticPdes.Analysis.tendsto_eLpNorm_translate_sub: the Lᵖ distance to a translate tends to zero with the translation.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §5.3.3, Theorem 3; H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Lemma 4.3.

theorem EllipticPdes.Analysis.memLp_comp_translate {d : ℕ} {p : ENNReal} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (h : EuclideanSpace ℝ (Fin d)) : MeasureTheory.MemLp (fun (y : EuclideanSpace ℝ (Fin d)) => f (y + h)) p MeasureTheory.volume

A translate of an Lᵖ function is an Lᵖ function, translation being measure preserving.

theorem EllipticPdes.Analysis.tendsto_eLpNorm_translate_sub_of_hasCompactSupport {d : ℕ} {p : ENNReal} {g : EuclideanSpace ℝ (Fin d) → ℝ} (hgc : Continuous g) (hgs : HasCompactSupport g) : Filter.Tendsto (fun (h : EuclideanSpace ℝ (Fin d)) => MeasureTheory.eLpNorm (fun (y : EuclideanSpace ℝ (Fin d)) => g (y + h) - g y) p MeasureTheory.volume) (nhds 0) (nhds 0)

Compactly supported case. For a continuous g with compact support, the Lᵖ distance to its translates tends to zero: uniform continuity bounds the difference uniformly, and every difference with ‖h‖ ≤ 1 is supported in one compact set.

theorem EllipticPdes.Analysis.tendsto_eLpNorm_translate_sub {d : ℕ} {p : ENNReal} (hp1 : 1 ≤ p) (hptop : p ≠ ⊤) {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : Filter.Tendsto (fun (h : EuclideanSpace ℝ (Fin d)) => MeasureTheory.eLpNorm (fun (y : EuclideanSpace ℝ (Fin d)) => f (y + h) - f y) p MeasureTheory.volume) (nhds 0) (nhds 0)

Continuity of translation in Lᵖ. The Lᵖ distance between an Lᵖ function and its translate tends to zero with the translation.

The three-term argument: approximate f by a continuous compactly supported g, translate g, and count the approximation twice, once on each side. Translation being an Lᵖ isometry is what makes the two terms equal.