English
There exists q ∈ ℚ with |ξ−q| ≤ 1/((n+1) q.den) and q.den ≤ n.
Русский
Существует q ∈ ℚ такое, что |ξ−q| ≤ 1/((n+1)q.den) и q.den ≤ n.
LaTeX
$$$$\\exists q\\in\\mathbb{Q}, |\\xi - q| ≤ \\frac{1}{(n+1)\\,\\mathrm{den}(q)} \\\\land \\mathrm{den}(q) ≤ n.$$$$
Lean4
/-- *Dirichlet's approximation theorem:*
For any real number `ξ` and positive natural `n`, there is a fraction `q`
such that `q.den ≤ n` and `|ξ - q| ≤ 1/((n+1)*q.den)`.
See also `AddCircle.exists_norm_nsmul_le`. -/
theorem exists_rat_abs_sub_le_and_den_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) :
∃ q : ℚ, |ξ - q| ≤ 1 / ((n + 1) * q.den) ∧ q.den ≤ n :=
by
obtain ⟨j, k, hk₀, hk₁, h⟩ := exists_int_int_abs_mul_sub_le ξ n_pos
have hk₀' : (0 : ℝ) < k := Int.cast_pos.mpr hk₀
have hden : ((j / k : ℚ).den : ℤ) ≤ k :=
by
convert le_of_dvd hk₀ (Rat.den_dvd j k)
exact Rat.intCast_div_eq_divInt _ _
refine ⟨j / k, ?_, Nat.cast_le.mp (hden.trans hk₁)⟩
rw [← div_div, le_div_iff₀ (Nat.cast_pos.mpr <| Rat.pos _ : (0 : ℝ) < _)]
refine (mul_le_mul_of_nonneg_left (Int.cast_le.mpr hden : _ ≤ (k : ℝ)) (abs_nonneg _)).trans ?_
rwa [← abs_of_pos hk₀', Rat.cast_div, Rat.cast_intCast, Rat.cast_intCast, ← abs_mul, sub_mul,
div_mul_cancel₀ _ hk₀'.ne', mul_comm]
