-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma summable_jacobiTheta₂'_term_iff (z τ : ℂ) :
    Summable (jacobiTheta₂'_term · z τ) ↔ 0 < im τ

Proof state:
case mp
z τ : ℂ
h : Summable fun x => jacobiTheta₂'_term x z τ
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term i z τ‖

Tactic:
have : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0 :=
  Int.cofinite_eq ▸ (mem_sup.mpr ⟨eventually_ne_atBot 0, eventually_ne_atTop 0⟩)

Result:
case mp
z τ : ℂ
h : Summable fun x => jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term i z τ‖

Proof state:
case h
z τ : ℂ
h : Summable fun x => jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ ↑|n|

Tactic:
rw [← Int.cast_one, Int.cast_le]

Result:
case h
z τ : ℂ
h : Summable fun x => jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ |n|

Proof state:
case mp
z τ : ℂ
h : Summable fun x => jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term i z τ‖

Tactic:
filter_upwards [this] with n hn

Result:
case h
z τ : ℂ
h : Summable fun x => jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term n z τ‖

Proof state:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 0 ≤ 2 * π * ↑|n|

Tactic:
positivity

Result:
no goals

Proof state:
z τ : ℂ
⊢ (Summable fun x => jacobiTheta₂'_term x z τ) ↔ 0 < τ.im

Tactic:
constructor

Result:
case mp
z τ : ℂ
⊢ (Summable fun x => jacobiTheta₂'_term x z τ) → 0 < τ.im

case mpr
z τ : ℂ
⊢ 0 < τ.im → Summable fun x => jacobiTheta₂'_term x z τ

Proof state:
case h
z τ : ℂ
h : Summable fun x => jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ (2 * π)⁻¹ * ‖2 * ↑π * I * ↑n‖

Tactic:
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]

Result:
case h
z τ : ℂ
h : Summable fun x => jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ ↑|n|

Proof state:
case mp
z τ : ℂ
⊢ (Summable fun x => jacobiTheta₂'_term x z τ) → Summable fun x => jacobiTheta₂_term x z τ

Tactic:
refine fun h ↦ (h.norm.mul_left (2 * π)⁻¹).of_norm_bounded_eventually _  ?_

Result:
case mp
z τ : ℂ
h : Summable fun x => jacobiTheta₂'_term x z τ
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term i z τ‖

Proof state:
case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖2 * ↑π * I * ↑n‖ * ‖jacobiTheta₂_term n z τ‖ ≤ 2 * π * ↑|n| * rexp (-π * (τ.im * ↑n ^ 2 - 2 * |z.im| * ↑|n|))

Tactic:
refine mul_le_mul (le_of_eq ?_) (norm_jacobiTheta₂_term_le hτ le_rfl le_rfl n)
  (norm_nonneg _) (by positivity)

Result:
case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖2 * ↑π * I * ↑n‖ = 2 * π * ↑|n|

Proof state:
case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖2 * ↑π * I * ↑n‖ = 2 * π * ↑|n|

Tactic:
simp_rw [norm_mul, Complex.norm_two, norm_I, Complex.norm_of_nonneg pi_pos.le,
  norm_intCast, mul_one, Int.cast_abs]

Result:
no goals

Proof state:
case h
z τ : ℂ
h : Summable fun x => jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ |n|

Tactic:
exact Int.one_le_abs hn

Result:
no goals

Proof state:
case mp
z τ : ℂ
⊢ (Summable fun x => jacobiTheta₂'_term x z τ) → 0 < τ.im

Tactic:
rw [← summable_jacobiTheta₂_term_iff (z := z)]

Result:
case mp
z τ : ℂ
⊢ (Summable fun x => jacobiTheta₂'_term x z τ) → Summable fun x => jacobiTheta₂_term x z τ

Proof state:
case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖jacobiTheta₂'_term n z τ‖ ≤ 2 * π * (↑|n| ^ 1 * rexp (-π * (τ.im * ↑n ^ 2 - 2 * |z.im| * ↑|n|)))

Tactic:
rw [jacobiTheta₂'_term, norm_mul, ← mul_assoc, pow_one]

Result:
case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖2 * ↑π * I * ↑n‖ * ‖jacobiTheta₂_term n z τ‖ ≤ 2 * π * ↑|n| * rexp (-π * (τ.im * ↑n ^ 2 - 2 * |z.im| * ↑|n|))

Proof state:
case h
z τ : ℂ
h : Summable fun x => jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term n z τ‖

Tactic:
rw [jacobiTheta₂'_term, norm_mul, ← mul_assoc]

Result:
case h
z τ : ℂ
h : Summable fun x => jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * ‖2 * ↑π * I * ↑n‖ * ‖jacobiTheta₂_term n z τ‖

Proof state:
case mpr
z τ : ℂ
⊢ 0 < τ.im → Summable fun x => jacobiTheta₂'_term x z τ

Tactic:
refine fun hτ ↦ ((summable_pow_mul_jacobiTheta₂_term_bound
  |z.im| hτ 1).mul_left (2 * π)).of_norm_bounded _ (fun n ↦ ?_)

Result:
case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖jacobiTheta₂'_term n z τ‖ ≤ 2 * π * (↑|n| ^ 1 * rexp (-π * (τ.im * ↑n ^ 2 - 2 * |z.im| * ↑|n|)))

Proof state:
case h
z τ : ℂ
h : Summable fun x => jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * ‖2 * ↑π * I * ↑n‖ * ‖jacobiTheta₂_term n z τ‖

Tactic:
refine le_mul_of_one_le_left (norm_nonneg _) ?_

Result:
case h
z τ : ℂ
h : Summable fun x => jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ (2 * π)⁻¹ * ‖2 * ↑π * I * ↑n‖