-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
/-- The series defining the theta function is summable if and only if `0 < im τ`. -/
lemma summable_jacobiTheta₂_term_iff (z τ : ℂ) : Summable (jacobiTheta₂_term · z τ) ↔ 0 < im τ

Proof state:
case refine_2.inr
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x => rexp (-(2 * π * ↑x * z.im))
⊢ False

Tactic:
rcases lt_trichotomy (im z) 0 with hz | hz | hz

Result:
case refine_2.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x => rexp (-(2 * π * ↑x * z.im))
hz : z.im < 0
⊢ False

case refine_2.inr.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x => rexp (-(2 * π * ↑x * z.im))
hz : z.im = 0
⊢ False

case refine_2.inr.inr.inr
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x => rexp (-(2 * π * ↑x * z.im))
hz : 0 < z.im
⊢ False

Proof state:
case refine_2.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto ((fun x => rexp (-(2 * π * ↑x * z.im))) ∘ fun a => ↑a) atTop (𝓝 0)
⊢ False

Tactic:
simp_rw [Function.comp_def, Int.cast_natCast] at h

Result:
case refine_2.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (fun x => rexp (-(2 * π * ↑x * z.im))) atTop (𝓝 0)
⊢ False

Proof state:
case refine_2.inr.inr.inr
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x => rexp (-(2 * π * ↑x * z.im))
hz : 0 < z.im
this : Function.Injective fun x => -↑x
⊢ False

Tactic:
replace h := (h.comp_injective this).tendsto_atTop_zero

Result:
case refine_2.inr.inr.inr
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
hz : 0 < z.im
this : Function.Injective fun x => -↑x
h : Tendsto ((fun x => rexp (-(2 * π * ↑x * z.im))) ∘ fun x => -↑x) atTop (𝓝 0)
⊢ False

Proof state:
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x => rexp (-(2 * π * ↑x * z.im))
hz : 0 < z.im
x✝¹ x✝ : ℕ
⊢ (fun x => -↑x) x✝¹ = (fun x => -↑x) x✝ → x✝¹ = x✝

Tactic:
simp only [neg_inj, Nat.cast_inj, imp_self]

Result:
no goals

Proof state:
case refine_2.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (fun x => rexp (-(2 * π * ↑x * z.im))) atTop (𝓝 0)
⊢ Tendsto (fun x => rexp (-(2 * π * ↑x * z.im))) atTop atTop

Tactic:
refine tendsto_exp_atTop.comp ?_

Result:
case refine_2.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (fun x => rexp (-(2 * π * ↑x * z.im))) atTop (𝓝 0)
⊢ Tendsto (fun x => -(2 * π * ↑x * z.im)) atTop atTop

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

Tactic:
simpa only [pow_zero, one_mul] using norm_jacobiTheta₂_term_le hτ le_rfl le_rfl

Result:
no goals

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

Tactic:
by_contra! hτ

Result:
case refine_2
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term x z τ
hτ : τ.im ≤ 0
⊢ False

Proof state:
case refine_2.inl
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term x z τ
hτ✝ : τ.im ≤ 0
hτ : τ.im < 0
⊢ Tendsto (fun n => rexp (-π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im)) atTop atTop

Tactic:
conv =>
  enter [1, n]
  rw [show -π * n ^ 2 * τ.im - 2 * π * n * z.im =
        n * (n * (-π * τ.im) - 2 * π * z.im) by ring]

Result:
case refine_2.inl
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term x z τ
hτ✝ : τ.im ≤ 0
hτ : τ.im < 0
⊢ Tendsto (fun n => rexp (↑n * (↑n * (-π * τ.im) - 2 * π * z.im))) atTop atTop

Proof state:
case refine_2.inr.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im = 0
⊢ (Summable fun x => rexp (-(2 * π * ↑x * z.im))) → False

Tactic:
simpa only [hz, mul_zero, neg_zero, Real.exp_zero, summable_const_iff] using one_ne_zero

Result:
no goals

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

Tactic:
refine (summable_pow_mul_jacobiTheta₂_term_bound |im z| hτ 0).of_norm_bounded _ ?_

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