/-
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: 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.
namespace Bugeaud01Problem 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$)
@[category research open, AMS 11]
theorem problem_10_1 : answer(sorry) ↔
∃ (α ξ : ℝ), 1 < |α| ∧ Transcendental ℚ α ∧ 0 < ξ ∧
Filter.Tendsto (fun n : ℕ ↦ distToNearestInt (ξ * α ^ n)) Filter.atTop (nhds 0) := ⊢ True ↔
∃ α ξ,
1 < |α| ∧ Transcendental ℚ α ∧ 0 < ξ ∧ Filter.Tendsto (fun n ↦ distToNearestInt (ξ * α ^ n)) Filter.atTop (nhds 0)
All goals completed! 🐙Problem 10.2. To prove that $\lVert e^n \rVert$ does not tend to 0 as n tends to infinity.
@[category research open, AMS 11]
theorem problem_10_2 :
¬ Filter.Tendsto (fun n : ℕ ↦ distToNearestInt (Real.exp n)) Filter.atTop (nhds 0) := ⊢ ¬Filter.Tendsto (fun n ↦ distToNearestInt (Real.exp ↑n)) Filter.atTop (nhds 0)
All goals completed! 🐙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].
@[category research open, AMS 11]
theorem problem_10_3 :
∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 1 ≤ n → Real.exp (-c * n) < distToNearestInt (Real.exp n) := ⊢ ∃ c, 0 < c ∧ ∀ (n : ℕ), 1 ≤ n → Real.exp (-c * ↑n) < distToNearestInt (Real.exp ↑n)
All goals completed! 🐙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$.
@[category research open, AMS 11]
theorem waldschmidt :
∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 2 ≤ n → (n : ℝ) ^ (-c) < distToNearestInt (Real.exp n) := ⊢ ∃ c, 0 < c ∧ ∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)
All goals completed! 🐙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$.
c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1)c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1n:ℕhn:1 ≤ nhn_pos:0 < ↑nh2:n ≥ 2⊢ Real.exp (-c * ↑n) ≤ Real.exp (Real.log ↑n * -c)
exact Real.exp_le_exp.mpr (c:ℝhc:0 < chyp:∀ (n : ℕ), 2 ≤ n → ↑n ^ (-c) < distToNearestInt (Real.exp ↑n)hd_pos:0 < distToNearestInt (Real.exp 1)c₀:ℝ := -Real.log (distToNearestInt (Real.exp 1)) + 1n:ℕhn:1 ≤ nhn_pos:0 < ↑nh2:n ≥ 2⊢ -c * ↑n ≤ Real.log ↑n * -c All goals completed! 🐙)
_ < distToNearestInt (Real.exp n) := hyp n h2end Bugeaud01