Documentation

TauCeti.Analysis.SpecificLimits.DyadicSum

Sums over dyadic scales #

For u > 0 and δ > 0, the sum over all dyadic scales 2 ^ j, j ∈ ℤ, of min (2 ^ j u) ((2 ^ j u) ^ (-δ)) is bounded independently of u: the terms with 2 ^ j u ≤ 1 form a geometric series of ratio 1/2 dominated by its largest term, and the terms with 2 ^ j u > 1 a geometric series of ratio 2 ^ (-δ). This is how per-scale estimates of the shape "at most 2 ^ j ‖h‖ for small scales and at most (2 ^ j ‖h‖) ^ (-δ) for large ones" are summed into a bound uniform in h, as in the verification of Hörmander's condition for the kernel of a Fourier multiplier cut into Littlewood–Paley pieces.

Main declarations #

References #

theorem TauCeti.sum_min_zpow_mul_rpow_neg_le {δ u : ℝ} (hδ : 0 < δ) (hu : 0 < u) (s : Finset ℤ) :
∑ j ∈ s, min (2 ^ j * u) ((2 ^ j * u) ^ (-δ)) ≤ 2 + (1 - 2 ^ (-δ))⁻¹

For u > 0 and δ > 0, summing min (2 ^ j u) ((2 ^ j u) ^ (-δ)) over any finite set of integers j gives at most 2 + (1 - 2 ^ (-δ))⁻¹, independently of u.