theorem uniformLimit_of_summable_deriv_supNorm {a b : ℝ} (ha : a ≤ b) (f : ℕ → ℝ → ℝ) (h_diff : ∀ (n : ℕ), DifferentiableOn ℝ (f (n + 1)) (Set.Icc a b)) (h_diff_cont : ∀ (n : ℕ), ContinuousOn (fun (x : ℝ) => deriv (f (n + 1)) x) (Set.Icc a b)) (h_summable : Summable fun (n : ℕ) => supNormOn (Set.Icc a b) fun (x : ℝ) => deriv (f (n + 1)) x) (hx0 : ∃ x0 ∈ Set.Icc a b, Summable fun (n : ℕ) => f (n + 1) x0) : ∃ (f_lim : ℝ → ℝ), DifferentiableOn ℝ f_lim (Set.Icc a b) ∧ TendstoUniformlyOn (fun (N : ℕ) (x : ℝ) => ∑ n ∈ Finset.range N, f (n + 1) x) f_lim Filter.atTop (Set.Icc a b) ∧ ∀ x ∈ Set.Icc a b, deriv f_lim x = ∑' (n : ℕ), deriv (f (n + 1)) x

Theorem 3.10: if f_n : [a,b] → ℝ are differentiable with continuous derivatives, the series ∑ ‖f_n'‖∞ (equation (3.u126)) is convergent, and ∑ f_n(x0) converges for some x0 ∈ [a,b], then the series ∑ f_n converges uniformly on [a,b] to a differentiable function f, and for all x ∈ [a,b] one has equation (3.u127): f'(x) = d/dx (∑ f_n(x)) = ∑ f_n'(x).

noncomputable def weierstrassFunction (x : ℝ) : ℝ

Definition 3.11: the Weierstrass function f : ℝ → ℝ defined by f(x) = ∑_{n=1}^{∞} 4^{-n} cos(32^n π x).

Equations

• weierstrassFunction x = ∑' (n : ℕ), (4 ^ (n + 1))⁻¹ * Real.cos (32 ^ (n + 1) * Real.pi * x)

theorem helperForProposition_3_21_termContinuous (n : ℕ) : Continuous fun (x : ℝ) => (4 ^ (n + 1))⁻¹ * Real.cos (32 ^ (n + 1) * Real.pi * x)

Helper for Proposition 3.21: each Weierstrass summand is continuous.

theorem helperForProposition_3_21_coeffRewrite (n : ℕ) : (4 ^ (n + 1))⁻¹ = (1 / 4) ^ (n + 1)

Helper for Proposition 3.21: rewrite Weierstrass coefficients as geometric powers.

theorem helperForProposition_3_21_majorantSummable : Summable fun (n : ℕ) => (1 / 4) ^ (n + 1)

Helper for Proposition 3.21: the geometric majorant for Weierstrass coefficients is summable.

theorem helperForProposition_3_21_termNormBound (n : ℕ) (x : ℝ) : ‖(4 ^ (n + 1))⁻¹ * Real.cos (32 ^ (n + 1) * Real.pi * x)‖ ≤ (1 / 4) ^ (n + 1)

Helper for Proposition 3.21: each Weierstrass summand is bounded by the geometric majorant.

theorem proposition_3_21 : Continuous weierstrassFunction

Proposition 3.21: the Weierstrass function f of Definition 3.11 is continuous on ℝ.

theorem helperForProposition_3_22_cosQuarterTurns (θ : ℝ) : Real.cos (θ + Real.pi / 2) - Real.cos θ = -(Real.sin θ + Real.cos θ) ∧ Real.cos (θ + 3 * Real.pi / 2) - Real.cos θ = Real.sin θ - Real.cos θ

Helper for Proposition 3.22: quarter-turn cosine increments at a phase θ rewrite in terms of sin θ and cos θ.

theorem helperForProposition_3_22_phaseChoiceCore (θ : ℝ) : ∃ j ∈ {1, 3}, 1 ≤ |Real.cos (θ + ↑j * Real.pi / 2) - Real.cos θ|

Helper for Proposition 3.22: for every phase θ, one of the shifts by π/2 or 3π/2 changes cosine by at least 1 in absolute value.

theorem helperForProposition_3_22_phaseChoice (x : ℝ) (N : ℕ) : ∃ j ∈ {1, 3}, 1 ≤ |Real.cos (32 ^ (N + 1) * Real.pi * x + ↑j * Real.pi / 2) - Real.cos (32 ^ (N + 1) * Real.pi * x)|

Helper for Proposition 3.22: instantiate the phase-choice lemma at Weierstrass scale N.

noncomputable def helperForProposition_3_22_phaseIndex (x : ℝ) (N : ℕ) : ℕ

