cauchySeq_of_dist_le_of_summable
theorem cauchySeq_of_dist_le_of_summable :
∀ {α : Type u_1} [inst : PseudoMetricSpace α] {f : ℕ → α} (d : ℕ → ℝ),
(∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n) → Summable d → CauchySeq f
This theorem states that given a sequence `f` of elements of a pseudometric space and a sequence `d` of real numbers, if the distance between each consecutive pair of points in the sequence `f` is less than or equal to the corresponding term in the sequence `d`, and the sequence `d` is summable (i.e., the sum of its terms converges to a finite value), then the sequence `f` is a Cauchy sequence.
In other words, if we can bound the distances between consecutive points of a sequence by a series that sums to a finite value, then the sequence itself exhibits the Cauchy property, which means it converges in its space. A sequence is Cauchy if, intuitively, elements become arbitrarily close to each other as we progress through the sequence.
More concisely: Given a sequence `f` in a pseudometric space and a summable sequence `d` of distances between consecutive terms in `f`, if every distance is less than or equal to the corresponding term in `d`, then `f` is a Cauchy sequence.
|
dist_le_tsum_of_dist_le_of_tendsto
theorem dist_le_tsum_of_dist_le_of_tendsto :
∀ {α : Type u_1} [inst : PseudoMetricSpace α] {f : ℕ → α} (d : ℕ → ℝ),
(∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n) →
Summable d →
∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), dist (f n) a ≤ ∑' (m : ℕ), d (n + m)
The theorem `dist_le_tsum_of_dist_le_of_tendsto` states that for any sequence of elements in a pseudometric space (represented as a function `f` from natural numbers to the elements of the space), and a sequence of real numbers `d`, if the distance between each consecutive pair of elements in the sequence `f` is less than or equal to the corresponding number in the sequence `d` and `d` is summable, then for any limit point `a` of the sequence `f` (that is, the sequence `f` tends to `a` as it goes to infinity), the distance from `f n` to `a` is less than or equal to the sum of the tail of sequence `d` starting from `n`. In mathematical terms, we have this inequality for all `n`: `dist (f n) a ≤ ∑' (m : ℕ), d (n + m)`.
More concisely: Given a sequence `(f : ℕ → X)` in a pseudometric space `(X, d)` and a summable sequence `(d : ℕ → ℝ)` of distances such that `d (n + m) ≥ dist (f (n + m), f n)` for all `n, m ∈ ℕ`, then for any limit point `a` of `f`, we have `dist (f n, a) ≤ ∑' m ∈ ℕ, d (n + m)`.
|
tsum_lt_tsum_of_nonneg
theorem tsum_lt_tsum_of_nonneg :
∀ {i : ℕ} {f g : ℕ → ℝ},
(∀ (b : ℕ), 0 ≤ f b) → (∀ (b : ℕ), f b ≤ g b) → f i < g i → Summable g → ∑' (n : ℕ), f n < ∑' (n : ℕ), g n
The theorem `tsum_lt_tsum_of_nonneg` states that for any natural number index `i` and any two sequences of real numbers `f` and `g`, if every term of `f` is non-negative, and every term of `f` is less than or equal to the corresponding term in `g`, and if the `i`-th term of `f` is strictly less than the `i`-th term of `g`, and if the series of `g` is summable, then the series of `f` is strictly less than the series of `g`. In mathematical terms, if $\forall b \in \mathbb{N},\ (0 \leq f(b)) \land (f(b) \leq g(b)) \land (f(i) < g(i))$, and if $\sum g(n)$ is finite, then $\sum f(n) < \sum g(n)$.
More concisely: If `f` is a sequence of non-negative real numbers that is term-wise less than another summable sequence `g`, with strict inequality holding at the `i`-th term, then the sum of `f` is strictly less than the sum of `g`.
|