Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.PositiveBesovCore

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

Positive Besov handoff for the cube Neumann W^{2,2} route

This file records the algebraic endpoint bridge from the positive vector Besov seminorms controlled by the Hessian/Poincare part of the C.2 argument to the downstream CubePoissonGradientDualTestNormL2CoreEstimate.

The remaining analytic content is intentionally visible in the hypotheses: uniform control of the positive vector partial seminorms of the Poisson gradient, and of the component averages.

theorem HCPolySupport.cubeBesovDualTestNorm_two_one_component_le_scaleWeight_mul_posVectorPartial_add_avg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (i : Fin d) (N : ℕ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : (cubeBesovDualTestNorm Q s 2 1 N fun (x : Vec d) => u x i) ≤ cubeBesovScaleWeight s Q * cubeBesovPositiveVectorPartialSeminormTwo Q s N u + cubeBesovScaleWeight s Q * ‖cubeAverage Q fun (x : Vec d) => u x i‖

Componentwise B¹_{2,1} positive dual-test control by the positive vector partial seminorm, plus the cube-average mode. This is the local form needed by the Neumann CZ endpoint target.

theorem HCPolySupport.cubeBesovDualTestNorm_two_one_eq_partialSeminormTop_add_avg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (g : Vec d → ℝ) : cubeBesovDualTestNorm Q s 2 1 N g = cubeBesovPartialSeminormTop Q s 2 N g + cubeBesovScaleWeight s Q * ‖cubeAverage Q g‖

Scalar form of the q = 1 dual-test norm at p = 2: the top positive partial seminorm plus the average mode.

theorem HCPolySupport.cubeBesovPartialSeminormTop_le_of_forall_depthSeminorm_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (g : Vec d → ℝ) {B : ℝ} (hB : ∀ j ∈ Finset.range (N + 1), cubeBesovDepthSeminorm Q s p g j ≤ B) : cubeBesovPartialSeminormTop Q s p N g ≤ B

A finite top seminorm is bounded once each depth seminorm in its finite range is bounded.

theorem HCPolySupport.cubeBesovDepthSeminorm_two_le_depthWeight_mul_of_descendant_oscillation_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (g : Vec d → ℝ) (j : ℕ) {A : ℝ} (hA : 0 ≤ A) (hosc : ∀ R ∈ descendantsAtDepth Q j, cubeBesovOscillation R 2 g ≤ A) : cubeBesovDepthSeminorm Q s 2 g j ≤ cubeBesovDepthWeight Q s j * A

If the scalar oscillation is uniformly bounded on every depth-j descendant, then the depth seminorm is bounded by the depth weight times that uniform bound.

theorem HCPolySupport.cubeBesovDepthSeminorm_two_le_depthWeight_mul_descendantsAverage_sq_rpow_half {d : ℕ} (Q : TriadicCube d) (s : ℝ) (g : Vec d → ℝ) (j : ℕ) (A : TriadicCube d → ℝ) (_hA : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ A R) (hosc : ∀ R ∈ descendantsAtDepth Q j, cubeBesovOscillation R 2 g ≤ A R) : cubeBesovDepthSeminorm Q s 2 g j ≤ cubeBesovDepthWeight Q s j * (descendantsAverage Q j fun (R : TriadicCube d) => A R ^ 2) ^ (1 / 2)

Averaged version of the scalar depth handoff. If the scalar oscillation is pointwise bounded by a nonnegative descendant-local quantity A R, then the depth seminorm is bounded by the depth weight times the descendant L² average of A. This is the form compatible with summing local Hessian energy, rather than taking a sup over all descendants.

theorem HCPolySupport.cubePoissonGradientDualTestNormL2CoreEstimate_of_posVectorPartial_and_average {d : ℕ} {Q : TriadicCube d} {Cpos Cavg : ℝ} (hCpos : 0 ≤ Cpos) (hCavg : 0 ≤ Cavg) (hpos : ∀ (F : Vec d → ℝ), MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q) → cubeAverage Q F = 0 → ∀ (W : MeanZeroNeumannPoissonSolution Q F) (N : ℕ), (cubeBesovScaleWeight 1 Q * cubeBesovPositiveVectorPartialSeminormTwo Q 1 N fun (x : Vec d) => W.w.toH1Function.grad x) ≤ Cpos * cubeLpNorm Q 2 F) (havg : ∀ (F : Vec d → ℝ), MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q) → cubeAverage Q F = 0 → ∀ (W : MeanZeroNeumannPoissonSolution Q F) (i : Fin d), cubeBesovScaleWeight 1 Q * ‖cubeAverage Q fun (x : Vec d) => W.w.toH1Function.grad x i‖ ≤ Cavg * cubeLpNorm Q 2 F) : CubePoissonGradientDualTestNormL2CoreEstimate Q (Cpos + Cavg)

If the Poisson gradient has uniform positive-vector Besov seminorm control and controlled component averages, then it satisfies the exact downstream L² core dual-test estimate.

This is deliberately conditional: proving the two hypotheses from the weak Hessian witness and local Poincare is the remaining analytic bridge.

theorem HCPolySupport.cubePoissonGradientDualTestNormL2CoreEstimate_of_partialSeminormTop_and_average {d : ℕ} {Q : TriadicCube d} {Csemi Cavg : ℝ} (hCsemi : 0 ≤ Csemi) (hCavg : 0 ≤ Cavg) (hsemi : ∀ (F : Vec d → ℝ), MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q) → cubeAverage Q F = 0 → ∀ (W : MeanZeroNeumannPoissonSolution Q F) (i : Fin d) (N : ℕ), (cubeBesovPartialSeminormTop Q 1 2 N fun (x : Vec d) => W.w.toH1Function.grad x i) ≤ Csemi * cubeLpNorm Q 2 F) (havg : ∀ (F : Vec d → ℝ), MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q) → cubeAverage Q F = 0 → ∀ (W : MeanZeroNeumannPoissonSolution Q F) (i : Fin d), cubeBesovScaleWeight 1 Q * ‖cubeAverage Q fun (x : Vec d) => W.w.toH1Function.grad x i‖ ≤ Cavg * cubeLpNorm Q 2 F) : CubePoissonGradientDualTestNormL2CoreEstimate Q (Csemi + Cavg)

Scalar-top-seminorm version of the endpoint handoff. This is the form fed most directly by descendant Poincare estimates for each gradient component.

theorem HCPolySupport.cubePoissonGradientDualTestNormL2CoreEstimate_of_depthSeminorm_and_average {d : ℕ} {Q : TriadicCube d} {Cdepth Cavg : ℝ} (hCdepth : 0 ≤ Cdepth) (hCavg : 0 ≤ Cavg) (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) (havg : ∀ (F : Vec d → ℝ), MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q) → cubeAverage Q F = 0 → ∀ (W : MeanZeroNeumannPoissonSolution Q F) (i : Fin d), cubeBesovScaleWeight 1 Q * ‖cubeAverage Q fun (x : Vec d) => W.w.toH1Function.grad x i‖ ≤ Cavg * cubeLpNorm Q 2 F) : CubePoissonGradientDualTestNormL2CoreEstimate Q (Cdepth + Cavg)

Depthwise scalar-seminorm version of the endpoint handoff. This is the form most directly targeted by descendant Poincare estimates.