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 · 4 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. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Dirichlet Kernel Localisation and Pointwise Fourier Convergence - Examples

1 · Prerequisites

2 · Summary

The companion page records the concrete leaves behind the A-page criteria: the Dirichlet kernel's removable value and sign changes, logarithmic growth of its L1 norm, the explicit sawtooth Fourier series, a localisation calculation with compactly supported data away from the evaluation point, and a continuous logarithmic-modulus counterexample showing that continuity alone does not force the Dini condition.

3 · Logical flowchart

4 · Definitions, theorems and proofs

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Lebesgue constants grow logarithmically

Statement

There are absolute constants c,C>0 such that, for every N≥1,

clog⁡(N+1)≤∫01∣DN(t)∣ dt≤Clog⁡(N+1).

Facts & Assumptions

Given: An integer N≥1.

[L1]

For t∉Z, DN(t)=sin⁡((2N+1)πt)sin⁡(πt), and in particular DN(1−t)=DN(t) for 0<t<1 (Closed form and size bounds for the Dirichlet kernel).

Proof

technique · direct
1.1L1L2algebra

For 0<t<1, [L1] gives DN(1−t)=DN(t), so ∫01∣DN(t)∣ dt=2∫01/2∣DN(t)∣ dt. Split the last integral at 1/(2N+1). On (0,1/(2N+1)], [L1] and the bound ∣DN(t)∣≤2N+1 give a contribution at most 1. On [1/(2N+1),1/2], one has 0<πt≤π/2<2, so [L2] implies sin⁡(πt)≥πt/3. Using [L1], ∣DN(t)∣≤1sin⁡(πt)≤3πt. Therefore ∫01∣DN(t)∣ dt≤2+6π∫1/(2N+1)1/2dtt≤Clog⁡(N+1) for a universal C.

1.2L1algebra

For m=0,…,N−1, let Jm:=[m+1/62N+1,m+5/62N+1]. These intervals lie in (0,1/2) and are disjoint. If t∈Jm, then (2N+1)πt∈[(m+1/6)π,(m+5/6)π], so ∣sin⁡((2N+1)πt)∣≥1/2. Also sin⁡(πt)≤πt. Hence [L1] gives ∣DN(t)∣≥12πt(t∈Jm).

2.1step 1.1step 1.2algebra

Integrating the lower bound from step 1.2 over each Jm and summing yields ∫01/2∣DN(t)∣ dt≥12π∑m=0N−1∫Jmdtt=12π∑m=0N−1log⁡ ⁣(m+5/6m+1/6). Since log⁡ ⁣(m+5/6m+1/6)≥2/3m+5/6≥23(m+1), one gets ∫01/2∣DN(t)∣ dt≥13π∑m=0N−11m+1≥13π∫1N+1dtt=13πlog⁡(N+1). Using step 1.1 once more, ∫01∣DN(t)∣ dt≥23πlog⁡(N+1).

3.1step 1.1step 2.1∎

Steps 1.1 and 2.1 give the two-sided logarithmic bound.

5 · Examples, counterexamples and false statements

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

The Dirichlet kernel at zero and away from zero

Example

For each N≥1,

DN(0)=2N+1,

while

DN ⁣(14N+2)=1sin⁡(π/(4N+2))>0,DN ⁣(34N+2)=−1sin⁡(3π/(4N+2))<0.

So the Dirichlet kernel has a removable peak at 0 and already changes sign at two explicit nearby points.

Facts & Assumptions

Given: An integer N≥1.

[L1]

The Dirichlet kernel is DN(t)=∑∣k∣≤Nek(t) (Dirichlet and Fejer kernels).

[L2]

For t∉Z, DN(t)=sin⁡((2N+1)πt)sin⁡(πt), and DN(0)=2N+1 (Closed form and size bounds for the Dirichlet kernel).

Verification

technique · direct
1.1L1L2algebra

At t=0, [L1] gives DN(0)=∑∣k∣≤Nek(0)=∑∣k∣≤N1=2N+1, which agrees with the removable value recorded in [L2].

2.1L2algebra∎

The numbers (4N+2)−1 and 3(4N+2)−1 are not integers, so [L2] applies. Since (2N+1)π/(4N+2)=π/2 and 3(2N+1)π/(4N+2)=3π/2, the numerator is respectively 1 and −1. The denominators are positive because their angles lie in (0,π). Hence the two displayed signs follow.

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

Fourier partial sums of the sawtooth

Example

Assume the Axiom of Countable Choice.

