Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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.

Poisson summation for Schwartz functions

Statement

Assume countable choice. For f∈S(Rn), ∑k∈Znf(x+k)=∑k∈Znf^(k)e2πik⋅x(x∈Rn). The left series converges locally uniformly with every derivative; the right series converges absolutely uniformly on all of Rn. At x=0 this gives ∑kf(k)=∑kf^(k), both sums absolutely convergent.

Facts & Assumptions

Given: The Axiom of Countable Choice (ACω); sums over Zn are limits over increasing integer cubes, with absolute convergence making their ordering immaterial.

[F1]

Fourier preserves Schwartz space (Fourier transform acts continuously on Schwartz space).

[F2]

Schwartz derivatives are integrable; their proof supplies the product-weight bound (Schwartz derivatives are integrable).

[F3]

Continuous periodic functions are uniquely determined by their coefficients (Fourier uniqueness for continuous functions on the Euclidean torus).

[F4]

Tonelli, Fubini and dominated convergence apply with nonnegative or absolute-integrable majorants as appropriate (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Fubini's theorem for L1 functions on a sigma-finite product, Dominated convergence).

[F6]

Complex interval FTC computes exponential integrals (Complex integration by parts on intervals and decaying lines).

[F7]

Translation substitution holds for integrable complex functions (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions).

Proof

technique · direct
1.1F2F5givenalgebra

For each β, expansion of W(y)=∏j(1+yj2) gives ∣∂βf(y)∣≤Aβ/W(y) with Aβ=∑ϵ∈{0,1}np2ϵ,β(f), as in [F2]. On a fixed bounded box ∣xj∣≤L, the elementary inequality 1+kj2≤(2+2L2)(1+(xj+kj)2) shows ∣∂βf(x+k)∣≤Aβ(2+2L2)n∏j(1+kj2)−1. The one-dimensional series of reciprocal weights converges: on 2r≤∣k∣<2r+1 its sum is at most 21−r, with the term k=0 separate. The finite product series therefore converges. Uniform tail bounds prove absolute uniform convergence of all derivative series on that box. Applying [F5] componentwise on each coordinate segment to finite partial sums, and iterating for ordered derivatives, proves that P(x)=∑kf(x+k) is smooth with the asserted derivatives. Absolute convergence permits reindexing, so P is periodic.

2.1step 1.1F2F4F7given

On Q=[0,1)n, the tiling {Q+k:k∈Zn} is disjoint and exhausts Rn. Translation substitution [F7] and [F4] give ∑k∫Q∣f(x+k)∣ dx=∫∣f∣<∞. Thus exchanging the coefficient integral and sum is justified. For ℓ∈Zn, substitute y=x+k in each term; e2πiℓ⋅k=1, so ∫QP(x)e−2πiℓ⋅x dx=∫Rnf(y)e−2πiℓ⋅y dy=f^(ℓ). The closed cube gives the same integral because its added coordinate faces are null.

2.2step 1.1F1F4F6given

By [F1] and the weight estimate of step 1.1 at x=0, ∑k∣f^(k)∣<∞. Therefore H(x)=∑kf^(k)e2πik⋅x converges absolutely uniformly for all x, is continuous and periodic. Its coefficient at ℓ is f^(ℓ): interchange sum and integral by the summable constant majorant, using [F4]. Each exponential product integral factors by [F4], and each factor is ∫01e2πirt dt=0 for nonzero integer r, by its antiderivative and [F6], or 1 for r=0. Hence only k=ℓ survives.

3.1step 2.1step 2.2F3∎

The continuous periodic function P−H has every coefficient zero by steps 2.1 and 2.2. [F3] makes it zero everywhere. Evaluation at zero gives the unshifted formula, with absolute convergence already proved. Countable choice is precisely the inherited Euclidean integration and Schwartz Fourier hypothesis; the lattice ordering, majorants and partial sums are explicit.

Depends on

Used by

Dependency tree · two levels

75 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