Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionParentL2

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

theorem HCPolySupport.memScalarL2_openCubeSet_succ_originCube_cubeCoordinateFoldReflectedScalar {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (hF : MemScalarL2 (openCubeSet (originCube d m)) F) : MemScalarL2 (openCubeSet (originCube d (m + 1))) (cubeCoordinateFoldReflectedScalar (originCube d m) F)

The all-face reflected scalar is L² on the centered parent cube.

theorem HCPolySupport.memVectorL2_openCubeSet_succ_originCube_cubeCoordinateFoldReflectedVectorField {d : ℕ} {m : ℤ} {G : Vec d → Vec d} (hG : MemVectorL2 (openCubeSet (originCube d m)) G) : MemVectorL2 (openCubeSet (originCube d (m + 1))) (cubeCoordinateFoldReflectedVectorField (originCube d m) G)

The all-face reflected vector field is L² on the centered parent cube.

theorem HCPolySupport.setIntegral_successorCube_foldedReflectedScalar_sq {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (hF : MemScalarL2 (openCubeSet (originCube d m)) F) : ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), cubeCoordinateFoldReflectedScalar (originCube d m) F x * cubeCoordinateFoldReflectedScalar (originCube d m) F x = 3 ^ d * ∫ (y : Vec d) in openCubeSet (originCube d m), F y * F y

Scalar reflected energy on the centered parent cube is 3^d copies of the original cube energy.

theorem HCPolySupport.setIntegral_successorCube_foldedReflectedVectorField_self_pairing {d : ℕ} {m : ℤ} {G : Vec d → Vec d} (hG : MemVectorL2 (openCubeSet (originCube d m)) G) : ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), vecDot (cubeCoordinateFoldReflectedVectorField (originCube d m) G x) (cubeCoordinateFoldReflectedVectorField (originCube d m) G x) = 3 ^ d * ∫ (y : Vec d) in openCubeSet (originCube d m), vecDot (G y) (G y)

Vector reflected energy on the centered parent cube is 3^d copies of the original cube energy.