English
The series defining jacobiTheta₂_term over n ∈ ℤ converges if and only if Im(τ) > 0.
Русский
Ряд, задающий jacobiTheta₂_term по n ∈ ℤ, сходится тогда и только тогда, когда Im(τ) > 0.
LaTeX
$$$\sum_{n\in\mathbb{Z}} \jacobiTheta_2\_term(n,z,\tau)\quad \text{converges} \iff \Im(\tau) > 0$$$
Lean4
/-- The series defining the theta function is summable if and only if `0 < im τ`. -/
theorem summable_jacobiTheta₂_term_iff (z τ : ℂ) : Summable (jacobiTheta₂_term · z τ) ↔ 0 < im τ := by
-- NB. This is a statement of no great mathematical interest; it is included largely to avoid
-- having to impose `0 < im τ` as a hypothesis on many later lemmas.
refine
Iff.symm
⟨fun hτ ↦ ?_, fun h ↦ ?_⟩ -- do quicker implication first!
· refine (summable_pow_mul_jacobiTheta₂_term_bound |im z| hτ 0).of_norm_bounded ?_
simpa only [pow_zero, one_mul] using norm_jacobiTheta₂_term_le hτ le_rfl le_rfl
· by_contra! hτ
rcases lt_or_eq_of_le hτ with hτ | hτ
· -- easy case `im τ < 0`
suffices Tendsto (fun n : ℕ ↦ ‖jacobiTheta₂_term (↑n) z τ‖) atTop atTop
by
replace h := (h.comp_injective (fun a b ↦ Int.ofNat_inj.mp)).tendsto_atTop_zero.norm
exact atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop _) this)
simp only [norm_jacobiTheta₂_term, Int.cast_natCast]
conv =>
enter [1, n]
rw [show -π * n ^ 2 * τ.im - 2 * π * n * z.im = n * (n * (-π * τ.im) - 2 * π * z.im) by ring]
refine tendsto_exp_atTop.comp (tendsto_natCast_atTop_atTop.atTop_mul_atTop₀ ?_)
exact
tendsto_atTop_add_const_right _ _
(tendsto_natCast_atTop_atTop.atTop_mul_const (mul_pos_of_neg_of_neg (neg_lt_zero.mpr pi_pos) hτ))
· -- case im τ = 0: 3-way split according to `im z`
simp_rw [← summable_norm_iff (E := ℂ), norm_jacobiTheta₂_term, hτ, mul_zero, zero_sub] at h
rcases lt_trichotomy (im z) 0 with hz | hz | hz
· replace h := (h.comp_injective (fun a b ↦ Int.ofNat_inj.mp)).tendsto_atTop_zero
simp_rw [Function.comp_def, Int.cast_natCast] at h
refine atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop 0) ?_)
refine tendsto_exp_atTop.comp ?_
simp only [tendsto_neg_atTop_iff, mul_assoc]
apply Filter.Tendsto.const_mul_atBot two_pos
exact (tendsto_natCast_atTop_atTop.atTop_mul_const_of_neg hz).const_mul_atBot pi_pos
· revert h
simpa only [hz, mul_zero, neg_zero, Real.exp_zero, summable_const_iff] using one_ne_zero
· have : ((-↑·) : ℕ → ℤ).Injective := fun _ _ ↦ by simp only [neg_inj, Nat.cast_inj, imp_self]
replace h := (h.comp_injective this).tendsto_atTop_zero
simp_rw [Function.comp_def, Int.cast_neg, Int.cast_natCast, mul_neg, neg_mul, neg_neg] at h
refine atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop 0) ?_)
exact
tendsto_exp_atTop.comp
((tendsto_natCast_atTop_atTop.const_mul_atTop (mul_pos two_pos pi_pos)).atTop_mul_const hz)
