differentiableAt_jacobiTheta — Mathlib

English

Jacobi theta is differentiable with respect to its complex arguments at any point τ with Im(τ) > 0.

Русский

Функция Якоби θ дифференцируема по комплексным аргументам в любой точке τ с Im(τ) > 0.

LaTeX

$$$\text{Differentiable}_{\mathbb{C}}(\jacobiTheta, \tau) \quad \text{for } \Im(\tau) > 0$$$

Lean4

theorem differentiableAt_jacobiTheta {τ : ℂ} (hτ : 0 < im τ) : DifferentiableAt ℂ jacobiTheta τ :=
  by
  simp_rw [funext jacobiTheta_eq_jacobiTheta₂]
  exact differentiableAt_jacobiTheta₂_snd 0 hτ

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