Theorems · Theorem · number theory
LSeriesSummable_of_isBigO_rpow
∀ {f : ℕ → ℂ} {x : ℝ} {s : ℂ}, x < s.re → (f =O[Filter.atTop] fun n => ↑n ^ (x - 1)) → LSeriesSummable f sIf f = O(n^(x-1)) and re s > x, then the LSeries of f is summable at s.
- Defined in
- Mathlib.NumberTheory.LSeries.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites34
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
- LE.le.transproof · cited by 3,151
- Filter.Eventuallyproof · cited by 3,134
- Filter.atTopstatement and proof · cited by 2,405
- le_reflproof · cited by 2,061
- Finset.rangeproof · cited by 1,341
- Finset.imageproof · cited by 910
- Complex.restatement and proof · cited by 882
- norm_nonnegproof · cited by 725
- Asymptotics.IsBigOstatement and proof · cited by 506
Cited by1
Results whose statement or proof uses this declaration.
- LSeries.abscissaOfAbsConv_le_of_isBigO_rpowproof · cited by 1