Coarse-graining support: Support.Sobolev.Foundations.CubeNeumannW22CZ.MemL2AndPairings

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

theorem HCPolySupport.setIntegral_cubeFaceNeighborSlabSet_faceNeighborSlabReflectedScalar_sq {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (i : Fin d) (hF : MemScalarL2 (openCubeSet Q) F) : ∫ (x : Vec d) in cubeFaceNeighborSlabSet Q i, faceNeighborSlabReflectedScalar Q i F x * faceNeighborSlabReflectedScalar Q i F x = 3 * ∫ (y : Vec d) in openCubeSet Q, F y * F y

The squared L² energy of the slab-reflected scalar on the lower/original/upper face-neighbor slab is three copies of the original cube energy.

theorem HCPolySupport.setIntegral_cubeFaceNeighborSlabSet_faceNeighborSlabReflectedVectorField_self_pairing {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (i : Fin d) (hG : MemVectorL2 (openCubeSet Q) G) : ∫ (x : Vec d) in cubeFaceNeighborSlabSet Q i, vecDot (faceNeighborSlabReflectedVectorField Q i G x) (faceNeighborSlabReflectedVectorField Q i G x) = 3 * ∫ (y : Vec d) in openCubeSet Q, vecDot (G y) (G y)

The vector self-pairing energy of the slab-reflected field on the lower/original/upper face-neighbor slab is three copies of the original cube energy.

theorem HCPolySupport.foldedScalar_sqIntegral_scale_card_of_L2 {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (hF : MemScalarL2 (openCubeSet Q) F) : ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, cubeCoordinateFoldReflectedScalar Q F x * cubeCoordinateFoldReflectedScalar 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 all-coordinate reflected scalar on the full reflection block is one copy of the original cube energy for each reflected cell. This is the MemScalarL2 wrapper around the geometric cell change-of-variables theorem.

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

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

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

The cross pairing of two all-coordinate reflected scalar fields on the full reflection block is one copy of the original cube pairing for each reflection cell.

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

The reflected scalar cross pairing on the full reflection block, with the cell count normalized to (3 : ℝ)^d.

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

The all-coordinate reflected scalar forcing is L² on the full reflection block whenever the original forcing is L² on Q.

theorem HCPolySupport.memLp_indicator_cubeFaceReflectionBlockSet_cubeCoordinateFoldReflectedScalar {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (hF : MemScalarL2 (openCubeSet Q) F) : MeasureTheory.MemLp ((cubeFaceReflectionBlockSet Q).indicator (cubeCoordinateFoldReflectedScalar Q F)) 2 MeasureTheory.volume

The block-indicator localization of the all-coordinate reflected scalar is a global L² function.

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

The global squared norm of the block-indicator reflected scalar is exactly the 3^d reflected copy count times the original cube scalar energy.

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

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

theorem HCPolySupport.memLp_indicator_cubeFaceReflectionBlockSet_cubeCoordinateFoldReflectedVectorField {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (hG : MemVectorL2 (openCubeSet Q) G) : MeasureTheory.MemLp ((cubeFaceReflectionBlockSet Q).indicator (cubeCoordinateFoldReflectedVectorField Q G)) 2 MeasureTheory.volume

The block-indicator localization of the all-coordinate reflected vector field is a global L² vector field.

theorem HCPolySupport.setIntegral_cubeReflection_foldedVectorSelfPairing_of_memVectorL2 {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (hG : MemVectorL2 (openCubeSet Q) G) : ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, vecDot (cubeCoordinateFoldReflectedVectorField Q G x) (cubeCoordinateFoldReflectedVectorField Q G x) = ↑(Fintype.card (Fin d → Fin 3)) * ∫ (y : Vec d) in openCubeSet Q, vecDot (G y) (G y)

The vector self-pairing energy of the all-coordinate reflected vector field on the full reflection block is one copy of the original cube energy for each reflected cell. This is the MemVectorL2 wrapper around the geometric cell change-of-variables theorem.

theorem HCPolySupport.setIntegral_cubeReflection_foldedVectorSelfPairing {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (hG : MemVectorL2 (openCubeSet Q) G) : ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, vecDot (cubeCoordinateFoldReflectedVectorField Q G x) (cubeCoordinateFoldReflectedVectorField Q G x) = 3 ^ d * ∫ (y : Vec d) in openCubeSet Q, vecDot (G y) (G y)

The vector self-pairing energy of the all-coordinate reflected field on the full reflection block, with the cell count normalized to (3 : ℝ)^d.

theorem HCPolySupport.setIntegral_openCubeSet_union_upperFaceReflectedScalar_sq {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (i : Fin d) (hF : MemScalarL2 (openCubeSet Q) F) : ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeUpperFaceNeighbor Q i), upperFaceReflectedScalar Q i F x * upperFaceReflectedScalar Q i F x = 2 * ∫ (y : Vec d) in openCubeSet Q, F y * F y

The squared L² energy of the upper-face reflected scalar on the doubled domain is two copies of the original cube energy.

theorem HCPolySupport.setIntegral_openCubeSet_union_lowerFaceReflectedScalar_sq {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (i : Fin d) (hF : MemScalarL2 (openCubeSet Q) F) : ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeLowerFaceNeighbor Q i), lowerFaceReflectedScalar Q i F x * lowerFaceReflectedScalar Q i F x = 2 * ∫ (y : Vec d) in openCubeSet Q, F y * F y

The squared L² energy of the lower-face reflected scalar on the doubled domain is two copies of the original cube energy.

theorem HCPolySupport.setIntegral_openCubeSet_union_upperFaceReflectedVectorField_self_pairing {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (i : Fin d) (hG : MemVectorL2 (openCubeSet Q) G) : ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeUpperFaceNeighbor Q i), vecDot (upperFaceReflectedVectorField Q i G x) (upperFaceReflectedVectorField Q i G x) = 2 * ∫ (y : Vec d) in openCubeSet Q, vecDot (G y) (G y)

The vector self-pairing energy of the upper-face reflected field on the doubled domain is two copies of the original cube energy.

theorem HCPolySupport.setIntegral_openCubeSet_union_lowerFaceReflectedVectorField_self_pairing {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (i : Fin d) (hG : MemVectorL2 (openCubeSet Q) G) : ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeLowerFaceNeighbor Q i), vecDot (lowerFaceReflectedVectorField Q i G x) (lowerFaceReflectedVectorField Q i G x) = 2 * ∫ (y : Vec d) in openCubeSet Q, vecDot (G y) (G y)

The vector self-pairing energy of the lower-face reflected field on the doubled domain is two copies of the original cube energy.