FormalConjectures/Books/BugeaudDistributionModuloOne/IntDistanceDistribution.lean

GitHub source file

5 declarations, 4 contain sorry, 0 declared as axioms

1. theorem Bugeaud01.problem_10_1 Problem 10.1 sorry line 52 source

   Source documentation

   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$)

   depends on sorry what this means

   Statement uses: Iff, True, Exists, Real, And, LT.lt, OfNat.ofNat, abs, Transcendental, Rat, Filter.Tendsto, Nat, distToNearestInt, HMul.hMul, HPow.hPow, Filter.atTop, nhds

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   57 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

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

   Mentions: distToNearestInt

2. theorem Bugeaud01.problem_10_2 Problem 10.2 sorry line 62 source

   Source documentation

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

   depends on sorry what this means

   Statement uses: Not, Filter.Tendsto, Nat, Real, distToNearestInt, Real.exp, Filter.atTop, nhds, OfNat.ofNat

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   17 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

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

   Mentions: distToNearestInt

3. theorem Bugeaud01.problem_10_3 Problem 10.3 sorry line 71 source

   Source documentation

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

   depends on sorry what this means

   Statement uses: Exists, Real, And, LT.lt, OfNat.ofNat, Nat, LE.le, Real.exp, HMul.hMul, Neg.neg, distToNearestInt

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   20 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

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

   Mentions: c, distToNearestInt

4. theorem Bugeaud01.waldschmidt 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$ sorry line 84 source

   Source documentation

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

   depends on sorry what this means

   Statement uses: Exists, Real, And, LT.lt, OfNat.ofNat, Nat, LE.le, HPow.hPow, Neg.neg, distToNearestInt, Real.exp

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   20 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

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

   Mentions: c, distToNearestInt

5. theorem Bugeaud01.problem_10_3_of_waldschmidt 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}$ line 95 source

   Source documentation

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

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Exists, Real, And, LT.lt, OfNat.ofNat, Nat, LE.le, HPow.hPow, Neg.neg, distToNearestInt, Real.exp, HMul.hMul

   Proof uses: Eq.mpr, abs, HSub.hSub, id, Eq, congrArg, round, Eq.trans, Int, Real.round_exp_one_eq_three, Int.cast_ofNat, Ne, propext, abs_pos, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 111 more

   160 instances, coercions and auxiliary constants left out.

   Tactic trace: 33 steps

   Open to load the checked before-and-after goal states.

   theorem problem_10_3_of_waldschmidt (h : type_of% waldschmidt) : type_of% problem_10_3 := by
   …

   Mentions: Bugeaud01.waldschmidt, Bugeaud01.problem_10_3