theorem reverse_triangle_three (a b c : ℝ) : |a + b + c| ≥ |a| - |b| - |c|

Theorem II (reverse triangle inequality, three terms). For all real numbers a, b, c, the absolute value of their sum is at least |a| - |b| - |c|.

theorem weierstrass_theorem_I : (∀ (x y : ℝ), |Real.cos x - Real.cos y| ≤ |x - y|) ∧ ∀ (c : ℝ) (K : ℕ), 0 < K → ∃ (y : ℝ), c + Real.pi / ↑K < y ∧ y < c + 3 * Real.pi / ↑K ∧ |Real.cos (↑K * c) - Real.cos (↑K * y)| ≥ 1

Theorem I (cosine oscillation lemma). Two statements about the cosine function: (1) cos is 1-Lipschitz, i.e. |cos x - cos y| ≤ |x - y| for all real x, y. (2) For every real c and every positive natural number K, there exists a point y in the open interval (c + π/K, c + 3π/K) such that |cos (K c) - cos (K y)| ≥ 1.

noncomputable def weierstrass_fun (x : ℝ) : ℝ

The Weierstrass nowhere-differentiable function f(x) = ∑_{k=0}^∞ cos(160^k x) / 4^k, defined as a tsum over the natural numbers.

theorem weierstrass_theorem_III : (∀ (x : ℝ), Summable fun (k : ℕ) => |Real.cos (160 ^ k * x) / 4 ^ k|) ∧ Continuous weierstrass_fun ∧ ∃ (B : ℝ), ∀ (x : ℝ), |weierstrass_fun x| ≤ B

Theorem III. The defining series of the Weierstrass function is well-behaved: (1) for every x ∈ ℝ, the series ∑ k, cos(160^k x) / 4^k is absolutely convergent; (2) the function weierstrass_fun is continuous and bounded on ℝ.

theorem weierstrass_summable (x : ℝ) : Summable fun (k : ℕ) => Real.cos (160 ^ k * x) / 4 ^ k

For every real x, the series ∑ k, cos(160^k x) / 4^k defining the Weierstrass function is summable, by comparison with the geometric series ∑ (1/4)^k.

theorem weierstrass_slope_lower_bound (c : ℝ) (n : ℕ) : ∃ (y : ℝ), y ≠ c ∧ |y - c| < 3 * Real.pi / 160 ^ n ∧ |(weierstrass_fun y - weierstrass_fun c) / (y - c)| ≥ 40 ^ n / (117 * Real.pi)

Slope blow-up lemma. For every real c and every natural number n, there exists a point y ≠ c with |y - c| < 3π / 160^n such that the difference quotient of the Weierstrass function between y and c has absolute value at least 40^n / (117 π). Since 40^n / (117 π) → ∞, this witnesses that the function cannot have a finite derivative at c.

theorem weierstrass_nowhere_differentiable (c : ℝ) : ¬DifferentiableAt ℝ weierstrass_fun c

Weierstrass's theorem. The function weierstrass_fun x = ∑ k, cos(160^k x) / 4^k is nowhere differentiable on ℝ: for every c, weierstrass_fun fails to be differentiable at c. The proof uses weierstrass_slope_lower_bound to exhibit a sequence of points approaching c along which the difference quotients diverge to infinity, contradicting the convergence of the slope to a finite derivative.