Theory Factor_Bound

(*
    Authors:      Jose Divasón
                  Sebastiaan Joosten
                  René Thiemann
                  Akihisa Yamada
*)
subsection ‹The Mignotte Bound›
theory Factor_Bound
imports 
  Mahler_Measure
  Polynomial_Factorization.Gauss_Lemma
  Subresultants.Coeff_Int 
begin

lemma binomial_mono_left: "n ≤ N ⟹ n choose k ≤ N choose k" 
proof (induct n arbitrary: k N)
  case (0 k N)
  thus ?case by (cases k, auto)
next
  case (Suc n k N) note IH = this
  show ?case
  proof (cases k)
    case (Suc kk)
    from IH obtain NN where N: "N = Suc NN" and le: "n ≤ NN" by (cases N, auto)     
    show ?thesis unfolding N Suc using IH(1)[OF le] 
      by (simp add: add_le_mono)
  qed auto
qed

definition choose_int where "choose_int m n = (if n < 0 then 0 else m choose (nat n))"

lemma choose_int_suc[simp]:
  "choose_int (Suc n) i = choose_int n (i-1) + choose_int n i"
proof(cases "nat i")
  case 0 thus ?thesis by (simp add:choose_int_def) next
  case (Suc v) hence "nat (i - 1) = v" "i≠0" by simp_all
    thus ?thesis unfolding choose_int_def Suc by simp
qed

lemma sum_le_1_prod: assumes d: "1 ≤ d" and c: "1 ≤ c"
  shows "c + d ≤ 1 + c * (d :: real)"
proof -
  from d c have "(c - 1) * (d - 1) ≥ 0" by auto
  thus ?thesis by (auto simp: field_simps)
qed

lemma mignotte_helper_coeff_int: "cmod (coeff_int (∏a←lst. [:- a, 1:]) i)
    ≤ choose_int (length lst - 1) i * (∏a←lst. (max 1 (cmod a))) 
    + choose_int (length lst - 1) (i - 1)"
