English
For τ with Im τ > 0, the Jacobi theta function has the expansion jacobiTheta(τ) = 1 + 2 ∑_{n≥0} exp(π i (n+1)^2 τ).
Русский
При Im(τ) > 0 функция Якоби θ имеет разложение θ(τ) = 1 + 2 ∑_{n≥0} exp(π i (n+1)^2 τ).
LaTeX
$$$\jacobiTheta\tau = 1 + 2 \sum_{n=0}^{\infty} e^{\pi i (n+1)^2 \tau}$$$
Lean4
theorem hasSum_nat_jacobiTheta {τ : ℂ} (hτ : 0 < im τ) :
HasSum (fun n : ℕ => cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2) :=
by
have := hasSum_jacobiTheta₂_term 0 hτ
simp_rw [jacobiTheta₂_term, mul_zero, zero_add, ← jacobiTheta_eq_jacobiTheta₂] at this
have := this.nat_add_neg
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, 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
convert this.div_const 2 using 1
simp_rw [mul_div_cancel_right₀ _ (two_ne_zero' ℂ)]
