jacobiTheta₂_term_fderiv — Mathlib

English

For all integers n and complex z,τ, the norm of jacobiTheta₂_term_fderiv is bounded by 3π|n|^2 times the norm of jacobiTheta₂_term.

Русский

Для всех целых n и комплексных z,τ норма границы производной jacobiTheta₂_term_fderiv не превышает 3π|n|^2 умножить на норму jacobiTheta₂_term.

LaTeX

$$$\|\jacobiTheta_2\_term\_fderiv(n,z,\tau)\| \le 3\pi\,|n|^{2}\, \|\jacobiTheta_2\_term(n,z,\tau)\|$$$

Lean4

/-- Summand in the series for the Fréchet derivative of the Jacobi theta function. -/
def jacobiTheta₂_term_fderiv (n : ℤ) (z τ : ℂ) : ℂ × ℂ →L[ℂ] ℂ :=
  cexp (2 * π * I * n * z + π * I * n ^ 2 * τ) •
    ((2 * π * I * n) • (ContinuousLinearMap.fst ℂ ℂ ℂ) + (π * I * n ^ 2) • (ContinuousLinearMap.snd ℂ ℂ ℂ))

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