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.
Lebesgue-point convergence for radial-majorized kernels
Statement
Assume countable choice. Let and let be measurable, with and , where is bounded, nonincreasing, and . For and a point with specified Lebesgue value , meaning , one has The integral is absolutely convergent for every . The value is the Lebesgue-point value, not an arbitrary changed value of the representative; this is the componentwise version of Lebesgue points and the Lebesgue set of an class.
Facts & Assumptions
Given: The stated data and The Axiom of Countable Choice ().
Open subsets of Euclidean space are Lebesgue measurable under countable choice (Assuming countable choice, every Borel subset of is Lebesgue measurable).
Measurable balls have positive finite measure by the cube bounds in Euclidean balls have positive finite Lebesgue measure.
Linear dilation scales the measure of a measurable set by its absolute determinant (A linear map of sends Lebesgue measurable sets to Lebesgue measurable sets, with when is invertible and Lebesgue null when it is not).
Tonelli gives countable nonnegative summation under the integral (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).
Complex Lebesgue substitution holds for C1 diffeomorphisms, including translations, reflections and positive dilations (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions).
Proof
Balls are open by the triangle inequality, so F1 establishes measurability before the cube bounds F2 are used. Put . F3 gives and . On that annulus ; hence as , where is the integral over . Integrability implies these tails tend to zero, by countable additivity on explicit integer annuli. Also disjoint annuli , , give .
Write . Boundedness of makes the integral with absolutely convergent: it is at most by reflection and translation of Lebesgue measure. Scaling the defining integral of K gives . Fact F5 applies to these affine diffeomorphisms and supplies both substitutions. Thus the absolute error is at most .
Given , fix such that for . For , the central ball contributes at most . Each dyadic shell whose lower radius is below contributes at most . Their sum is bounded by , where , independently of . These regions cover .
On , the contribution from is at most by step 1.1. The contribution from is at most by integrability and scaling. The total error therefore has limit superior at most . Letting proves convergence. The proof uses the stated countable-choice Euclidean measure interfaces and explicit shells, with no full AC or choice of witnesses at different points.
Depends on
Lebesgue points and the Lebesgue set of an class
An approximate identity on
Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
Euclidean balls have positive finite Lebesgue measure
A linear map of sends Lebesgue measurable sets to Lebesgue measurable sets, with when is invertible and Lebesgue null when it is not
Assuming countable choice, every Borel subset of is Lebesgue measurable
The Axiom of Countable Choice ()
A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions