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.
Local uniform convergence of the periodized Gaussian
Statement
For every , the series defining converges absolutely and uniformly on each compact interval of . Its sum is continuous on and has period one.
Facts & Assumptions
Given: A real parameter .
Periodized Gaussian gridding kernel: is the series , with the real constant from the real elementary functions.
Dedekind completeness implies the Archimedean property: the natural numbers are unbounded above.
For , , and for the series diverges: if , then and its tails tend to zero.
The exponential function is strictly increasing, The exponential is positive and satisfies , Continuity and derivative on a real interval, The exponential function is smooth and , Sum, product, quotient, and chain rules from difference quotients, and Real elementary functions and their domains: is continuous and strictly increasing, by its power series, and for every real ; the difference-quotient definition and scalar power, sum and chain rules show each summand is differentiable and hence continuous, so each finite partial sum is continuous.
Real elementary functions and their domains: , whose integrand is at least on ; hence .
Proof
Given: .
Put using [F5] and , and set by [F4]. Fix and choose an integer by [F2]. For and , one has , hence . Since is increasing, the th nonnegative summand is at most by [F6]. The two-sided geometric tail is finite and tends to zero uniformly in as its starting index tends to infinity, by [F3]. This proves absolute and uniform convergence on every compact interval.
Each finite partial sum is continuous by [F1] and [F4]. Fix and , choose , and choose a partial-sum index for which the uniform tail on is below by step 1.1. Continuity of that finite partial sum at gives a neighborhood where its change is below ; the two tail values contribute less than . Thus the full sum is continuous at . Absolute convergence permits the reindexing in , giving . Since was arbitrary, the sum is continuous and one-periodic.
Depends on
- Periodized Gaussian gridding kernel
- Real elementary functions and their domains
- For $|r| < 1$, $\sum_{k \ge 0} r^k = 1/(1-r)$, and for $|r| \ge 1$ the series diverges
- Dedekind completeness implies the Archimedean property
- The exponential function is strictly increasing
- The exponential addition formula $\exp(x+y)=\exp(x)\exp(y)$
- The exponential is positive and satisfies $\exp(-x)=1/\exp(x)$
- Continuity and derivative on a real interval
- The exponential function is smooth and $(\exp)'=\exp$
- Sum, product, quotient, and chain rules from difference quotients
Used by
- Explicit periodized Gaussian spread-tail bound Lemma
- Explicit tail for the periodized Gaussian image sum Lemma
- Fourier series of the periodized Gaussian Lemma
Cited to discharge well-definedness by Periodized Gaussian gridding kernel.
Dependency tree · two levels
43 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 44–46 (standard reference, not scraped)
- Leslie Greengard and June-Yub Lee, Accelerating the Nonuniform Fast Fourier Transform (standard reference, not scraped)