Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)
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.

Euclidean Gaussian transform with the 2π normalization

Statement

Assume countable choice. For n1, t>0, and ξRn, F(eπtx2)(ξ)=tn/2eπξ2/t. Every polynomial times a positive real Gaussian is absolutely integrable.

Facts & Assumptions

Given: n1, t>0 and The Axiom of Countable Choice (ACω).

[F1]

The real improper Gaussian integral equals π (The Gaussian integral ex2dx=π).

[F2]

Nonnegative convergent improper integrals agree with Lebesgue integrals under countable choice (A nonnegative improper Riemann integral on a half-line agrees with the Lebesgue integral).

[F3]

Exponential growth dominates each nonnegative integer power (The exponential dominates every fixed nonnegative integer power at +).

[F4]

Complex differentiation under the integral is valid under an integrable derivative majorant (Differentiation under the integral sign).

[F5]

Complex integration by parts on the line holds for integrable products and vanishing product boundaries; its finite-interval FTC also holds (Complex integration by parts on intervals and decaying lines).

[F6]

Absolutely integrable product integrals may be exchanged (Fubini's theorem for L^1 functions on a sigma-finite product).

[F7]

The C1 Lebesgue substitution formula uses the absolute determinant (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions).

[F8]

Euler's formula and real trigonometric derivatives give (e2πixξ)ξ=2πixe2πixξ (exp(x+iy)=ex(cosy+isiny), exp(x+iy)=ex, and eiπ+1=0, The derivatives of sine and cosine are cosine and minus sine).

Proof

1.1

For c>0 and integer m0, F3 bounds xmecx2/2 on the tails, and it is bounded on a compact middle interval by continuity. Thus xmecx2Cecx2/2. F1, F2 on both half-lines (reflect the negative half), and F7 give integrability of these majorants and eπx2dx=1. In several dimensions bound a polynomial by a finite sum of monomials and factor the Gaussian; successive nonnegative integration gives the product of the finite one-dimensional bounds.

F1F2F3F6F7given
2.1

Put G(ξ)=eπx2e2πixξdx in dimension one. F4 applies on every frequency interval with derivative majorant 2πxeπx2 from step 1.1. Hence G(ξ)=2πixeπx2e2πixξdx. Apply F5 to u=eπx2 and v=e2πixξ: both derivative products are integrable by step 1.1 and uv0 at both ends. Since u=2πxu and v=2πiξv, it follows that xuv=iξG(ξ), and therefore G=2πξG.

F4F5F8step 1.1
3.1

The product rule gives (eπξ2G(ξ))=0. Applying the finite-interval complex FTC to its real and imaginary parts shows this product is constant, equal to G(0)=1. Thus G(ξ)=eπξ2. F6 tensors this formula in n coordinates; absolute integrability is supplied by step 1.1. Finally substitute y=tx using F7; the Jacobian is tn/2 and the frequency becomes ξ/t. This gives exactly the claimed formula. Countable choice is inherited from F2 and F7, and the argument uses neither later Schwartz theory nor a Fourier inversion theorem.

F2F5F6F7step 1.1step 2.1

Depends on

Used by

Dependency tree · two levels

69 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