Documentation

Mathlib.NumberTheory.LSeries.Convergence

Convergence of L-series #

We define LSeries.abscissaOfAbsConv f (as an EReal) to be the infimum of all real numbers x such that the L-series of f converges for complex arguments with real part x and provide some results about it.

Tags #

L-series, abscissa of convergence

source
๐Ÿ”ธ coverage
noncomputable def LSeries.abscissaOfAbsConv (f : โ„• โ†’ โ„‚) :
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.

Equations
    Instances For
      source
      ๐Ÿ“ coverage
      theorem LSeries.abscissaOfAbsConv_congr {f g : โ„• โ†’ โ„‚} (h : โˆ€ {n : โ„•}, n โ‰  0 โ†’ f n = g n) :
      abscissaOfAbsConv f = abscissaOfAbsConv g
      source
      ๐Ÿ“ coverage
      theorem LSeries.abscissaOfAbsConv_congr' {f g : โ„• โ†’ โ„‚} (h : f =แถ [Filter.atTop] g) :
      abscissaOfAbsConv f = abscissaOfAbsConv g

      If f and g agree on large n : โ„•, then their LSeries have the same abscissa of absolute convergence.

      source
      ๐Ÿ“ coverage
      theorem LSeriesSummable_of_abscissaOfAbsConv_lt_re {f : โ„• โ†’ โ„‚} {s : โ„‚} (hs : LSeries.abscissaOfAbsConv f < โ†‘s.re) :
      LSeriesSummable f s
      source
      ๐Ÿ“ coverage
      theorem LSeriesSummable_lt_re_of_abscissaOfAbsConv_lt_re {f : โ„• โ†’ โ„‚} {s : โ„‚} (hs : LSeries.abscissaOfAbsConv f < โ†‘s.re) :
      โˆƒ x < s.re, LSeriesSummable f โ†‘x
      source
      ๐Ÿ“ coverage
      theorem LSeriesSummable.abscissaOfAbsConv_le {f : โ„• โ†’ โ„‚} {s : โ„‚} (h : LSeriesSummable f s) :
      LSeries.abscissaOfAbsConv f โ‰ค โ†‘s.re
      source
      ๐Ÿ“ coverage
      theorem LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable {f : โ„• โ†’ โ„‚} {x : โ„} (h : โˆ€ (y : โ„), x < y โ†’ LSeriesSummable f โ†‘y) :
      abscissaOfAbsConv f โ‰ค โ†‘x
      source
      ๐Ÿ“ coverage
      theorem LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' {f : โ„• โ†’ โ„‚} {x : EReal} (h : โˆ€ (y : โ„), x < โ†‘y โ†’ LSeriesSummable f โ†‘y) :
      abscissaOfAbsConv f โ‰ค x
      source
      ๐Ÿ“ coverage
      theorem LSeries.abscissaOfAbsConv_le_of_le_const_mul_rpow {f : โ„• โ†’ โ„‚} {x : โ„} (h : โˆƒ (C : โ„), โˆ€ (n : โ„•), n โ‰  0 โ†’ โ€–f nโ€– โ‰ค C * โ†‘n ^ x) :
      abscissaOfAbsConv f โ‰ค โ†‘x + 1

      If โ€–f nโ€– is bounded by a constant times n^x, then the abscissa of absolute convergence of f is bounded by x + 1.

      source
      ๐Ÿ“ coverage
      theorem LSeries.abscissaOfAbsConv_le_of_isBigO_rpow {f : โ„• โ†’ โ„‚} {x : โ„} (h : f =O[Filter.atTop] fun (n : โ„•) => โ†‘n ^ x) :
      abscissaOfAbsConv f โ‰ค โ†‘x + 1

      If โ€–f nโ€– is O(n^x), then the abscissa of absolute convergence of f is bounded by x + 1.

      source
      ๐Ÿ“ coverage
      theorem LSeries.abscissaOfAbsConv_le_of_le_const {f : โ„• โ†’ โ„‚} (h : โˆƒ (C : โ„), โˆ€ (n : โ„•), n โ‰  0 โ†’ โ€–f nโ€– โ‰ค C) :
      abscissaOfAbsConv f โ‰ค 1

      If f is bounded, then the abscissa of absolute convergence of f is bounded above by 1.

      source
      ๐Ÿ“ coverage
      theorem LSeries.abscissaOfAbsConv_le_one_of_isBigO_one {f : โ„• โ†’ โ„‚} (h : f =O[Filter.atTop] fun (x : โ„•) => 1) :
      abscissaOfAbsConv f โ‰ค 1

      If f is O(1), then the abscissa of absolute convergence of f is bounded above by 1.

      source
      ๐Ÿ“ coverage
      theorem LSeries.summable_real_of_abscissaOfAbsConv_lt {f : โ„• โ†’ โ„} {x : โ„} (h : (abscissaOfAbsConv fun (x : โ„•) => โ†‘(f x)) < โ†‘x) :
      Summable fun (n : โ„•) => f n / โ†‘n ^ x

      If f is real-valued and x is strictly greater than the abscissa of absolute convergence of f, then the real series โˆ‘' n, f n / n ^ x converges.

      source
      ๐Ÿ“ coverage
      theorem LSeries.abscissaOfAbsConv_binop_le {F : (โ„• โ†’ โ„‚) โ†’ (โ„• โ†’ โ„‚) โ†’ โ„• โ†’ โ„‚} (hF : โˆ€ {f g : โ„• โ†’ โ„‚} {s : โ„‚}, LSeriesSummable f s โ†’ LSeriesSummable g s โ†’ LSeriesSummable (F f g) s) (f g : โ„• โ†’ โ„‚) :
      abscissaOfAbsConv (F f g) โ‰ค max (abscissaOfAbsConv f) (abscissaOfAbsConv g)

      If F is a binary operation on โ„• โ†’ โ„‚ with the property that the LSeries of F f g converges whenever the LSeries of f and g do, then the abscissa of absolute convergence of F f g is at most the maximum of the abscissa of absolute convergence of f and that of g.