proof(induct lst arbitrary:i)
  case Nil thus ?case by (auto simp:coeff_int_def choose_int_def)
  case (Cons v xs i)
  show ?case
  proof (cases "xs = []")
    case True
    show ?thesis unfolding True
      by (cases "nat i", cases "nat (i - 1)", auto simp: coeff_int_def choose_int_def)
  next
    case False
    hence id: "length (v # xs) - 1 = Suc (length xs - 1)" by auto
    have id': "choose_int (length xs) i = choose_int (Suc (length xs - 1)) i" for i
      using False by (cases xs, auto)
    let ?r = "(∏a←xs. [:- a, 1:])"
    let ?mv = "(∏a←xs. (max 1 (cmod a)))"
    let ?c1 = "real (choose_int (length xs - 1) (i - 1 - 1))" 
    let ?c2 = "real (choose_int (length (v # xs) - 1) i - choose_int (length xs - 1) i)" 
    let "?m xs n" = "choose_int (length xs - 1) n * (∏a←xs. (max 1 (cmod a)))"
    have le1:"1 ≤ max 1 (cmod v)" by auto
    have le2:"cmod v ≤ max 1 (cmod v)" by auto
    have mv_ge_1:"1 ≤ ?mv" by (rule prod_list_ge1, auto)
    obtain a b c d where abcd : 
      "a = real (choose_int (length xs - 1) i)" 
      "b = real (choose_int (length xs - 1) (i - 1))" 
      "c = (∏a←xs. max 1 (cmod a))" 
      "d = cmod v" by auto
    {
      have c1: "c ≥ 1" unfolding abcd by (rule mv_ge_1)
      have b: "b = 0 ∨ b ≥ 1" unfolding abcd by auto
      have a: "a = 0 ∨ a ≥ 1" unfolding abcd by auto
      hence a0: "a ≥ 0" by auto
      have acd: "a * (c * d) ≤ a * (c * max 1 d)" using a0 c1
        by (simp add: mult_left_mono)
      from b have "b * (c + d) ≤ b * (1  + (c * max 1 d))" 
      proof 
        assume "b ≥ 1" 
        hence "?thesis = (c + d ≤ 1 + c * max 1 d)" by simp
        also have …
        proof (cases "d ≥ 1")
          case False
          hence id: "max 1 d = 1" by simp
          show ?thesis using False unfolding id by simp
        next
          case True
          hence id: "max 1 d = d" by simp
          show ?thesis using True c1 unfolding id by (rule sum_le_1_prod)
        qed
        finally show ?thesis .
      qed auto
      with acd have "b * c + (b * d + a * (c * d)) ≤ b + (a * (c * max 1 d) + b * (c * max 1 d))" 
        by (auto simp: field_simps)
    } note abcd_main = this      
    have "cmod (coeff_int ([:- v, 1:] * ?r) i) ≤ cmod (coeff_int ?r (i - 1)) + cmod (coeff_int (smult v ?r) i)"
      using norm_triangle_ineq4 by auto
    also have "… ≤ ?m xs (i - 1) + (choose_int (length xs - 1) (i - 1 - 1)) + cmod (coeff_int (smult v ?r) i)" 
      using Cons[of "i-1"] by auto
    also have "choose_int (length xs - 1) (i - 1) = choose_int (length (v # xs) - 1) i - choose_int (length xs - 1) i" 
      unfolding id choose_int_suc by auto
    also have "?c2 * (∏a←xs. max 1 (cmod a)) + ?c1 +
       cmod (coeff_int (smult v (∏a←xs. [:- a, 1:])) i) ≤ 
       ?c2 * (∏a←xs. max 1 (cmod a)) + ?c1 + cmod v * (
         real (choose_int (length xs - 1) i) * (∏a←xs. max 1 (cmod a)) + 
         real (choose_int (length xs - 1) (i - 1)))"
      using mult_mono'[OF order_refl Cons, of "cmod v" i, simplified] by (auto simp: norm_mult)
    also have "… ≤ ?m (v # xs) i + (choose_int (length xs) (i - 1))" using abcd_main[unfolded abcd]
      by (simp add: field_simps id')
    finally show ?thesis by simp
  qed
qed

lemma mignotte_helper_coeff_int': "cmod (coeff_int (∏a←lst. [:- a, 1:]) i)
    ≤ ((length lst - 1) choose i) * (∏a←lst. (max 1 (cmod a))) 
    + min i 1 * ((length lst - 1) choose (nat (i - 1)))"
  by (rule order.trans[OF mignotte_helper_coeff_int], auto simp: choose_int_def min_def)

lemma mignotte_helper_coeff: 
  "cmod (coeff h i) ≤ (degree h - 1 choose i) * mahler_measure_poly h 
      + min i 1 * (degree h - 1 choose (i - 1)) * cmod (lead_coeff h)"
proof -
  let ?r = "complex_roots_complex h"
  have "cmod (coeff h i) = cmod (coeff (smult (lead_coeff h) (∏a←?r. [:- a, 1:])) i)"
    unfolding complex_roots by auto
  also have "… = cmod (lead_coeff h) * cmod (coeff (∏a←?r. [:- a, 1:]) i)" by(simp add:norm_mult)
  also have "… ≤ cmod (lead_coeff h) * ((degree h - 1 choose i) * mahler_measure_monic h + 
    (min i 1 * ((degree h - 1) choose nat (int i - 1))))"    
    unfolding mahler_measure_monic_def
    by (rule mult_left_mono, insert mignotte_helper_coeff_int'[of ?r i], auto)
  also have "… = (degree h - 1 choose i) * mahler_measure_poly h + cmod (lead_coeff h) * (
    min i 1 * ((degree h - 1) choose nat (int i - 1)))" 
    unfolding mahler_measure_poly_via_monic by (simp add: field_simps)
  also have "nat (int i - 1) = i - 1" by (cases i, auto)
  finally show ?thesis by (simp add: ac_simps split: if_splits)
qed

