# Documentation

Mathlib.NumberTheory.ModularForms.JacobiTheta.Basic

# Jacobi's theta function #

This file defines the Jacobi theta function

$$\theta(\tau) = \sum_{n \in \mathbb{Z}} \exp (i \pi n ^ 2 \tau),$$

and proves the modular transformation properties θ (τ + 2) = θ τ and θ (-1 / τ) = (-I * τ) ^ (1 / 2) * θ τ, using Poisson's summation formula for the latter. We also show that θ is differentiable on ℍ, and θ(τ) - 1 has exponential decay as im τ → ∞.

noncomputable def jacobiTheta (z : ) :

Jacobi's theta function ∑' (n : ℤ), exp (π * I * n ^ 2 * τ).

Instances For
theorem norm_exp_mul_sq_le {z : } (hz : 0 < z.im) (n : ) :
Complex.exp ( * n ^ 2 * z) Real.exp ( * z.im) ^
theorem exists_summable_bound_exp_mul_sq {R : } (hR : 0 < R) :
bd, Summable bd ∀ {τ : }, R τ.im∀ (n : ), Complex.exp ( * n ^ 2 * τ) bd n
theorem summable_exp_mul_sq {z : } (hz : 0 < z.im) :
Summable fun n => Complex.exp ( * n ^ 2 * z)
theorem jacobiTheta_S_smul (τ : UpperHalfPlane) :
= () ^ (1 / 2) *
theorem hasSum_nat_jacobiTheta {z : } (hz : 0 < z.im) :
HasSum (fun n => Complex.exp ( * (n + 1) ^ 2 * z)) (( - 1) / 2)
theorem jacobiTheta_eq_tsum_nat {z : } (hz : 0 < z.im) :
= 1 + 2 * ∑' (n : ), Complex.exp ( * (n + 1) ^ 2 * z)
theorem norm_jacobiTheta_sub_one_le {z : } (hz : 0 < z.im) :
- 1 2 / (1 - Real.exp ( * z.im)) * Real.exp ( * z.im)

An explicit upper bound for ‖jacobiTheta τ - 1‖.

theorem isBigO_at_im_infty_jacobiTheta_sub_one :
(fun τ => - 1) =O[Filter.comap Complex.im Filter.atTop] fun τ => Real.exp ( * τ.im)

The norm of jacobiTheta τ - 1 decays exponentially as im τ → ∞.

theorem differentiableAt_jacobiTheta {z : } (hz : 0 < z.im) :
theorem continuousAt_jacobiTheta {z : } (hz : 0 < z.im) :