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

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

Restricting weak divergence equations to an interior axis cube

The weak equation is originally posed on an ambient open set. A test whose topological support lies in an axis subcube has zero Euclidean gradient off that subcube, so both flux pairings have exactly the same set integral on the subcube and on the ambient set. This is the support argument needed to pass a parent-cube equation to the comparison cube; it does not assume a second, local PDE.

theorem HCPolySupport.CubeCalderonZygmund.weakDivergence_restrict_axisCube {d : ℕ} {U : Set (Vec d)} (z : Vec d) (L : ℝ) (hBU : axisCube z L ⊆ U) {sigma0 : ℝ} (u : H1Function U) (H : Vec d → Vec d) (hweak : ∀ (phi : Vec d → ℝ), ContDiff ℝ (↑⊤) phi → HasCompactSupport phi → tsupport phi ⊆ U → sigma0 * ∫ (y : Vec d) in U, vecDot (u.grad y) (euclideanGradient phi y) = -∫ (y : Vec d) in U, vecDot (H y) (euclideanGradient phi y)) (phi : Vec d → ℝ) : ContDiff ℝ (↑⊤) phi → HasCompactSupport phi → tsupport phi ⊆ axisCube z L → sigma0 * ∫ (y : Vec d) in axisCube z L, vecDot ((u.restrict ⋯ hBU).grad y) (euclideanGradient phi y) = -∫ (y : Vec d) in axisCube z L, vecDot (H y) (euclideanGradient phi y)

Restrict a scalar weak divergence equation to an interior open axis cube.

The restricted function has definitionally the same gradient. The conclusion keeps the coefficient and sign of the parent equation verbatim; its only new input is geometric containment of the subcube in the ambient domain.