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.
The classical Weierstrass function
Definition
Let and let be an odd integer. The integers and rationals are identified with their canonical copies in (The integers as equivalence classes of pairs of naturals, The integers embed in the rationals, The rationals embed densely in the reals), and powers are those of Integer powers . The classical Weierstrass function with parameters is
The sum begins at . Its existence at every real , and the fact that it defines a continuous real function, are proved in The classical Weierstrass series converges uniformly to a continuous function ↗.
Remarks
The restriction that be odd is not needed for convergence. It enters the probe-point identities used in the nowhere-differentiability argument, where odd powers preserve parity.
Depends on
- A series of real-valued functions and its pointwise and uniform convergence through its partial sums
- Sine and cosine defined by their real power series
- Pi as twice the smallest positive zero of cosine
- Integer powers $a^m$
- The integers as equivalence classes of pairs of naturals
- The integers embed in the rationals
- The rationals embed densely in the reals
Used by
- A uniform limit of smooth functions need not be differentiable anywhere Corollary
- The Weierstrass function with a=1/2 and b=15 Example
- Nearest-integer probe points for the Weierstrass function Lemma
- The classical Weierstrass series converges uniformly to a continuous function Theorem
- Under ab>1+3π/2, the classical Weierstrass function is continuous everywhere and differentiable nowhere Theorem
Dependency tree · two levels
35 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
- Jeff Calder, Weierstrass's Non-Differentiable Function, Theorem 1 (standard reference, not scraped)
- John K. Hunter, An Introduction to Real Analysis, Example 9.24 (standard reference, not scraped)