jacobiTheta₂_undef — Mathlib

English

If im(τ) ≤ 0, then jacobiTheta₂(z, τ) = 0 for all z ∈ ℂ.

Русский

Пусть Im(τ) ≤ 0. Тогда для всех z ∈ ℂ выполняется jacobiTheta₂(z, τ) = 0.

LaTeX

$$$\operatorname{Im}(\tau) \le 0 \implies \ jacobiTheta_2(z,\tau) = 0.$$$

Lean4

theorem jacobiTheta₂_undef (z : ℂ) {τ : ℂ} (hτ : im τ ≤ 0) : jacobiTheta₂ z τ = 0 :=
  by
  apply tsum_eq_zero_of_not_summable
  rw [summable_jacobiTheta₂_term_iff]
  exact not_lt.mpr hτ

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