-- 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:
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im < 0
this : Tendsto (fun n => ‖jacobiTheta₂_term (↑n) z τ‖) atTop atTop
h : Tendsto (fun x => ‖((fun x => jacobiTheta₂_term x z τ) ∘ fun a => ↑a) x‖) atTop (𝓝 ‖0‖)
⊢ False

Tactic:
exact atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop _) this)

Result:
no goals

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

Tactic:
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τ))

Result:
no goals

Proof state:
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

Tactic:
simp_rw [Function.comp_def, Int.cast_neg, Int.cast_natCast, mul_neg, neg_mul, neg_neg] at h

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)) atTop (𝓝 0)
⊢ False

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

Tactic:
ring

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 => 2 * (π * (↑x * z.im))) atTop atBot

Tactic:
apply Filter.Tendsto.const_mul_atBot two_pos

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 => π * (↑x * z.im)) atTop atBot

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 * (↑n * (-π * τ.im) - 2 * π * z.im))) atTop atTop

Tactic:
refine tendsto_exp_atTop.comp (tendsto_natCast_atTop_atTop.atTop_mul_atTop₀ ?_)

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

Proof state:
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)) atTop (𝓝 0)
⊢ False

Tactic:
refine atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop 0) ?_)

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)) atTop (𝓝 0)
⊢ Tendsto (fun x => rexp (2 * π * ↑x * z.im)) atTop atTop

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)
⊢ False

Tactic:
refine atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop 0) ?_)

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 => rexp (-(2 * π * ↑x * z.im))) atTop atTop

Proof state:
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term x z τ
hτ✝ : τ.im ≤ 0
hτ : τ.im < 0
this : Tendsto (fun n => ‖jacobiTheta₂_term (↑n) z τ‖) atTop atTop
⊢ False

Tactic:
replace h := (h.comp_injective (fun a b ↦ Int.ofNat_inj.mp)).tendsto_atTop_zero.norm

Result:
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im < 0
this : Tendsto (fun n => ‖jacobiTheta₂_term (↑n) z τ‖) atTop atTop
h : Tendsto (fun x => ‖((fun x => jacobiTheta₂_term x z τ) ∘ fun a => ↑a) x‖) atTop (𝓝 ‖0‖)
⊢ False

Proof state:
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)) atTop (𝓝 0)
⊢ Tendsto (fun x => rexp (2 * π * ↑x * z.im)) atTop atTop

Tactic:
exact tendsto_exp_atTop.comp ((tendsto_natCast_atTop_atTop.const_mul_atTop
  (mul_pos two_pos pi_pos)).atTop_mul_const hz)

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 => π * (↑x * z.im)) atTop atBot

Tactic:
exact (tendsto_natCast_atTop_atTop.atTop_mul_const_of_neg hz).const_mul_atBot pi_pos

Result:
no goals

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

Tactic:
refine Iff.symm ⟨fun hτ ↦ ?_, fun h ↦ ?_⟩

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

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

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

Tactic:
simp_rw [← summable_norm_iff (E := ℂ), norm_jacobiTheta₂_term, hτ, mul_zero, zero_sub] at h

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

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

Tactic:
rcases lt_or_eq_of_le hτ with hτ | hτ

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

case refine_2.inr
z τ : ℂ
h : Summable fun x => jacobiTheta₂_term x z τ
hτ✝ : τ.im ≤ 0
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
⊢ False

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

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

Proof state:
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

Tactic:
revert h

Result:
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

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

Tactic:
simp only [norm_zero, Function.comp_def, norm_jacobiTheta₂_term, Int.cast_natCast]

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 ^ 2 * τ.im - 2 * π * ↑n * z.im)) atTop atTop

Proof state:
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

Tactic:
replace h := (h.comp_injective (fun a b ↦ Int.ofNat_inj.mp)).tendsto_atTop_zero

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))) ∘ fun a => ↑a) atTop (𝓝 0)
⊢ 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))) atTop (𝓝 0)
⊢ Tendsto (fun x => -(2 * π * ↑x * z.im)) atTop atTop

Tactic:
simp only [tendsto_neg_atTop_iff, mul_assoc]

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 atBot