Commit 2024-02-27 13:37 b640e0bb

View on Github →

feat(NumberTheory/LSeries/*): add material on convergence (#10728) This continues a series of PRs on L-series. Here we add ArithmeticFunction.LSeriesHasSum (in NumberTheory.LSeries.Basic) and ArithmeticFunction.abscissaOfAbsConv (in a new file NumberTheory.LSeries.Convergence), together with some results about these notions. See here on Zulip.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/LSeries/Basic.lean

added theorem ArithmeticFunction.LSeriesHasSum.LSeriesSummable

added theorem ArithmeticFunction.LSeriesHasSum.LSeries_eq

added def ArithmeticFunction.LSeriesHasSum

added theorem ArithmeticFunction.LSeriesSummable.LSeriesHasSum

added theorem ArithmeticFunction.LSeriesSummable.isBigO_rpow

added theorem ArithmeticFunction.LSeriesSummable.le_const_mul_rpow

added theorem ArithmeticFunction.LSeriesSummable.of_re_le_re

added theorem ArithmeticFunction.LSeriesSummable_of_isBigO_rpow

added theorem ArithmeticFunction.LSeriesSummable_of_le_const_mul_rpow

added theorem ArithmeticFunction.norm_LSeriesTerm_eq

added theorem ArithmeticFunction.norm_LSeriesTerm_le_of_re_le_re

Created Mathlib/NumberTheory/LSeries/Convergence.lean

added theorem ArithmeticFunction.LSeriesSummable.abscissaOfAbsConv_le

added theorem ArithmeticFunction.LSeriesSummable_lt_re_of_abscissaOfAbsConv_lt_re

added theorem ArithmeticFunction.LSeriesSummable_of_abscissaOfAbsConv_lt_re

added theorem ArithmeticFunction.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable'

added theorem ArithmeticFunction.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable

added theorem ArithmeticFunction.abscissaOfAbsConv_le_of_isBigO_rpow

added theorem ArithmeticFunction.abscissaOfAbsConv_le_of_le_const

added theorem ArithmeticFunction.abscissaOfAbsConv_le_of_le_const_mul_rpow

added theorem ArithmeticFunction.abscissaOfAbsConv_le_one_of_isBigO_one