English
There exists a nonzero integral vector ξ ∈ β → 𝓞K solving a ξ = 0 with each coordinate having house bounded by a power bound in terms of constants c1(K), q, p, A, etc.
Русский
Существует ненулевой целочисленный вектор ξ ∈ β → 𝓞K, удовлетворяющий уравнению a · ξ = 0, причем каждый компонент ξ_l имеет house не выше указанной константы, зависящей от констант c1(K), q, p, A и т. д.
LaTeX
$$$\\exists \\xi : β \\to \\mathcal{O}_K, \\; \\xi \\neq 0 \\land a \\cdot_V \\xi = 0 \\land \\forall l, \\operatorname{house}(\\xi(l).1) \\le c_1(K) \\cdot ((c_1(K) q A)^{(p/(q-p))}).$$$
Lean4
/-- There exists a "small" non-zero algebraic integral solution of an
non-trivial underdetermined system of linear equations with algebraic integer coefficients. -/
theorem exists_ne_zero_int_vec_house_le :
∃ (ξ : β → 𝓞 K), ξ ≠ 0 ∧ a *ᵥ ξ = 0 ∧ ∀ l, house (ξ l).1 ≤ c₁ K * ((c₁ K * q * A) ^ ((p : ℝ) / (q - p))) := by
classical
let h := finrank ℚ K
have hphqh : p * h < q * h := mul_lt_mul_of_pos_right hpq finrank_pos
have h0ph : 0 < p * h := by rw [mul_pos_iff]; constructor; exact ⟨h0p, finrank_pos⟩
have hfinp : Fintype.card (α × (K →+* ℂ)) = p * h := by rw [Fintype.card_prod, cardα, Embeddings.card]
have hfinq : Fintype.card (β × (K →+* ℂ)) = q * h := by rw [Fintype.card_prod, cardβ, Embeddings.card]
have ⟨x, hxl, hmulvec0, hxbound⟩ :=
Int.Matrix.exists_ne_zero_int_vec_norm_le' (asiegel K a) (by rwa [hfinp, hfinq]) (by rwa [hfinp])
(asiegel_ne_0 K a ha)
simp only [hfinp, hfinq, Nat.cast_mul] at hmulvec0 hxbound
rw [← sub_mul, mul_div_mul_right _ _ (mod_cast finrank_pos.ne')] at hxbound
have Apos : 0 ≤ A := by
have ⟨k⟩ := Fintype.card_pos_iff.1 (cardα ▸ h0p)
have ⟨l⟩ := Fintype.card_pos_iff.1 (cardβ ▸ h0p.trans hpq)
exact le_trans (house_nonneg _) (habs k l)
use ξ K x, ξ_ne_0 K x hxl, ξ_mulVec_eq_0 K a x hxl hmulvec0, house_le_bound K a hpq x habs Apos hxbound
