def pointwiseConverges {S : Type u} (f : ℕ → S → ℝ) (g : S → ℝ) : Prop

Definition 6.1.1: A sequence of functions fₙ : S → ℝ converges pointwise to f : S → ℝ if for every x ∈ S, the real sequence fₙ x converges to f x (this is the default meaning of "converges" for sequences of functions unless specified otherwise).

Equations

• pointwiseConverges f g = ∀ (x : S), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))

theorem pointwiseConverges_iff_abs_sub_lt {S : Type u} (f : ℕ → S → ℝ) (g : S → ℝ) : pointwiseConverges f g ↔ ∀ (x : S), ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |f n x - g x| < ε

Proposition 6.1.5: A sequence of functions fₙ : S → ℝ converges pointwise to f : S → ℝ if and only if for every x ∈ S and every ε > 0 there exists N such that |fₙ x - f x| < ε for all n ≥ N.

theorem pointwiseConverges_pow_even (x : ℝ) : x ∈ Set.Icc (-1) 1 → Filter.Tendsto (fun (n : ℕ) => x ^ (2 * n)) Filter.atTop (nhds (if x = 1 ∨ x = -1 then 1 else 0))

Example 6.1.2: On [-1,1], the sequence fₙ x := x^(2 n) converges pointwise to the function that is 1 at x = -1 and x = 1, and 0 everywhere else in the closed interval. Outside [-1,1] the powers x^(2 n) do not converge.

theorem tendsto_partialSums_geometric_of_abs_lt_one (x : ℝ) : x ∈ Set.Ioo (-1) 1 → Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), x ^ k) Filter.atTop (nhds (1 / (1 - x)))

Example 6.1.3: For x ∈ (-1, 1) the partial sums of the geometric series fₙ(x) = \sum_{k=0}^n x^k converge to 1 / (1 - x), so the function \sum_{k=0}^\infty x^k is defined on (-1, 1) as this limit.

theorem tendsto_sin_nat_mul_zero : Filter.Tendsto (fun (n : ℕ) => Real.sin (↑n * 0)) Filter.atTop (nhds 0)

Example 6.1.4: The sequence of functions fₙ(x) = \sin (n x) does not converge pointwise to any function on any interval, even though it converges at isolated points such as x = 0 or x = π.

theorem tendsto_sin_nat_mul_pi : Filter.Tendsto (fun (n : ℕ) => Real.sin (↑n * Real.pi)) Filter.atTop (nhds 0)

A concrete convergent point for fₙ(x) = \sin (n x) is x = π, where the sequence is constantly zero.

theorem exists_irrational_div_two_pi_in_Icc {a b : ℝ} (h : a < b) : ∃ x ∈ Set.Icc a b, Irrational (x / (2 * Real.pi))

In any nontrivial interval, we can choose x with x / (2π) irrational.

theorem not_tendsto_sin_nat_mul_of_irrational {x : ℝ} (hx : Irrational (x / (2 * Real.pi))) : ¬∃ (l : ℝ), Filter.Tendsto (fun (n : ℕ) => Real.sin (↑n * x)) Filter.atTop (nhds l)

theorem exists_nonconvergent_sin_nat_mul (a b : ℝ) (h : a < b) : ∃ x ∈ Set.Icc a b, ¬∃ (l : ℝ), Filter.Tendsto (fun (n : ℕ) => Real.sin (↑n * x)) Filter.atTop (nhds l)

For any interval [a, b] there is a point where the sequence fₙ(x) = \sin (n x) fails to converge.

def uniformConverges {S : Type u} (f : ℕ → S → ℝ) (g : S → ℝ) : Prop

Definition 6.1.6: A sequence of functions fₙ : S → ℝ converges uniformly to f : S → ℝ if for every ε > 0 there exists N such that for all n ≥ N and all x ∈ S, we have |fₙ x - f x| < ε.

Equations

• uniformConverges f g = ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∀ (x : S), |f n x - g x| < ε

theorem uniformConverges.pointwiseConverges {S : Type u} (f : ℕ → S → ℝ) (g : S → ℝ) (h : uniformConverges f g) : _root_.pointwiseConverges f g

Proposition 6.1.7: If a sequence of functions fₙ : S → ℝ converges uniformly to f : S → ℝ, then it converges pointwise to f.

