dist_le_of_le_geometric_of_tendsto

English

If m>1 and f(i) majorizes i ≤ f(i), then ∑ 1/m^{f(i)} converges.

Русский

Если m>1 и f(i) удовлетворяет i ≤ f(i), то ∑ 1/m^{f(i)} сходится.

LaTeX

$$$$\sum_{i=0}^{\infty} \frac{1}{m^{f(i)}} < \infty, \quad m>1.$$$$

Lean4

/-- If `dist (f n) (f (n+1))` is bounded by `C * r^n`, `r < 1`, then the distance from
`f 0` to the limit of `f` is bounded above by `C / (1 - r)`. -/
theorem dist_le_of_le_geometric_of_tendsto {a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) :
    dist (f n) a ≤ C * r ^ n / (1 - r) :=
  by
  have := aux_hasSum_of_le_geometric hr hu
  convert dist_le_tsum_of_dist_le_of_tendsto _ hu ⟨_, this⟩ ha n
  simp only [pow_add, mul_left_comm C, mul_div_right_comm]
  rw [mul_comm]
  exact (this.mul_left _).tsum_eq.symm

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