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

The sequence of functions f_n(x) = n^{-1/2} sin(n x) on ℝ.

Equations

• sinScaledSeq n x = (√↑n)⁻¹ * Real.sin (↑n * x)

def sinScaledLimit : ℝ → ℝ

The constant zero function on ℝ.

Equations

• sinScaledLimit x✝ = 0

theorem helperForProposition_3_19_eventually_inv_sqrt_lt {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, (√↑n)⁻¹ < ε

Helper for Proposition 3.19: for any ε>0, eventually 1/√n < ε.

theorem helperForProposition_3_19_norm_sinScaledSeq_le_inv_sqrt (n : ℕ) (x : ℝ) : ‖sinScaledSeq n x - sinScaledLimit x‖ ≤ (√↑n)⁻¹

Helper for Proposition 3.19: uniform bound for the scaled sine sequence.

theorem helperForProposition_3_19_deriv_sinScaledSeq (n : ℕ) (x : ℝ) : deriv (sinScaledSeq n) x = (√↑n)⁻¹ * (Real.cos (↑n * x) * ↑n)

Helper for Proposition 3.19: derivative of the scaled sine sequence.

theorem helperForProposition_3_19_not_tendsto_deriv_at_zero : ¬Filter.Tendsto (fun (n : ℕ) => deriv (sinScaledSeq n) 0) Filter.atTop (nhds (deriv sinScaledLimit 0))

Helper for Proposition 3.19: the derivatives at 0 do not converge to the derivative of the limit.

theorem proposition_3_19 : TendstoUniformlyOn sinScaledSeq sinScaledLimit Filter.atTop (Set.Icc 0 (2 * Real.pi)) ∧ (¬∀ x ∈ Set.Icc 0 (2 * Real.pi), Filter.Tendsto (fun (n : ℕ) => deriv (sinScaledSeq n) x) Filter.atTop (nhds (deriv sinScaledLimit x))) ∧ ¬TendstoUniformlyOn (fun (n : ℕ) (x : ℝ) => deriv (sinScaledSeq n) x) (fun (x : ℝ) => deriv sinScaledLimit x) Filter.atTop (Set.Icc 0 (2 * Real.pi))

Proposition 3.19: for f_n(x) = n^{-1/2} sin(n x) on [0, 2π] and f(x)=0, (f_n) converges uniformly to f on [0, 2π], but (f_n') does not converge pointwise to f' (hence not uniformly); in particular, d/dx (lim f_n) ≠ lim (d/dx f_n).

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

The sequence of functions f_n(x) = sqrt(1/n^2 + x^2) on ℝ.

Equations

• sqrtShiftedSeq n x = √(1 / ↑n ^ 2 + x ^ 2)

def absFun : ℝ → ℝ

The absolute value function on ℝ.

Equations

• absFun x = |x|

theorem helperForProposition_3_20_sqrtShiftedSeq_zero_eq_absFun : sqrtShiftedSeq 0 = absFun

Helper for Proposition 3.20: at n = 0, the sequence equals the absolute value.

theorem helperForProposition_3_20_not_differentiableAt_absFun_zero : ¬DifferentiableAt ℝ absFun 0

Helper for Proposition 3.20: absFun is not differentiable at 0.

theorem helperForProposition_3_20_Icc_mem_nhds_zero : Set.Icc (-1) 1 ∈ nhds 0

Helper for Proposition 3.20: Set.Icc (-1) 1 is a neighborhood of 0.

theorem helperForProposition_3_20_not_differentiableOn_absFun_Icc : ¬DifferentiableOn ℝ absFun (Set.Icc (-1) 1)

Helper for Proposition 3.20: absFun is not differentiable on [-1,1].

theorem helperForProposition_3_20_not_differentiableOn_sqrtShiftedSeq_zero : ¬DifferentiableOn ℝ (sqrtShiftedSeq 0) (Set.Icc (-1) 1)

Helper for Proposition 3.20: the sequence is not differentiable on [-1,1] at n = 0.

theorem helperForProposition_3_20_not_forall_differentiableOn : ¬∀ (n : ℕ), DifferentiableOn ℝ (sqrtShiftedSeq n) (Set.Icc (-1) 1)

Helper for Proposition 3.20: the full differentiability claim over all n is false.

theorem helperForProposition_3_20_eventually_inv_lt {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, (↑n)⁻¹ < ε

Helper for Proposition 3.20: for any ε>0, eventually 1/n < ε.

theorem helperForProposition_3_20_eventually_inv_succ_lt {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, (↑n + 1)⁻¹ < ε

Helper for Proposition 3.20: for any ε>0, eventually (n+1)⁻¹ < ε.

theorem helperForProposition_3_20_norm_sqrtShiftedSeq_sub_absFun_le_inv (n : ℕ) (x : ℝ) : ‖sqrtShiftedSeq n x - absFun x‖ ≤ (↑n)⁻¹

Helper for Proposition 3.20: uniform bound for the shifted square-root sequence.

theorem helperForProposition_3_20_inner_ne_zero_of_one_le (n : ℕ) (hn : 1 ≤ n) (x : ℝ) : 1 / ↑n ^ 2 + x ^ 2 ≠ 0

Helper for Proposition 3.20: the inner expression is nonzero for n ≥ 1.

theorem helperForProposition_3_20_differentiableAt_sqrtShiftedSeq_of_one_le (n : ℕ) (hn : 1 ≤ n) (x : ℝ) : DifferentiableAt ℝ (sqrtShiftedSeq n) x

Helper for Proposition 3.20: differentiability of sqrtShiftedSeq for n ≥ 1.

theorem helperForProposition_3_20_differentiableOn_sqrtShiftedSeq_of_one_le (n : ℕ) (hn : 1 ≤ n) : DifferentiableOn ℝ (sqrtShiftedSeq n) (Set.Icc (-1) 1)

Helper for Proposition 3.20: differentiability on [-1,1] for n ≥ 1.

theorem helperForProposition_3_20_differentiableOn_sqrtShiftedSeq_succ (n : ℕ) : DifferentiableOn ℝ (sqrtShiftedSeq (n + 1)) (Set.Icc (-1) 1)

Helper for Proposition 3.20: differentiability on [-1,1] for n + 1.

theorem proposition_3_20 : TendstoUniformlyOn sqrtShiftedSeq absFun Filter.atTop (Set.Icc (-1) 1) ∧ (∀ (n : ℕ), 1 ≤ n → DifferentiableOn ℝ (sqrtShiftedSeq n) (Set.Icc (-1) 1)) ∧ ¬DifferentiableAt ℝ absFun 0

Proposition 3.20: define f_n(x) = sqrt(1/n^2 + x^2) and f(x)=|x|. Then f_n converges uniformly to f on [-1,1], each f_n (for n ≥ 1) is differentiable on [-1,1], and f is not differentiable at 0; in particular, a uniform limit of differentiable functions need not be differentiable.

theorem helperForTheorem_3_9_continuousOn_g_Icc {a b : ℝ} (f : ℕ → ℝ → ℝ) (g : ℝ → ℝ) (h_diff_cont : ∀ (n : ℕ), 1 ≤ n → ContinuousOn (fun (x : ℝ) => deriv (f n) x) (Set.Icc a b)) (h_unif : TendstoUniformlyOn (fun (n : ℕ) (x : ℝ) => deriv (f n) x) g Filter.atTop (Set.Icc a b)) : ContinuousOn g (Set.Icc a b)

Helper for Theorem 3.9: g is continuous on [a,b] as a uniform limit of continuous derivatives on [a,b].

theorem helperForTheorem_3_9_abs_sub_le_interval_length {a b x x0 : ℝ} (ha : a ≤ b) (hx : x ∈ Set.Icc a b) (hx0 : x0 ∈ Set.Icc a b) : |x - x0| ≤ b - a

Helper for Theorem 3.9: any two points of [a,b] are at distance at most b - a.

theorem helperForTheorem_3_9_sub_eq_integral_deriv {a b : ℝ} (f : ℕ → ℝ → ℝ) (h_diff : ∀ (n : ℕ), 1 ≤ n → DifferentiableOn ℝ (f n) (Set.Icc a b)) (h_diff_cont : ∀ (n : ℕ), 1 ≤ n → ContinuousOn (fun (x : ℝ) => deriv (f n) x) (Set.Icc a b)) {n : ℕ} (hn : 1 ≤ n) {x0 x : ℝ} (hx0 : x0 ∈ Set.Icc a b) (hx : x ∈ Set.Icc a b) : f n x - f n x0 = ∫ (t : ℝ) in x0..x, deriv (f n) t

Helper for Theorem 3.9: for n ≥ 1, f_n x - f_n x0 is the integral of f_n' between x0 and x.

theorem helperForTheorem_3_9_integral_error_bound_on_uIcc {a b : ℝ} (ha : a ≤ b) (f : ℕ → ℝ → ℝ) (g gExt : ℝ → ℝ) {n : ℕ} {x0 x δ : ℝ} (h_gExt_eq : ∀ t ∈ Set.Icc a b, gExt t = g t) (h_bound : ∀ t ∈ Set.Icc a b, ‖deriv (f n) t - g t‖ ≤ δ) (hδ_nonneg : 0 ≤ δ) (hx0 : x0 ∈ Set.Icc a b) (hx : x ∈ Set.Icc a b) : ‖∫ (t : ℝ) in x0..x, deriv (f n) t - gExt t‖ ≤ δ * (b - a)

Helper for Theorem 3.9: uniform derivative bounds on [a,b] control the integral error term uniformly on x ∈ [a,b].

theorem helperForTheorem_3_9_dist_bound_fn_to_flim {a b : ℝ} (f : ℕ → ℝ → ℝ) (gExt : ℝ → ℝ) (h_diff : ∀ (n : ℕ), 1 ≤ n → DifferentiableOn ℝ (f n) (Set.Icc a b)) (h_diff_cont : ∀ (n : ℕ), 1 ≤ n → ContinuousOn (fun (x : ℝ) => deriv (f n) x) (Set.Icc a b)) {n : ℕ} (hn : 1 ≤ n) {x0 x l : ℝ} (hx0 : x0 ∈ Set.Icc a b) (hx : x ∈ Set.Icc a b) (h_int_gExt : IntervalIntegrable gExt MeasureTheory.volume x0 x) : dist (f n x) (l + ∫ (t : ℝ) in x0..x, gExt t) ≤ dist (f n x0) l + ‖∫ (t : ℝ) in x0..x, deriv (f n) t - gExt t‖

Helper for Theorem 3.9: the distance from f_n x to the candidate limit value is bounded by the basepoint error and an integral error term.

theorem uniformLimit_of_uniformlyConvergentDerivatives {a b : ℝ} (ha : a ≤ b) (f : ℕ → ℝ → ℝ) (g : ℝ → ℝ) (h_diff : ∀ (n : ℕ), 1 ≤ n → DifferentiableOn ℝ (f n) (Set.Icc a b)) (h_diff_cont : ∀ (n : ℕ), 1 ≤ n → ContinuousOn (fun (x : ℝ) => deriv (f n) x) (Set.Icc a b)) (h_unif : TendstoUniformlyOn (fun (n : ℕ) (x : ℝ) => deriv (f n) x) g Filter.atTop (Set.Icc a b)) (hx0 : ∃ x0 ∈ Set.Icc a b, ∃ (l : ℝ), Filter.Tendsto (fun (n : ℕ) => f n x0) Filter.atTop (nhds l)) : ∃ (f_lim : ℝ → ℝ), DifferentiableOn ℝ f_lim (Set.Icc a b) ∧ TendstoUniformlyOn f f_lim Filter.atTop (Set.Icc a b) ∧ ∀ x ∈ Set.Icc a b, deriv f_lim x = g x

Theorem 3.9: if f_n : [a,b] → ℝ are differentiable with continuous derivatives, f_n' converges uniformly to g on [a,b], and f_n(x0) converges for some x0 ∈ [a,b], then there is a differentiable f : [a,b] → ℝ with f_n → f uniformly on [a,b] and f' = g on [a,b].

noncomputable def supNormOn {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] (s : Set α) (f : α → β) : ℝ

The sup norm of a function on a set, defined as the supremum of ‖f x‖ over the set.

Equations

• supNormOn s f = sSup ((fun (x : α) => ‖f x‖) '' s)

theorem helperForTheorem_3_10_norm_deriv_le_supNormOn {a b : ℝ} (f : ℕ → ℝ → ℝ) (h_diff_cont : ∀ (n : ℕ), ContinuousOn (fun (x : ℝ) => deriv (f (n + 1)) x) (Set.Icc a b)) (n : ℕ) {x : ℝ} (hx : x ∈ Set.Icc a b) : ‖deriv (f (n + 1)) x‖ ≤ supNormOn (Set.Icc a b) fun (y : ℝ) => deriv (f (n + 1)) y

Helper for Theorem 3.10: a pointwise derivative norm on [a,b] is bounded by the corresponding sup norm.

theorem helperForTheorem_3_10_tendstoUniformlyOn_derivSeries {a b : ℝ} (f : ℕ → ℝ → ℝ) (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) : TendstoUniformlyOn (fun (N : ℕ) (x : ℝ) => ∑ n ∈ Finset.range N, deriv (f (n + 1)) x) (fun (x : ℝ) => ∑' (n : ℕ), deriv (f (n + 1)) x) Filter.atTop (Set.Icc a b)

Helper for Theorem 3.10: derivative partial sums converge uniformly on [a,b] to the termwise derivative series.

noncomputable def helperForTheorem_3_10_liftedPartialSum {a b : ℝ} (ha : a ≤ b) (f : ℕ → ℝ → ℝ) (x0 : ℝ) (N : ℕ) : ℝ → ℝ

Helper for Theorem 3.10: lifted partial sums based at x0, built from an integral of the IccExtend of derivative partial sums.

Equations

• One or more equations did not get rendered due to their size.

theorem helperForTheorem_3_10_continuous_subtype_derivPartialSum {a b : ℝ} (f : ℕ → ℝ → ℝ) (h_diff_cont : ∀ (n : ℕ), ContinuousOn (fun (x : ℝ) => deriv (f (n + 1)) x) (Set.Icc a b)) (N : ℕ) : Continuous fun (y : ↑(Set.Icc a b)) => ∑ n ∈ Finset.range N, deriv (f (n + 1)) ↑y

Helper for Theorem 3.10: continuity of the subtype derivative partial-sum map.

theorem helperForTheorem_3_10_hasDerivAt_liftedPartialSum {a b : ℝ} (ha : a ≤ b) (f : ℕ → ℝ → ℝ) (h_diff_cont : ∀ (n : ℕ), ContinuousOn (fun (x : ℝ) => deriv (f (n + 1)) x) (Set.Icc a b)) (x0 : ℝ) (N : ℕ) (x : ℝ) : HasDerivAt (helperForTheorem_3_10_liftedPartialSum ha f x0 N) (Set.IccExtend ha (fun (y : ↑(Set.Icc a b)) => ∑ n ∈ Finset.range N, deriv (f (n + 1)) ↑y) x) x

Helper for Theorem 3.10: the lifted partial sum has derivative equal to the corresponding IccExtend derivative partial sum.

theorem helperForTheorem_3_10_deriv_liftedPartialSum {a b : ℝ} (ha : a ≤ b) (f : ℕ → ℝ → ℝ) (h_diff_cont : ∀ (n : ℕ), ContinuousOn (fun (x : ℝ) => deriv (f (n + 1)) x) (Set.Icc a b)) (x0 : ℝ) (N : ℕ) (x : ℝ) : deriv (helperForTheorem_3_10_liftedPartialSum ha f x0 N) x = Set.IccExtend ha (fun (y : ↑(Set.Icc a b)) => ∑ n ∈ Finset.range N, deriv (f (n + 1)) ↑y) x

Helper for Theorem 3.10: explicit formula for the derivative of a lifted partial sum.

theorem helperForTheorem_3_10_deriv_liftedPartialSum_on_Icc {a b : ℝ} (ha : a ≤ b) (f : ℕ → ℝ → ℝ) (h_diff_cont : ∀ (n : ℕ), ContinuousOn (fun (x : ℝ) => deriv (f (n + 1)) x) (Set.Icc a b)) (x0 : ℝ) (N : ℕ) {x : ℝ} (hx : x ∈ Set.Icc a b) : deriv (helperForTheorem_3_10_liftedPartialSum ha f x0 N) x = ∑ n ∈ Finset.range N, deriv (f (n + 1)) x

Helper for Theorem 3.10: on [a,b], the derivative of the lifted partial sum equals the raw derivative partial sum.

theorem helperForTheorem_3_10_differentiableOn_liftedPartialSum {a b : ℝ} (ha : a ≤ b) (f : ℕ → ℝ → ℝ) (h_diff_cont : ∀ (n : ℕ), ContinuousOn (fun (x : ℝ) => deriv (f (n + 1)) x) (Set.Icc a b)) (x0 : ℝ) (N : ℕ) : DifferentiableOn ℝ (helperForTheorem_3_10_liftedPartialSum ha f x0 N) (Set.Icc a b)

Helper for Theorem 3.10: each lifted partial sum is differentiable on [a,b].

theorem helperForTheorem_3_10_continuousOn_deriv_liftedPartialSum {a b : ℝ} (ha : a ≤ b) (f : ℕ → ℝ → ℝ) (h_diff_cont : ∀ (n : ℕ), ContinuousOn (fun (x : ℝ) => deriv (f (n + 1)) x) (Set.Icc a b)) (x0 : ℝ) (N : ℕ) : ContinuousOn (fun (x : ℝ) => deriv (helperForTheorem_3_10_liftedPartialSum ha f x0 N) x) (Set.Icc a b)

Helper for Theorem 3.10: the derivative of each lifted partial sum is continuous on [a,b].

theorem helperForTheorem_3_10_lifted_eq_rawPartialSum_on_Icc {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)) {x0 x : ℝ} (hx0 : x0 ∈ Set.Icc a b) (hx : x ∈ Set.Icc a b) (N : ℕ) : helperForTheorem_3_10_liftedPartialSum ha f x0 N x = ∑ n ∈ Finset.range N, f (n + 1) x

Helper for Theorem 3.10: on [a,b], each lifted partial sum coincides with the corresponding raw partial sum of f.