Let f be the one-periodic sawtooth given by f(0)=0 and f(x)=x−12 for 0<x<1. Then f^(0)=0 and, for k≠0,

f^(k)=−12πik.

Hence

SNf(x)=−∑k=1Nsin⁡(2πkx)πk.

At every noninteger x, SNf(x)→f(x), while at every integer x, SNf(x)→0.

Facts & Assumptions

Given: The Axiom of Countable Choice and the one-periodic sawtooth f(0)=0 and f(x)=x−12 for 0<x<1.

[L1]

Fourier coefficients and partial sums are defined by the one-period formulas in Period-one Fourier coefficients, partial sums, and convolution on the torus.

[L2]

Assuming the Axiom of Countable Choice, a one-periodic bounded-variation function converges at each point to the midpoint of its one-sided limits under Fourier partial sums (Dirichlet-Jordan pointwise convergence).

Verification

technique · direct
1.1L1algebra

Since ∫01(x−12) dx=0, [L1] gives f^(0)=0. For k≠0, direct integration gives f^(k)=∫01(x−12)e−2πikx dx=−12πik.

2.1L1step 1.1algebra

Insert the coefficients from step 1.1 into the partial-sum formula [L1]. Pairing the k and −k terms gives SNf(x)=−∑k=1Nsin⁡(2πkx)πk.

3.1L2step 2.1choosealgebra∎

The sawtooth is piecewise C1, hence of bounded variation on one period. If x∉Z, choose the unique integer m with y:=x−m∈(0,1). Because both f and its Fourier partial sums are one-periodic, one has SNf(x)=SNf(y) and f(x)=f(y)=y−12. The one-sided limits at y therefore both equal f(x), so [L2] gives SNf(x)→f(x). At an integer x, the one-sided limits are −1/2 and 1/2, whose midpoint is 0, so [L2] gives SNf(x)→0.

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

Localisation for functions equal on an arc

Example

Assume the Axiom of Countable Choice.

Let f≡0 and let g=1[1/4,3/4], both extended one-periodically. Then f and g agree on the arc (−1/8,1/8) modulo 1, so

SNg(0)−SNf(0)→0.

Since SNf(0)=0 for every N, this gives

SNg(0)→0.

Facts & Assumptions

Given: The Axiom of Countable Choice and the one-periodic functions f≡0 and g=1[1/4,3/4].

[L1]

Assuming the Axiom of Countable Choice, if two one-period integrable functions agree almost everywhere on a neighborhood of x, then their Fourier partial sums at x differ by a term tending to 0 (Riemann localisation principle for Fourier series).

Verification

technique · direct
1.1L1given

On the interval (−1/8,1/8) modulo 1, the indicator g vanishes, so f=g=0 there. Thus the hypothesis of [L1] holds at x=0.

2.1L1step 1.1algebra∎

Applying [L1] at x=0 gives SNg(0)−SNf(0)→0. But every Fourier coefficient of the zero function is 0, so SNf(0)=0 for all N. Therefore SNg(0)→0.

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-04Open item page →

Continuity alone does not satisfy a Dini modulus

Statement refuted

Assume the Axiom of Countable Choice.

Every continuous one-periodic function automatically satisfies the Dini integrability condition at each point.

Facts & Assumptions

Given: The Axiom of Countable Choice and the Dini criterion on the Fourier page (Dini pointwise convergence criterion for Fourier series).

[L1]

Assuming the Axiom of Countable Choice, if ∫0δ∣f(x+t)+f(x−t)−2s∣t dt<∞, then the Fourier partial sums converge to s at x (Dini pointwise convergence criterion for Fourier series).

Counterexample

technique · direct
1.1givenalgebra

Let d(x,Z):=min⁡m∈Z∣x−m∣ and define the one-periodic function f(x):={0,d(x,Z)=0,1log⁡(e/d(x,Z)),d(x,Z)>0. Because d(x,Z)→0 exactly when x approaches an integer and 1/log⁡(e/r)→0 as r↓0, the function f is continuous on T.

2.1L1step 1.1algebra∎

At x=0 one has f(0)=0 and, for 0<t≤1/4, d(t,Z)=d(−t,Z)=t. Hence f(t)+f(−t)−2f(0)=2log⁡(e/t). Therefore ∫01/4∣f(t)+f(−t)−2f(0)∣t dt=2∫01/4dttlog⁡(e/t)=∞, because the change of variables u=log⁡(e/t) turns the integral into ∫log⁡(4e)∞du/u. So the hypothesis in [L1] fails at x=0: f is continuous but does not satisfy the Dini condition there.

Sources