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 : TypeChapter6.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.

open Filter

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

theorem Chapter6.Sequence.isCauchy_iff_isCauSeq (a: ℕ → ℝ) :
    (a:Sequence).IsCauchy ↔ IsCauSeq _root_.abs a := bya:ℕ → ℝ⊢ (↑a).IsCauchy ↔ IsCauSeq _root_.abs a
  simp_rw [IsCauchy.coe, Real.dist_eq, IsCauSeq]a:ℕ → ℝ⊢ (∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε) ↔ ∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < ε
  constructormpa:ℕ → ℝ⊢ (∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε) → ∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < εmpra:ℕ → ℝ⊢ (∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < ε) → ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε <;>mpa:ℕ → ℝ⊢ (∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε) → ∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < εmpra:ℕ → ℝ⊢ (∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < ε) → ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε intro h ε hεmpra:ℕ → ℝh:∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < εε:ℝhε:ε > 0⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε <;>mpa:ℕ → ℝh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ εε:ℝhε:ε > 0⊢ ∃ i, ∀ j ≥ i, |a j - a i| < εmpra:ℕ → ℝh:∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < εε:ℝhε:ε > 0⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε have ⟨ N, h ⟩ := h _ (half_pos hε)mpra:ℕ → ℝh✝:∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < εε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε <;>mpa:ℕ → ℝh✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ εε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε / 2⊢ ∃ i, ∀ j ≥ i, |a j - a i| < εmpra:ℕ → ℝh✝:∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < εε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε use Nha:ℕ → ℝh✝:∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < εε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2⊢ ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε
  .ha:ℕ → ℝh✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ εε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε / 2⊢ ∀ j ≥ N, |a j - a N| < ε intro n hnha:ℕ → ℝh✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ εε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε / 2n:ℕhn:n ≥ N⊢ |a n - a N| < ε; linarith [h n hn N (bya:ℕ → ℝh✝:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ εε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, ∀ k ≥ N, |a j - a k| ≤ ε / 2n:ℕhn:n ≥ N⊢ N ≥ N rflAll goals completed! 🐙)]
  intro n hn m hmha:ℕ → ℝh✝:∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < εε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2n:ℕhn:n ≥ Nm:ℕhm:m ≥ N⊢ |a n - a m| ≤ ε
  calc
    _ ≤ |a n - a N| + |a m - a N| := bya:ℕ → ℝh✝:∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < εε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2n:ℕhn:n ≥ Nm:ℕhm:m ≥ N⊢ |a n - a m| ≤ |a n - a N| + |a m - a N| grind [abs_sub_comm, abs_sub_le]All goals completed! 🐙
    _ ≤ ε/2 + ε/2 := bya:ℕ → ℝh✝:∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < εε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2n:ℕhn:n ≥ Nm:ℕhm:m ≥ N⊢ |a n - a N| + |a m - a N| ≤ ε / 2 + ε / 2 grindAll goals completed! 🐙
    _ = _ := bya:ℕ → ℝh✝:∀ ε > 0, ∃ i, ∀ j ≥ i, |a j - a i| < εε:ℝhε:ε > 0N:ℕh:∀ j ≥ N, |a j - a N| < ε / 2n:ℕhn:n ≥ Nm:ℕhm:m ≥ N⊢ ε / 2 + ε / 2 = ε linarithAll goals completed! 🐙

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

theorem Chapter6.Sequence.Cauchy_iff_CauchySeq (a: ℕ → ℝ) :
    (a:Sequence).IsCauchy ↔ CauchySeq a := bya:ℕ → ℝ⊢ (↑a).IsCauchy ↔ CauchySeq a
  rw [isCauchy_iff_isCauSeq]a:ℕ → ℝ⊢ IsCauSeq _root_.abs a ↔ CauchySeq a
  convert isCauSeq_iff_cauchySeqAll goals completed! 🐙

Identification with Filter.Tendsto.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ : Filter α) (l₂ : Filter β) : PropFilter.Tendsto

