# Theory Factor_Bound

```(*
Authors:      Jose Divasón
Sebastiaan Joosten
René Thiemann
*)
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]
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
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]
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

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)
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 h¦ ≠ 0" using nz(2) by auto
hence lh: "¦lead_coeff h¦ ≥ 1" by linarith
also have "… ≥ ¦lead_coeff g¦ * 1"
by (rule mult_mono, insert lh, auto)
qed (auto simp: g0)
finally have "¦coeff g k¦ ≤ ?n * mahler_measure f + real_of_int (?n' * ¦lead_coeff f¦)" by simp
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)"
also have "… ≤ real (degree g - 1 choose k) * mahler_measure g
+ real (min k 1 * (degree g - 1 choose (k - 1))) * mahler_measure g"
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
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
```