English
If x satisfies LiouvilleWith p x, then for any nonzero integer m, LiouvilleWith p (m · x) holds (equivalently, mul_int).
Русский
Если x удовлетворяет LiouvilleWith p x, то для любого ненулевого целого m верно LiouvilleWith p (m · x).
LaTeX
$$$ \forall p\; x \in \mathbb R,\ \forall m \in \mathbb Z,\ m \neq 0 \Rightarrow LiouvilleWith p (m \cdot x) $$$
Lean4
/-- If `x` satisfies Liouville condition with exponent `p` and `q < p`, then `x`
satisfies Liouville condition with exponent `q` and constant `1`. -/
theorem frequently_lt_rpow_neg (h : LiouvilleWith p x) (hlt : q < p) :
∃ᶠ n : ℕ in atTop, ∃ m : ℤ, x ≠ m / n ∧ |x - m / n| < n ^ (-q) :=
by
rcases h.exists_pos with ⟨C, _hC₀, hC⟩
have : ∀ᶠ n : ℕ in atTop, C < n ^ (p - q) := by
simpa only [(· ∘ ·), neg_sub, one_div] using
((tendsto_rpow_atTop (sub_pos.2 hlt)).comp tendsto_natCast_atTop_atTop).eventually (eventually_gt_atTop C)
refine (this.and_frequently hC).mono ?_
rintro n ⟨hnC, hn, m, hne, hlt⟩
replace hn : (0 : ℝ) < n := Nat.cast_pos.2 hn
refine ⟨m, hne, hlt.trans <| (div_lt_iff₀ <| rpow_pos_of_pos hn _).2 ?_⟩
rwa [mul_comm, ← rpow_add hn, ← sub_eq_add_neg]
