English
The derivative θ₂' is odd in z: θ₂'(−z, τ) = − θ₂'(z, τ).
Русский
Производная θ₂' по z нечетна: θ₂'(−z, τ) = − θ₂'(z, τ).
LaTeX
$$$\theta_2'(-z, \tau) = -\theta_2'(z, \tau)$$$
Lean4
theorem jacobiTheta₂'_add_left' (z τ : ℂ) :
jacobiTheta₂' (z + τ) τ = cexp (-π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * π * I * jacobiTheta₂ z τ) :=
by
rcases le_or_gt τ.im 0 with hτ | hτ
· simp_rw [jacobiTheta₂_undef _ hτ, jacobiTheta₂'_undef _ hτ, mul_zero, sub_zero, mul_zero]
have (n : ℤ) :
jacobiTheta₂'_term n (z + τ) τ =
cexp (-π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (n + 1) z τ - 2 * π * I * jacobiTheta₂_term (n + 1) z τ) :=
by
simp only [jacobiTheta₂'_term, jacobiTheta₂_term]
conv_rhs =>
rw [← sub_mul, mul_comm, mul_assoc, ← Complex.exp_add, Int.cast_add, Int.cast_one, mul_add, mul_one,
add_sub_cancel_right]
congr 2
ring
rw [jacobiTheta₂', funext this, tsum_mul_left, ← (Equiv.subRight (1 : ℤ)).tsum_eq]
simp only [jacobiTheta₂, jacobiTheta₂', Equiv.subRight_apply, sub_add_cancel,
(hasSum_jacobiTheta₂'_term z hτ).summable.tsum_sub ((hasSum_jacobiTheta₂_term z hτ).summable.mul_left _),
tsum_mul_left]
