Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedverified 2026-09-23 (gpt-6-sol)
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

Assume the Axiom of Countable Choice. Let f:R→C be one-periodic with f∣[0,1]∈L1([0,1]), and let x,s∈R. If

σNf(x)⟶s(N→∞),

then

Arf(x)⟶s(r↑1).

Facts & Assumptions

Given: Countable Choice, a one-periodic integrable function f, a point x∈R, 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.1L1algebra

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

2.1step 1.1algebra

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

3.1step 2.1givenchoosealgebra∎

Let ε>0. Choose N0 so large that ∣σN−s∣<ε/2 for all N≥N0, and put M:=max⁡0≤N<N0∣σN−s∣. By step 2.1, ∣Arf(x)−s∣≤M∑N=0N0−1wN(r)+ε2∑N=N0∞wN(r). The tail sum is at most ε/2, and for each fixed N one has wN(r)→0 as r↑1, 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.

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