English
The series ∑ jacobiTheta₂_term_fderiv x z τ converges if and only if Im τ > 0.
Русский
Ряд ∑ jacobiTheta₂_term_fderiv x z τ сходится тогда и только тогда, когда Im(τ) > 0.
LaTeX
$$$\sum_{n\in\mathbb{Z}} jacobiTheta_2\_term\_fderiv(n,z,\tau) \quad \text{converges} \iff \Im(\tau) > 0$$$
Lean4
theorem summable_jacobiTheta₂_term_fderiv_iff (z τ : ℂ) : Summable (jacobiTheta₂_term_fderiv · z τ) ↔ 0 < im τ :=
by
constructor
· rw [← summable_jacobiTheta₂_term_iff (z := z)]
intro h
have := h.norm
refine this.of_norm_bounded_eventually ?_
have : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0 :=
Int.cofinite_eq ▸ (mem_sup.mpr ⟨eventually_ne_atBot 0, eventually_ne_atTop 0⟩)
filter_upwards [this] with n hn
refine le_trans ?_ (norm_jacobiTheta₂_term_fderiv_ge n z τ)
apply le_mul_of_one_le_left (norm_nonneg _)
refine one_le_pi_div_two.trans (mul_le_mul_of_nonneg_left ?_ pi_pos.le)
refine (by norm_num : 2⁻¹ ≤ (1 : ℝ)).trans ?_
rw [one_le_sq_iff_one_le_abs, ← Int.cast_abs, abs_abs, ← Int.cast_one, Int.cast_le]
exact Int.one_le_abs hn
· intro hτ
refine ((summable_pow_mul_jacobiTheta₂_term_bound |z.im| hτ 2).mul_left (3 * π)).of_norm_bounded (fun n ↦ ?_)
refine (norm_jacobiTheta₂_term_fderiv_le n z τ).trans (?_ : 3 * π * |n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ _)
simp_rw [mul_assoc (3 * π)]
refine mul_le_mul_of_nonneg_left ?_ (mul_pos (by simp : 0 < (3 : ℝ)) pi_pos).le
refine mul_le_mul_of_nonneg_left ?_ (pow_nonneg (Int.cast_nonneg.mpr (abs_nonneg _)) _)
exact norm_jacobiTheta₂_term_le hτ le_rfl le_rfl n
