Rational approximations to linear subspaces | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: N. de Saxcé, `Rational approximations to linear subspaces`, Annals of Math, 203 (3) 2026. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2026-203-3-LinearSubspaces.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1 (hd : 2 ≤ d) (l : ℕ) (hl0 : 0 < l) (hld : l < d) (k : ℕ) (hk1 : 1 ≤ k) (hkl : k ≤ l) :
    (∀ x : Submodule ℝ ℝᵈ, finrank ℝ x = l → LinearSubspaces.diophantineExponent k x ≥ d / (k * (d - l))) ∧
    (∃ x : Submodule ℝ ℝᵈ, finrank ℝ x = l ∧ LinearSubspaces.diophantineExponent k x = d / (k * (d - l))) := byd:ℕhd:2 ≤ dl:ℕhl0:0 < lhld:l < dk:ℕhk1:1 ≤ khkl:k ≤ l⊢ (∀ (x : Submodule ℝ ℝᵈ), finrank ℝ ↥x = l → diophantineExponent k x ≥ ↑d / (↑k * (↑d - ↑l))) ∧
  ∃ x, finrank ℝ ↥x = l ∧ diophantineExponent k x = ↑d / (↑k * (↑d - ↑l))
  sorryAll goals completed! 🐙