Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

Normalized Hermite Fourier eigenfunctions

Statement

Assume countable choice. On R set h0(x)=21/4eπx2,a=πx12πddx,hm=(m!)1/2(a)mh0. Then (hm)m0 is an orthonormal basis of complex L2(R), each hm is Schwartz, and h^m=(i)mhm. Basis means every fL2 has the norm-convergent expansion f=m0f,hmhm, with the pairing linear in its first variable.

Facts & Assumptions

Given: The Axiom of Countable Choice (ACω), the Schwartz definition Schwartz space and its seminorms, and the everywhere-convergent exponential series The complex exponential by its power series.

[F1]

Polynomial Gaussians are Schwartz (Polynomial Gaussians are Schwartz).

[F2]

The Gaussian transform and integral have the stated 2π normalization (Euclidean Gaussian transform with the 2π normalization).

[F3]

Fourier interchanges differentiation and polynomial multiplication with their 2π factors (Fourier transform acts continuously on Schwartz space).

[F4]

Complex integration by parts holds on decaying lines (Complex integration by parts on intervals and decaying lines).

[F5]

Complex L2 is complete, with Cauchy–Schwarz and the first-variable-linear pairing (Complex completeness, density, and inner product: the consumer interface).

[F6]

An integrable function with zero transform vanishes a.e. (Uniqueness of the L1 Fourier transform).

[F7]

Dominated convergence passes limits through integrals (Dominated convergence).

[F8]

Plancherel identifies the resulting eigenfunction identities also in L2 (Plancherel theorem).

Verification

1.1

Put a=πx+(2π)1d/dx and um=(a)mh0. Differentiation gives ah0=0 and aaaa=I, since (d/dx)(xf)xf=f. Induction gives aum=mum1 for m1, and aaum=mum for m0. If um=Qmh0, then Qm+1=2πxQm(2π)1Qm. Thus Qm is real of degree m with leading coefficient (2π)m, and [F1] makes every um Schwartz.

F1givenalgebra
2.1

For polynomial Gaussians v,w, [F4] gives av,w=v,aw: derivative products are polynomial Gaussians and integrable, and their endpoint products vanish. Consequently N=aa is symmetric on these functions, since Nv,w=av,aw=v,Nw. Step 1.1 implies (ml)um,ul=0. Also um22=aum1,um=mum122. The base norm is h022=2e2πx2dx=1 by [F2]. Hence um22=m! and the normalized functions are orthonormal, including m=0.

step 1.1F2F4F5
2.2

The derivative identities [F3] give F(av)=(i/(2π))(v^)iπξv^=iav^. Since [F2] gives h^0=h0, induction yields u^m=(i)mum and the asserted normalized identity. All operations are on Schwartz functions, so this also holds for their Plancherel classes.

step 1.1F2F3F8
2.3

Suppose fL2 is orthogonal to all hm. By the nonzero real leading coefficients in step 1.1, triangular induction expresses each monomial xr as a real linear combination of Q0,,Qr. Therefore f(x)h0(x)xrdx=0 for every r; these integrals exist by [F5], since xrh0L2. Put v=fh0L1 by [F5]. For fixed real ξ, the exponential Taylor partial sums are bounded by e2πξx. The majorant fh0e2πξx is integrable by [F5]: its second factor has finite square integral, because 2πx2+4πξxπx2+4πξ2. Thus [F7] integrates the exponential series termwise, all terms being the zero moments. It gives v^(ξ)=0 for every ξ. By [F6], v=0 a.e.; positivity of h0 gives f=0 a.e.

step 1.1F5F6F7given
3.1

For arbitrary fL2, put sN=m=0Nf,hmhm. Finite orthogonality in step 2.1 gives fsN22=f22m=0Nf,hm20. Hence the coefficient-square partial sums are bounded increasing and converge; their tails give sMsN220. Completeness in [F5] supplies sL2 with sNs. Pairing continuity shows fs,hm=0 for every m, so step 2.3 gives f=s. This proves the promised expansion, not merely orthogonality. All sequences are specified; countable choice is inherited from the complex integral and completeness interfaces.

step 2.1step 2.3F5

Depends on

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