exists_ne_zero_int_vec_norm_le' — Mathlib

English

A variant of Siegel’s lemma: under cardinality conditions and A ≠ 0, there exists a nonzero integer vector t with A t = 0 and a similar bound on ∥t∥.

Русский

Вариант теоремы Сигеля: при условиях на кардинальности и A ≠ 0 существует ненулевая вектор-решение t в ℤ^β с A t = 0 и подобной границей на ∥t∥.

LaTeX

$$∃ t: β → ℤ, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (n * ‖A‖) ^ ((m : ℝ) / (n - m))$$

Lean4

theorem exists_ne_zero_int_vec_norm_le' (hn : Fintype.card α < Fintype.card β) (hm : 0 < Fintype.card α) (hA : A ≠ 0) :
    ∃ t : β → ℤ, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (n * ‖A‖) ^ ((m : ℝ) / (n - m)) :=
  by
  have := exists_ne_zero_int_vec_norm_le A hn hm
  rwa [max_eq_right] at this
  exact Int.Matrix.one_le_norm_A_of_ne_zero _ hA

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