English
If x satisfies LiouvilleWith p x, then so does x multiplied by any nonzero rational r; i.e., LiouvilleWith p (x · r) holds for r ≠ 0.
Русский
Если x удовлетворяет LiouvilleWith p x, то и x, умноженное на любое ненулевое рациональное число r, удовлетворяет LiouvilleWith p (x · r).
LaTeX
$$$ \forall p x \in \mathbb R,\ \forall r \in \mathbb Q,\ r \neq 0\Rightarrow LiouvilleWith p (r \cdot x) $$$
Lean4
/-- The constant `C` provided by the definition of `LiouvilleWith` can be made positive.
We also add `1 ≤ n` to the list of assumptions about the denominator. While it is equivalent to
the original statement, the case `n = 0` breaks many arguments. -/
theorem exists_pos (h : LiouvilleWith p x) :
∃ (C : ℝ) (_h₀ : 0 < C), ∃ᶠ n : ℕ in atTop, 1 ≤ n ∧ ∃ m : ℤ, x ≠ m / n ∧ |x - m / n| < C / n ^ p :=
by
rcases h with ⟨C, hC⟩
refine ⟨max C 1, zero_lt_one.trans_le <| le_max_right _ _, ?_⟩
refine ((eventually_ge_atTop 1).and_frequently hC).mono ?_
rintro n ⟨hle, m, hne, hlt⟩
refine ⟨hle, m, hne, hlt.trans_le ?_⟩
gcongr
apply le_max_left
