Convergence of the Flint Hills and Cookson Hills series

References:

• Wikipedia: Examples of numerical series
• MathWorld: Flint Hills Series
• Alekseyev, On the Flint Hills series
• MathWorld: Cookson Hills Series

theorem FlintCooksonHills.flint_hills_series_converges : True ↔ Summable fun (n : ℕ) => 1 / ((↑n + 1) ^ 3 * Real.sin (↑n + 1) ^ 2)

The Flint Hills series summing $csc(n)^2 / n^3$ from $n=1$ to $\infty$ converges. (Note that we 0-index the series below.)

theorem FlintCooksonHills.cookson_hills_series_converges : True ↔ Summable fun (n : ℕ) => 1 / ((↑n + 1) ^ 3 * Real.cos (↑n + 1) ^ 2)

The Cookson Hills series summing $sec(n)^2 / n^3$ from $n=1$ to $\infty$ converges.