theorem Chapter6.Sequence.tendsto_iff_Tendsto (a: ℕ → ℝ) (L:ℝ) :
    (a:Sequence).TendsTo L ↔ atTop.Tendsto a (nhds L) := bya:ℕ → ℝL:ℝ⊢ (↑a).TendsTo L ↔ Tendsto a atTop (nhds L)
  rw [Metric.tendsto_atTop, tendsTo_iff]a:ℕ → ℝL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, |(↑a).seq n - L| ≤ ε) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a n) L < ε
  constructormpa:ℕ → ℝL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, |(↑a).seq n - L| ≤ ε) → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a n) L < εmpra:ℕ → ℝL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a n) L < ε) → ∀ ε > 0, ∃ N, ∀ n ≥ N, |(↑a).seq n - L| ≤ ε <;>mpa:ℕ → ℝL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, |(↑a).seq n - L| ≤ ε) → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a n) L < εmpra:ℕ → ℝL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a n) L < ε) → ∀ ε > 0, ∃ N, ∀ n ≥ N, |(↑a).seq n - L| ≤ ε intro h ε hεmpra:ℕ → ℝL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a n) L < εε:ℝhε:ε > 0⊢ ∃ N, ∀ n ≥ N, |(↑a).seq n - L| ≤ ε
  .mpa:ℕ → ℝL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, |(↑a).seq n - L| ≤ εε:ℝhε:ε > 0⊢ ∃ N, ∀ n ≥ N, dist (a n) L < ε have ⟨ N, hN ⟩ := h _ (half_pos hε)mpa:ℕ → ℝL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, |(↑a).seq n - L| ≤ εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, |(↑a).seq n - L| ≤ ε / 2⊢ ∃ N, ∀ n ≥ N, dist (a n) L < ε; use N.toNatha:ℕ → ℝL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, |(↑a).seq n - L| ≤ εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, |(↑a).seq n - L| ≤ ε / 2⊢ ∀ n ≥ N.toNat, dist (a n) L < ε; intro n hnha:ℕ → ℝL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, |(↑a).seq n - L| ≤ εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, |(↑a).seq n - L| ≤ ε / 2n:ℕhn:n ≥ N.toNat⊢ dist (a n) L < ε
    specialize hN n (Int.toNat_le.mp hn)ha:ℕ → ℝL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, |(↑a).seq n - L| ≤ εε:ℝhε:ε > 0N:ℤn:ℕhn:n ≥ N.toNathN:|(↑a).seq ↑n - L| ≤ ε / 2⊢ dist (a n) L < ε; simp at hNha:ℕ → ℝL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, |(↑a).seq n - L| ≤ εε:ℝhε:ε > 0N:ℤn:ℕhn:n ≥ N.toNathN:|a n - L| ≤ ε / 2⊢ dist (a n) L < ε
    rw [Real.dist_eq]ha:ℕ → ℝL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, |(↑a).seq n - L| ≤ εε:ℝhε:ε > 0N:ℤn:ℕhn:n ≥ N.toNathN:|a n - L| ≤ ε / 2⊢ |a n - L| < ε; linarithAll goals completed! 🐙
  have ⟨ N, hN ⟩ := h ε hεmpra:ℕ → ℝL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a n) L < εε:ℝhε:ε > 0N:ℕhN:∀ n ≥ N, dist (a n) L < ε⊢ ∃ N, ∀ n ≥ N, |(↑a).seq n - L| ≤ ε; use Nha:ℕ → ℝL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a n) L < εε:ℝhε:ε > 0N:ℕhN:∀ n ≥ N, dist (a n) L < ε⊢ ∀ n ≥ ↑N, |(↑a).seq n - L| ≤ ε; intro n hnha:ℕ → ℝL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a n) L < εε:ℝhε:ε > 0N:ℕhN:∀ n ≥ N, dist (a n) L < εn:ℤhn:n ≥ ↑N⊢ |(↑a).seq n - L| ≤ ε
  have hpos : n ≥ 0 := bya:ℕ → ℝL:ℝ⊢ (↑a).TendsTo L ↔ Tendsto a atTop (nhds L) grindAll goals completed! 🐙
  rw [ge_iff_le, ←Int.le_toNat hpos] at hnha:ℕ → ℝL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a n) L < εε:ℝhε:ε > 0N:ℕhN:∀ n ≥ N, dist (a n) L < εn:ℤhn:N ≤ n.toNathpos:n ≥ 0⊢ |(↑a).seq n - L| ≤ ε
  simp [hpos, ←Real.dist_eq, le_of_lt (hN n.toNat hn)]All goals completed! 🐙

