Mollification of Lipschitz functions

Let ψ be K-Lipschitz on a finite-dimensional real normed space and let ρ be a smooth bump centred at 0. The derivative in a direction v of the mollification ρ.normed μ ⋆ ψ is the mollification of the directional derivative ∂_v ψ, which exists almost everywhere by Rademacher's theorem and is the weak derivative of ψ. Hence these derivatives are bounded by K ‖v‖. When the radii shrink to zero with a bounded ratio of outer to inner radius, they converge to ∂_v ψ almost everywhere, by the Lebesgue differentiation theorem. By dominated convergence, integrals against the mollifications and against their directional derivatives then converge to the integrals against ψ and ∂_v ψ.

These are the estimates that pass an identity proved for smooth factors to Lipschitz ones by dominated convergence, as in the Leibniz rule TauCeti.HasWeakLineDerivOn.lipschitzWith_smul.

Main results

• LipschitzWith.fderiv_normed_convolution_apply: the directional derivative of the mollification is the mollification of the almost-everywhere directional derivative.
• LipschitzWith.norm_fderiv_normed_convolution_apply_le: these derivatives are bounded by K ‖v‖.
• LipschitzWith.ae_tendsto_fderiv_normed_convolution_apply: they converge almost everywhere to the directional derivative as the bumps shrink.
• LipschitzWith.tendsto_integral_normed_convolution_smul and LipschitzWith.tendsto_integral_fderiv_normed_convolution_apply_smul: integrals against the mollifications and against their directional derivatives converge as the bumps shrink.

References

• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised ed., §4.2.2 and §4.2.3.

theorem LipschitzWith.fderiv_normed_convolution_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {K : NNReal} {ψ : E → ℝ} (hψ : LipschitzWith K ψ) (ρ : ContDiffBump 0) (x v : E) : (fderiv ℝ (MeasureTheory.convolution (ρ.normed μ) ψ (ContinuousLinearMap.lsmul ℝ ℝ) μ) x) v = MeasureTheory.convolution (ρ.normed μ) (fun (y : E) => lineDeriv ℝ ψ y v) (ContinuousLinearMap.lsmul ℝ ℝ) μ x

The derivative in a direction v of the mollification of a Lipschitz function is the mollification of its directional derivative ∂_v ψ, which exists almost everywhere.

theorem LipschitzWith.norm_fderiv_normed_convolution_apply_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {K : NNReal} {ψ : E → ℝ} (hψ : LipschitzWith K ψ) (ρ : ContDiffBump 0) (x v : E) : ‖(fderiv ℝ (MeasureTheory.convolution (ρ.normed μ) ψ (ContinuousLinearMap.lsmul ℝ ℝ) μ) x) v‖ ≤ ↑K * ‖v‖

The derivatives in a direction v of the mollifications of a K-Lipschitz function are bounded by K ‖v‖.

theorem LipschitzWith.ae_tendsto_fderiv_normed_convolution_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {K : NNReal} {ψ : E → ℝ} (hψ : LipschitzWith K ψ) {ι : Type u_2} {l : Filter ι} {ρ : ι → ContDiffBump 0} {C : ℝ} (hρ : Filter.Tendsto (fun (i : ι) => (ρ i).rOut) l (nhds 0)) (h'ρ : ∀ᶠ (i : ι) in l, (ρ i).rOut ≤ C * (ρ i).rIn) (v : E) : ∀ᵐ (x : E) ∂μ, Filter.Tendsto (fun (i : ι) => (fderiv ℝ (MeasureTheory.convolution ((ρ i).normed μ) ψ (ContinuousLinearMap.lsmul ℝ ℝ) μ) x) v) l (nhds (lineDeriv ℝ ψ x v))

As normalized bumps shrink to 0 with a bounded ratio of outer to inner radius, the derivatives in a direction v of the mollifications of a Lipschitz function converge almost everywhere to its directional derivative ∂_v ψ.

theorem LipschitzWith.tendsto_integral_normed_convolution_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {K : NNReal} {ψ : E → ℝ} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] (hψ : LipschitzWith K ψ) {ι : Type u_3} {l : Filter ι} [l.IsCountablyGenerated] {ρ : ι → ContDiffBump 0} (hρ : Filter.Tendsto (fun (i : ι) => (ρ i).rOut) l (nhds 0)) {w : E → G} (hw : MeasureTheory.Integrable w μ) (hψw : MeasureTheory.Integrable (fun (x : E) => ψ x • w x) μ) : Filter.Tendsto (fun (i : ι) => ∫ (x : E), MeasureTheory.convolution ((ρ i).normed μ) ψ (ContinuousLinearMap.lsmul ℝ ℝ) μ x • w x ∂μ) l (nhds (∫ (x : E), ψ x • w x ∂μ))

As normalized bumps shrink to 0, integrals against the mollifications of a Lipschitz function ψ converge to the integral against ψ: ∫ (ρᵢ ⋆ ψ) w → ∫ ψ w whenever w and ψ w are integrable.

theorem LipschitzWith.tendsto_integral_fderiv_normed_convolution_apply_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {K : NNReal} {ψ : E → ℝ} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] (hψ : LipschitzWith K ψ) {ι : Type u_3} {l : Filter ι} [l.IsCountablyGenerated] {ρ : ι → ContDiffBump 0} {C : ℝ} (hρ : Filter.Tendsto (fun (i : ι) => (ρ i).rOut) l (nhds 0)) (h'ρ : ∀ᶠ (i : ι) in l, (ρ i).rOut ≤ C * (ρ i).rIn) (v : E) {w : E → G} (hw : MeasureTheory.Integrable w μ) : Filter.Tendsto (fun (i : ι) => ∫ (x : E), (fderiv ℝ (MeasureTheory.convolution ((ρ i).normed μ) ψ (ContinuousLinearMap.lsmul ℝ ℝ) μ) x) v • w x ∂μ) l (nhds (∫ (x : E), lineDeriv ℝ ψ x v • w x ∂μ))

As normalized bumps shrink to 0 with a bounded ratio of outer to inner radius, integrals against the directional derivatives of the mollifications of a Lipschitz function ψ converge to the integral against its directional derivative: ∫ ∂_v (ρᵢ ⋆ ψ) w → ∫ (∂_v ψ) w for integrable w.