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

Dini pointwise convergence criterion for Fourier series

Statement

Assume the Axiom of Countable Choice.

Let f be a one-period integrable function, let x,s∈R, and assume there is δ∈(0,1/2) such that

∫0δ∣f(x+t)+f(x−t)−2s∣t dt<∞.

Then

SNf(x)→sas N→∞.

Facts & Assumptions

Given: The Axiom of Countable Choice, a one-period integrable function f, reals x,s, and a real δ with 0<δ<1/2 such that ∫0δ∣f(x+t)+f(x−t)−2s∣t dt<∞.

[L1]

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

[L2]

Assuming the Axiom of Countable Choice, Fourier coefficients of an L1(T) function tend to 0 at infinity (Riemann-Lebesgue lemma for Fourier coefficients).

[L3]

SNf(x)−s=∫01/2(f(x+t)+f(x−t)−2s)DN(t) dt (Symmetric difference formula for Fourier partial sums).

Proof

technique · direct
1.1L3givenalgebra

Put a(t):=f(x+t)+f(x−t)−2s. By [L3], SNf(x)−s=∫0δa(t)DN(t) dt+∫δ1/2a(t)DN(t) dt.

2.1L1L4step 1.1givenalgebra

For 0<t≤δ<1/2, one has 0<πt<π/2<2, so [L4] gives sin⁡(πt)≥πt/3. Define ψ0(t):=1(0,δ](t) a(t)eiπtsin⁡(πt). Then ∣ψ0(t)∣≤3π 1(0,δ](t)∣a(t)∣t, so the hypothesis makes ψ0∈L1(T). Using [L1], ∫0δa(t)DN(t) dt=Im⁡∫01ψ0(t)e2πiNt dt=Im⁡ ψ^0(−N).

2.2L1step 1.1algebra

Define ψ1(t):=1[δ,1/2](t) a(t)eiπtsin⁡(πt). Since sin⁡(πt) is bounded away from 0 on [δ,1/2] and a∈L1([δ,1/2]), one has ψ1∈L1(T). Again [L1] turns the second integral in step 1.1 into ∫δ1/2a(t)DN(t) dt=Im⁡ ψ^1(−N).

3.1L2step 2.1step 2.2algebra∎

By [L2], both ψ^0(−N) and ψ^1(−N) tend to 0. Steps 2.1 and 2.2 therefore make both integrals in step 1.1 tend to 0. Hence SNf(x)−s→0, or equivalently SNf(x)→s.

Depends on

Used by

Dependency tree · two levels

13 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