jacobiTheta_eq_tsum_nat — Mathlib

English

For τ with Im τ > 0, jacobiTheta(τ) equals 1 + 2 ∑_{n≥0} exp(π i (n+1)^2 τ), written with natural-number indexing.

Русский

Для Im(τ) > 0 функция θ(τ) записывается как θ(τ) = 1 + 2 ∑_{n≥0} exp(π i (n+1)^2 τ), используя индекс по натуральному числу.

LaTeX

$$$\jacobiTheta\tau = 1 + 2 \sum_{n \ge 0} e^{\pi i (n+1)^2 \tau}$$$

Lean4

theorem jacobiTheta_eq_tsum_nat {τ : ℂ} (hτ : 0 < im τ) :
    jacobiTheta τ = ↑1 + ↑2 * ∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ) := by
  rw [(hasSum_nat_jacobiTheta hτ).tsum_eq, mul_div_cancel₀ _ (two_ne_zero' ℂ), ← add_sub_assoc, add_sub_cancel_left]

Похожие утверждения