Transformation identities and estimates for the one-variable Jacobi theta function

Three identities, a positivity statement and two estimates for Mathlib's jacobiTheta, θ(τ) = ∑_n e^{πi n² τ}, complementing the transformation laws in Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable.

Main results

• TauCeti.jacobiTheta_sub_natCast_div_two: splitting n by parity, θ(τ - N/2) = e^{-πiN/2} θ(τ) + (1 - e^{-πiN/2}) θ(4τ) for every natural number N.
• TauCeti.jacobiTheta_I_mul: the functional equation on the imaginary axis, θ(iy) = θ(i/y) / √y for y > 0.
• TauCeti.jacobiTheta_one_add_I_mul: the functional equation on the line re τ = 1, θ(1 + iy) = ∑_n e^{-π (n - 1/2)² / y} / √y for y > 0.
• TauCeti.jacobiTheta_one_add_I_mul_pos: hence θ(1 + iy) is a positive real number, although its terms (-1)^n e^{-π n² y} alternate in sign.
• TauCeti.norm_jacobiTheta₂_sub_one_le: for real z, ‖θ₂(z, τ) - 1‖ ≤ ‖θ(i im τ) - 1‖.
• TauCeti.tendsto_jacobiTheta_comap_im_atTop: θ(τ) → 1 as im τ → ∞.

theorem TauCeti.jacobiTheta_sub_natCast_div_two (N : ℕ) {τ : ℂ} (hτ : 0 < τ.im) : jacobiTheta (τ - ↑N / 2) = Complex.exp (-↑Real.pi * Complex.I * ↑N / 2) * jacobiTheta τ + (1 - Complex.exp (-↑Real.pi * Complex.I * ↑N / 2)) * jacobiTheta (4 * τ)

Splitting θ(τ - N/2) by the parity of n: the shift multiplies the even terms by 1 and the odd terms by e^{-πiN/2}, and the even terms alone form θ(4τ).

theorem TauCeti.jacobiTheta_I_mul {y : ℝ} (hy : 0 < y) : jacobiTheta (Complex.I * ↑y) = jacobiTheta (Complex.I / ↑y) / ↑√y

The functional equation on the imaginary axis: θ(iy) = θ(i/y) / √y.

theorem TauCeti.jacobiTheta_one_add_I_mul {y : ℝ} (hy : 0 < y) : jacobiTheta (1 + Complex.I * ↑y) = ↑((∑' (n : ℤ), Real.exp (-Real.pi * (↑n - 1 / 2) ^ 2 / y)) / √y)

The functional equation on the line re τ = 1: θ(1 + iy) = ∑_n e^{-π (n - 1/2)² / y} / √y for y > 0. The shift by 1 multiplies the n-th term of θ(iy) by (-1)^n, and the series √y ∑_n (-1)^n e^{-π n² y} is the Fourier expansion of the Gaussian lattice sum ∑_n e^{-π (n - 1/2)² / y} (Real.gaussianLatticeSum_eq_fourier).

theorem TauCeti.jacobiTheta_one_add_I_mul_pos {y : ℝ} (hy : 0 < y) : 0 < jacobiTheta (1 + Complex.I * ↑y)

θ(1 + iy) is a positive real number for y > 0, although its terms (-1)^n e^{-π n² y} alternate in sign: by the functional equation jacobiTheta_one_add_I_mul it is a Gaussian lattice sum divided by √y.

theorem TauCeti.norm_jacobiTheta₂_sub_one_le {z τ : ℂ} (hz : z.im = 0) (hτ : 0 < τ.im) : ‖jacobiTheta₂ z τ - 1‖ ≤ ‖jacobiTheta (Complex.I * ↑τ.im) - 1‖

For real z, the two-variable theta function θ₂(z, τ) is at least as close to 1 as θ(i im τ): its terms have the absolute values e^{-π n² im τ} of the terms of θ(i im τ).

theorem TauCeti.tendsto_jacobiTheta_comap_im_atTop : Filter.Tendsto jacobiTheta (Filter.comap Complex.im Filter.atTop) (nhds 1)

The theta function tends to 1 as im τ → ∞.