lemma mignotte_coeff_helper:
  "abs (coeff h i) ≤ 
   (degree h - 1 choose i) * mahler_measure h +
   (min i 1 * (degree h - 1 choose (i - 1)) * abs (lead_coeff h))"
  unfolding mahler_measure_def
  using mignotte_helper_coeff[of "of_int_poly h" i] 
  by auto

lemma cmod_through_lead_coeff[simp]:
  "cmod (lead_coeff (of_int_poly h)) = abs (lead_coeff h)"
  by simp

lemma choose_approx: "n ≤ N ⟹ n choose k ≤ N choose (N div 2)" 
  by (rule order.trans[OF binomial_mono_left binomial_maximum])

text ‹For Mignotte's factor bound, we currently do not support queries for individual coefficients,
  as we do not have a combined factor bound algorithm.›

definition mignotte_bound :: "int poly ⇒ nat ⇒ int" where
  "mignotte_bound f d = (let d' = d - 1; d2 = d' div 2; binom = (d' choose d2) in
     (mahler_approximation 2 binom f + binom * abs (lead_coeff f)))" 

lemma mignotte_bound_main:  
  assumes "f ≠ 0" "g dvd f" "degree g ≤ n"
  shows "¦coeff g k¦ ≤ ⌊real (n - 1 choose k) * mahler_measure f⌋ +
       int (min k 1 * (n - 1 choose (k - 1))) * ¦lead_coeff f¦"   
