Theorems · Theorem · number theory
LSeriesSummable.isBigO_rpow
∀ {f : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → f =O[Filter.atTop] fun n => ↑n ^ s.reIf the LSeries of f is summable at s, then f = O(n^(re s)).
- Defined in
- Mathlib.NumberTheory.LSeries.Basic
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Norm.normproof · cited by 5,413
- Filter.atTopstatement · cited by 2,405
- Complex.restatement and proof · cited by 882
- Asymptotics.IsBigOstatement · cited by 506
- abs_of_nonnegproof · cited by 279
- Filter.eventually_atTopproof · cited by 112
- Nat.cast_nonnegproof · cited by 109
- Real.norm_eq_absproof · cited by 88
- LSeriesSummablestatement and proof · cited by 59
- Asymptotics.IsBigO.of_boundproof · cited by 15
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.