def MetricSequence (X : Type u) : Type u

Definition 7.3.1. A sequence in a metric space (X, d) is a function x : ℕ → X, written xₙ for its terms and {xₙ} for the whole sequence. It is bounded if there exists p ∈ X and B ∈ ℝ such that dist p (xₙ) ≤ B for all n. Equivalently, the image set {xₙ : n ∈ ℕ} is bounded. A subsequence of {xₙ} is any sequence of the form {x_{n_k}} where n_{k+1} > n_k for all k.

Equations

• MetricSequence X = (ℕ → X)

def MetricBoundedSequence {X : Type u} [PseudoMetricSpace X] (x : MetricSequence X) : Prop

A sequence is bounded when all of its terms lie in a ball of finite radius around some point of the space.

Equations

• MetricBoundedSequence x = ∃ (p : X) (B : ℝ), ∀ (n : ℕ), dist p (x n) ≤ B

theorem range_subset_closedBall_of_boundedSequence {X : Type u} [PseudoMetricSpace X] (x : MetricSequence X) : MetricBoundedSequence x → ∃ (p : X) (B : ℝ), Set.range x ⊆ Metric.closedBall p B

A bounded sequence's range lies in a closed ball.

theorem metricBoundedSequence_of_isBounded_range {X : Type u} [PseudoMetricSpace X] (x : MetricSequence X) : Bornology.IsBounded (Set.range x) → MetricBoundedSequence x

A bounded range yields a pointwise distance bound for the sequence.

theorem metricBoundedSequence_iff_isBounded_range {X : Type u} [PseudoMetricSpace X] (x : MetricSequence X) : MetricBoundedSequence x ↔ Bornology.IsBounded (Set.range x)

The book's notion of a bounded sequence agrees with boundedness of its range in the bornology of the metric space.

def IsMetricSubsequence {X : Type u} (y x : MetricSequence X) : Prop

A subsequence of x is obtained by precomposing with a strictly increasing map of indices.

Equations

• IsMetricSubsequence y x = ∃ (n : ℕ → ℕ), StrictMono n ∧ ∀ (k : ℕ), y k = x (n k)

def MetricConvergesTo {X : Type u} [PseudoMetricSpace X] (x : MetricSequence X) (p : X) : Prop

Definition 7.3.2. A sequence {xₙ} in a metric space converges to a point p if for every ε > 0 there exists M ∈ ℕ such that dist (xₙ) p < ε for all n ≥ M. In this case p is a limit of the sequence.

Equations

• MetricConvergesTo x p = ∀ ε > 0, ∃ (M : ℕ), ∀ ⦃n : ℕ⦄, M ≤ n → dist (x n) p < ε

def MetricConvergentSequence {X : Type u} [PseudoMetricSpace X] (x : MetricSequence X) : Prop

A sequence is convergent when it has a (not necessarily unique) limit.

Equations

• MetricConvergentSequence x = ∃ (p : X), MetricConvergesTo x p

theorem metricConvergesTo_iff_tendsto {X : Type u} [PseudoMetricSpace X] (x : MetricSequence X) (p : X) : MetricConvergesTo x p ↔ Filter.Tendsto x Filter.atTop (nhds p)

The book's notion of convergence agrees with the usual filter convergence of sequences.

def MetricDivergentSequence {X : Type u} [PseudoMetricSpace X] (x : MetricSequence X) : Prop

A sequence is divergent when it does not converge.

Equations

• MetricDivergentSequence x = ¬MetricConvergentSequence x

theorem metricConvergentSequence_limit_unique {X : Type u} [MetricSpace X] {x : MetricSequence X} {p q : X} (hp : MetricConvergesTo x p) (hq : MetricConvergesTo x q) : p = q

Proposition 7.3.3. A convergent sequence in a metric space has a unique limit.

theorem metricConvergentSequence_bounded {X : Type u} [PseudoMetricSpace X] {x : MetricSequence X} (hx : MetricConvergentSequence x) : MetricBoundedSequence x

Proposition 7.3.4. A convergent sequence in a metric space is bounded.

theorem real_dist_eq_self_of_nonneg {r : ℝ} (hr : 0 ≤ r) : dist r 0 = r

Nonnegative reals have distance to zero equal to themselves.

theorem metricConvergesTo_dist_to_zero {X : Type u} [PseudoMetricSpace X] {x : MetricSequence X} {p : X} (hx : MetricConvergesTo x p) : MetricConvergesTo (fun (n : ℕ) => dist (x n) p) 0

Distances to a limit point converge to zero.

theorem metricConvergesTo_of_dist_le_of_tendsto {X : Type u} [PseudoMetricSpace X] {x : MetricSequence X} {p : X} {a : ℕ → ℝ} (ha : ∀ (n : ℕ), dist (x n) p ≤ a n) (hat : Filter.Tendsto a Filter.atTop (nhds 0)) : MetricConvergesTo x p

A distance bound by a sequence tending to zero forces convergence.

theorem metricConvergesTo_iff_exists_distance_bound {X : Type u} [PseudoMetricSpace X] {x : MetricSequence X} {p : X} : MetricConvergesTo x p ↔ ∃ (a : ℕ → ℝ), (∀ (n : ℕ), dist (x n) p ≤ a n) ∧ Filter.Tendsto a Filter.atTop (nhds 0)

Proposition 7.3.5. A sequence in a metric space converges to p if and only if there is a real sequence controlling the distances to p that itself tends to zero.

theorem metricConvergesTo_subsequence {X : Type u} [PseudoMetricSpace X] {x y : MetricSequence X} {p : X} (hx : MetricConvergesTo x p) (hy : IsMetricSubsequence y x) : MetricConvergesTo y p

