summable_inv_of_isBigO_rpow_inv — Mathlib

English

If the inverse of f is big-O of |n|^(-a) with a > 1, then ∑ f(n)^{-1} converges (is summable).

Русский

Если обратная функция f имеет порядок O(|n|^{-a}) при a>1, то сумма ∑ f(n)^{-1} сходится.

LaTeX

$$$1 < a \\quad\\land\\quad (\\forall n, f(n)^{-1} = O\\_{cofinite} |n|^{-a}) \\Rightarrow \\ Summable (n \\mapsto f(n)^{-1})$$$

Lean4

/-- If the inverse of a function `isBigO` to `(|(n : ℝ)| ^ a)⁻¹` for `1 < a`, then the function is
Summable. -/
theorem summable_inv_of_isBigO_rpow_inv {α : Type*} [NormedField α] [CompleteSpace α] {f : ℤ → α} {a : ℝ} (hab : 1 < a)
    (hf : (fun n ↦ (f n)⁻¹) =O[cofinite] fun n ↦ (|(n : ℝ)| ^ a)⁻¹) : Summable fun n ↦ (f n)⁻¹ :=
  summable_of_isBigO ((Real.summable_abs_int_rpow hab).congr fun b ↦ Real.rpow_neg (abs_nonneg ↑b) a) hf

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