1. FormalConjectures
  2. Books
  3. BugeaudDistributionModuloOne
  4. Problem10_5
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

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.

namespace Bugeaud05open Filter

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}$.

@[category research open, AMS 11] theorem problem_10_5 (K : IntermediateField ℚ ℝ) [FiniteDimensional ℚ K] {ε : ℝ} (hε : 0 < ε) : ∃ t : ℕ → K, (∀ n, 0 < (t n : ℝ)) ∧ IsLacunaryReal (fun k => (t k : ℝ)) ∧ ∀ ξ : ℝ, ξ ∉ K → (1 - ε) ≤ limsup (fun n => Int.fract (ξ * (t n : ℝ))) atTop := K:IntermediateField ℚ ℝinst✝:FiniteDimensional ℚ ↥Kε:ℝhε:0 < ε⊢ ∃ t, (∀ (n : ℕ), 0 < ↑(t n)) ∧ (IsLacunaryReal fun k ↦ ↑(t k)) ∧ ∀ ξ ∉ K, 1 - ε ≤ limsup (fun n ↦ Int.fract (ξ * ↑(t n))) atTop All goals completed! 🐙

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]$.

@[category research open, AMS 11] theorem problem_10_5_moreover (K : IntermediateField ℚ ℝ) [FiniteDimensional ℚ K] {ε : ℝ} (hε : 0 < ε) : ∃ t : ℕ → K, (∀ n, 0 < (t n : ℝ)) ∧ IsLacunaryReal (fun k => (t k : ℝ)) ∧ ∀ ξ : ℝ, ξ ∉ K → ∀ a, a ∈ Set.Icc (0 : ℝ) (1 - ε) → ∃ y ∈ Set.Icc a (a + ε), MapClusterPt y atTop (fun n => Int.fract (ξ * (t n : ℝ))) := K:IntermediateField ℚ ℝinst✝:FiniteDimensional ℚ ↥Kε:ℝhε:0 < ε⊢ ∃ t, (∀ (n : ℕ), 0 < ↑(t n)) ∧ (IsLacunaryReal fun k ↦ ↑(t k)) ∧ ∀ ξ ∉ K, ∀ a ∈ Set.Icc 0 (1 - ε), ∃ y ∈ Set.Icc a (a + ε), MapClusterPt y atTop fun n ↦ Int.fract (ξ * ↑(t n)) All goals completed! 🐙

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.

