English
A detailed explicit form of the functional equation for jacobiTheta₂' relating it to jacobiTheta₂'' and a power of −Iτ, up to standard constants.
Русский
Подробная явная форма функционального уравнения для jacobiTheta₂', связанная с jacobiTheta₂'' и степенью от −Iτ с учётом констант.
LaTeX
$$$$\\text{(detailed equation expressing }\\mathrm{jacobiTheta_2'}(z,\\tau) = C(\\tau) \\cdot \\mathrm{jacobiTheta_2''}(z, -1/\\tau) \\text{ with } C(\\tau) = (-2\\pi)/(-i\\tau)^{3/2} ).$$$$
Lean4
theorem jacobiTheta₂'_functional_equation' (z τ : ℂ) :
jacobiTheta₂' z τ = (-2 * π) / (-I * τ) ^ (3 / 2 : ℂ) * jacobiTheta₂'' z (-1 / τ) :=
by
rcases eq_or_ne τ 0 with rfl | hτ
· rw [jacobiTheta₂'_undef _ (by simp), mul_zero, zero_cpow (by simp), div_zero, zero_mul]
have aux1 : (-2 * π : ℂ) / (2 * π * I) = I := by
rw [div_eq_iff two_pi_I_ne_zero, mul_comm I, mul_assoc _ I I, I_mul_I, neg_mul, mul_neg, mul_one]
rw [jacobiTheta₂'_functional_equation, ← mul_one_div _ τ, mul_right_comm _ (cexp _),
(by rw [cpow_one, ← div_div, div_self (neg_ne_zero.mpr I_ne_zero)] : 1 / τ = -I / (-I * τ) ^ (1 : ℂ)),
div_mul_div_comm, ← cpow_add _ _ (mul_ne_zero (neg_ne_zero.mpr I_ne_zero) hτ), ← div_mul_eq_mul_div,
(by norm_num : (1 / 2 + 1 : ℂ) = 3 / 2), mul_assoc (1 / _), mul_assoc (1 / _), ← mul_one_div (-2 * π : ℂ),
mul_comm _ (1 / _), mul_assoc (1 / _)]
congr 1
rw [jacobiTheta₂'', div_add' _ _ _ two_pi_I_ne_zero, ← mul_div_assoc, ← mul_div_assoc, ←
div_mul_eq_mul_div (-2 * π : ℂ), mul_assoc, aux1, mul_div z (-1), mul_neg_one, neg_div τ z, jacobiTheta₂_neg_left,
jacobiTheta₂'_neg_left, neg_mul, ← mul_neg, ← mul_neg, mul_div, mul_neg_one, neg_div, neg_mul, neg_mul, neg_div]
congr 2
rw [neg_sub, ← sub_eq_neg_add, mul_comm _ (_ * I), ← mul_assoc]
