Analysis I, Chapter 6 epilogue: Connections with Mathlib limits

In this (technical) epilogue, we show that various operations and properties we have defined for "Chapter 6" sequences Chapter6.Sequence are equivalent to Mathlib operations. Note however that Mathlib's operations are defined in far greater generality than the setting of real-valued sequences, in particular using the language of filters.

theorem Chapter6.Sequence.isCauchy_iff_isCauSeq (a : ℕ → ℝ) : (↑a).IsCauchy ↔ IsCauSeq _root_.abs a

Identification with the Cauchy sequence support in Mathlib/Algebra/Order/CauSeq/Basic

theorem Chapter6.Sequence.Cauchy_iff_CauchySeq (a : ℕ → ℝ) : (↑a).IsCauchy ↔ CauchySeq a

Identification with the Cauchy sequence support in Mathlib/Topology/UniformSpace/Cauchy

theorem Chapter6.Sequence.tendsto_iff_Tendsto (a : ℕ → ℝ) (L : ℝ) : (↑a).TendsTo L ↔ Filter.Tendsto a Filter.atTop (nhds L)

Identification with Filter.Tendsto

theorem Chapter6.Sequence.tendsto_iff_Tendsto' (a : Sequence) (L : ℝ) : a.TendsTo L ↔ Filter.Tendsto a.seq Filter.atTop (nhds L)

theorem Chapter6.Sequence.converges_iff_Tendsto (a : ℕ → ℝ) : (↑a).Convergent ↔ ∃ (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L)

theorem Chapter6.Sequence.converges_iff_Tendsto' (a : Sequence) : a.Convergent ↔ ∃ (L : ℝ), Filter.Tendsto a.seq Filter.atTop (nhds L)

instance inst_real_complete : CauSeq.IsComplete ℝ norm

A technicality: CauSeq.IsComplete ℝ was established for _root_.abs but not for norm.

theorem Chapter6.Sequence.lim_eq_CauSeq_lim (a : ℕ → ℝ) (ha : (↑a).IsCauchy) : lim ↑a = CauSeq.lim ⟨a, ⋯⟩

Identification with CauSeq.lim

theorem Chapter6.Sequence.lim_eq_limUnder (a : ℕ → ℝ) (ha : (↑a).Convergent) : lim ↑a = limUnder Filter.atTop a

Identification with limUnder

theorem Chapter6.Sequence.isBounded_iff_isBounded_range (a : ℕ → ℝ) : (↑a).IsBounded ↔ Bornology.IsBounded (Set.range a)

Identification with Bornology.IsBounded

theorem Chapter6.Sequence.sup_eq_sSup (a : ℕ → ℝ) : (↑a).sup = sSup (Set.range fun (n : ℕ) => ↑(a n))

theorem Chapter6.Sequence.inf_eq_sInf (a : ℕ → ℝ) : (↑a).inf = sInf (Set.range fun (n : ℕ) => ↑(a n))

theorem Chapter6.Sequence.bddAbove_iff (a : ℕ → ℝ) : (↑a).BddAbove ↔ _root_.BddAbove (Set.range a)

theorem Chapter6.Sequence.bddBelow_iff (a : ℕ → ℝ) : (↑a).BddBelow ↔ _root_.BddBelow (Set.range a)

theorem Chapter6.Sequence.Monotone_iff (a : ℕ → ℝ) : (↑a).IsMonotone ↔ Monotone a

theorem Chapter6.Sequence.Antitone_iff (a : ℕ → ℝ) : (↑a).IsAntitone ↔ Antitone a

theorem Chapter6.Sequence.limit_point_iff (a : ℕ → ℝ) (L : ℝ) : (↑a).LimitPoint L ↔ MapClusterPt L Filter.atTop a

Identification with MapClusterPt

theorem Chapter6.Sequence.limsup_eq (a : ℕ → ℝ) : (↑a).limsup = Filter.limsup (fun (n : ℕ) => ↑(a n)) Filter.atTop

Identification with Filter.limsup

theorem Chapter6.Sequence.liminf_eq (a : ℕ → ℝ) : (↑a).liminf = Filter.liminf (fun (n : ℕ) => ↑(a n)) Filter.atTop

Identification with Filter.liminf

theorem Chapter6.Real.rpow_eq_rpow (x α : ℝ) : rpow x α = x ^ α

Identification of rpow and Mathlib exponentiation