Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

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

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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