Helper for Proposition 3.22: choose a phase index j_N(x) ∈ {1,3} at each scale N.

Equations

• helperForProposition_3_22_phaseIndex x N = Classical.choose ⋯

theorem helperForProposition_3_22_phaseIndex_mem (x : ℝ) (N : ℕ) : helperForProposition_3_22_phaseIndex x N ∈ {1, 3}

Helper for Proposition 3.22: the chosen phase index lies in {1,3}.

theorem helperForProposition_3_22_phaseIndex_largeCosIncrement (x : ℝ) (N : ℕ) : 1 ≤ |Real.cos (32 ^ (N + 1) * Real.pi * x + ↑(helperForProposition_3_22_phaseIndex x N) * Real.pi / 2) - Real.cos (32 ^ (N + 1) * Real.pi * x)|

Helper for Proposition 3.22: the chosen phase index forces a unit-sized cosine increment.

theorem helperForProposition_3_22_phaseIndex_pos (x : ℝ) (N : ℕ) : 0 < ↑(helperForProposition_3_22_phaseIndex x N)

Helper for Proposition 3.22: the chosen phase index is positive.

noncomputable def helperForProposition_3_22_scale (x : ℝ) (N : ℕ) : ℝ

Helper for Proposition 3.22: define the scale h_N(x) = j_N(x)/(2·32^(N+1)).

Equations

• helperForProposition_3_22_scale x N = ↑(helperForProposition_3_22_phaseIndex x N) / (2 * 32 ^ (N + 1))

theorem helperForProposition_3_22_scale_pos (x : ℝ) (N : ℕ) : 0 < helperForProposition_3_22_scale x N

Helper for Proposition 3.22: all chosen scales are positive.

theorem helperForProposition_3_22_phaseIndex_eq_one_or_three (x : ℝ) (N : ℕ) : helperForProposition_3_22_phaseIndex x N = 1 ∨ helperForProposition_3_22_phaseIndex x N = 3

Helper for Proposition 3.22: the chosen phase index is either 1 or 3.

theorem helperForProposition_3_22_phaseIndex_le_three (x : ℝ) (N : ℕ) : ↑(helperForProposition_3_22_phaseIndex x N) ≤ 3

Helper for Proposition 3.22: the chosen phase index is at most 3.

theorem helperForProposition_3_22_scale_le_three_div (x : ℝ) (N : ℕ) : helperForProposition_3_22_scale x N ≤ 3 / (2 * 32 ^ (N + 1))

Helper for Proposition 3.22: each chosen scale is bounded by 3/(2·32^(N+1)).

theorem helperForProposition_3_22_threeDivPow_tendsto_zero : Filter.Tendsto (fun (N : ℕ) => 3 / (2 * 32 ^ (N + 1))) Filter.atTop (nhds 0)

Helper for Proposition 3.22: the model upper bound 3/(2·32^(N+1)) tends to 0.

theorem helperForProposition_3_22_scale_tendsto_zero (x : ℝ) : Filter.Tendsto (fun (N : ℕ) => helperForProposition_3_22_scale x N) Filter.atTop (nhds 0)

Helper for Proposition 3.22: the chosen scales tend to 0.

theorem helperForProposition_3_22_scale_tendsto_nhdsWithin_zero (x : ℝ) : Filter.Tendsto (fun (N : ℕ) => helperForProposition_3_22_scale x N) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

Helper for Proposition 3.22: the chosen scales approach 0 through positive values.

theorem helperForProposition_3_22_notTendsto_of_absLowerBound {q : ℕ → ℝ} (hbound : ∀ (N : ℕ), 8 ^ N ≤ |q N|) (L : ℝ) : ¬Filter.Tendsto q Filter.atTop (nhds L)

Helper for Proposition 3.22: any real sequence with exponential lower bound (8^N ≤ |q_N|) cannot converge to a finite real limit.

noncomputable def helperForProposition_3_22_term (n : ℕ) (x : ℝ) : ℝ

Helper for Proposition 3.22: the basic Weierstrass summand at index n.

Equations

• helperForProposition_3_22_term n x = (4 ^ (n + 1))⁻¹ * Real.cos (32 ^ (n + 1) * Real.pi * x)

theorem helperForProposition_3_22_termSummable (x : ℝ) : Summable fun (n : ℕ) => helperForProposition_3_22_term n x

Helper for Proposition 3.22: each Weierstrass term sequence is summable at fixed x.

theorem helperForProposition_3_22_tailCosCancellationAtChosenScale (x : ℝ) (N n : ℕ) (hn : N < n) : Real.cos (32 ^ (n + 1) * Real.pi * (x + helperForProposition_3_22_scale x N)) = Real.cos (32 ^ (n + 1) * Real.pi * x)

