therefore
Sign up
Open navigation
All open problems
Source labels openChecked July 26, 2026

BooksNumber theory

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

Problem 10.5 (first part). Let K\mathbb{K} be a real number field. Then, for any ε>0\varepsilon > 0, there exists a lacunary sequence (tn)n≥1(t_n)_{n \ge 1} of positive numbers in K\mathbb{K} such that lim sup⁡n→∞{ξtn}≥1−ε,\limsup_{n \to \infty} \{\xi t_n\} \ge 1 - \varepsilon,...

Number theoryAMS 11

Mathematical statement

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

Statement source: Books statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

problem_10_5

Canonical source
Complete statement target, proof intentionally absentLean 4
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 := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References

Pinned Formal Conjectures sourceformalization