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 is independent of the chosen Borel representatives
Statement
Assume the Axiom of Countable Choice. Let . If are Borel representatives of and are Borel representatives of , then for almost every ,
Facts & Assumptions
Given: The Axiom of Countable Choice and two Borel representatives for each of the classes and .
The integrands from Borel representatives are measurable (Borel representatives make the convolution integrand Borel measurable).
The Lebesgue integral respects almost-everywhere equality (Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree).
Lebesgue measurability and null sets are translation invariant (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation).
Under Countable Choice, reflection preserves Lebesgue null sets (For a nonzero real , dilation by multiplies Lebesgue outer measure by , and reflection in the origin preserves it, The Axiom of Countable Choice ()).
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
Let and . These are Borel null sets. For every fixed , the set where the first factors differ is , null by reflection [L4] followed by translation [L3]. The second factors differ only on , so the two section integrands agree for almost every , outside .
By [L1], both section integrands are measurable, and step 1.1 says they agree almost everywhere in . Thus [L2] gives equality of their integrals at every where either section product is absolutely integrable.
For either choice of representatives, the nonnegative function is product-measurable by [L1]. Tonelli [L5] and translation invariance [L3] give The second equality uses [L5] for the measure-preserving translation , and the representatives have the same norms as their classes. Hence each section product is absolutely integrable for almost every ; intersect the two full-measure sets. Step 2.1 gives equality there, proving the statement.
Depends on
- Borel representatives make the convolution integrand Borel measurable
- Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree
- Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation
- For a nonzero real $c$, dilation by $c$ multiplies Lebesgue outer measure by $|c|^n$, and reflection in the origin preserves it
- Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
- Integral invariance under measure-preserving maps
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
- FALSE: the Borel-representative discipline in convolution is unnecessary because continuous precomposition always preserves Lebesgue measurability False statement
- Fourier transform turns L1 convolution into multiplication Theorem
- If f,g ∈ L¹(ℝⁿ), then f*g exists almost everywhere, belongs to L¹, and ‖f*g‖₁ ≤ ‖f‖₁ ‖g‖₁ Theorem
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
- Walter Rudin, Real and Complex Analysis, 3rd ed. (standard reference, not scraped)