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.
Agreement of the integral and L2 transforms
Statement
Assume countable choice. If , its bounded continuous integral transform represents almost everywhere.
Facts & Assumptions
Given: The Axiom of Countable Choice ().
Plancherel is a continuous extension of the Schwartz transform (Plancherel theorem).
The integral transform has supremum bound (The L1 transform is bounded and uniformly continuous).
One smooth compactly supported sequence approximates in both norms (Simultaneous L1 and L2 smooth approximation).
Complex norm convergence has an almost-everywhere convergent subsequence of representatives with the correct limit class (Complex completeness, density, and inner product: the consumer interface).
Proof
Choose the sequence of [F3]. Its terms are Schwartz, since every weighted derivative has compact support and is bounded. Thus [F1] identifies with the class of . Also by [F2], whereas in norm by [F1].
By [F4], a subsequence of the transform classes has measurable representatives tending a.e. to a representative of . Those representatives and the continuous functions agree off a countable union of measurable null sets, so the corresponding subsequence of also tends to a.e. Step 1.1 gives its pointwise limit at every point by uniform convergence. Uniqueness of complex limits gives a.e. Countable choice is inherited from [F3], [F4] and Plancherel; no pointwise convergence of an arbitrary norm-convergent sequence is assumed.