feat(ModularForms/JacobiTheta): derivative of theta function (#11824)

This is a rewrite of `JacobiTheta/TwoVariable.lean`, adding a number of new results needed for Hurwitz and Dirichlet L-series.

The main addition is developing the theory of the `z`-derivative of the theta function, as an object of study in its own right (functional equations, periodicity, holomorphy etc) – this is needed to prove analytic continuation + functional equations for odd Dirichlet characters. 

We also add a number of new results about the existing `jacobiTheta2` function:
- converses of all the convergence statements (showing the series are *never* convergent if tau is outside the upper half-plane), which allows hypotheses to be removed from several results further downstream
- differentiability in both variables jointly, not just each variable separately as before.

Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean

@@ -27,7 +27,8 @@ open scoped Real BigOperators UpperHalfPlane
 noncomputable def jacobiTheta (τ : ℂ) : ℂ := ∑' n : ℤ, cexp (π * I * (n : ℂ) ^ 2 * τ)
 #align jacobi_theta jacobiTheta
 
-lemma jacobiTheta_eq_jacobiTheta₂ (τ : ℂ) : jacobiTheta τ = jacobiTheta₂ 0 τ := tsum_congr (by simp)
+lemma jacobiTheta_eq_jacobiTheta₂ (τ : ℂ) : jacobiTheta τ = jacobiTheta₂ 0 τ :=
+  tsum_congr (by simp [jacobiTheta₂_term])
 
 theorem jacobiTheta_two_add (τ : ℂ) : jacobiTheta (2 + τ) = jacobiTheta τ := by
   simp_rw [jacobiTheta_eq_jacobiTheta₂, add_comm, jacobiTheta₂_add_right]
@@ -44,14 +45,13 @@ set_option linter.uppercaseLean3 false in
 theorem jacobiTheta_S_smul (τ : ℍ) :
     jacobiTheta ↑(ModularGroup.S • τ) = (-I * τ) ^ (1 / 2 : ℂ) * jacobiTheta τ := by
   have h0 : (τ : ℂ) ≠ 0 := ne_of_apply_ne im (zero_im.symm ▸ ne_of_gt τ.2)
-  simp_rw [UpperHalfPlane.modular_S_smul, jacobiTheta_eq_jacobiTheta₂]
-  conv_rhs => erw [← ofReal_zero, jacobiTheta₂_functional_equation 0 τ.2]
-  rw [zero_pow two_ne_zero, mul_zero, zero_div, Complex.exp_zero, mul_one, ← mul_assoc, mul_one_div]
-  erw [div_self]
-  rw [one_mul, UpperHalfPlane.coe_mk, inv_neg, neg_div, one_div]
-  · rfl
-  · rw [Ne, cpow_eq_zero_iff, not_and_or]
+  have h1 : (-I * τ) ^ (1 / 2 : ℂ) ≠ 0 := by
+    rw [Ne, cpow_eq_zero_iff, not_and_or]
     exact Or.inl <| mul_ne_zero (neg_ne_zero.mpr I_ne_zero) h0
+  simp_rw [UpperHalfPlane.modular_S_smul, jacobiTheta_eq_jacobiTheta₂]
+  conv_rhs => erw [← ofReal_zero, jacobiTheta₂_functional_equation 0 τ]
+  rw [zero_pow two_ne_zero, mul_zero, zero_div, Complex.exp_zero, mul_one, ← mul_assoc, mul_one_div,
+    div_self h1, one_mul, UpperHalfPlane.coe_mk, inv_neg, neg_div, one_div]
 set_option linter.uppercaseLean3 false in
 #align jacobi_theta_S_smul jacobiTheta_S_smul
 
@@ -72,30 +72,11 @@ theorem norm_exp_mul_sq_le {τ : ℂ} (hτ : 0 < τ.im) (n : ℤ) :
     exact pow_le_pow_of_le_one (exp_pos _).le h.le ((sq n.natAbs).symm ▸ n.natAbs.le_mul_self)
 #align norm_exp_mul_sq_le norm_exp_mul_sq_le
 
-theorem exists_summable_bound_exp_mul_sq {R : ℝ} (hR : 0 < R) :
-    ∃ bd : ℤ → ℝ, Summable bd ∧ ∀ {τ : ℂ} (_ : R ≤ τ.im) (n : ℤ),
-      ‖cexp (π * I * (n : ℂ) ^ 2 * τ)‖ ≤ bd n := by
-  let y := rexp (-π * R)
-  have h : y < 1 := exp_lt_one_iff.mpr (mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hR)
-  refine ⟨fun n ↦ y ^ n.natAbs, .of_nat_of_neg ?_ ?_, fun hτ n ↦ ?_⟩; pick_goal 3
-  · refine' (norm_exp_mul_sq_le (hR.trans_le hτ) n).trans _
-    dsimp [y]
-    gcongr rexp ?_ ^ _
-    rwa [mul_le_mul_left_of_neg (neg_lt_zero.mpr pi_pos)]
-  all_goals
-    simpa only [Int.natAbs_neg, Int.natAbs_ofNat] using
-      summable_geometric_of_lt_one (Real.exp_pos _).le h
-#align exists_summable_bound_exp_mul_sq exists_summable_bound_exp_mul_sq
-
-theorem summable_exp_mul_sq {τ : ℂ} (hτ : 0 < τ.im) :
-    Summable fun n : ℤ => cexp (π * I * (n : ℂ) ^ 2 * τ) :=
-  let ⟨_, h, h'⟩ := exists_summable_bound_exp_mul_sq hτ
-  .of_norm_bounded _ h (h' <| le_refl _)
-#align summable_exp_mul_sq summable_exp_mul_sq
-
 theorem hasSum_nat_jacobiTheta {τ : ℂ} (hτ : 0 < im τ) :
     HasSum (fun n : ℕ => cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2) := by
-  have := (summable_exp_mul_sq hτ).hasSum.sum_nat_of_sum_int
+  have := hasSum_jacobiTheta₂_term 0 hτ
+  simp_rw [jacobiTheta₂_term, mul_zero, zero_add, ← jacobiTheta_eq_jacobiTheta₂] at this
+  have := this.sum_nat_of_sum_int
   rw [← hasSum_nat_add_iff' 1] at this
   simp_rw [Finset.sum_range_one, Int.cast_neg, Int.cast_natCast, Nat.cast_zero, neg_zero,
     Int.cast_zero, sq (0 : ℂ), mul_zero, zero_mul, neg_sq, ← mul_two,
@@ -154,7 +135,7 @@ set_option linter.uppercaseLean3 false in
 theorem differentiableAt_jacobiTheta {τ : ℂ} (hτ : 0 < im τ) :
     DifferentiableAt ℂ jacobiTheta τ := by
   simp_rw [funext jacobiTheta_eq_jacobiTheta₂]
-  exact differentiableAt_jacobiTheta₂ 0 hτ
+  exact differentiableAt_jacobiTheta₂_snd 0 hτ
 #align differentiable_at_jacobi_theta differentiableAt_jacobiTheta
 
 theorem continuousAt_jacobiTheta {τ : ℂ} (hτ : 0 < im τ) : ContinuousAt jacobiTheta τ :=