corollaryroutine

Flint–Hills series converges

So the Flint–Hills series ∑1/(n3sin⁡2n)\sum 1/(n^3\sin^2 n) converges
classical case feeding the general criterion
Corollary·thm:flinthills·§1 Introduction

Statement (paper)

The classical Flint--Hills series converges.

In plain English

The classical Flint–Hills series, ∑n≥11/(n3sin⁡2n)\sum_{n\ge1} 1/(n^3\sin^2 n), converges.

Why it's here

This follows by combining the main theorem with the dyadic convergence lemma. Theorem 1.1 gives the irrationality exponent of π\pi equal to 2, which yields the bound ∥qα∥≥cq1−ν\|q\alpha\|\ge c q^{1-\nu} with ν<5/2\nu<5/2 for the relevant α\alpha related to π\pi, and the lemma then converts this into convergence of the sum.
Classified routine:
This is a direct consequence of the main theorem and the dyadic convergence lemma: the irrationality exponent bound applies to 1/\pi, and |\sin n| is comparable to \|n/\pi\|.

Uses

thmIrrationality exponent of pi is 2lemFlint–Hills sum converges for finite irrationality exponent

Used by

corGeneralized Flint–Hills series convergence criterion

Sources

PaperOpen
Section
§1 Introduction
Page
—
Label
thm:flinthills
Line
main.tex:90
Leannot aligned

Phase 2 aligns this node to a Lean declaration.