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 * τ).

Equations

• jacobiTheta z = ∑' (n : ℤ), Complex.exp (↑Real.pi * Complex.I * ↑n ^ 2 * z)

theorem norm_exp_mul_sq_le {z : ℂ} (hz : 0 < z.im) (n : ℤ) : ‖Complex.exp (↑Real.pi * Complex.I * ↑n ^ 2 * z)‖ ≤ Real.exp (-Real.pi * z.im) ^ Int.natAbs n

theorem exists_summable_bound_exp_mul_sq {R : ℝ} (hR : 0 < R) : ∃ (bd : ℤ → ℝ), Summable bd ∧ ∀ {τ : ℂ}, R ≤ τ.im → ∀ (n : ℤ), ‖Complex.exp (↑Real.pi * Complex.I * ↑n ^ 2 * τ)‖ ≤ bd n

theorem summable_exp_mul_sq {z : ℂ} (hz : 0 < z.im) : Summable fun (n : ℤ) => Complex.exp (↑Real.pi * Complex.I * ↑n ^ 2 * z)

theorem jacobiTheta_two_add (z : ℂ) : jacobiTheta (2 + z) = jacobiTheta z

theorem jacobiTheta_T_sq_smul (τ : UpperHalfPlane) : jacobiTheta ↑(ModularGroup.T ^ 2 • τ) = jacobiTheta ↑τ

theorem jacobiTheta_S_smul (τ : UpperHalfPlane) : jacobiTheta ↑(ModularGroup.S • τ) = (-Complex.I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ

theorem hasSum_nat_jacobiTheta {z : ℂ} (hz : 0 < z.im) : HasSum (fun (n : ℕ) => Complex.exp (↑Real.pi * Complex.I * (↑n + 1) ^ 2 * z)) ((jacobiTheta z - 1) / 2)

theorem jacobiTheta_eq_tsum_nat {z : ℂ} (hz : 0 < z.im) : jacobiTheta z = 1 + 2 * ∑' (n : ℕ), Complex.exp (↑Real.pi * Complex.I * (↑n + 1) ^ 2 * z)

theorem norm_jacobiTheta_sub_one_le {z : ℂ} (hz : 0 < z.im) : ‖jacobiTheta z - 1‖ ≤ 2 / (1 - Real.exp (-Real.pi * z.im)) * Real.exp (-Real.pi * z.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 differentiableAt_jacobiTheta {z : ℂ} (hz : 0 < z.im) : DifferentiableAt ℂ jacobiTheta z

theorem continuousAt_jacobiTheta {z : ℂ} (hz : 0 < z.im) : ContinuousAt jacobiTheta z