Coarse-graining support: Support.Sobolev.Fractional.TailSummation #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Backwards geometric tail summation #
The per-pair scale accounting of the Besov-to-Gagliardo direction: summing the
coefficients q^j over any finite set of depths on which q^j is bounded by
M costs at most 2 * M, provided the ratio q is at least 3. Applied
with q = 3^{s p + d} and M = (dist x y)^{-(s p + d)}-ish this is the
geometric tail that makes the comparison constant dimensional.
theorem
HCPolySupport.Gagliardo.sum_pow_le_two_mul_of_forall_le
{q : ENNReal}
(hq3 : 3 ≤ q)
(hqt : q ≠ ⊤)
{M : ENNReal}
{F : Finset ℕ}
(hF : ∀ j ∈ F, q ^ j ≤ M)
:
Backwards geometric summation: if every term q^j, j ∈ F, is bounded by
M and the ratio satisfies 3 ≤ q < ∞, then the total is at most 2 * M.