Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionParentSmoothBound

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

noncomputable def HCPolySupport.MeanZeroNeumannPoissonSolution.originCubeParentReducedOriginalEnergyBound {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (_i : Fin d) : ℝ

Original-cube energy bound obtained after reading the fixed-radii reflected-parent reduced smooth-test constant through the all-face reflection identities.

Equations

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

noncomputable def HCPolySupport.MeanZeroNeumannPoissonSolution.originCubeParentReducedNormEnergyBound {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (_i : Fin d) : ℝ

The same reflected-parent reduced energy bound, but with the original-cube forcing, gradient, and value integrals rewritten as the normalized forcing L² norm and the solver's L² realizations.

Equations

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

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.norm_gradToHilbertVectorL2_le_solverCubeLpNorm {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) : ‖W.w.toH1Function.gradToHilbertVectorL2‖ ≤ cubeMeanZeroH1CoerciveConstant (originCube d m) * ((cubeVolume (originCube d m) + 1) * cubeLpNorm (originCube d m) 2 F)

The solver gradient L² realization on the original cube is controlled by the normalized forcing L² norm.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.norm_toScalarL2_le_solverCubeLpNorm {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) : ‖W.w.toH1Function.toScalarL2‖ ≤ cubeMeanZeroH1CoerciveConstant (originCube d m) * (cubeMeanZeroH1CoerciveConstant (originCube d m) * ((cubeVolume (originCube d m) + 1) * cubeLpNorm (originCube d m) 2 F))

The solver value L² realization on the original cube is controlled by the normalized forcing L² norm, using the cube coercive estimate once more after the gradient estimate.

noncomputable def HCPolySupport.MeanZeroNeumannPoissonSolution.originCubeParentReducedSolverEnergyBound (d : ℕ) (m : ℤ) (F : Vec d → ℝ) (_i : Fin d) : ℝ

A fully forcing-facing version of the reflected-parent reduced energy bound. The remaining constants are explicit cube geometry and the coercive constant already used by the Neumann solver.

Equations

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

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.originCubeParentReducedNormEnergyBound_le_solverEnergyBound {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) (i : Fin d) : W.originCubeParentReducedNormEnergyBound i ≤ originCubeParentReducedSolverEnergyBound d m F i

The reflected-parent reduced norm energy is bounded by the explicit forcing-facing solver energy expression.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.originCubeParentReducedOriginalEnergyBound_eq_normEnergyBound {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) (i : Fin d) : W.originCubeParentReducedOriginalEnergyBound i = W.originCubeParentReducedNormEnergyBound i

The raw original-cube reflected-parent energy expression is exactly the same as its norm-realized form.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.reflectedParent_smoothTestEnergy_le_parentEnergy {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) {uP : H1Function (openCubeSet (originCube d (m + 1)))} (huP_toFun : uP.toFun = cubeCoordinateFoldReflectedScalar (originCube d m) W.w.toH1Function.toFun) (huP_grad : uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => W.w.toH1Function.grad y) (i : Fin d) : WeakPoissonEquationOn.openCubeInnerQuotientHessianSmoothTestReducedBound uP (cubeCoordinateFoldReflectedScalar (originCube d m) F) i (originCubeParentThreeQuarterSevenEighthCutoff d m) ≤ W.originCubeParentReducedOriginalEnergyBound i

A fixed-radii reduced smooth-test constant on the reflected parent is bounded by the corresponding original-cube energy expression.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.exists_hasWeakHessianOn_originCube_canonicalRadii_hessianCoordL2NormSum_le_reducedBound {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hmean : cubeAverage (originCube d m) F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), uP.toFun = cubeCoordinateFoldReflectedScalar (originCube d m) W.w.toH1Function.toFun ∧ (uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => W.w.toH1Function.grad y) ∧ ∃ (H : HasWeakHessianOn (openCubeSet (originCube d m)) W.w.toH1Function), H.hessianCoordL2NormSum ≤ ∑ i : Fin d, ∑ _j : Fin d, WeakPoissonEquationOn.openCubeInnerQuotientHessianSmoothTestReducedBound uP (cubeCoordinateFoldReflectedScalar (originCube d m) F) i (originCubeParentThreeQuarterSevenEighthCutoff d m)

The fixed-radii reflected-parent Hessian estimate with the raw smooth-test constant replaced by the reduced unweighted H¹ bound.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.exists_reflectedHessian_originalEnergyBound {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hmean : cubeAverage (originCube d m) F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), uP.toFun = cubeCoordinateFoldReflectedScalar (originCube d m) W.w.toH1Function.toFun ∧ (uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => W.w.toH1Function.grad y) ∧ ∃ (H : HasWeakHessianOn (openCubeSet (originCube d m)) W.w.toH1Function), H.hessianCoordL2NormSum ≤ ∑ i : Fin d, ∑ _j : Fin d, W.originCubeParentReducedOriginalEnergyBound i

The fixed-radii reflected-parent Hessian estimate, with the right-hand side expressed entirely in original-cube energy terms.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.exists_reflectedHessian_energyBound {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hmean : cubeAverage (originCube d m) F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), uP.toFun = cubeCoordinateFoldReflectedScalar (originCube d m) W.w.toH1Function.toFun ∧ (uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => W.w.toH1Function.grad y) ∧ ∃ (H : HasWeakHessianOn (openCubeSet (originCube d m)) W.w.toH1Function), H.hessianCoordL2NormSum ≤ ∑ i : Fin d, ∑ _j : Fin d, W.originCubeParentReducedNormEnergyBound i

The fixed-radii reflected-parent Hessian estimate with the right-hand side expressed through solver L² norms.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.exists_hasWeakHessianOn_originCube_canonicalRadii_hessianCoordL2NormSum_le_solverEnergyBound {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hmean : cubeAverage (originCube d m) F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), uP.toFun = cubeCoordinateFoldReflectedScalar (originCube d m) W.w.toH1Function.toFun ∧ (uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => W.w.toH1Function.grad y) ∧ ∃ (H : HasWeakHessianOn (openCubeSet (originCube d m)) W.w.toH1Function), H.hessianCoordL2NormSum ≤ ∑ i : Fin d, ∑ _j : Fin d, originCubeParentReducedSolverEnergyBound d m F i

The fixed-radii reflected-parent Hessian estimate with the right-hand side controlled by the explicit forcing-facing solver energy expression.