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 : ℕ) => ∑ i ∈ Finset.range n, a i) → IsCauSeq abv fun (n : ℕ) => ∑ i ∈ Finset.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 : ℕ) => ∑ n ∈ Finset.range m, abv (f n))
:
IsCauSeq abv fun (m : ℕ) => ∑ n ∈ Finset.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 : ℕ) => ∑ n ∈ Finset.range m, abv (f n))
(hb : IsCauSeq abv fun (m : ℕ) => ∑ n ∈ Finset.range m, g n)
(ε : α)
(ε0 : 0 < ε)
:
∃ (i : ℕ),
∀ j ≥ i,
abv
((∑ k ∈ Finset.range j, f k) * ∑ k ∈ Finset.range j, g k - ∑ n ∈ Finset.range j, ∑ m ∈ Finset.range (n + 1), 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 n.succ ≤ 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 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 : ℕ) => ∑ m ∈ Finset.range n, x ^ m
theorem
IsCauSeq.geo_series_const
{α : Type u_1}
[LinearOrderedField α]
[Archimedean α]
(a : α)
{x : α}
(hx1 : |x| < 1)
:
IsCauSeq abs fun (m : ℕ) => ∑ n ∈ Finset.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 ≤ m → abv (f m.succ) ≤ r * abv (f m))
:
IsCauSeq abv fun (m : ℕ) => ∑ n ∈ Finset.range m, f n