Documentation

Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

# Asymptotic bounds for Jacobi theta functions

The goal of this file is to establish some technical lemmas about the asymptotics of the sums

F_nat k a t = ∑' (n : ℕ), (n + a) ^ k * exp (-π * (n + a) ^ 2 * t)

and

F_int k a t = ∑' (n : ℤ), |n + a| ^ k * exp (-π * (n + a) ^ 2 * t).

Here k : ℕ and a : ℝ (resp a : UnitAddCircle) are fixed, and we are interested in asymptotics as t → ∞. These results are needed for the theory of Hurwitz zeta functions (and hence Dirichlet L-functions, etc).

Main results #

theorem HurwitzKernelBounds.isBigO_exp_neg_mul_of_le {c : } {d : } (hcd : c d) :
(fun (t : ) => Real.exp (-d * t)) =O[Filter.atTop] fun (t : ) => Real.exp (-c * t)
def HurwitzKernelBounds.f_nat (k : ) (a : ) (t : ) (n : ) :

Summand in the sum to be bounded ( version).

Equations
Instances For
    def HurwitzKernelBounds.g_nat (k : ) (a : ) (t : ) (n : ) :

    An upper bound for the summand when 0 ≤ a.

    Equations
    Instances For
      theorem HurwitzKernelBounds.f_le_g_nat (k : ) {a : } {t : } (ha : 0 a) (ht : 0 < t) (n : ) :
      def HurwitzKernelBounds.F_nat (k : ) (a : ) (t : ) :

      The sum to be bounded ( version).

      Equations
      Instances For

        Sum over with k = 0 #

        Here we use direct comparison with a geometric series.

        theorem HurwitzKernelBounds.F_nat_zero_le {a : } (ha : 0 a) {t : } (ht : 0 < t) :
        theorem HurwitzKernelBounds.isBigO_atTop_F_nat_zero_sub {a : } (ha : 0 a) :
        ∃ (p : ), 0 < p (fun (t : ) => HurwitzKernelBounds.F_nat 0 a t - if a = 0 then 1 else 0) =O[Filter.atTop] fun (t : ) => Real.exp (-p * t)

        Sum over with k = 1 #

        Here we use comparison with the series ∑ n * r ^ n, where r = exp (-π * t).

        theorem HurwitzKernelBounds.F_nat_one_le {a : } (ha : 0 a) {t : } (ht : 0 < t) :
        theorem HurwitzKernelBounds.isBigO_atTop_F_nat_one {a : } (ha : 0 a) :
        ∃ (p : ), 0 < p HurwitzKernelBounds.F_nat 1 a =O[Filter.atTop] fun (t : ) => Real.exp (-p * t)
        def HurwitzKernelBounds.f_int (k : ) (a : ) (t : ) (n : ) :

        Summand in the sum to be bounded ( version).

        Equations
        Instances For

          The sum to be bounded ( version).

          Equations
          Instances For
            theorem HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub (a : UnitAddCircle) :
            ∃ (p : ), 0 < p (fun (t : ) => HurwitzKernelBounds.F_int 0 a t - if a = 0 then 1 else 0) =O[Filter.atTop] fun (t : ) => Real.exp (-p * t)
            theorem HurwitzKernelBounds.isBigO_atTop_F_int_one (a : UnitAddCircle) :
            ∃ (p : ), 0 < p HurwitzKernelBounds.F_int 1 a =O[Filter.atTop] fun (t : ) => Real.exp (-p * t)