section ‹Factor bound›
text ‹This theory extends the work about factor bounds which was carried out
in the Berlekamp-Zassenhaus development.›
theory Factor_Bound_2
imports Berlekamp_Zassenhaus.Factor_Bound
LLL_Basis_Reduction.Norms
begin
lemma norm_1_bound_mignotte: "norm1 f ≤ 2^(degree f) * mahler_measure f"
proof (cases "f = 0")
case f0: False
have cf: "coeffs f = map (λ i. coeff f i) [0 ..< Suc( degree f)]" unfolding coeffs_def
using f0 by auto
have "real_of_int (sum_list (map abs (coeffs f)))
= (∑i≤degree f. real_of_int ¦poly.coeff f i¦)"
unfolding cf of_int_hom.hom_sum_list unfolding sum_list_sum_nth
by (rule sum.cong, force, auto simp: o_def nth_append)
also have "… ≤ (∑i≤degree f. real (degree f choose i) * mahler_measure f)"
by (rule sum_mono, rule Mignotte_bound)
also have "… = real (sum (λ i. (degree f choose i)) {..degree f}) * mahler_measure f"
unfolding sum_distrib_right[symmetric] by auto
also have "… = 2^(degree f) * mahler_measure f" unfolding choose_row_sum by auto
finally show ?thesis unfolding norm1_def .
qed (auto simp: mahler_measure_ge_0 norm1_def)
lemma mahler_measure_l2norm: "mahler_measure f ≤ sqrt (of_int ∥f∥⇧^{2})"
using Landau_inequality_mahler_measure[of f] unfolding sq_norm_poly_def
by (auto simp: power2_eq_square)
lemma sq_norm_factor_bound:
fixes f h :: "int poly"
assumes dvd: "h dvd f" and f0: "f ≠ 0"
shows "∥h∥⇧^{2} ≤ 2 ^ (2 * degree h) * ∥f∥⇧^{2}"
proof -
let ?r = real_of_int
have h21: "?r ∥h∥⇧^{2} ≤ (?r (norm1 h))^2" using norm2_le_norm1_int[of h]
by (metis of_int_le_iff of_int_power)
also have "… ≤ (2^(degree h) * mahler_measure h)^2"
using power_mono[OF norm_1_bound_mignotte[of h], of 2]
by (auto simp: norm1_ge_0)
also have "… = 2^(2 * degree h) * (mahler_measure h)^2"
by (simp add: power_even_eq power_mult_distrib)
also have "… ≤ 2^(2 * degree h) * (mahler_measure f)^2"
by (rule mult_left_mono[OF power_mono], auto simp: mahler_measure_ge_0
mahler_measure_dvd[OF f0 dvd])
also have "… ≤ 2^(2 * degree h) * ?r (∥f∥⇧^{2})"
proof (rule mult_left_mono)
have "?r (∥f∥⇧^{2}) ≥ 0" by auto
from real_sqrt_pow2[OF this]
show "(mahler_measure f)⇧^{2} ≤ ?r (∥f∥⇧^{2})"
using power_mono[OF mahler_measure_l2norm[of f], of 2]
by (auto simp: mahler_measure_ge_0)
qed auto
also have "… = ?r (2^(2*degree h) * ∥f∥⇧^{2})"
by (simp add: ac_simps)
finally show "∥h∥⇧^{2} ≤ 2 ^ (2 * degree h) * ∥f∥⇧^{2}" unfolding of_int_le_iff .
qed
end