cauchySeq_finset_of_geometric_bound

English

If a bounded sequence f(n) satisfies a geometric bound, then the partial sums over finite sets form a Cauchy net in the finite-set topology.

Русский

Если f(n) ограничена и удовлетворяет геометрическому ограничению, то частичные суммы по конечным множествам образуют последовательность Цочи в топологии конечных множеств.

LaTeX

$$CauchySeq (fun s : Finset ℕ => ∑ x ∈ s, f x)$$

Lean4

/-- If `‖f n‖ ≤ C * r ^ n` for all `n : ℕ` and some `r < 1`, then the partial sums of `f` form a
Cauchy sequence. This lemma does not assume `0 ≤ r` or `0 ≤ C`. -/
theorem cauchySeq_finset_of_geometric_bound (hr : r < 1) (hf : ∀ n, ‖f n‖ ≤ C * r ^ n) :
    CauchySeq fun s : Finset ℕ ↦ ∑ x ∈ s, f x :=
  cauchySeq_finset_of_norm_bounded (aux_hasSum_of_le_geometric hr (dist_partial_sum_le_of_le_geometric hf)).summable hf

Похожие утверждения