Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionParentH1Graph

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

Parent reflected H¹ graph membership

This file proves the remaining parent-cube weak-gradient constraints for the all-face coordinate-fold reflection. The point is to avoid a separate Sobolev trace/gluing theorem: parent test functions are folded back to the original cube, the original weak derivative identity is applied to the signed folded scalar test, and the graph constructor then recovers the parent H1Function with the exact reflected representatives.

theorem HCPolySupport.setIntegral_cubeFaceReflectionCellCube_reflectedScalar_mul_deriv_eq {d : ℕ} {Q : TriadicCube d} {F φ : Vec d → ℝ} (i : Fin d) (choice : Fin d → Fin 3) : ∫ (x : Vec d) in openCubeSet (cubeFaceReflectionCellCube Q choice), cubeCoordinateFoldReflectedScalar Q F x * euclideanCoordDeriv i φ x = ∫ (y : Vec d) in openCubeSet Q, F y * euclideanCoordDeriv i φ (cubeFaceReflectionCellFoldMap Q choice y)

Change variables on one reflection cell in the scalar pairing with a parent coordinate derivative.

theorem HCPolySupport.setIntegral_cubeFaceReflectionBlockSet_reflectedScalar_mul_deriv_eq_folded {d : ℕ} {Q : TriadicCube d} {F φ : Vec d → ℝ} (hF : MemScalarL2 (openCubeSet Q) F) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (i : Fin d) : ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, cubeCoordinateFoldReflectedScalar Q F x * euclideanCoordDeriv i φ x = ∫ (y : Vec d) in openCubeSet Q, F y * ∑ choice : Fin d → Fin 3, euclideanCoordDeriv i φ (cubeFaceReflectionCellFoldMap Q choice y)

Scalar reflected pairing on the full reflection block, folded back to the original cube.

theorem HCPolySupport.setIntegral_originCube_succ_reflectedScalar_mul_deriv_eq_folded {d : ℕ} {m : ℤ} {F φ : Vec d → ℝ} (hF : MemScalarL2 (openCubeSet (originCube d m)) F) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (i : Fin d) : ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), cubeCoordinateFoldReflectedScalar (originCube d m) F x * euclideanCoordDeriv i φ x = ∫ (y : Vec d) in openCubeSet (originCube d m), F y * ∑ choice : Fin d → Fin 3, euclideanCoordDeriv i φ (cubeFaceReflectionCellFoldMap (originCube d m) choice y)

Centered parent-cube form of the scalar reflected derivative pairing.

theorem HCPolySupport.cubeFaceReflectionFoldedParentVectorField_smul_basisVec {d : ℕ} (Q : TriadicCube d) (i : Fin d) (φ : Vec d → ℝ) (y : Vec d) : cubeFaceReflectionFoldedParentVectorField Q (fun (x : Vec d) => φ x • basisVec i) y = cubeFaceReflectionFoldedParentScalarTest Q i φ y • basisVec i

Folding the parent vector test φ eᵢ is the signed scalar fold in the ith basis direction.

theorem HCPolySupport.vecDot_cubeFaceReflectionFoldedParentVectorField_smul_basisVec {d : ℕ} (Q : TriadicCube d) (i : Fin d) (φ : Vec d → ℝ) (G y : Vec d) : vecDot (cubeFaceReflectionFoldedParentVectorField Q (fun (x : Vec d) => φ x • basisVec i) y) G = cubeFaceReflectionFoldedParentScalarTest Q i φ y * G i

Component pairing form of the folded parent vector test φ eᵢ.

theorem HCPolySupport.setIntegral_originCube_succ_reflectedVectorField_coord_mul_eq_folded {d : ℕ} {m : ℤ} {G : Vec d → Vec d} {φ : Vec d → ℝ} (hG : MemVectorL2 (openCubeSet (originCube d m)) G) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (i : Fin d) : ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), cubeCoordinateFoldReflectedVectorField (originCube d m) G x i * φ x = ∫ (y : Vec d) in openCubeSet (originCube d m), G y i * cubeFaceReflectionFoldedParentScalarTest (originCube d m) i φ y

The parent vector reflected pairing in coordinate form, folded back to the original cube against the signed folded scalar test.

theorem HCPolySupport.mem_h1GraphClosedSubmodule_cubeCoordinateFoldReflection_originCube {d : ℕ} {m : ℤ} (u : H1Function (openCubeSet (originCube d m))) (hscalar : MemScalarL2 (openCubeSet (originCube d (m + 1))) (cubeCoordinateFoldReflectedScalar (originCube d m) u.toFun)) (hvector : MemVectorL2 (openCubeSet (originCube d (m + 1))) (cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => u.grad y)) : (toScalarL2 hscalar, toHilbertVectorL2OfVecField hvector) ∈ h1GraphClosedSubmodule

The all-face coordinate-fold reflection of an origin-cube H¹ function defines a point of the closed parent-cube weak-gradient graph.