differentiableAt_jacobiTheta₂_fst

English

For z ∈ ℂ and τ with im τ > 0, the function x ↦ θ₂(x,τ) has derivative at x = z equal to θ₂'(z,τ) applied to the pair (1,0).

Русский

Для фиксированного τ с положительной мнимой частью, производная по z существт: d/dz θ₂(z,τ) = θ₂'(z,τ) и она равна применению к (1,0).

LaTeX

$$$\text{HasDerivAt}(\lambda x. \theta_2(x,\tau), \; (\theta_2)'(z,\tau), \; z)$.$$

Lean4

/-- Differentiability of `Θ z τ` in `z`, for fixed `τ`. -/
theorem differentiableAt_jacobiTheta₂_fst (z : ℂ) {τ : ℂ} (hτ : 0 < im τ) : DifferentiableAt ℂ (jacobiTheta₂ · τ) z :=
  ((hasFDerivAt_jacobiTheta₂ z hτ).comp (𝕜 := ℂ) z (hasFDerivAt_prodMk_left z τ) :).differentiableAt

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