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 N≥0,

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

If t∉Z, then

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

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

∣DN(t)∣≤2N+1(t∈R),

while for t∉Z,

∣DN(t)∣≤1∣sin⁡(πt)∣.

Facts & Assumptions

Given: An integer N≥0 and a real t.

[L1]

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

Proof

technique · direct
1.1L1algebra

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

1.2L1algebra

Assume t∉Z and put z=e2πit≠1. Then [L1, algebra] DN(t)=z−N∑j=02Nzj=z−N1−z2N+11−z. Rewriting numerator and denominator with half-angle factors yields DN(t)=e−πi(2N+1)t−eπi(2N+1)te−πit−eπit=sin⁡((2N+1)πt)sin⁡(πt).

2.1L1step 1.2algebra∎

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

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