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 (jointly in both variables).

Additionally, we show some analogous results about the derivative (in the z-variable)

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

(Note that the Mellin transform of θ will give us functional equations for L-functions of even Dirichlet characters, and that of θ' will do the same for odd Dirichlet characters.)

Definitions of the summands

def jacobiTheta₂_term (n : ℤ) (z τ : ℂ) : ℂ

Summand in the series for the Jacobi theta function.

def jacobiTheta₂_term_fderiv (n : ℤ) (z τ : ℂ) : ℂ × ℂ →L[ℂ] ℂ

Summand in the series for the Fréchet derivative of the Jacobi theta function.

theorem hasFDerivAt_jacobiTheta₂_term (n : ℤ) (z τ : ℂ) : HasFDerivAt (fun (p : ℂ × ℂ) => jacobiTheta₂_term n p.1 p.2) (jacobiTheta₂_term_fderiv n z τ) (z, τ)

def jacobiTheta₂'_term (n : ℤ) (z τ : ℂ) : ℂ

Summand in the series for the z-derivative of the Jacobi theta function.

Bounds for the summands

We show that the sums of the three functions jacobiTheta₂_term, jacobiTheta₂'_term and jacobiTheta₂_term_fderiv are locally uniformly convergent in the domain 0 < im τ, and diverge everywhere else.

theorem norm_jacobiTheta₂_term (n : ℤ) (z τ : ℂ) : ‖jacobiTheta₂_term n z τ‖ = Real.exp (-Real.pi * ↑n ^ 2 * τ.im - 2 * Real.pi * ↑n * z.im)

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

A uniform upper bound for jacobiTheta₂_term on compact subsets.

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

A uniform upper bound for jacobiTheta₂'_term on compact subsets.

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

The uniform bound we have given is summable, and remains so after multiplying by any fixed power of |n| (we shall need this for k = 0, 1, 2).

theorem summable_jacobiTheta₂_term_iff (z τ : ℂ) : (Summable fun (x : ℤ) => jacobiTheta₂_term x z τ) ↔ 0 < τ.im

The series defining the theta function is summable if and only if 0 < im τ.

theorem norm_jacobiTheta₂_term_fderiv_le (n : ℤ) (z τ : ℂ) : ‖jacobiTheta₂_term_fderiv n z τ‖ ≤ 3 * Real.pi * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖

theorem norm_jacobiTheta₂_term_fderiv_ge (n : ℤ) (z τ : ℂ) : Real.pi * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

theorem summable_jacobiTheta₂_term_fderiv_iff (z τ : ℂ) : (Summable fun (x : ℤ) => jacobiTheta₂_term_fderiv x z τ) ↔ 0 < τ.im

theorem summable_jacobiTheta₂'_term_iff (z τ : ℂ) : (Summable fun (x : ℤ) => jacobiTheta₂'_term x z τ) ↔ 0 < τ.im

Definitions of the functions

def jacobiTheta₂ (z τ : ℂ) : ℂ

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

def jacobiTheta₂_fderiv (z τ : ℂ) : ℂ × ℂ →L[ℂ] ℂ

Fréchet derivative of the two-variable Jacobi theta function.

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

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

theorem hasSum_jacobiTheta₂_term (z : ℂ) {τ : ℂ} (hτ : 0 < τ.im) : HasSum (fun (n : ℤ) => jacobiTheta₂_term n z τ) (jacobiTheta₂ z τ)

theorem hasSum_jacobiTheta₂_term_fderiv (z : ℂ) {τ : ℂ} (hτ : 0 < τ.im) : HasSum (fun (n : ℤ) => jacobiTheta₂_term_fderiv n z τ) (jacobiTheta₂_fderiv z τ)

theorem hasSum_jacobiTheta₂'_term (z : ℂ) {τ : ℂ} (hτ : 0 < τ.im) : HasSum (fun (n : ℤ) => jacobiTheta₂'_term n z τ) (jacobiTheta₂' z τ)

theorem jacobiTheta₂_undef (z : ℂ) {τ : ℂ} (hτ : τ.im ≤ 0) : jacobiTheta₂ z τ = 0

theorem jacobiTheta₂_fderiv_undef (z : ℂ) {τ : ℂ} (hτ : τ.im ≤ 0) : jacobiTheta₂_fderiv z τ = 0

theorem jacobiTheta₂'_undef (z : ℂ) {τ : ℂ} (hτ : τ.im ≤ 0) : jacobiTheta₂' z τ = 0

Derivatives and continuity

theorem hasFDerivAt_jacobiTheta₂ (z : ℂ) {τ : ℂ} (hτ : 0 < τ.im) : HasFDerivAt (fun (p : ℂ × ℂ) => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

theorem continuousAt_jacobiTheta₂ (z : ℂ) {τ : ℂ} (hτ : 0 < τ.im) : ContinuousAt (fun (p : ℂ × ℂ) => jacobiTheta₂ p.1 p.2) (z, τ)

theorem differentiableAt_jacobiTheta₂_fst (z : ℂ) {τ : ℂ} (hτ : 0 < τ.im) : DifferentiableAt ℂ (fun (x : ℂ) => jacobiTheta₂ x τ) z

Differentiability of Θ z τ in z, for fixed τ.

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

Differentiability of Θ z τ in τ, for fixed z.

theorem hasDerivAt_jacobiTheta₂_fst (z : ℂ) {τ : ℂ} (hτ : 0 < τ.im) : HasDerivAt (fun (x : ℂ) => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z

theorem continuousAt_jacobiTheta₂' (z : ℂ) {τ : ℂ} (hτ : 0 < τ.im) : ContinuousAt (fun (p : ℂ × ℂ) => jacobiTheta₂' p.1 p.2) (z, τ)

Periodicity and conjugation

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

@[simp]

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

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

theorem jacobiTheta₂_conj (z τ : ℂ) : (starRingEnd ℂ) (jacobiTheta₂ z τ) = jacobiTheta₂ ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

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

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

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

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

theorem jacobiTheta₂'_conj (z τ : ℂ) : (starRingEnd ℂ) (jacobiTheta₂' z τ) = jacobiTheta₂' ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Functional equations

theorem jacobiTheta₂_functional_equation (z τ : ℂ) : 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₂ z τ is an explicit factor times jacobiTheta₂ (z / τ) (-1 / τ). This is the key lemma behind the proof of the functional equation for L-series of even Dirichlet characters.

theorem jacobiTheta₂'_functional_equation (z τ : ℂ) : jacobiTheta₂' z τ = 1 / (-Complex.I * τ) ^ (1 / 2) * Complex.exp (-↑Real.pi * Complex.I * z ^ 2 / τ) / τ * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑Real.pi * Complex.I * z * jacobiTheta₂ (z / τ) (-1 / τ))

The functional equation for the derivative of the Jacobi theta function, relating jacobiTheta₂' z τ to jacobiTheta₂' (z / τ) (-1 / τ). This is the key lemma behind the proof of the functional equation for L-series of odd Dirichlet characters.