Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionParentTestWeakIdentity

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

Weak derivative identity for folded parent tests

The signed folded parent test is generally not compactly supported inside the original open cube, but it vanishes on the two relevant coordinate faces. This file packages the face-zero cutoff closure needed to use it in the original cube weak-gradient identity.

theorem HCPolySupport.H1Function.integral_mul_deriv_foldedParentScalarTest_eq_neg_integral_mul_originCube {d : ℕ} (m : ℤ) (u : H1Function (openCubeSet (originCube d m))) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ openCubeSet (originCube d (m + 1))) : ∫ (y : Vec d) in openCubeSet (originCube d m), u.toFun y * euclideanCoordDeriv i (cubeFaceReflectionFoldedParentScalarTest (originCube d m) i φ) y = -∫ (y : Vec d) in openCubeSet (originCube d m), u.grad y i * cubeFaceReflectionFoldedParentScalarTest (originCube d m) i φ y

The original-cube weak derivative identity may be tested against the signed folded parent test.

theorem HCPolySupport.H1Function.integral_mul_foldedParentScalarTest_derivSum_eq_neg_integral_mul_originCube {d : ℕ} (m : ℤ) (u : H1Function (openCubeSet (originCube d m))) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ openCubeSet (originCube d (m + 1))) : ∫ (y : Vec d) in openCubeSet (originCube d m), u.toFun y * ∑ choice : Fin d → Fin 3, euclideanCoordDeriv i φ (cubeFaceReflectionCellFoldMap (originCube d m) choice y) = -∫ (y : Vec d) in openCubeSet (originCube d m), u.grad y i * cubeFaceReflectionFoldedParentScalarTest (originCube d m) i φ y

The same weak identity with the folded-test derivative expanded into the cellwise parent derivative sum.