Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionParentOrthogonality

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

noncomputable def HCPolySupport.cubeFaceReflectionFoldedParentVectorField {d : ℕ} (Q : TriadicCube d) (g : Vec d → Vec d) : Vec d → Vec d

Fold a parent-cube vector field back to the original cube by summing the signed pullbacks from all reflection cells. This is the test field whose solenoidal zero-normal property is the concrete Hodge-orthogonality task left by the reflection argument.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.memVectorL2_openCubeSet_cubeFaceReflectionFoldedParentVectorField {d : ℕ} {m : ℤ} {g : Vec d → Vec d} (hg : MemVectorL2 (openCubeSet (originCube d (m + 1))) g) : MemVectorL2 (openCubeSet (originCube d m)) (cubeFaceReflectionFoldedParentVectorField (originCube d m) g)

The finite folded parent vector field is L² on the original cube.

theorem HCPolySupport.setIntegral_cubeFaceReflectionCellCube_vecDot_field_reflectedVectorField_eq {d : ℕ} {Q : TriadicCube d} {g G : Vec d → Vec d} (choice : Fin d → Fin 3) : ∫ (x : Vec d) in openCubeSet (cubeFaceReflectionCellCube Q choice), vecDot (g x) (cubeCoordinateFoldReflectedVectorField Q G x) = ∫ (y : Vec d) in openCubeSet Q, vecDot ((cubeFaceReflectionCellFoldLinear choice) (g (cubeFaceReflectionCellFoldMap Q choice y))) (G y)

Change variables on one reflection cell in the pairing between an arbitrary parent vector field and a reflected original-cube vector field.

theorem HCPolySupport.setIntegral_cubeFaceReflectionBlockSet_vecDot_field_reflectedVectorField_eq_folded {d : ℕ} {Q : TriadicCube d} {g G : Vec d → Vec d} (hgCell : ∀ (choice : Fin d → Fin 3), MemVectorL2 (openCubeSet (cubeFaceReflectionCellCube Q choice)) g) (hG : MemVectorL2 (openCubeSet Q) G) : ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, vecDot (g x) (cubeCoordinateFoldReflectedVectorField Q G x) = ∫ (y : Vec d) in openCubeSet Q, vecDot (cubeFaceReflectionFoldedParentVectorField Q g y) (G y)

The block pairing with a reflected vector field is the original-cube pairing against the finite folded parent vector field.

theorem HCPolySupport.setIntegral_originCube_succ_vecDot_field_reflectedVectorField_eq_folded {d : ℕ} {m : ℤ} {g G : Vec d → Vec d} (hg : MemVectorL2 (openCubeSet (originCube d (m + 1))) g) (hG : MemVectorL2 (openCubeSet (originCube d m)) G) : ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), vecDot (g x) (cubeCoordinateFoldReflectedVectorField (originCube d m) G x) = ∫ (y : Vec d) in openCubeSet (originCube d m), vecDot (cubeFaceReflectionFoldedParentVectorField (originCube d m) g y) (G y)

Centered parent-cube form of the folded-field reduction. To prove the Hodge orthogonality demanded by the parent reflection potential theorem, it is enough to show that this folded field is solenoidal zero-normal on the original cube.

theorem HCPolySupport.foldedParent_isSolenoidalZeroTrace_of_reflectedTests {d : ℕ} {m : ℤ} {g : Vec d → Vec d} (hg : MemVectorL2 (openCubeSet (originCube d (m + 1))) g) (hsol : IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d (m + 1))) g) (hreflect : ∀ (φ : H1Function (openCubeSet (originCube d m))), ∃ (ψ : H1Function (openCubeSet (originCube d (m + 1)))), ψ.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => φ.grad y) : IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d m)) (cubeFaceReflectionFoldedParentVectorField (originCube d m) g)

If every original-cube H¹ test admits the expected all-face reflected H¹ realization on the centered parent cube, then folding a parent solenoidal zero-normal field back to the original cube preserves the solenoidal zero-normal test identity. This is the remaining Sobolev gluing lemma in its most concrete form.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionParent_orthogonal_of_folded_solenoidal {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) {g : Vec d → Vec d} (hg : MemVectorL2 (openCubeSet (originCube d (m + 1))) g) (hfoldSol : IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d m)) (cubeFaceReflectionFoldedParentVectorField (originCube d m) 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

Conditional discharge of the parent Hodge orthogonality: after folding a parent solenoidal test field back to the original cube, the remaining analytic claim is exactly that the folded field is solenoidal zero-normal there.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionParent_reflectedGradient_isPotentialOn_originCube_of_folded_solenoidal {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hfoldSol : ∀ {g : Vec d → Vec d}, MemVectorL2 (openCubeSet (originCube d (m + 1))) g → IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d (m + 1))) g → IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d m)) (cubeFaceReflectionFoldedParentVectorField (originCube d m) g)) : IsPotentialOn (openCubeSet (originCube d (m + 1))) (cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => W.w.toH1Function.grad y)

Hodge-potential handoff with the remaining trace/gluing task isolated to a single preservation property for folded parent solenoidal tests.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.exists_cubeFaceReflectionParent_weakPoissonEquationOn_originCube_of_folded_solenoidal {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hfoldSol : ∀ {g : Vec d → Vec d}, MemVectorL2 (openCubeSet (originCube d (m + 1))) g → IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d (m + 1))) g → IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d m)) (cubeFaceReflectionFoldedParentVectorField (originCube d m) g)) (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)

Full weak-equation handoff from the folded-solenoidal preservation lemma. This is the exact interface needed before applying the interior H² estimate on the centered parent cube.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.exists_cubeFaceReflectionParent_weakPoissonEquationOn_originCube_of_parent_reflected_h1_tests {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hreflect : ∀ (φ : H1Function (openCubeSet (originCube d m))), ∃ (ψ : H1Function (openCubeSet (originCube d (m + 1)))), ψ.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => φ.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)

End-to-end conditional form of the reflection route: it remains to construct the reflected parent H¹ test for every original-cube H¹ test.