feat(data/polynomial/ring_division): add bUnion_roots_finite (#16670)

Add three lemmas about polynomials needed for #15143 

From flt-regular

Co-authored-by: Damiano Testa <adomani@gmail.com>

src/data/polynomial/degree/definitions.lean

@@ -253,6 +253,20 @@ begin
   { rwa [degree_eq_nat_degree hp, with_bot.coe_lt_coe] }
 end
 
+lemma ext_iff_nat_degree_le {p q : R[X]} {n : ℕ} (hp : p.nat_degree ≤ n) (hq : q.nat_degree ≤ n) :
+  p = q ↔ (∀ i ≤ n, p.coeff i = q.coeff i) :=
+begin
+  refine iff.trans polynomial.ext_iff _,
+  refine forall_congr (λ i, ⟨λ h _, h, λ h, _⟩),
+  refine (le_or_lt i n).elim h (λ k, _),
+  refine (coeff_eq_zero_of_nat_degree_lt (hp.trans_lt k)).trans
+    (coeff_eq_zero_of_nat_degree_lt (hq.trans_lt k)).symm,
+end
+
+lemma ext_iff_degree_le {p q : R[X]} {n : ℕ} (hp : p.degree ≤ n) (hq : q.degree ≤ n) :
+  p = q ↔ (∀ i ≤ n, p.coeff i = q.coeff i)  :=
+ext_iff_nat_degree_le (nat_degree_le_of_degree_le hp) (nat_degree_le_of_degree_le hq)
+
 @[simp] lemma coeff_nat_degree_succ_eq_zero {p : R[X]} : p.coeff (p.nat_degree + 1) = 0 :=
 coeff_eq_zero_of_nat_degree_lt (lt_add_one _)
 

src/data/polynomial/ring_division.lean

@@ -665,6 +665,32 @@ lemma root_set_finite (p : T[X])
   (S : Type*) [comm_ring S] [is_domain S] [algebra T S] : (p.root_set S).finite :=
 set.to_finite _
 
+/-- The set of roots of all polynomials of bounded degree and having coefficients in a finite set
+is finite. -/
+lemma bUnion_roots_finite {R S : Type*} [semiring R] [comm_ring S] [is_domain S]
+  (m : R →+* S) (d : ℕ) {U : set R} (h : U.finite) :
+  (⋃ (f : R[X]) (hf : f.nat_degree ≤ d ∧ ∀ i, (f.coeff i) ∈ U),
+    ((f.map m).roots.to_finset : set S)).finite :=
+begin
+  refine set.finite.bUnion _ _,
+  { -- We prove that the set of polynomials under consideration is finite because its
+    -- image by the injective map `π` is finite
+    let π : R[X] → finset.range (d+1) → R := λ f i, f.coeff i,
+    have h_inj : set.inj_on π {f : R[X] | f.nat_degree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U},
+    { intros x hx y hy hxy,
+      rw ext_iff_nat_degree_le hx.1 hy.1,
+      exact_mod_cast λ i hi, congr_fun hxy ⟨i, finset.mem_range_succ_iff.mpr hi⟩, },
+    have h_fin : (set.pi set.univ (λ e : finset.range (d+1), U)).finite := set.finite.pi (λ e, h),
+    refine set.finite.of_finite_image (set.finite.subset h_fin _) h_inj,
+    rw set.image_subset_iff,
+    intros f hf,
+    rw [set.mem_preimage, set.mem_univ_pi],
+    exact λ i, hf.2 i, },
+  { intros i hi,
+    convert root_set_finite (i.map m) S,
+    simp only [algebra.id.map_eq_id, map_id], },
+end
+
 theorem mem_root_set_iff' {p : T[X]} {S : Type*} [comm_ring S] [is_domain S]
   [algebra T S] (hp : p.map (algebra_map T S) ≠ 0) (a : S) :
   a ∈ p.root_set S ↔ (p.map (algebra_map T S)).eval a = 0 :=

src/topology/algebra/polynomial.lean

@@ -140,12 +140,22 @@ variables {F K : Type*} [field F] [normed_field K]
 
 open multiset
 
+lemma eq_one_of_roots_le {p : F[X]} {f : F →+* K} {B : ℝ} (hB : B < 0)
+  (h1 : p.monic) (h2 : splits f p) (h3 : ∀ z ∈ (map f p).roots, ∥z∥ ≤ B) :
+  p = 1 :=
+h1.nat_degree_eq_zero_iff_eq_one.mp begin
+  contrapose !hB,
+  rw nat_degree_eq_card_roots h2 at hB,
+  obtain ⟨z, hz⟩ := multiset.card_pos_iff_exists_mem.mp (zero_lt_iff.mpr hB),
+  exact le_trans (norm_nonneg _) (h3 z hz),
+end
+
 lemma coeff_le_of_roots_le {p : F[X]} {f : F →+* K} {B : ℝ} (i : ℕ)
   (h1 : p.monic) (h2 : splits f p) (h3 : ∀ z ∈ (map f p).roots, ∥z∥ ≤ B) :
   ∥ (map f p).coeff i ∥ ≤ B^(p.nat_degree - i) * p.nat_degree.choose i  :=
 begin
   have hcd : card (map f p).roots = p.nat_degree := (nat_degree_eq_card_roots h2).symm,
-  by_cases hB : 0 ≤ B,
+  obtain hB | hB := le_or_lt 0 B,
   { by_cases hi : i ≤ p.nat_degree,
     { rw [eq_prod_roots_of_splits h2, monic.def.mp h1, ring_hom.map_one, ring_hom.map_one, one_mul],
       rw prod_X_sub_C_coeff,
@@ -184,23 +194,32 @@ begin
       rw_mod_cast mul_zero,
       { rwa monic.nat_degree_map h1,
         apply_instance, }}},
-  { push_neg at hB,
-    have noroots : (map f p).roots = 0,
-    { contrapose! hB,
-      obtain ⟨z, hz⟩ := exists_mem_of_ne_zero hB,
-      exact le_trans (norm_nonneg z) (h3 z hz), },
-    suffices : p.nat_degree = 0,
-    { by_cases hi : i = 0,
-      { rw [this, hi, (monic.nat_degree_eq_zero_iff_eq_one h1).mp this],
-        simp only [polynomial.map_one, coeff_one_zero, norm_one, pow_zero, nat.choose_self,
-          nat.cast_one, mul_one], },
-      { replace hi := zero_lt_iff.mpr hi,
-        rw ←this at hi,
-        rw [nat.choose_eq_zero_of_lt hi, coeff_eq_zero_of_nat_degree_lt, norm_zero],
-        rw_mod_cast mul_zero,
-        { rwa monic.nat_degree_map h1,
-          apply_instance, }}},
-    rw [←hcd, noroots, card_zero], },
+  { rw [eq_one_of_roots_le hB h1 h2 h3, polynomial.map_one, nat_degree_one, zero_tsub, pow_zero,
+      one_mul, coeff_one],
+    split_ifs; norm_num [h], },
+end
+
+/-- The coefficients of the monic polynomials of bounded degree with bounded roots are
+uniformely bounded. -/
+lemma coeff_bdd_of_roots_le {B : ℝ} {d : ℕ} (f : F →+* K) {p : F[X]}
+  (h1 : p.monic) (h2 : splits f p) (h3 : p.nat_degree ≤ d) (h4 : ∀ z ∈ (map f p).roots, ∥z∥ ≤ B)
+  (i : ℕ) : ∥(map f p).coeff i∥ ≤ (max B 1) ^ d * d.choose (d / 2) :=
+begin
+  obtain hB | hB := le_or_lt 0 B,
+  { apply (coeff_le_of_roots_le i h1 h2 h4).trans,
+    calc
+    _   ≤ (max B 1) ^ (p.nat_degree - i) * (p.nat_degree.choose i)
+      : mul_le_mul_of_nonneg_right (pow_le_pow_of_le_left hB (le_max_left _ _) _) _
+    ... ≤ (max B 1) ^ d * (p.nat_degree.choose i)
+      : mul_le_mul_of_nonneg_right ((pow_mono (le_max_right _ _)) (le_trans (nat.sub_le _ _) h3)) _
+    ... ≤ (max B 1) ^ d * d.choose (d / 2)
+      : mul_le_mul_of_nonneg_left (nat.cast_le.mpr ((i.choose_mono h3).trans
+        (i.choose_le_middle d))) _,
+    all_goals { positivity, }},
+  { rw [eq_one_of_roots_le hB h1 h2 h4, polynomial.map_one, coeff_one],
+    refine trans _ (one_le_mul_of_one_le_of_one_le (one_le_pow_of_one_le (le_max_right B 1) d) _),
+    { split_ifs; norm_num, },
+    { exact_mod_cast nat.succ_le_iff.mpr (nat.choose_pos (d.div_le_self 2)), }},
 end
 
 end roots