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

Proof state:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 0 < 3

Tactic:
norm_num

Result:
no goals

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

Tactic:
intro h

Result:
case mp
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term_fderiv x z τ
⊢ Summable fun x => jacobiTheta₂_term x z τ

Proof state:
case h
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term_fderiv x z τ
this✝ : Summable fun x => ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 2⁻¹ ≤ ↑|n| ^ 2

Tactic:
refine (by norm_num : 2⁻¹ ≤ (1 : ℝ)).trans ?_

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

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

Tactic:
refine le_trans ?_ (norm_jacobiTheta₂_term_fderiv_ge n z τ)

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

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

Tactic:
refine mul_le_mul_of_nonneg_left ?_ (mul_pos (by norm_num : 0 < (3 : ℝ)) pi_pos).le

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

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

Tactic:
apply le_mul_of_one_le_left (norm_nonneg _)

Result:
case h
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term_fderiv x z τ
this✝ : Summable fun x => ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ π * ↑|n| ^ 2

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

Tactic:
refine (norm_jacobiTheta₂_term_fderiv_le n z τ).trans
  (?_ : 3 * π * |n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ _)

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

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

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

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

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

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

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

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

Tactic:
intro hτ

Result:
case mpr
z τ : ℂ
hτ : 0 < τ.im
⊢ Summable fun x => jacobiTheta₂_term_fderiv x z τ

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

Tactic:
rw [one_le_sq_iff_one_le_abs, ← Int.cast_abs, abs_abs, ← Int.cast_one, Int.cast_le]

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

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

Tactic:
constructor

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

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

Proof state:
case h
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term_fderiv x z τ
this✝ : Summable fun x => ‖jacobiTheta₂_term_fderiv 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 τ : ℂ
h : Summable fun x => jacobiTheta₂_term_fderiv x z τ
this✝ : Summable fun x => ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ ‖jacobiTheta₂_term_fderiv i z τ‖

Tactic:
filter_upwards [this] with n hn

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

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

Tactic:
simp_rw [mul_assoc (3 * π)]

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

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

Tactic:
refine mul_le_mul_of_nonneg_left ?_ (pow_nonneg (Int.cast_nonneg.mpr (abs_nonneg _)) _)

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

Proof state:
case mp
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term_fderiv x z τ
this : Summable fun x => ‖jacobiTheta₂_term_fderiv x z τ‖
⊢ Summable fun x => jacobiTheta₂_term x z τ

Tactic:
refine this.of_norm_bounded_eventually _ ?_

Result:
case mp
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term_fderiv x z τ
this : Summable fun x => ‖jacobiTheta₂_term_fderiv x z τ‖
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ ‖jacobiTheta₂_term_fderiv i z τ‖

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

Tactic:
exact norm_jacobiTheta₂_term_le hτ le_rfl le_rfl n

Result:
no goals

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

Tactic:
norm_num

Result:
no goals

Proof state:
case mp
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term_fderiv x z τ
⊢ Summable fun x => jacobiTheta₂_term x z τ

Tactic:
have := h.norm

Result:
case mp
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term_fderiv x z τ
this : Summable fun x => ‖jacobiTheta₂_term_fderiv x z τ‖
⊢ Summable fun x => jacobiTheta₂_term x z τ