Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ArbitraryCubeEndpoint

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

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

The centered-cube C.2 depth constant combining inverse square-root volume, unit-scale mean-zero coercivity, and the dimension-squared parent solver energy factor.

Equations

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

theorem HCPolySupport.originCubeWeakInteriorDepthConstantExact_nonneg (d : ℕ) (m : ℤ) : 0 ≤ originCubeWeakInteriorDepthConstantExact d m

noncomputable def HCPolySupport.cubeWeakInteriorDepthConstant {d : ℕ} (Q : TriadicCube d) : ℝ

The C.2 depth constant for an arbitrary cube, transported from the scale-sharp centered-cube estimate at the same scale.

Equations

• HCPolySupport.cubeWeakInteriorDepthConstant Q = HCPolySupport.originCubeWeakInteriorDepthConstantExact d Q.scale

theorem HCPolySupport.cubeWeakInteriorDepthConstant_nonneg {d : ℕ} (Q : TriadicCube d) : 0 ≤ cubeWeakInteriorDepthConstant Q

theorem HCPolySupport.originCubeWeakInteriorDepthConstantExact_eq_unit (d : ℕ) (m : ℤ) : originCubeWeakInteriorDepthConstantExact d m = originCubeWeakInteriorDepthConstantExact d 0

theorem HCPolySupport.cubeWeakInteriorDepthConstant_eq_dimensionConstant {d : ℕ} (Q : TriadicCube d) : cubeWeakInteriorDepthConstant Q = originCubeWeakInteriorDepthConstantExact d 0

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.originCube_sum_reducedSolverEnergyBoundExact_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, originCubeParentReducedSolverEnergyBoundExact d m F k ≤ originCubeWeakInteriorDepthConstantExact d m * cubeLpNorm (originCube d m) 2 F

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.exists_hasWeakHessianOn_cube_hessianCoordL2NormSum_le_solverEnergyBound {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (hmean : cubeAverage Q F = 0) (W : MeanZeroNeumannPoissonSolution Q F) : ∃ (H : HasWeakHessianOn (openCubeSet Q) W.w.toH1Function), H.hessianCoordL2NormSum ≤ ∑ i : Fin d, ∑ _j : Fin d, originCubeParentReducedSolverEnergyBoundExact d Q.scale (fun (x : Vec d) => F (x + triadicCubeShift Q)) i

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

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubePoissonGradientDualTestNormL2CoreEstimate_cube {d : ℕ} (Q : TriadicCube d) : CubePoissonGradientDualTestNormL2CoreEstimate Q (cubeWeakInteriorDepthConstant Q + cubePoissonGradientAverageConstant Q)