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.
Borel representatives make the convolution integrand Borel measurable
Statement
Let be Borel measurable functions. Then
is Borel measurable on . In particular, for each fixed , the section is measurable.
Facts & Assumptions
Given: Borel measurable functions on .
The functions and are Borel measurable by hypothesis.
For positive Euclidean dimensions, the Borel product is the Euclidean Borel sigma-algebra; in particular this applies to and (The Borel product of R^m and R^n is the Borel sigma-algebra of R^{m+n}).
Composition of Borel measurable maps preserves measurability (Composition with a Borel measurable outer map preserves measurability).
Proof
If , every space and function in the statement has a one-point domain, so the conclusion is immediate. For , the map , , is continuous and hence Borel measurable. The coordinate projections are continuous, so [L3] makes and Borel measurable maps to .
The pair is Borel measurable: the preimage of every open rectangle is , and such rectangles generate the product Borel sigma-algebra by [L2]. Complex multiplication is continuous, so [L3] makes Borel measurable. For fixed , the map is continuous, and its composite with is the stated measurable section.