Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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.

A continuous function with divergent Fourier series at a prescribed point

Statement refuted

Continuity of a one-periodic real function guarantees convergence of its Fourier series at a prescribed point.

More precisely, assume DC. For every x0T there exists fC(T,R) such that

supN0SNf(x0)=.

Facts & Assumptions

Given: DC and a prescribed point x0T=R/Z.

[F1]

On real or complex C(T) the functional fSNf(x0) is bounded, has norm DN1, and these norms are unbounded (Fourier partial-sum operator norm equals the Lebesgue constant).

[F2]

Assuming DC, a pointwise bounded family of bounded linear maps from a Banach space to a normed space has uniformly bounded operator norms (Uniform boundedness principle).

[F3]

For a nonempty compact metric space K, C(K,R) is complete in the supremum metric (C(K,R) is complete in the supremum metric for every nonempty compact metric space K).

[F4]

Assuming countable choice, if a one-period integrable function h satisfies 0δh(x+t)+h(xt)2sdt/t< for some δ(0,1/2), then SNh(x)s (Dini pointwise convergence criterion for Fourier series).

Counterexample

technique · direct application of uniform boundedness
1.1

Let X={fC([0,1],R):f(0)=f(1)} with the supremum norm. The interval is nonempty and compact, so a Cauchy sequence in X has a continuous uniform limit by the completeness theorem. Its endpoint values remain equal, since f(0)f(1)2ffj for every approximating member fj. Thus X is a real Banach space, identified isometrically with the real continuous periodic functions.

F3algebra
2.1

Define TN:XR by TNf=SNf(x0). These maps are real-valued bounded linear functionals, and supNTN=. If all fX had supNTNf<, uniform boundedness on this Banach space would make the operator norms uniformly bounded. Hence there exists a real fX with supNTNf=. Every individual value is finite, so this sequence cannot converge.

F1F2step 1.1
3.1

For this witness, vanishing on any neighborhood of x0 is impossible: if it vanished there, choose 0<δ<1/2 within that neighborhood. The Dini integral with s=0 would be zero, giving SNf(x0)0. DC supplies the countable choice assumed by that criterion. This contradicts the unboundedness in step 2.1 and proves the stated localization observation.

F4step 2.1given

Depends on

Used by

Dependency tree · two levels

21 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