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 , , and , Every polynomial times a positive real Gaussian is absolutely integrable.
Facts & Assumptions
Given: , and The Axiom of Countable Choice ().
The real improper Gaussian integral equals (The Gaussian integral ).
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).
Exponential growth dominates each nonnegative integer power (The exponential dominates every fixed nonnegative integer power at ).
Complex differentiation under the integral is valid under an integrable derivative majorant (Differentiation under the integral sign).
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).
Absolutely integrable product integrals may be exchanged (Fubini's theorem for L^1 functions on a sigma-finite product).
The Lebesgue substitution formula uses the absolute determinant (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions).
Euler's formula and real trigonometric derivatives give (, , and , The derivatives of sine and cosine are cosine and minus sine).
Proof
For and integer , F3 bounds on the tails, and it is bounded on a compact middle interval by continuity. Thus . F1, F2 on both half-lines (reflect the negative half), and F7 give integrability of these majorants and . 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.
Put in dimension one. F4 applies on every frequency interval with derivative majorant from step 1.1. Hence . Apply F5 to and : both derivative products are integrable by step 1.1 and at both ends. Since and , it follows that , and therefore .
The product rule gives . Applying the finite-interval complex FTC to its real and imaginary parts shows this product is constant, equal to . Thus . F6 tensors this formula in coordinates; absolute integrability is supplied by step 1.1. Finally substitute using F7; the Jacobian is and the frequency becomes . 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.
Depends on
- The integral transform is representative independent
- A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions
- Fubini's theorem for L^1 functions on a sigma-finite product
- Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
- Dominated convergence
- The Gaussian integral $\int_{-\infty}^{\infty}e^{-x^2}\,dx=\sqrt{\pi}$
- A nonnegative improper Riemann integral on a half-line agrees with the Lebesgue integral
- Differentiation under the integral sign
- Complex integration by parts on intervals and decaying lines
- The exponential dominates every fixed nonnegative integer power at $+\infty$
- The derivatives of sine and cosine are cosine and minus sine
- $\exp(x+iy)=e^x(\cos y+i\sin y)$, $|\exp(x+iy)|=e^x$, and $e^{i\pi}+1=0$
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
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
- Semyon Dyatlov, MIT 18.155 (2022) (standard reference, not scraped)