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

Bounded variation gives one-sided Dirichlet integrability

Statement

Assume the Axiom of Countable Choice.

Let 0<δ<1/2, and let u:[0,δ]R have bounded variation. Assume that u(0)=0 and limt0u(t)=0. Then

0δu(t)sin((2N+1)πt)sin(πt)dt0as N.

Facts & Assumptions

Given: The Axiom of Countable Choice, a real δ with 0<δ<1/2 and a bounded-variation function u:[0,δ]R such that u(0)=0 and limt0u(t)=0.

[L1]

Jordan decomposition writes u=u(0)+PuNu with Pu,Nu nondecreasing, normalized by Pu(0)=Nu(0)=0, and minimal among such decompositions (Jordan decomposition for functions of bounded variation).

[L2]

The variation identity is Var[0,η](u)=Pu(η)+Nu(η) for every η[0,δ] (The positive and negative variations are nondecreasing and give the Jordan identities).

[L3]

The Dirichlet kernel satisfies DN(t)=sin((2N+1)πt)/sin(πt) for tZ (Closed form and size bounds for the Dirichlet kernel).

[L6]

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

Proof

technique · direct
1.1

By [L1], write u=PuNu with Pu(0)=Nu(0)=0 and Pu,Nu nondecreasing. Let p:=inf0<tδPu(t)=limt0Pu(t),q:=inf0<tδNu(t)=limt0Nu(t). Since u(t)0, one has pq=0. If p=q>0, define P~(0)=N~(0)=0 and P~(t)=Pu(t)p, N~(t)=Nu(t)p for t>0. Then P~,N~ are again nondecreasing, nonnegative, normalized, and satisfy u=P~N~, but P~(t)<Pu(t) for every t>0, contradicting the minimality in [L1]. Hence p=q=0, so Pu(t)0,Nu(t)0,Var[0,t](u)=Pu(t)+Nu(t)0 as t0 by [L2].

L1L2givencontradiction
1.2

For 0tδ, define HN(t):=0tDN(s)ds. Using [L3] and the change of variables y=(2N+1)πs, HN(t)=0(2N+1)πtsinygN(y)dy, where gN(y):=1(2N+1)πsin(y/(2N+1)). If (2N+1)πt1, then 0<y/(2N+1)1<2, so [L5] and sinyy give sinygN(y)3/π on [0,(2N+1)πt], hence HN(t)3/π. If (2N+1)πt>1, the same estimate controls the part on [0,1], while on [1,(2N+1)πt] the function gN is positive and decreasing because 0<y/(2N+1)π/2. Bonnet's theorem [L4] therefore gives a point ξ with 1(2N+1)πtsinygN(y)dy=gN(1)1ξsinydy+gN((2N+1)πt)ξ(2N+1)πtsinydy. The absolute value is at most 2gN(1)+2gN((2N+1)πt)4gN(1)12π by monotonicity of gN and [L5]. Thus HN(t)15π(0tδ, N0).

L3L4L5algebra
2.1

Fix ε>0. By step 1.1, choose η(0,δ) such that Var[0,η](u)<πε60. Applying [L4] to the monotone functions Pu and Nu on [0,η], and using Pu(0)=Nu(0)=0, step 1.2 yields 0ηPu(t)DN(t)dt30πPu(η),0ηNu(t)DN(t)dt30πNu(η). Therefore 0ηu(t)DN(t)dt30π(Pu(η)+Nu(η))=30πVar[0,η](u)<ε2.

L2L4step 1.1step 1.2givenchoosealgebra
3.1

On [η,δ], define ψ(t):=1[η,δ](t)u(t)eiπtsin(πt). Because sin(πt) is bounded away from 0 on [η,δ] and u is bounded on the compact interval [η,δ], one has ψL1(T). By [L3], ηδu(t)DN(t)dt=Im01ψ(t)e2πiNtdt=Imψ^(N).

L3step 2.1algebra
4.1

By [L6], ψ^(N)0. So step 3.1 gives ηδu(t)DN(t)dt0. Choose N0 such that the absolute value of this integral is below ε/2 for every NN0. Combining with step 2.1 shows that, for NN0, 0δu(t)DN(t)dt<ε. Since DN(t)=sin((2N+1)πt)/sin(πt) on (0,δ] by [L3], the stated limit follows.

L3L6step 2.1step 3.1choosealgebra

Depends on

Used by

Dependency tree · two levels

49 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