Coarse-graining support: #
Support.Deterministic.ConstantCoefficientDirichletBesov.StandardProjectionBoundaryGap
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Projection gaps from boundary-budgeted increments #
This file sits downstream of StandardProjectionBoundary: the boundary file
controls one martingale increment by an abstract ancestor budget. Here we
insert that one-increment estimate into the already-proved telescoping estimate
for the projection gap P_j u - P_0 u.
theorem
HCPolySupport.cubeBesovOverlappingPositiveVectorDepthSeminorm_cubeIncrementVec_le_sqrt_boundaryBudget
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(u : Vec d → Vec d)
{j m : ℕ}
(hmj : m ≤ j)
(B : TriadicCube d → ℝ)
(hB : ∀ R ∈ descendantsAtDepth Q (m + 1), 0 ≤ B R)
(hbound :
∀ R ∈ descendantsAtDepth Q (m + 1),
∀ S ∈ descendantBoundaryLayerAtDepth R (j - m),
overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S (cubeIncrementVec Q (m + 1) u)) ^ 2 ≤ B R)
:
Seminorm form of the one-increment boundary-budget estimate.
theorem
HCPolySupport.cubeBesovOverlappingPositiveVectorDepthSeminorm_gap_zero_le_sum_sqrt_boundaryBudget
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(u : Vec d → Vec d)
(j : ℕ)
(B : ℕ → TriadicCube d → ℝ)
(hincLoc :
∀ S ∈ overlapCentersAtDepth Q j,
∀ m ∈ Finset.range j, MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S))
(hB : ∀ m ∈ Finset.range j, ∀ R ∈ descendantsAtDepth Q (m + 1), 0 ≤ B m R)
(hbound :
∀ m ∈ Finset.range j,
∀ R ∈ descendantsAtDepth Q (m + 1),
∀ S ∈ descendantBoundaryLayerAtDepth R (j - m),
overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S (cubeIncrementVec Q (m + 1) u)) ^ 2 ≤ B m R)
:
The projection gap is controlled by the sum of square-root boundary budgets for its martingale increments.