Theorems · Definition · number theory
LSeries.abscissaOfAbsConv
(ℕ → ℂ) → EReal
The abscissa x : EReal of absolute convergence of the L-series associated to f:
the series converges absolutely at s when re s > x and does not converge absolutely
when re s < x.
- Defined in
- Mathlib.NumberTheory.LSeries.Convergence
- Cited by
- 50 results in Mathlib
- Foundations
- Depth 193 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.
- Realproof · cited by 25,697
- Set.ofPredproof · cited by 6,101
- Set.imageproof · cited by 5,609
- Complexstatement and proof · cited by 5,565
- Complex.ofRealproof · cited by 1,654
- InfSet.sInfproof · cited by 935
- ERealstatement · cited by 793
- Real.toERealproof · cited by 303
- LSeriesSummableproof · cited by 59
Cited by50
Results whose statement or proof uses this declaration.
- LSeriesSummable_of_abscissaOfAbsConv_lt_restatement and proof · cited by 9
- LSeries.abscissaOfAbsConv_binop_lestatement and proof · cited by 3
- LSeries.abscissaOfAbsConv_congrstatement · cited by 3
- LSeries.abscissaOfAbsConv_onestatement · cited by 3
- LSeries.positivestatement and proof · cited by 3
- LSeriesSummable.abscissaOfAbsConv_lestatement · cited by 3
- LSeries_hasDerivAtstatement and proof · cited by 3
- DirichletCharacter.LSeries_twist_vonMangoldt_eqproof · cited by 2
- DirichletCharacter.absicssaOfAbsConv_eq_onestatement · cited by 2
- LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummablestatement · cited by 2
- LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable'statement · cited by 2
- LSeries.iteratedDeriv_alternatingstatement and proof · cited by 2