Alphabeta Math
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.

5 results · all verified · 5 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 5 also cleared it.

Fejer and Poisson Summability of Fourier Series - Examples

1 · Prerequisites

2 · Summary

The companion page records the clean coefficient computations behind the two positive kernels, a standard square-wave summation example, and two boundary counterexamples: uniform convergence fails without continuity of the target representative, and Abel summability does not reverse to ordinary convergence.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

Fejer means of a single character

Example

Let kZ. For every N0,

σNek=(1kN+1)+ek.

Facts & Assumptions

Given: An integer k and an integer N0.

[L1]

The Cesaro means are defined by σNf=1N+1j=0NSjf (Cesaro and Abel means of a Fourier series).

Verification

technique · direct
1.1

The Fourier coefficients of ek vanish except at k, where the coefficient is 1. Hence Sjek={0,j<k,ek,jk.

L1algebra
2.1

If k>N, then every term in the Cesaro average from [L1] is 0, so σNek=0. If kN, then exactly N+1k of the terms equal ek, and therefore σNek=N+1kN+1ek=(1kN+1)ek. This is the same as the displayed ()+ formula, and for N=0 it gives σ0e0=e0 and σ0ek=0 for k0.

L1step 1.1algebra
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

Poisson integral of a single character

Example

Let kZ and 0r<1. Then

Arek=rkek.

Facts & Assumptions

Given: An integer k and a parameter r with 0r<1.

[L1]

The Abel means are defined by Arf(x)=mZrmf^(m)em(x) (Cesaro and Abel means of a Fourier series).

Verification

technique · direct
1.1

The Fourier coefficients of ek vanish except at k, where the coefficient is 1. Substituting into [L1] leaves only one term: Arek(x)=rkek(x).

L1algebra
2.1

Since step 1.1 holds for every x, it is exactly the asserted identity Arek=rkek.

step 1.1
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

Fejer summation of the square wave

Example

Let q be the one-periodic square wave defined by

q(x)={1,0<x<1/2,1,1/2<x<0,

with q(0)=q(1/2)=0. Then

σNq(x)=4πm=0(N1)/2(12m+1N+1)sin(2π(2m+1)x)2m+1,

and

σNq(0)0.

Moreover σNq(x)1 for every x and every N, so these positive means recover the midpoint value without a fixed Gibbs overshoot.

Facts & Assumptions

Given: The one-periodic square wave q above.

[L1]

The Cesaro means are defined by averaging Fourier partial sums (Cesaro and Abel means of a Fourier series).

[L2]

If both one-sided limits exist at a point, the Fejer means converge there to their midpoint (Fejer means converge to midpoint values at jumps).

[L3]

The Fejer kernels are nonnegative and have integral 1 (The Fejer kernel is a positive approximate identity).

Verification

technique · direct
1.1

Direct integration gives q^(2m)=0 for every m and q^(2m+1)=2πi(2m+1),q^((2m+1))=2πi(2m+1). Hence Sjq(x)=4π0m, 2m+1jsin(2π(2m+1)x)2m+1.

L1algebra
2.1

Averaging the partial sums from step 1.1 as in [L1] shows that the odd mode 2m+1 appears with weight 1(2m+1)/(N+1) when 2m+1N and with weight 0 otherwise. This is exactly the displayed formula for σNq.

L1step 1.1algebra
3.1

The one-sided limits at 0 are 1 and 1, so [L2] gives σNq(0)1+12=0. Also [L1] and [L3] give σNq(x)=01q(xt)FN(t)dt, and because q1, positivity and total mass one imply σNq(x)1 for every x. Thus the Fejer means average across the jump and do not exhibit a fixed overshoot.

L1L2L3step 2.1algebra
CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

Fejer means need not converge uniformly for discontinuous data

Statement refuted

For every one-periodic integrable function f, the Fejer means σNf converge uniformly to f.

Facts & Assumptions

Given: The one-periodic step function f(x):={1,0<x<1/2,0,1/2<x<0, with f(0)=f(1/2)=0.

[L1]

The Fejer means are averages of the Fourier partial sums (Cesaro and Abel means of a Fourier series).

Counterexample

technique · direct
1.1

For each N, the function Sjf is a trigonometric polynomial for every 0jN, so [L1] makes σNf a trigonometric polynomial as well. In particular, every σNf is continuous.

L1algebra
2.1

If σNf converged uniformly to f, then the uniform limit of the continuous functions σNf would be continuous. But the chosen f has a jump at 0, so it is discontinuous. Therefore uniform convergence to f is impossible. This single step function refutes the universal statement.

step 1.1algebra
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

Abel summability does not imply ordinary convergence

Statement refuted

If a series is Abel summable, then its ordinary partial sums converge.

Facts & Assumptions

Given: Grandi's series 11+11+.

[F1]

For r<1, the geometric-series identity gives 1r+r2r3+=11+r.

Counterexample

technique · direct
1.1

The ordinary partial sums are 1,0,1,0,, so they do not converge.

givenalgebra
2.1

For 0r<1, [F1] makes the associated Abel sum 1r+r2r3+=11+r. As r1, this tends to 1/2. Thus the series is Abel summable but not ordinarily convergent, refuting the statement.

F1step 1.1algebra

Sources