theorem exists_x_pow_even_ge_half (N : ℕ) : ∃ x ∈ Set.Ioo (-1) 1, x ^ (2 * N) > 1 / 2

Helper for Example 6.1.8: for any N there is x ∈ (-1,1) with x^(2N) > 1/2.

theorem not_uniformConverges_pow_even_on_unit_interval : ¬uniformConverges (fun (n : ℕ) (x : { x : ℝ // x ∈ Set.Icc (-1) 1 }) => ↑x ^ (2 * n)) fun (x : { x : ℝ // x ∈ Set.Icc (-1) 1 }) => if ↑x = 1 ∨ ↑x = -1 then 1 else 0

Example 6.1.8: The sequence of even powers fₙ(x) = x^(2 n) converges pointwise on [-1,1] to the function that is 1 at the endpoints and 0 elsewhere, but this convergence is not uniform on the whole interval.

theorem uniformConverges_pow_even_on_subinterval {a : ℝ} (ha_pos : 0 < a) (ha_lt_one : a < 1) : uniformConverges (fun (n : ℕ) (x : { x : ℝ // x ∈ Set.Icc (-a) a }) => ↑x ^ (2 * n)) fun (x : { x : ℝ // x ∈ Set.Icc (-a) a }) => 0

Example 6.1.8 (continued): If we restrict to [-a, a] with 0 < a < 1, then the even powers fₙ(x) = x^(2 n) converge uniformly to 0 on that smaller interval.

noncomputable def uniformNormOn {S : Type u} (A : Set S) (f : S → ℝ) : ℝ

Definition 6.1.9: For a bounded function f : S → ℝ, the uniform norm is the supremum of the absolute value of f over the set S; this coincides with the usual sup (or infinity) norm.

Equations

• uniformNormOn A f = sSup ((fun (x : S) => |f x|) '' A)

theorem uniformConverges_iff_uniformNormOn_tendsto_zero {S : Type u} (f : ℕ → S → ℝ) (g : S → ℝ) (hbounded : ∀ (n : ℕ), BddAbove ((fun (x : S) => |f n x - g x|) '' Set.univ)) : uniformConverges f g ↔ Filter.Tendsto (fun (n : ℕ) => uniformNormOn Set.univ fun (x : S) => f n x - g x) Filter.atTop (nhds 0)

Proposition 6.1.10: A sequence of bounded functions fₙ : S → ℝ converges uniformly to f : S → ℝ if and only if the uniform norms of the difference fₙ - f converge to 0.

theorem uniformConverges_nat_mul_add_sin_div_nat : uniformConverges (fun (n : ℕ) (x : { x : ℝ // x ∈ Set.Icc 0 1 }) => (↑n.succ * ↑x + Real.sin (↑n.succ * ↑x ^ 2)) / ↑n.succ) fun (x : { x : ℝ // x ∈ Set.Icc 0 1 }) => ↑x

Example 6.1.11: For fₙ(x) = (n x + \sin (n x^2)) / n on [0,1], the sequence converges uniformly to the identity function x ↦ x.

def uniformlyCauchy {S : Type u} (f : ℕ → S → ℝ) : Prop

Definition 6.1.12: A sequence of bounded functions fₙ : S → ℝ is uniformly Cauchy (Cauchy in the uniform norm) if for every ε > 0 there exists N such that for all m, k ≥ N, the uniform norm of fₘ - fₖ on S is less than ε.

Equations

• uniformlyCauchy f = ∀ ε > 0, ∃ (N : ℕ), ∀ m ≥ N, ∀ k ≥ N, (uniformNormOn Set.univ fun (x : S) => f m x - f k x) < ε

theorem uniformlyCauchy_iff_exists_uniformLimit {S : Type u} (f : ℕ → S → ℝ) (hbounded : ∀ (n : ℕ), BddAbove ((fun (x : S) => |f n x|) '' Set.univ)) : uniformlyCauchy f ↔ ∃ (g : S → ℝ), uniformConverges f g

Proposition 6.1.13: For bounded functions fₙ : S → ℝ, the sequence is uniformly Cauchy (Cauchy in the uniform norm) if and only if there exists a function f : S → ℝ such that fₙ converges uniformly to f.