x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n : ℕ
⊢ ∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ n
x : ℝ
⊢ (∀ (p : ℝ), LiouvilleWith p x) ↔ Liouville x
refine ⟨fun H n => ?_, Liouville.liouvilleWith⟩
case intro.intro.intro.intro
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < ↑b ^ (-↑n)
⊢ ∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ n
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n : ℕ
⊢ ∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ n
rcases ((eventually_gt_atTop 1).and_frequently
  ((H (n + 1)).frequently_lt_rpow_neg (lt_add_one (n : ℝ)))).exists
  with  ⟨b, hb, a, hne, hlt⟩
no goals
case intro.intro.intro.intro
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < ↑b ^ (-↑n)
⊢ ∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ n
exact ⟨a, b, by exact_mod_cast hb, hne, by simpa [rpow_neg] using hlt⟩
no goals
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < ↑b ^ (-↑n)
⊢ 1 < ↑b
exact_mod_cast hb
no goals
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < ↑b ^ (-↑n)
⊢ abs (x - ↑a / ↑↑b) < 1 / ↑↑b ^ n
simpa [rpow_neg] using hlt