On approximation to a real number by algebraic numbers of bounded degree

Problem statement

Notes: Unavailable.

Source: A. Poëls, `On approximation to a real number by algebraic numbers of bounded degree`, Annals of Math, 201 (1) 2025. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2025-201-1-OnApproximationOfReals.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_1 (n : ℕ) (hn : n ≥ 2) (ξ : ℝ) (hξ : Transcendental ℚ ξ) :
    letI a : ℝ := 1 / (2 - Real.log 2)
    (ω⋆ n ξ : EReal) ≥ (a : EReal) * n := byn:ℕhn:n ≥ 2ξ:ℝhξ:Transcendental ℚ ξ⊢ ↑(ω⋆ n ξ) ≥ ↑(1 / (2 - Real.log 2)) * ↑n
  sorryAll goals completed! 🐙