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

• HurwitzKernelBounds.isBigO_atTop_F_nat_zero_sub : for 0 ≤ a, the function F_nat 0 a - (if a = 0 then 1 else 0) decays exponentially at ∞ (i.e. it satisfies =O[atTop] fun t ↦ exp (-p * t) for some real 0 < p).
• HurwitzKernelBounds.isBigO_atTop_F_nat_one : for 0 ≤ a, the function F_nat 1 a decays exponentially at ∞.
• HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub : for any a : UnitAddCircle, the function F_int 0 a - (if a = 0 then 1 else 0) decays exponentially at ∞.
• HurwitzKernelBounds.isBigO_atTop_F_int_one: the function F_int 1 a decays exponentially at ∞.

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

• HurwitzKernelBounds.f_nat k a t n = (↑n + a) ^ k * Real.exp (-Real.pi * (↑n + a) ^ 2 * t)

def HurwitzKernelBounds.g_nat (k : ℕ) (a t : ℝ) (n : ℕ) : ℝ

An upper bound for the summand when 0 ≤ a.

Equations

• HurwitzKernelBounds.g_nat k a t n = (↑n + a) ^ k * Real.exp (-Real.pi * (↑n + a ^ 2) * t)

theorem HurwitzKernelBounds.f_le_g_nat (k : ℕ) {a t : ℝ} (ha : 0 ≤ a) (ht : 0 < t) (n : ℕ) : ‖HurwitzKernelBounds.f_nat k a t n‖ ≤ HurwitzKernelBounds.g_nat k a t n

def HurwitzKernelBounds.F_nat (k : ℕ) (a t : ℝ) : ℝ

The sum to be bounded (ℕ version).

Equations

• HurwitzKernelBounds.F_nat k a t = ∑' (n : ℕ), HurwitzKernelBounds.f_nat k a t n

theorem HurwitzKernelBounds.summable_f_nat (k : ℕ) (a : ℝ) {t : ℝ} (ht : 0 < t) : Summable (HurwitzKernelBounds.f_nat k a t)

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) : ‖HurwitzKernelBounds.F_nat 0 a t‖ ≤ Real.exp (-Real.pi * a ^ 2 * t) / (1 - Real.exp (-Real.pi * t))

theorem HurwitzKernelBounds.F_nat_zero_zero_sub_le {t : ℝ} (ht : 0 < t) : ‖HurwitzKernelBounds.F_nat 0 0 t - 1‖ ≤ Real.exp (-Real.pi * t) / (1 - Real.exp (-Real.pi * 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) : ‖HurwitzKernelBounds.F_nat 1 a t‖ ≤ Real.exp (-Real.pi * (a ^ 2 + 1) * t) / (1 - Real.exp (-Real.pi * t)) ^ 2 + a * Real.exp (-Real.pi * a ^ 2 * t) / (1 - Real.exp (-Real.pi * 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

• HurwitzKernelBounds.f_int k a t n = |↑n + a| ^ k * Real.exp (-Real.pi * (↑n + a) ^ 2 * t)

theorem HurwitzKernelBounds.f_int_ofNat (k : ℕ) {a : ℝ} (ha : 0 ≤ a) (t : ℝ) (n : ℕ) : HurwitzKernelBounds.f_int k a t (Int.ofNat n) = HurwitzKernelBounds.f_nat k a t n

theorem HurwitzKernelBounds.f_int_negSucc (k : ℕ) {a : ℝ} (ha : a ≤ 1) (t : ℝ) (n : ℕ) : HurwitzKernelBounds.f_int k a t (Int.negSucc n) = HurwitzKernelBounds.f_nat k (1 - a) t n

theorem HurwitzKernelBounds.summable_f_int (k : ℕ) (a : ℝ) {t : ℝ} (ht : 0 < t) : Summable (HurwitzKernelBounds.f_int k a t)

def HurwitzKernelBounds.F_int (k : ℕ) (a : UnitAddCircle) (t : ℝ) : ℝ

The sum to be bounded (ℤ version).

Equations

• HurwitzKernelBounds.F_int k a t = ⋯.lift a

theorem HurwitzKernelBounds.F_int_eq_of_mem_Icc (k : ℕ) {a : ℝ} (ha : a ∈ Set.Icc 0 1) {t : ℝ} (ht : 0 < t) : HurwitzKernelBounds.F_int k (↑a) t = HurwitzKernelBounds.F_nat k a t + HurwitzKernelBounds.F_nat k (1 - a) t

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)