Theorems · Theorem · number theory

EisensteinSeries.summable_inv_of_isBigO_rpow_inv

∀ {α : Type u_1} [inst : NormedField α] [CompleteSpace α] {f : ℤ → α} {a : ℝ},
  1 < a → ((fun n => (f n)⁻¹) =O[Filter.cofinite] fun n => (|↑n| ^ a)⁻¹) → Summable fun n => (f n)⁻¹

If the inverse of a function isBigO to (|(n : ℝ)| ^ a)⁻¹ for 1 < a, then the function is Summable.

Defined in

Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Cited by

5 results in Mathlib

Foundations

Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldCompleteSpace