English
If x is Liouville, then for every n there are infinitely many rationals a/b with b > 0, such that x ≠ a/b and |x − a/b| < 1/b^n.
Русский
Если x — число Лиувилля, то для каждого натурального n существует бесконечно много рациональных a/b с b > 0 таких, что x ≠ a/b и |x − a/b| < 1/b^n.
LaTeX
$$$$ \forall x \in \mathbb{R},\; Liouville(x) \Rightarrow \forall n \in \mathbb{N},\; \exists^\infty b \in \mathbb{N}, \exists a \in \mathbb{Z}, x \neq a/b \land |x - a/b| < 1/(b)^n. $$$$
Lean4
/-- If `x` is a Liouville number, then for any `n`, for infinitely many denominators `b` there
exists a numerator `a` such that `x ≠ a / b` and `|x - a / b| < 1 / b ^ n`. -/
theorem frequently_exists_num (hx : Liouville x) (n : ℕ) :
∃ᶠ b : ℕ in atTop, ∃ a : ℤ, x ≠ a / b ∧ |x - a / b| < 1 / (b : ℝ) ^ n :=
by
refine Classical.not_not.1 fun H => ?_
simp only [not_exists, not_frequently, not_and, not_lt, eventually_atTop] at H
rcases H with ⟨N, hN⟩
have : ∀ b > (1 : ℕ), ∀ᶠ m : ℕ in atTop, ∀ a : ℤ, 1 / (b : ℝ) ^ m ≤ |x - a / b| :=
by
intro b hb
replace hb : (1 : ℝ) < b := Nat.one_lt_cast.2 hb
have H : Tendsto (fun m => 1 / (b : ℝ) ^ m : ℕ → ℝ) atTop (𝓝 0) :=
by
simp only [one_div]
exact tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt hb)
refine (H.eventually (hx.irrational.eventually_forall_le_dist_cast_div b)).mono ?_
exact fun m hm a => hm a
have : ∀ᶠ m : ℕ in atTop, ∀ b < N, 1 < b → ∀ a : ℤ, 1 / (b : ℝ) ^ m ≤ |x - a / b| :=
(finite_lt_nat N).eventually_all.2 fun b _hb => eventually_imp_distrib_left.2 (this b)
rcases (this.and (eventually_ge_atTop n)).exists with ⟨m, hm, hnm⟩
rcases hx m with ⟨a, b, hb, hne, hlt⟩
lift b to ℕ using zero_le_one.trans hb.le; norm_cast at hb; push_cast at hne hlt
rcases le_or_gt N b with h | h
· refine (hN b h a hne).not_gt (hlt.trans_le ?_)
gcongr
exact_mod_cast hb.le
· exact (hm b h hb _).not_gt hlt