Helper for Proposition 3.22: at chosen scale, all modes n > N cancel exactly.

theorem helperForProposition_3_22_powRatio (N : ℕ) : (4 ^ (N + 1))⁻¹ * 32 ^ (N + 1) = 8 ^ (N + 1)

Helper for Proposition 3.22: ratio identity 32^(N+1)/4^(N+1)=8^(N+1).

theorem helperForProposition_3_22_termDifferenceQuotientBound (n : ℕ) (x h : ℝ) (hh : 0 < h) : |(helperForProposition_3_22_term n (x + h) - helperForProposition_3_22_term n x) / h| ≤ Real.pi * 8 ^ (n + 1)

Helper for Proposition 3.22: a single scaled term-difference quotient is bounded by π·8^(n+1).

theorem helperForProposition_3_22_geometricBound (N : ℕ) : ∑ n ∈ Finset.range N, 8 ^ (n + 1) ≤ 8 / 7 * 8 ^ N

Helper for Proposition 3.22: geometric bound for the low-frequency remainder weights.

theorem helperForProposition_3_22_coeffOverScale (N j : ℕ) (hjpos : 0 < ↑j) : (4 ^ (N + 1))⁻¹ / (↑j / (2 * 32 ^ (N + 1))) = 16 / ↑j * 8 ^ N

Helper for Proposition 3.22: coefficient/scale algebra at phase index j.

theorem helperForProposition_3_22_differenceQuotientSplitAtScale (x : ℝ) (N : ℕ) : have h := helperForProposition_3_22_scale x N; (weierstrassFunction (x + h) - weierstrassFunction x) / h = (helperForProposition_3_22_term N (x + h) - helperForProposition_3_22_term N x) / h + ∑ n ∈ Finset.range N, (helperForProposition_3_22_term n (x + h) - helperForProposition_3_22_term n x) / h

Helper for Proposition 3.22: split the chosen-scale difference quotient into dominant n = N term and low-frequency remainder (n < N).

theorem helperForProposition_3_22_dominantTermLowerBoundAtScale (x : ℝ) (N : ℕ) : have h := helperForProposition_3_22_scale x N; 16 / 3 * 8 ^ N ≤ |(helperForProposition_3_22_term N (x + h) - helperForProposition_3_22_term N x) / h|

Helper for Proposition 3.22: the dominant (n = N) increment has size at least (16/3)·8^N at the chosen scale.

theorem helperForProposition_3_22_remainderBoundAtScale (x : ℝ) (N : ℕ) : have h := helperForProposition_3_22_scale x N; |∑ n ∈ Finset.range N, (helperForProposition_3_22_term n (x + h) - helperForProposition_3_22_term n x) / h| ≤ 8 * Real.pi / 7 * 8 ^ N

Helper for Proposition 3.22: the low-frequency remainder (n < N) is bounded by (8π/7)·8^N at the chosen scale.

theorem helperForProposition_3_22_differenceQuotientLowerBoundAtChosenScale (x : ℝ) (N : ℕ) : 8 ^ N ≤ |(weierstrassFunction (x + helperForProposition_3_22_scale x N) - weierstrassFunction x) / helperForProposition_3_22_scale x N|

Helper for Proposition 3.22: the chosen-scale difference quotients have exponential lower bound.

theorem helperForProposition_3_22_notTendstoAlongChosenScales (x L : ℝ) : ¬Filter.Tendsto (fun (N : ℕ) => (weierstrassFunction (x + helperForProposition_3_22_scale x N) - weierstrassFunction x) / helperForProposition_3_22_scale x N) Filter.atTop (nhds L)

Helper for Proposition 3.22: chosen-scale difference quotients do not converge to any finite limit.

theorem helperForProposition_3_22_differentiableAt_imp_tendstoAlongChosenScales (x : ℝ) (hx : DifferentiableAt ℝ weierstrassFunction x) : ∃ (L : ℝ), Filter.Tendsto (fun (N : ℕ) => (weierstrassFunction (x + helperForProposition_3_22_scale x N) - weierstrassFunction x) / helperForProposition_3_22_scale x N) Filter.atTop (nhds L)

Helper for Proposition 3.22: differentiability at x implies convergence of chosen-scale difference quotients to some finite real limit.

theorem proposition_3_22 (x : ℝ) : ¬DifferentiableAt ℝ weierstrassFunction x

Proposition 3.22: the Weierstrass function f of Definition 3.11 is nowhere differentiable on ℝ, i.e., for every x ∈ ℝ the limit lim_{h→0} (f(x+h)-f(x))/h does not exist.