dist_le_of_le_geometric_of_tendsto₀

English

If r<1 and f is a geometric majorant, then HasSum of the geometric series with ratio r equals r/(1−r).

Русский

Если r<1 и имеется верхняя геометрическая граница, то имеет место HasSum геометрической серии с коэффициентом r, равное r/(1−r).

LaTeX

$$$$\text{HasSum } (r^n) = \frac{r}{1-r}.$$$$

Lean4

/-- If `dist (f n) (f (n+1))` is bounded by `C * r^n`, `r < 1`, then the distance from
`f n` to the limit of `f` is bounded above by `C * r^n / (1 - r)`. -/
theorem dist_le_of_le_geometric_of_tendsto₀ {a : α} (ha : Tendsto f atTop (𝓝 a)) : dist (f 0) a ≤ C / (1 - r) :=
  (aux_hasSum_of_le_geometric hr hu).tsum_eq ▸
    dist_le_tsum_of_dist_le_of_tendsto₀ _ hu ⟨_, aux_hasSum_of_le_geometric hr hu⟩ ha

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