MATHLIBANNEX / CANONICAL DECLARATION CARD

Strong local convergence of mollified derivatives

MathlibAnnex.Mollification.tendsto_eLpNorm_fderiv_mollify_sub

theorem

Approximates the derivative in local , where is the dimension of the domain.

Statement

Fix a positive integer and an integer . Let and satisfy and let be compact. For , let be the chosen smooth nonnegative bump kernel centered at zero, with inner radius and outer radius , divided by its positive Lebesgue integral. Thus and its topological support is contained in . Using this same kernel, define the normalized convolution Then and for all sufficiently small positive . Here is induced by the two sup norms. The exponent is the already fixed domain dimension, not another parameter.

Assumptions

The dimension satisfies , while may be zero. The compact set may be empty or have empty interior. The displayed Lipschitz bound holds on the whole domain. Neither nor is assumed to belong to on the whole space. The derivative is defined almost everywhere by Rademacher’s theorem; choosing zero at nondifferentiability points gives the same quantities.

Conclusion

Both the seminorm convergence and eventual membership hold for Lebesgue measure restricted to . The original derivative itself belongs to by measurability and the bound .

Notes

Linearity of mollification for locally integrable summands and a common compact support bound for mollifications of a compactly supported map will be used later. Those auxiliary results concern the same kernels and are cited here; the present theorem does not assume that has compact support.

Proof route

First prove . On , each coordinate of this convolution equals the convolution of a bounded, compactly supported scalar function. Scalar convergence and a finite coordinate estimate then give the required operator-norm convergence.

Proof steps

  1. Differentiate the convolution. Fix and . Rademacher’s theorem and preservation of Lebesgue-null sets by give differentiability of at for almost every . For every increment ,

    The integrand is integrable for each , because is continuous and the kernel has compact support. The proposed derivative is measurable and is bounded by the same integrable function. These are the hypotheses for differentiation under the integral, which gives

    For the th input vector and the th output coordinate, this reads

  2. Replace a derivative coordinate by a compactly supported one without changing its convolution on . Choose with and put . For and , define the scalar function

    It is measurable, , and it vanishes outside the compact set . Hence .

    If , , and , then

    Consequently, for every ,

    If the kernel factor is nonzero, this follows from ; otherwise both sides vanish. Also . Substituting into Step 1 gives

  3. Prove convergence for that scalar function. The normalized bumps have outer radius and outer-to-inner radius ratio . The Lebesgue-differentiation convolution theorem therefore gives

    Normalization and nonnegativity give

    Set . If and with , then

    so . Consequently

    Dominated convergence, followed by taking the th root, proves

    Its norm is no larger. Step 2 therefore proves convergence of every derivative-coordinate difference on .

  4. Pass from coordinates to the operator norm. For a linear map and ,

    Taking the maximum over and then the supremum over gives . To justify the finite-sum estimate, fix and write, on ,

    Steps 2–3 give measurable with . Thus and , because has finite measure. For , apply Hölder to and , with conjugate exponents and :

    If , divide by its power; if it is zero, the desired inequality is immediate. For the same inequality is the equality . This proves the finite-sum form of Minkowski used here, and hence

    The last limit uses Step 3 for each of the finitely many pairs . For every operator is zero and the conclusion is immediate. Finally, is smooth for every . Its derivative is continuous and bounded on compact , so . This supplies the membership assertion as well as the convergence.

Main citations

Lean source signature (exact)

theorem tendsto_eLpNorm_fderiv_mollify_sub
    {m N : ℕ} {f : (Fin (m + 1) → ℝ) → (Fin N → ℝ)} {C : ℝ≥0} (hf : LipschitzWith C f)
    {K : Set ((Fin (m + 1) → ℝ))} (hK : IsCompact K) :
    (Tendsto (fun ε => eLpNorm
      (fun x => fderiv ℝ (mollify ε f) x - fderiv ℝ f x)
      ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K)) (𝓝[>] (0 : ℝ)) (𝓝 0)) ∧
      ∀ᶠ ε in 𝓝[>] (0 : ℝ), MemLp
        (fun x => fderiv ℝ (mollify ε f) x) ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K)
In the source Mathematical meaning
{m N : ℕ} {f : (Fin (m + 1) → ℝ) → (Fin N → ℝ)} The positive domain dimension is and the output dimension is . The input is .
{C : ℝ≥0} (hf : LipschitzWith C f) A nonnegative constant and the global bound for all .
{K : Set ((Fin (m + 1) → ℝ))} (hK : IsCompact K) The integration set is compact, possibly empty.
fderiv ℝ (mollify ε f) x - fderiv ℝ f x The continuous-linear-map difference ; its norm is the operator norm induced by the sup norms.
((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K) The exponent is the already fixed domain dimension , and the measure is Lebesgue measure restricted to . The seminorm takes values in .
In the source Mathematical meaning
(𝓝[>] (0 : ℝ)) (𝓝 0) The first output is convergence to zero as through positive values: .
∀ᶠ ε in 𝓝[>] (0 : ℝ), MemLp The second, conjunctive output holds for all sufficiently small positive : . Membership includes a.e. strong measurability and finite seminorm, not just a pointwise bound.
Exact surrounding binder context (separate excerpt) 
noncomputable section
open Set MeasureTheory Filter
open scoped Convolution Topology ENNReal NNReal Pointwise
namespace MathlibAnnex
namespace Mollification

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Exact content identity

Declaration: MathlibAnnex.Mollification.tendsto_eLpNorm_fderiv_mollify_sub

Accepted content SHA-256: 2b5f64576a032a3d0f209601db7ec4155cdd19e8f87f625f6a7a1437104445b3

Accepted source guide SHA-256: e8dda24a67f2e7c8929b348569786f54bb3adbdbabfff4377049c0fc9c1c6317

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