Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.OriginCubeEndpoint

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

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

The origin-cube depth constant obtained by combining the reflected-parent Hessian estimate with the parent-normalized descendant Poincare handoff.

Equations

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

theorem HCPolySupport.originCubeWeakInteriorDepthConstant_nonneg (d : ℕ) (m : ℤ) : 0 ≤ originCubeWeakInteriorDepthConstant d m

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.originCube_sum_reducedSolverEnergyBound_le_depthConstant_mul_cubeLpNorm {d : ℕ} {m : ℤ} {F : Vec d → ℝ} : (cubeVolume (originCube d m))⁻¹ ^ (1 / 2) * (originCubeMeanZeroH1CoerciveEstimate d 0).constantValue * ∑ k : Fin d, ∑ _l : Fin d, originCubeParentReducedSolverEnergyBound d m F k ≤ originCubeWeakInteriorDepthConstant d m * cubeLpNorm (originCube d m) 2 F

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeBesovDepthSeminorm_grad_originCube_le_weakInteriorDepthConstant {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) (hmean : cubeAverage (originCube d m) F = 0) (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (i : Fin d) (_N j : ℕ) (_hj : j ∈ Finset.range (_N + 1)) : cubeBesovDepthSeminorm (originCube d m) 1 2 (fun (x : Vec d) => W.w.toH1Function.grad x i) j ≤ originCubeWeakInteriorDepthConstant d m * cubeLpNorm (originCube d m) 2 F

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubePoissonGradientDualTestNormL2CoreEstimate_originCube {d : ℕ} (m : ℤ) : CubePoissonGradientDualTestNormL2CoreEstimate (originCube d m) (originCubeWeakInteriorDepthConstant d m + cubePoissonGradientAverageConstant (originCube d m))