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.
If , then exists almost everywhere, belongs to , and
Statement
If , then exists for almost every , belongs to , and satisfies
Facts & Assumptions
Given: Functions .
The Borel-representative integrand is measurable and representative independent (Borel representatives make the convolution integrand Borel measurable, Convolution on is independent of the chosen Borel representatives).
Tonelli and Fubini apply on sigma-finite product spaces (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Fubini's theorem for L^1 functions on a sigma-finite product).
The integral triangle inequality is available (The modulus of an integral is bounded by the integral of the modulus).
Proof
Choose Borel representatives of and define [L1, L2, given, choose, algebra] By [L1], is measurable on . For each , by translation invariance of Lebesgue measure.
Integrating the identity from step 1.1 in and applying [L2] gives [L2, step 1.1, algebra] Hence for almost every , the section is absolutely integrable, so is defined there.
For those , [L1, L2, L3, step 2.1, algebra] by [L3]. Another application of [L2] then yields By [L1], the resulting class is independent of the chosen Borel representatives.
Depends on
- Borel representatives make the convolution integrand Borel measurable
- Convolution on $L^1(\mathbb{R}^n)$ is independent of the chosen Borel representatives
- Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
- Fubini's theorem for L^1 functions on a sigma-finite product
- The modulus of an integral is bounded by the integral of the modulus
Used by
- If 1 < p < ∞ and q is conjugate to p, then f*g is continuous and vanishes at infinity Corollary
- 1_[0,1] * 1_[0,1] is the tent function Example
- FALSE: if f,g ∈ L¹(ℝⁿ), then f*g(x) is defined for every x False statement
- Convolution on L¹(ℝⁿ) is bilinear, commutative, and associative Proposition
- The support of a convolution lies in the closure of the support sumset Theorem
- Young's convolution inequality Theorem
Dependency tree · two levels
22 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)