Bugeaud Collection of Conjectures and Open Questions: Spectrum of Sequence

References:

• [Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10.
• [Men73] Mendès France, Michel. "Les ensembles de Bésineau." Séminaire Delange-Pisot-Poitou 15.1 (1973): 1-6.

def Bugeaud.Spectrum (x : ℕ → ℝ) : Set ℝ

The spectrum of a sequence $(x_n)_{n \ge 1}$ of real numbers is the set of irrational real numbers $\theta \in (0, 1)$ such that the sequence $(x_n - n\theta)_{n \ge 1}$ is not uniformly distributed modulo one.

Equations

• Bugeaud.Spectrum x = {θ : ℝ | θ ∈ Set.Ioo 0 1 ∧ Irrational θ ∧ ¬IsEquidistributedModuloOne fun (n : ℕ) => x n - ↑n * θ}

theorem Bugeaud.spectrum_xi_alpha_pow_countable (ξ : ℝ) (hξ : ξ ≠ 0) (α : ℝ) (hα : 1 < α) : (Spectrum fun (n : ℕ) => ξ * α ^ n).Countable

Problem 10.4. Let $\xi$ be a non-zero real number and $\alpha > 1$ be a real number. The spectrum of the sequence $(\xi \alpha^n)_{n \ge 1}$ is at most countable. Posed by Mendès France [Men73].