Documentation

Mathlib.Algebra.Order.CauSeq.BigOperators

Cauchy sequences and big operators #

This file proves some more lemmas about basic Cauchy sequences that involve finite sums.

theorem IsCauSeq.of_abv_le {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} {a : α} (n : ) (hm : ∀ (m : ), n mabv (f m) a m) :
(IsCauSeq abs fun (n : ) => iFinset.range n, a i)IsCauSeq abv fun (n : ) => iFinset.range n, f i
theorem IsCauSeq.of_abv {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} (hf : IsCauSeq abs fun (m : ) => nFinset.range m, abv (f n)) :
IsCauSeq abv fun (m : ) => nFinset.range m, f n
theorem cauchy_product {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} {g : β} (ha : IsCauSeq abs fun (m : ) => nFinset.range m, abv (f n)) (hb : IsCauSeq abv fun (m : ) => nFinset.range m, g n) (ε : α) (ε0 : 0 < ε) :
∃ (i : ), ji, abv ((kFinset.range j, f k) * kFinset.range j, g k - nFinset.range j, mFinset.range (n + 1), f m * g (n - m)) < ε
theorem IsCauSeq.of_decreasing_bounded {α : Type u_1} [LinearOrderedField α] [Archimedean α] (f : α) {a : α} {m : } (ham : nm, |f n| a) (hnm : nm, f n.succ f n) :
IsCauSeq abs f
theorem IsCauSeq.of_mono_bounded {α : Type u_1} [LinearOrderedField α] [Archimedean α] (f : α) {a : α} {m : } (ham : nm, |f n| a) (hnm : nm, f n f n.succ) :
IsCauSeq abs f
theorem IsCauSeq.geo_series {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] [Archimedean α] [Nontrivial β] (x : β) (hx1 : abv x < 1) :
IsCauSeq abv fun (n : ) => mFinset.range n, x ^ m
theorem IsCauSeq.geo_series_const {α : Type u_1} [LinearOrderedField α] [Archimedean α] (a : α) {x : α} (hx1 : |x| < 1) :
IsCauSeq abs fun (m : ) => nFinset.range m, a * x ^ n
theorem IsCauSeq.series_ratio_test {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] [Archimedean α] {f : β} (n : ) (r : α) (hr0 : 0 r) (hr1 : r < 1) (h : ∀ (m : ), n mabv (f m.succ) r * abv (f m)) :
IsCauSeq abv fun (m : ) => nFinset.range m, f n