English
Dirichlet’s approximation theorem on the AddCircle: for a given ξ, there exists j ∈ {1,...,n} with ∥j·ξ∥ small, expressed via the Fourier-analytic framework on the circle.
Русский
Теорема аппроксимации Дирихле на AddCircle: для данного ξ существует j ∈ {1,...,n} такое, что ∥j·ξ∥ малое, выраженное через фурье-анализ на окружности.
LaTeX
$$$$ \\exists j \\in [1,n], \\; \\|j\\cdot \\xi\\| \\le \\frac{T}{\\uparrow(n+1)\\uparrow}. $$$$
Lean4
/-- **Dirichlet's approximation theorem**
See also `Real.exists_rat_abs_sub_le_and_den_le`. -/
theorem exists_norm_nsmul_le (ξ : 𝕊) {n : ℕ} (hn : 0 < n) : ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ T / ↑(n + 1) :=
by
apply NormedAddCommGroup.exists_norm_nsmul_le (μ := volume) ξ hn
rw [AddCircle.measure_univ, volume_closedBall, ← ENNReal.ofReal_nsmul, mul_div_cancel₀ _ two_ne_zero,
min_eq_right (div_le_self hT.out.le <| by simp), nsmul_eq_mul,
mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr n.succ_ne_zero)]
