|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Weiyi Wang. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Weiyi Wang |
| 5 | +-/ |
| 6 | +import Mathlib.Analysis.Real.Pi.Bounds |
| 7 | +import Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn |
| 8 | + |
| 9 | +/-! |
| 10 | +# Weierstrass function: a function that is continuous everywhere but differentiable nowhere |
| 11 | +
|
| 12 | +This file defines the real-valued Weierstrass function as |
| 13 | +
|
| 14 | +$$f(x) = \sum_{n=0}^\infty a^n \cos (b^n\pi x)$$ |
| 15 | +
|
| 16 | +and prove that it is continuous everywhere but differentiable nowhere for $a \in (0, 1)$, and |
| 17 | +positive odd integer $b$ such that |
| 18 | +
|
| 19 | +$$ab > 1 + \frac{3}{2}\pi$ |
| 20 | +
|
| 21 | +which is the original bound given by Karl Weierstrass. There is a better bound $ab \ge 1$ given by |
| 22 | +G. H. Hardy, but it is not implemented here. |
| 23 | +
|
| 24 | +## References |
| 25 | +
|
| 26 | +* [Weierstrass, Karl, *Über continuirliche Functionen eines reellen Arguments, die für keinen Werth |
| 27 | +des letzeren einen bestimmten Differentialquotienten besitzen*][weierstrass1895] |
| 28 | +
|
| 29 | +-/ |
| 30 | + |
| 31 | +open Real Topology Filter |
| 32 | + |
| 33 | +/-! |
| 34 | +### Definition |
| 35 | +
|
| 36 | +For real parameter $a$ and $b$, define the Weierstrass function as |
| 37 | +$$f(x) = \sum_{n=0}^\infty a^n \cos (b^n\pi x)$$ |
| 38 | +-/ |
| 39 | + |
| 40 | +noncomputable |
| 41 | +def weierstrass (a b x : ℝ) := ∑' n, a ^ n * cos (b ^ n * π * x) |
| 42 | + |
| 43 | +/-! |
| 44 | +### Continuity |
| 45 | +
|
| 46 | +We show that for $a \in (0, 1)$, the summation in the definition is uniformly convergent, |
| 47 | +each term is uniformly continuous, and therefore Weierstrass function is uniformly continuous. |
| 48 | +-/ |
| 49 | + |
| 50 | +theorem hasSumUniformlyOn_weierstrass {a : ℝ} (ha : a ∈ Set.Ioo 0 1) (b : ℝ) : |
| 51 | + HasSumUniformlyOn (fun n x ↦ a ^ n * cos (b ^ n * π * x)) (weierstrass a b) Set.univ := by |
| 52 | + have habs : |(|a|)| < 1 := by grind [abs_abs, abs_lt] |
| 53 | + apply HasSumUniformlyOn.of_norm_le_summable (summable_geometric_of_abs_lt_one habs) |
| 54 | + intro n x _ |
| 55 | + simpa using mul_le_mul_of_nonneg_left (abs_cos_le_one (b ^ n * π * x)) (abs_nonneg (a ^ n)) |
| 56 | + |
| 57 | +theorem tendstoUniformly_weierstrass {a : ℝ} (ha : a ∈ Set.Ioo 0 1) (b : ℝ) : |
| 58 | + TendstoUniformly (fun s x ↦ ∑ n ∈ s, a ^ n * cos (b ^ n * π * x)) |
| 59 | + (weierstrass a b) atTop := by |
| 60 | + rw [← tendstoUniformlyOn_univ] |
| 61 | + exact (hasSumUniformlyOn_iff_tendstoUniformlyOn).mp (hasSumUniformlyOn_weierstrass ha b) |
| 62 | + |
| 63 | +theorem summable_weierstrass {a : ℝ} (ha : a ∈ Set.Ioo 0 1) (b x : ℝ) : |
| 64 | + Summable fun n ↦ a ^ n * cos (b ^ n * π * x) := |
| 65 | + (hasSumUniformlyOn_weierstrass ha b).summableUniformlyOn.summable (Set.mem_univ x) |
| 66 | + |
| 67 | +theorem uniformContinuous_weierstrass {a : ℝ} (ha : a ∈ Set.Ioo 0 1) (b : ℝ) : |
| 68 | + UniformContinuous (weierstrass a b) := by |
| 69 | + apply TendstoUniformly.uniformContinuous (tendstoUniformly_weierstrass ha b) |
| 70 | + refine .of_forall fun s ↦ s.uniformContinuous_sum fun n _ ↦ ?_ |
| 71 | + exact (lipschitzWith_cos.uniformContinuous.comp (uniformContinuous_id.const_mul' _)).const_mul' _ |
| 72 | + |
| 73 | +/-! |
| 74 | +### Non-differentiability |
| 75 | +
|
| 76 | +To show that Weierstrass function $f(x)$ is not differentiable at any $x$, we choose a sequence |
| 77 | +$\{x_m\}$ such that, as $m\to\infty$ |
| 78 | + - $\{x_m\}$ converges to $x$ |
| 79 | + - The slope $(f(x_m) - f(x)) / (x_m - x)$ grows unbounded |
| 80 | +which means the derivative $f'(x)$ cannot exist. |
| 81 | +-/ |
| 82 | + |
| 83 | +noncomputable |
| 84 | +def xm (b x : ℝ) (m : ℕ) := ⌊b ^ m * x + 3 / 2⌋ / b ^ m |
| 85 | + |
| 86 | +/-! |
| 87 | +Show that $x_m \in (x, x + 3 / (2b^m)]$, and it tends to $x$ by squeeze theorem. |
| 88 | +-/ |
| 89 | + |
| 90 | +theorem lt_xm {b : ℝ} (hb : 0 < b) (x : ℝ) (m : ℕ) : x < xm b x m := by |
| 91 | + unfold xm |
| 92 | + grw [← Int.sub_one_lt_floor] |
| 93 | + field_simp |
| 94 | + grind |
| 95 | + |
| 96 | +theorem le_xm {b : ℝ} (hb : 0 < b) (x : ℝ) : (fun _ ↦ x) ≤ xm b x := fun m ↦ (lt_xm hb x m).le |
| 97 | + |
| 98 | +theorem xm_le {b : ℝ} (hb : 0 < b) (x : ℝ) : xm b x ≤ fun m ↦ x + (3 / 2) * b⁻¹ ^ m := by |
| 99 | + rw [Pi.le_def] |
| 100 | + intro m |
| 101 | + unfold xm |
| 102 | + grw [Int.floor_le] |
| 103 | + apply le_of_eq |
| 104 | + have hb0' : b ^ m ≠ 0 := by simp [hb.ne.symm] |
| 105 | + rw [add_div, mul_div_cancel_left_of_imp (by simp [hb0']), inv_pow, div_eq_mul_inv] |
| 106 | + |
| 107 | +theorem tendsto_xm {b : ℝ} (hb : 1 < b) (x : ℝ) : Tendsto (xm b x ·) atTop (𝓝 x) := by |
| 108 | + unfold xm |
| 109 | + have hb0 : 0 < b := lt_trans (by norm_num) hb |
| 110 | + refine tendsto_of_tendsto_of_tendsto_of_le_of_le ?_ ?_ (le_xm hb0 x) (xm_le hb0 x) |
| 111 | + · exact tendsto_const_nhds_iff.mpr rfl |
| 112 | + rw [show 𝓝 x = 𝓝 (x + (3 / 2) * 0) by simp] |
| 113 | + refine tendsto_const_nhds.add (Tendsto.const_mul _ ?_) |
| 114 | + refine tendsto_pow_atTop_nhds_zero_of_lt_one (by simpa using hb0.le) ?_ |
| 115 | + exact (inv_lt_one₀ hb0).mpr hb |
| 116 | + |
| 117 | +theorem tendsto_inv_xm_sub_x {b : ℝ} (hb : 1 < b) (x : ℝ) : |
| 118 | + Tendsto (fun m ↦ (xm b x m - x)⁻¹) atTop atTop := by |
| 119 | + have hb0 : 0 < b := lt_trans (by norm_num) hb |
| 120 | + apply Tendsto.inv_tendsto_nhdsGT_zero |
| 121 | + refine tendsto_nhdsWithin_iff.mpr ⟨?_, .of_forall fun m ↦ by simpa using lt_xm hb0 x m⟩ |
| 122 | + rw [tendsto_sub_nhds_zero_iff] |
| 123 | + exact tendsto_xm hb x |
| 124 | + |
| 125 | +/-! |
| 126 | +To estimate the slope $(f(x_m) - f(x)) / (x_m - x)$, we break the infinite sum in |
| 127 | +$f(x_m) - f(x)$ into two parts |
| 128 | +
|
| 129 | +$$ f(x_m) - f(x) = ∑_{n=0}^{m-1} a^n (\cos(b^n\pi x_m) - \cos(b^n\pi x)) |
| 130 | ++ ∑_{n=m}^{\infty} a^n (\cos(b^n\pi x_m) - \cos(b^n\pi x)) = A + B$$ |
| 131 | +-/ |
| 132 | + |
| 133 | +/-- The partial sum has upper bound in absolute value $|A| \le |x_m - x| \pi (ab)^m / (ab - 1)$ -/ |
| 134 | +theorem weierstrass_partial {a : ℝ} (ha : 0 < a) {b : ℕ} (hab : 1 < a * b) (x : ℝ) (m : ℕ) : |
| 135 | + |∑ n ∈ Finset.range m, a ^ n * (cos (b ^ n * π * xm b x m) - cos (b ^ n * π * x))| ≤ |
| 136 | + |xm b x m - x| * (π / (a * b - 1) * (a * b) ^ m) := by |
| 137 | + grw [Finset.abs_sum_le_sum_abs] |
| 138 | + simp_rw [abs_mul, abs_pow, abs_eq_self.mpr ha.le] |
| 139 | + apply le_trans <| Finset.sum_le_sum fun n _ ↦ |
| 140 | + mul_le_mul_of_nonneg_left (abs_cos_sub_cos_le _ _) (pow_nonneg ha.le _) |
| 141 | + have (n : ℕ) : a ^ n * |b ^ n * π * xm b x m - b ^ n * π * x| = |
| 142 | + (a * b) ^ n * (π * |xm b x m - x|) := by |
| 143 | + simp_rw [← mul_sub, abs_mul, abs_pow, mul_pow] |
| 144 | + rw [abs_eq_self.mpr pi_nonneg, abs_eq_self.mpr b.cast_nonneg] |
| 145 | + ring |
| 146 | + simp_rw [this, ← Finset.sum_mul, geom_sum_eq hab.ne.symm] |
| 147 | + field_simp |
| 148 | + refine div_le_div_of_nonneg_right ?_ (sub_nonneg.mpr hab.le) |
| 149 | + simp [sub_one_mul] |
| 150 | + |
| 151 | +/-- The remainder has lower bound in absolute value $|B| \ge |x_m - x| 2 (ab)^m / 3$ -/ |
| 152 | +theorem weierstrass_remainder {a : ℝ} (ha : 0 < a) {b : ℕ} (hb : Odd b) {x : ℝ} {m : ℕ} |
| 153 | + (hsum : Summable fun n ↦ |
| 154 | + a ^ (n + m) * (cos (b ^ (n + m) * π * xm b x m) - cos (b ^ (n + m) * π * x))) : |
| 155 | + |xm b x m - x| * (2 / 3 * (a * b) ^ m) ≤ |
| 156 | + |∑' n, a ^ (n + m) * (cos (b ^ (n + m) * π * xm b x m) - cos (b ^ (n + m) * π * x))| := by |
| 157 | + have hb0 : b ≠ 0 := fun h ↦ Nat.not_odd_zero (h ▸ hb) |
| 158 | + have hb0' : (0 : ℝ) < b := by simpa using Nat.pos_of_ne_zero hb0 |
| 159 | + -- We are going to show that all terms in the sum have the same sign, |
| 160 | + -- and we only need to use the first term to get the lower bound |
| 161 | + trans a ^ m * (1 + cos ((b ^ m * x - ⌊b ^ m * x + 2⁻¹⌋) * π)) |
| 162 | + · -- Show that the first term (after simplification) satisfies the bound |
| 163 | + suffices a ^ m * (2 / 3 * b ^ m * |xm b x m - x|) ≤ |
| 164 | + a ^ m * (1 + cos ((b ^ m * x - ⌊b ^ m * x + 2⁻¹⌋) * π)) by |
| 165 | + convert this using 1 |
| 166 | + ring |
| 167 | + refine mul_le_mul_of_nonneg_left ?_ (pow_nonneg ha.le _) |
| 168 | + trans 1 |
| 169 | + · rw [abs_eq_self.mpr (by simpa using (lt_xm hb0' _ _).le), xm] |
| 170 | + grw [Int.floor_le] |
| 171 | + apply le_of_eq |
| 172 | + have : b ^ m ≠ (0 : ℝ) := by simp [hb0] |
| 173 | + field_simp |
| 174 | + ring |
| 175 | + · rw [le_add_iff_nonneg_right] |
| 176 | + refine cos_nonneg_of_mem_Icc (Set.mem_Icc.mpr ⟨?_, ?_⟩) |
| 177 | + · grw [Int.floor_le] |
| 178 | + grind |
| 179 | + · grw [← Int.sub_one_lt_floor] |
| 180 | + apply le_of_eq |
| 181 | + ring |
| 182 | + -- Show that the first cos in each term is always ±1 |
| 183 | + have h1 (n : ℕ) : cos (b ^ (n + m) * π * xm b x m) = - (-1) ^ (⌊b ^ m * x + 2⁻¹⌋) := |
| 184 | + calc |
| 185 | + _ = cos (b ^ n * ⌊b ^ m * x + 2⁻¹ + 1⌋ * π / b ^ m * b ^ m) := by |
| 186 | + rw [xm] |
| 187 | + ring_nf |
| 188 | + _ = cos (b ^ n * (⌊b ^ m * x + 2⁻¹⌋ + 1) * π) := by |
| 189 | + simp [hb0] |
| 190 | + _ = cos ((b ^ n * (⌊b ^ m * x + 2⁻¹⌋ + 1) : ℤ) * π) := by norm_num |
| 191 | + _ = (-1) ^ (b ^ n * (⌊b ^ m * x + 2⁻¹⌋ + 1)) := by rw [cos_int_mul_pi] |
| 192 | + _ = ((-1) ^ b ^ n) ^ (⌊b ^ m * x + 2⁻¹⌋) * (-1) ^ b ^ n := by |
| 193 | + rw [mul_add_one, zpow_add₀ (by simp), zpow_mul] |
| 194 | + norm_cast |
| 195 | + _ = _ := by |
| 196 | + simp [Odd.neg_one_pow (show Odd (b ^ n) from hb.pow)] |
| 197 | + -- Show that the second cos in each term is always ±cos(...) |
| 198 | + have h2 (n : ℕ) : cos (b ^ (n + m) * π * x) = |
| 199 | + (-1) ^ (⌊b ^ m * x + 2⁻¹⌋) * cos (b ^ n * (b ^ m * x - ⌊b ^ m * x + 2⁻¹⌋) * π) := |
| 200 | + calc |
| 201 | + _ = cos (b ^ n * (b ^ m * x - ⌊b ^ m * x + 2⁻¹⌋) * π + |
| 202 | + (b ^ n * (⌊b ^ m * x + 2⁻¹⌋) : ℤ) * π) := by |
| 203 | + push_cast |
| 204 | + ring_nf |
| 205 | + _ = ((-1) ^ b ^ n) ^ (⌊b ^ m * x + 2⁻¹⌋) * |
| 206 | + cos (b ^ n * (b ^ m * x - ⌊b ^ m * x + 2⁻¹⌋) * π) := by |
| 207 | + rw [cos_add_int_mul_pi, zpow_mul] |
| 208 | + norm_cast |
| 209 | + _ = _ := by |
| 210 | + simp [Odd.neg_one_pow (show Odd (b ^ n) from hb.pow)] |
| 211 | + -- Show that all terms have the same sign, and the first term agrees with the one we previously |
| 212 | + -- assumed |
| 213 | + have h3 (n : ℕ) : a ^ (n + m) * (cos (b ^ (n + m) * π * xm b x m) - cos (b ^ (n + m) * π * x)) |
| 214 | + = - (-1) ^ (⌊b ^ m * x + 2⁻¹⌋) * |
| 215 | + (a ^ (n + m) * (1 + cos (b ^ n * (b ^ m * x - ⌊b ^ m * x + 2⁻¹⌋) * π))) := by |
| 216 | + rw [h1, h2] |
| 217 | + ring |
| 218 | + simp_rw [h3, tsum_mul_left] at ⊢ hsum |
| 219 | + rw [summable_mul_left_iff (by grind [zpow_ne_zero])] at hsum |
| 220 | + rw [abs_mul, abs_neg, abs_neg_one_zpow, one_mul] |
| 221 | + have h (n : ℕ) : 0 ≤ a ^ (n + m) * (1 + cos (b ^ n * (b ^ m * x - ⌊b ^ m * x + 2⁻¹⌋) * π)) := by |
| 222 | + apply mul_nonneg (by positivity) |
| 223 | + grind [neg_one_le_cos] |
| 224 | + -- extract first term |
| 225 | + rw [abs_eq_self.mpr (tsum_nonneg h), Summable.tsum_eq_zero_add hsum] |
| 226 | + simpa using tsum_nonneg (fun n ↦ h (n + 1)) |
| 227 | + |
| 228 | +/-! |
| 229 | +With bounds for $|A|$ and $|B|$ found, we have |
| 230 | +
|
| 231 | +$$ |f(x_m) - f(x)| = |A + B| \ge |B| - |A| \ge |
| 232 | + |x_m - x| (ab)^m \left(\frac{2}{3} - \frac{\pi}{ab - 1}\right) $$ |
| 233 | +
|
| 234 | +It is obvious that $|f(x_m) - f(x)| / |x_m - x|$ grows exponentially and gives no limit for the |
| 235 | +derivative. |
| 236 | +-/ |
| 237 | + |
| 238 | +theorem weierstrass_slope {a : ℝ} (ha : a ∈ Set.Ioo 0 1) {b : ℕ} (hb : Odd b) (hab : 1 < a * b) |
| 239 | + (x : ℝ) (m : ℕ) : |
| 240 | + |xm b x m - x| * ((2 / 3 - π / (a * b - 1)) * (a * b) ^ m) ≤ |
| 241 | + |weierstrass a b (xm b x m) - weierstrass a b x| := by |
| 242 | + simp_rw [weierstrass] |
| 243 | + obtain hsxm := summable_weierstrass ha b (xm b x m) |
| 244 | + obtain hsx := summable_weierstrass ha b x |
| 245 | + obtain hsum := hsxm.sub hsx |
| 246 | + rw [← hsxm.tsum_sub hsx] |
| 247 | + simp_rw [← mul_sub] at ⊢ hsum |
| 248 | + rw [← hsum.sum_add_tsum_nat_add m] |
| 249 | + obtain hsum_shift := (summable_nat_add_iff m).mpr hsum |
| 250 | + rw [add_comm] |
| 251 | + refine le_trans ?_ (abs_sub_abs_le_abs_add _ _) |
| 252 | + rw [sub_mul (2 / 3), mul_sub |xm b x m - x|] |
| 253 | + exact sub_le_sub (weierstrass_remainder ha.1 hb hsum_shift) (weierstrass_partial ha.1 hab x m) |
| 254 | + |
| 255 | +theorem not_differentiableAt_weierstrass |
| 256 | + {a : ℝ} (ha : a ∈ Set.Ioo 0 1) {b : ℕ} (hb : Odd b) (hab : 3 / 2 * π + 1 < a * b) (x : ℝ) : |
| 257 | + ¬ DifferentiableAt ℝ (weierstrass a b) x := by |
| 258 | + have hb0 : b ≠ 0 := fun h ↦ Nat.not_odd_zero (h ▸ hb) |
| 259 | + have hb0' : (0 : ℝ) < b := by simpa using Nat.pos_of_ne_zero hb0 |
| 260 | + have hb1 : (1 : ℝ) < b := by |
| 261 | + contrapose! hab with hb1 |
| 262 | + apply (mul_le_one₀ (ha.2.le) hb0'.le hb1).trans |
| 263 | + simp [pi_nonneg] |
| 264 | + have hab' : 1 < a * b := lt_trans (lt_add_of_pos_left _ (mul_pos (by norm_num) pi_pos)) hab |
| 265 | + by_contra! |
| 266 | + obtain ⟨f', h⟩ := this |
| 267 | + have : Tendsto (fun m ↦ (xm b x m - x)⁻¹ * (weierstrass a b (xm b x m) - weierstrass a b x)) |
| 268 | + atTop (𝓝 (f' 1)) := by |
| 269 | + convert (h.lim_real 1).comp (tendsto_inv_xm_sub_x hb1 x) |
| 270 | + simp |
| 271 | + obtain h := (continuous_abs.tendsto _).comp this |
| 272 | + contrapose! h |
| 273 | + apply not_tendsto_nhds_of_tendsto_atTop |
| 274 | + -- To show the absolute value of slope tends to ∞, it suffices to show its lower bound does. |
| 275 | + suffices Tendsto ((2 / 3 - π / (a * b - 1)) * (a * b) ^ ·) atTop atTop by |
| 276 | + refine tendsto_atTop_mono (fun m ↦ ?_) this |
| 277 | + rw [Function.comp_apply, abs_mul, abs_inv] |
| 278 | + rw [le_inv_mul_iff₀ (by simpa [sub_eq_zero] using (lt_xm hb0' x _).ne.symm)] |
| 279 | + exact weierstrass_slope ha hb hab' x m |
| 280 | + have hpos : 0 < 2 / 3 - π / (a * b - 1) := by |
| 281 | + rw [sub_pos, div_lt_iff₀ (by simpa using hab'), ← div_lt_iff₀' (by norm_num), lt_sub_iff_add_lt] |
| 282 | + convert hab using 1 |
| 283 | + grind |
| 284 | + exact (tendsto_const_nhds_iff.mpr rfl).pos_mul_atTop hpos (tendsto_pow_atTop_atTop_of_one_lt hab') |
| 285 | + |
| 286 | +/-- A concrete example of $a$ and $b$ to show that the condition is not vacuous. -/ |
| 287 | +theorem not_differentiableAt_weierstrass_seven (x : ℝ) : |
| 288 | + ¬ DifferentiableAt ℝ (weierstrass 0.9 7) x := by |
| 289 | + apply not_differentiableAt_weierstrass (by norm_num) (by decide) |
| 290 | + grw [pi_lt_d2] |
| 291 | + norm_num |
| 292 | + |
| 293 | +theorem exists_continuous_and_not_differentiableAt : |
| 294 | + ∃ f : ℝ → ℝ, UniformContinuous f ∧ ∀ x, ¬ DifferentiableAt ℝ f x := |
| 295 | + ⟨weierstrass 0.9 7, uniformContinuous_weierstrass (by norm_num) _, |
| 296 | + not_differentiableAt_weierstrass_seven⟩ |
0 commit comments