Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionParentExactEnergy

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

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.norm_gradToHilbertVectorL2_le_solverCubeLpNorm_exact {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 / 2) * cubeLpNorm (originCube d m) 2 F)

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.norm_toScalarL2_le_solverCubeLpNorm_exact {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 / 2) * cubeLpNorm (originCube d m) 2 F))

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

Scale-sharp forcing-facing reflected-parent reduced energy expression.

Equations

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

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.originCubeParentReducedNormEnergyBound_le_solverEnergyBoundExact {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 ≤ originCubeParentReducedSolverEnergyBoundExact d m F i

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.exists_reflected_parent_weakHessian_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, originCubeParentReducedSolverEnergyBoundExact d m F i

noncomputable def HCPolySupport.MeanZeroNeumannPoissonSolution.originCubeParentReducedSolverEnergyInsideExact (d : ℕ) (m : ℤ) : ℝ

The forcing-independent factor under the square root in the exact reflected Neumann solver bound, using the square root of cube volume.

Equations

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

noncomputable def HCPolySupport.MeanZeroNeumannPoissonSolution.originCubeParentReducedSolverEnergyConstantExact (d : ℕ) (m : ℤ) : ℝ

The square-root factor multiplying the normalized L² forcing norm in the exact reflected Neumann solver bound.

Equations

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

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.originCubeParentReducedSolverEnergyConstantExact_nonneg (d : ℕ) (m : ℤ) : 0 ≤ originCubeParentReducedSolverEnergyConstantExact d m

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.parentSolverEnergyConstant_volumeCancel (d : ℕ) (m : ℤ) : (cubeVolume (originCube d m))⁻¹ ^ (1 / 2) * originCubeParentReducedSolverEnergyConstantExact d m = originCubeParentReducedSolverEnergyConstantExact d 0

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.originCubeParentReducedSolverEnergyBoundExact_eq_constant_mul_cubeLpNorm (d : ℕ) (m : ℤ) (F : Vec d → ℝ) (i : Fin d) : originCubeParentReducedSolverEnergyBoundExact d m F i = originCubeParentReducedSolverEnergyConstantExact d m * cubeLpNorm (originCube d m) 2 F