Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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.

L2 Fourier inversion

Statement

Assume countable choice. On complex L2, F22f=Rf, Rf(x)=f(−x), and F2−1=RF2. For f∈L2, the truncated integrals ∫∣x∣≤Rf(x)e−2πix⋅ξ dx converge in L2 to F2f as R→∞. The corresponding positive-sign integrals converge in L2 to F2−1f. No pointwise convergence is asserted.

Facts & Assumptions

[F1]

Plancherel is unitary and obtained by Schwartz approximation (Plancherel theorem).

[F3]

Integral and norm transforms agree on the intersection (Agreement of the integral and L2 transforms).

[F6]

Dominated convergence holds (Dominated convergence).

[F7]

The complex integral substitution formula applies to a C1 diffeomorphism (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions).

Proof

technique · direct
1.1F1F2F7given

Apply substitution to ∣f∣2 with the C1 diffeomorphism x↦−x, whose absolute Jacobian is one. It gives ∥Rf∥2=∥f∥2 and preserves null equivalence, so R is an isometry on classes with R2=I. For Schwartz approximants uj→f supplied in [F1], [F2] gives F22uj=Ruj. Both sides converge in norm by [F1] and the reflection isometry, hence F22f=Rf. Associativity then gives F2R=RF2 and both inverse identities for RF2.

2.1step 1.1F1F3F4F5F6∎

The closed ball BR={∣x∣≤R} is measurable and finite-measure by [F4]. Thus for fR=1BRf, [F5] gives ∥fR∥1≤λ(BR)1/2∥f∥2, and fR∈L2 as well. [F6] applied to the explicit integer tails of ∣f∣2 gives ∥fR−f∥2→0 for all real R→∞ by monotonicity between integers. By [F3], its integral transform is F2fR, and [F1] gives error norm ∥F2fR−F2f∥2=∥fR−f∥2→0. The positive-sign integral is the reflection of this integral transform; step 1.1 gives its limit RF2f=F2−1f.

Depends on

Used by

Dependency tree · two levels

63 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