dist_le_of_le_geometric_two_of_tendsto₀

English

If ∑' i 1/m^{f(i)} converges, then the sequence of partial sums is bounded by a finite value.

Русский

Если сумма ∑' i 1/m^{f(i)} сходится, частичные суммы ограничены конечным числом.

LaTeX

$$$$\sum_{i=0}^{\infty} \frac{1}{m^{f(i)}} < \infty \implies \text{bounded}.$$$$

Lean4

/-- If `dist (f n) (f (n+1))` is bounded by `(C / 2) / 2^n`, then the distance from
`f 0` to the limit of `f` is bounded above by `C`. -/
theorem dist_le_of_le_geometric_two_of_tendsto₀ {a : α} (ha : Tendsto f atTop (𝓝 a)) : dist (f 0) a ≤ C :=
  tsum_geometric_two' C ▸ dist_le_tsum_of_dist_le_of_tendsto₀ _ hu₂ (summable_geometric_two' C) ha

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