Theorems · Theorem · number theory
LSeriesSummable_of_bounded_of_one_lt_re
∀ {f : ℕ → ℂ} {m : ℝ}, (∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ m) → ∀ {s : ℂ}, 1 < s.re → LSeriesSummable f sIf f is bounded, then its LSeries is summable at s when re s > 1.
- Defined in
- Mathlib.NumberTheory.LSeries.Basic
- Cited by
- 5 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.
Cites9
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.normstatement and proof · cited by 5,413
- mul_oneproof · cited by 3,885
- sub_selfproof · cited by 996
- Complex.restatement and proof · cited by 882
- Real.rpow_zeroproof · cited by 69
- LSeriesSummablestatement · cited by 59
- LSeriesSummable_of_le_const_mul_rpowproof · cited by 3
Cited by5
Results whose statement or proof uses this declaration.
- ArithmeticFunction.LSeriesSummable_moebius_iffproof · cited by 2
- DirichletCharacter.LSeriesSummable_of_one_lt_reproof · cited by 2
- ZMod.LSeriesSummable_of_one_lt_reproof · cited by 1
- LSeriesSummable_of_bounded_of_one_lt_realproof · cited by 0
- DirichletCharacter.LSeriesSummable_zetaMulproof · cited by 0