Аналіз I, Розділ 6, Епілог: Зв'язки з операціями границь у Mathlib

У цьому (технічному) епілозі ми показуємо, що різні операції та властивості, які ми визначили для послідовностей «Розділу 6» Chapter6.Sequence, еквівалентні операціям у Mathlib. Зауважте, однак, що операції Mathlib визначені в набагато більшій загальності, ніж випадок послідовностей дійсних чисел, зокрема з використанням мови фільтрів.

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

Зпівставлення із підтримкою Коші-послідовностей у Mathlib/Algebra/Order/CauSeq/Basic

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

Зпівставлення із CauchySeq у Mathlib/Topology/UniformSpace/Cauchy

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

Зпівставлення із 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

Технічна деталь: CauSeq.IsComplete ℝ було встановлено для _root_.abs, але не для norm.

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

Зпівставлення із CauSeq.lim

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

Зпівставлення із limUnder

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

Зпівставлення із 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

Зпівставлення із MapClusterPt

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

Зпівставлення із Filter.limsup

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

Зпівставлення із Filter.liminf

theorem Chapter6.Real.rpow_eq_rpow {x : ℝ} (hx : x > 0) (α : ℝ) : rpow x α = x ^ α

Зпівставлення rpow та експоненціювання Mathlib