exists_nat_abs_mul_sub_round_le — Mathlib

English

There is a natural-number version of the Dirichlet approximation giving k and y with k>0, y≤n and |kξ−round(kξ)| small.

Русский

Существует натуральная версия аппроксимации Дирихле, задающая k и y с k>0, y≤n и малого значения |kξ−round(kξ)|.

LaTeX

$$$$\\exists k∈\\mathbb{N}, 0

Lean4

/-- *Dirichlet's approximation theorem:*
For any real number `ξ` and positive natural `n`, there is a natural number `k`,
with `0 < k ≤ n` such that `|k*ξ - round(k*ξ)| ≤ 1/(n+1)`.
-/
theorem exists_nat_abs_mul_sub_round_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) :
    ∃ k : ℕ, 0 < k ∧ k ≤ n ∧ |↑k * ξ - round (↑k * ξ)| ≤ 1 / (n + 1) :=
  by
  obtain ⟨j, k, hk₀, hk₁, h⟩ := exists_int_int_abs_mul_sub_le ξ n_pos
  have hk := toNat_of_nonneg hk₀.le
  rw [← hk] at hk₀ hk₁ h
  exact ⟨k.toNat, natCast_pos.mp hk₀, Nat.cast_le.mp hk₁, (round_le (↑k.toNat * ξ) j).trans h⟩

Похожие утверждения