[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
⊢ ‖cexp (↑π * I * ↑n ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ Int.natAbs n
[PROOFSTEP]
let y := rexp (-π * z.im)
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
⊢ ‖cexp (↑π * I * ↑n ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ Int.natAbs n
[PROOFSTEP]
have h : y < 1 := exp_lt_one_iff.mpr (mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hz)
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ ‖cexp (↑π * I * ↑n ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ Int.natAbs n
[PROOFSTEP]
refine' (le_of_eq _).trans (_ : y ^ n ^ 2 ≤ _)
[GOAL]
case refine'_1
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ ‖cexp (↑π * I * ↑n ^ 2 * z)‖ = y ^ n ^ 2
[PROOFSTEP]
rw [Complex.norm_eq_abs, Complex.abs_exp]
[GOAL]
case refine'_1
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ rexp (↑π * I * ↑n ^ 2 * z).re = y ^ n ^ 2
[PROOFSTEP]
have : (↑π * I * (n : ℂ) ^ 2 * z).re = -π * z.im * (n : ℝ) ^ 2 :=
  by
  rw [(by push_cast ; ring : ↑π * I * (n : ℂ) ^ 2 * z = ↑(π * (n : ℝ) ^ 2) * (z * I)), ofReal_mul_re, mul_I_re]
  ring
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ (↑π * I * ↑n ^ 2 * z).re = -π * z.im * ↑n ^ 2
[PROOFSTEP]
rw [(by push_cast ; ring : ↑π * I * (n : ℂ) ^ 2 * z = ↑(π * (n : ℝ) ^ 2) * (z * I)), ofReal_mul_re, mul_I_re]
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ ↑π * I * ↑n ^ 2 * z = ↑(π * ↑n ^ 2) * (z * I)
[PROOFSTEP]
push_cast
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ ↑π * I * ↑n ^ 2 * z = ↑π * ↑n ^ 2 * (z * I)
[PROOFSTEP]
ring
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ π * ↑n ^ 2 * -z.im = -π * z.im * ↑n ^ 2
[PROOFSTEP]
ring
[GOAL]
case refine'_1
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
this : (↑π * I * ↑n ^ 2 * z).re = -π * z.im * ↑n ^ 2
⊢ rexp (↑π * I * ↑n ^ 2 * z).re = y ^ n ^ 2
[PROOFSTEP]
obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (sq_nonneg n)
[GOAL]
case refine'_1.intro
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
this : (↑π * I * ↑n ^ 2 * z).re = -π * z.im * ↑n ^ 2
m : ℕ
hm : n ^ 2 = ↑m
⊢ rexp (↑π * I * ↑n ^ 2 * z).re = y ^ n ^ 2
[PROOFSTEP]
rw [this, exp_mul, ← Int.cast_pow, rpow_int_cast, hm, zpow_ofNat]
[GOAL]
case refine'_2
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ y ^ n ^ 2 ≤ rexp (-π * z.im) ^ Int.natAbs n
[PROOFSTEP]
have : n ^ 2 = ↑(n.natAbs ^ 2) := by rw [Nat.cast_pow, Int.natAbs_sq]
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ n ^ 2 = ↑(Int.natAbs n ^ 2)
[PROOFSTEP]
rw [Nat.cast_pow, Int.natAbs_sq]
[GOAL]
case refine'_2
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
this : n ^ 2 = ↑(Int.natAbs n ^ 2)
⊢ y ^ n ^ 2 ≤ rexp (-π * z.im) ^ Int.natAbs n
[PROOFSTEP]
rw [this, zpow_ofNat]
[GOAL]
case refine'_2
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
this : n ^ 2 = ↑(Int.natAbs n ^ 2)
⊢ y ^ Int.natAbs n ^ 2 ≤ rexp (-π * z.im) ^ Int.natAbs n
[PROOFSTEP]
exact pow_le_pow_of_le_one (exp_pos _).le h.le ((sq n.natAbs).symm ▸ n.natAbs.le_mul_self)
[GOAL]
R : ℝ
hR : 0 < R
⊢ ∃ bd, Summable bd ∧ ∀ {τ : ℂ}, R ≤ τ.im → ∀ (n : ℤ), ‖cexp (↑π * I * ↑n ^ 2 * τ)‖ ≤ bd n
[PROOFSTEP]
let y := rexp (-π * R)
[GOAL]
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
⊢ ∃ bd, Summable bd ∧ ∀ {τ : ℂ}, R ≤ τ.im → ∀ (n : ℤ), ‖cexp (↑π * I * ↑n ^ 2 * τ)‖ ≤ bd n
[PROOFSTEP]
have h : y < 1 := exp_lt_one_iff.mpr (mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hR)
[GOAL]
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
⊢ ∃ bd, Summable bd ∧ ∀ {τ : ℂ}, R ≤ τ.im → ∀ (n : ℤ), ‖cexp (↑π * I * ↑n ^ 2 * τ)‖ ≤ bd n
[PROOFSTEP]
refine' ⟨fun n => y ^ n.natAbs, summable_int_of_summable_nat _ _, fun hτ n => _⟩
[GOAL]
case refine'_1
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
⊢ Summable fun n => y ^ Int.natAbs ↑n
case refine'_2
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
⊢ Summable fun n => y ^ Int.natAbs (-↑n)
case refine'_3
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
τ✝ : ℂ
hτ : R ≤ τ✝.im
n : ℤ
⊢ ‖cexp (↑π * I * ↑n ^ 2 * τ✝)‖ ≤ (fun n => y ^ Int.natAbs n) n
[PROOFSTEP]
pick_goal 3
[GOAL]
case refine'_3
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
τ✝ : ℂ
hτ : R ≤ τ✝.im
n : ℤ
⊢ ‖cexp (↑π * I * ↑n ^ 2 * τ✝)‖ ≤ (fun n => y ^ Int.natAbs n) n
[PROOFSTEP]
refine' (norm_exp_mul_sq_le (hR.trans_le hτ) n).trans _
[GOAL]
case refine'_3
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
τ✝ : ℂ
hτ : R ≤ τ✝.im
n : ℤ
⊢ rexp (-π * τ✝.im) ^ Int.natAbs n ≤ (fun n => y ^ Int.natAbs n) n
[PROOFSTEP]
refine' pow_le_pow_of_le_left (exp_pos _).le (Real.exp_le_exp.mpr _) _
[GOAL]
case refine'_3
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
τ✝ : ℂ
hτ : R ≤ τ✝.im
n : ℤ
⊢ -π * τ✝.im ≤ -π * R
[PROOFSTEP]
rwa [mul_le_mul_left_of_neg (neg_lt_zero.mpr pi_pos)]
[GOAL]
case refine'_1
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
⊢ Summable fun n => y ^ Int.natAbs ↑n
case refine'_2 R : ℝ hR : 0 < R y : ℝ := rexp (-π * R) h : y < 1 ⊢ Summable fun n => y ^ Int.natAbs (-↑n)
[PROOFSTEP]
all_goals simpa only [Int.natAbs_neg, Int.natAbs_ofNat] using summable_geometric_of_lt_1 (Real.exp_pos _).le h
[GOAL]
case refine'_1
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
⊢ Summable fun n => y ^ Int.natAbs ↑n
[PROOFSTEP]
simpa only [Int.natAbs_neg, Int.natAbs_ofNat] using summable_geometric_of_lt_1 (Real.exp_pos _).le h
[GOAL]
case refine'_2
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
⊢ Summable fun n => y ^ Int.natAbs (-↑n)
[PROOFSTEP]
simpa only [Int.natAbs_neg, Int.natAbs_ofNat] using summable_geometric_of_lt_1 (Real.exp_pos _).le h
[GOAL]
z : ℂ
⊢ jacobiTheta (2 + z) = jacobiTheta z
[PROOFSTEP]
refine' tsum_congr fun n => _
[GOAL]
z : ℂ
n : ℤ
⊢ cexp (↑π * I * ↑n ^ 2 * (2 + z)) = cexp (↑π * I * ↑n ^ 2 * z)
[PROOFSTEP]
suffices cexp (↑π * I * (n : ℂ) ^ 2 * 2) = 1 by rw [mul_add, Complex.exp_add, this, one_mul]
[GOAL]
z : ℂ
n : ℤ
this : cexp (↑π * I * ↑n ^ 2 * 2) = 1
⊢ cexp (↑π * I * ↑n ^ 2 * (2 + z)) = cexp (↑π * I * ↑n ^ 2 * z)
[PROOFSTEP]
rw [mul_add, Complex.exp_add, this, one_mul]
[GOAL]
z : ℂ
n : ℤ
⊢ cexp (↑π * I * ↑n ^ 2 * 2) = 1
[PROOFSTEP]
rw [(by push_cast ; ring : ↑π * I * ↑n ^ 2 * 2 = ↑(n ^ 2) * (2 * π * I)), Complex.exp_int_mul, Complex.exp_two_pi_mul_I,
  one_zpow]
[GOAL]
z : ℂ
n : ℤ
⊢ ↑π * I * ↑n ^ 2 * 2 = ↑(n ^ 2) * (2 * ↑π * I)
[PROOFSTEP]
push_cast
[GOAL]
z : ℂ
n : ℤ
⊢ ↑π * I * ↑n ^ 2 * 2 = ↑n ^ 2 * (2 * ↑π * I)
[PROOFSTEP]
ring
[GOAL]
τ : ℍ
⊢ jacobiTheta ↑(ModularGroup.T ^ 2 • τ) = jacobiTheta ↑τ
[PROOFSTEP]
suffices ↑(ModularGroup.T ^ 2 • τ) = (2 : ℂ) + ↑τ by simp_rw [this, jacobiTheta_two_add]
[GOAL]
τ : ℍ
this : ↑(ModularGroup.T ^ 2 • τ) = 2 + ↑τ
⊢ jacobiTheta ↑(ModularGroup.T ^ 2 • τ) = jacobiTheta ↑τ
[PROOFSTEP]
simp_rw [this, jacobiTheta_two_add]
[GOAL]
τ : ℍ
⊢ ↑(ModularGroup.T ^ 2 • τ) = 2 + ↑τ
[PROOFSTEP]
have : ModularGroup.T ^ (2 : ℕ) = ModularGroup.T ^ (2 : ℤ) := by rfl
[GOAL]
τ : ℍ
⊢ ModularGroup.T ^ 2 = ModularGroup.T ^ 2
[PROOFSTEP]
rfl
[GOAL]
τ : ℍ
this : ModularGroup.T ^ 2 = ModularGroup.T ^ 2
⊢ ↑(ModularGroup.T ^ 2 • τ) = 2 + ↑τ
[PROOFSTEP]
simp_rw [this, UpperHalfPlane.modular_T_zpow_smul, UpperHalfPlane.coe_vadd]
[GOAL]
τ : ℍ
this : ModularGroup.T ^ 2 = ModularGroup.T ^ 2
⊢ ↑↑2 + ↑τ = 2 + ↑τ
[PROOFSTEP]
norm_cast
[GOAL]
τ : ℍ
⊢ jacobiTheta ↑(ModularGroup.S • τ) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ
[PROOFSTEP]
unfold jacobiTheta
[GOAL]
τ : ℍ
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑(ModularGroup.S • τ)) =
    (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
rw [UpperHalfPlane.modular_S_smul, UpperHalfPlane.coe_mk]
[GOAL]
τ : ℍ
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
have ha : 0 < (-I * τ).re :=
  by
  rw [neg_mul, neg_re, mul_re, I_re, I_im, zero_mul, one_mul, zero_sub, neg_neg]
  exact τ.im_pos
[GOAL]
τ : ℍ
⊢ 0 < (-I * ↑τ).re
[PROOFSTEP]
rw [neg_mul, neg_re, mul_re, I_re, I_im, zero_mul, one_mul, zero_sub, neg_neg]
[GOAL]
τ : ℍ
⊢ 0 < (↑τ).im
[PROOFSTEP]
exact τ.im_pos
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
have ha' : (-I * τ) ^ (1 / 2 : ℂ) ≠ 0 := by
  rw [Ne.def, cpow_eq_zero_iff]
  contrapose! ha
  rw [ha.1, zero_re]
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
⊢ (-I * ↑τ) ^ (1 / 2) ≠ 0
[PROOFSTEP]
rw [Ne.def, cpow_eq_zero_iff]
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
⊢ ¬(-I * ↑τ = 0 ∧ 1 / 2 ≠ 0)
[PROOFSTEP]
contrapose! ha
[GOAL]
τ : ℍ
ha : -I * ↑τ = 0 ∧ 1 / 2 ≠ 0
⊢ (-I * ↑τ).re ≤ 0
[PROOFSTEP]
rw [ha.1, zero_re]
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
have hτ : (τ : ℂ) ≠ 0 := τ.ne_zero
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
have := Complex.tsum_exp_neg_mul_int_sq ha
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
this :
  ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2) = 1 / (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / (-I * ↑τ) * ↑n ^ 2)
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
rw [mul_comm ((1 : ℂ) / _) _, mul_one_div, eq_div_iff ha', mul_comm _ (_ ^ _), eq_comm] at this 
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
this : ∑' (n : ℤ), cexp (-↑π / (-I * ↑τ) * ↑n ^ 2) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
have expo1 : ∀ n : ℤ, -↑π / (-I * ↑τ) * (n : ℂ) ^ 2 = ↑π * I * (n : ℂ) ^ 2 * (-↑τ)⁻¹ :=
  by
  intro n
  field_simp [hτ, I_ne_zero]
  ring_nf
  rw [I_sq, mul_neg, mul_one, neg_neg]
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
this : ∑' (n : ℤ), cexp (-↑π / (-I * ↑τ) * ↑n ^ 2) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
⊢ ∀ (n : ℤ), -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
[PROOFSTEP]
intro n
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
this : ∑' (n : ℤ), cexp (-↑π / (-I * ↑τ) * ↑n ^ 2) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
n : ℤ
⊢ -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
[PROOFSTEP]
field_simp [hτ, I_ne_zero]
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
this : ∑' (n : ℤ), cexp (-↑π / (-I * ↑τ) * ↑n ^ 2) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
n : ℤ
⊢ ↑π * ↑n ^ 2 * ↑τ = -(↑π * I * ↑n ^ 2 * (I * ↑τ))
[PROOFSTEP]
ring_nf
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
this : ∑' (n : ℤ), cexp (-↑π / (-I * ↑τ) * ↑n ^ 2) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
n : ℤ
⊢ ↑π * ↑n ^ 2 * ↑τ = -(↑π * ↑n ^ 2 * ↑τ * I ^ 2)
[PROOFSTEP]
rw [I_sq, mul_neg, mul_one, neg_neg]
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
this : ∑' (n : ℤ), cexp (-↑π / (-I * ↑τ) * ↑n ^ 2) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
expo1 : ∀ (n : ℤ), -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
simp_rw [expo1] at this 
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
expo1 : ∀ (n : ℤ), -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
this : ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
have expo2 : ∀ n : ℤ, -↑π * (-I * ↑τ) * (n : ℂ) ^ 2 = ↑π * I * (n : ℂ) ^ 2 * ↑τ :=
  by
  intro n
  ring_nf
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
expo1 : ∀ (n : ℤ), -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
this : ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
⊢ ∀ (n : ℤ), -↑π * (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * ↑τ
[PROOFSTEP]
intro n
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
expo1 : ∀ (n : ℤ), -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
this : ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
n : ℤ
⊢ -↑π * (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * ↑τ
[PROOFSTEP]
ring_nf
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
expo1 : ∀ (n : ℤ), -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
this : ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
expo2 : ∀ (n : ℤ), -↑π * (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * ↑τ
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
simp_rw [expo2] at this 
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
expo1 : ∀ (n : ℤ), -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
expo2 : ∀ (n : ℤ), -↑π * (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * ↑τ
this : ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
exact this
[GOAL]
z : ℂ
hz : 0 < z.im
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * z)) ((jacobiTheta z - 1) / 2)
[PROOFSTEP]
have := (summable_exp_mul_sq hz).hasSum.sum_nat_of_sum_int
[GOAL]
z : ℂ
hz : 0 < z.im
this :
  HasSum (fun n => cexp (↑π * I * ↑↑n ^ 2 * z) + cexp (↑π * I * ↑(-↑n) ^ 2 * z))
    (∑' (b : ℤ), cexp (↑π * I * ↑b ^ 2 * z) + cexp (↑π * I * ↑0 ^ 2 * z))
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * z)) ((jacobiTheta z - 1) / 2)
[PROOFSTEP]
rw [← @hasSum_nat_add_iff' ℂ _ _ _ _ 1] at this 
[GOAL]
z : ℂ
hz : 0 < z.im
this :
  HasSum (fun n => cexp (↑π * I * ↑↑(n + 1) ^ 2 * z) + cexp (↑π * I * ↑(-↑(n + 1)) ^ 2 * z))
    (∑' (b : ℤ), cexp (↑π * I * ↑b ^ 2 * z) + cexp (↑π * I * ↑0 ^ 2 * z) -
      ∑ i in Finset.range 1, (cexp (↑π * I * ↑↑i ^ 2 * z) + cexp (↑π * I * ↑(-↑i) ^ 2 * z)))
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * z)) ((jacobiTheta z - 1) / 2)
[PROOFSTEP]
simp_rw [Finset.sum_range_one, Int.cast_neg, Int.cast_ofNat, Nat.cast_zero, neg_zero, Int.cast_zero, sq (0 : ℂ),
  mul_zero, zero_mul, neg_sq, ← mul_two, Complex.exp_zero, add_sub_assoc, (by norm_num : (1 : ℂ) - 1 * 2 = -1), ←
  sub_eq_add_neg, Nat.cast_add, Nat.cast_one] at this 
[GOAL]
z : ℂ
hz : 0 < z.im
this : HasSum (fun n => cexp (↑π * I * ↑(n + 1) ^ 2 * z) * 2) (∑' (b : ℤ), cexp (↑π * I * ↑b ^ 2 * z) + (1 - 1 * 2))
⊢ 1 - 1 * 2 = -1
[PROOFSTEP]
norm_num
[GOAL]
z : ℂ
hz : 0 < z.im
this : HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * z) * 2) (∑' (b : ℤ), cexp (↑π * I * ↑b ^ 2 * z) - 1)
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * z)) ((jacobiTheta z - 1) / 2)
[PROOFSTEP]
convert this.div_const 2 using 1
[GOAL]
case h.e'_5
z : ℂ
hz : 0 < z.im
this : HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * z) * 2) (∑' (b : ℤ), cexp (↑π * I * ↑b ^ 2 * z) - 1)
⊢ (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * z)) = fun i => cexp (↑π * I * (↑i + 1) ^ 2 * z) * 2 / 2
[PROOFSTEP]
simp_rw [mul_div_cancel (G₀ := ℂ) _ two_ne_zero]
[GOAL]
z : ℂ
hz : 0 < z.im
⊢ jacobiTheta z = 1 + 2 * ∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)
[PROOFSTEP]
rw [(hasSum_nat_jacobiTheta hz).tsum_eq, mul_div_cancel' _ (two_ne_zero' ℂ), ← add_sub_assoc, add_sub_cancel']
[GOAL]
z : ℂ
hz : 0 < z.im
⊢ ‖jacobiTheta z - 1‖ ≤ 2 / (1 - rexp (-π * z.im)) * rexp (-π * z.im)
[PROOFSTEP]
suffices ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im)) by
  calc
    ‖jacobiTheta z - 1‖ = ↑2 * ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * z)‖ := by
      rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hz), norm_mul, Complex.norm_eq_abs, Complex.abs_two]
    _ ≤ 2 * (rexp (-π * z.im) / (1 - rexp (-π * z.im))) := by rwa [mul_le_mul_left (zero_lt_two' ℝ)]
    _ = 2 / (1 - rexp (-π * z.im)) * rexp (-π * z.im) := by rw [div_mul_comm, mul_comm]
[GOAL]
z : ℂ
hz : 0 < z.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
⊢ ‖jacobiTheta z - 1‖ ≤ 2 / (1 - rexp (-π * z.im)) * rexp (-π * z.im)
[PROOFSTEP]
calc
  ‖jacobiTheta z - 1‖ = ↑2 * ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * z)‖ := by
    rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hz), norm_mul, Complex.norm_eq_abs, Complex.abs_two]
  _ ≤ 2 * (rexp (-π * z.im) / (1 - rexp (-π * z.im))) := by rwa [mul_le_mul_left (zero_lt_two' ℝ)]
  _ = 2 / (1 - rexp (-π * z.im)) * rexp (-π * z.im) := by rw [div_mul_comm, mul_comm]
[GOAL]
z : ℂ
hz : 0 < z.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
⊢ ‖jacobiTheta z - 1‖ = 2 * ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖
[PROOFSTEP]
rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hz), norm_mul, Complex.norm_eq_abs, Complex.abs_two]
[GOAL]
z : ℂ
hz : 0 < z.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
⊢ 2 * ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ 2 * (rexp (-π * z.im) / (1 - rexp (-π * z.im)))
[PROOFSTEP]
rwa [mul_le_mul_left (zero_lt_two' ℝ)]
[GOAL]
z : ℂ
hz : 0 < z.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
⊢ 2 * (rexp (-π * z.im) / (1 - rexp (-π * z.im))) = 2 / (1 - rexp (-π * z.im)) * rexp (-π * z.im)
[PROOFSTEP]
rw [div_mul_comm, mul_comm]
[GOAL]
z : ℂ
hz : 0 < z.im
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
[PROOFSTEP]
have : ∀ n : ℕ, ‖cexp (π * I * ((n : ℂ) + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1) :=
  by
  intro n
  simpa only [Int.cast_add, Int.cast_one] using norm_exp_mul_sq_le hz (n + 1)
[GOAL]
z : ℂ
hz : 0 < z.im
⊢ ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1)
[PROOFSTEP]
intro n
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℕ
⊢ ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1)
[PROOFSTEP]
simpa only [Int.cast_add, Int.cast_one] using norm_exp_mul_sq_le hz (n + 1)
[GOAL]
z : ℂ
hz : 0 < z.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1)
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
[PROOFSTEP]
have s : HasSum (fun n : ℕ => rexp (-π * z.im) ^ (n + 1)) (rexp (-π * z.im) / (1 - rexp (-π * z.im))) :=
  by
  simp_rw [pow_succ, div_eq_mul_inv, hasSum_mul_left_iff (Real.exp_ne_zero _)]
  exact
    hasSum_geometric_of_lt_1 (exp_pos (-π * z.im)).le
      (exp_lt_one_iff.mpr <| mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hz)
