corollaryroutineinferred_dep

Generalized Flint–Hills series convergence criterion

So ∑1/(na∣sin⁡n∣b)\sum 1/(n^a|\sin n|^b) converges iff a>max⁡{1,b}a>\max\{1,b\}
payoff of the main theorem
Corollary·series:generalized·§5 Flint--Hills series and its generalization

Statement (paper)

For fixed real numbers a,b>0a,b>0, the series ∑n=1∞1na∣sin⁡n∣b \sum_{n=1}^{\infty}\frac{1}{n^a|\sin n|^b} with angles in radians converges if and only if a>max⁡{1,b}a>\max\{1,b\}.

In plain English

For fixed real a,b>0a,b>0, the series ∑n≥11/(na∣sin⁡n∣b)\sum_{n\ge1} 1/(n^a|\sin n|^b) converges if and only if a>max⁡{1,b}a>\max\{1,b\}.

Why it's here

This extends the classical Flint–Hills series (the case a=3a=3, b=2b=2) to a full convergence criterion in both exponents. The sufficiency direction rests on the finite irrationality exponent of π\pi from the main theorem, in the same way as the Flint–Hills corollary, while the condition a>1a>1 is the necessary baseline since ∣sin⁡n∣≤1|\sin n|\le 1.
Classified routine:
This extends the paper’s dyadic Flint–Hills argument using the main theorem’s irrationality-exponent bound. Necessity follows from |sin n|≤1 and the standard continued-fraction approximations to 1/π.

Uses

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

Used by

Nothing in the paper

Sources

PaperOpen
Section
§5 Flint--Hills series and its generalization
Page
—
Label
series:generalized
Line
sections/series.tex:97
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: The generalized corollary reuses the nearest-multiple grouping from the preceding corollary’s proof (sections/series.tex:130–135; see lines 66–87).