Documentation

Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Jacobi's theta function #

This file defines the one-variable 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 (τ : ) :

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

Equations
Instances For
    theorem norm_exp_mul_sq_le {τ : } (hτ : 0 < τ.im) (n : ) :
    Complex.exp (Real.pi * Complex.I * n ^ 2 * τ) Real.exp (-Real.pi * τ.im) ^ n.natAbs
    theorem hasSum_nat_jacobiTheta {τ : } (hτ : 0 < τ.im) :
    HasSum (fun (n : ) => Complex.exp (Real.pi * Complex.I * (n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
    theorem jacobiTheta_eq_tsum_nat {τ : } (hτ : 0 < τ.im) :
    jacobiTheta τ = 1 + 2 * ∑' (n : ), Complex.exp (Real.pi * Complex.I * (n + 1) ^ 2 * τ)
    theorem norm_jacobiTheta_sub_one_le {τ : } (hτ : 0 < τ.im) :

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

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

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

    theorem continuousAt_jacobiTheta {τ : } (hτ : 0 < τ.im) :