continuousAt_jacobiTheta₂ — Mathlib

English

For im τ > 0, the two-variable Jacobi theta function θ₂: (z,τ) ↦ θ₂(z,τ) is differentiable in (z,τ) with derivative Θ₂_fderiv(z,τ).

Русский

При im τ > 0 функция θ₂(z,τ) двух переменных по переменным z и τ дифференцируема, её производная обозначается θ₂_fderiv(z,τ).

LaTeX

$$$\text{HasFDerivAt}(\, (z,\tau) \mapsto \theta_2(z,\tau)\,,\; \theta_2\_\text{fderiv}(z,\tau),\ (z,\tau)).$$$

Lean4

theorem continuousAt_jacobiTheta₂ (z : ℂ) {τ : ℂ} (hτ : 0 < im τ) :
    ContinuousAt (fun p : ℂ × ℂ ↦ jacobiTheta₂ p.1 p.2) (z, τ) :=
  (hasFDerivAt_jacobiTheta₂ z hτ).continuousAt

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