Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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 n≥1 and let K:Rn→C be measurable, with ∫K=1 and ∣K(y)∣≤Φ(∣y∣), where Φ:[0,∞)→[0,∞) is bounded, nonincreasing, and J:=∫Φ(∣y∣) dy<∞. For f∈L1(Rn;C) and a point x with specified Lebesgue value a∈C, meaning A(r):=∫∣y∣<r∣f(x−y)−a∣ dy=o(rn), one has ∫ε−nK(y/ε)f(x−y) dy⟶a(ε↓0). The integral is absolutely convergent for every ε>0. The value a 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 Lloc1 class.

Facts & Assumptions

[F1]

Open subsets of Euclidean space are Lebesgue measurable under countable choice (Assuming countable choice, every Borel subset of Rn is Lebesgue measurable).

[F2]

Measurable balls have positive finite measure by the cube bounds in Euclidean balls have positive finite Lebesgue measure.

[F4]

Tonelli gives countable nonnegative summation under the integral (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F5]

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

1.1F1F2F3F4given

Balls are open by the triangle inequality, so F1 establishes measurability before the cube bounds F2 are used. Put vn=∣B(0,1)∣∈(0,∞). F3 gives ∣B(0,r)∣=vnrn and ∣B(0,r)∖B(0,r/2)∣=vn(1−2−n)rn. On that annulus Φ(∣y∣)≥Φ(r); hence rnΦ(r)≤Jr/[vn(1−2−n)]→0 as r→∞, where Jr is the integral over ∣y∣≥r/2. Integrability implies these tails tend to zero, by countable additivity on explicit integer annuli. Also disjoint annuli 2j−1≤∣y∣<2j, j≥0, give ∑j≥02jnΦ(2j)≤J/[vn(1−2−n)].

1.2F5given

Write H(y)=∣f(x−y)−a∣. Boundedness of Φ makes the integral with f absolutely convergent: it is at most ε−nΦ(0)∥f∥1 by reflection and translation of Lebesgue measure. Scaling the defining integral of K gives ∫ε−nK(y/ε) dy=1. Fact F5 applies to these affine diffeomorphisms and supplies both substitutions. Thus the absolute error is at most ∫ε−nΦ(∣y∣/ε)H(y) dy.

2.1F4step 1.1step 1.2given

Given η>0, fix δ>0 such that A(r)≤ηrn for 0<r<δ. For ε<δ/2, the central ball contributes at most Φ(0)ε−nA(ε)≤ηΦ(0). Each dyadic shell 2jε≤∣y∣<2j+1ε whose lower radius is below δ/2 contributes at most ε−nΦ(2j)A(2j+1ε)≤η2n2jnΦ(2j). Their sum is bounded by ηC, where C=Φ(0)+2nJ/[vn(1−2−n)], independently of ε. These regions cover ∣y∣<δ/2.

3.1F5step 1.1step 1.2step 2.1∎

On ∣y∣≥δ/2, the contribution from ∣f(x−y)∣ is at most ε−nΦ(δ/(2ε))∥f∥1→0 by step 1.1. The contribution from ∣a∣ is at most ∣a∣∫∣z∣≥δ/(2ε)Φ(∣z∣) dz→0 by integrability and scaling. The total error therefore has limit superior at most ηC. Letting η↓0 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

Dependency tree · 2 levels

Sources