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.
Depends on
Used by
- Newtonian potential of compactly supported data Definition
- FALSE: the Borel-representative discipline in convolution is unnecessary because continuous precomposition always preserves Lebesgue measurability False statement
- Complex translation, convolution, approximate identities, and mollification Lemma
- Convolution on L¹(ℝⁿ) is independent of the chosen Borel representatives Lemma
- Differentiation of L-one functions for a doubling weight Lemma
- 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
- Newtonian potentials solve the distributional Poisson equation Theorem
- Young's convolution inequality under Countable Choice Theorem
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
- Walter Rudin, Real and Complex Analysis, 3rd ed. (standard reference, not scraped)