Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.HessianBesovSummation

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

Descendant summation for the C.2 Hessian-to-Besov bridge

This file packages the finite summation side of the scale-sharp C.2 handoff. The analytic disjoint-restriction estimate is still supplied as an explicit sum hypothesis; the theorem below converts that sum bound into the descendant average required by HessianBesovDepth.

theorem HCPolySupport.HasWeakHessianOn.cubeBesovDepthSeminorm_gradient_le_depthWeightedHessianRow {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (i : Fin d) (j : ℕ) (hC : (R : TriadicCube d) → R ∈ descendantsAtDepth Q j → H1CoerciveEstimate (openCubeSet R)) {K B : ℝ} (hK : 0 ≤ K) (hfactor : ∀ (R : TriadicCube d) (hR : R ∈ descendantsAtDepth Q j), (cubeVolume R)⁻¹ ^ (1 / 2) * (hC R hR).constantValue ≤ K) (hsum : ∑ R ∈ descendantsAtDepth Q j, (if hR : R ∈ descendantsAtDepth Q j then ‖((H.restrict ⋯ ⋯).gradCoordH1Function i).gradToVectorL2‖ else 0) ^ 2 ≤ B ^ 2) : cubeBesovDepthSeminorm Q 1 2 (fun (x : Vec d) => u.grad x i) j ≤ cubeBesovDepthWeight Q 1 j * (K * ((↑(descendantsAtDepth Q j).card)⁻¹ * B ^ 2) ^ (1 / 2))

Scale-sharp depth handoff from a finite descendant sum bound on the restricted Hessian row. This is the exact form meant to receive the future disjoint-restriction estimate ∑_R ‖row‖²_{L²(R)} ≤ ‖row‖²_{L²(Q)}.