Documentation

Mathlib.NumberTheory.LSeries.Basic

L-series #

Given a sequence f: ℕ → ℂ, we define the corresponding L-series.

Main Definitions #

Main Results #

Notation #

We introduce L as notation for LSeries and ↗f as notation for fun n : ℕ ↦ (f n : ℂ), both scoped to LSeries.notation. The latter makes it convenient to use arithmetic functions or Dirichlet characters (or anything that coerces to a function N → R, where coerces to N and R coerces to ) as arguments to LSeries etc.

Tags #

L-series

The terms of an L-series #

We define the nth term evaluated at a complex number s of the L-series associated to a sequence f : ℕ → ℂ, LSeries.term f s n, and provide some basic API.

We set LSeries.term f s 0 = 0, and for positive n, LSeries.term f s n = f n / n ^ s.

noncomputable def LSeries.term (f : ) (s : ) (n : ) :

The nth term of the L-series of f evaluated at s. We set it to zero when n = 0.

Equations
Instances For
    theorem LSeries.term_def (f : ) (s : ) (n : ) :
    LSeries.term f s n = if n = 0 then 0 else f n / n ^ s
    @[simp]
    theorem LSeries.term_zero (f : ) (s : ) :
    LSeries.term f s 0 = 0
    @[simp]
    theorem LSeries.term_of_ne_zero {n : } (hn : n 0) (f : ) (s : ) :
    LSeries.term f s n = f n / n ^ s
    theorem LSeries.term_of_ne_zero' {s : } (hs : s 0) (f : ) (n : ) :
    LSeries.term f s n = f n / n ^ s

    If s ≠ 0, then the if .. then .. else construction in LSeries.term isn't needed, since 0 ^ s = 0.

    theorem LSeries.term_congr {f : } {g : } (h : ∀ {n : }, n 0f n = g n) (s : ) (n : ) :
    theorem LSeries.norm_term_eq (f : ) (s : ) (n : ) :
    LSeries.term f s n = if n = 0 then 0 else f n / n ^ s.re
    theorem LSeries.norm_term_le {f : } {g : } (s : ) {n : } (h : f n g n) :
    theorem LSeries.norm_term_le_of_re_le_re (f : ) {s : } {s' : } (h : s.re s'.re) (n : ) :

    We define LSeries f s of f : ℕ → ℂ as the sum over LSeries.term f s. We also provide predicates LSeriesSummable f s stating that LSeries f s is summable and LSeriesHasSum f s a stating that the L-series of f is summable at s and converges to a : ℂ.

    noncomputable def LSeries (f : ) (s : ) :

    The value of the L-series of the sequence f at the point s if it converges absolutely there, and 0 otherwise.

    Equations
    Instances For
      theorem LSeries_congr {f : } {g : } (s : ) (h : ∀ {n : }, n 0f n = g n) :
      LSeries f s = LSeries g s
      def LSeriesSummable (f : ) (s : ) :

      LSeriesSummable f s indicates that the L-series of f converges absolutely at s.

      Equations
      Instances For
        theorem LSeriesSummable_congr {f : } {g : } (s : ) (h : ∀ {n : }, n 0f n = g n) :
        theorem LSeriesSummable.congr' {f : } {g : } (s : ) (h : f =ᶠ[Filter.atTop] g) (hf : LSeriesSummable f s) :

        If f and g agree on large n : ℕ and the LSeries of f converges at s, then so does that of g.

        theorem LSeriesSummable_congr' {f : } {g : } (s : ) (h : f =ᶠ[Filter.atTop] g) :

        If f and g agree on large n : ℕ, then the LSeries of f converges at s if and only if that of g does.

        def LSeriesHasSum (f : ) (s : ) (a : ) :

        This states that the L-series of the sequence f converges absolutely at s and that the value there is a.

        Equations
        Instances For
          theorem LSeriesHasSum.LSeriesSummable {f : } {s : } {a : } (h : LSeriesHasSum f s a) :
          theorem LSeriesHasSum.LSeries_eq {f : } {s : } {a : } (h : LSeriesHasSum f s a) :
          LSeries f s = a
          theorem LSeriesHasSum_iff {f : } {s : } {a : } :
          theorem LSeriesHasSum_congr {f : } {g : } (s : ) (a : ) (h : ∀ {n : }, n 0f n = g n) :
          theorem LSeriesSummable.of_re_le_re {f : } {s : } {s' : } (h : s.re s'.re) (hf : LSeriesSummable f s) :
          theorem LSeriesSummable_iff_of_re_eq_re {f : } {s : } {s' : } (h : s.re = s'.re) :
          def LSeries.delta (n : ) :

          The indicator function of {1} ⊆ ℕ with values in .

          Equations
          Instances For

            Notation #

            The value of the L-series of the sequence f at the point s if it converges absolutely there, and 0 otherwise.

            Equations
            Instances For

              We introduce notation ↗f for f interpreted as a function ℕ → ℂ.

              Let R be a ring with a coercion to . Then we can write ↗χ when χ : DirichletCharacter R or ↗f when f : ArithmeticFunction R or simply f : N → R with a coercion from to N as an argument to LSeries, LSeriesHasSum, LSeriesSummable etc.

              Equations
              Instances For

                The indicator function of {1} ⊆ ℕ with values in .

                Equations
                Instances For

                  LSeries of 0 and δ #

                  @[simp]
                  theorem LSeries_zero :
                  theorem LSeries.term_delta (s : ) (n : ) :
                  LSeries.term LSeries.delta s n = if n = 1 then 1 else 0
                  theorem LSeries.mul_delta {f : } (h : f 1 = 1) :
                  theorem LSeries.delta_mul {f : } (h : f 1 = 1) :

                  The L-series of δ is the constant function 1.

                  Criteria for and consequences of summability of L-series #

                  We relate summability of L-series with bounds on the coefficients in terms of powers of n.

                  theorem LSeriesSummable.le_const_mul_rpow {f : } {s : } (h : LSeriesSummable f s) :
                  ∃ (C : ), ∀ (n : ), n 0f n C * n ^ s.re

                  If the LSeries of f is summable at s, then f n is bounded in absolute value by a constant times n^(re s).

                  theorem LSeriesSummable.isBigO_rpow {f : } {s : } (h : LSeriesSummable f s) :
                  f =O[Filter.atTop] fun (n : ) => n ^ s.re

                  If the LSeries of f is summable at s, then f = O(n^(re s)).

                  theorem LSeriesSummable_of_le_const_mul_rpow {f : } {x : } {s : } (hs : x < s.re) (h : ∃ (C : ), ∀ (n : ), n 0f n C * n ^ (x - 1)) :

                  If f n is bounded in absolute value by a constant times n^(x-1) and re s > x, then the LSeries of f is summable at s.

                  theorem LSeriesSummable_of_isBigO_rpow {f : } {x : } {s : } (hs : x < s.re) (h : f =O[Filter.atTop] fun (n : ) => n ^ (x - 1)) :

                  If f = O(n^(x-1)) and re s > x, then the LSeries of f is summable at s.

                  theorem LSeriesSummable_of_bounded_of_one_lt_re {f : } {m : } (h : ∀ (n : ), n 0Complex.abs (f n) m) {s : } (hs : 1 < s.re) :

                  If f is bounded, then its LSeries is summable at s when re s > 1.

                  theorem LSeriesSummable_of_bounded_of_one_lt_real {f : } {m : } (h : ∀ (n : ), n 0Complex.abs (f n) m) {s : } (hs : 1 < s) :

                  If f is bounded, then its LSeries is summable at s : ℝ when s > 1.