Mahler's 3/2 Problem

Reference: Wikipedia

noncomputable def Mahler32.Ω (α : ℝ) : ℝ

For a real number α, define Ω(α) as $$ \Omega (\alpha )=\inf _{\theta > 0}\left({\limsup _{n\rightarrow \infty }\left\lbrace {\theta \alpha ^{n}}\right\rbrace -\liminf _{n\rightarrow \infty }\left\lbrace {\theta \alpha ^{n}}\right\rbrace }\right). $$

Equations

• Mahler32.Ω α = ⨅ (θ : ℝ), ⨅ (_ : 0 < θ), Filter.limsup (fun (n : ℕ) => Int.fract (θ * α ^ n)) Filter.atTop - Filter.liminf (fun (n : ℕ) => Int.fract (θ * α ^ n)) Filter.atTop

def Mahler32.IsZNumber (x : ℝ) : Prop

A Z-number is a real number x such that the fractional parts of x(3/2)^n are less than 1/2 for all positive integers n.

Equations

• Mahler32.IsZNumber x = ∀ n > 0, Int.fract (x * (3 / 2) ^ n) < 1 / 2

theorem Mahler32.mahler_conjecture (x : ℝ) (h : x ≠ 0) (hx : IsZNumber x) : False

The Mahler Conjecture states that there are no non-zero Z-numbers.

theorem Mahler32.mahler_conjecture.variants.consequence (H : ∀ (x : ℝ), x ≠ 0 → IsZNumber x → False) : 1 / 2 < Ω (3 / 2)

If Mahler's conjecture is true, i.e. there are no Z-numbers, then Ω(3/2) exceeds 1/2.

theorem Mahler32.mahler_conjecture.variants.flatto_lagarias_pollington (p q : ℕ) (hq : 1 < q) (hpq : p.Coprime q) (hpq' : q < p) : 1 / ↑p < Ω (↑p / ↑q)

It is known that for all rational p/q > 1 in lowest terms, we have Ω(p/q) > 1/p.