TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-21

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.

Under $a b > 1 + 3 π / 2$ , the classical Weierstrass function is continuous everywhere and differentiable nowhere

Statement

Let $0 < a < 1$ , let $b > 1$ be an odd integer, and let $W_{a, b}$ be the classical Weierstrass function (The classical Weierstrass function). If $a b > 1 + 3 π / 2$ , then $W_{a, b}$ is continuous at every real point and differentiable at no real point.

Facts & Assumptions

Given: Parameters $0 < a < 1$ and an odd integer $b > 1$ satisfying $a b > 1 + 3 π / 2$ , and an arbitrary point $x_{0} \in R$ .

[L1]

The sum $W_{a, b} : R \to R$ is continuous (The classical Weierstrass series converges uniformly to a continuous function).

[L2]

For every $m \geq 1$ , the low-frequency increment at the probes satisfies $∣ A_{m} ∣ < π (a b)^{m} (x_{m} - x_{0}) / (a b - 1)$ (Low-frequency bound for the Weierstrass difference quotient).

[L3]

For the tail increment at the same probes, $∣ B_{m} ∣ \geq (2 / 3) (a b)^{m} (x_{m} - x_{0})$ (The Weierstrass tail has one sign and dominates at the probe points).

[L4]

If $∣ r ∣ > 1$ , then $∣ r ∣^{m}$ diverges to $+ \infty$ (For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ ).

[L5]

Differentiability at $x_{0}$ requires the finite limit of $(W_{a, b} (x) - W_{a, b} (x_{0})) / (x - x_{0})$ as $x \to x_{0}$ (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set).

[L6]

The probes satisfy $x_{m} > x_{0}$ and $x_{m} \to x_{0}$ (Nearest-integer probe points for the Weierstrass function).

[L7]

The number $π = 2 γ$ is positive because the smallest positive zero of cosine satisfies $γ \in (0, 2)$ (Pi as twice the smallest positive zero of cosine, Cosine has a smallest positive zero, lying strictly between zero and two).

Proof

technique · direct

1.1givenL1L6

Fix $x_{0}$ and use [L6] for its probe sequence $(x_{m})$ . Continuity at $x_{0}$ already follows from [L1].

1.2givenL7algebra

The hypothesis $a b > 1 + 3 π / 2$ and positivity of $π$ give $a b > 1$ and $c : = \frac{2}{3} - \frac{π}{a b - 1} > 0.$

2.1step 1.1L2L3algebra

For $m \geq 1$ , splitting the series increment at frequency $m$ gives $W_{a, b} (x_{m}) - W_{a, b} (x_{0}) = A_{m} + B_{m}$ . The reverse triangle inequality and [L2] to [L3] yield $∣ W_{a, b} (x_{m}) - W_{a, b} (x_{0}) ∣ \geq (a b)^{m} (\frac{2}{3} - \frac{π}{a b - 1}) (x_{m} - x_{0}) .$

3.1step 1.2step 2.1L4algebra

Since $x_{m} - x_{0} > 0$ , divide step 2.1 by it. Step 1.2 and [L4] show that the absolute values of the selected difference quotients are at least $c (a b)^{m}$ and tend to $+ \infty$ .

4.1step 1.1step 3.1L1L5∎

Although $x_{m} \to x_{0}$ , the difference quotients along this sequence have no finite limit by step 3.1, so [L5] rules out differentiability at $x_{0}$ . The point $x_{0}$ was arbitrary, while [L1] gives continuity everywhere. Then $W_{a, b}$ is continuous at every real point and differentiable at no real point.

Depends on

Used by

Dependency tree · two levels

61 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)

Under ab>1+3π/2ab>1+3π/2, the classical Weierstrass function is continuous everywhere and differentiable nowhere