English
If card α < card β and card α > 0, for a matrix A ∈ M_{α×β}(ℤ), there exists a nonzero t ∈ ℤ^β with A t = 0 and a bound on ∥t∥ in terms of A, α, β, and chosen real numbers n,m.
Русский
Если карта α меньше карты β и карта α положительна, для матрицы A существует ненулевая вектор-решение t в ℤ^β такие что A t = 0 и существует показатель границы нормы ∥t∥ в терминах A, α, β и чисел n,m.
LaTeX
$$∃ t: β → ℤ, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (n * max(1, ‖A‖))^{ (m : ℝ) / (n - m) }$$
Lean4
theorem exists_ne_zero_int_vec_norm_le (hn : Fintype.card α < Fintype.card β) (hm : 0 < Fintype.card α) :
∃ t : β → ℤ, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (n * max 1 ‖A‖) ^ ((m : ℝ) / (n - m)) := by
classical
-- Pigeonhole
rcases Finset.exists_ne_map_eq_of_card_lt_of_maps_to (card_S_lt_card_T A hn hm) (image_T_subset_S A) with
⟨x, hxT, y, hyT, hneq, hfeq⟩
-- Proofs that x - y ≠ 0 and x - y is a solution
refine
⟨x - y, sub_ne_zero.mpr hneq, by simp only [mulVec_sub, sub_eq_zero, hfeq], ?_⟩
-- Inequality
have n_mul_norm_A_pow_e_nonneg : 0 ≤ (n * max 1 ‖A‖) ^ e := by positivity
rw [← norm_replicateCol (ι := Unit), norm_le_iff n_mul_norm_A_pow_e_nonneg]
intro i j
simp only [replicateCol_apply, Pi.sub_apply]
rw [Int.norm_eq_abs, ← Int.cast_abs]
refine le_trans ?_ (Nat.floor_le n_mul_norm_A_pow_e_nonneg)
norm_cast
rw [abs_le]
rw [Finset.mem_Icc] at hxT hyT
constructor
· simp only [neg_le_sub_iff_le_add]
apply le_trans (hyT.2 i)
norm_cast
simp only [le_add_iff_nonneg_left]
exact hxT.1 i
· simp only [tsub_le_iff_right]
apply le_trans (hxT.2 i)
norm_cast
simp only [le_add_iff_nonneg_right]
exact hyT.1 i
