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

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

theorem jacobiTheta_eq_jacobiTheta₂ (τ : ℂ) : jacobiTheta τ = jacobiTheta₂ 0 τ

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

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 norm_exp_mul_sq_le {τ : ℂ} (hτ : 0 < τ.im) (n : ℤ) : ‖Complex.exp (↑Real.pi * Complex.I * ↑n ^ 2 * τ)‖ ≤ Real.exp (-Real.pi * τ.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 {τ : ℂ} (hτ : 0 < τ.im) : Summable fun (n : ℤ) => Complex.exp (↑Real.pi * Complex.I * ↑n ^ 2 * τ)

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

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