Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 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.

Dirichlet-Jordan pointwise convergence

Statement

Assume the Axiom of Countable Choice.

Let f:R→R be one-periodic and of bounded variation on one period. Then for every x∈R,

SNf(x)→f(x+)+f(x−)2as N→∞.

Facts & Assumptions

Given: The Axiom of Countable Choice, a one-periodic real function f of bounded variation on one period, and a real x.

[L1]

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

[L2]

Assuming the Axiom of Countable Choice, if u:[0,δ]→R is of bounded variation with u(0)=0 and u(t)→0 as t↓0, then ∫0δu(t)sin⁡((2N+1)πt)sin⁡(πt) dt→0 (Bounded variation gives one-sided Dirichlet integrability).

[L3]

A bounded-variation function has both one-sided limits at every point (A bounded-variation function has at most countably many discontinuities, all of the first kind).

[L4]

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

[L5]

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

Proof

technique · direct
1.1L3givenchoosealgebra

By [L3], the one-sided limits f(x+) and f(x−) exist. Put s:=f(x+)+f(x−)2. Choose δ∈(0,1/2) and define, on [0,δ], u+(0):=0,u−(0):=0, u+(t):=f(x+t)−f(x+)andu−(t):=f(x−t)−f(x−)(0<t≤δ). Because translations and reflections preserve bounded variation on a compact interval, and changing a function at one point preserves bounded variation, both u+ and u− have bounded variation on [0,δ]. The cited one-sided-limit result [L3] gives u±(t)→0 as t↓0, and by construction u±(0)=0.

2.1L1step 1.1algebra

Applying [L1] with the value s from step 1.1 yields SNf(x)−s=∫0δ(u+(t)+u−(t))DN(t) dt+∫δ1/2(f(x+t)+f(x−t)−2s)DN(t) dt.

3.1L2L5step 1.1algebra

By [L2] applied to u+ and to u−, and then using [L5], ∫0δu+(t)DN(t) dt→0,∫0δu−(t)DN(t) dt→0. Hence the first integral in step 2.1 tends to 0.

3.2L4L5step 2.1algebra

Define ψ(t):=1[δ,1/2](t) (f(x+t)+f(x−t)−2s)eiπtsin⁡(πt). Since sin⁡(πt) is bounded away from 0 on [δ,1/2] and the numerator is integrable there, ψ∈L1(T). By [L5], the second integral in step 2.1 equals Im⁡∫01ψ(t)e2πiNt dt=Im⁡ ψ^(−N), so it tends to 0 by [L4].

4.1step 1.1step 2.1step 3.1step 3.2algebra∎

Steps 3.1 and 3.2 make both integrals in step 2.1 tend to 0. Therefore SNf(x)−s→0, which is exactly SNf(x)→f(x+)+f(x−)2.

Depends on

Used by

Dependency tree · two levels

18 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