Shifting before mollifying

Mollifying a function near the boundary of its domain asks for values the function does not have. The global approximation theorem answers by shifting first: the function is translated into the domain far enough that the mollifier of the shift only ever sees points where the function is defined, and then the shift and the mollifier radius are sent to zero together.

This file proves that the two limits compose, so that a shifted mollification converges to the function it started from. The identity that makes it work is that convolution commutes with translation, so the mollification error of the shift is the shift of the mollification error, which has the same norm.

Main declarations

• EllipticPdes.Extension.convolution_comp_translate: convolution commutes with translation.
• EllipticPdes.Extension.tendsto_eLpNorm_translate_convolution_sub: a shifted mollification converges in Lᵖ to the function, as the shift and the radius go to zero together.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §5.3.3, Theorem 3.

theorem EllipticPdes.Extension.convolution_comp_translate {d : ℕ} (f ρ : EuclideanSpace ℝ (Fin d) → ℝ) (h x : EuclideanSpace ℝ (Fin d)) : MeasureTheory.convolution (fun (y : EuclideanSpace ℝ (Fin d)) => f (y + h)) ρ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x = MeasureTheory.convolution f ρ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume (x + h)

Convolution commutes with translation. Convolving a translate is translating the convolution, by the change of variables t ↦ t + h in the defining integral.

theorem EllipticPdes.Extension.tendsto_eLpNorm_translate_convolution_sub {d : ℕ} {p : ℝ} (hp : 1 ≤ p) {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume) {ι : Type u_1} {l : Filter ι} {φ : ι → ContDiffBump 0} {K : ℝ} {hv : ι → EuclideanSpace ℝ (Fin d)} (hφ : Filter.Tendsto (fun (i : ι) => (φ i).rOut) l (nhds 0)) (hK : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn) (hh : Filter.Tendsto hv l (nhds 0)) : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (MeasureTheory.convolution (fun (y : EuclideanSpace ℝ (Fin d)) => f (y + hv i)) ((φ i).normed MeasureTheory.volume) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume - f) (ENNReal.ofReal p) MeasureTheory.volume) l (nhds 0)

Convergence of a shifted mollification. For f in Lᵖ, translating by hᵢ and mollifying at radius (φ i).rOut gives a family converging to f in Lᵖ, as soon as both the shift and the radius tend to zero.

The error splits into the mollification error of the shift and the shift error. The first is the shift of the mollification error, by convolution_comp_translate, and translation is an Lᵖ isometry, so it has the norm of the mollification error of f itself.