Mollification on W^{1,p}(ℝⁿ)

The smooth approximate identity TauCeti.normedBumpLp averages the translates of an Lᵖ class against a normalized bump. Applied to value-gradient jets it preserves W^{1,p}(ℝⁿ): translation preserves the weak-derivative identities on the whole space (TauCeti.Sobolev1JetLp.translateLp_mem_w1pSubmodule), and the average is a Bochner integral of translates, which stays in the closed subspace W^{1,p}(ℝⁿ). This gives the mollification operator TauCeti.W1p.normedBumpL on W^{1,p}(ℝⁿ), and the strong convergence of the approximate identity on jets is exactly its convergence to the identity in the Sobolev norm (TauCeti.W1p.tendsto_normedBumpL). No commutation of derivatives with convolution is needed: the weak gradient is mollified together with the value because both are components of one jet.

If the jet of u vanishes outside a compact set, the mollified jet has a smooth compactly supported representative (TauCeti.normedBumpLp_ae_eq_convolution), so the mollification is a test function (TauCeti.W1p.normedBumpL_mem_range_of_ae_eq_zero).

The ambient space is any finite-dimensional real inner product space E with an additive Haar measure; ℝⁿ stands for the whole-space case Ω = ⊤.

Main declarations

• TauCeti.Sobolev1JetLp.normedBumpLp_mem_w1pSubmodule: mollification preserves W^{1,p}(ℝⁿ).
• TauCeti.W1p.normedBumpL: mollification by a normalized smooth bump, as a continuous linear operator on W^{1,p}(ℝⁿ).
• TauCeti.W1p.value_normedBumpL, TauCeti.W1p.gradient_normedBumpL: the value and weak gradient of a mollification are the Lᵖ mollifications of the value and weak gradient.
• TauCeti.W1p.norm_normedBumpL_le_one: this operator is a contraction.
• TauCeti.W1p.tendsto_normedBumpL: mollifications with shrinking bumps converge in W^{1,p}.
• TauCeti.W1p.normedBumpL_mem_range_of_ae_eq_zero: mollifying a Sobolev function whose jet vanishes outside a compact set produces a test function.

References

L. C. Evans, Partial Differential Equations, §5.3.1; H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Theorem 9.2.

theorem TauCeti.instIsAddHaarMeasureRestrictCoeOpensTop_tauCeti_1 {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] : (mu.restrict ↑⊤).IsAddHaarMeasure

The whole-space restriction of an additive Haar measure is the measure itself.

theorem TauCeti.Sobolev1JetLp.normedBumpLp_mem_w1pSubmodule {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (phi : ContDiffBump 0) {J : ↥(Sobolev1JetLp mu ⊤ p)} (hJ : J ∈ w1pSubmodule mu ⊤ p) : (normedBumpLp hp phi (mu.restrict ↑⊤)) J ∈ w1pSubmodule mu ⊤ p

Mollification preserves W^{1,p}(ℝⁿ). The mollified jet is a Bochner integral of translates of the jet, each of which lies in the closed subspace W^{1,p}(ℝⁿ).

noncomputable def TauCeti.W1p.normedBumpL {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (phi : ContDiffBump 0) : ↥(W1p mu ⊤ p) →L[ℝ] ↥(W1p mu ⊤ p)

Mollification on W^{1,p}(ℝⁿ): averaging the translates of a Sobolev function against the normalized form of a smooth bump, as a continuous linear operator. The value and the weak gradient are mollified together, as the two components of one Lᵖ jet.

Equations

• TauCeti.W1p.normedBumpL hp phi = (TauCeti.normedBumpLp hp phi (mu.restrict ↑⊤) ∘SL (↑(TauCeti.w1pSubmodule mu ⊤ p)).subtypeL).codRestrict ↑(TauCeti.w1pSubmodule mu ⊤ p) ⋯

theorem TauCeti.W1p.coe_normedBumpL {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (phi : ContDiffBump 0) (u : ↥(W1p mu ⊤ p)) : ↑((normedBumpL hp phi) u) = (normedBumpLp hp phi (mu.restrict ↑⊤)) ↑u

The jet of the mollification is the mollification of the jet.

theorem TauCeti.Sobolev1JetLp.value_normedBumpLp {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (phi : ContDiffBump 0) (J : ↥(Sobolev1JetLp mu ⊤ p)) : value ((normedBumpLp hp phi (mu.restrict ↑⊤)) J) = (normedBumpLp hp phi (mu.restrict ↑⊤)) (value J)

The value component of a mollified whole-space jet is the mollification of its value component.

theorem TauCeti.Sobolev1JetLp.gradient_normedBumpLp {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (phi : ContDiffBump 0) (J : ↥(Sobolev1JetLp mu ⊤ p)) : gradient ((normedBumpLp hp phi (mu.restrict ↑⊤)) J) = (normedBumpLp hp phi (mu.restrict ↑⊤)) (gradient J)

The gradient component of a mollified whole-space jet is the mollification of its gradient component.

theorem TauCeti.W1p.value_normedBumpL {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (phi : ContDiffBump 0) (u : ↥(W1p mu ⊤ p)) : value ((normedBumpL hp phi) u) = (normedBumpLp hp phi (mu.restrict ↑⊤)) (value u)

The value of a mollified Sobolev function is the Lᵖ mollification of its value.

theorem TauCeti.W1p.gradient_normedBumpL {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (phi : ContDiffBump 0) (u : ↥(W1p mu ⊤ p)) : gradient ((normedBumpL hp phi) u) = (normedBumpLp hp phi (mu.restrict ↑⊤)) (gradient u)

The weak gradient of a mollified Sobolev function is the Lᵖ mollification of its weak gradient.

theorem TauCeti.W1p.norm_normedBumpL_le_one {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (phi : ContDiffBump 0) : ‖normedBumpL hp phi‖ ≤ 1

Mollification by a normalized nonnegative bump does not increase the W^{1,p} norm when p < ∞.

theorem TauCeti.W1p.tendsto_normedBumpL {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) {I : Type u_2} {l : Filter I} {phi : I → ContDiffBump 0} (hphi : Filter.Tendsto (fun (i : I) => (phi i).rOut) l (nhds 0)) (u : ↥(W1p mu ⊤ p)) : Filter.Tendsto (fun (i : I) => (normedBumpL hp (phi i)) u) l (nhds u)

Mollification converges in W^{1,p}(ℝⁿ). For 1 ≤ p < ∞, mollifying a Sobolev function with normalized smooth bumps whose radii shrink to zero converges to it in the Sobolev norm.

theorem TauCeti.W1p.normedBumpL_mem_range_of_ae_eq_zero {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (phi : ContDiffBump 0) {u : ↥(W1p mu ⊤ p)} {K : Set E} (hK : IsCompact K) (hu : ∀ᵐ (x : E) ∂mu.restrict ↑⊤, x ∉ K → ↑↑↑u x = 0) : (normedBumpL hp phi) u ∈ (ofTestFunctionₗ mu ⊤ p).range

A compactly supported Sobolev function mollifies to a test function. If the jet of u vanishes almost everywhere outside a compact set, its mollification has a smooth compactly supported representative.