hasSum_jacobiTheta₂_term — Mathlib

English

The HasSum statement expresses that jacobiTheta₂_term_fderiv sums to jacobiTheta₂_fderiv over n.

Русский

Утверждение hasSum для jacobiTheta₂_term_fderiv означает, что сумма по n равна jacobiTheta₂_fderiv.

LaTeX

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

Lean4

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

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