English
The Jacobi theta function θ₂ satisfies a functional equation linking θ₂(z,τ) to θ₂(z/τ, -1/τ) via explicit factors: θ₂(z,τ) = 1/(-iτ)^{1/2} e^{−π i z^2/τ} θ₂(z/τ, -1/τ).
Русский
У функции θ₂ выполняется функциональное уравнение: θ₂(z,τ) выражается через θ₂(z/τ, -1/τ) с известными множителями.
LaTeX
$$$\theta_2(z,\tau) = 1/(-i\tau)^{1/2} \; e^{ -\pi i z^2/\tau } \; \theta_2(z/\tau, -1/\tau).$$$
Lean4
/-- 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 / (-I * τ) ^ (1 / 2 : ℂ) * cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ) :=
by
rcases le_or_gt (im τ) 0 with hτ | hτ
· have : (-1 / τ).im ≤ 0 := by
rw [neg_div, neg_im, one_div, inv_im, neg_nonpos]
exact div_nonneg (neg_nonneg.mpr hτ) (normSq_nonneg τ)
rw [jacobiTheta₂_undef z hτ, jacobiTheta₂_undef _ this, mul_zero]
unfold jacobiTheta₂ jacobiTheta₂_term
have h2 : 0 < (-I * τ).re := by
simpa only [neg_mul, neg_re, mul_re, I_re, zero_mul, I_im, one_mul, zero_sub, neg_neg] using hτ
calc
_ = ∑' n : ℤ, cexp (-π * (-I * τ) * ↑n ^ 2 + 2 * π * (I * z) * ↑n) := tsum_congr (fun n ↦ by ring_nf)
_ = 1 / (-I * τ) ^ (1 / 2 : ℂ) * ∑' (n : ℤ), cexp (-π / (-I * τ) * (n + I * (I * z)) ^ 2) := by
rw [tsum_exp_neg_quadratic h2]
_ =
1 / (-I * τ) ^ (1 / 2 : ℂ) * cexp (π * I * (-1 / τ) * z ^ 2) *
∑' (n : ℤ), cexp (2 * π * I * n * (z / τ) + π * I * n ^ 2 * (-1 / τ)) :=
by
simp_rw [mul_assoc _ (cexp _), ← tsum_mul_left (a := cexp _), ← Complex.exp_add]
congr 2 with n : 1; congr 1
field_simp
ring_nf
simp_rw [I_sq, I_pow_four]
ring_nf
_ = _ := by
congr 3
ring