h:∀ (K : IntermediateField ℚ ℝ) [FiniteDimensional ℚ ↥K] {ε : ℝ}, 0 < ε → ∃ t, (∀ (n : ℕ), 0 < ↑(t n)) ∧ (IsLacunaryReal fun k ↦ ↑(t k)) ∧ ∀ ξ ∉ K, ∀ a ∈ Set.Icc 0 (1 - ε), ∃ y ∈ Set.Icc a (a + ε), MapClusterPt y atTop fun n ↦ Int.fract (ξ * ↑(t n))K:IntermediateField ℚ ℝinst✝:FiniteDimensional ℚ ↥Kε:ℝhε:0 < εt:ℕ → ↥Khpos:∀ (n : ℕ), 0 < ↑(t n)hlac:IsLacunaryReal fun k ↦ ↑(t k)hξ:∀ ξ ∉ K, ∀ a ∈ Set.Icc 0 (1 - ε), ∃ y ∈ Set.Icc a (a + ε), MapClusterPt y atTop fun n ↦ Int.fract (ξ * ↑(t n))ξ:ℝhξK:ξ ∉ Khb:IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ Int.fract (ξ * ↑(t n))hε1:ε ≤ 1y:ℝhy:y ∈ Set.Icc (1 - ε) (1 - ε + ε)hcluster:MapClusterPt y atTop fun n ↦ Int.fract (ξ * ↑(t n))hb_ge:IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) atTop fun n ↦ Int.fract (ξ * ↑(t n))hcob:IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ Int.fract (ξ * ↑(t n))hle:y ≤ limsup (fun n ↦ Int.fract (ξ * ↑(t n))) atTop⊢ 1 - ε ≤ limsup (fun n ↦ Int.fract (ξ * ↑(t n))) atTop All goals completed! 🐙 h:∀ (K : IntermediateField ℚ ℝ) [FiniteDimensional ℚ ↥K] {ε : ℝ}, 0 < ε → ∃ t, (∀ (n : ℕ), 0 < ↑(t n)) ∧ (IsLacunaryReal fun k ↦ ↑(t k)) ∧ ∀ ξ ∉ K, ∀ a ∈ Set.Icc 0 (1 - ε), ∃ y ∈ Set.Icc a (a + ε), MapClusterPt y atTop fun n ↦ Int.fract (ξ * ↑(t n))K:IntermediateField ℚ ℝinst✝:FiniteDimensional ℚ ↥Kε:ℝhε:0 < εt:ℕ → ↥Khpos:∀ (n : ℕ), 0 < ↑(t n)hlac:IsLacunaryReal fun k ↦ ↑(t k)hξ:∀ ξ ∉ K, ∀ a ∈ Set.Icc 0 (1 - ε), ∃ y ∈ Set.Icc a (a + ε), MapClusterPt y atTop fun n ↦ Int.fract (ξ * ↑(t n))ξ:ℝhξK:ξ ∉ Khb:IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ Int.fract (ξ * ↑(t n))hε1:¬ε ≤ 1⊢ 1 - ε ≤ limsup (fun n ↦ Int.fract (ξ * ↑(t n))) atTop h:∀ (K : IntermediateField ℚ ℝ) [FiniteDimensional ℚ ↥K] {ε : ℝ}, 0 < ε → ∃ t, (∀ (n : ℕ), 0 < ↑(t n)) ∧ (IsLacunaryReal fun k ↦ ↑(t k)) ∧ ∀ ξ ∉ K, ∀ a ∈ Set.Icc 0 (1 - ε), ∃ y ∈ Set.Icc a (a + ε), MapClusterPt y atTop fun n ↦ Int.fract (ξ * ↑(t n))K:IntermediateField ℚ ℝinst✝:FiniteDimensional ℚ ↥Kε:ℝhε:0 < εt:ℕ → ↥Khpos:∀ (n : ℕ), 0 < ↑(t n)hlac:IsLacunaryReal fun k ↦ ↑(t k)hξ:∀ ξ ∉ K, ∀ a ∈ Set.Icc 0 (1 - ε), ∃ y ∈ Set.Icc a (a + ε), MapClusterPt y atTop fun n ↦ Int.fract (ξ * ↑(t n))ξ:ℝhξK:ξ ∉ Khb:IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ Int.fract (ξ * ↑(t n))hε1:1 < ε⊢ 1 - ε ≤ limsup (fun n ↦ Int.fract (ξ * ↑(t n))) atTop h:∀ (K : IntermediateField ℚ ℝ) [FiniteDimensional ℚ ↥K] {ε : ℝ}, 0 < ε → ∃ t, (∀ (n : ℕ), 0 < ↑(t n)) ∧ (IsLacunaryReal fun k ↦ ↑(t k)) ∧ ∀ ξ ∉ K, ∀ a ∈ Set.Icc 0 (1 - ε), ∃ y ∈ Set.Icc a (a + ε), MapClusterPt y atTop fun n ↦ Int.fract (ξ * ↑(t n))K:IntermediateField ℚ ℝinst✝:FiniteDimensional ℚ ↥Kε:ℝhε:0 < εt:ℕ → ↥Khpos:∀ (n : ℕ), 0 < ↑(t n)hlac:IsLacunaryReal fun k ↦ ↑(t k)hξ:∀ ξ ∉ K, ∀ a ∈ Set.Icc 0 (1 - ε), ∃ y ∈ Set.Icc a (a + ε), MapClusterPt y atTop fun n ↦ Int.fract (ξ * ↑(t n))ξ:ℝhξK:ξ ∉ Khb:IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ Int.fract (ξ * ↑(t n))hε1:1 < εh0:0 ≤ limsup (fun n ↦ Int.fract (ξ * ↑(t n))) atTop⊢ 1 - ε ≤ limsup (fun n ↦ Int.fract (ξ * ↑(t n))) atTop All goals completed! 🐙end Bugeaud05