Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.HessianBesovDepth

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

Descendant Poincare to Besov depth bounds

This file combines the gradient-coordinate Poincare bridge with the scalar Besov depth handoff. The remaining quantitative input is deliberately explicit: a uniform bound over all descendants at one depth for the local Hessian-row Poincare quantities.

theorem HCPolySupport.HasWeakHessianOn.cubeBesovDepthSeminorm_gradCoord_le_depthWeight_mul_of_descendant_hessianRow_bound {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)) {A : ℝ} (hA : 0 ≤ A) (hrow : ∀ (R : TriadicCube d) (hR : R ∈ descendantsAtDepth Q j), ((cubeVolume R)⁻¹ + 1) * (hC R hR).constantValue * ‖((H.restrict ⋯ ⋯).gradCoordH1Function i).gradToVectorL2‖ ≤ A) : cubeBesovDepthSeminorm Q 1 2 (fun (x : Vec d) => u.grad x i) j ≤ cubeBesovDepthWeight Q 1 j * A

Descendant Poincare plus the scalar depth handoff. If the local Poincare-controlled Hessian-row quantity is bounded by A on every depth-j descendant, then the depth-j Besov seminorm of the gradient component is bounded by the depth weight times A.

theorem HCPolySupport.HasWeakHessianOn.cubeBesovDepthSeminorm_gradCoord_le_depthWeight_mul_descendantsAverage_sq_rpow_half {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)) : cubeBesovDepthSeminorm Q 1 2 (fun (x : Vec d) => u.grad x i) j ≤ cubeBesovDepthWeight Q 1 j * (descendantsAverage Q j fun (R : TriadicCube d) => (if hR : R ∈ descendantsAtDepth Q j then ((cubeVolume R)⁻¹ + 1) * (hC R hR).constantValue * ‖((H.restrict ⋯ ⋯).gradCoordH1Function i).gradToVectorL2‖ else 0) ^ 2) ^ (1 / 2)

Averaged descendant Poincare handoff for a Hessian row. This avoids the too-strong descendant supremum from cubeBesovDepthSeminorm_gradCoord_le_depthWeight_mul_of_descendant_hessianRow_bound; the right side is the descendant L² average of the local Poincare-controlled Hessian-row quantities.

theorem HCPolySupport.HasWeakHessianOn.cubeBesovDepthSeminorm_gradient_le_weightedDescendantVolumeNorm {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)) : cubeBesovDepthSeminorm Q 1 2 (fun (x : Vec d) => u.grad x i) j ≤ cubeBesovDepthWeight Q 1 j * (descendantsAverage Q j fun (R : TriadicCube d) => (if hR : R ∈ descendantsAtDepth Q j then (cubeVolume R)⁻¹ ^ (1 / 2) * (hC R hR).constantValue * ‖((H.restrict ⋯ ⋯).gradCoordH1Function i).gradToVectorL2‖ else 0) ^ 2) ^ (1 / 2)

Scale-sharp averaged descendant Poincare handoff for a Hessian row.

This is the q=2 version of the previous averaged estimate with the exact normalized L² factor volume^{-1/2}. It is the correct summation shape for the reflection proof: descendant volumes and the number of descendants can cancel when the restricted Hessian-row norms are squared and averaged.

theorem HCPolySupport.HasWeakHessianOn.cubeBesovDepthSeminorm_gradCoord_le_depthWeightedBy_const_mul {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) (hB : 0 ≤ B) (hfactor : ∀ (R : TriadicCube d) (hR : R ∈ descendantsAtDepth Q j), (cubeVolume R)⁻¹ ^ (1 / 2) * (hC R hR).constantValue ≤ K) (havg : (descendantsAverage Q j fun (R : TriadicCube d) => (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 * B)

Scale-sharp averaged Hessian-row handoff with the remaining quantitative inputs explicit: a uniform bound K on volume(R)^{-1/2} * PoincareConstant(R), and an L² descendant-average bound B on the restricted Hessian row.

theorem HCPolySupport.HasWeakHessianOn.cubeBesovDepthSeminorm_gradCoord_le_depthWeight_mul_const_mul_of_descendantsAverage_hessianRow {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) (hB : 0 ≤ B) (hfactor : ∀ (R : TriadicCube d) (hR : R ∈ descendantsAtDepth Q j), ((cubeVolume R)⁻¹ + 1) * (hC R hR).constantValue ≤ K) (havg : (descendantsAverage Q j fun (R : TriadicCube d) => (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 * B)

Averaged Hessian-row handoff with the two remaining quantitative inputs made explicit: a uniform bound K on the descendant-local Poincare prefactor, and an L² descendant-average bound B on the restricted Hessian row.

theorem HCPolySupport.HasWeakHessianOn.cubeBesovDepthSeminorm_gradCoord_le_depthWeight_mul_const_mul_global_hessianRow {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) * (hC R hR).constantValue ≤ K) : cubeBesovDepthSeminorm Q 1 2 (fun (x : Vec d) => u.grad x i) j ≤ cubeBesovDepthWeight Q 1 j * (K * ‖(H.gradCoordH1Function i).gradToVectorL2‖)

Variant of the averaged Hessian-row handoff using only the global Hessian row norm. The localization input is discharged by monotonicity of the L² norm under restriction; the remaining quantitative hypothesis is the uniform bound K for the descendant-local Poincare prefactor.

theorem HCPolySupport.HasWeakHessianOn.cubeBesovDepthSeminorm_gradCoord_le_depthWeight_mul_const_mul_hessianCoordL2NormSum {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) * (hC R hR).constantValue ≤ K) : cubeBesovDepthSeminorm Q 1 2 (fun (x : Vec d) => u.grad x i) j ≤ cubeBesovDepthWeight Q 1 j * (K * H.hessianCoordL2NormSum)

Depth estimate stated in terms of the global Hessian-coordinate sum. This is the form aligned with the reflected interior estimate, which controls H.hessianCoordL2NormSum.