Mollification of weakly differentiable functions

This file proves the identity at the heart of mollification in Sobolev spaces. If u' is the weak derivative of u in the direction v on an open domain and rho is smooth with compact support, then

D_v (u ⋆ rho) = u' ⋆ rho

at every point x for which x - tsupport rho lies in the domain. The convolved function (and, for the Fréchet form, its weak derivative field) is assumed locally integrable on the whole space; zero extensions of domain Lᵖ functions satisfy this assumption. No weak derivative identity outside the domain is required.

The results hold for functions with values in an arbitrary real Banach space and for any s-finite, left-invariant measure on a real normed space, such as an additive Haar measure.

This identity applies successively to the derivative fields of a Sobolev function, and is the analytic input to local smooth approximation and Meyers--Serrin density.

Main statements

• TauCeti.HasWeakLineDerivOn.hasLineDerivAt_convolution_right: convolution by a smooth, compactly supported scalar kernel turns a local weak directional derivative into the corresponding classical directional derivative.
• TauCeti.HasWeakFDerivOn.hasFDerivAt_convolution_right: the Fréchet form, identifying the derivative with the convolution of the weak derivative field.
• TauCeti.HasWeakLineDerivOn.lineDeriv_convolution_right and TauCeti.HasWeakFDerivOn.fderiv_convolution_right: the corresponding derivative equations.

References

L. C. Evans, Partial Differential Equations, Section 5.3.1, Theorem 1; L. C. Evans and R. F. Gariepy, Measure Theory and Fine Properties of Functions, Section 4.1.1.

theorem TauCeti.HasWeakLineDerivOn.hasLineDerivAt_convolution_right {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddLeftInvariant] [MeasureTheory.SFinite mu] {Omega : TopologicalSpace.Opens E} {u u' : E → F} {v : E} (h : HasWeakLineDerivOn mu Omega u u' v) (hu : MeasureTheory.LocallyIntegrable u mu) (rho : E → ℝ) (hrho : ContDiff ℝ (↑⊤) rho) (hrho_cpt : HasCompactSupport rho) (x : E) (hx : ∀ y ∈ tsupport rho, x - y ∈ Omega) : HasLineDerivAt ℝ (MeasureTheory.convolution u rho (ContinuousLinearMap.lsmul ℝ ℝ).flip mu) (MeasureTheory.convolution u' rho (ContinuousLinearMap.lsmul ℝ ℝ).flip mu x) x v

A weak derivative commutes with convolution by a smooth compactly supported kernel. If u' is the weak derivative of u in the direction v on Omega, then the convolution of u with rho has directional derivative (u' ⋆ rho) x in the direction v at every point x whose translated kernel support x - tsupport rho is contained in Omega.

theorem TauCeti.HasWeakLineDerivOn.lineDeriv_convolution_right {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddLeftInvariant] [MeasureTheory.SFinite mu] {Omega : TopologicalSpace.Opens E} {u u' : E → F} {v : E} (h : HasWeakLineDerivOn mu Omega u u' v) (hu : MeasureTheory.LocallyIntegrable u mu) (rho : E → ℝ) (hrho : ContDiff ℝ (↑⊤) rho) (hrho_cpt : HasCompactSupport rho) (x : E) (hx : ∀ y ∈ tsupport rho, x - y ∈ Omega) : lineDeriv ℝ (MeasureTheory.convolution u rho (ContinuousLinearMap.lsmul ℝ ℝ).flip mu) x v = MeasureTheory.convolution u' rho (ContinuousLinearMap.lsmul ℝ ℝ).flip mu x

The directional derivative of a convolution with a smooth compactly supported kernel is the convolution of the weak directional derivative with that kernel.

theorem TauCeti.HasWeakFDerivOn.hasFDerivAt_convolution_right {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddLeftInvariant] [MeasureTheory.SFinite mu] {Omega : TopologicalSpace.Opens E} {u : E → F} {U : E → E →L[ℝ] F} (h : HasWeakFDerivOn mu Omega u U) (hu : MeasureTheory.LocallyIntegrable u mu) (hU : MeasureTheory.LocallyIntegrable U mu) (rho : E → ℝ) (hrho : ContDiff ℝ (↑⊤) rho) (hrho_cpt : HasCompactSupport rho) (x : E) (hx : ∀ y ∈ tsupport rho, x - y ∈ Omega) : HasFDerivAt (MeasureTheory.convolution u rho (ContinuousLinearMap.lsmul ℝ ℝ).flip mu) (MeasureTheory.convolution U rho (ContinuousLinearMap.lsmul ℝ ℝ).flip mu x) x

The Fréchet derivative of a mollification is the mollification of the weak derivative. If U is a weak derivative field of u on Omega and both are locally integrable on the whole space, the convolution of u with a smooth compactly supported scalar kernel rho has derivative (U ⋆ rho) x at every point x whose translated kernel support x - tsupport rho lies in Omega.

theorem TauCeti.HasWeakFDerivOn.fderiv_convolution_right {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddLeftInvariant] [MeasureTheory.SFinite mu] {Omega : TopologicalSpace.Opens E} {u : E → F} {U : E → E →L[ℝ] F} (h : HasWeakFDerivOn mu Omega u U) (hu : MeasureTheory.LocallyIntegrable u mu) (hU : MeasureTheory.LocallyIntegrable U mu) (rho : E → ℝ) (hrho : ContDiff ℝ (↑⊤) rho) (hrho_cpt : HasCompactSupport rho) (x : E) (hx : ∀ y ∈ tsupport rho, x - y ∈ Omega) : fderiv ℝ (MeasureTheory.convolution u rho (ContinuousLinearMap.lsmul ℝ ℝ).flip mu) x = MeasureTheory.convolution U rho (ContinuousLinearMap.lsmul ℝ ℝ).flip mu x

The Fréchet derivative of a convolution with a smooth compactly supported kernel is the convolution of the weak Fréchet derivative field with that kernel.