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

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

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

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

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

theorem Bugeaud01.problem_10_2 : ¬Filter.Tendsto (fun (n : ℕ) => distToNearestInt (Real.exp ↑n)) Filter.atTop (nhds 0)

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

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

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

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

Waldschmidt [Wal03] conjectured that a stronger result holds, namely that there exists a positive real number~$c$ such that $\lVert e^n \rVert > 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$.

theorem Bugeaud01.problem_10_3_of_waldschmidt (h : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)) : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), 1 ≤ n → Real.exp (-c * ↑n) < distToNearestInt (Real.exp ↑n)

Waldschmidt's conjecture is stronger than Mahler's: since $\log n \le n$ for $n \ge 1$, the polynomial lower bound $n^{-c}$ dominates the exponential lower bound $e^{-cn}$. For the $n = 1$ case (not covered by Waldschmidt's $n \ge 2$), we choose a larger constant using the numerical bound $\lVert e \rVert = 3 - e > 0$.