jacobiTheta — Mathlib

English

Jacobi’s one-variable theta function is defined by summing exp(π i n^2 τ) over all integers n.

Русский

Гиперфункция Якоби θ(τ) определяется как сумма по всем целым n: exp(π i n^2 τ).

LaTeX

$$$\operatorname{jacobiTheta}(\tau) = \sum_{n\in \mathbb{Z}} e^{\pi i n^{2} \tau}.$$$

Lean4

/-- Jacobi's one-variable theta function `∑' (n : ℤ), exp (π * I * n ^ 2 * τ)`. -/
noncomputable def jacobiTheta (τ : ℂ) : ℂ :=
  ∑' n : ℤ, cexp (π * I * (n : ℂ) ^ 2 * τ)

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