DivFreePairing

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

Weakly divergence-free fields annihilate H¹ gradients

Source: ABK26 (e.sensitivity.basic.split), closure step of the weak integration by parts.

A vector field t on an open bounded convex carrier U that is coordinatewise square integrable, supported in a compact subset of U, and weakly divergence free (it annihilates every smooth compactly supported test gradient) satisfies ∫ t · ∇w = 0 for every w ∈ H¹(U).

The compact interior support substitutes for the vanishing normal trace. The proof smooths w with CoarseGraining's convex-domain smoothing operator, cuts off the smooth representative to a test equal to w's smoothing near the support of t, applies the weak divergence-free hypothesis to the cutoff product, and passes to the limit in L²(U).

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.integral_vecDot_grad_eq_zero_of_weak_div_free {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hUne : U.Nonempty) {t : HCPolySupport.Vec d → HCPolySupport.Vec d} (htmem : ∀ (j : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => t x j) {K : Set (HCPolySupport.Vec d)} (hK : IsCompact K) (hKU : K ⊆ U) (htK : ∀ x ∉ K, t x = 0) (hdivfree : ∀ (ψ : HCPolySupport.Vec d → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ U → ∑ j : Fin d, ∫ (x : HCPolySupport.Vec d) in U, t x j * HCPolySupport.euclideanCoordDeriv j ψ x = 0) (w : HCPolySupport.H1Function U) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (t x) (w.grad x) = 0

Divergence-free pairing lemma. A coordinatewise L² vector field with compact support inside an open bounded convex carrier that annihilates every smooth compactly supported test gradient also annihilates every H¹ gradient. This is the trace-free mechanism of the weak integration by parts in e.sensitivity.basic.split.