Weierstrass function: a function that is continuous everywhere but differentiable nowhere

This file defines the real-valued Weierstrass function as

$$f(x) = \sum_{n=0}^\infty a^n \cos (b^n\pi x)$$

and prove that it is continuous everywhere but differentiable nowhere for $a \in (0, 1)$, and a positive odd integer $b$ such that

$$ab > 1 + \frac{3}{2}\pi$$

which is the original bound given by Karl Weierstrass. There is a better bound $ab \ge 1$ given by G. H. Hardy with a less elementary proof, which is not implemented here.

References

• Weierstrass, Karl, Über continuirliche Functionen eines reellen Arguments, die für keinen Werth des letzeren einen bestimmten Differentialquotienten besitzen
• G. H. Hardy, Weierstrass's Non-Differentiable Function

Definition

For real parameter $a$ and $b$, define the Weierstrass function as $$f(x) = \sum_{n=0}^\infty a^n \cos (b^n\pi x)$$

noncomputable def NowhereDifferentiable.weierstrass (a b x : ℝ) : ℝ

Equations

• NowhereDifferentiable.weierstrass a b x = ∑' (n : ℕ), a ^ n * Real.cos (b ^ n * Real.pi * x)

Continuity

We show that for $a \in (0, 1)$, the summation in the definition is uniformly convergent, each term is uniformly continuous, and therefore Weierstrass function is uniformly continuous.

theorem NowhereDifferentiable.hasSumUniformlyOn_weierstrass {a : ℝ} (ha : a ∈ Set.Ioo 0 1) (b : ℝ) : HasSumUniformlyOn (fun (n : ℕ) (x : ℝ) => a ^ n * Real.cos (b ^ n * Real.pi * x)) (weierstrass a b) Set.univ

theorem NowhereDifferentiable.tendstoUniformly_weierstrass {a : ℝ} (ha : a ∈ Set.Ioo 0 1) (b : ℝ) : TendstoUniformly (fun (s : Finset ℕ) (x : ℝ) => ∑ n ∈ s, a ^ n * Real.cos (b ^ n * Real.pi * x)) (weierstrass a b) Filter.atTop

theorem NowhereDifferentiable.summable_weierstrass {a : ℝ} (ha : a ∈ Set.Ioo 0 1) (b x : ℝ) : Summable fun (n : ℕ) => a ^ n * Real.cos (b ^ n * Real.pi * x)

theorem NowhereDifferentiable.uniformContinuous_weierstrass {a : ℝ} (ha : a ∈ Set.Ioo 0 1) (b : ℝ) : UniformContinuous (weierstrass a b)

Non-differentiability

To show that Weierstrass function $f(x)$ is not differentiable at any $x$, we choose a sequence $\{x_m\}$ such that, as $m\to\infty$

• $\{x_m\}$ converges to $x$
• The slope $(f(x_m) - f(x)) / (x_m - x)$ grows unbounded which means the derivative $f'(x)$ cannot exist.

@[reducible, inline]

noncomputable abbrev NowhereDifferentiable.seq (b x : ℝ) (m : ℕ) : ℝ

The approximating sequence seq is defined as $x_m = \lfloor b^m x + 3/2 \rfloor / b^m$

Equations

• NowhereDifferentiable.seq b x m = ↑⌊b ^ m * x + 3 / 2⌋ / b ^ m

theorem NowhereDifferentiable.seq_mul_pow {b : ℝ} (hb : b ≠ 0) (x : ℝ) (m : ℕ) : seq b x m * b ^ m = ↑⌊b ^ m * x + 2⁻¹⌋ + 1

Show that $x_m \in (x, x + 3 / (2b^m)]$, and it tends to $x$ by squeeze theorem.

theorem NowhereDifferentiable.lt_seq {b : ℝ} (hb : 0 < b) (x : ℝ) (m : ℕ) : x < seq b x m

theorem NowhereDifferentiable.le_seq {b : ℝ} (hb : 0 < b) (x : ℝ) (m : ℕ) : x ≤ seq b x m

theorem NowhereDifferentiable.seq_le {b : ℝ} (hb : 0 < b) (x : ℝ) (m : ℕ) : seq b x m ≤ x + 3 / 2 * b⁻¹ ^ m

