Local convergence of mollifications after zero extension

For a subset t ⊆ s of a measurable set s, extend an Lᵖ(s) function by zero to the ambient space, average it against a normalized smooth bump, and restrict the result to t. As the radius shrinks, this converges in Lᵖ(t) to the original function restricted to t whenever 1 ≤ p < ∞. The result applies to every Banach-valued field, including all weak derivative fields of a Sobolev function, and requires no regularity of the boundary of s.

This is the local form of the strong approximate-identity theorem. It does not assert that the zero extension is weakly differentiable across the boundary.

The zero-extension convolution is also identified almost everywhere with the abstract Lᵖ average. Thus the same mollification can be used through its norm-convergent Lᵖ class or through its smooth pointwise representative.

Main declarations

• TauCeti.normedBumpLp_extendByZero_ae_eq_convolution: the abstract mollification of a zero extension has the classical convolution as a representative.
• TauCeti.tendsto_normedBumpLp_extendByZero_restrict: zero-extension mollifications converge locally in Lᵖ.

References

L. C. Evans, Partial Differential Equations, Chapter 5, §5.3.1.

theorem TauCeti.instFiniteDimensionalReal_tauCeti_1 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E] : FiniteDimensional ℝ E

theorem TauCeti.instIsAddHaarMeasureRestrictUniv_tauCeti {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] : (mu.restrict Set.univ).IsAddHaarMeasure

theorem TauCeti.normedBumpLp_extendByZero_ae_eq_convolution {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] {s : Set E} (hp : p ≠ ⊤) (phi : ContDiffBump 0) (hs : MeasurableSet s) (f : ↥(MeasureTheory.Lp F p (mu.restrict s))) : ↑↑((normedBumpLp hp phi (mu.restrict Set.univ)) ((extendByZeroLpₗᵢ ℝ mu hs ⋯) f)) =ᵐ[mu.restrict Set.univ] MeasureTheory.convolution (phi.normed (mu.restrict Set.univ)) (s.indicator ↑↑f) (ContinuousLinearMap.lsmul ℝ ℝ) (mu.restrict Set.univ)

Mollifying a zero extension is represented almost everywhere by convolving the pointwise zero extension with the normalized bump. This identifies the abstract Lᵖ average used for norm convergence with the classical smooth convolution used for differentiation.

theorem TauCeti.tendsto_normedBumpLp_extendByZero_restrict {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] {s t : Set E} (hp : p ≠ ⊤) (hs : MeasurableSet s) (hts : t ⊆ s) {I : Type u_3} {l : Filter I} {phi : I → ContDiffBump 0} (hphi : Filter.Tendsto (fun (i : I) => (phi i).rOut) l (nhds 0)) (f : ↥(MeasureTheory.Lp F p (mu.restrict s))) : Filter.Tendsto (fun (i : I) => (MeasureTheory.Lp.LpToLpOfMeasureLeSMul tendsto_normedBumpLp_extendByZero_restrict._proof_1 ⋯) ((normedBumpLp hp (phi i) (mu.restrict Set.univ)) ((extendByZeroLpₗᵢ ℝ mu hs ⋯) f))) l (nhds ((MeasureTheory.Lp.LpToLpOfMeasureLeSMul tendsto_normedBumpLp_extendByZero_restrict._proof_1 ⋯) f))

Zero-extend an Lᵖ(s) field, mollify it, and restrict to t ⊆ s. For p < ∞, this converges in Lᵖ(t) to the original field restricted to t.