Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.VectorFieldAndApex.ReflectedEqCellSlab

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

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionCell_reflectedGradient_isPotentialOn {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (choice : Fin d → Fin 3) : IsPotentialOn (openCubeSet (cubeFaceReflectionCellCube Q choice)) (cubeCoordinateFoldReflectedVectorField Q fun (y : Vec d) => W.w.toH1Function.grad y)

The reflected Neumann gradient is a Sobolev potential on each individual reflection cell. This is the cellwise gluing datum for the global block construction.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_reflectedGradient_isPotentialOn {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) : IsPotentialOn (cubeFaceReflectionBlockSet Q) (cubeCoordinateFoldReflectedVectorField Q fun (y : Vec d) => W.w.toH1Function.grad y)

The reflected Neumann gradient is a Sobolev potential on the whole all-coordinate reflection block.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.upperFace_reflectedVectorField_weakEquationOnUnion {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hmean : cubeAverage Q F = 0) (hgradMain : MeasureTheory.Integrable (fun (x : Vec d) => vecDot (W.w.toH1Function.grad x) (euclideanGradient φ x)) (MeasureTheory.volume.restrict (openCubeSet Q))) (hgradReflected : MeasureTheory.Integrable (fun (x : Vec d) => vecDot (W.w.toH1Function.grad x) (euclideanGradient (fun (z : Vec d) => φ (cubeUpperFaceReflection Q i z)) x)) (MeasureTheory.volume.restrict (openCubeSet Q))) (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict (openCubeSet Q))) (hFmain : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ x) (MeasureTheory.volume.restrict (openCubeSet Q))) (hFreflected : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ (cubeUpperFaceReflection Q i x)) (MeasureTheory.volume.restrict (openCubeSet Q))) : ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeUpperFaceNeighbor Q i), vecDot (upperFaceReflectedVectorField Q i (fun (y : Vec d) => W.w.toH1Function.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeUpperFaceNeighbor Q i), upperFaceReflectedScalar Q i F x * φ x

Upper-face reflected weak equation in reflected-field notation.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.lowerFace_reflectedVectorField_weakEquationOnUnion {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hmean : cubeAverage Q F = 0) (hgradMain : MeasureTheory.Integrable (fun (x : Vec d) => vecDot (W.w.toH1Function.grad x) (euclideanGradient φ x)) (MeasureTheory.volume.restrict (openCubeSet Q))) (hgradReflected : MeasureTheory.Integrable (fun (x : Vec d) => vecDot (W.w.toH1Function.grad x) (euclideanGradient (fun (z : Vec d) => φ (cubeLowerFaceReflection Q i z)) x)) (MeasureTheory.volume.restrict (openCubeSet Q))) (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict (openCubeSet Q))) (hFmain : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ x) (MeasureTheory.volume.restrict (openCubeSet Q))) (hFreflected : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ (cubeLowerFaceReflection Q i x)) (MeasureTheory.volume.restrict (openCubeSet Q))) : ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeLowerFaceNeighbor Q i), vecDot (lowerFaceReflectedVectorField Q i (fun (y : Vec d) => W.w.toH1Function.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeLowerFaceNeighbor Q i), lowerFaceReflectedScalar Q i F x * φ x

Lower-face reflected weak equation in reflected-field notation.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.upperFaceReflection_weakEquation_on_union {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφs : HasCompactSupport φ) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeUpperFaceNeighbor Q i), vecDot (upperFaceReflectedVectorField Q i (fun (y : Vec d) => W.w.toH1Function.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeUpperFaceNeighbor Q i), upperFaceReflectedScalar Q i F x * φ x

Compact-test upper-face reflected weak equation in reflected-field notation, using the normalized cube L² hypothesis from the endpoint interfaces.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.lowerFaceReflection_weakEquation_on_union {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφs : HasCompactSupport φ) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeLowerFaceNeighbor Q i), vecDot (lowerFaceReflectedVectorField Q i (fun (y : Vec d) => W.w.toH1Function.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeLowerFaceNeighbor Q i), lowerFaceReflectedScalar Q i F x * φ x

Compact-test lower-face reflected weak equation in reflected-field notation, using the normalized cube L² hypothesis from the endpoint interfaces.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.faceNeighborSlab_reflectedVectorField_weakEquationOnSlab_of_compactSupport {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφs : HasCompactSupport φ) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (openCubeSet Q))) : ∫ (x : Vec d) in cubeFaceNeighborSlabSet Q i, vecDot (faceNeighborSlabReflectedVectorField Q i (fun (y : Vec d) => W.w.toH1Function.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d) in cubeFaceNeighborSlabSet Q i, faceNeighborSlabReflectedScalar Q i F x * φ x

Compact-test weak equation on the lower/original/upper one-coordinate reflected slab, in reflected-field notation. Algebraically this is the lower one-face reflected equation plus the upper one-face reflected equation, minus the original cube equation.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.faceNeighborSlab_reflectedVectorField_weakEquationOnSlab {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφs : HasCompactSupport φ) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : ∫ (x : Vec d) in cubeFaceNeighborSlabSet Q i, vecDot (faceNeighborSlabReflectedVectorField Q i (fun (y : Vec d) => W.w.toH1Function.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d) in cubeFaceNeighborSlabSet Q i, faceNeighborSlabReflectedScalar Q i F x * φ x

Compact-test weak equation on the lower/original/upper one-coordinate reflected slab, with the right-hand side given in the normalized cube L² measure used by the endpoint interfaces.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionCell_reflectedVectorField_weakEquationOnCell_of_compactSupport {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (choice : Fin d → Fin 3) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφs : HasCompactSupport φ) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (openCubeSet Q))) : ∫ (x : Vec d) in openCubeSet (cubeFaceReflectionCellCube Q choice), vecDot (cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d) in openCubeSet (cubeFaceReflectionCellCube Q choice), cubeCoordinateFoldReflectedScalar Q F x * φ x

Compact-test weak equation on a single all-coordinate reflection-block cell. The proof tests the original cube equation with φ precomposed by the cell fold, then changes variables through the fold map.