theorem Chapter6.Sequence.tendsto_iff_Tendsto' (a: Sequence) (L:ℝ) : a.TendsTo L ↔ atTop.Tendsto a.seq (nhds L) := bya:SequenceL:ℝ⊢ a.TendsTo L ↔ Tendsto a.seq atTop (nhds L)
  rw [Metric.tendsto_atTop, tendsTo_iff]a:SequenceL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a.seq n) L < ε
  constructormpa:SequenceL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε) → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a.seq n) L < εmpra:SequenceL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a.seq n) L < ε) → ∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε <;>mpa:SequenceL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε) → ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a.seq n) L < εmpra:SequenceL:ℝ⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a.seq n) L < ε) → ∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε intro h ε hεmpra:SequenceL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a.seq n) L < εε:ℝhε:ε > 0⊢ ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε
  .mpa:SequenceL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ εε:ℝhε:ε > 0⊢ ∃ N, ∀ n ≥ N, dist (a.seq n) L < ε have ⟨ N, hN ⟩ := h _ (half_pos hε)mpa:SequenceL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ ε / 2⊢ ∃ N, ∀ n ≥ N, dist (a.seq n) L < ε; use Nha:SequenceL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ ε / 2⊢ ∀ n ≥ N, dist (a.seq n) L < ε; peel 2 hNh.h.ha:SequenceL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ ε / 2n✝:ℤa✝:n✝ ≥ Nthis:|a.seq n✝ - L| ≤ ε / 2⊢ dist (a.seq n✝) L < ε; rw [Real.dist_eq]h.h.ha:SequenceL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, |a.seq n - L| ≤ ε / 2n✝:ℤa✝:n✝ ≥ Nthis:|a.seq n✝ - L| ≤ ε / 2⊢ |a.seq n✝ - L| < ε; linarithAll goals completed! 🐙
  have ⟨ N, hN ⟩ := h _ hεmpra:SequenceL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a.seq n) L < εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, dist (a.seq n) L < ε⊢ ∃ N, ∀ n ≥ N, |a.seq n - L| ≤ ε; use Nha:SequenceL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a.seq n) L < εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, dist (a.seq n) L < ε⊢ ∀ n ≥ N, |a.seq n - L| ≤ ε; peel 2 hNh.h.ha:SequenceL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a.seq n) L < εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, dist (a.seq n) L < εn✝:ℤa✝:n✝ ≥ Nthis:dist (a.seq n✝) L < ε⊢ |a.seq n✝ - L| ≤ ε; rw [←Real.dist_eq]h.h.ha:SequenceL:ℝh:∀ ε > 0, ∃ N, ∀ n ≥ N, dist (a.seq n) L < εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, dist (a.seq n) L < εn✝:ℤa✝:n✝ ≥ Nthis:dist (a.seq n✝) L < ε⊢ dist (a.seq n✝) L ≤ ε; linarithAll goals completed! 🐙

theorem Chapter6.Sequence.converges_iff_Tendsto (a: ℕ → ℝ) :
    (a:Sequence).Convergent ↔ ∃ L, atTop.Tendsto a (nhds L) := bya:ℕ → ℝ⊢ (↑a).Convergent ↔ ∃ L, Tendsto a atTop (nhds L) simp_rw [←tendsto_iff_Tendsto]All goals completed! 🐙

