Аналіз I, Розділ 6, Епілог

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.Cauchy_iff_CauSeq (a : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ↔ IsCauSeq _root_.abs a

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

theorem Chapter6.Sequence.Cauchy_iff_CauchySeq (a : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ↔ CauchySeq a

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

theorem Chapter6.Sequence.tendsto_iff_Tendsto (a : ℕ → ℝ) (L : ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.tendsTo L ↔ Filter.Tendsto a Filter.atTop (nhds L)

Identifiction 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 : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.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 : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy) : lim { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } = CauSeq.lim ⟨a, ⋯⟩

Identification with CauSeq.lim

theorem Chapter6.Sequence.isBounded_iff_isBounded_range (a : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isBounded ↔ Bornology.IsBounded (Set.range a)

Identification with Bornology.IsBounded

theorem Chapter6.Sequence.sup_eq_sSup (a : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.sup = sSup (Set.range fun (n : ℕ) => ↑(a n))

theorem Chapter6.Sequence.inf_eq_sInf (a : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.inf = sInf (Set.range fun (n : ℕ) => ↑(a n))

theorem Chapter6.Sequence.bddAbove_iff (a : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.bddAbove ↔ BddAbove (Set.range a)

theorem Chapter6.Sequence.bddBelow_iff (a : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.bddBelow ↔ BddBelow (Set.range a)

theorem Chapter6.Sequence.Monotone_iff (a : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isMonotone ↔ Monotone a

theorem Chapter6.Sequence.Antitone_iff (a : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isAntitone ↔ Antitone a

theorem Chapter6.Sequence.limit_point_iff (a : ℕ → ℝ) (L : ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.limit_point L ↔ MapClusterPt L Filter.atTop a

Identification with Filter.MapClusterPt

theorem Chapter6.Sequence.limsup_eq (a : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.limsup = Filter.limsup (fun (n : ℕ) => ↑(a n)) Filter.atTop

Identification with Filter.limsup

theorem Chapter6.Sequence.liminf_eq (a : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.liminf = Filter.liminf (fun (n : ℕ) => ↑(a n)) Filter.atTop

Identification with Filter.liminf