Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-23 (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.

Convolution on L1(Rn) is independent of the chosen Borel representatives

Statement

Assume the Axiom of Countable Choice. Let f,g∈L1(Rn). If f~1,f~2 are Borel representatives of f and g~1,g~2 are Borel representatives of g, then for almost every x∈Rn,

∫f~1(x−y)g~1(y) dy=∫f~2(x−y)g~2(y) dy.

Facts & Assumptions

Given: The Axiom of Countable Choice and two Borel representatives for each of the L1 classes f and g.

[L1]

The integrands from Borel representatives are measurable (Borel representatives make the convolution integrand Borel measurable).

[L3]

Lebesgue measurability and null sets are translation invariant (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation).

[L5]

Tonelli applies to nonnegative product-measurable functions, and integrals are unchanged by measure-preserving maps (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Integral invariance under measure-preserving maps).

Proof

technique · direct
1.1L3L4givenalgebra

Let Nf:={f~1≠f~2} and Ng:={g~1≠g~2}. These are Borel null sets. For every fixed x, the set where the first factors differ is x−Nf, null by reflection [L4] followed by translation [L3]. The second factors differ only on Ng, so the two section integrands agree for almost every y, outside (x−Nf)∪Ng.

2.1L1L2step 1.1

By [L1], both section integrands are measurable, and step 1.1 says they agree almost everywhere in y. Thus [L2] gives equality of their integrals at every x where either section product is absolutely integrable.

3.1L1L3L5step 2.1∎

For either choice of representatives, the nonnegative function H(x,y):=∣f~i(x−y)g~i(y)∣ is product-measurable by [L1]. Tonelli [L5] and translation invariance [L3] give ∫Rn ⁣∫RnH(x,y) dy dx=∫Rn∣g~i(y)∣(∫Rn∣f~i(x−y)∣ dx)dy=∥f∥1∥g∥1<∞. The second equality uses [L5] for the measure-preserving translation x↦x−y, and the representatives have the same L1 norms as their classes. Hence each section product is absolutely integrable for almost every x; intersect the two full-measure sets. Step 2.1 gives equality there, proving the statement.

Depends on

Used by

Dependency tree · two levels

48 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