Documentation

TauCeti.MeasureTheory.Function.Lp.ApproximateIdentity

Smooth approximate identities in Lᵖ #

Let φ be a smooth bump function centred at the origin and normalized to have integral one. This file defines the corresponding averaging operator on Lᵖ by the Bochner integral

f ↦ ∫ t, φ(t) f(· - t)

as a continuous linear map of norm at most one, and proves that these operators converge strongly to the identity when the outer radii of the bumps tend to zero. The result holds for 1 ≤ p < ∞, for functions with values in an arbitrary real Banach space, and for every additive Haar measure on a finite-dimensional real normed space.

The integral is taken directly in Lᵖ. This avoids choosing pointwise representatives: translation is continuous in Lᵖ, so the average is a Bochner integral of a continuous compactly supported Lᵖ-valued function. The proof is the standard approximate-identity estimate

‖∫ φ(t) (f(· - t) - f) dt‖ₚ ≤ sup_{t ∈ supp φ} ‖f(· - t) - f‖ₚ.

This is the Lᵖ convergence input for mollification in Sobolev spaces. Together with commutation of mollification and weak differentiation, it approximates both the value and every weak derivative by the same smooth kernel.

Main declarations #

References #

L. C. Evans, Partial Differential Equations, Chapter 5, §5.3.1; H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Proposition 4.21.

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

Averaging an Lᵖ function against the normalized form of a smooth bump centred at zero, as a continuous linear operator on Lᵖ.

The average is a Bochner integral in Lᵖ, so it is independent of all choices of pointwise representative. The restriction p < ∞ ensures that translation is strongly continuous, hence that the Lᵖ-valued integrand is integrable; that integrability is what makes the average additive, and the operator is a contraction by TauCeti.norm_normedBumpLp_le_one.

Completeness of F is not part of the definition, exactly as for MeasureTheory.average and convolution: the Bochner integral is formed in whatever normed space is at hand, and it is 0 unless that space is complete. So this operator is the advertised average of the translates of its argument precisely when F is a Banach space, which is the setting of TauCeti.tendsto_normedBumpLp; the contraction bound holds in either case.

Equations
Instances For
    source
    theorem TauCeti.normedBumpLp_apply {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (phi : ContDiffBump 0) (f : ↥(MeasureTheory.Lp F p mu)) :
    (normedBumpLp hp phi mu) f = ∫ (t : E), phi.normed mu t • (mu.translateLp p (-t)) f ∂mu

    The defining Bochner-integral formula for normedBumpLp.

    source
    theorem TauCeti.normedBumpLp_eq_normedBumpAverageL {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (phi : ContDiffBump 0) :
    normedBumpLp hp phi mu = normedBumpAverageL phi mu (mu.translateLp p) ⋯

    normedBumpLp is the normalized-bump average of the Lᵖ translation action.

    source
    theorem TauCeti.compLpL_normedBumpLp {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace F] [CompleteSpace G] (hp : p ≠ ⊤) (phi : ContDiffBump 0) (L : F →L[ℝ] G) (f : ↥(MeasureTheory.Lp F p mu)) :
    (ContinuousLinearMap.compLpL p mu L) ((normedBumpLp hp phi mu) f) = (normedBumpLp hp phi mu) ((ContinuousLinearMap.compLpL p mu L) f)

    Averaging against a normalized bump commutes with postcomposition by a continuous linear map between Banach spaces.

    source
    theorem TauCeti.norm_normedBumpLp_le_one {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (phi : ContDiffBump 0) :
    ‖normedBumpLp hp phi mu‖ ≤ 1

    Averaging against a normalized nonnegative bump does not increase the Lᵖ norm when p < ∞.

    source
    theorem TauCeti.tendsto_normedBumpLp {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] [CompleteSpace F] {I : Type u_3} {l : Filter I} (hp : p ≠ ⊤) {phi : I → ContDiffBump 0} (hphi : Filter.Tendsto (fun (i : I) => (phi i).rOut) l (nhds 0)) (f : ↥(MeasureTheory.Lp F p mu)) :
    Filter.Tendsto (fun (i : I) => (normedBumpLp hp (phi i) mu) f) l (nhds f)

    Smooth approximate identity in Lᵖ. Let phi i be normalized smooth bumps centred at zero. If their outer radii tend to zero, then averaging any f ∈ Lᵖ against these bumps converges to f in the Lᵖ norm.

    The hypothesis p < ∞ is used to obtain strong translation continuity in this general setting, and F is assumed complete so that the Lᵖ-valued Bochner integral defining the average is the limit of its approximating sums. No positivity or normalization hypotheses are exposed because they are already supplied by ContDiffBump.normed.