hasSum_jacobiTheta₂_term_fderiv

English

Same HasSum relation as above for the z-derivative case; the sum equals jacobiTheta₂_fderiv.

Русский

Та же связь hasSum для производной по z; сумма равна jacobiTheta₂_fderiv.

LaTeX

$$$\text{HasSum}\bigl( n \mapsto \jacobiTheta_2\_term\_fderiv n z \tau, \ \jacobiTheta_2\_fderiv z \tau \bigr)$$$

Lean4

theorem hasSum_jacobiTheta₂_term_fderiv (z : ℂ) {τ : ℂ} (hτ : 0 < im τ) :
    HasSum (fun n ↦ jacobiTheta₂_term_fderiv n z τ) (jacobiTheta₂_fderiv z τ) :=
  ((summable_jacobiTheta₂_term_fderiv_iff z τ).mpr hτ).hasSum

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