English
The two-variable Jacobi theta function with derivative is continuous at (z,τ) when im τ > 0.
Русский
Двухпеременная функция Джакобиθ₂' непрерывна в точке (z,τ) при im τ > 0.
LaTeX
$$$\text{ContinuousAt}(\lambda p. \theta_2'(p.1,p.2), (z,\tau))$, при $0<\operatorname{Im}\tau$.$$
Lean4
theorem continuousAt_jacobiTheta₂' (z : ℂ) {τ : ℂ} (hτ : 0 < im τ) :
ContinuousAt (fun p : ℂ × ℂ ↦ jacobiTheta₂' p.1 p.2) (z, τ) :=
by
obtain ⟨T, hT, hτ'⟩ := exists_between hτ
obtain ⟨S, hz⟩ := exists_gt |im z|
let V := {u | |im u| < S} ×ˢ {v | T < im v}
have hVo : IsOpen V :=
((_root_.continuous_abs.comp continuous_im).isOpen_preimage _ isOpen_Iio).prod
(continuous_im.isOpen_preimage _ isOpen_Ioi)
refine ContinuousOn.continuousAt ?_ (hVo.mem_nhds ⟨hz, hτ'⟩)
let u (n : ℤ) : ℝ := 2 * π * |n| * rexp (-π * (T * n ^ 2 - 2 * S * |n|))
have hu : Summable u := by
simpa only [u, mul_assoc, pow_one] using (summable_pow_mul_jacobiTheta₂_term_bound S hT 1).mul_left (2 * π)
refine continuousOn_tsum (fun n ↦ ?_) hu (fun n ⟨z', τ'⟩ ⟨hz', hτ'⟩ ↦ ?_)
· apply Continuous.continuousOn
unfold jacobiTheta₂'_term jacobiTheta₂_term
fun_prop
· exact norm_jacobiTheta₂'_term_le hT (le_of_lt hz') (le_of_lt hτ') n
