infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrational

English

The set of good rational approximations is infinite iff ξ is irrational.

Русский

Множество хороших рациональных приближений бесконечно тогда и только тогда, когда ξ иррационально.

LaTeX

$$$$\\{q∈\\mathbb{Q} : |ξ-q| < 1/(q.den)^2\\}.\\\\Infinite \\;\\iff\\; ξ\\;\\text{irrational}.$$$$

Lean4

/-- The set of good rational approximations to a real number `ξ` is infinite if and only if
`ξ` is irrational. -/
theorem infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrational (ξ : ℝ) :
    {q : ℚ | |ξ - q| < 1 / (q.den : ℝ) ^ 2}.Infinite ↔ Irrational ξ :=
  by
  refine
    ⟨fun h => (irrational_iff_ne_rational ξ).mpr fun a b _ H => Set.not_infinite.mpr ?_ h,
      Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational⟩
  convert Rat.finite_rat_abs_sub_lt_one_div_den_sq ((a : ℚ) / b) with q
  rw [H, (by (push_cast; rfl) : (1 : ℝ) / (q.den : ℝ) ^ 2 = (1 / (q.den : ℚ) ^ 2 : ℚ))]
  norm_cast

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