jacobiTheta₂'' — Mathlib

English

The complex conjugate of jacobiTheta₂'' satisfies conj(jacobiTheta₂''(z,τ)) = jacobiTheta₂''(conj(z), -conj(τ)).

Русский

Комплексное сопряжение jacobiTheta₂''(z,τ) даёт conj(jacobiTheta₂''(z,τ)) = jacobiTheta₂''(conj(z), -conj(τ)).

LaTeX

$$$$\\overline{\\operatorname{jacobiTheta_2''}(z,\\tau)} = \\operatorname{jacobiTheta_2''}(\\overline{z}, -\\overline{\\tau}).$$$$

Lean4

/-- Variant of `jacobiTheta₂'` which we introduce to simplify some formulae. -/
def jacobiTheta₂'' (z τ : ℂ) : ℂ :=
  cexp (π * I * z ^ 2 * τ) * (jacobiTheta₂' (z * τ) τ / (2 * π * I) + z * jacobiTheta₂ (z * τ) τ)

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