Proposition 7.3.6. (i) A subsequence of a sequence converging to p also converges to p. (ii) If some tail of a sequence converges to p, then the original sequence converges to p.

theorem metricConvergesTo_of_tail {X : Type u} [PseudoMetricSpace X] {x : MetricSequence X} {p : X} {K : ℕ} (hx : MetricConvergesTo (fun (n : ℕ) => x (n + K.succ)) p) : MetricConvergesTo x p

theorem dist_eval_le_sup {a b : ℝ} (h k : C(↑(Set.Icc a b), ℝ)) (x : ↑(Set.Icc a b)) : dist (h x) (k x) ≤ dist h k

The distance between evaluations of two continuous functions is controlled by their supremum distance.

theorem sup_norm_le_of_pointwise {a b : ℝ} (h k : C(↑(Set.Icc a b), ℝ)) {ε : ℝ} (hε : 0 ≤ ε) (hpoint : ∀ (x : ↑(Set.Icc a b)), dist (h x) (k x) ≤ ε) : dist h k ≤ ε

A uniform pointwise bound on two continuous functions gives a bound on their supremum distance.

theorem uniformConvergence_iff_convergesInSupMetric {a b : ℝ} (f : MetricSequence C(↑(Set.Icc a b), ℝ)) (g : C(↑(Set.Icc a b), ℝ)) : (∀ ε > 0, ∃ (M : ℕ), ∀ ⦃n : ℕ⦄, M ≤ n → ∀ (x : ↑(Set.Icc a b)), dist ((f n) x) (g x) < ε) ↔ MetricConvergesTo f g

Example 7.3.7. For continuous real-valued functions on a closed interval [a, b] endowed with the uniform (supremum) norm, convergence of a sequence in the metric space sense is the same as uniform convergence.

theorem metricConvergesTo_euclidean_iff_coordinates {n : ℕ} (x : MetricSequence (EuclideanSpace ℝ (Fin n))) (l : EuclideanSpace ℝ (Fin n)) : MetricConvergesTo x l ↔ ∀ (k : Fin n), MetricConvergesTo (fun (m : ℕ) => (x m).ofLp k) (l.ofLp k)

Proposition 7.3.9. A sequence in Euclidean space ℝⁿ converges if and only if each coordinate sequence converges, and the limit vector has the coordinatewise limits.

theorem convergent_euclidean_iff_coordinates {n : ℕ} (x : MetricSequence (EuclideanSpace ℝ (Fin n))) : MetricConvergentSequence x ↔ ∀ (k : Fin n), MetricConvergentSequence fun (m : ℕ) => (x m).ofLp k

A sequence in ℝⁿ converges exactly when every coordinate sequence converges. In this case the limit is the vector of the coordinate limits.

theorem tendsto_complex_iff_real_im (z : MetricSequence ℂ) (x y : ℝ) : Filter.Tendsto z Filter.atTop (nhds (↑x + ↑y * Complex.I)) ↔ Filter.Tendsto (fun (n : ℕ) => (z n).re) Filter.atTop (nhds x) ∧ Filter.Tendsto (fun (n : ℕ) => (z n).im) Filter.atTop (nhds y)

Convergence of complex numbers is equivalent to convergence of the real and imaginary parts.

theorem metricConvergesTo_complex_iff_re_im (z : MetricSequence ℂ) (x y : ℝ) : MetricConvergesTo z (↑x + ↑y * Complex.I) ↔ MetricConvergesTo (fun (n : ℕ) => (z n).re) x ∧ MetricConvergesTo (fun (n : ℕ) => (z n).im) y

Example 7.3.10. In the complex plane viewed as ℝ², a sequence zₙ = xₙ + i yₙ converges to x + i y if and only if the real parts converge to x and the imaginary parts converge to y.

theorem metricConvergesTo_eventually_mem_open {X : Type u} [PseudoMetricSpace X] {x : MetricSequence X} {p : X} {U : Set X} (hx : MetricConvergesTo x p) (hUopen : IsOpen U) (hpU : p ∈ U) : ∃ (M : ℕ), ∀ ⦃n : ℕ⦄, M ≤ n → x n ∈ U

theorem tendsto_of_eventually_mem_open {X : Type u} [PseudoMetricSpace X] {x : MetricSequence X} {p : X} (hx : ∀ {U : Set X}, IsOpen U → p ∈ U → ∃ (M : ℕ), ∀ ⦃n : ℕ⦄, M ≤ n → x n ∈ U) : Filter.Tendsto x Filter.atTop (nhds p)

theorem metricConvergesTo_iff_eventually_mem_nhds {X : Type u} [PseudoMetricSpace X] {x : MetricSequence X} {p : X} : MetricConvergesTo x p ↔ ∀ {U : Set X}, IsOpen U → p ∈ U → ∃ (M : ℕ), ∀ ⦃n : ℕ⦄, M ≤ n → x n ∈ U

Proposition 7.3.11. A sequence in a metric space converges to p exactly when eventually all of its terms lie in every open neighborhood of p.

theorem mem_closed_of_converges {X : Type u} [PseudoMetricSpace X] {E : Set X} (hE : IsClosed E) {x : MetricSequence X} (hx : ∀ (n : ℕ), x n ∈ E) {p : X} (hxlim : MetricConvergesTo x p) : p ∈ E

Proposition 7.3.12. In a metric space, a closed set contains the limit of a convergent sequence of its points.

theorem mem_closure_iff_metricConvergesTo_seq {X : Type u} [PseudoMetricSpace X] {A : Set X} {p : X} : p ∈ closure A ↔ ∃ (x : MetricSequence X), (∀ (n : ℕ), x n ∈ A) ∧ MetricConvergesTo x p

Proposition 7.3.13. A point lies in the closure of a set in a metric space exactly when it is the limit of a sequence of points from that set.