mathlib

dc0f25ac - feat(number_theory/diophantine_approximation): add new file proving Dirichlet's approximation theorem (#18019)

feat(number_theory/diophantine_approximation): add new file proving Dirichlet's approximation theorem (#18019) This PR adds a new file, `number_theory/diophantine_approximation.lean`, that contains proofs of various versions of **Dirichlet's approximation theorem**, ```lean lemma real.exists_int_int_abs_mul_sub_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) : ∃ j k : ℤ, 0 < k ∧ k ≤ n ∧ |↑k * ξ - j| ≤ 1 / (n + 1) lemma real.exists_nat_abs_mul_sub_round_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) : ∃ k : ℕ, 0 < k ∧ k ≤ n ∧ |↑k * ξ - round (↑k * ξ)| ≤ 1 / (n + 1) ``` and ```lean lemma real.exists_rat_abs_sub_le_and_denom_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) : ∃ q : ℚ, |ξ - q| ≤ 1 / ((n + 1) * q.denom) ∧ q.denom ≤ n ``` and also the following consequence: ```lean lemma real.rat_approx_infinite_of_irrational {ξ : ℝ} (hξ : irrational ξ) : {q : ℚ | |ξ - q| < 1 / q.denom ^ 2}.infinite ``` The proof of `exists_int_int_abs_mul_sub_le` is the standard one based on the pigeonhole principle. See also the [discussion on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Diophantine.20approximation/near/318002909).