theorem NowhereDifferentiable.tendsto_seq {b : ℝ} (hb : 1 < b) (x : ℝ) : Filter.Tendsto (fun (x_1 : ℕ) => seq b x x_1) Filter.atTop (nhds x)

theorem NowhereDifferentiable.tendsto_seq_sub_inv {b : ℝ} (hb : 1 < b) (x : ℝ) : Filter.Tendsto (fun (m : ℕ) => (seq b x m - x)⁻¹) Filter.atTop Filter.atTop

To estimate the slope $(f(x_m) - f(x)) / (x_m - x)$, we break the infinite sum in $f(x_m) - f(x)$ into two parts $f(x_m) - f(x) = A + B$, where

$$ A = ∑_{n=0}^{m-1} a^n (\cos(b^n\pi x_m) - \cos(b^n\pi x)) $$ $$ B = ∑_{n=m}^{\infty} a^n (\cos(b^n\pi x_m) - \cos(b^n\pi x)) $$

theorem NowhereDifferentiable.weierstrass_partial {a : ℝ} (ha : 0 < a) {b : ℕ} (hab : 1 < a * ↑b) (x : ℝ) (m : ℕ) : |∑ n ∈ Finset.range m, a ^ n * (Real.cos (↑b ^ n * Real.pi * seq (↑b) x m) - Real.cos (↑b ^ n * Real.pi * x))| ≤ |seq (↑b) x m - x| * (Real.pi / (a * ↑b - 1) * (a * ↑b) ^ m)

The partial sum has upper bound in absolute value $|A| \le |x_m - x| \pi (ab)^m / (ab - 1)$

theorem NowhereDifferentiable.weierstrass_remainder {a : ℝ} (ha : 0 < a) {b : ℕ} (hb : Odd b) {x : ℝ} {m : ℕ} (hsum : Summable fun (n : ℕ) => a ^ (n + m) * (Real.cos (↑b ^ (n + m) * Real.pi * seq (↑b) x m) - Real.cos (↑b ^ (n + m) * Real.pi * x))) : |seq (↑b) x m - x| * (2 / 3 * (a * ↑b) ^ m) ≤ |∑' (n : ℕ), a ^ (n + m) * (Real.cos (↑b ^ (n + m) * Real.pi * seq (↑b) x m) - Real.cos (↑b ^ (n + m) * Real.pi * x))|

The remainder has lower bound in absolute value $|B| \ge |x_m - x| 2 (ab)^m / 3$

With bounds for $|A|$ and $|B|$ found, we have

$$ |f(x_m) - f(x)| = |A + B| \ge |B| - |A| \ge |x_m - x| (ab)^m \left(\frac{2}{3} - \frac{\pi}{ab - 1}\right) $$

It is obvious that $|f(x_m) - f(x)| / |x_m - x|$ grows exponentially and gives no limit for the derivative.

theorem NowhereDifferentiable.weierstrass_slope {a : ℝ} (ha : a ∈ Set.Ioo 0 1) {b : ℕ} (hb : Odd b) (hab : 1 < a * ↑b) (x : ℝ) (m : ℕ) : |seq (↑b) x m - x| * ((2 / 3 - Real.pi / (a * ↑b - 1)) * (a * ↑b) ^ m) ≤ |weierstrass a (↑b) (seq (↑b) x m) - weierstrass a (↑b) x|

theorem NowhereDifferentiable.not_differentiableAt_weierstrass {a : ℝ} (ha : a ∈ Set.Ioo 0 1) {b : ℕ} (hb : Odd b) (hab : 3 / 2 * Real.pi + 1 < a * ↑b) (x : ℝ) : ¬DifferentiableAt ℝ (weierstrass a ↑b) x

theorem NowhereDifferentiable.not_differentiableAt_weierstrass_seven (x : ℝ) : ¬DifferentiableAt ℝ (weierstrass 0.9 7) x

A concrete example of $a$ and $b$ to show that the condition is not vacuous.

theorem NowhereDifferentiable.exists_uniformContinuous_and_not_differentiableAt : ∃ (f : ℝ → ℝ), UniformContinuous f ∧ ∀ (x : ℝ), ¬DifferentiableAt ℝ f x