Alphabeta Math
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.

Poisson periodization of a normalized Gaussian on a full-rank lattice

Statement

Assume Countable Choice and use the full-rank cell and angular frequencies of Neutral point sources and Fourier data on a three-dimensional torus. Here S(R3) denotes the Schwartz space of smooth functions whose derivatives decay faster than every inverse polynomial. For α>0 let gα(x)=α3π3/2e−α2∣x∣2. For every x∈R3 the two series below converge absolutely, locally uniformly in x, and ∑λ∈Λgα(x+λ)=1V∑k∈Z3e−∣κk∣2/(4α2)eiκk⋅x. The lattice Poisson theorem is applied only to this Schwartz Gaussian; it is not applied to a compactly supported or finite-smoothness assignment window.

Facts & Assumptions

Given: Countable Choice, an invertible cell matrix A, V=∣det⁡A∣, Λ=AZ3, Λ∗=A−TZ3, κk=2πA−Tk, α>0, and x∈R3.

[A1]

Countable Choice is required by the published lattice Poisson theorem and the Gaussian transform supplier (The Axiom of Countable Choice (ACω)).

[F1]

For f∈S(R3), both lattice series converge absolutely and the periodization satisfies ∑λ∈Λf(x+λ)=V−1∑ξ∈Λ∗f^(ξ)e2πiξ⋅x under Countable Choice (Poisson summation for a full-rank lattice).

[F2]

With f^(ξ)=∫R3f(x)e−2πiξ⋅xdx, F(e−πt∣x∣2)(ξ)=t−3/2e−π∣ξ∣2/t for t>0 under Countable Choice (Euclidean Gaussian transform with the 2π normalization).

[F3]

The normalized Gaussian in the screened-kernel definition is gα(x)=α3π−3/2e−α2∣x∣2 (Gaussian screened Coulomb kernel and its self limit).

[F4]

The lattice is AZ3, its dual is A−TZ3, and the physical angular frequency for index k is κk=2πA−Tk (Neutral point sources and Fourier data on a three-dimensional torus).

Proof

technique · direct
1.1givenA1F2F3algebra

Put t=α2/π>0. By [F2], the Fourier transform of e−πt∣x∣2 is t−3/2e−π∣ξ∣2/t. Multiplying the input by α3/π3/2 cancels t−3/2=(π/α2)3/2, so g^α(ξ)=e−π2∣ξ∣2/α2. Each derivative of gα is a polynomial times e−α2∣x∣2. For every degree d and integer N, choose an integer m>(d+N)/2; the inequality ey≥ym/m! for y≥0 bounds ∣x∣d(1+∣x∣)Ne−α2∣x∣2 on ∣x∣≥1, and continuity bounds it on the unit ball. Hence gα∈S(R3), so [F1] applies.

1.2givenF3F4algebra

Fix a compact set C⊂R3 and choose R with ∣x∣≤R on C. Since A is invertible, ∣An∣≥c∣n∣ for c=∥A−1∥2−1>0. For ∣n∣≥2R/c, ∣x+An∣≥c∣n∣/2 uniformly on C, so gα(x+An)≤α3π−3/2e−b∣n∣2 with b=α2c2/4>0. This majorant is summable: ∑n∈Z3e−b∣n∣2=(∑j∈Ze−bj2)3<∞, since e−bj2≤e−b∣j∣ for ∣j∣≥1. The remaining finitely many indices have bounded terms. Bounding every series tail by the corresponding majorant tail proves absolute uniform convergence on C.

2.1A1F1F4step 1.1step 1.2algebra∎

Apply [F1] to gα. Every ξ∈Λ∗ has the unique form ξ=A−Tk with k∈Z3; by [F4], 2πξ=κk. Therefore π2∣ξ∣2/α2=∣κk∣2/(4α2) and e2πiξ⋅x=eiκk⋅x. Substitution in the periodization formula gives exactly the displayed reciprocal series, and [F1] supplies absolute convergence on both sides. At x=0, absolute convergence of the reciprocal series gives ∑ke−∣κk∣2/(4α2)<∞. Since ∣eiκk⋅x∣=1, this same sum bounds reciprocal-series tails uniformly in all x. Together with step 1.2 this proves both asserted local uniform convergence claims.

Depends on

Used by

Dependency tree · two levels

39 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