Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.StandardProjectionSummation

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

Summing geometric-tail depth estimates

The sharp boundary comparison gives a one-depth estimate whose hard term is a lower-triangular geometric tail of ordinary positive depth seminorms. This file converts such one-depth estimates into finite q = 2 positive Besov estimates.

theorem HCPolySupport.sq_cubeBesovOverlappingPositiveVectorPartialSeminormTwo_le_of_depth_geometric_tail {d : ℕ} (Q : TriadicCube d) (t : ℝ) (N : ℕ) (u : Vec d → Vec d) {A B r : ℝ} (hB_nonneg : 0 ≤ B) (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hdepth : ∀ j ∈ Finset.range (N + 1), cubeBesovOverlappingPositiveVectorDepthSeminorm Q t u j ^ 2 ≤ A * cubeBesovPositiveVectorDepthSeminorm Q t u j ^ 2 + B * (∑ m ∈ Finset.range j, r ^ (j - m) * cubeBesovPositiveVectorDepthSeminorm Q t u m) ^ 2) : cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q t N u ^ 2 ≤ (A + B * (1 - r)⁻¹ ^ 2) * cubeBesovPositiveVectorPartialSeminormTwo Q t N u ^ 2

If every overlapping depth contribution is controlled by the same-depth ordinary contribution plus a lower-triangular geometric tail of ordinary depth contributions, then the finite overlapping q = 2 seminorm is controlled by the ordinary finite q = 2 seminorm with the corresponding geometric loss.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorPartialSeminormTwo_le_sqrt_loss_of_depth_geometric_tail {d : ℕ} (Q : TriadicCube d) (t : ℝ) (N : ℕ) (u : Vec d → Vec d) {A B r : ℝ} (hB_nonneg : 0 ≤ B) (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hloss_nonneg : 0 ≤ A + B * (1 - r)⁻¹ ^ 2) (hdepth : ∀ j ∈ Finset.range (N + 1), cubeBesovOverlappingPositiveVectorDepthSeminorm Q t u j ^ 2 ≤ A * cubeBesovPositiveVectorDepthSeminorm Q t u j ^ 2 + B * (∑ m ∈ Finset.range j, r ^ (j - m) * cubeBesovPositiveVectorDepthSeminorm Q t u m) ^ 2) : cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q t N u ≤ √(A + B * (1 - r)⁻¹ ^ 2) * cubeBesovPositiveVectorPartialSeminormTwo Q t N u

Square-root form of sq_cubeBesovOverlappingPositiveVectorPartialSeminormTwo_le_of_depth_geometric_tail.