feat: generalize Siegel's lemma to A = 0 (#14852)

The Wikipedia statement of Siegel's lemma did not contain the hypothesis `A != 0` in the lean formalization. A slight variant of the statement is still true if `A = 0`. The original statement is recovered under the assumption `A != 0`.

Co-authored-by: Michail Karatarakis <40603357+mkaratarakis@users.noreply.github.com>



Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Author: digama0

Mathlib/NumberTheory/SiegelsLemma.lean

@@ -46,7 +46,7 @@ variable {α β : Type _} [Fintype α] [Fintype β] [DecidableEq β] [DecidableE
 local notation3 "m" => Fintype.card α
 local notation3 "n" => Fintype.card β
 local notation3 "e" => m / ((n : ℝ) - m) -- exponent
-local notation3 "B" => Nat.floor (((n : ℝ) * ‖A‖) ^ e)
+local notation3 "B" => Nat.floor (((n : ℝ) * max 1 ‖A‖) ^ e)
 -- B' is the vector with all components = B
 local notation3 "B'" => fun _ : β => (B : ℤ)
 -- T is the box [0 B]^n
@@ -116,10 +116,8 @@ private lemma card_S_eq : (Finset.Icc N P).card = ∏ i : α, (P i - N i + 1) :=
   rw [Int.card_Icc_of_le (N i) (P i) (N_le_P_add_one A i)]
   exact add_sub_right_comm (P i) 1 (N i)
 
-variable  (hA : A ≠ 0)
-
 /-- The sup norm of a non-zero integer matrix is at least one  -/
-lemma one_le_norm_A_of_ne_zero : 1 ≤ ‖A‖ := by
+lemma one_le_norm_A_of_ne_zero (hA : A ≠ 0) : 1 ≤ ‖A‖ := by
   by_contra! h
   apply hA
   ext i j
@@ -140,49 +138,49 @@ private lemma card_S_lt_card_T : (S).card < (T).card := by
   rify -- This is necessary because ‖A‖ is a real number
   calc
   ∏ x : α, (∑ x_1 : β, ↑B * ↑(A x x_1)⁺ - ∑ x_1 : β, ↑B * -↑(A x x_1)⁻ + 1)
-    ≤ ∏ x : α, (n * ‖A‖ * B + 1) := by
+    ≤ ∏ x : α, (n * max 1 ‖A‖ * B + 1) := by
       refine Finset.prod_le_prod (fun i _ ↦ ?_) (fun i _ ↦ ?_)
       · have h := N_le_P_add_one A i
         rify at h
         linarith only [h]
       · simp only [mul_neg, sum_neg_distrib, sub_neg_eq_add, add_le_add_iff_right]
-        have h1 : n * ‖A‖ * B = ∑ _ : β, ‖A‖ * B := by
+        have h1 : n * max 1 ‖A‖ * B = ∑ _ : β, max 1 ‖A‖ * B := by
           simp only [sum_const, card_univ, nsmul_eq_mul]
           ring
-        simp_rw [h1, ← Finset.sum_add_distrib, ← mul_add, mul_comm ‖A‖, ← Int.cast_add]
+        simp_rw [h1, ← Finset.sum_add_distrib, ← mul_add, mul_comm (max 1 ‖A‖), ← Int.cast_add]
         gcongr with j _
         rw [posPart_add_negPart (A i j), Int.cast_abs]
-        exact norm_entry_le_entrywise_sup_norm A
-  _  = (n * ‖A‖ * B + 1) ^ m := by simp only [prod_const, card_univ]
-  _  ≤ (n * ‖A‖) ^ m * (B + 1) ^ m := by
+        exact le_trans (norm_entry_le_entrywise_sup_norm A) (le_max_right ..)
+  _  = (n * max 1 ‖A‖ * B + 1) ^ m := by simp only [prod_const, card_univ]
+  _  ≤ (n * max 1 ‖A‖) ^ m * (B + 1) ^ m := by
         rw [← mul_pow, mul_add, mul_one]
         gcongr
         have H : 1 ≤ (n : ℝ) := mod_cast (hm.trans hn)
-        exact one_le_mul_of_one_le_of_one_le H <| one_le_norm_A_of_ne_zero A hA
-  _ = ((n * ‖A‖) ^ (m / ((n : ℝ) - m))) ^ ((n : ℝ) - m)  * (B + 1) ^ m := by
+        exact one_le_mul_of_one_le_of_one_le H <| le_max_left ..
+  _ = ((n * max 1 ‖A‖) ^ (m / ((n : ℝ) - m))) ^ ((n : ℝ) - m)  * (B + 1) ^ m := by
         congr 1
-        rw [← rpow_mul (mul_nonneg (Nat.cast_nonneg' n) (norm_nonneg A)), ← Real.rpow_natCast,
-          div_mul_cancel₀]
+        rw [← rpow_mul (mul_nonneg (Nat.cast_nonneg' n) (le_trans zero_le_one (le_max_left ..))),
+          ← Real.rpow_natCast, div_mul_cancel₀]
         exact sub_ne_zero_of_ne (mod_cast hn.ne')
   _ < (B + 1) ^ ((n : ℝ) - m) * (B + 1) ^ m := by
         gcongr
         · exact sub_pos.mpr (mod_cast hn)
-        · exact Nat.lt_floor_add_one ((n * ‖A‖) ^ e)
+        · exact Nat.lt_floor_add_one ((n * max 1 ‖A‖) ^ e)
   _ = (B + 1) ^ n := by
         rw [← rpow_natCast, ← rpow_add (Nat.cast_add_one_pos B), ← rpow_natCast, sub_add_cancel]
 
 end preparation
 
-theorem exists_ne_zero_int_vec_norm_le (hA_nezero : A ≠ 0) : ∃ t : β → ℤ, t ≠ 0 ∧
-    A *ᵥ t = 0 ∧ ‖t‖ ≤ (n * ‖A‖) ^ ((m : ℝ) / (n - m)) := by
+theorem exists_ne_zero_int_vec_norm_le : ∃ t : β → ℤ, t ≠ 0 ∧
+    A *ᵥ t = 0 ∧ ‖t‖ ≤ (n * max 1 ‖A‖) ^ ((m : ℝ) / (n - m)) := by
   -- Pigeonhole
   rcases Finset.exists_ne_map_eq_of_card_lt_of_maps_to
-    (card_S_lt_card_T A hn hm hA_nezero) (image_T_subset_S A)
+    (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 * ‖A‖) ^ e := by positivity
+  have n_mul_norm_A_pow_e_nonneg : 0 ≤ (n * max 1 ‖A‖) ^ e := by positivity
   rw [← norm_col (ι := Unit), norm_le_iff n_mul_norm_A_pow_e_nonneg]
   intro i j
   simp only [col_apply, Pi.sub_apply]
@@ -203,4 +201,11 @@ theorem exists_ne_zero_int_vec_norm_le (hA_nezero : A ≠ 0) : ∃ t : β → 
     simp only [le_add_iff_nonneg_right]
     exact hyT.1 i
 
+
+theorem exists_ne_zero_int_vec_norm_le' (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
+
 end Int.Matrix