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.

Cesaro summability implies Abel summability

Statement

Let f:RC be one-periodic with f[0,1]L1([0,1]), and let x,sR. If

σNf(x)s(N),

then

Arf(x)s(r1).

Facts & Assumptions

Given: A one-periodic integrable function f, a point xR, and a scalar s such that σNf(x)s.

[L1]

The Cesaro means and Abel means are defined in Cesaro and Abel means of a Fourier series.

Proof

technique · direct
1.1

Let SN:=SNf(x) and σN:=σNf(x). Since SN=(N+1)σNNσN1(N0, σ1:=0), one has N=0rNSN=(1r)N=0(N+1)rNσN for 0r<1. On the other hand, the definition of Arf(x) in [L1] gives Arf(x)=(1r)N=0rNSN=(1r)2N=0(N+1)rNσN.

L1algebra
2.1

Put wN(r):=(1r)2(N+1)rN(N0). These weights are nonnegative, and N=0wN(r)=(1r)2N=0(N+1)rN=1. Therefore step 1.1 rewrites the Abel mean as Arf(x)s=N=0wN(r)(σNs).

step 1.1algebra
3.1

Let ε>0. Choose N0 so large that σNs<ε/2 for all NN0, and put M:=max0N<N0σNs. By step 2.1, Arf(x)sMN=0N01wN(r)+ε2N=N0wN(r). The tail sum is at most ε/2, and for each fixed N one has wN(r)0 as r1, so the finite initial sum is <ε/(2M) for r close enough to 1 when M>0, and is already 0 when M=0. Hence Arf(x)s<ε for all r sufficiently close to 1. Therefore Arf(x)s.

step 2.1givenchoosealgebra

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 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