# mathlib3documentation

number_theory.modular_forms.jacobi_theta.basic

# 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 τ → ∞.

noncomputable def jacobi_theta (z : ) :

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

Equations
theorem norm_exp_mul_sq_le {z : } (hz : 0 < z.im) (n : ) :
theorem exists_summable_bound_exp_mul_sq {R : } (hR : 0 < R) :
(bd : ), summable bd {τ : }, R τ.im (n : ), cexp * n ^ 2 * τ) bd n
theorem summable_exp_mul_sq {z : } (hz : 0 < z.im) :
summable (λ (n : ), cexp * n ^ 2 * z))
theorem jacobi_theta_two_add (z : ) :
theorem has_sum_nat_jacobi_theta {z : } (hz : 0 < z.im) :
has_sum (λ (n : ), cexp * (n + 1) ^ 2 * z)) ((jacobi_theta z - 1) / 2)
theorem jacobi_theta_eq_tsum_nat {z : } (hz : 0 < z.im) :
= 1 + 2 * ∑' (n : ), cexp * (n + 1) ^ 2 * z)
theorem norm_jacobi_theta_sub_one_le {z : } (hz : 0 < z.im) :

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

theorem is_O_at_im_infty_jacobi_theta_sub_one  :
(λ (τ : ), - 1) =O[] λ (τ : ), rexp (-real.pi * τ.im)

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

theorem differentiable_at_jacobi_theta {z : } (hz : 0 < z.im) :
theorem continuous_at_jacobi_theta {z : } (hz : 0 < z.im) :