-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma hasFDerivAt_jacobiTheta₂ (z : ℂ) {τ : ℂ} (hτ : 0 < im τ) :
    HasFDerivAt (fun p : ℂ × ℂ ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n => 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
⊢ HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

Tactic:
have hu_sum : Summable u := by
  simp_rw [u, mul_assoc (3 * π)]
  exact (summable_pow_mul_jacobiTheta₂_term_bound S hT 2).mul_left _

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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n => 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
⊢ HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n => 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
⊢ Summable fun n => 3 * π * (↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|)))

Tactic:
exact (summable_pow_mul_jacobiTheta₂_term_bound S hT 2).mul_left _

Result:
no goals

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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n => 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
n : ℤ
p : ℂ × ℂ
hp : p ∈ V
⊢ ‖jacobiTheta₂_term n p.1 p.2‖ ≤ rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))

Tactic:
exact norm_jacobiTheta₂_term_le hT (le_of_lt hp.1) (le_of_lt hp.2) n

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}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n => 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
⊢ HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

Tactic:
have hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n := by
  refine fun n p hp ↦ (norm_jacobiTheta₂_term_fderiv_le n p.1 p.2).trans ?_
  refine mul_le_mul_of_nonneg_left ?_ (by positivity)
  exact norm_jacobiTheta₂_term_le hT (le_of_lt hp.1) (le_of_lt hp.2) 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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n => 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
⊢ HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2
⊢ HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

Tactic:
have hf (n : ℤ) : ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p :=
  fun p _ ↦ hasFDerivAt_jacobiTheta₂_term n p.1 p.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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
⊢ HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (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}
⊢ IsOpen {v | T < v.im}

Tactic:
exact continuous_im.isOpen_preimage _ isOpen_Ioi

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}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n => 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
⊢ HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

Tactic:
have hf_sum : Summable fun n : ℤ ↦ f n (z, τ) := by
  refine (summable_pow_mul_jacobiTheta₂_term_bound S hT 0).of_norm_bounded _ ?_
  simpa only [pow_zero, one_mul] using norm_jacobiTheta₂_term_le hT hz.le hτ'.le

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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n => 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
hf_sum : Summable fun n => f n (z, τ)
⊢ HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
⊢ HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

Tactic:
let f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2
⊢ HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)