jacobiTheta_eq_jacobiTheta₂

Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

URI: https://scilib.ai/kg/mathlib#jacobiTheta_eq_jacobiTheta₂

English

Jacobi’s theta function equals the second theta function evaluated at 0: θ(τ) = θ₂(0, τ).

Русский

θ(τ) = θ₂(0, τ).

LaTeX

$$$\operatorname{jacobiTheta}(\tau) = \operatorname{jacobiTheta}_{2}(0, \tau).$$$

Lean4

theorem jacobiTheta_eq_jacobiTheta₂ (τ : ℂ) : jacobiTheta τ = jacobiTheta₂ 0 τ :=
  tsum_congr (by simp [jacobiTheta₂_term])

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru