Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.NeumannInterior

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

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.exists_hasWeakHessianOn_restrict_hessianCoordL2NormSum_le_of_strict_inner_margin {d : ℕ} {V : Set (Vec d)} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (hV : IsOpenBoundedConvexDomain V) {ρ₁ ρ₂ σ₁ σ₂ ν : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hη_sub : tsupport η.toFun ⊆ V) (hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V) (θ : QuantitativeCubeCutoff Q σ₁ σ₂) (hVν : V ⊆ scaledClosedCubeSet Q ν) (hν_nonneg : 0 ≤ ν) (hνσ : ν < σ₁) (hσ₁_lt_one : σ₁ < 1) (hσ₂_nonneg : 0 ≤ σ₂) (hσ₂_lt_one : σ₂ < 1) (hρ₁_nonneg : 0 ≤ ρ₁) : ∃ (uS : H1Function (scaledOpenCubeSet Q ρ₁)), uS.toFun = W.w.toH1Function.toFun ∧ uS.grad = W.w.toH1Function.grad ∧ ∃ (H : HasWeakHessianOn (scaledOpenCubeSet Q ρ₁) uS), H.hessianCoordL2NormSum ≤ ∑ i : Fin d, ∑ _j : Fin d, WeakPoissonEquationOn.openCubeInnerQuotientHessianSmoothTestBound W.w.toH1Function F i θ

Local strict-inner weak Hessian estimate for a cube Neumann solution.

This is the direct Neumann-solution consumer of the hlim-free interior difference-quotient theorem. It is still an interior estimate: boundary crossing is reserved for the reflected-block enlargement step.