English
For irrational ξ there exists q′ with |ξ−q′| < |ξ−q| and q′ is a better rational approximation than q.
Русский
Для иррационального ξ существует q′ с меньшей погрешностью, чем у q, т.е. лучшее рациональное приближение.
LaTeX
$$$$\\exists q'∈\\mathbb{Q}\\, (|ξ-q'|<|ξ-q|).$$$$
Lean4
/-- Given any rational approximation `q` to the irrational real number `ξ`, there is
a good rational approximation `q'` such that `|ξ - q'| < |ξ - q|`. -/
theorem exists_rat_abs_sub_lt_and_lt_of_irrational {ξ : ℝ} (hξ : Irrational ξ) (q : ℚ) :
∃ q' : ℚ, |ξ - q'| < 1 / (q'.den : ℝ) ^ 2 ∧ |ξ - q'| < |ξ - q| :=
by
have h := abs_pos.mpr (sub_ne_zero.mpr <| Irrational.ne_rat hξ q)
obtain ⟨m, hm⟩ := exists_nat_gt (1 / |ξ - q|)
have m_pos : (0 : ℝ) < m := (one_div_pos.mpr h).trans hm
obtain ⟨q', hbd, hden⟩ := exists_rat_abs_sub_le_and_den_le ξ (Nat.cast_pos.mp m_pos)
have den_pos : (0 : ℝ) < q'.den := Nat.cast_pos.mpr q'.pos
have md_pos := mul_pos (add_pos m_pos zero_lt_one) den_pos
refine
⟨q', lt_of_le_of_lt hbd ?_,
lt_of_le_of_lt hbd <|
(one_div_lt md_pos h).mpr <|
hm.trans <|
lt_of_lt_of_le (lt_add_one _) <|
(le_mul_iff_one_le_right <| add_pos m_pos zero_lt_one).mpr <| mod_cast (q'.pos : 1 ≤ q'.den)⟩
rw [sq, one_div_lt_one_div md_pos (mul_pos den_pos den_pos), mul_lt_mul_iff_left₀ den_pos]
exact lt_add_of_le_of_pos (Nat.cast_le.mpr hden) zero_lt_one
