English
A real x is Liouville iff it satisfies LiouvilleWith p x for all exponents p.
Русский
Число x является числом Лиувилля тогда и только тогда, когда удовлетворяет LiouvilleWith p x для всех показателей p.
LaTeX
$$$$ (\forall p \in \mathbb{R}, LiouvilleWith(p,x)) \iff Liouville(x). $$$$
Lean4
/-- The set of Liouville numbers is a residual set. -/
theorem eventually_residual_liouville : ∀ᶠ x in residual ℝ, Liouville x :=
by
rw [Filter.Eventually, setOf_liouville_eq_irrational_inter_iInter_iUnion]
refine eventually_residual_irrational.and ?_
refine residual_of_dense_Gδ ?_ (Rat.isDenseEmbedding_coe_real.dense.mono ?_)
·
exact
.iInter fun n => IsOpen.isGδ <| isOpen_iUnion fun a => isOpen_iUnion fun b => isOpen_iUnion fun _hb => isOpen_ball
· rintro _ ⟨r, rfl⟩
simp only [mem_iInter, mem_iUnion]
refine fun n => ⟨r.num * 2, r.den * 2, ?_, ?_⟩
· have := r.pos; cutsat
· convert @mem_ball_self ℝ _ (r : ℝ) _ _
· push_cast
-- Workaround for https://github.com/leanprover/lean4/pull/6438; this eliminates an
-- `Expr.mdata` that would cause `norm_cast` to skip a numeral.
rw [Eq.refl (2 : ℝ)]
norm_cast
simp [Rat.divInt_mul_right (two_ne_zero)]
· refine one_div_pos.2 (pow_pos (Int.cast_pos.2 ?_) _)
exact mul_pos (Int.natCast_pos.2 r.pos) zero_lt_two
