Bugeaud Collection of Conjectures and Open Questions: Fractional Parts of Powers

The question

problem_10_1. Problem 10.1. Are there a transcendental number $\alpha$ and a positive real number $\xi$ such that $\Vert \xi {\alpha }^n\Vert$ tends to~$0$ as~$n$ tends to infinity? [Har19] (Trivial for $|\alpha |<1$)

problem_10_2. Problem 10.2. To prove that $\Vert e^n\Vert$ does not tend to 0 as n tends to infinity.

problem_10_3. Problem 10.3. To prove that there exists a positive real number~$c$ such that $\Vert e^n\Vert >e^{-cn}$, for every~$n\ge 1$. Posed by Mahler [Mah53].

waldschmidt. Waldschmidt [Wal03] conjectured that a stronger result holds, namely that there exists a positive real number~$c$ such that $\Vert e^n\Vert >n^{-c}$ for every~$n\ge 2$. This is supported by metrical results [Kok45].

Note: the bound $n^{-c}$ equals $1$ when $n=1$ for all $c$, while the distance to the nearest integer is always at most $1/2$, so the conjecture must start at $n\ge 2$.

Chapter 10 of the book collects open questions. This file formalizes Problems 10.1, 10.2, 10.3 and the unnumbered conjecture by Waldschmidt.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Books.BugeaudDistributionModuloOne.IntDistanceDistribution (4 statements). answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem problem_10_1 : answer(sorry) ↔
    ∃ (α ξ : ℝ), 1 < |α| ∧ Transcendental ℚ α ∧ 0 < ξ ∧
      Filter.Tendsto (fun n : ℕ ↦ distToNearestInt (ξ * α ^ n)) Filter.atTop (nhds 0)

theorem problem_10_2 :
    ¬ Filter.Tendsto (fun n : ℕ ↦ distToNearestInt (Real.exp n)) Filter.atTop (nhds 0)

theorem problem_10_3 :
    ∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 1 ≤ n → Real.exp (-c * n) < distToNearestInt (Real.exp n)

theorem waldschmidt :
    ∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 2 ≤ n → (n : ℝ) ^ (-c) < distToNearestInt (Real.exp n)

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• [Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10.
• [Har19] Hardy, Gr H. "A problem of Diophantine approximation." J. Indian Math. Soc 11 (1919): 162-166.
• [Kok45] Koksma, J. F. "Sur la théorie métrique des approximations diophantiques." Indag. Math 7 (1945): 54-70.
• [Mah53] Mahler, Kurt. "On the approximation of logarithms of algebraic numbers." Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences 245.898 (1953): 371-398.
• [Wal03](http://webusers.imj-prg.fr/~michel.waldschmidt/articles/pdf/Cetraro.pdf) Waldschmidt, Michel. "Linear independence measures for logarithms of algebraic numbers." Diophantine Approximation: Lectures given at the CIME Summer School held in Cetraro, Italy, June 28–July 6, 2000. Berlin, Heidelberg: Springer Berlin Heidelberg, 2003. 249-344.

Source and licence

Imported from Formal Conjectures (books), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.