Summability of the deterministic cutoff multiplier

This module is the layer-L2 home of the lattice majorants for the Fourier multiplier of a fixed smooth cutoff. The results are purely deterministic and are shared by the random Fourier-series construction and the R-324 frequency-routing argument.

noncomputable def Anderson4D.latticeSummabilityWeight (k : Z4) : ℝ

Product p-series weight on ℤ⁴. The exponent two in each coordinate makes it summable and its total polynomial degree is eight.

Equations

• Anderson4D.latticeSummabilityWeight k = ∏ i : Fin Anderson4D.dim, ((↑(k i).natAbs + 1) ^ 2)⁻¹

def Anderson4D.latticePolynomialWeight (r : ℕ) (k : Z4) : ℝ

A convenient polynomial lattice weight. The added one in every coordinate avoids exceptional treatment of the zero mode.

Equations

• Anderson4D.latticePolynomialWeight r k = (∑ i : Fin Anderson4D.dim, (↑(k i).natAbs + 1)) ^ r

theorem Anderson4D.latticePolynomialWeight_nonneg (r : ℕ) (k : Z4) : 0 ≤ latticePolynomialWeight r k

theorem Anderson4D.summable_latticeSummabilityWeight : Summable latticeSummabilityWeight

The explicit degree-eight product weight is summable on ℤ⁴.

theorem Anderson4D.SmoothCutoff.exists_symbol_norm_le_latticeSummabilityWeight (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (k : Z4), ‖ρ.symbol ε k‖ ≤ C * latticeSummabilityWeight k

At every positive scale the cutoff symbol is dominated by a fixed summable product weight on ℤ⁴.

theorem Anderson4D.SmoothCutoff.summable_norm_symbol (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : Summable fun (k : Z4) => ‖ρ.symbol ε k‖

Consequently, every positive-scale cutoff symbol is absolutely summable on the Fourier lattice.

theorem Anderson4D.SmoothCutoff.exists_latticePolynomialWeight_mul_norm_symbol_le (ρ : SmoothCutoff) (r : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (k : Z4), latticePolynomialWeight r k * ‖ρ.symbol ε k‖ ≤ C * latticeSummabilityWeight k

Rapid decay survives multiplication by a polynomial lattice weight of arbitrary degree.

theorem Anderson4D.SmoothCutoff.summable_latticePolynomialWeight_mul_norm_symbol (ρ : SmoothCutoff) (r : ℕ) {ε : ℝ} (hε : 0 < ε) : Summable fun (k : Z4) => latticePolynomialWeight r k * ‖ρ.symbol ε k‖

Every polynomially weighted cutoff symbol is absolutely summable.