differentiableAt_jacobiTheta₂_snd

English

For z ∈ ℂ and τ with im τ > 0, the function τ ↦ θ₂(z,τ) is differentiable at τ with derivative θ₂'(z,τ).

Русский

Для фиксированного z функция τ ↦ θ₂(z,τ) дифференцируема в τ с производной θ₂'(z,τ).

LaTeX

$$$\text{DifferentiableAt}(\tau \mapsto \theta_2(z,\tau), \theta_2'(z,\tau))$.$$

Lean4

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

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