Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.GradientAverage

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

Average mode for the cube Neumann CZ endpoint

The B^1_{2,1} dual-test norm contains a cube-average term for each gradient component. This file packages the existing Neumann energy estimate and the standard ‖average‖ ≤ L² bound into the exact average-mode estimate needed by the endpoint handoff.

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

The current cube-dependent constant supplied by the existing Neumann energy estimate for controlling the average mode of the Poisson gradient.

Equations

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

theorem HCPolySupport.cubePoissonGradientAverageConstant_nonneg {d : ℕ} (Q : TriadicCube d) : 0 ≤ cubePoissonGradientAverageConstant Q

theorem HCPolySupport.cubePoissonGradientAverageConstant_eq_dimensionConstant {d : ℕ} (Q : TriadicCube d) : cubePoissonGradientAverageConstant Q = ↑d * (originCubeMeanZeroH1CoerciveEstimate d 0).constantValue

theorem HCPolySupport.meanZeroNeumannPoissonSolution_cubeBesovScaleWeight_norm_cubeAverage_grad_le {d : ℕ} (Q : TriadicCube d) {F : Vec d → ℝ} (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (W : MeanZeroNeumannPoissonSolution Q F) (i : Fin d) : cubeBesovScaleWeight 1 Q * ‖cubeAverage Q fun (x : Vec d) => W.w.toH1Function.grad x i‖ ≤ cubePoissonGradientAverageConstant Q * cubeLpNorm Q 2 F

Component-average bound for the Poisson gradient, in exactly the weighted form consumed by cubePoissonGradientDualTestNormL2CoreEstimate_of_depthSeminorm_and_average.

theorem HCPolySupport.cubePoissonGradientDualTestNormL2CoreEstimate_of_depthSeminorm {d : ℕ} {Q : TriadicCube d} {Cdepth : ℝ} (hCdepth : 0 ≤ Cdepth) (hdepth : ∀ (F : Vec d → ℝ), MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q) → cubeAverage Q F = 0 → ∀ (W : MeanZeroNeumannPoissonSolution Q F) (i : Fin d) (N j : ℕ), j ∈ Finset.range (N + 1) → cubeBesovDepthSeminorm Q 1 2 (fun (x : Vec d) => W.w.toH1Function.grad x i) j ≤ Cdepth * cubeLpNorm Q 2 F) : CubePoissonGradientDualTestNormL2CoreEstimate Q (Cdepth + cubePoissonGradientAverageConstant Q)

Endpoint handoff with the average mode already discharged by the Neumann energy estimate. After this lemma, the remaining endpoint input is only the uniform depth-seminorm estimate for each gradient component.