theorem Chapter6.Sequence.converges_iff_Tendsto' (a: Sequence) :
    a.Convergent ↔ ∃ L, atTop.Tendsto a.seq (nhds L) := bya:Sequence⊢ a.Convergent ↔ ∃ L, Tendsto a.seq atTop (nhds L) simp_rw [←tendsto_iff_Tendsto']All goals completed! 🐙

A technicality: CauSeq.IsComplete ℝ : (abv : ℝ → ?m.1) → [IsAbsoluteValue abv] → PropCauSeq.IsComplete ℝ was established for abs.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α_root_.abs but not for Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝnorm.

instance inst_real_complete : CauSeq.IsComplete ℝ norm := by⊢ CauSeq.IsComplete ℝ norm convert Real.instIsCompleteAbsAll goals completed! 🐙

Identification with CauSeq.lim.{u_1, u_2} {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] [CauSeq.IsComplete β abv] (s : CauSeq β abv) : βCauSeq.lim

theorem Chapter6.Sequence.lim_eq_CauSeq_lim (a:ℕ → ℝ) (ha: (a:Sequence).IsCauchy) :
    Chapter6.lim (a:Sequence) = CauSeq.lim  ⟨ a, (isCauchy_iff_isCauSeq a).mp ha⟩ := bya:ℕ → ℝha:(↑a).IsCauchy⊢ lim ↑a = CauSeq.lim ⟨a, ⋯⟩
  have h1 := CauSeq.tendsto_limit ⟨ a, (isCauchy_iff_isCauSeq a).mp ha⟩a:ℕ → ℝha:(↑a).IsCauchyh1:?_mvar.37089 := CauSeq.tendsto_limit ⟨_fvar.37083, (Chapter6.Sequence.isCauchy_iff_isCauSeq _fvar.37083).mp _fvar.37084⟩⊢ lim ↑a = CauSeq.lim ⟨a, ⋯⟩
  have h2 := lim_def ((a:Sequence).Cauchy_iff_convergent.mp ha)a:ℕ → ℝha:(↑a).IsCauchyh1:?_mvar.37089 := CauSeq.tendsto_limit ⟨_fvar.37083, (Chapter6.Sequence.isCauchy_iff_isCauSeq _fvar.37083).mp _fvar.37084⟩h2:?_mvar.37497 := Chapter6.Sequence.lim_def ((Chapter6.Sequence.Cauchy_iff_convergent ↑_fvar.37083).mp _fvar.37084)⊢ lim ↑a = CauSeq.lim ⟨a, ⋯⟩
  rw [←tendsto_iff_Tendsto] at h1a:ℕ → ℝha:(↑a).IsCauchyh1:(↑↑⟨a, ⋯⟩).TendsTo (CauSeq.lim ⟨a, ⋯⟩)h2:(↑a).TendsTo (lim ↑a)⊢ lim ↑a = CauSeq.lim ⟨a, ⋯⟩
  by_contra! ha:ℕ → ℝha:(↑a).IsCauchyh1:(↑↑⟨a, ⋯⟩).TendsTo (CauSeq.lim ⟨a, ⋯⟩)h2:(↑a).TendsTo (lim ↑a)h:lim ↑a ≠ CauSeq.lim ⟨a, ⋯⟩⊢ False; apply (a:Sequence).tendsTo_unique at ha:ℕ → ℝha:(↑a).IsCauchyh1:(↑↑⟨a, ⋯⟩).TendsTo (CauSeq.lim ⟨a, ⋯⟩)h2:(↑a).TendsTo (lim ↑a)h:¬((↑a).TendsTo (lim ↑a) ∧ (↑a).TendsTo (CauSeq.lim ⟨a, ⋯⟩))⊢ False; tautoAll goals completed! 🐙

Identification with limUnder.{u_1, u_3} {X : Type u_1} [TopologicalSpace X] {α : Type u_3} [Nonempty X] (f : Filter α) (g : α → X) : XlimUnder

theorem declaration uses 'sorry'Chapter6.Sequence.lim_eq_limUnder (a:ℕ → ℝ) (ha: (a:Sequence).Convergent) :
    Chapter6.lim (a:Sequence) = limUnder Filter.atTop a := bya:ℕ → ℝha:(↑a).Convergent⊢ lim ↑a = limUnder atTop a
    sorryAll goals completed! 🐙

Identification with Bornology.IsBounded.{u_2} {α : Type u_2} [Bornology α] (s : Set α) : PropBornology.IsBounded

theorem Chapter6.Sequence.isBounded_iff_isBounded_range (a:ℕ → ℝ):
    (a:Sequence).IsBounded ↔ Bornology.IsBounded (Set.range a) := bya:ℕ → ℝ⊢ (↑a).IsBounded ↔ Bornology.IsBounded (Set.range a)
  simp [isBounded_def, boundedBy_def, Metric.isBounded_iff]a:ℕ → ℝ⊢ (∃ M, 0 ≤ M ∧ ∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M) ↔ ∃ C, ∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ C
  constructormpa:ℕ → ℝ⊢ (∃ M, 0 ≤ M ∧ ∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M) → ∃ C, ∀ (a_2 a_3 : ℕ), dist (a a_2) (a a_3) ≤ Cmpra:ℕ → ℝ⊢ (∃ C, ∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ C) → ∃ M, 0 ≤ M ∧ ∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M
  .mpa:ℕ → ℝ⊢ (∃ M, 0 ≤ M ∧ ∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M) → ∃ C, ∀ (a_2 a_3 : ℕ), dist (a a_2) (a a_3) ≤ C intro ⟨ M, hM, h ⟩mpa:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M⊢ ∃ C, ∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ C; use 2*Mha:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M⊢ ∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ 2 * M; intro n mha:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ Mn:ℕm:ℕ⊢ dist (a n) (a m) ≤ 2 * M
    calc
      _ = |a n - a m| := Real.dist_eq _ _
      _ ≤ |a n| + |a m| := abs_sub _ _
      _ ≤ M + M := bya:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ Mn:ℕm:ℕ⊢ |a n| + |a m| ≤ M + M gcongrh₁a:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ Mn:ℕm:ℕ⊢ |a n| ≤ Mh₂a:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ Mn:ℕm:ℕ⊢ |a m| ≤ M; convert h nh₂a:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ Mn:ℕm:ℕ⊢ |a m| ≤ M; convert h mAll goals completed! 🐙
      _ = _ := bya:ℕ → ℝM:ℝhM:0 ≤ Mh:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ Mn:ℕm:ℕ⊢ M + M = 2 * M ringAll goals completed! 🐙
  intro ⟨ C, h ⟩mpra:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ C⊢ ∃ M, 0 ≤ M ∧ ∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ M
  have : C ≥ 0 := bya:ℕ → ℝ⊢ (↑a).IsBounded ↔ Bornology.IsBounded (Set.range a) specialize h 0 0a:ℕ → ℝC:ℝh:dist (a 0) (a 0) ≤ C⊢ C ≥ 0; simpa using hAll goals completed! 🐙
  refine ⟨ C + |a 0|, bya:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:_fvar.61970 ≥ 0 := 
  Eq.mpr (id ge_iff_le._simp_1)
    (Eq.mp (congrArg (fun x => x ≤ _fvar.61970) (dist_self (@_fvar.40435 0))) (@_fvar.61971 0 0))⊢ 0 ≤ C + |a 0| positivityAll goals completed! 🐙, ?_ ⟩
  intro nmpra:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:_fvar.61970 ≥ 0 := ?_mvar.62136n:ℤ⊢ |if 0 ≤ n then a n.toNat else 0| ≤ C + |a 0|; by_cases hn: n ≥ 0pos._@._hyg.2080a:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:_fvar.61970 ≥ 0 := ?_mvar.62136n:ℤhn:n ≥ 0⊢ |if 0 ≤ n then a n.toNat else 0| ≤ C + |a 0|neg._@._hyg.2080a:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:_fvar.61970 ≥ 0 := ?_mvar.62136n:ℤhn:¬n ≥ 0⊢ |if 0 ≤ n then a n.toNat else 0| ≤ C + |a 0| <;>pos._@._hyg.2080a:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:_fvar.61970 ≥ 0 := ?_mvar.62136n:ℤhn:n ≥ 0⊢ |if 0 ≤ n then a n.toNat else 0| ≤ C + |a 0|neg._@._hyg.2080a:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:_fvar.61970 ≥ 0 := ?_mvar.62136n:ℤhn:¬n ≥ 0⊢ |if 0 ≤ n then a n.toNat else 0| ≤ C + |a 0| simp [hn]neg._@._hyg.2080a:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:_fvar.61970 ≥ 0 := ?_mvar.62136n:ℤhn:¬n ≥ 0⊢ 0 ≤ C + |a 0|
  .pos._@._hyg.2080a:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:_fvar.61970 ≥ 0 := ?_mvar.62136n:ℤhn:n ≥ 0⊢ |a n.toNat| ≤ C + |a 0| calc
      _ ≤ |a n.toNat - a 0| + |a 0| := bya:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:_fvar.61970 ≥ 0 := 
  Eq.mpr (id ge_iff_le._simp_1)
    (Eq.mp (congrArg (fun x => x ≤ _fvar.61970) (dist_self (@_fvar.40435 0))) (@_fvar.61971 0 0))n:ℤhn:n ≥ 0⊢ |a n.toNat| ≤ |a n.toNat - a 0| + |a 0| convert abs_add_le _ _h.e'_3.h.e'_4a:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:_fvar.61970 ≥ 0 := 
  Eq.mpr (id ge_iff_le._simp_1)
    (Eq.mp (congrArg (fun x => x ≤ _fvar.61970) (dist_self (@_fvar.40435 0))) (@_fvar.61971 0 0))n:ℤhn:n ≥ 0⊢ a n.toNat = a n.toNat - a 0 + a 0convert_4a:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:_fvar.61970 ≥ 0 := 
  Eq.mpr (id ge_iff_le._simp_1)
    (Eq.mp (congrArg (fun x => x ≤ _fvar.61970) (dist_self (@_fvar.40435 0))) (@_fvar.61971 0 0))n:ℤhn:n ≥ 0⊢ AddLeftMono ℝ; abelconvert_4a:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:_fvar.61970 ≥ 0 := 
  Eq.mpr (id ge_iff_le._simp_1)
    (Eq.mp (congrArg (fun x => x ≤ _fvar.61970) (dist_self (@_fvar.40435 0))) (@_fvar.61971 0 0))n:ℤhn:n ≥ 0⊢ AddLeftMono ℝ; infer_instanceAll goals completed! 🐙
      _ ≤ C + |a 0| := bya:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:_fvar.61970 ≥ 0 := 
  Eq.mpr (id ge_iff_le._simp_1)
    (Eq.mp (congrArg (fun x => x ≤ _fvar.61970) (dist_self (@_fvar.40435 0))) (@_fvar.61971 0 0))n:ℤhn:n ≥ 0⊢ |a n.toNat - a 0| + |a 0| ≤ C + |a 0| gcongrbca:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:_fvar.61970 ≥ 0 := 
  Eq.mpr (id ge_iff_le._simp_1)
    (Eq.mp (congrArg (fun x => x ≤ _fvar.61970) (dist_self (@_fvar.40435 0))) (@_fvar.61971 0 0))n:ℤhn:n ≥ 0⊢ |a n.toNat - a 0| ≤ C; rw [←Real.dist_eq]bca:ℕ → ℝC:ℝh:∀ (a_1 a_2 : ℕ), dist (a a_1) (a a_2) ≤ Cthis:_fvar.61970 ≥ 0 := 
  Eq.mpr (id ge_iff_le._simp_1)
    (Eq.mp (congrArg (fun x => x ≤ _fvar.61970) (dist_self (@_fvar.40435 0))) (@_fvar.61971 0 0))n:ℤhn:n ≥ 0⊢ dist (a n.toNat) (a 0) ≤ C; convert h n.toNat 0All goals completed! 🐙
  positivityAll goals completed! 🐙

theorem declaration uses 'sorry'Chapter6.Sequence.sup_eq_sSup (a:ℕ → ℝ):
    (a:Sequence).sup = sSup (Set.range (fun n ↦ (a n:EReal))) := bya:ℕ → ℝ⊢ (↑a).sup = sSup (Set.range fun n => ↑(a n)) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Chapter6.Sequence.inf_eq_sInf (a:ℕ → ℝ):
    (a:Sequence).inf = sInf (Set.range (fun n ↦ (a n:EReal))) := bya:ℕ → ℝ⊢ (↑a).inf = sInf (Set.range fun n => ↑(a n)) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Chapter6.Sequence.bddAbove_iff (a:ℕ → ℝ):
    (a:Sequence).BddAbove ↔ _root_.BddAbove (Set.range a) := bya:ℕ → ℝ⊢ (↑a).BddAbove ↔ _root_.BddAbove (Set.range a) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Chapter6.Sequence.bddBelow_iff (a:ℕ → ℝ):
    (a:Sequence).BddBelow ↔ _root_.BddBelow (Set.range a) := bya:ℕ → ℝ⊢ (↑a).BddBelow ↔ _root_.BddBelow (Set.range a) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Chapter6.Sequence.Monotone_iff (a:ℕ → ℝ): (a:Sequence).IsMonotone ↔ Monotone a := bya:ℕ → ℝ⊢ (↑a).IsMonotone ↔ Monotone a sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Chapter6.Sequence.Antitone_iff (a:ℕ → ℝ): (a:Sequence).IsAntitone ↔ Antitone a := bya:ℕ → ℝ⊢ (↑a).IsAntitone ↔ Antitone a sorryAll goals completed! 🐙

Identification with MapClusterPt.{u_1, u_3} {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} (x : X) (F : Filter ι) (u : ι → X) : PropMapClusterPt

theorem Chapter6.Sequence.limit_point_iff (a:ℕ → ℝ) (L:ℝ) :
    (a:Sequence).LimitPoint L ↔ MapClusterPt L .atTop a := bya:ℕ → ℝL:ℝ⊢ (↑a).LimitPoint L ↔ MapClusterPt L atTop a
  simp_rw [limit_point_def, mapClusterPt_iff_frequently, frequently_atTop, Metric.mem_nhds_iff]a:ℕ → ℝL:ℝ⊢ (∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε) ↔
  ∀ (s : Set ℝ), (∃ ε > 0, Metric.ball L ε ⊆ s) → ∀ (a_2 : ℕ), ∃ b ≥ a_2, a b ∈ s
  constructormpa:ℕ → ℝL:ℝ⊢ (∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε) →
  ∀ (s : Set ℝ), (∃ ε > 0, Metric.ball L ε ⊆ s) → ∀ (a_3 : ℕ), ∃ b ≥ a_3, a b ∈ smpra:ℕ → ℝL:ℝ⊢ (∀ (s : Set ℝ), (∃ ε > 0, Metric.ball L ε ⊆ s) → ∀ (a_2 : ℕ), ∃ b ≥ a_2, a b ∈ s) →
  ∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε
  .mpa:ℕ → ℝL:ℝ⊢ (∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε) →
  ∀ (s : Set ℝ), (∃ ε > 0, Metric.ball L ε ⊆ s) → ∀ (a_3 : ℕ), ∃ b ≥ a_3, a b ∈ s intro h s ⟨ ε, hε, hεs ⟩ Nmpa:ℕ → ℝL:ℝh:∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ εs:Set ℝε:ℝhε:ε > 0hεs:Metric.ball L ε ⊆ sN:ℕ⊢ ∃ b ≥ N, a b ∈ s
    have ⟨ n, hn1, hn2 ⟩ := h _ (half_pos hε) N (bya:ℕ → ℝL:ℝh:∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ εs:Set ℝε:ℝhε:ε > 0hεs:Metric.ball L ε ⊆ sN:ℕ⊢ ↑N ≥ 0 positivityAll goals completed! 🐙)
    have hn : n ≥ 0 := bya:ℕ → ℝL:ℝ⊢ (↑a).LimitPoint L ↔ MapClusterPt L atTop a grindAll goals completed! 🐙
    refine ⟨ n.toNat, bya:ℕ → ℝL:ℝh:∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ εs:Set ℝε:ℝhε:ε > 0hεs:Metric.ball L ε ⊆ sN:ℕn:ℤhn1:n ≥ ↑Nhn2:|(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε / 2hn:_fvar.87001 ≥ 0 := 
  Chapter6.Sequence.limit_point_iff._proof_5 _fvar.84983 _fvar.84984 _fvar.86552 _fvar.86555 _fvar.86606 _fvar.86607
    _fvar.86608 _fvar.86702 _fvar.87001 _fvar.87002 _fvar.87003⊢ n.toNat ≥ N rwa [ge_iff_le, Int.le_toNat hn]a:ℕ → ℝL:ℝh:∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ εs:Set ℝε:ℝhε:ε > 0hεs:Metric.ball L ε ⊆ sN:ℕn:ℤhn1:n ≥ ↑Nhn2:|(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε / 2hn:_fvar.87001 ≥ 0 := 
  Chapter6.Sequence.limit_point_iff._proof_5 _fvar.84983 _fvar.84984 _fvar.86552 _fvar.86555 _fvar.86606 _fvar.86607
    _fvar.86608 _fvar.86702 _fvar.87001 _fvar.87002 _fvar.87003⊢ ↑N ≤ n, ?_ ⟩
    apply hεsmp.aa:ℕ → ℝL:ℝh:∀ ε > 0, ∀ N ≥ 0, ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ εs:Set ℝε:ℝhε:ε > 0hεs:Metric.ball L ε ⊆ sN:ℕn:ℤhn1:n ≥ ↑Nhn2:|(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε / 2hn:_fvar.87001 ≥ 0 := ?_mvar.89751⊢ a n.toNat ∈ Metric.ball L ε; simp [Real.dist_eq, hn] at *mp.aa:ℕ → ℝL:ℝs:Set ℝε:ℝhεs:Metric.ball L ε ⊆ sN:ℕn:ℤh:∀ (ε : ℝ), 0 < ε → ∀ (N : ℤ), 0 ≤ N → ∃ n, N ≤ n ∧ |(if 0 ≤ n then a n.toNat else 0) - L| ≤ εhε:0 < εhn1:↑N ≤ nhn2:|a n.toNat - L| ≤ ε / 2hn:True⊢ |a n.toNat - L| < ε; linarithAll goals completed! 🐙
  intro h ε hε N _mpra:ℕ → ℝL:ℝh:∀ (s : Set ℝ), (∃ ε > 0, Metric.ball L ε ⊆ s) → ∀ (a_2 : ℕ), ∃ b ≥ a_2, a b ∈ sε:ℝhε:ε > 0N:ℤa✝:N ≥ 0⊢ ∃ n ≥ N, |(if n ≥ 0 then a n.toNat else 0) - L| ≤ ε
  have ⟨ n, hn1, hn2 ⟩ := h (Metric.ball L ε) ⟨ _, hε, bya:ℕ → ℝL:ℝh:∀ (s : Set ℝ), (∃ ε > 0, Metric.ball L ε ⊆ s) → ∀ (a_2 : ℕ), ∃ b ≥ a_2, a b ∈ sε:ℝhε:ε > 0N:ℤa✝:N ≥ 0⊢ Metric.ball L ε ⊆ Metric.ball L ε aesopAll goals completed! 🐙 ⟩ N.toNat
  have hn : n ≥ 0 := bya:ℕ → ℝL:ℝ⊢ (↑a).LimitPoint L ↔ MapClusterPt L atTop a positivityAll goals completed! 🐙
  refine ⟨ n, bya:ℕ → ℝL:ℝh:∀ (s : Set ℝ), (∃ ε > 0, Metric.ball L ε ⊆ s) → ∀ (a_2 : ℕ), ∃ b ≥ a_2, a b ∈ sε:ℝhε:ε > 0N:ℤa✝:N ≥ 0n:ℕhn1:n ≥ N.toNathn2:a n ∈ Metric.ball L εhn:_fvar.116180 ≥ 0 := zero_le _fvar.116180⊢ ↑n ≥ N rwa [ge_iff_le, ←Int.toNat_le]a:ℕ → ℝL:ℝh:∀ (s : Set ℝ), (∃ ε > 0, Metric.ball L ε ⊆ s) → ∀ (a_2 : ℕ), ∃ b ≥ a_2, a b ∈ sε:ℝhε:ε > 0N:ℤa✝:N ≥ 0n:ℕhn1:n ≥ N.toNathn2:a n ∈ Metric.ball L εhn:_fvar.116180 ≥ 0 := zero_le _fvar.116180⊢ N.toNat ≤ n, ?_ ⟩
  simp [Real.dist_eq, hn] at *mpra:ℕ → ℝL:ℝε:ℝN:ℤn:ℕh:∀ (s : Set ℝ) (x : ℝ), 0 < x → Metric.ball L x ⊆ s → ∀ (a_3 : ℕ), ∃ b, a_3 ≤ b ∧ a b ∈ shε:0 < εa✝:0 ≤ Nhn1:N ≤ ↑nhn2:|a n - L| < εhn:True⊢ |a n - L| ≤ ε; linarithAll goals completed! 🐙

Identification with Filter.limsup.{u_1, u_2} {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (u : β → α) (f : Filter β) : αFilter.limsup

theorem declaration uses 'sorry'Chapter6.Sequence.limsup_eq (a:ℕ → ℝ) :
    (a:Sequence).limsup = atTop.limsup (fun n ↦ (a n:EReal)) := bya:ℕ → ℝ⊢ (↑a).limsup = Filter.limsup (fun n => ↑(a n)) atTop
  simp_rw [Filter.limsup_eq, eventually_atTop]a:ℕ → ℝ⊢ (↑a).limsup = sInf {a_1 | ∃ a_2, ∀ b ≥ a_2, ↑(a b) ≤ a_1}
  sorryAll goals completed! 🐙

Identification with Filter.liminf.{u_1, u_2} {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (u : β → α) (f : Filter β) : αFilter.liminf

theorem declaration uses 'sorry'Chapter6.Sequence.liminf_eq (a:ℕ → ℝ) :
    (a:Sequence).liminf = atTop.liminf (fun n ↦ (a n:EReal)) := bya:ℕ → ℝ⊢ (↑a).liminf = Filter.liminf (fun n => ↑(a n)) atTop
  simp_rw [Filter.liminf_eq, eventually_atTop]a:ℕ → ℝ⊢ (↑a).liminf = sSup {a_1 | ∃ a_2, ∀ b ≥ a_2, a_1 ≤ ↑(a b)}
  sorryAll goals completed! 🐙

Identification of Unknown identifier `rpow`rpow and Mathlib exponentiation

theorem declaration uses 'sorry'Chapter6.Real.rpow_eq_rpow (x:ℝ) (α:ℝ) : rpow x α = x^α := byx:ℝα:ℝ⊢ rpow x α = x ^ α
  sorryAll goals completed! 🐙