/-
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 FormalConjecturesUtilBugeaud Collection of Conjectures and Open Questions: Rapidly Increasing Sequences Dense Modulo One
References:
[Bos94] Boshernitzan, Michael D. "Density modulo 1 of dilations of sublacunary sequences." Advances in Mathematics 108.1 (1994): 104-117.
[Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10.
[Fur67] Furstenberg, H. "Disjointness in ergodic theory, minimal sets, and a problem in diophantine approximation". Math. Systems Theory 1, 1–49 (1967).
[Mat80] de Mathan, Bernard. "Numbers contravening a condition in density modulo 1." Acta Mathematica Hungarica 36.3-4 (1980): 237-241.
[Pol79] Pollington, Andrew Douglas. "On the density of sequence ${n_ {k}\xi} $." Illinois Journal of Mathematics 23.4 (1979): 511-515.
namespace Bugeaud06open FilterThe Pollington–de Mathan theorem [Pol79][Mat80]. For every lacunary sequence $(m_n){n \ge 1}$ of positive integers, the set of real numbers $\xi$ for which $({\xi m_n}){n \ge 1}$ is not dense modulo one has full Hausdorff dimension.
@[category research solved, AMS 11]
theorem pollington_de_mathan (m : ℕ → ℕ) (hm : ∀ n, 0 < m n) (hlac : IsLacunary m) :
dimH {ξ : ℝ | ¬ Dense (Set.range fun n => (↑(ξ * m n) : AddCircle (1 : ℝ)))} = 1 := m:ℕ → ℕhm:∀ (n : ℕ), 0 < m nhlac:IsLacunary m⊢ dimH {ξ | ¬Dense (Set.range fun n ↦ ↑(ξ * ↑(m n)))} = 1
All goals completed! 🐙The Pollington–de Mathan theorem implies that a lacunary sequence cannot answer Problem 10.6.
h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n ↦ ↑(ξ * ↑(m n)))} = 1m₀:ℕ → ℕ := fun n ↦ 2 ^ nhm₀:m₀ = fun n ↦ 2 ^ nhpos:∀ (n : ℕ), 0 < m₀ nhlac:IsLacunary m₀hd:∀ (ξ : ℝ), Irrational ξ → Dense (Set.range fun n ↦ ↑(ξ * ↑(m₀ n)))hdim:0 = 1hcount:{ξ | ¬Dense (Set.range fun n ↦ ↑(ξ * ↑(m₀ n)))}.Countable⊢ False
All goals completed! 🐙Furstenberg's theorem [Fur67] (the $\times 2, \times 3$ case). For every irrational number $\xi$, the two-parameter family $({\xi , 2^m 3^n})_{m, n \ge 1}$ is dense modulo one.
@[category research solved, AMS 11]
theorem furstenberg_two_three (ξ : ℝ) (hξ : Irrational ξ) :
Dense {x : AddCircle (1 : ℝ) |
∃ m n : ℕ, 0 < m ∧ 0 < n ∧ x = ↑(ξ * (2 ^ m * 3 ^ n : ℕ))} := ξ:ℝhξ:Irrational ξ⊢ Dense {x | ∃ m n, 0 < m ∧ 0 < n ∧ x = ↑(ξ * ↑(2 ^ m * 3 ^ n))}
All goals completed! 🐙Boshernitzan's theorem [Bos94]. Given a real sublacunary sequence $r$, the set of real numbers $\xi$ for which $({\xi r_n})_{n \ge 1}$ is not dense modulo one has Hausdorff dimension zero.
@[category research solved, AMS 11]
theorem boshernitzan (r : ℕ → ℝ) (hr : ∀ n, 0 < r n) (hunb : ¬ BddAbove (Set.range r))
(hsub : Tendsto (fun n => r (n + 1) / r n) atTop (nhds 1)) :
dimH {ξ : ℝ | ¬ Dense (Set.range fun n => (↑(ξ * r n) : AddCircle (1 : ℝ)))} = 0 := r:ℕ → ℝhr:∀ (n : ℕ), 0 < r nhunb:¬BddAbove (Set.range r)hsub:Tendsto (fun n ↦ r (n + 1) / r n) atTop (nhds 1)⊢ dimH {ξ | ¬Dense (Set.range fun n ↦ ↑(ξ * r n))} = 0
All goals completed! 🐙The sequence defined by $m_0 = 2$ and $m_{n+1} = \lceil m_n (1 + 1/\log n) \rceil$.
noncomputable def mSeq : ℕ → ℕ
| 0 => 2
| (n + 1) => ⌈(mSeq n : ℝ) * (1 + 1 / Real.log n)⌉₊The sequence $m$ eventually grows at least geometrically with a logarithmic correction.
def IsGenuinelySublacunary (m : ℕ → ℕ) : Prop :=
∃ c > 0, ∀ᶠ (n : ℕ) in atTop, (1 + c / Real.log n) ≤ (m (n+1) : ℝ) / m n
The sequence mSeq, given by $m_{n+1} = \lceil m_n (1 + 1/\log n) \rceil$, is
genuinely sublacunary: taking $c = 1$, we have $m_{n+1}/m_n \ge 1 + 1/\log n$ because
$\lceil m_n (1 + 1/\log n) \rceil \ge m_n (1 + 1/\log n)$.
mSeq_pos:∀ (n : ℕ), 0 < mSeq nn:ℕhpos:0 < ↑(mSeq n)⊢ ↑(mSeq n) * (1 + 1 / Real.log ↑n) ≤ ↑⌈↑(mSeq n) * (1 + 1 / Real.log ↑n)⌉₊
All goals completed! 🐙The sequence $m$ eventually grows at least as fast as $\exp(n^{\alpha})$, i.e., super-exponential growth when $\alpha > 1$, and stretched-exponential when $0 < \alpha < 1$.
def HasIntermediateGrowth (α : ℝ) (m : ℕ → ℕ) : Prop :=
∀ᶠ (n : ℕ) in atTop, Real.exp ((n : ℝ) ^ α) ≤ m n
mSeq has intermediate (subexponential but super-polynomial) growth: for every
0 < α < 1 its terms eventually dominate $\exp(n^\alpha)$.
@[category test, AMS 11]
lemma example_hasIntermediateGrowth (α : ℝ) (hα₀ : 0 < α) (hα₁ : α < 1) :
HasIntermediateGrowth α mSeq := α:ℝhα₀:0 < αhα₁:α < 1⊢ HasIntermediateGrowth α mSeq
All goals completed! 🐙Problem 10.6. Find a very rapidly increasing sequence $(m_n){n \ge 1}$ of positive integers such that $({\xi m_n}){n \ge 1}$ is dense modulo one for every irrational number $\xi$. Note: Furstenberg's $2^m3^n$ is sublacunary but requires two parameters.
@[category research open, AMS 11]
theorem problem_10_6_variant_1 :
∃ m : ℕ → ℕ,
StrictMono m ∧
IsGenuinelySublacunary m ∧
∀ ξ : ℝ, Irrational ξ →
Dense (Set.range fun n => (↑(ξ * m n) : AddCircle (1 : ℝ))) := ⊢ ∃ m, StrictMono m ∧ IsGenuinelySublacunary m ∧ ∀ (ξ : ℝ), Irrational ξ → Dense (Set.range fun n ↦ ↑(ξ * ↑(m n)))
All goals completed! 🐙Problem 10.6, intermediate-growth variant.
@[category research open, AMS 11]
theorem problem_10_6_variant_2 :
∃ m : ℕ → ℕ,
StrictMono m ∧
(∃ α : ℝ, 0 < α ∧ α < 1 ∧ HasIntermediateGrowth α m) ∧
∀ ξ : ℝ, Irrational ξ →
Dense (Set.range fun n => (↑(ξ * m n) : AddCircle (1 : ℝ))) := ⊢ ∃ m,
StrictMono m ∧
(∃ α, 0 < α ∧ α < 1 ∧ HasIntermediateGrowth α m) ∧ ∀ (ξ : ℝ), Irrational ξ → Dense (Set.range fun n ↦ ↑(ξ * ↑(m n)))
All goals completed! 🐙end Bugeaud06