Trigonometric and harmonic-number series

Closed forms for series in powers of sin, cos or tan, central binomial series in trigonometric arguments, partial-fraction series of trigonometric functions, and identities with harmonic or odd harmonic numbers, as in Ramanujan's notebooks Chapter 9.

• Arcsine series and central binomial sums
• Arctangent sums and series
• Central binomial series in trigonometric arguments
• Partial-fraction series over odd integers
• Power series in sin x and tan x
• Series from Nörlund's digamma identity
• Series with odd harmonic numbers

TheoremA closed form for \(\sum \sin^2(n\delta)/(n^2\delta)\)#●ready to prove

For every real \(\delta\) with \(0 < \delta < \pi\),

\[\sum_{n=1}^{\infty} \frac{\sin^2(n\delta)}{n^2\delta} = \frac{\pi - \delta}{2}.\]

public theorem_wanted tsum_sin_sq_mul_div_sq_mul
    {δ : ℝ} (hδ0 : 0 < δ) (hδpi : δ < Real.pi) :
    (∑' n : ℕ,
        (Real.sin ((n + 1 : ℕ) * δ)) ^ 2 / (((n + 1 : ℕ) ^ 2) * δ))
      = (Real.pi - δ) / 2

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Sequences, series, summability; Convergence and divergence of infinite limiting processes), problem ma_proofbench_l1_03.

TheoremPartial fraction expansion of \(\pi^2/\sin^2(\pi u)\)#●ready to prove

For every real number \(u\) that is not an integer,

\[\sum_{n \in \mathbb{Z}} \frac{1}{(u+n)^2} = \frac{\pi^2}{\sin^2(\pi u)}.\]

public theorem_wanted tsum_one_div_add_int_sq_eq_pi_sq_div_sin_sq
    (u : ℝ) (hu : u ∉ Set.range (fun n : ℤ => (n : ℝ))) :
    (∑' n : ℤ, 1 / ((u + n) ^ 2)) =
      (Real.pi ^ 2) / (Real.sin (Real.pi * u) ^ 2)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Sequences, series, summability; Convergence and divergence of infinite limiting processes), problem ma_proofbench_l2_09.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.