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 : ) => Finset.sum (Finset.range n) fun (i : ) => a i)IsCauSeq abv fun (n : ) => Finset.sum (Finset.range n) fun (i : ) => f i
theorem IsCauSeq.of_abv {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} (hf : IsCauSeq abs fun (m : ) => Finset.sum (Finset.range m) fun (n : ) => abv (f n)) :
IsCauSeq abv fun (m : ) => Finset.sum (Finset.range m) fun (n : ) => f n
theorem cauchy_product {α : Type u_1} {β : Type u_2} [LinearOrderedField α] [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : β} {g : β} (ha : IsCauSeq abs fun (m : ) => Finset.sum (Finset.range m) fun (n : ) => abv (f n)) (hb : IsCauSeq abv fun (m : ) => Finset.sum (Finset.range m) fun (n : ) => g n) (ε : α) (ε0 : 0 < ε) :
∃ (i : ), ji, abv (((Finset.sum (Finset.range j) fun (k : ) => f k) * Finset.sum (Finset.range j) fun (k : ) => g k) - Finset.sum (Finset.range j) fun (n : ) => Finset.sum (Finset.range (n + 1)) fun (m : ) => 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 (Nat.succ n) 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 (Nat.succ n)) :
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 : ) => Finset.sum (Finset.range n) fun (m : ) => x ^ m
theorem IsCauSeq.geo_series_const {α : Type u_1} [LinearOrderedField α] [Archimedean α] (a : α) {x : α} (hx1 : |x| < 1) :
IsCauSeq abs fun (m : ) => Finset.sum (Finset.range m) fun (n : ) => 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 (Nat.succ m)) r * abv (f m)) :
IsCauSeq abv fun (m : ) => Finset.sum (Finset.range m) fun (n : ) => f n