The two-variable Jacobi theta function

This file defines the two-variable Jacobi theta function

$$\theta(z, \tau) = \sum_{n \in \mathbb{Z}} \exp (2 i \pi n z + i \pi n ^ 2 \tau),$$

and proves the functional equation relating the values at (z, τ) and (z / τ, -1 / τ), using Poisson's summation formula. We also show holomorphy (in both variables individually, not jointly).

noncomputable def jacobiTheta₂ (z : ℂ) (τ : ℂ) : ℂ

The two-variable Jacobi theta function, θ z τ = ∑' (n : ℤ), cexp (2 * π * I * n * z + π * I * n ^ 2 * τ).

The sum is only convergent for 0 < im τ; we are implictly extending it by 0 for other values of τ.

Equations

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

theorem jacobiTheta₂_term_bound {S : ℝ} {T : ℝ} (hT : 0 < T) {z : ℂ} {τ : ℂ} (hz : |z.im| ≤ S) (hτ : T ≤ τ.im) (n : ℤ) : ‖Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * z + ↑Real.pi * Complex.I * ↑n ^ 2 * τ)‖ ≤ Real.exp (-Real.pi * (T * ↑n ^ 2 - 2 * S * ↑|n|))

A uniform bound for the summands in the Jacobi theta function on compact subsets.

theorem summable_jacobiTheta₂_term_bound (S : ℝ) {T : ℝ} (hT : 0 < T) : Summable fun (n : ℤ) => Real.exp (-Real.pi * (T * ↑n ^ 2 - 2 * S * ↑|n|))

theorem differentiableAt_jacobiTheta₂ (z : ℂ) {τ : ℂ} (hτ : 0 < τ.im) : DifferentiableAt ℂ (jacobiTheta₂ z) τ

Differentiability of Θ z τ in τ, for fixed z. (This is weaker than differentiability in both variables simultaneously, but we do not have a version of differentiableOn_tsum_of_summable_norm in multiple variables yet.)

theorem jacobiTheta₂_add_right (z : ℂ) (τ : ℂ) : jacobiTheta₂ z (τ + 2) = jacobiTheta₂ z τ

The two-variable Jacobi theta function is periodic in τ with period 2.

theorem jacobiTheta₂_add_left (z : ℂ) (τ : ℂ) : jacobiTheta₂ (z + 1) τ = jacobiTheta₂ z τ

The two-variable Jacobi theta function is periodic in z with period 1.

theorem jacobiTheta₂_add_left' (z : ℂ) (τ : ℂ) : jacobiTheta₂ (z + τ) τ = Complex.exp (-↑Real.pi * Complex.I * (τ + 2 * z)) * jacobiTheta₂ z τ

The two-variable Jacobi theta function is quasi-periodic in z with period τ.

theorem jacobiTheta₂_neg_left (z : ℂ) (τ : ℂ) : jacobiTheta₂ (-z) τ = jacobiTheta₂ z τ

The two-variable Jacobi theta function is even in z.

theorem jacobiTheta₂_functional_equation (z : ℂ) {τ : ℂ} (hτ : 0 < τ.im) : jacobiTheta₂ z τ = 1 / (-Complex.I * τ) ^ (1 / 2) * Complex.exp (-↑Real.pi * Complex.I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)

The functional equation for the Jacobi theta function: jacobiTheta₂ x τ is an explict factor times jacobiTheta₂ (x / τ) (-1 / τ). This is the key lemma behind the proof of the functional equation for Dirichlet L-series.