Coarse-graining support: #
Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionWeakEquation
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_reflectedVectorField_weakEquationOnParent_originCube
{d : ℕ}
{m : ℤ}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution (originCube d m) F)
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφs : HasCompactSupport φ)
(hmean : cubeAverage (originCube d m) F = 0)
(hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m)))
:
∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), vecDot (cubeCoordinateFoldReflectedVectorField (originCube d m) (fun (y : Vec d) => W.w.toH1Function.grad y) x)
(euclideanGradient φ x) = ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), cubeCoordinateFoldReflectedScalar (originCube d m) F x * φ x
The centered all-face reflection weak equation may be read on the next
larger centered cube at the level of set integrals. This avoids the false
shortcut of claiming an H¹ parent-domain object before proving the weak
gradient gluing across the internal faces.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionParent_weakPoissonEquationOn_originCube_of_grad_eq
{d : ℕ}
{m : ℤ}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution (originCube d m) F)
(uP : H1Function (openCubeSet (originCube d (m + 1))))
(huP_grad :
uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => W.w.toH1Function.grad y)
(hmean : cubeAverage (originCube d m) F = 0)
(hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m)))
:
WeakPoissonEquationOn (openCubeSet (originCube d (m + 1))) uP (cubeCoordinateFoldReflectedScalar (originCube d m) F)
If the reflected vector field has already been realized as the weak
gradient of an H¹ function on the centered parent cube, the parent integral
identity becomes the standard WeakPoissonEquationOn interface. This theorem
isolates the remaining gluing task to constructing that H1Function.