LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Explicit periodized Gaussian spread-tail bound

Statement

Let $d \geq 1$ , $τ_{r} > 0$ , and integers $M_{r}, w_{r} \geq 1$ satisfy $M_{r} \geq 2 w_{r} + 1$ . Define $a_{r} = π / (τ_{r} M_{r}^{2})$ and $S_{r} = \frac{2}{1 - \exp (- a_{r})}, T_{r} = 2 \exp (- a_{r} w_{r}^{2}) (1 + \frac{1}{2 a_{r} w_{r}}) .$ For $x = (x_{r})_{r = 1}^{d} \in [0, 1)^{d}$ , let $W_{r} (x_{r}) = {ℓ \in {0, \dots, M_{r} - 1} : \min_{n \in Z} ∣ ℓ / M_{r} - x_{r} - n ∣ \leq w_{r} / M_{r}}, W (x) = \prod_{r = 1}^{d} W_{r} (x_{r}) .$ With $Φ_{τ} (z) = \prod_{r = 1}^{d} ϕ_{τ_{r}} (z_{r})$ , the omitted spreading mass obeys $\sum_{ℓ \in \prod_{r} {0, \dots, M_{r} - 1} ∖ W (x)} Φ_{τ} (ℓ_{1} / M_{1} - x_{1}, \dots, ℓ_{d} / M_{d} - x_{d}) \leq T_{d}, T_{d} : = \sum_{r = 1}^{d} T_{r} \prod_{s \neq r} S_{s} .$ Also $\sum_{ℓ_{r} = 0}^{M_{r} - 1} ϕ_{τ_{r}} (ℓ_{r} / M_{r} - x_{r}) \leq S_{r}$ for every coordinate and point.

Facts & Assumptions

Given: The stated finite dimension, positive $τ_{r}$ , integers $M_{r}, w_{r}$ , and point $x$ .

[F1]

Local uniform convergence of the periodized Gaussian: each periodized Gaussian is nonnegative, one-periodic, and its defining integer series converges absolutely and locally uniformly.

[F2]

For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges: for $0 < q < 1$ , the geometric series converges and its finite tails have the usual explicit sum.

[F3]

Continuity and derivative on a real interval, The exponential function is smooth and $(\exp)^{'} = \exp$ , and Sum, product, quotient, and chain rules from difference quotients: the power and product rules give $(t^{2})^{'} = 2 t$ , and the constant function has zero derivative by its difference quotient; hence $(t \mapsto - a t^{2})^{'} = - 2 a t$ . Combining this with $(\exp)^{'} = \exp$ and the scalar chain rule shows that $f_{a} (t) = \exp (- a t^{2})$ is differentiable with derivative $f_{a}^{'} (t) = - 2 a t \exp (- a t^{2})$ for $a > 0$ .

[F4]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ : if $G^{'} = g$ on a compact interval and $g$ is integrable, then $\int_{u}^{v} g = G (v) - G (u)$ .

[F5]

The exponential dominates every fixed nonnegative integer power at $+ \infty$ and The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ : $\exp (- a R^{2}) = 1 / \exp (a R^{2}) \to 0$ as $R \to \infty$ for $a > 0$ .

[F6]

Real elementary functions and their domains, The exponential function is strictly increasing, and The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ : $π = 4 \int_{0}^{1} (1 + t^{2})^{- 1} d t \geq 2 > 0$ , $\exp (0) = 1$ , and the exponential is positive and strictly increasing; hence $a_{r} > 0$ and $0 < \exp (- a_{r}) < 1$ .

Proof

1.1F1F2F6constructalgebra

Fix one coordinate, write $M = M_{r}$ , $τ = τ_{r}$ , $w = w_{r}$ , $a = π / (τ M^{2}) > 0$ by [F6], and $y = M x_{r}$ . Reindexing the finite grid index and period index by $m = ℓ + n M$ gives $\sum_{ℓ = 0}^{M - 1} ϕ_{τ} (ℓ / M - x_{r}) = \sum_{m \in Z} \exp (- a (m - y)^{2}) .$ For every integer $s \geq 0$ , at most two integers satisfy $s \leq ∣ m - y ∣ < s + 1$ . Their terms are at most $\exp (- a s^{2})$ ; for $s \geq 1$ , $s^{2} \geq s$ . Thus the sum is at most $2 \sum_{s = 0}^{\infty} \exp (- a s) = 2 / (1 - \exp (- a)) = S_{r}$ by [F2].

1.2F1F3F4F5algebra

If $ℓ \notin W_{r} (x_{r})$ , then every $m = ℓ + n M$ satisfies $∣ m - y ∣ > w$ . On either side of $y$ , the lattice distances form a unit-spaced sequence $d + n$ with $d > w$ . The first term is at most $\exp (- a w^{2})$ . For each later term, monotonicity of $f_{a}$ gives $f_{a} (d + n) \leq \int_{d + n - 1}^{d + n} f_{a} (t) d t$ . For $R > w$ , [F3]–[F4] give $\int_{w}^{R} f_{a} (t) d t \leq \frac{1}{w} \int_{w}^{R} t f_{a} (t) d t = \frac{\exp (- a w^{2}) - \exp (- a R^{2})}{2 a w} \leq \frac{\exp (- a w^{2})}{2 a w} .$ By [F5], the last subtracted term tends to zero as $R \to \infty$ . Taking limits of the finite tail sums, which converge by [F1], bounds each side by $\exp (- a w^{2}) (1 + 1 / (2 a w))$ . Both sides together yield $\sum_{ℓ \notin W_{r} (x_{r})} ϕ_{τ} (ℓ / M - x_{r}) \leq T_{r}$ .

2.1step 1.1step 1.2algebra∎

The complement of the product set $W (x)$ is the union of the $d$ sets where at least one coordinate index is outside its $W_{r} (x_{r})$ . Since all kernel terms are nonnegative, the total omitted product mass is at most the sum of the $d$ coordinate-tail product sums. Each such finite product factors into the one-coordinate tail in step 1.2 and the full-coordinate masses in step 1.1; hence it is at most $T_{r} \prod_{s \neq r} S_{s}$ . Summing over $r$ gives $T_{d}$ .

Depends on

Used by

Dependency tree · two levels

53 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jens Keiner, Stefan Kunis, and Antje Vollrath, The Nonequispaced FFT and its Applications, Part I, slides 48 and 54–58 (standard reference, not scraped)
Leslie Greengard and June-Yub Lee, Accelerating the Nonuniform Fast Fourier Transform (standard reference, not scraped)