-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma continuousAt_jacobiTheta₂' (z : ℂ) {τ : ℂ} (hτ : 0 < im τ) :
    ContinuousAt (fun p : ℂ × ℂ ↦ jacobiTheta₂' p.1 p.2) (z, τ)

Proof state:
case intro.intro.intro
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : Summable u
⊢ ContinuousOn (fun p => jacobiTheta₂' p.1 p.2) V

Tactic:
refine continuousOn_tsum (fun n ↦ ?_) hu (fun n ⟨z', τ'⟩ ⟨hz', hτ'⟩ ↦ ?_)

Result:
case intro.intro.intro.refine_1
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : Summable u
n : ℤ
⊢ ContinuousOn (fun p => jacobiTheta₂'_term n p.1 p.2) V

case intro.intro.intro.refine_2
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ'✝ : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : Summable u
n : ℤ
x✝¹ : ℂ × ℂ
z' τ' : ℂ
x✝ : (z', τ') ∈ V
hz' : (z', τ').1 ∈ {u | |u.im| < S}
hτ' : (z', τ').2 ∈ {v | T < v.im}
⊢ ‖jacobiTheta₂'_term n (z', τ').1 (z', τ').2‖ ≤ u n

Proof state:
case intro.intro
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
⊢ ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)

Tactic:
obtain ⟨S, hz⟩ := exists_gt |im z|

Result:
case intro.intro.intro
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
⊢ ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)

Proof state:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
⊢ Summable u

Tactic:
simpa only [u, mul_assoc, pow_one]
using (summable_pow_mul_jacobiTheta₂_term_bound S hT 1).mul_left (2 * π)

Result:
no goals

Proof state:
case intro.intro.intro
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
⊢ ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)

Tactic:
have hVo : IsOpen V := ((_root_.continuous_abs.comp continuous_im).isOpen_preimage _
  isOpen_Iio).prod (continuous_im.isOpen_preimage _ isOpen_Ioi)

Result:
case intro.intro.intro
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
⊢ ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)

Proof state:
case intro.intro.intro
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
⊢ ContinuousOn (fun p => jacobiTheta₂' p.1 p.2) V

Tactic:
have hu : Summable u  := by simpa only [u, mul_assoc, pow_one]
    using (summable_pow_mul_jacobiTheta₂_term_bound S hT 1).mul_left (2 * π)

Result:
case intro.intro.intro
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : Summable u
⊢ ContinuousOn (fun p => jacobiTheta₂' p.1 p.2) V

Proof state:
case intro.intro.intro
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
⊢ ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)

Tactic:
refine ContinuousOn.continuousAt ?_ (hVo.mem_nhds ⟨hz, hτ'⟩)

Result:
case intro.intro.intro
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
⊢ ContinuousOn (fun p => jacobiTheta₂' p.1 p.2) V

Proof state:
case intro.intro.intro.refine_1.h
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : Summable u
n : ℤ
⊢ Continuous fun p => jacobiTheta₂'_term n p.1 p.2

Tactic:
unfold jacobiTheta₂'_term jacobiTheta₂_term

Result:
case intro.intro.intro.refine_1.h
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : Summable u
n : ℤ
⊢ Continuous fun p => 2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * p.1 + ↑π * I * ↑n ^ 2 * p.2)

Proof state:
case intro.intro.intro
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
⊢ ContinuousOn (fun p => jacobiTheta₂' p.1 p.2) V

Tactic:
let u (n : ℤ) : ℝ := 2 * π * |n| * rexp (-π * (T * n ^ 2 - 2 * S * |n|))

Result:
case intro.intro.intro
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
⊢ ContinuousOn (fun p => jacobiTheta₂' p.1 p.2) V

Proof state:
z τ : ℂ
hτ : 0 < τ.im
⊢ ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)

Tactic:
obtain ⟨T, hT, hτ'⟩ := exists_between hτ

Result:
case intro.intro
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
⊢ ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)

Proof state:
case intro.intro.intro
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
⊢ ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)

Tactic:
let V := {u | |im u| < S} ×ˢ {v | T < im v}

Result:
case intro.intro.intro
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
⊢ ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (z, τ)

Proof state:
case intro.intro.intro.refine_1
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : Summable u
n : ℤ
⊢ ContinuousOn (fun p => jacobiTheta₂'_term n p.1 p.2) V

Tactic:
apply Continuous.continuousOn

Result:
case intro.intro.intro.refine_1.h
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : Summable u
n : ℤ
⊢ Continuous fun p => jacobiTheta₂'_term n p.1 p.2

Proof state:
case intro.intro.intro.refine_1.h
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : Summable u
n : ℤ
⊢ Continuous fun p => 2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * p.1 + ↑π * I * ↑n ^ 2 * p.2)

Tactic:
fun_prop

Result:
no goals

Proof state:
case intro.intro.intro.refine_2
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ'✝ : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n => 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : Summable u
n : ℤ
x✝¹ : ℂ × ℂ
z' τ' : ℂ
x✝ : (z', τ') ∈ V
hz' : (z', τ').1 ∈ {u | |u.im| < S}
hτ' : (z', τ').2 ∈ {v | T < v.im}
⊢ ‖jacobiTheta₂'_term n (z', τ').1 (z', τ').2‖ ≤ u n

Tactic:
exact norm_jacobiTheta₂'_term_le hT (le_of_lt hz') (le_of_lt hτ') n

Result:
no goals