Weierstrass function

TheoremCosine oscillation (phase-shift form)#✓fully proved

For every real number \(\theta\) there is a real number \(\varphi\) with \(\pi < \varphi < 3\pi\) such that \(|\cos\theta - \cos(\theta + \varphi)| \ge 1\).

The two candidate shifts are \(3\pi/2\) and \(5\pi/2\), where \(\cos(\theta + \varphi)\) equals \(\sin\theta\) and \(-\sin\theta\) respectively; at least one of \(|\cos\theta - \sin\theta|\) and \(|\cos\theta + \sin\theta|\) is at least \(1\), since their squares sum to \(2\).

theorem exists_cos_sub_cos_ge_one (θ : ℝ) :
    ∃ φ : ℝ, π < φ ∧ φ < 3 * π ∧ 1 ≤ |cos θ - cos (θ + φ)|

Used by 1

Used byCosine oscillation (scaled form)

TheoremCosine oscillation (scaled form)#✓fully proved

For every real number \(c\) and every positive integer \(K\), there is a real number \(y\) with \(c + \pi / K < y < c + 3\pi / K\) such that \(|\cos(Kc) - \cos(Ky)| \ge 1\).

This is the estimate that drives the slope blow-up in the proof that the Weierstrass function is nowhere differentiable.

theorem exists_cos_oscillation (c : ℝ) (K : ℕ) (hK : 0 < K) :
    ∃ y : ℝ, c + π / K < y ∧ y < c + 3 * π / K ∧
      1 ≤ |cos ((K : ℝ) * c) - cos ((K : ℝ) * y)|

Uses 1 · Used by 1

Proof usesCosine oscillation (phase-shift form)

Used bySlope blow-up lemma

DefinitionThe Weierstrass function#✓fully proved

The Weierstrass function is the function \(W : \mathbb{R} \to \mathbb{R}\) given by \(W(x) = \sum_{k \ge 0} \cos(160^k x) / 4^k\), the sum running over all natural numbers \(k\).

noncomputable def weierstrassFun (x : ℝ) : ℝ :=
  ∑' k : ℕ, cos (160 ^ k * x) / 4 ^ k

Used by 4

Used byContinuity of the Weierstrass function · Bound on the Weierstrass function · The Weierstrass function is nowhere differentiable · Slope blow-up lemma

TheoremTermwise bound for the Weierstrass series#✓fully proved

For every natural number \(k\) and every real number \(x\), \(|\cos(160^k x) / 4^k| \le (1/4)^k\).

The right-hand side is the \(k\)-th term of a convergent geometric series.

theorem norm_weierstrassFun_term_le (k : ℕ) (x : ℝ) :
    ‖cos (160 ^ k * x) / 4 ^ k‖ ≤ (1 / 4 : ℝ) ^ k

Used by 4

Used byContinuity of the Weierstrass function · Absolute convergence of the Weierstrass series · Summability of the Weierstrass series · Bound on the Weierstrass function

TheoremSummability of the Weierstrass series#✓fully proved

For every real number \(x\), the series \(\sum_{k \ge 0} \cos(160^k x) / 4^k\) defining the Weierstrass function is summable, by comparison with the geometric series \(\sum_{k \ge 0} (1/4)^k\).

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

Uses 1 · Used by 1

Proof usesTermwise bound for the Weierstrass series

Used bySlope blow-up lemma

TheoremAbsolute convergence of the Weierstrass series#✓fully proved

For every real number \(x\), the series \(\sum_{k \ge 0} \cos(160^k x) / 4^k\) defining the Weierstrass function converges absolutely, that is, \(\sum_{k \ge 0} |\cos(160^k x) / 4^k|\) is summable.

theorem summable_abs_weierstrassFun_terms (x : ℝ) :
    Summable (fun k : ℕ => |cos (160 ^ k * x) / 4 ^ k|)

Uses 1

Proof usesTermwise bound for the Weierstrass series

TheoremContinuity of the Weierstrass function#✓fully proved

The Weierstrass function \(W(x) = \sum_{k \ge 0} \cos(160^k x) / 4^k\) is continuous on \(\mathbb{R}\).

It is a uniform limit of continuous partial sums.

theorem continuous_weierstrassFun : Continuous weierstrassFun

Uses 2

Statement usesThe Weierstrass function

Proof usesTermwise bound for the Weierstrass series

TheoremBound on the Weierstrass function#✓fully proved

The Weierstrass function \(W(x) = \sum_{k \ge 0} \cos(160^k x) / 4^k\) satisfies \(|W(x)| \le 4/3\) for every real number \(x\).

theorem weierstrassFun_abs_le (x : ℝ) : |weierstrassFun x| ≤ 4 / 3

Uses 2

Statement usesThe Weierstrass function

Proof usesTermwise bound for the Weierstrass series

TheoremReverse triangle inequality, three terms#✓fully proved

For all real numbers a, b, c, the absolute value of their sum is at least |a| - |b| - |c|.

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

Used by 1

Used bySlope blow-up lemma

TheoremSlope blow-up lemma#✓fully proved

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

theorem weierstrassFun_slope_lower_bound (c : ℝ) (n : ℕ) :
    ∃ y : ℝ, y ≠ c ∧ |y - c| < 3 * π / (160 : ℝ) ^ n ∧
      |(weierstrassFun y - weierstrassFun c) / (y - c)| ≥
        (40 : ℝ) ^ n / (117 * π)

Uses 4 · Used by 1

Statement usesThe Weierstrass function

Proof usesCosine oscillation (scaled form) · Reverse triangle inequality, three terms · Summability of the Weierstrass series

Used byThe Weierstrass function is nowhere differentiable

TheoremThe Weierstrass function is nowhere differentiable#✓fully proved

The Weierstrass function \(W(x) = \sum_{k=0}^{\infty} \cos(160^k x) / 4^k\) is differentiable at no point of \(\mathbb{R}\): for every real number \(c\), \(W\) is not differentiable at \(c\).

The proof uses the slope blow-up lemma to exhibit a sequence of points approaching \(c\) along which the absolute values of the difference quotients of \(W\) tend to infinity, contradicting the convergence of the slope to a finite derivative.

theorem weierstrassFun_nowhere_differentiable :
    ∀ c : ℝ, ¬ DifferentiableAt ℝ weierstrassFun c

Uses 2

Statement usesThe Weierstrass function

Proof usesSlope blow-up lemma

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.