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.
Normalized Hermite Fourier eigenfunctions
Statement
Assume countable choice. On set Then is an orthonormal basis of complex , each is Schwartz, and . Basis means every has the norm-convergent expansion , with the pairing linear in its first variable.
Facts & Assumptions
Given: The Axiom of Countable Choice (), the Schwartz definition Schwartz space and its seminorms, and the everywhere-convergent exponential series The complex exponential by its power series.
Polynomial Gaussians are Schwartz (Polynomial Gaussians are Schwartz).
The Gaussian transform and integral have the stated normalization (Euclidean Gaussian transform with the 2π normalization).
Fourier interchanges differentiation and polynomial multiplication with their factors (Fourier transform acts continuously on Schwartz space).
Complex integration by parts holds on decaying lines (Complex integration by parts on intervals and decaying lines).
Complex is complete, with Cauchy–Schwarz and the first-variable-linear pairing (Complex completeness, density, and inner product: the consumer interface).
An integrable function with zero transform vanishes a.e. (Uniqueness of the L1 Fourier transform).
Dominated convergence passes limits through integrals (Dominated convergence).
Plancherel identifies the resulting eigenfunction identities also in (Plancherel theorem).
Verification
Put and . Differentiation gives and , since . Induction gives for , and for . If , then . Thus is real of degree with leading coefficient , and [F1] makes every Schwartz.
For polynomial Gaussians , [F4] gives : derivative products are polynomial Gaussians and integrable, and their endpoint products vanish. Consequently is symmetric on these functions, since . Step 1.1 implies . Also . The base norm is by [F2]. Hence and the normalized functions are orthonormal, including .
The derivative identities [F3] give . Since [F2] gives , induction yields and the asserted normalized identity. All operations are on Schwartz functions, so this also holds for their Plancherel classes.
Suppose is orthogonal to all . By the nonzero real leading coefficients in step 1.1, triangular induction expresses each monomial as a real linear combination of . Therefore for every ; these integrals exist by [F5], since . Put by [F5]. For fixed real , the exponential Taylor partial sums are bounded by . The majorant is integrable by [F5]: its second factor has finite square integral, because . Thus [F7] integrates the exponential series termwise, all terms being the zero moments. It gives for every . By [F6], a.e.; positivity of gives a.e.
For arbitrary , put . Finite orthogonality in step 2.1 gives . Hence the coefficient-square partial sums are bounded increasing and converge; their tails give . Completeness in [F5] supplies with . Pairing continuity shows for every , so step 2.3 gives . This proves the promised expansion, not merely orthogonality. All sequences are specified; countable choice is inherited from the complex integral and completeness interfaces.
Depends on
- Schwartz space and its seminorms
- Fourier transform acts continuously on Schwartz space
- Euclidean Gaussian transform with the 2π normalization
- Uniqueness of the L1 Fourier transform
- Dominated convergence
- Plancherel theorem
- Complex completeness, density, and inner product: the consumer interface
- Complex integration by parts on intervals and decaying lines
- The complex exponential by its power series
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Polynomial Gaussians are Schwartz
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
61 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
- Daniel W. Stroock, Topics in Fourier Analysis (2024) (standard reference, not scraped)