Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05
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.

Abel means converge in L^p, uniformly, and at Lebesgue points

Statement

Assume the Axiom of Countable Choice.

Let f:RC be one-periodic with f[0,1]L1([0,1]).

  1. If 1p< and f[0,1]Lp([0,1]), then ArffLp([0,1])0(r1).
  2. If f is continuous, then supxRArf(x)f(x)0(r1).
  3. If x is a Lebesgue point of f, then Arf(x)f(x)(r1).

In particular, Arf(x)f(x) for almost every x.

Facts & Assumptions

Given: The Axiom of Countable Choice and a one-periodic function f with f[0,1]L1([0,1]).

[L1]

The Abel means satisfy Arf=fPr, so Arf(x)=01f(xt)Pr(t)dt for every x and every 0r<1 (Cesaro and Abel means of a Fourier series).

[L2]

The Poisson kernels are nonnegative, have integral 1, and their mass on [δ,1δ] tends to 0 as r1 (The Poisson kernel on the circle is a positive approximate identity).

[L3]

At a Lebesgue point, limh0+12hhhf(xt)f(x)dt=0 (Lebesgue points and the Lebesgue set of an Lloc1 class).

[L4]

Assuming the Axiom of Countable Choice, almost every point is a Lebesgue point (Almost every point is a Lebesgue point of a locally integrable function).

[L5]

Assuming the Axiom of Countable Choice, Cc(R) is dense in Lp(R) for 1p< (Cc(Rn) is dense in Lp(Rn) for 1p<).

Proof

technique · direct
1.1

Let g be one-periodic and in Lp([0,1]) for some 1p<. Using [L1] and the positivity and unit mass in [L2], Jensen's inequality gives Arg(x)p01g(xt)pPr(t)dt. Integrating in x over [0,1] shows ArgLp([0,1])gLp([0,1]), and hence ArgArhLp([0,1])ghLp([0,1]).

L1L2algebra
1.2

Assume now that f is continuous, and let ε>0. Uniform continuity modulo 1 gives δ(0,1/2] such that f(xt)f(x)<ε/2 whenever t[0,δ][1δ,1]. Using [L1] and [L2] exactly as in the Fejer proof yields Arf(x)f(x)ε/2+2fδ1δPr(t)dt. By [L2], the far term is <ε/2 for all r close enough to 1, uniformly in x. Therefore Arff uniformly.

L1L2givenchoosealgebra
1.3

Assume x is a Lebesgue point of f, and let ε>0. By [L3], choose δ(0,1/2] so that hhf(xt)f(x)dt<ε4h(0<hδ). Define G(h):=0h(f(x+t)f(x)+f(xt)f(x))dt, so G(h)<εh/4 for 0<hδ. Pairing [0,1/2] and [1/2,1] in [L1] gives Arf(x)f(x)01/2(f(x+t)f(x)+f(xt)f(x))Pr(t)dt. Set ar:=min(δ,1r). On (0,ar), the closed form in [L2] gives Pr(t)2/(1r), so this interval contributes at most ε/2. If ar<δ and r1/2, then sin(πt)2t on [ar,δ], so [L2] gives Pr(t)1r216rt21r4t2. The same integration-by-parts estimate as in the Fejer proof shows that [ar,δ] contributes at most 3ε/16. Finally, [δ,1/2] contributes o(1) as r1 by [L2]. Hence Arf(x)f(x).

L1L2L3chooseconstructalgebra
2.1

Let 1p< and assume f[0,1]Lp([0,1]). Let ε>0. Repeating the construction from the Fejer Lp theorem with [L5], one obtains a continuous one-periodic function u such that fuLp([0,1])<ε/3. Then step 1.1 and the uniform convergence of step 1.2 give ArffLp([0,1])Ar(fu)Lp([0,1])+AruuLp([0,1])+ufLp([0,1])<ε for all r sufficiently close to 1. Hence Arff in Lp([0,1]).

L5step 1.1step 1.2choosealgebra
3.1

Step 1.3 proves the pointwise conclusion at every Lebesgue point, and [L4] therefore gives the almost-everywhere convergence.

L4step 1.3

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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