WeakGradientLocality

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Locality of the weak gradient

The weak gradient is a local object: if u has weak gradient Du on each member of an open cover of W, it has weak gradient Du on W itself. This fact is absent from Mathlib and from the compiled part of CoarseGraining, and it is the first frontier item of the §4.3 odd-reflection chain: it is what turns the one-face harmonicity transfer into a statement about the whole reflected window, and what upgrades a localized zero-trace hypothesis (a hypothesis about η · v for cutoffs η) into a statement about v.

The argument

Only one ingredient is genuinely missing: a smooth partition of a compactly supported test function subordinate to the cover. It is built here from scratch and without any manifold machinery, by a telescoping product:

• exists_contDiff_eq_one_nhds upgrades Mathlib's exists_smooth_tsupport_subset (a bump equal to 1 at one point) to a bump identically 1 on a neighbourhood of the point, by composing with a rescaled Real.smoothTransition;
• the compact set tsupport φ is covered by finitely many such neighbourhoods, so the product ∏ (1 - gᶜ) of the corresponding bump defects vanishes on tsupport φ, hence φ · ∏ (1 - gᶜ) = 0 everywhere;
• exists_smooth_decomposition_of_open_cover then telescopes 1 - ∏_{c ∈ t} (1 - gᶜ) = ∑ gᶜ ∏_{earlier} (1 - g) by induction on the finite index set, producing finitely many smooth compactly supported pieces ψ j summing to φ, each supported in one member of the cover.

No normalization, no division, and no SmoothPartitionOfUnity is needed: the telescoping identity is exact, and the pieces need not be nonnegative or sum to one off tsupport φ.

The L² hypotheses in the locality statements are not decoration. The weak derivative predicate HasWeakPartialDerivOn is an identity between Bochner integrals, and splitting the integral of φ = ∑ ψ j across the sum requires each summand to be genuinely integrable; u, Du ∈ L²(W) (the H¹ carrier's own data) is exactly what makes the Hölder pairing with the smooth compactly supported pieces integrable.

Main results

• exists_contDiff_eq_one_nhds — a smooth compactly supported bump equal to 1 on a neighbourhood of a point and supported in a prescribed neighbourhood.
• exists_smooth_decomposition_of_open_cover — the finite smooth decomposition of a compactly supported test function subordinate to an open cover.
• hasWeakPartialDerivOn_iUnion, hasWeakGradientOn_iUnion — locality on a union of open sets.
• hasWeakGradientOn_of_open_cover — the cover form (the shape consumers use).
• hasWeakGradientOn_union — the two-set specialization.

The opposite (easy) direction — restriction of a weak gradient to an open subset — is CoarseGraining's HasWeakGradientOn.restrict and is not repeated here.

1. A smooth bump identically one near a point

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.oneNear (t : ℝ) : ℝ

Mathlib's smooth transition, rescaled to vanish on (-∞, 1/2] and to equal 1 on [3/4, ∞).

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.oneNear t = (4 * t - 2).smoothTransition

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_contDiff_eq_one_nhds {d : ℕ} {s : Set (HCPolySupport.Vec d)} {x : HCPolySupport.Vec d} (hs : s ∈ nhds x) : ∃ (g : HCPolySupport.Vec d → ℝ) (W : Set (HCPolySupport.Vec d)), ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g ∧ tsupport g ⊆ s ∧ IsOpen W ∧ x ∈ W ∧ ∀ y ∈ W, g y = 1

A smooth bump identically one on a neighbourhood.

Mathlib's exists_smooth_tsupport_subset produces a smooth compactly supported bump supported in s and equal to 1 at x. Composing it with the rescaled smooth transition oneNear produces one equal to 1 on a whole open neighbourhood of x, which is what the telescoping decomposition below needs (a product of defects 1 - g must vanish identically on the covered compact set, not merely at chosen points).