MATHLIBANNEX / CANONICAL DECLARATION CARD

Differentiating a local mollification through its kernel

MathlibAnnex.WeakGradient.localMollification_fderiv_apply

theorem

Writes a directional derivative without differentiating the locally integrable input.

Statement

Let be a finite-dimensional real normed vector space with its Borel measurable structure and an additive Haar measure . Fix . For , let be the normalized smooth bump centered at zero with inner and outer radii It is nonnegative, has integral one, and has compact support in . If is locally integrable, put Then, for every , , and direction ,

Assumptions

Only local integrability of is assumed. The theorem does not require a weak equation, global integrability, Lipschitz continuity, or differentiability of . The dimension may be zero. The kernel is the specified normalized bump for these radii; no extra scaling formula for a universal kernel is assumed.

Conclusion

The derivative is a genuine Fréchet derivative of the mollification, and the displayed scalar integral is integrable. Differentiation falls on the smooth compactly supported kernel, not on .

In the local application, with compact and contained in an open set on which is locally integrable. Local integrability gives , and measurability of compact gives integrability of on , hence the hypothesis of this theorem. Separately, the rank-one trace identity explains why the same directional kernel derivative occurs in the divergence test used later; it is not an assumption on .

Proof route

Apply the compact-kernel differentiation theorem for convolution, evaluate its operator-valued integral in direction , and change variables by the Haar-measure-preserving reflection .

Proof steps

  1. Apply the derivative theorem with its hypotheses. The normalized bump is and compactly supported, while is locally integrable on all of . The compact-kernel convolution differentiation theorem therefore yields

    This is an integral of continuous linear functionals on . The derivative is continuous and compactly supported. Multiplication against the locally integrable translate of is therefore integrable, which justifies this operator-valued integral.

  2. Evaluate and change variables. Evaluation is continuous linear, so it commutes with that integrable Bochner integral:

    Translation and negation preserve additive Haar measure on the real vector space. Thus the measurable bijection , its own inverse, permits substitution . Since , the preceding formula becomes

    No derivative of has been used.

Main citations

Lean source signature (exact)

theorem localMollification_fderiv_apply
    (R : ℝ) (hR : 0 < R) {v : E → ℝ}
    (hv : LocallyIntegrable v μ) (k : ℕ) (y : E) (e : E) :
    fderiv ℝ (localMollification (μ := μ) R hR v k) y (e) =
      ∫ z, v z *
        fderiv ℝ (normalizedShrinkingBump (μ := μ) R hR k) (y - z) (e) ∂μ
In the source Mathematical meaning
[NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : Measure E} [μ.IsAddHaarMeasure] The finite-dimensional real normed space , with Borel measurable structure and additive Haar measure . Dimension zero is allowed.
(R : ℝ) (hR : 0 < R) {v : E → ℝ} (hv : LocallyIntegrable v μ) The positive radius and locally integrable scalar function . No derivative of is assumed.
(k : ℕ) (y : E) (e : E) The kernel index , point and direction .
normalizedShrinkingBump (μ := μ) R hR k The normalized kernel , with inner radius , outer radius and integral one, in the cited definitions.
localMollification (μ := μ) R hR v k The scalar mollification .
In the source Mathematical meaning
fderiv ℝ (localMollification (μ := μ) R hR v k) y (e) The derivative evaluated on , a real number.
∫ z, v z * fderiv ℝ (normalizedShrinkingBump (μ := μ) R hR k) (y - z) (e) ∂μ The output formula . The derivative falls on the smooth kernel, not on .
Exact surrounding binder context (separate excerpts)

Exact source lines 11–17:

noncomputable section
open Set Metric MeasureTheory Filter TopologicalSpace ContinuousLinearMap
open scoped ENNReal Topology Convolution BigOperators
namespace MathlibAnnex.WeakGradient
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
variable {μ : Measure E} [μ.IsAddHaarMeasure]

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

Exact content identity

Declaration: MathlibAnnex.WeakGradient.localMollification_fderiv_apply

Accepted content SHA-256: 53fd32f1ec326a98c2b1dcfeaff7b1fc8e8743f6b690592ea00cc15721e7e43f

Accepted source guide SHA-256: 575b274040370cb823dabc732ad4a92e8adf030582ff26e29bb3a7fcb6ebdc75

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