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:RR be one-periodic and of bounded variation on one period. Then for every xR,

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(xt)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 t0, then 0δu(t)sin((2N+1)πt)sin(πt)dt0 (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 tZ, DN(t)=sin((2N+1)πt)/sin(πt) (Closed form and size bounds for the Dirichlet kernel).

Proof

technique · direct
1.1

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(xt)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 t0, and by construction u±(0)=0.

L3givenchoosealgebra
2.1

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(xt)2s)DN(t)dt.

L1step 1.1algebra
3.1

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

L2L5step 1.1algebra
3.2

Define ψ(t):=1[δ,1/2](t)(f(x+t)+f(xt)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 Im01ψ(t)e2πiNtdt=Imψ^(N), so it tends to 0 by [L4].

L4L5step 2.1algebra
4.1

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

step 1.1step 2.1step 3.1step 3.2algebra

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