Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionParentPotential

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

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionParent_reflectedGradient_isPotentialOn_originCube_of_orthogonal {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (horth : ∀ {g : Vec d → Vec d}, MemVectorL2 (openCubeSet (originCube d (m + 1))) g → IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d (m + 1))) g → ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), vecDot (g x) (cubeCoordinateFoldReflectedVectorField (originCube d m) (fun (y : Vec d) => W.w.toH1Function.grad y) x) = 0) : IsPotentialOn (openCubeSet (originCube d (m + 1))) (cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => W.w.toH1Function.grad y)

Hodge-style reduction of the remaining parent-cube reflection gluing task: it is enough to prove that the reflected Neumann gradient is orthogonal to all solenoidal zero-normal fields on the centered parent cube.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.exists_cubeFaceReflectionParent_weakPoissonEquationOn_originCube_of_isPotentialOn {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hpot : IsPotentialOn (openCubeSet (originCube d (m + 1))) (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))) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), (uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => W.w.toH1Function.grad y) ∧ WeakPoissonEquationOn (openCubeSet (originCube d (m + 1))) uP (cubeCoordinateFoldReflectedScalar (originCube d m) F)

Once the parent reflected vector field is known to be a potential, choose an H¹ potential and put the parent reflected equation into the WeakPoissonEquationOn interface.