[GOAL]
z : ℂ
hz : 0 < z.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1)
⊢ HasSum (fun n => rexp (-π * z.im) ^ (n + 1)) (rexp (-π * z.im) / (1 - rexp (-π * z.im)))
[PROOFSTEP]
simp_rw [pow_succ, div_eq_mul_inv, hasSum_mul_left_iff (Real.exp_ne_zero _)]
[GOAL]
z : ℂ
hz : 0 < z.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1)
⊢ HasSum (fun i => rexp (-π * z.im) ^ i) (1 - rexp (-π * z.im))⁻¹
[PROOFSTEP]
exact
  hasSum_geometric_of_lt_1 (exp_pos (-π * z.im)).le
    (exp_lt_one_iff.mpr <| mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hz)
[GOAL]
z : ℂ
hz : 0 < z.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1)
s : HasSum (fun n => rexp (-π * z.im) ^ (n + 1)) (rexp (-π * z.im) / (1 - rexp (-π * z.im)))
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
[PROOFSTEP]
have aux : Summable fun n : ℕ => ‖cexp (π * I * ((n : ℂ) + 1) ^ 2 * z)‖ :=
  summable_of_nonneg_of_le (fun n => norm_nonneg _) this s.summable
[GOAL]
z : ℂ
hz : 0 < z.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1)
s : HasSum (fun n => rexp (-π * z.im) ^ (n + 1)) (rexp (-π * z.im) / (1 - rexp (-π * z.im)))
aux : Summable fun n => ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
[PROOFSTEP]
exact (norm_tsum_le_tsum_norm aux).trans ((tsum_mono aux s.summable this).trans (le_of_eq s.tsum_eq))
[GOAL]
⊢ (fun τ => jacobiTheta τ - 1) =O[comap im atTop] fun τ => rexp (-π * τ.im)
[PROOFSTEP]
simp_rw [IsBigO, IsBigOWith, Filter.eventually_comap, Filter.eventually_atTop]
[GOAL]
⊢ ∃ c a, ∀ (b : ℝ), b ≥ a → ∀ (a : ℂ), a.im = b → ‖jacobiTheta a - 1‖ ≤ c * ‖rexp (-π * a.im)‖
[PROOFSTEP]
refine'
  ⟨2 / (1 - rexp (-π)), 1, fun y hy z hz =>
    (norm_jacobiTheta_sub_one_le (hz.symm ▸ zero_lt_one.trans_le hy : 0 < im z)).trans _⟩
