jacobiTheta₂_neg_left — Mathlib

English

Derivative quasi-periodicity: θ₂'(z+τ, τ) = e^{-π i (τ+2z)} [θ₂'(z, τ) − 2π i z θ₂(z, τ)].

Русский

Производная по z имеет квазипериодичность: θ₂'(z+τ, τ) = e^{-π i (τ+2z)} [θ₂'(z, τ) − 2π i z θ₂(z, τ)].

LaTeX

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

Lean4

/-- The two-variable Jacobi theta function is even in `z`. -/
@[simp]
theorem jacobiTheta₂_neg_left (z τ : ℂ) : jacobiTheta₂ (-z) τ = jacobiTheta₂ z τ :=
  by
  conv_lhs => rw [jacobiTheta₂, ← Equiv.tsum_eq (Equiv.neg ℤ)]
  refine tsum_congr (fun n ↦ ?_)
  simp_rw [jacobiTheta₂_term, Equiv.neg_apply, Int.cast_neg, neg_sq, mul_assoc, neg_mul_neg]

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