English
The same criterion as above; Summable (jacobiTheta₂_term_fderiv · z τ) iff Im τ > 0.
Русский
То же условие; суммируемость (jacobiTheta₂_term_fderiv · z τ) эквивалентна Im τ > 0.
LaTeX
$$$\operatorname{Summable}(\lambda n.\ jacobiTheta_2\_term\_fderiv(n,z,\tau))) \;\Leftrightarrow \Im(\tau) > 0$$$
Lean4
theorem summable_jacobiTheta₂'_term_iff (z τ : ℂ) : Summable (jacobiTheta₂'_term · z τ) ↔ 0 < im τ :=
by
constructor
· rw [← summable_jacobiTheta₂_term_iff (z := z)]
refine fun h ↦ (h.norm.mul_left (2 * π)⁻¹).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
rw [jacobiTheta₂'_term, norm_mul, ← mul_assoc]
refine le_mul_of_one_le_left (norm_nonneg _) ?_
simp_rw [norm_mul, norm_I, norm_real, mul_one, norm_of_nonneg pi_pos.le, ← ofReal_ofNat, norm_real,
norm_of_nonneg two_pos.le, ← ofReal_intCast, norm_real, Real.norm_eq_abs, ← Int.cast_abs, ← mul_assoc _ (2 * π),
inv_mul_cancel₀ (mul_pos two_pos pi_pos).ne', one_mul]
rw [← Int.cast_one, Int.cast_le]
exact Int.one_le_abs hn
· refine fun hτ ↦
((summable_pow_mul_jacobiTheta₂_term_bound |z.im| hτ 1).mul_left (2 * π)).of_norm_bounded (fun n ↦ ?_)
rw [jacobiTheta₂'_term, norm_mul, ← mul_assoc, pow_one]
refine mul_le_mul (le_of_eq ?_) (norm_jacobiTheta₂_term_le hτ le_rfl le_rfl n) (norm_nonneg _) (by positivity)
simp_rw [norm_mul, Complex.norm_two, norm_I, Complex.norm_of_nonneg pi_pos.le, norm_intCast, mul_one, Int.cast_abs]
