Smooth approximate identities in arbitrary-order Sobolev spaces

On the whole space, average translations of a function in W^{k,p} against a normalized smooth bump. Translation preserves every weak derivative and the full iterated graph norm, so this gives a contraction on W^{k,p} when p < ∞. The same strong continuity of translation implies that these averages converge in the Sobolev norm when the bump radii tend to zero.

The value and every highest weak derivative of the Sobolev average are the corresponding Lᵖ averages. These identities make the construction usable together with the pointwise convolution and smoothness theory for mollifiers.

The argument is the standard mollification proof from L. C. Evans, Partial Differential Equations, §5.3.1.

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

noncomputable def TauCeti.Wkp.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) (k : ℕ) : Wkp mu ⊤ p k →L[ℝ] Wkp mu ⊤ p k

Mollification by a normalized smooth bump on the whole-space Sobolev space W^{k,p}, as a continuous linear operator. It averages the Sobolev translations in the Bochner sense. The restriction p < ∞ supplies the strong continuity that makes this integrand Bochner integrable.

Equations

• TauCeti.Wkp.normedBumpL hp phi k = TauCeti.normedBumpAverageL phi (mu.restrict ↑⊤) (fun (h : E) => TauCeti.Wkp.translateLIE h k) ⋯

theorem TauCeti.Wkp.normedBumpL_apply {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) (k : ℕ) (u : Wkp mu ⊤ p k) : (normedBumpL hp phi k) u = ∫ (t : E) in ↑⊤, phi.normed (mu.restrict ↑⊤) t • translate (-t) k u ∂mu

The defining Bochner-integral formula for Sobolev mollification.

theorem TauCeti.Wkp.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) (k : ℕ) : ‖normedBumpL hp phi k‖ ≤ 1

Mollification by a normalized nonnegative bump does not increase the W^{k,p} norm.

@[simp]

theorem TauCeti.Wkp.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) (k : ℕ) (u : Wkp mu ⊤ p k) : value k ((normedBumpL hp phi k) u) = (normedBumpLp hp phi (mu.restrict ↑⊤)) (value k u)

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

@[simp]

theorem TauCeti.Wkp.normedBumpL_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) : normedBumpL hp phi 0 = normedBumpLp hp phi (mu.restrict ↑⊤)

At order zero, Sobolev mollification is the existing Lᵖ approximate identity.

@[simp]

theorem TauCeti.Wkp.normedBumpL_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 = W1p.normedBumpL hp phi

At order one, Sobolev mollification agrees with the existing W^{1,p} mollifier.

theorem TauCeti.Wkp.lowerOrder_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) (k : ℕ) (u : Wkp mu ⊤ p (k + 1)) : lowerOrder k ((normedBumpL hp phi (k + 1)) u) = (normedBumpL hp phi k) (lowerOrder k u)

Mollification commutes with forgetting the highest weak derivative.

theorem TauCeti.Wkp.iteratedGradient_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) (k : ℕ) (u : Wkp mu ⊤ p (k + 1)) : iteratedGradient k ((normedBumpL hp phi (k + 1)) u) = (normedBumpLp hp phi (mu.restrict ↑⊤)) (iteratedGradient k u)

The highest weak derivative of a Sobolev mollification is the Lᵖ mollification of the highest weak derivative.

theorem TauCeti.Wkp.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)) (k : ℕ) (u : Wkp mu ⊤ p k) : Filter.Tendsto (fun (i : I) => (normedBumpL hp (phi i) k) u) l (nhds u)

Smooth approximate identity in W^{k,p}(ℝⁿ). Normalized smooth bumps whose outer radii tend to zero converge strongly to the identity on every finite-exponent whole-space Sobolev space.