mathlib documentation

number_theory.modular_forms.jacobi_theta

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.

noncomputable def jacobi_theta (τ : upper_half_plane) :

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

Equations

jacobi_theta τ = ∑' (n : ℤ), cexp (↑real.pi * complex.I * ↑n ^ 2 * ↑τ)

theorem jacobi_theta_unif_summable {R : ℝ} (hR : 0 < R) :

∃ (bd : ℤ → ℝ), summable bd ∧ ∀ {τ : upper_half_plane}, R ≤ τ.im → ∀ (n : ℤ), ‖cexp (↑real.pi * complex.I * ↑n ^ 2 * ↑τ)‖ ≤ bd n

theorem jacobi_theta_summable (τ : upper_half_plane) :

summable (λ (n : ℤ), cexp (↑real.pi * complex.I * ↑n ^ 2 * ↑τ))

theorem jacobi_theta_two_vadd (τ : upper_half_plane) :

jacobi_theta (2 +ᵥ τ) = jacobi_theta τ

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 τ