Jacobi's theta function #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 τ → ∞.
theorem
jacobi_theta_T_sq_smul
(τ : upper_half_plane) :
jacobi_theta ↑(modular_group.T ^ 2 • τ) = jacobi_theta ↑τ
theorem
jacobi_theta_S_smul
(τ : upper_half_plane) :
jacobi_theta ↑(modular_group.S • τ) = (-complex.I * ↑τ) ^ (1 / 2) * jacobi_theta ↑τ
theorem
is_O_at_im_infty_jacobi_theta_sub_one
:
(λ (τ : ℂ), jacobi_theta τ - 1) =O[filter.comap complex.im filter.at_top] λ (τ : ℂ), rexp (-real.pi * τ.im)
The norm of jacobi_theta τ - 1 decays exponentially as im τ → ∞.