Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.VectorFieldAndApex.BlockGlobalAndApex

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

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_reflectedVectorField_weakEquationOnBlock_of_compactSupport {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) {φ : 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 cubeFaceReflectionBlockSet Q, vecDot (cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, cubeCoordinateFoldReflectedScalar Q F x * φ x

Compact-test weak equation on the full all-coordinate reflection block, obtained by summing the single-cell weak equations over the finite 3^d cell decomposition.

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

Compact-test weak equation on the full all-coordinate reflection block, with the right-hand side given in the normalized cube L² measure used by the endpoint interfaces.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_reflectedVectorField_weakEquationOn_univ_of_compl_zero {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφs : HasCompactSupport φ) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (hgrad_zero : ∀ x ∉ cubeFaceReflectionBlockSet Q, vecDot (cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) (euclideanGradient φ x) = 0) (hforce_zero : ∀ x ∉ cubeFaceReflectionBlockSet Q, cubeCoordinateFoldReflectedScalar Q F x * φ x = 0) : ∫ (x : Vec d), vecDot (cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d), cubeCoordinateFoldReflectedScalar Q F x * φ x

Promote the reflected-block compact-test weak equation to a whole-space weak equation when the chosen test has zero contribution off the reflected block.

This is the interface used by the smooth Euclidean -Δu test: a mollified or cutoff test supported inside the reflection block can be read as a global compactly supported test on ℝ^d.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_reflectedVectorField_weakEquationOn_univ_of_test_zero {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφs : HasCompactSupport φ) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (hφ_zero : ∀ x ∉ cubeFaceReflectionBlockSet Q, φ x = 0) (hgradφ_zero : ∀ x ∉ cubeFaceReflectionBlockSet Q, euclideanGradient φ x = 0) : ∫ (x : Vec d), vecDot (cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d), cubeCoordinateFoldReflectedScalar Q F x * φ x

Whole-space reflected weak equation from pointwise zero of the test and its Euclidean gradient off the reflection block.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_reflectedVectorField_weakEquationOn_univ_of_tsupport_subset {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφs : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ cubeFaceReflectionBlockSet Q) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : ∫ (x : Vec d), vecDot (cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d), cubeCoordinateFoldReflectedScalar Q F x * φ x

Whole-space reflected weak equation for compact smooth tests whose topological support is contained in the reflection block.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.foldedBlockReflection_weakEquation_of_supportedTest {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφs : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ cubeFaceReflectionBlockSet Q) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : ∫ (x : Vec d), vecDot (cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d), (cubeFaceReflectionBlockSet Q).indicator (cubeCoordinateFoldReflectedScalar Q F) x * φ x

Whole-space reflected weak equation with the reflected forcing localized by the reflection-block indicator. This is the global forcing form used by Euclidean L² estimates.

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

The reflected Neumann gradient is L² on the full reflection block.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_reflectedGradient_indicator_memLp {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) : MeasureTheory.MemLp ((cubeFaceReflectionBlockSet Q).indicator (cubeCoordinateFoldReflectedVectorField Q fun (y : Vec d) => W.w.toH1Function.grad y)) 2 MeasureTheory.volume

The block-indicator localization of the reflected Neumann gradient is a global L² vector field.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_reflectedVectorField_globalWeakEquationWithL2Forcing {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : MeasureTheory.MemLp ((cubeFaceReflectionBlockSet Q).indicator (cubeCoordinateFoldReflectedScalar Q F)) 2 MeasureTheory.volume ∧ ∀ (φ : Vec d → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ cubeFaceReflectionBlockSet Q → ∫ (x : Vec d), vecDot (cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d), (cubeFaceReflectionBlockSet Q).indicator (cubeCoordinateFoldReflectedScalar Q F) x * φ x

Global reflected weak equation packaged with the global L² forcing witness needed by Euclidean estimates.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_reflectedVectorField_globalWeakEquationWithL2Data {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : MeasureTheory.MemLp ((cubeFaceReflectionBlockSet Q).indicator (cubeCoordinateFoldReflectedVectorField Q fun (y : Vec d) => W.w.toH1Function.grad y)) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp ((cubeFaceReflectionBlockSet Q).indicator (cubeCoordinateFoldReflectedScalar Q F)) 2 MeasureTheory.volume ∧ ∀ (φ : Vec d → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ cubeFaceReflectionBlockSet Q → ∫ (x : Vec d), vecDot (cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d), (cubeFaceReflectionBlockSet Q).indicator (cubeCoordinateFoldReflectedScalar Q F) x * φ x

Global reflected weak equation packaged with both global L² data: the block-indicator reflected gradient and the block-indicator reflected forcing.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_reflectedVectorField_weakEquationOnBlock_h10 {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (φ : H10Function (cubeFaceReflectionBlockSet Q)) : ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, vecDot (cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) (φ.grad x) = ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, cubeCoordinateFoldReflectedScalar Q F x * φ.toFun x

H10-test version of the reflected weak equation on the all-coordinate reflection block. This is the density bridge from the compact-test reflection identity to the Sobolev test space needed for the eventual reflected potential/limit argument.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_reflectedVectorField_energyIdentity_of_h10Potential {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (uR : H10Function (cubeFaceReflectionBlockSet Q)) (huR_grad : uR.grad = cubeCoordinateFoldReflectedVectorField Q fun (y : Vec d) => W.w.toH1Function.grad y) : ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, vecDot (cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) (cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) = ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, cubeCoordinateFoldReflectedScalar Q F x * uR.toFun x

Energy identity obtained by testing the reflected H10 weak equation against a supplied H10 potential for the reflected gradient. This isolates the next hard step: constructing such a potential for the reflected Neumann gradient.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_reflectedVectorField_energyIdentity_blockFold {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, vecDot (cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) (cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) = ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, cubeCoordinateFoldReflectedScalar Q F x * W.w.toH1Function.cubeFaceReflectionBlockFold.toFun x

Energy identity for the reflected block-folded H¹ potential. This avoids any zero-trace claim: both sides are reduced by cell reflection to 3^d copies of the original Neumann self-test identity on Q.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_smoothLocalizedEuclideanCZ_of_reflectedGradient {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_supp : HasCompactSupport u) (hu_sub : tsupport u ⊆ cubeFaceReflectionBlockSet Q) (hgrad : (fun (x : Vec d) => euclideanGradient u x) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) : ∑ i : Fin d, ∑ j : Fin d, ∫ (x : Vec d), euclideanCoordSecondDeriv i j u x ^ 2 ≤ (∫ (x : Vec d), ‖(cubeFaceReflectionBlockSet Q).indicator (cubeCoordinateFoldReflectedScalar Q F) x‖ ^ 2) ^ (1 / 2) * (∫ (x : Vec d), ‖euclideanCoordLaplacian u x‖ ^ 2) ^ (1 / 2)

Smooth localized Euclidean CZ estimate obtained from the reflected weak equation, assuming the smooth potential has the reflected vector field as its gradient. This isolates the remaining density/mollification bridge.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_smoothLocalizedEuclideanCZ_of_reflectedGradient_cubeEnergy {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_supp : HasCompactSupport u) (hu_sub : tsupport u ⊆ cubeFaceReflectionBlockSet Q) (hgrad : (fun (x : Vec d) => euclideanGradient u x) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) : ∑ i : Fin d, ∑ j : Fin d, ∫ (x : Vec d), euclideanCoordSecondDeriv i j u x ^ 2 ≤ (3 ^ d * ∫ (y : Vec d) in openCubeSet Q, F y * F y) ^ (1 / 2) * (∫ (x : Vec d), ‖euclideanCoordLaplacian u x‖ ^ 2) ^ (1 / 2)

Smooth localized Euclidean CZ estimate from the reflected weak equation, with the all-space reflected forcing norm converted back to the original cube forcing energy.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_smoothLocalizedEuclideanCZ_of_reflectedGradient_forcingL2 {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_supp : HasCompactSupport u) (hu_sub : tsupport u ⊆ cubeFaceReflectionBlockSet Q) (hgrad : (fun (x : Vec d) => euclideanGradient u x) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) : ∑ i : Fin d, ∑ j : Fin d, ∫ (x : Vec d), euclideanCoordSecondDeriv i j u x ^ 2 ≤ ∫ (x : Vec d), ‖(cubeFaceReflectionBlockSet Q).indicator (cubeCoordinateFoldReflectedScalar Q F) x‖ ^ 2

Smooth localized reflected Euclidean CZ estimate with the Laplacian factor cancelled on the Euclidean side.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlock_smoothLocalizedEuclideanCZ_of_reflectedGradient_cubeForcingL2 {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_supp : HasCompactSupport u) (hu_sub : tsupport u ⊆ cubeFaceReflectionBlockSet Q) (hgrad : (fun (x : Vec d) => euclideanGradient u x) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => W.w.toH1Function.grad y) x) : ∑ i : Fin d, ∑ j : Fin d, ∫ (x : Vec d), euclideanCoordSecondDeriv i j u x ^ 2 ≤ 3 ^ d * ∫ (y : Vec d) in openCubeSet Q, F y * F y

Smooth localized reflected Euclidean CZ estimate with forcing energy converted back to the original cube.