MathlibAnnex.WeakGradient.localMollification_fderiv_apply_eq_zero
theorem
Substitutes a translated smooth kernel into the weak equation and tracks the reflection sign.
Statement
Let be a finite-dimensional real normed vector space with its Borel structure and an additive Haar measure . Let be open and locally integrable on . Assume for every vector field for which a compact set satisfies Here . Fix and with , and define For , let be the normalized smooth bump centered at zero with inner radius and outer radius ; thus , , and its closed support lies in . Put Then for every , every , and every ,
Assumptions
The ball data are supplied here; the theorem does not choose them. Only local integrability of on is required, not global integrability or Lipschitz continuity. The weak predicate alone would not imply integrability, so the separate local-integrability hypothesis is retained. Dimension zero and any direction, including , are allowed.
Conclusion
Every directional derivative of this localized mollification vanishes at every point of the inner ball. The conclusion is pointwise for the smooth function ; it does not claim that the rough function is pointwise constant.
The local ball data also name the middle ball . The translated test field used in the proof has a chosen compact carrier inside this middle ball and hence inside . A carrier is a compact set containing the nonzero set and its closure; it need not equal either. For a set , denotes its indicator, equal to one on and zero off . Thus the localized function is also written .
Proof route
Use as the actual vector test field. Its divergence is the negative kernel derivative. Compact localization leaves its weak integral unchanged, and the derivative formula for convolution identifies the resulting zero integral with .
Proof steps
Construct an admissible field. Define
It is (in fact smooth), and its nonzero set is contained in . Finite dimensionality makes this closed ball compact. For , since and ,
Thus , so the weak equation applies to this very field and carrier.
Compute the divergence with its sign. For an arbitrary direction , differentiating the reflected smooth kernel gives
The rank-one trace identity says that the trace of the map is . Substituting gives
The minus sign comes from differentiating .
Identify the localized integral. On , both and . Off , the field is zero on an open neighborhood, because is closed and contains its nonzero set. Consequently and there. These two cases give the pointwise identity
As is open and hence measurable, integration and the weak equation yield
Here the compact-localization integrability lemma applies to the given local integrability on and the compact set , and makes globally integrable. The kernel derivative is continuous, bounded, and compactly supported after translation; the displayed products are integrable as well.
Substitute the derivative formula. The localized function is locally integrable on . Apply the derivative formula for local mollifications with this same , the positive radius , the index , the point , and the direction . It identifies the last integral below with . Using Step 2 in Step 3 gives
Therefore . The calculation differentiates the smooth kernel and its convolution, never or the discontinuous cutoff .
Main citations
- Exact
declaration and its source —
MathlibAnnex.WeakGradient.localMollification_fderiv_apply_eq_zero - Weak
test equation with chosen compact carriers —
MathlibAnnex.WeakDivergenceZero - Derivative
of convolution through the compact kernel —
MathlibAnnex.WeakGradient.localMollification_fderiv_apply - Rank-one
trace identity —
MathlibAnnex.trace_smulRight - Local
ball data and the three nested balls —
MathlibAnnex.WeakGradient.LocalBallData - Compact
localization of a locally integrable function —
MathlibAnnex.WeakGradient.integrable_compactLocalization - Divergence
of a reflected scalar kernel times a direction —
MathlibAnnex.divergence_sub_smul - Derivative
vanishes on a zero neighborhood off the carrier —
MathlibAnnex.CompactC1VectorField.fderiv_eq_zero_of_not_mem_carrier - Translated
small closed balls lie in the middle ball —
MathlibAnnex.WeakGradient.LocalBallData.translated_closedBall_subset_middle - The
outer radius is at most half the local radius —
MathlibAnnex.WeakGradient.shrinkingBump_rOut_le_half - The
translated bump vector test field —
MathlibAnnex.WeakGradient.translatedBumpField - Its
compact carrier lies in the open domain —
MathlibAnnex.WeakGradient.translatedBumpField_carrier_subset - Divergence
of the translated bump field —
MathlibAnnex.WeakGradient.divergence_translatedBumpField - The
weak integral equals the localized whole-space integral —
MathlibAnnex.WeakGradient.weakIntegral_eq_localized_bumpIntegral
Lean source signature (exact)
theorem localMollification_fderiv_apply_eq_zero
{U : Set E} {u : E → ℝ}
(hU : IsOpen U)
(hu : LocallyIntegrableOn u U μ)
(hweak : WeakDivergenceZero μ U u)
{x : E} (D : LocalBallData U x)
{y : E} (hy : y ∈ D.inner) (k : ℕ) (e : E) :
fderiv ℝ
(localMollification (μ := μ) D.radius D.radius_pos
(compactLocalization D.carrier u) k) y (e) = 0| 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. |
(hweak : WeakDivergenceZero μ U u) |
The scalar weak equation for every vector field with a compact carrier contained in ; . |
(hU : IsOpen U) (hu : LocallyIntegrableOn u U μ) |
The set is open and is locally integrable on . Whole-space integrability or Lipschitz continuity of is not assumed. |
{x : E} (D : LocalBallData U x) |
The point and the supplied ball record. Its three fields are read in the next three rows. |
D.radius |
The radius . |
D.radius_pos |
The hypothesis . |
D.closed_four_subset |
The closed ball is contained in , with this same . |
D.inner; D.middle; D.carrier |
The cited definitions give , and , respectively. |
{y : E} (hy : y ∈ D.inner) (k : ℕ) (e : E) |
The point , kernel index and arbitrary direction . |
compactLocalization D.carrier u |
The scalar function , equal to on and zero elsewhere. |
| In the source | Mathematical meaning |
|---|---|
localMollification (μ := μ) D.radius D.radius_pos
(compactLocalization D.carrier u) k |
The same localized mollification , with the normalized kernel of radii and . |
fderiv ℝ (localMollification (μ := μ) D.radius D.radius_pos
(compactLocalization D.carrier u) k) y (e) = 0 |
The conclusion , pointwise for this smooth function. It does not assert a derivative or pointwise constancy of . |
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_eq_zero
Accepted content SHA-256: 5c79f9b268f22ebca5088199373a63f4e1f0103fe21e49a328326e591727acbd
Accepted source guide SHA-256: 2ec6c53eb4326bb445202980fed27249a05c34c9e9480a01cbeac8d3e444fe3a
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73