English
Jacobi theta function with z shifted by 1 is periodic in z: jacobiTheta₂''(z+1,τ) = jacobiTheta₂''(z,τ).
Русский
Функция jacobiTheta₂'' имеет период 1 по переменной z: jacobiTheta₂''(z+1,τ) = jacobiTheta₂''(z,τ).
LaTeX
$$$$\\operatorname{jacobiTheta_2''}(z+1,\\tau) = \\operatorname{jacobiTheta_2''}(z,\\tau).$$$$
Lean4
/-- Restatement of `jacobiTheta₂'_add_left'`: the function `jacobiTheta₂''` is 1-periodic in `z`. -/
theorem jacobiTheta₂''_add_left (z τ : ℂ) : jacobiTheta₂'' (z + 1) τ = jacobiTheta₂'' z τ :=
by
simp only [jacobiTheta₂'', add_mul z 1, one_mul, jacobiTheta₂'_add_left', jacobiTheta₂_add_left']
generalize jacobiTheta₂ (z * τ) τ = J
generalize jacobiTheta₂' (z * τ) τ = J'
simp_rw [div_add' _ _ _ two_pi_I_ne_zero, ← mul_div_assoc]
refine
congr_arg (· / (2 * π * I))
?_
-- get all exponential terms to left
rw [mul_left_comm _ (cexp _), ← mul_add, mul_assoc (cexp _), ← mul_add, ← mul_assoc (cexp _), ← Complex.exp_add]
congrm (cexp ?_ * ?_) <;> ring
