Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.HessianRestrictionSum

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

Disjoint restriction summation for Hessian rows

This file proves the measure-theoretic part of the C.2 depth summation: the sum of squared L² norms of a Hessian row over disjoint descendant open cubes is bounded by the parent-cube row norm.

theorem HCPolySupport.HasWeakHessianOn.descendants_sum_restrict_gradCoordH1Function_gradToVectorL2_norm_sq_le {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (i : Fin d) (j : ℕ) : ∑ R ∈ descendantsAtDepth Q j, (if hR : R ∈ descendantsAtDepth Q j then ‖((H.restrict ⋯ ⋯).gradCoordH1Function i).gradToVectorL2‖ else 0) ^ 2 ≤ ‖(H.gradCoordH1Function i).gradToVectorL2‖ ^ 2

Squared L² norms of a Hessian row over depth-j descendant open cubes sum to at most the parent-cube squared row norm.

theorem HCPolySupport.HasWeakHessianOn.besovGradientCoord_le_hessianGradientCoordL2 {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 : ℝ} (hK : 0 ≤ K) (hfactor : ∀ (R : TriadicCube d) (hR : R ∈ descendantsAtDepth Q j), (cubeVolume R)⁻¹ ^ (1 / 2) * (hC R hR).constantValue ≤ K) : cubeBesovDepthSeminorm Q 1 2 (fun (x : Vec d) => u.grad x i) j ≤ cubeBesovDepthWeight Q 1 j * (K * ((↑(descendantsAtDepth Q j).card)⁻¹ * ‖(H.gradCoordH1Function i).gradToVectorL2‖ ^ 2) ^ (1 / 2))

Scale-sharp depth handoff after disjoint restriction summation, stated with the global Hessian row norm.

theorem HCPolySupport.HasWeakHessianOn.besovGradientCoord_le_hessianCoordL2Norm {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 : ℝ} (hK : 0 ≤ K) (hfactor : ∀ (R : TriadicCube d) (hR : R ∈ descendantsAtDepth Q j), (cubeVolume R)⁻¹ ^ (1 / 2) * (hC R hR).constantValue ≤ K) : cubeBesovDepthSeminorm Q 1 2 (fun (x : Vec d) => u.grad x i) j ≤ cubeBesovDepthWeight Q 1 j * (K * ((↑(descendantsAtDepth Q j).card)⁻¹ * H.hessianCoordL2NormSum ^ 2) ^ (1 / 2))

Scale-sharp depth handoff after disjoint restriction summation, in the global Hessian-coordinate-sum form produced by the reflected interior theorem.