Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedverified 2026-09-26 (gpt-6-sol)
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 f~,g~:Rn→C be Borel measurable functions. Then

H(x,y):=f~(x−y)g~(y)

is Borel measurable on R2n. In particular, for each fixed x∈Rn, the section y↦H(x,y) is measurable.

Facts & Assumptions

Given: Borel measurable functions f~,g~ on Rn.

[A1]

The functions f~ and g~ are Borel measurable by hypothesis.

[L2]

For positive Euclidean dimensions, the Borel product is the Euclidean Borel sigma-algebra; in particular this applies to Rn×Rn and C×C≅R4 (The Borel product of R^m and R^n is the Borel sigma-algebra of R^{m+n}).

[L3]

Composition of Borel measurable maps preserves measurability (Composition with a Borel measurable outer map preserves measurability).

Proof

technique · direct
1.1A1L3givenconstruct

If n=0, every space and function in the statement has a one-point domain, so the conclusion is immediate. For n≥1, the map T:R2n→R2n, T(x,y)=(x−y,y), is continuous and hence Borel measurable. The coordinate projections are continuous, so [L3] makes h1(x,y)=f~(x−y) and h2(x,y)=g~(y) Borel measurable maps to C.

2.1L2L3step 1.1∎

The pair (h1,h2):R2n→C2 is Borel measurable: the preimage of every open rectangle U×V is h1−1(U)∩h2−1(V), and such rectangles generate the product Borel sigma-algebra by [L2]. Complex multiplication C2→C is continuous, so [L3] makes H=h1h2 Borel measurable. For fixed x, the map y↦(x,y) is continuous, and its composite with H is the stated measurable section.

Depends on

Used by

Dependency tree · two levels

9 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