Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04
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.

Closed form and size bounds for the Dirichlet kernel

Statement

For every integer N0,

DN(t)=1+2k=1Ncos(2πkt).

If tZ, then

DN(t)=sin((2N+1)πt)sin(πt).

If mZ, then DN(m)=2N+1. In particular DN is even and

DN(t)2N+1(tR),

while for tZ,

DN(t)1sin(πt).

Facts & Assumptions

Given: An integer N0 and a real t.

[L1]

The Dirichlet kernel is DN(t)=kNe2πikt (Dirichlet and Fejer kernels).

Proof

technique · direct
1.1

Pair the terms with indices k and k in [L1]. This gives DN(t)=1+k=1N(e2πikt+e2πikt)=1+2k=1Ncos(2πkt). Hence DN is even. If t=mZ, then every exponential equals 1, so DN(m)=2N+1.

L1algebra
1.2

Assume tZ and put z=e2πit1. Then [L1, algebra] DN(t)=zNj=02Nzj=zN1z2N+11z. Rewriting numerator and denominator with half-angle factors yields DN(t)=eπi(2N+1)teπi(2N+1)teπiteπit=sin((2N+1)πt)sin(πt).

L1algebra
2.1

The triangle inequality applied to [L1] gives DN(t)2N+1 for every t. If tZ, step 1.2 and sin((2N+1)πt)1 give DN(t)1sin(πt).

L1step 1.2algebra

Depends on

Used by

Dependency tree · two levels

2 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