Coarse-graining support: Support.Sobolev.Foundations.CubeDirichletH2.ReflectionDivergenceRhs

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

Dirichlet odd reflection for a divergence-form right-hand side

On a centered cube, the product-odd reflection of a zero-trace scalar function has the corresponding odd-reflected vector field as its gradient. Reflecting the vector datum by the same rule preserves the constant-coefficient divergence-form weak equation, including its sign.

theorem HCPolySupport.exists_h1Function_cubeDirichletOddReflectionParent_divergence_rhs_originCube {d : ℕ} {m : ℤ} {sigma0 : ℝ} {u : H10Function (openCubeSet (originCube d m))} {h : Vec d → Vec d} (hh : MemVectorL2 (openCubeSet (originCube d m)) h) (hweak : ∀ (ψ : H10Function (openCubeSet (originCube d m))), sigma0 * ∫ (x : Vec d) in openCubeSet (originCube d m), vecDot (u.grad x) (ψ.grad x) = -∫ (x : Vec d) in openCubeSet (originCube d m), vecDot (h x) (ψ.grad x)) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), uP.toFun = cubeDirichletOddReflectionScalar (originCube d m) u.toFun ∧ (uP.grad = cubeDirichletOddReflectionVectorField (originCube d m) fun (y : Vec d) => u.grad y) ∧ ∀ (φ : Vec d → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ openCubeSet (originCube d (m + 1)) → sigma0 * ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), vecDot (uP.grad x) (euclideanGradient φ x) = -∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), vecDot (cubeDirichletOddReflectionVectorField (originCube d m) h x) (euclideanGradient φ x)

A scalar constant-coefficient divergence-form equation on a centered cube extends to compactly supported smooth tests on the centered parent cube under all-face Dirichlet odd reflection. No sign or positivity assumption on the constant coefficient is needed.