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 ≤ m → abv (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 : ℕ),
∀ j ≥ i,
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 : ∀ n ≥ m, |f n| ≤ a)
(hnm : ∀ n ≥ m, f (Nat.succ n) ≤ f n)
:
IsCauSeq abs f
theorem
IsCauSeq.of_mono_bounded
{α : Type u_1}
[LinearOrderedField α]
[Archimedean α]
(f : ℕ → α)
{a : α}
{m : ℕ}
(ham : ∀ n ≥ m, |f n| ≤ a)
(hnm : ∀ n ≥ m, 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 ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m))
:
IsCauSeq abv fun (m : ℕ) => Finset.sum (Finset.range m) fun (n : ℕ) => f n