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 residual set of continuous functions has unbounded partial sums at zero
Example
Assume DC. In the real Banach space with supremum norm, the set
is a dense .
Facts & Assumptions
Given: DC, the period-one torus with Haar mass one, and real continuous functions with the supremum norm.
For each , evaluation on real has norm , and these norms are unbounded (Fourier partial-sum operator norm equals the Lebesgue constant).
Under DC, a family of bounded linear maps from a Banach space to a normed space either has uniformly bounded norms or has a dense set of points with unbounded output norms (Baire dichotomy for a pointwise-defined family of bounded linear operators).
For every nonempty compact metric space , is complete in the supremum metric ( is complete in the supremum metric for every nonempty compact metric space ).
Verification
Real continuous periodic functions identify isometrically with . A Cauchy sequence has a continuous uniform limit by completeness on the nonempty compact interval. Endpoint equality passes to that limit because evaluation at either endpoint changes by at most the uniform error. Hence is Banach.
The family consists of bounded linear maps, with unbounded operator norms. The bounded-norm alternative in the dichotomy is therefore excluded; its other alternative says precisely that is dense and in .
Explicitly, . Each inner set is open by continuity of , and the displayed membership condition is exactly unboundedness of the sequence of finite values. Thus the topology in this conclusion is topology on a space of functions; it asserts no full-measure set of points of the torus for any fixed function.
Depends on
Used by
Nothing in the library uses this result yet.
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
- Laugesen, Harmonic Analysis Lecture Notes (standard reference, not scraped)