[GOAL]
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ 2 / (1 - rexp (-π * z.im)) * rexp (-π * z.im) ≤ 2 / (1 - rexp (-π)) * ‖rexp (-π * z.im)‖
[PROOFSTEP]
rw [Real.norm_eq_abs, Real.abs_exp]
[GOAL]
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ 2 / (1 - rexp (-π * z.im)) * rexp (-π * z.im) ≤ 2 / (1 - rexp (-π)) * rexp (-π * z.im)
[PROOFSTEP]
refine' mul_le_mul_of_nonneg_right _ (exp_pos _).le
[GOAL]
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ 2 / (1 - rexp (-π * z.im)) ≤ 2 / (1 - rexp (-π))
[PROOFSTEP]
rw [div_le_div_left (zero_lt_two' ℝ), sub_le_sub_iff_left, exp_le_exp, neg_mul, neg_le_neg_iff]
[GOAL]
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ π ≤ π * z.im
[PROOFSTEP]
exact le_mul_of_one_le_right pi_pos.le (hz.symm ▸ hy)
[GOAL]
case hb
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ 0 < 1 - rexp (-π * z.im)
[PROOFSTEP]
rw [sub_pos, exp_lt_one_iff, neg_mul, neg_lt_zero]
[GOAL]
case hb
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ 0 < π * z.im
[PROOFSTEP]
exact mul_pos pi_pos (hz.symm ▸ zero_lt_one.trans_le hy)
[GOAL]
case hc
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ 0 < 1 - rexp (-π)
[PROOFSTEP]
rw [sub_pos, exp_lt_one_iff, neg_lt_zero]
[GOAL]
case hc
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ 0 < π
[PROOFSTEP]
exact pi_pos
[GOAL]
z : ℂ
hz : 0 < z.im
⊢ DifferentiableAt ℂ jacobiTheta z
[PROOFSTEP]
suffices
  ∀ (y : ℝ) (_ : 0 < y), DifferentiableOn ℂ (fun z => ∑' n : ℤ, cexp (π * I * (n : ℂ) ^ 2 * z)) {w : ℂ | y < im w}
  by
  let ⟨y, hy, hy'⟩ := exists_between hz
  exact (this y hy).differentiableAt ((Complex.continuous_im.isOpen_preimage _ isOpen_Ioi).mem_nhds hy')
[GOAL]
z : ℂ
hz : 0 < z.im
this : ∀ (y : ℝ), 0 < y → DifferentiableOn ℂ (fun z => ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * z)) {w | y < w.im}
⊢ DifferentiableAt ℂ jacobiTheta z
[PROOFSTEP]
let ⟨y, hy, hy'⟩ := exists_between hz
[GOAL]
z : ℂ
hz : 0 < z.im
this : ∀ (y : ℝ), 0 < y → DifferentiableOn ℂ (fun z => ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * z)) {w | y < w.im}
y : ℝ
hy : 0 < y
hy' : y < z.im
⊢ DifferentiableAt ℂ jacobiTheta z
[PROOFSTEP]
exact (this y hy).differentiableAt ((Complex.continuous_im.isOpen_preimage _ isOpen_Ioi).mem_nhds hy')
[GOAL]
z : ℂ
hz : 0 < z.im
⊢ ∀ (y : ℝ), 0 < y → DifferentiableOn ℂ (fun z => ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * z)) {w | y < w.im}
[PROOFSTEP]
intro y hy
[GOAL]
z : ℂ
hz : 0 < z.im
y : ℝ
hy : 0 < y
⊢ DifferentiableOn ℂ (fun z => ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * z)) {w | y < w.im}
[PROOFSTEP]
have h1 :
  ∀ (n : ℤ) (w : ℂ) (_ : y < im w),
    DifferentiableWithinAt ℂ (fun v : ℂ => cexp (π * I * (n : ℂ) ^ 2 * v)) {z : ℂ | y < im z} w :=
  fun n w _ => (differentiableAt_id.const_mul _).cexp.differentiableWithinAt
[GOAL]
z : ℂ
hz : 0 < z.im
y : ℝ
hy : 0 < y
h1 : ∀ (n : ℤ) (w : ℂ), y < w.im → DifferentiableWithinAt ℂ (fun v => cexp (↑π * I * ↑n ^ 2 * v)) {z | y < z.im} w
⊢ DifferentiableOn ℂ (fun z => ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * z)) {w | y < w.im}
[PROOFSTEP]
have h2 : IsOpen {w : ℂ | y < im w} := continuous_im.isOpen_preimage _ isOpen_Ioi
[GOAL]
z : ℂ
hz : 0 < z.im
y : ℝ
hy : 0 < y
h1 : ∀ (n : ℤ) (w : ℂ), y < w.im → DifferentiableWithinAt ℂ (fun v => cexp (↑π * I * ↑n ^ 2 * v)) {z | y < z.im} w
h2 : IsOpen {w | y < w.im}
⊢ DifferentiableOn ℂ (fun z => ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * z)) {w | y < w.im}
[PROOFSTEP]
obtain ⟨bd, bd_s, le_bd⟩ := exists_summable_bound_exp_mul_sq hy
[GOAL]
case intro.intro
z : ℂ
hz : 0 < z.im
y : ℝ
hy : 0 < y
h1 : ∀ (n : ℤ) (w : ℂ), y < w.im → DifferentiableWithinAt ℂ (fun v => cexp (↑π * I * ↑n ^ 2 * v)) {z | y < z.im} w
h2 : IsOpen {w | y < w.im}
bd : ℤ → ℝ
bd_s : Summable bd
le_bd : ∀ {τ : ℂ}, y ≤ τ.im → ∀ (n : ℤ), ‖cexp (↑π * I * ↑n ^ 2 * τ)‖ ≤ bd n
⊢ DifferentiableOn ℂ (fun z => ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * z)) {w | y < w.im}
[PROOFSTEP]
exact differentiableOn_tsum_of_summable_norm bd_s h1 h2 fun i w hw => le_bd (le_of_lt hw) i
