jacobiTheta₂_add_left' — Mathlib

English

A quasi-periodicity in z: θ₂(z+τ, τ) = exp(-π i (τ+2z)) θ₂(z, τ).

Русский

Квазипериодичность по z: θ₂(z+τ, τ) = e^{-π i (τ+2z)} θ₂(z, τ).

LaTeX

$$$\theta_2(z+\tau, \tau) = e^{-\pi i (\tau + 2 z)} \theta_2(z, \tau)$$$

Lean4

/-- The two-variable Jacobi theta function is quasi-periodic in `z` with period `τ`. -/
theorem jacobiTheta₂_add_left' (z τ : ℂ) : jacobiTheta₂ (z + τ) τ = cexp (-π * I * (τ + 2 * z)) * jacobiTheta₂ z τ :=
  by
  conv_rhs => rw [jacobiTheta₂, ← tsum_mul_left, ← (Equiv.addRight 1).tsum_eq]
  refine tsum_congr (fun n ↦ ?_)
  simp_rw [jacobiTheta₂_term, ← Complex.exp_add, Equiv.coe_addRight, Int.cast_add]
  ring_nf

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