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

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

L² control for odd reflected Dirichlet forcing

Odd reflection has the same squared magnitude as the unsigned coordinate-fold reflection already used in the Neumann/CZ layer. This file records the scalar forcing consequences of that observation.

theorem HCPolySupport.memScalarL2_cubeFaceReflectionBlockSet_cubeDirichletOddReflectionScalar {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (hF : MemScalarL2 (openCubeSet Q) F) : MemScalarL2 (cubeFaceReflectionBlockSet Q) (cubeDirichletOddReflectionScalar Q F)

The all-coordinate odd reflected scalar is L² on the reflection block whenever the original scalar is L² on the cube.

theorem HCPolySupport.setIntegral_cubeFaceReflectionBlockSet_cubeDirichletOddReflectionScalar_sq_of_memScalarL2 {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (hF : MemScalarL2 (openCubeSet Q) F) : ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, cubeDirichletOddReflectionScalar Q F x * cubeDirichletOddReflectionScalar Q F x = ↑(Fintype.card (Fin d → Fin 3)) * ∫ (y : Vec d) in openCubeSet Q, F y * F y

The squared L² energy of the odd reflected scalar on the full reflection block is one copy of the original cube energy for each reflection cell.

theorem HCPolySupport.oddReflectionScalar_block_sqIntegral_scale_of_L2 {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (hF : MemScalarL2 (openCubeSet Q) F) : ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, cubeDirichletOddReflectionScalar Q F x * cubeDirichletOddReflectionScalar Q F x = 3 ^ d * ∫ (y : Vec d) in openCubeSet Q, F y * F y

The squared L² energy of the odd reflected scalar on the full reflection block, with the cell count normalized to (3 : ℝ)^d.

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

The odd reflected scalar forcing is L² on the centered parent cube.

theorem HCPolySupport.memVectorL2_cubeFaceReflectionBlockSet_cubeDirichletOddReflectionVectorField {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (hG : MemVectorL2 (openCubeSet Q) G) : MemVectorL2 (cubeFaceReflectionBlockSet Q) (cubeDirichletOddReflectionVectorField Q G)

The all-coordinate odd reflected vector field is L² on the full reflection block whenever the original vector field is L² on the cube.

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

The odd reflected vector field is L² on the centered parent cube.

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

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

theorem HCPolySupport.setIntegral_successorCube_dirichletOddReflectedVectorField_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 (cubeDirichletOddReflectionVectorField (originCube d m) G x) (cubeDirichletOddReflectionVectorField (originCube d m) G x) = 3 ^ d * ∫ (y : Vec d) in openCubeSet (originCube d m), vecDot (G y) (G y)

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