Sequences with Large Gaps

References:

• [Wa01] Wang, Yuefei. "On the Fatou set of an entire function with gaps." Tohoku Mathematical Journal, Second Series 53.1 (2001): 163-170.

def HasFabryGaps (n : ℕ → ℕ) : Prop

A sequence of natural numbers n₀ < n₁ < ... is said to have Fabry gaps if nₖ / k → ∞. This is the terminology adopted in [Wa01] and some other sources.

Equations

• HasFabryGaps n = (StrictMono n ∧ Filter.Tendsto (fun (k : ℕ) => ↑(n k) / ↑k) Filter.atTop Filter.atTop)

def HasFejerGaps (n : ℕ → ℕ) : Prop

A sequence of natural numbers n₀ < n₁ < ... is said to have Fejér gaps if ∑' 1 / nₖ < ∞. This is the terminology adopted in [Wa01] and some other sources.

Equations

• HasFejerGaps n = (StrictMono n ∧ Summable fun (k : ℕ) => (↑(n k))⁻¹)

theorem HasFejerGaps.hasFabryGaps {f : ℕ → ℕ} (hf : HasFejerGaps f) : HasFabryGaps f