ReflectionWeakEquation

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Neumann divergence equations under even reflection

A compactly supported parent test is folded through every reflection cell and summed on the source cube. Its gradient is exactly the folded parent gradient appearing in the existing change-of-variables theorem. Subtracting its source average makes it an admissible mean-zero Neumann test without changing that gradient. This proves the reflected divergence equation without introducing any boundary or comparison hypothesis.

noncomputable def HCPolySupport.neumannEvenFoldedParentScalarTest {d : ℕ} (Q : TriadicCube d) (phi : Vec d → ℝ) : Vec d → ℝ

Unsigned fold of a parent scalar test through all reflection cells.

Equations

• HCPolySupport.neumannEvenFoldedParentScalarTest Q phi y = ∑ choice : Fin d → Fin 3, phi (HCPolySupport.cubeFaceReflectionCellFoldMap Q choice y)

theorem HCPolySupport.contDiff_neumannEvenFoldedParentScalarTest {d : ℕ} (Q : TriadicCube d) {phi : Vec d → ℝ} (hphi : ContDiff ℝ (↑⊤) phi) : ContDiff ℝ (↑⊤) (neumannEvenFoldedParentScalarTest Q phi)

The unsigned folded parent test is smooth.

theorem HCPolySupport.hasCompactSupport_neumannEvenFoldedParentScalarTest {d : ℕ} (Q : TriadicCube d) {phi : Vec d → ℝ} (hphi : HasCompactSupport phi) : HasCompactSupport (neumannEvenFoldedParentScalarTest Q phi)

The unsigned folded parent test has compact support.

theorem HCPolySupport.euclideanCoordDeriv_neumannEvenFoldedParentScalarTest {d : ℕ} (Q : TriadicCube d) (i : Fin d) {phi : Vec d → ℝ} (hphi : ContDiff ℝ (↑⊤) phi) (y : Vec d) : euclideanCoordDeriv i (neumannEvenFoldedParentScalarTest Q phi) y = ∑ choice : Fin d → Fin 3, cubeFaceReflectionCellFoldSign choice i * euclideanCoordDeriv i phi (cubeFaceReflectionCellFoldMap Q choice y)

Coordinate derivative of the unsigned folded parent test.

theorem HCPolySupport.euclideanGradient_neumannEvenFoldedParentScalarTest {d : ℕ} (Q : TriadicCube d) {phi : Vec d → ℝ} (hphi : ContDiff ℝ (↑⊤) phi) : euclideanGradient (neumannEvenFoldedParentScalarTest Q phi) = cubeFaceReflectionFoldedParentVectorField Q (euclideanGradient phi)

The gradient of the folded scalar test is the existing folded parent vector field applied to the parent gradient.

theorem HCPolySupport.IsMeanZeroNeumannRhsWeakSolution.scalarMatrix_neg_weak {d : ℕ} {U : Set (Vec d)} {sigma0 : ℝ} {u : H1MeanZeroFunction U} {h : Vec d → Vec d} (hweak : IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => scalarMatrix sigma0) U u fun (x : Vec d) => -h x) (psi : H1MeanZeroFunction U) : sigma0 * ∫ (x : Vec d) in U, vecDot (u.toH1Function.grad x) (psi.toH1Function.grad x) = -∫ (x : Vec d) in U, vecDot (h x) (psi.toH1Function.grad x)

Convert the raw scalar-matrix Neumann predicate with datum -h to the explicit constant-coefficient negative-pairing equation.

theorem HCPolySupport.H1MeanZeroFunction.cubeFaceReflectionBlockFold_neumannDivergence_weakEquationOnBlock {d : ℕ} {m : ℤ} {sigma0 : ℝ} (u : H1MeanZeroFunction (openCubeSet (originCube d m))) {h : Vec d → Vec d} (hh : MemVectorL2 (openCubeSet (originCube d m)) h) (hweak : IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => scalarMatrix sigma0) (openCubeSet (originCube d m)) u fun (x : Vec d) => -h x) {phi : Vec d → ℝ} (hphi : ContDiff ℝ (↑⊤) phi) (hphi_compact : HasCompactSupport phi) : sigma0 * ∫ (x : Vec d) in cubeFaceReflectionBlockSet (originCube d m), vecDot (u.toH1Function.cubeFaceReflectionBlockFold.grad x) (euclideanGradient phi x) = -∫ (x : Vec d) in cubeFaceReflectionBlockSet (originCube d m), vecDot (cubeCoordinateFoldReflectedVectorField (originCube d m) h x) (euclideanGradient phi x)

The block-folded source solution satisfies the reflected compact-test divergence equation on the full reflection block.

theorem HCPolySupport.exists_h1Function_neumannEvenReflectionParent_divergence_rhs_originCube {d : ℕ} {m : ℤ} {sigma0 : ℝ} (u : H1MeanZeroFunction (openCubeSet (originCube d m))) {h : Vec d → Vec d} (hh : MemVectorL2 (openCubeSet (originCube d m)) h) (hweak : IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => scalarMatrix sigma0) (openCubeSet (originCube d m)) u fun (x : Vec d) => -h x) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), (uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => u.toH1Function.grad y) ∧ ∀ (phi : Vec d → ℝ), ContDiff ℝ (↑⊤) phi → HasCompactSupport phi → tsupport phi ⊆ openCubeSet (originCube d (m + 1)) → sigma0 * ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), vecDot (uP.grad x) (euclideanGradient phi x) = -∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), vecDot (cubeCoordinateFoldReflectedVectorField (originCube d m) h x) (euclideanGradient phi x)

An honest parent-cube H¹ realization of the Neumann even reflection, together with its compact-test divergence equation.

theorem HCPolySupport.exists_h1Function_neumannEvenReflectionParent_divergence_rhs_of_cubeData {d : ℕ} {m : ℤ} {q : FiniteLpExponent} {sigma0 : ℝ} (u : H1MeanZeroFunction (openCubeSet (originCube d m))) (h : CubeEuclideanL2LpField (originCube d m) q) (hweak : IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => scalarMatrix sigma0) (openCubeSet (originCube d m)) u fun (x : Vec d) => -h.toField x) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), (uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => u.toH1Function.grad y) ∧ ∀ (phi : Vec d → ℝ), ContDiff ℝ (↑⊤) phi → HasCompactSupport phi → tsupport phi ⊆ openCubeSet (originCube d (m + 1)) → sigma0 * ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), vecDot (uP.grad x) (euclideanGradient phi x) = -∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), vecDot (h.neumannEvenReflectionToParent.toField x) (euclideanGradient phi x)

The reflected-parent package specialized to an L² ∩ L^p cube datum.