English
Differentiable functional equation for θ₂': θ₂'(zτ) relates to θ₂' via explicit factors and combination with θ₂.
Русский
Дифференциальное функциональное уравнение для θ₂': связь между θ₂'(z,τ) и θ₂'(z/τ, -1/τ) через явные множители и комбинацию с θ₂.
LaTeX
$$$\theta_2'(z,\tau) = \frac{1}{(-i\tau)^{1/2}} \cdot e^{ -\pi i z^2/\tau }/\tau \cdot (\theta_2'(z/τ) (-1/τ) - 2\pi i z θ_2(z/τ) (-1/τ)).$$$
Lean4
/-- The functional equation for the derivative of the Jacobi theta function, relating
`jacobiTheta₂' z τ` to `jacobiTheta₂' (z / τ) (-1 / τ)`. This is the key lemma behind the proof of
the functional equation for L-series of odd Dirichlet characters. -/
theorem jacobiTheta₂'_functional_equation (z τ : ℂ) :
jacobiTheta₂' z τ =
1 / (-I * τ) ^ (1 / 2 : ℂ) * cexp (-π * I * z ^ 2 / τ) / τ *
(jacobiTheta₂' (z / τ) (-1 / τ) - 2 * π * I * z * jacobiTheta₂ (z / τ) (-1 / τ)) :=
by
rcases le_or_gt (im τ) 0 with hτ | hτ
·
rw [jacobiTheta₂'_undef z hτ, jacobiTheta₂'_undef, jacobiTheta₂_undef, mul_zero, sub_zero, mul_zero] <;>
rw [neg_div, neg_im, one_div, inv_im, neg_nonpos] <;>
exact div_nonneg (neg_nonneg.mpr hτ) (normSq_nonneg τ)
have hτ' : 0 < (-1 / τ).im :=
by
rw [div_eq_mul_inv, neg_one_mul, neg_im, inv_im, neg_div, neg_neg]
exact div_pos hτ (normSq_pos.mpr (fun h ↦ lt_irrefl 0 (zero_im ▸ h ▸ hτ)))
have hj : HasDerivAt (fun w ↦ jacobiTheta₂ (w / τ) (-1 / τ)) ((1 / τ) * jacobiTheta₂' (z / τ) (-1 / τ)) z :=
by
have := hasDerivAt_jacobiTheta₂_fst (z / τ) hτ'
simpa only [mul_comm, one_div] using this.comp z (hasDerivAt_mul_const τ⁻¹)
calc
_ = deriv (jacobiTheta₂ · τ) z := (hasDerivAt_jacobiTheta₂_fst z hτ).deriv.symm
_ = deriv (fun z ↦ 1 / (-I * τ) ^ (1 / 2 : ℂ) * cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z := by
rw [funext (jacobiTheta₂_functional_equation · τ)]
_ = 1 / (-I * τ) ^ (1 / 2 : ℂ) * deriv (fun z ↦ cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z := by
simp_rw [mul_assoc, deriv_const_mul_field]
_ =
1 / (-I * τ) ^ (1 / 2 : ℂ) *
(deriv (fun z ↦ cexp (-π * I * z ^ 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
cexp (-π * I * z ^ 2 / τ) * deriv (fun z ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z) :=
by
rw [deriv_fun_mul _ hj.differentiableAt]
exact (((differentiableAt_pow 2).const_mul _).mul_const _).cexp
_ = _ := by
rw [hj.deriv]
simp only [div_eq_mul_inv _ τ]
rw [deriv_cexp (((differentiableAt_pow _).const_mul _).mul_const _), mul_comm, deriv_mul_const_field,
deriv_const_mul_field, deriv_pow_field]
ring_nf
