jacobiTheta₂_add_right — Mathlib

English

The two-variable Jacobi theta function is periodic in the τ-variable with period 2: θ₂(z, τ+2) = θ₂(z, τ).

Русский

Двухпеременная функция Джакобиθ₂ периодична по τ с периодом 2: θ₂(z, τ+2) = θ₂(z, τ).

LaTeX

$$$\theta_2(z, \tau+2) = \theta_2(z, \tau)$$$

Lean4

/-- The two-variable Jacobi theta function is periodic in `τ` with period 2. -/
theorem jacobiTheta₂_add_right (z τ : ℂ) : jacobiTheta₂ z (τ + 2) = jacobiTheta₂ z τ :=
  by
  refine tsum_congr (fun n ↦ ?_)
  simp_rw [jacobiTheta₂_term, Complex.exp_add]
  suffices cexp (π * I * n ^ 2 * 2 : ℂ) = 1 by rw [mul_add, Complex.exp_add, this, mul_one]
  rw [(by push_cast; ring : (π * I * n ^ 2 * 2 : ℂ) = (n ^ 2 :) * (2 * π * I)), exp_int_mul, exp_two_pi_mul_I, one_zpow]

Похожие утверждения