Bugeaud Collection of Conjectures and Open Questions: Lacunary Sequences in Real Number Fields

The following problems were proposed and discussed by Dubickas as Conjecture 2 in [Dub09].

References:

• [Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10.
• [Dub09] Dubickas, Artūras. "An approximation property of lacunary sequences." Israel Journal of Mathematics 170.1 (2009): 95-111.

theorem Bugeaud.problem_10_5 (K : IntermediateField ℚ ℝ) [FiniteDimensional ℚ ↥K] {ε : ℝ} (hε : 0 < ε) : ∃ (t : ℕ → ↥K), (∀ (n : ℕ), 0 < ↑(t n)) ∧ (IsLacunaryReal fun (k : ℕ) => ↑(t k)) ∧ ∀ ξ ∉ K, 1 - ε ≤ Filter.limsup (fun (n : ℕ) => Int.fract (ξ * ↑(t n))) Filter.atTop

Problem 10.5 (first part). Let $\mathbb{K}$ be a real number field. Then, for any $\varepsilon > 0$, there exists a lacunary sequence $(t_n)_{n \ge 1}$ of positive numbers in $\mathbb{K}$ such that $$\limsup_{n \to \infty} \{\xi t_n\} \ge 1 - \varepsilon,$$ for any real number $\xi$ not in $\mathbb{K}$.

theorem Bugeaud.problem_10_5_moreover (K : IntermediateField ℚ ℝ) [FiniteDimensional ℚ ↥K] {ε : ℝ} (hε : 0 < ε) : ∃ (t : ℕ → ↥K), (∀ (n : ℕ), 0 < ↑(t n)) ∧ (IsLacunaryReal fun (k : ℕ) => ↑(t k)) ∧ ∀ ξ ∉ K, ∀ a ∈ Set.Icc 0 (1 - ε), ∃ y ∈ Set.Icc a (a + ε), MapClusterPt y Filter.atTop fun (n : ℕ) => Int.fract (ξ * ↑(t n))

Problem 10.5 ("moreover" clause). With the same hypotheses as problem_10_5, the sequence $(t_n)$ can be chosen so that, for any real $\xi$ not in $\mathbb{K}$, each subinterval of $[0, 1]$ of length $\varepsilon$ contains a limit point of the sequence $(\{\xi t_n\})_{n \ge 1}$. This is strictly stronger than problem_10_5: the limsup bound is the special case at the subinterval $[1 - \varepsilon, 1]$.

theorem Bugeaud.problem_10_5_of_moreover (h : ∀ (K : IntermediateField ℚ ℝ) [FiniteDimensional ℚ ↥K] {ε : ℝ}, 0 < ε → ∃ (t : ℕ → ↥K), (∀ (n : ℕ), 0 < ↑(t n)) ∧ (IsLacunaryReal fun (k : ℕ) => ↑(t k)) ∧ ∀ ξ ∉ K, ∀ a ∈ Set.Icc 0 (1 - ε), ∃ y ∈ Set.Icc a (a + ε), MapClusterPt y Filter.atTop fun (n : ℕ) => Int.fract (ξ * ↑(t n))) (K : IntermediateField ℚ ℝ) [FiniteDimensional ℚ ↥K] {ε : ℝ} (hε : 0 < ε) : ∃ (t : ℕ → ↥K), (∀ (n : ℕ), 0 < ↑(t n)) ∧ (IsLacunaryReal fun (k : ℕ) => ↑(t k)) ∧ ∀ ξ ∉ K, 1 - ε ≤ Filter.limsup (fun (n : ℕ) => Int.fract (ξ * ↑(t n))) Filter.atTop

The "moreover" form of Problem 10.5 implies the first part: applying the cluster-point density to the subinterval $[1 - \varepsilon, 1]$ yields the required lower bound on the limsup.