Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.LocalHarmonicReplacement

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Local harmonic replacement on axis cubes

This file constructs the zero-trace correction for a scalar constant-coefficient divergence equation. Subtracting the correction from the original function produces a harmonic remainder, while direct testing by the correction gives the dimension-free Hilbert-vector energy estimate used in the good-lambda argument.

theorem HCPolySupport.CubeCalderonZygmund.exists_local_harmonic_replacement_axisCube {d : ℕ} [NeZero d] (z : Vec d) {L sigma0 : ℝ} (hL : 0 < L) (hsigma0 : 0 < sigma0) (u : H1Function (axisCube z L)) {h : Vec d → Vec d} (hh : MemVectorL2 (axisCube z L) h) (hweak : ∀ (φ : Vec d → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ axisCube z L → sigma0 * ∫ (x : Vec d) in axisCube z L, vecDot (u.grad x) (euclideanGradient φ x) = -∫ (x : Vec d) in axisCube z L, vecDot (h x) (euclideanGradient φ x)) : ∃ (w : H10Function (axisCube z L)), (∀ (ψ : H10Function (axisCube z L)), sigma0 * ∫ (x : Vec d) in axisCube z L, vecDot (w.grad x) (ψ.grad x) = -∫ (x : Vec d) in axisCube z L, vecDot (h x) (ψ.grad x)) ∧ WeakPoissonEquationOn (axisCube z L) (u - w.toH1Function) 0 ∧ ‖w.gradToHilbertVectorL2‖ ≤ sigma0⁻¹ * ‖toHilbertVectorL2OfVecField hh‖

A local scalar divergence equation on an axis cube admits a zero-trace correction with the same equation. The remainder is harmonic, and the correction has the sharp Hilbert-vector energy bound with no dimension loss.