Schmidt's subspace theorem | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: W.M. Schmidt, Diophantine approximation, Lecture Notes in Mathematics 785, Springer Verlag 1980, Chap. V,VI,VII.

Informal solution: Unavailable.

theorem declaration uses `sorry`schmidt_subspace (σ : Type*) [Fintype σ] (hσ : 2 ≤ Fintype.card σ)
    (L : σ → σ → ℂ)
    (alg : ∀ i j, IsAlgebraic ℚ (L i j)) (ind : LinearIndependent ℂ L)
    (ε : ℝ) (pos : 0 < ε) :
    ∃ s : Finset (σ → ℤ), 0 ∉ s ∧ ∀ x : σ → ℤ,
      ‖∏ i, ∑ j, L i j * x j‖ < ‖x‖ ^ (-ε) → ∃ c ∈ s, ∑ i, c i * x i = 0 := byσ:Type u_1inst✝:Fintype σhσ:2 ≤ Fintype.card σL:σ → σ → ℂalg:∀ (i j : σ), IsAlgebraic ℚ (L i j)ind:LinearIndependent ℂ Lε:ℝpos:0 < ε⊢ ∃ s, 0 ∉ s ∧ ∀ (x : σ → ℤ), ‖∏ i, ∑ j, L i j * ↑(x j)‖ < ‖x‖ ^ (-ε) → ∃ c ∈ s, ∑ i, c i * x i = 0
  sorryAll goals completed! 🐙