proof-
  let ?bnd = 2
  let ?n = "(n - 1) choose k" 
  let ?n' = "min k 1 * ((n - 1) choose (k - 1))" 
  let ?approx = "mahler_approximation ?bnd ?n f" 
  obtain h where gh:"g * h = f" using assms by (metis dvdE)
  have nz:"g≠0" "h≠0" using gh assms(1) by auto
  have g1:"(1::real) ≤ mahler_measure h" using mahler_measure_poly_ge_1 gh assms(1) by auto
  note g0 = mahler_measure_ge_0
  have to_n: "(degree g - 1 choose k) ≤ real ?n"
    using binomial_mono_left[of "degree g - 1" "n - 1" k] assms(3) by auto
  have to_n': "min k 1 * (degree g - 1 choose (k - 1)) ≤ real ?n'"
    using binomial_mono_left[of "degree g - 1" "n - 1" "k - 1"] assms(3)
    by (simp add: min_def)
  have "¦coeff g k¦ ≤ (degree g - 1 choose k) * mahler_measure g
    + (real (min k 1 * (degree g - 1 choose (k - 1))) * ¦lead_coeff g¦)" 
    using mignotte_coeff_helper[of g k] by simp
  also have "… ≤ ?n * mahler_measure f + real ?n' * ¦lead_coeff f¦"
  proof (rule add_mono[OF mult_mono[OF to_n] mult_mono[OF to_n']])
    have "mahler_measure g  ≤ mahler_measure g * mahler_measure h" using g1 g0[of g]
      using mahler_measure_poly_ge_1 nz(1) by force
    thus "mahler_measure g ≤ mahler_measure f"
      using measure_eq_prod[of "of_int_poly g" "of_int_poly h"]
      unfolding mahler_measure_def gh[symmetric] by (auto simp: hom_distribs)
    have *: "lead_coeff f = lead_coeff g * lead_coeff h" 
      unfolding arg_cong[OF gh, of lead_coeff, symmetric] by (rule lead_coeff_mult)
    have "¦lead_coeff h¦ ≠ 0" using nz(2) by auto
    hence lh: "¦lead_coeff h¦ ≥ 1" by linarith
    have "¦lead_coeff f¦ = ¦lead_coeff g¦ * ¦lead_coeff h¦" unfolding * by (rule abs_mult)
    also have "… ≥ ¦lead_coeff g¦ * 1" 
      by (rule mult_mono, insert lh, auto)
    finally have "¦lead_coeff g¦ ≤ ¦lead_coeff f¦" by simp
    thus "real_of_int ¦lead_coeff g¦ ≤ real_of_int ¦lead_coeff f¦" by simp
  qed (auto simp: g0)
  finally have "¦coeff g k¦ ≤ ?n * mahler_measure f + real_of_int (?n' * ¦lead_coeff f¦)" by simp
  from floor_mono[OF this, folded floor_add_int]
  have "¦coeff g k¦ ≤ floor (?n * mahler_measure f) + ?n' * ¦lead_coeff f¦" by linarith
  thus ?thesis unfolding mignotte_bound_def Let_def using mahler_approximation[of ?n f ?bnd] by auto
qed

lemma Mignotte_bound: 
  shows "of_int ¦coeff g k¦ ≤ (degree g choose k) * mahler_measure g"
proof (cases "k ≤ degree g ∧ g ≠ 0")
  case False
  hence "coeff g k = 0" using le_degree by (cases "g = 0", auto)
  thus ?thesis using mahler_measure_ge_0[of g] by auto
next
  case kg: True
  hence g: "g ≠ 0" "g dvd g" by auto
  from mignotte_bound_main[OF g le_refl, of k]
  have "real_of_int ¦coeff g k¦
    ≤ of_int ⌊real (degree g - 1 choose k) * mahler_measure g⌋ +
      of_int (int (min k 1 * (degree g - 1 choose (k - 1))) * ¦lead_coeff g¦)" by linarith
  also have "… ≤ real (degree g - 1 choose k) * mahler_measure g 
     + real (min k 1 * (degree g - 1 choose (k - 1))) * (of_int ¦lead_coeff g¦ * 1)"
    by (rule add_mono, force, auto)
  also have "… ≤ real (degree g - 1 choose k) * mahler_measure g 
     + real (min k 1 * (degree g - 1 choose (k - 1))) * mahler_measure g"
    by (rule add_left_mono[OF mult_left_mono], 
    unfold mahler_measure_def mahler_measure_poly_def,
    rule mult_mono, auto intro!: prod_list_ge1)  
  also have "… = 
    (real ((degree g - 1 choose k) + (min k 1 * (degree g - 1 choose (k - 1))))) * mahler_measure g" 
    by (auto simp: field_simps)
  also have "(degree g - 1 choose k) + (min k 1 * (degree g - 1 choose (k - 1))) = degree g choose k"
  proof (cases "k = 0")
    case False
    then obtain kk where k: "k = Suc kk" by (cases k, auto)
    with kg obtain gg where g: "degree g = Suc gg" by (cases "degree g", auto)
    show ?thesis unfolding k g by auto
  qed auto
  finally show ?thesis .
qed

lemma mignotte_bound:  
  assumes "f ≠ 0" "g dvd f" "degree g ≤ n"
  shows "¦coeff g k¦ ≤ mignotte_bound f n"  
proof -
  let ?bnd = 2
  let ?n = "(n - 1) choose ((n - 1) div 2)" 
  have to_n: "(n - 1 choose k) ≤ real ?n" for k
    using choose_approx[OF le_refl] by auto
  from mignotte_bound_main[OF assms, of k]
  have "¦coeff g k¦ ≤ 
    ⌊real (n - 1 choose k) * mahler_measure f⌋ + 
    int (min k 1 * (n - 1 choose (k - 1))) * ¦lead_coeff f¦" .
  also have "… ≤ ⌊real (n - 1 choose k) * mahler_measure f⌋ + 
    int ((n - 1 choose (k - 1))) * ¦lead_coeff f¦"
    by (rule add_left_mono[OF mult_right_mono], cases k, auto)
  also have "… ≤ mignotte_bound f n" 
    unfolding mignotte_bound_def Let_def
    by (rule add_mono[OF order.trans[OF floor_mono[OF mult_right_mono] 
    mahler_approximation[of ?n f ?bnd]] mult_right_mono], insert to_n mahler_measure_ge_0, auto)
  finally show ?thesis .
qed

text ‹As indicated before, at the moment the only available factor bound is Mignotte's one.
  As future work one might use a combined bound.›

definition factor_bound :: "int poly ⇒ nat ⇒ int" where
  "factor_bound = mignotte_bound"

lemma factor_bound: assumes "f ≠ 0" "g dvd f" "degree g ≤ n"
  shows "¦coeff g k¦ ≤ factor_bound f n"
  unfolding factor_bound_def by (rule mignotte_bound[OF assms])

text ‹We further prove a result for factor bounds and scalar multiplication.›

lemma factor_bound_ge_0: "f ≠ 0 ⟹ factor_bound f n ≥ 0" 
  using factor_bound[of f 1 n 0] by auto

lemma factor_bound_smult: assumes f: "f ≠ 0" and d: "d ≠ 0" 
  and dvd: "g dvd smult d f" and deg: "degree g ≤ n" 
  shows "¦coeff g k¦ ≤ ¦d¦ * factor_bound f n" 
proof -
  let ?nf = "primitive_part f" let ?cf = "content f" 
  let ?ng = "primitive_part g" let ?cg = "content g" 
  from content_dvd_contentI[OF dvd] have "?cg dvd abs d * ?cf" 
    unfolding content_smult_int .  
  hence dvd_c: "?cg dvd d * ?cf" using d
    by (metis abs_content_int abs_mult dvd_abs_iff)
  from primitive_part_dvd_primitive_partI[OF dvd] have "?ng dvd smult (sgn d) ?nf" unfolding primitive_part_smult_int .
  hence dvd_n: "?ng dvd ?nf" using d 
    by (metis content_eq_zero_iff dvd dvd_smult_int f mult_eq_0_iff content_times_primitive_part smult_smult)
  define gc where "gc = gcd ?cf ?cg" 
  define cg where "cg = ?cg div gc"   
  from dvd d f have g: "g ≠ 0" by auto  
  from f have cf: "?cf ≠ 0" by auto
  from g have cg: "?cg ≠ 0" by auto
  hence gc: "gc ≠ 0" unfolding gc_def by auto
  have cg_dvd: "cg dvd ?cg" unfolding cg_def gc_def using g by (simp add: div_dvd_iff_mult)
  have cg_id: "?cg = cg * gc" unfolding gc_def cg_def using g cf by simp
  from dvd_smult_int[OF d dvd] have ngf: "?ng dvd f" .
  have gcf: "¦gc¦ dvd content f" unfolding gc_def by auto
  have dvd_f: "smult gc ?ng dvd f" 
  proof (rule dvd_content_dvd, 
      unfold content_smult_int content_primitive_part[OF g] 
      primitive_part_smult_int primitive_part_idemp)
    show "¦gc¦ * 1 dvd content f" using gcf by auto
    show "smult (sgn gc) (primitive_part g) dvd primitive_part f" 
      using dvd_n cf gc using zsgn_def by force
  qed    
  have "cg dvd d" using dvd_c unfolding gc_def cg_def using cf cg d
    by (simp add: div_dvd_iff_mult dvd_gcd_mult)
  then obtain h where dcg: "d = cg * h" unfolding dvd_def by auto
  with d have "h ≠ 0" by auto
  hence h1: "¦h¦ ≥ 1" by simp
  have "degree (smult gc (primitive_part g)) = degree g" 
    using gc by auto
  from factor_bound[OF f dvd_f, unfolded this, OF deg, of k, unfolded coeff_smult]
  have le: "¦gc * coeff ?ng k¦ ≤ factor_bound f n" .
  note f0 = factor_bound_ge_0[OF f, of n]
  from mult_left_mono[OF le, of "abs cg"]
  have "¦cg * gc * coeff ?ng k¦ ≤ ¦cg¦ * factor_bound f n" 
    unfolding abs_mult[symmetric] by simp
  also have "cg * gc * coeff ?ng k = coeff (smult ?cg ?ng) k" unfolding cg_id by simp
  also have "… = coeff g k" unfolding content_times_primitive_part by simp
  finally have "¦coeff g k¦ ≤ 1 * (¦cg¦ * factor_bound f n)" by simp
  also have "… ≤ ¦h¦ * (¦cg¦ * factor_bound f n)" 
    by (rule mult_right_mono[OF h1], insert f0, auto)
  also have "… = (¦cg * h¦) * factor_bound f n" by (simp add: abs_mult)
  finally show ?thesis unfolding dcg .
qed

end