section ‹Normal Polynomials› theory Normal_Poly imports "RRI_Misc" begin text ‹ Here we define normal polynomials as defined in Basu, S., Pollack, R., Roy, M.-F.: Algorithms in Real Algebraic Geometry. Springer Berlin Heidelberg, Berlin, Heidelberg (2016). › definition normal_poly :: "('a::{comm_ring_1,ord}) poly ⇒ bool" where "normal_poly p ≡ (p ≠ 0) ∧ (∀ i. 0 ≤ coeff p i) ∧ (∀ i. coeff p i * coeff p (i+2) ≤ (coeff p (i+1))^2) ∧ (∀ i j k. i ≤ j ⟶ j ≤ k ⟶ 0 < coeff p i ⟶ 0 < coeff p k ⟶ 0 < coeff p j)" lemma normal_non_zero: "normal_poly p ⟹ p ≠ 0" using normal_poly_def by blast lemma normal_coeff_nonneg: "normal_poly p ⟹ 0 ≤ coeff p i" using normal_poly_def by metis lemma normal_poly_coeff_mult: "normal_poly p ⟹ coeff p i * coeff p (i+2) ≤ (coeff p (i+1))^2" using normal_poly_def by blast lemma normal_poly_pos_interval: "normal_poly p ⟹ i ≤ j ⟹ j ≤ k ⟹ 0 < coeff p i ⟹ 0 < coeff p k ⟹ 0 < coeff p j" using normal_poly_def by blast lemma normal_polyI: assumes "(p ≠ 0)" and "(⋀ i. 0 ≤ coeff p i)" and "(⋀ i. coeff p i * coeff p (i+2) ≤ (coeff p (i+1))^2)" and "(⋀ i j k. i ≤ j ⟹ j ≤ k ⟹ 0 < coeff p i ⟹ 0 < coeff p k ⟹ 0 < coeff p j)" shows "normal_poly p" using assms by (force simp: normal_poly_def) lemma linear_normal_iff: fixes x::real shows "normal_poly [:-x, 1:] ⟷ x ≤ 0" proof assume "normal_poly [:-x, 1:]" thus "x ≤ 0" using normal_coeff_nonneg[of "[:-x, 1:]" 0] by auto next assume "x ≤ 0" then have "0 ≤ coeff [:- x, 1:] i" for i by (cases i) (simp_all add: pCons_one) moreover have "0 < coeff [:- x, 1:] j" if "i ≤ j" "j ≤ k" "0 < coeff [:- x, 1:] i" "0 < coeff [:- x, 1:] k" for i j k apply (cases "k=0 ∨ i=0") subgoal using that by (smt (z3) bot_nat_0.extremum_uniqueI degree_pCons_eq_if le_antisym le_degree not_less_eq_eq) subgoal using that by (smt (z3) One_nat_def degree_pCons_eq_if le_degree less_one not_le one_neq_zero pCons_one verit_la_disequality) done ultimately show "normal_poly [:-x, 1:]" unfolding normal_poly_def by auto qed lemma quadratic_normal_iff: fixes z::complex shows "normal_poly [:(cmod z)⇧^{2}, -2*Re z, 1:] ⟷ Re z ≤ 0 ∧ 4*(Re z)^2 ≥ (cmod z)^2" proof assume "normal_poly [:(cmod z)⇧^{2}, - 2 * Re z, 1:]" hence "-2*Re z ≥ 0 ∧ (cmod z)^2 ≥ 0 ∧ (-2*Re z)^2 ≥ (cmod z)^2" using normal_coeff_nonneg[of _ 1] normal_poly_coeff_mult[of _ 0] by fastforce thus "Re z ≤ 0 ∧ 4*(Re z)^2 ≥ (cmod z)^2" by auto next assume asm:"Re z ≤ 0 ∧ 4*(Re z)^2 ≥ (cmod z)^2" define P where "P=[:(cmod z)⇧^{2}, - 2 * Re z, 1:]" have "0 ≤ coeff P i" for i unfolding P_def using asm apply (cases "i=0∨i=1∨i=2") by (auto simp:numeral_2_eq_2 coeff_eq_0) moreover have "coeff P i * coeff P (i + 2) ≤ (coeff P (i + 1))⇧^{2}" for i apply (cases "i=0∨i=1∨i=2") using asm unfolding P_def by (auto simp:coeff_eq_0) moreover have "0 < coeff P j" if "0 < coeff P k" "0 < coeff P i" "j ≤ k" "i ≤ j" for i j k using that unfolding P_def apply (cases "k=0 ∨ k=1 ∨ k=2") subgoal using asm by (smt (z3) One_nat_def Suc_1 bot_nat_0.extremum_uniqueI coeff_pCons_0 coeff_pCons_Suc le_Suc_eq zero_less_power2) subgoal by (auto simp:coeff_eq_0) done moreover have "P≠0" unfolding P_def by auto ultimately show "normal_poly P" unfolding normal_poly_def by blast qed lemma normal_of_no_zero_root: fixes f::"real poly" assumes hzero: "poly f 0 ≠ 0" and hdeg: "i ≤ degree f" and hnorm: "normal_poly f" shows "0 < coeff f i" proof - have "coeff f 0 > 0" using hzero normal_coeff_nonneg[OF hnorm] by (metis eq_iff not_le_imp_less poly_0_coeff_0) moreover have "coeff f (degree f) > 0" using normal_coeff_nonneg[OF hnorm] normal_non_zero[OF hnorm] by (meson dual_order.irrefl eq_iff eq_zero_or_degree_less not_le_imp_less) moreover have "0 ≤ i" by simp ultimately show "0 < coeff f i" using hdeg normal_poly_pos_interval[OF hnorm] by blast qed lemma normal_divide_x: fixes f::"real poly" assumes hnorm: "normal_poly (f*[:0,1:])" shows "normal_poly f" proof (rule normal_polyI) show "f ≠ 0" using normal_non_zero[OF hnorm] by auto next fix i show "0 ≤ coeff f i" using normal_coeff_nonneg[OF hnorm, of "Suc i"] by (simp add: coeff_pCons) next fix i show "coeff f i * coeff f (i + 2) ≤ (coeff f (i + 1))⇧^{2}" using normal_poly_coeff_mult[OF hnorm, of "Suc i"] by (simp add: coeff_pCons) next fix i j k show "i ≤ j ⟹ j ≤ k ⟹ 0 < coeff f i ⟹ 0 < coeff f k ⟹ 0 < coeff f j" using normal_poly_pos_interval[of _ "Suc i" "Suc j" "Suc k", OF hnorm] by (simp add: coeff_pCons) qed lemma normal_mult_x: fixes f::"real poly" assumes hnorm: "normal_poly f" shows "normal_poly (f * [:0, 1:])" proof (rule normal_polyI) show "f * [:0, 1:] ≠ 0" using normal_non_zero[OF hnorm] by auto next fix i show "0 ≤ coeff (f * [:0, 1:]) i" using normal_coeff_nonneg[OF hnorm, of "i-1"] by (cases i, auto simp: coeff_pCons) next fix i show "coeff (f * [:0, 1:]) i * coeff (f * [:0, 1:]) (i + 2) ≤ (coeff (f * [:0, 1:]) (i + 1))⇧^{2}" using normal_poly_coeff_mult[OF hnorm, of "i-1"] by (cases i, auto simp: coeff_pCons) next fix i j k show "i ≤ j ⟹ j ≤ k ⟹ 0 < coeff (f * [:0, 1:]) i ⟹ 0 < coeff (f * [:0, 1:]) k ⟹ 0 < coeff (f * [:0, 1:]) j" using normal_poly_pos_interval[of _ "i-1" "j-1" "k-1", OF hnorm] apply (cases i, force) apply (cases j, force) apply (cases k, force) by (auto simp: coeff_pCons) qed lemma normal_poly_general_coeff_mult: fixes f::"real poly" assumes "normal_poly f" and "h ≤ j" shows "coeff f (h+1) * coeff f (j+1) ≥ coeff f h * coeff f (j+2)" using assms proof (induction j) case 0 then show ?case using normal_poly_coeff_mult by (auto simp: power2_eq_square)[1] next case (Suc j) then show ?case proof (cases "h = Suc j") assume "h = Suc j" "normal_poly f" thus ?thesis using normal_poly_coeff_mult by (auto simp: power2_eq_square) next assume "(normal_poly f ⟹ h ≤ j ⟹ coeff f h * coeff f (j + 2) ≤ coeff f (h + 1) * coeff f (j + 1))" "normal_poly f" and h: "h ≤ Suc j" "h ≠ Suc j" hence IH: "coeff f h * coeff f (j + 2) ≤ coeff f (h + 1) * coeff f (j + 1)" by linarith show ?thesis proof (cases "coeff f (Suc j + 1) = 0", cases "coeff f (Suc j + 2) = 0") show "coeff f (Suc j + 1) = 0 ⟹ coeff f (Suc j + 2) = 0 ⟹ coeff f h * coeff f (Suc j + 2) ≤ coeff f (h + 1) * coeff f (Suc j + 1)" by (metis assms(1) mult_zero_right normal_coeff_nonneg) next assume 1: "coeff f (Suc j + 1) = 0" "coeff f (Suc j + 2) ≠ 0" hence "coeff f (Suc j + 2) > 0" "¬coeff f (Suc j + 1) > 0" using normal_coeff_nonneg[of f "Suc j + 2"] assms(1) by auto hence "coeff f h > 0 ⟹ False" using normal_poly_pos_interval[of f h "Suc j + 1" "Suc j + 2"] assms(1) h by force hence "coeff f h = 0" using normal_coeff_nonneg[OF assms(1)] less_eq_real_def by auto thus "coeff f h * coeff f (Suc j + 2) ≤ coeff f (h + 1) * coeff f (Suc j + 1)" using 1 by fastforce next assume 1: "coeff f (Suc j + 1) ≠ 0" show "coeff f h * coeff f (Suc j + 2) ≤ coeff f (h + 1) * coeff f (Suc j + 1)" proof (cases "coeff f (Suc j) = 0") assume 2: "coeff f (Suc j) = 0" hence "coeff f (Suc j + 1) > 0" "¬coeff f (Suc j) > 0" using normal_coeff_nonneg[of f "Suc j + 1"] assms(1) 1 by auto hence "coeff f h > 0 ⟹ False" using normal_poly_pos_interval[of f h "Suc j" "Suc j + 1"] assms(1) h by force hence "coeff f h = 0" using normal_coeff_nonneg[OF assms(1)] less_eq_real_def by auto thus "coeff f h * coeff f (Suc j + 2) ≤ coeff f (h + 1) * coeff f (Suc j + 1)" by (simp add: assms(1) normal_coeff_nonneg) next assume 2: "coeff f (Suc j) ≠ 0" from normal_poly_coeff_mult[OF assms(1), of "Suc j"] normal_coeff_nonneg[OF assms(1), of "Suc j"] normal_coeff_nonneg[OF assms(1), of "Suc (Suc j)"] 1 2 have 3: "coeff f (Suc j + 1) / coeff f (Suc j) ≥ coeff f (Suc j + 2) / coeff f (Suc j + 1)" by (auto simp: power2_eq_square divide_simps algebra_simps) have "(coeff f h * coeff f (j + 2)) * (coeff f (Suc j + 2) / coeff f (Suc j + 1)) ≤ (coeff f (h + 1) * coeff f (j + 1)) * (coeff f (Suc j + 1) / coeff f (Suc j))" apply (rule mult_mono[OF IH]) using 3 by (simp_all add: assms(1) normal_coeff_nonneg) thus "coeff f h * coeff f (Suc j + 2) ≤ coeff f (h + 1) * coeff f (Suc j + 1)" using 1 2 by fastforce qed qed qed qed lemma normal_mult: fixes f g::"real poly" assumes hf: "normal_poly f" and hg: "normal_poly g" defines "df ≡ degree f" and "dg ≡ degree g" shows "normal_poly (f*g)" using df_def hf proof (induction df arbitrary: f) text ‹We shall first show that without loss of generality we may assume ‹poly f 0 ≠ 0›, this is done by induction on the degree, if 0 is a root then we derive the result from ‹f/[:0,1:]›.› fix f::"real poly" fix i::nat assume "0 = degree f" and hf: "normal_poly f" then obtain a where "f = [:a:]" using degree_0_iff by auto then show "normal_poly (f*g)" apply (subst normal_polyI) subgoal using normal_non_zero[OF hf] normal_non_zero[OF hg] by auto subgoal using normal_coeff_nonneg[of _ 0, OF hf] normal_coeff_nonneg[OF hg] by simp subgoal using normal_coeff_nonneg[of _ 0, OF hf] normal_poly_coeff_mult[OF hg] by (auto simp: algebra_simps power2_eq_square mult_left_mono)[1] subgoal using normal_non_zero[OF hf] normal_coeff_nonneg[of _ 0, OF hf] normal_poly_pos_interval[OF hg] by (simp add: zero_less_mult_iff) subgoal by simp done next case (Suc df) then show ?case proof (cases "poly f 0 = 0") assume "poly f 0 = 0" and hf:"normal_poly f" moreover then obtain f' where hdiv: "f = f'*[:0,1:]" by (smt (verit) dvdE mult.commute poly_eq_0_iff_dvd) ultimately have hf': "normal_poly f'" using normal_divide_x by blast assume "Suc df = degree f" hence "degree f' = df" using hdiv normal_non_zero[OF hf'] by (auto simp: degree_mult_eq) moreover assume "⋀f. df = degree f ⟹ normal_poly f ⟹ normal_poly (f * g)" ultimately have "normal_poly (f'*g)" using hf' by blast thus "normal_poly (f*g)" using hdiv normal_mult_x by fastforce next assume hf: "normal_poly f" and hf0: "poly f 0 ≠ 0" define dg where "dg ≡ degree g" show "normal_poly (f * g)" using dg_def hg proof (induction dg arbitrary: g) text ‹Similarly we may assume ‹poly g 0 ≠ 0›.› fix g::"real poly" fix i::nat assume "0 = degree g" and hg: "normal_poly g" then obtain a where "g = [:a:]" using degree_0_iff by auto then show "normal_poly (f*g)" apply (subst normal_polyI) subgoal using normal_non_zero[OF hg] normal_non_zero[OF hf] by auto subgoal using normal_coeff_nonneg[of _ 0, OF hg] normal_coeff_nonneg[OF hf] by simp subgoal using normal_coeff_nonneg[of _ 0, OF hg] normal_poly_coeff_mult[OF hf] by (auto simp: algebra_simps power2_eq_square mult_left_mono) subgoal using normal_non_zero[OF hf] normal_coeff_nonneg[of _ 0, OF hg] normal_poly_pos_interval[OF hf] by (simp add: zero_less_mult_iff) by simp next case (Suc dg) then show ?case proof (cases "poly g 0 = 0") assume "poly g 0 = 0" and hg:"normal_poly g" moreover then obtain g' where hdiv: "g = g'*[:0,1:]" by (smt (verit) dvdE mult.commute poly_eq_0_iff_dvd) ultimately have hg': "normal_poly g'" using normal_divide_x by blast assume "Suc dg = degree g" hence "degree g' = dg" using hdiv normal_non_zero[OF hg'] by (auto simp: degree_mult_eq) moreover assume "⋀g. dg = degree g ⟹ normal_poly g ⟹ normal_poly (f * g)" ultimately have "normal_poly (f*g')" using hg' by blast thus "normal_poly (f*g)" using hdiv normal_mult_x by fastforce next text ‹It now remains to show that $(fg)_i \geq 0$. This follows by decomposing $\{(h, j) \in \mathbf{Z}^2 | h > j\} = \{(h, j) \in \mathbf{Z}^2 | h \leq j\} \cup \{(h, h - 1) \in \mathbf{Z}^2 | h \in \mathbf{Z}\}$. Note in order to avoid working with infinite sums over integers all these sets are bounded, which adds some complexity compared to the proof of lemma 2.55 in Basu, S., Pollack, R., Roy, M.-F.: Algorithms in Real Algebraic Geometry. Springer Berlin Heidelberg, Berlin, Heidelberg (2016).› assume hg0: "poly g 0 ≠ 0" and hg: "normal_poly g" have "f * g ≠ 0" using hf hg by (simp add: normal_non_zero Suc.prems) moreover have "⋀i. coeff (f*g) i ≥ 0" apply (subst coeff_mult, rule sum_nonneg, rule mult_nonneg_nonneg) using normal_coeff_nonneg[OF hf] normal_coeff_nonneg[OF hg] by auto moreover have " coeff (f*g) i * coeff (f*g) (i+2) ≤ (coeff (f*g) (i+1))^2" for i proof - text ‹$(fg)_{i+1}^2 - (fg)_i(fg)_{i+2} = \left(\sum_x f_xg_{i+1-x}\right)^2 - \left(\sum_x f_xg_{i+2-x}\right)\left(\sum_x f_xg_{i-x}\right)$› have "(coeff (f*g) (i+1))^2 - coeff (f*g) i * coeff (f*g) (i+2) = (∑x≤i+1. coeff f x * coeff g (i + 1 - x)) * (∑x≤i+1. coeff f x * coeff g (i + 1 - x)) - (∑x≤i+2. coeff f x * coeff g (i + 2 - x)) * (∑x≤i. coeff f x * coeff g (i - x))" by (auto simp: coeff_mult power2_eq_square algebra_simps) text ‹$\dots = \sum_{x, y} f_xg_{i+1-x}f_yg_{i+1-y} - \sum_{x, y} f_xg_{i+2-x}f_yg_{i-y}$› also have "... = (∑x≤i+1. ∑y≤i+1. coeff f x * coeff g (i + 1 - x) * coeff f y * coeff g (i + 1 - y)) - (∑x≤i+2. ∑y≤i. coeff f x * coeff g (i + 2 - x) * coeff f y * coeff g (i - y))" by (subst sum_product, subst sum_product, auto simp: algebra_simps) text ‹$\dots = \sum_{h \leq j} f_hg_{i+1-h}f_jg_{i+1-j} + \sum_{h>j} f_hg_{i+1-h}f_jg_{i+1-j} - \sum_{h \leq j} f_hg_{i+2-h}f_jg_{i-j} - \sum_{h>j} f_hg_{i+2-h}f_jg_{i-j}$› also have "... = (∑(h, j)∈{(h, j). i+1 ≥ j ∧ j ≥ h}. coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j)) + (∑(h, j)∈{(h, j). i+1 ≥ h ∧ h > j}. coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j)) - ((∑(h, j)∈{(h, j). i ≥ j ∧ j ≥ h}. coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j)) + (∑(h, j)∈{(h, j). i + 2 ≥ h ∧ h > j ∧ i ≥ j}. coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j)))" proof - have "(∑x≤i + 1. ∑y≤i + 1. coeff f x * coeff g (i + 1 - x) * coeff f y * coeff g (i + 1 - y)) = (∑(h, j)∈{(h, j). j ≤ i + 1 ∧ h ≤ j}. coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j)) + (∑(h, j)∈{(h, j). h ≤ i + 1 ∧ j < h}. coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j))" proof (subst sum.union_disjoint[symmetric]) have H:"{(h, j). j ≤ i + 1 ∧ h ≤ j} ⊆ {..i+1} × {..i+1}" "{(h, j). h ≤ i + 1 ∧ j < h} ⊆ {..i+1} × {..i+1}" "finite ({..i+1} × {..i+1})" by (fastforce, fastforce, fastforce) show "finite {(h, j). j ≤ i + 1 ∧ h ≤ j}" apply (rule finite_subset) using H by (blast, blast) show "finite {(h, j). h ≤ i + 1 ∧ j < h}" apply (rule finite_subset) using H by (blast, blast) show "{(h, j). j ≤ i + 1 ∧ h ≤ j} ∩ {(h, j). h ≤ i + 1 ∧ j < h} = {}" by fastforce show "(∑x≤i + 1. ∑y≤i + 1. coeff f x * coeff g (i + 1 - x) * coeff f y * coeff g (i + 1 - y)) = (∑(h, j)∈{(h, j). j ≤ i + 1 ∧ h ≤ j} ∪ {(h, j). h ≤ i + 1 ∧ j < h}. coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j))" apply (subst sum.cartesian_product, rule sum.cong) apply force by blast qed moreover have "(∑x≤i + 2. ∑y≤i. coeff f x * coeff g (i + 2 - x) * coeff f y * coeff g (i - y)) = (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j}. coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j)) + (∑(h, j)∈{(h, j). i + 2 ≥ h ∧ h > j ∧ i ≥ j}. coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j))" proof (subst sum.union_disjoint[symmetric]) have H:"{(h, j). j ≤ i ∧ h ≤ j} ⊆ {..i+2} × {..i}" "{(h, j). i + 2 ≥ h ∧ h > j ∧ i ≥ j} ⊆ {..i+2} × {..i}" "finite ({..i+2} × {..i})" by (fastforce, fastforce, fastforce) show "finite {(h, j). j ≤ i ∧ h ≤ j}" apply (rule finite_subset) using H by (blast, blast) show "finite {(h, j). i + 2 ≥ h ∧ h > j ∧ i ≥ j}" apply (rule finite_subset) using H by (blast, blast) show "{(h, j). j ≤ i ∧ h ≤ j} ∩ {(h, j). i + 2 ≥ h ∧ h > j ∧ i ≥ j} = {}" by fastforce show "(∑x≤i + 2. ∑y≤i. coeff f x * coeff g (i + 2 - x) * coeff f y * coeff g (i - y)) = (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j} ∪ {(h, j). i + 2 ≥ h ∧ h > j ∧ i ≥ j}. coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j))" apply (subst sum.cartesian_product, rule sum.cong) apply force by blast qed ultimately show ?thesis by presburger qed text ‹$\dots = \sum_{h \leq j} f_hg_{i+1-h}f_jg_{i+1-j} + \sum_{h \leq j} f_{j+1}g_{i-j}f_{h-2}g_{i+2-h} + \sum_h f_hg_{i+1-h}f_{h-1}g_{i+2-h} - \sum_{h \leq j} f_hg_{i+2-h}f_jg_{i-j} - \sum_{h \leq j} f_{j+1}g_{i+1-j}f_{h-2}g_{i+1-h} - \sum_h f_hg_{i+2-h}f_{h-1}g_{i+1-h}$› also have "... = (∑(h, j)∈{(h, j). j ≤ i + 1 ∧ h ≤ j}. coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j)) + (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}. coeff f (j+1) * coeff g (i - j) * coeff f (h-1) * coeff g (i + 2 - h)) + (∑h∈{1..i+1}. coeff f h * coeff g (i + 1 - h) * coeff f (h-1) * coeff g (i + 2 - h)) - ((∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j}. coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j)) + (∑(h, j)∈{(h, j). j ≤ i + 1 ∧ h ≤ j ∧ 0 < h}. coeff f (j+1) * coeff g (i + 1 - j) * coeff f (h-1) * coeff g (i + 1 - h)) + (∑h∈{1..i+1}. coeff f h * coeff g (i + 2 - h) * coeff f (h-1) * coeff g (i + 1 - h)))" proof - have "(∑(h, j)∈{(h, j). h ≤ i + 1 ∧ j < h}. coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j)) = (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}. coeff f (j + 1) * coeff g (i - j) * coeff f (h - 1) * coeff g (i + 2 - h)) + (∑h = 1..i + 1. coeff f h * coeff g (i + 1 - h) * coeff f (h - 1) * coeff g (i + 2 - h))" proof - have 1: "(∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}. coeff f (j + 1) * coeff g (i - j) * coeff f (h - 1) * coeff g (i + 2 - h)) = (∑(h, j)∈{(h, j). h ≤ i + 1 ∧ j < h ∧ h ≠ j + 1}. coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j))" proof (rule sum.reindex_cong) show "{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h} = (λ(h, j). (j+1, h-1)) ` {(h, j). h ≤ i + 1 ∧ j < h ∧ h ≠ j + 1}" proof show "(λ(h, j). (j + 1, h - 1)) ` {(h, j). h ≤ i + 1 ∧ j < h ∧ h ≠ j + 1} ⊆ {(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}" by fastforce show "{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h} ⊆ (λ(h, j). (j + 1, h - 1)) ` {(h, j). h ≤ i + 1 ∧ j < h ∧ h ≠ j + 1}" proof fix x assume "x ∈ {(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}" then obtain h j where "x = (h, j)" "j ≤ i" "h ≤ j" "0 < h" by blast hence "j + 1 ≤ i + 1 ∧ h - 1 < j + 1 ∧ j + 1 ≠ h - 1 + 1 ∧ x = ((h - 1) + 1, (j + 1) - 1)" by auto thus "x ∈ (λ(h, j). (j + 1, h - 1)) ` {(h, j). h ≤ i + 1 ∧ j < h ∧ h ≠ j + 1}" by (auto simp: image_iff) qed qed show "inj_on (λ(h, j). (j + 1, h - 1)) {(h, j). h ≤ i + 1 ∧ j < h ∧ h ≠ j + 1}" proof fix x y::"nat×nat" assume "x ∈ {(h, j). h ≤ i + 1 ∧ j < h ∧ h ≠ j + 1}" "y ∈ {(h, j). h ≤ i + 1 ∧ j < h ∧ h ≠ j + 1}" thus "(case x of (h, j) ⇒ (j + 1, h - 1)) = (case y of (h, j) ⇒ (j + 1, h - 1)) ⟹ x = y" by auto qed show "⋀x. x ∈ {(h, j). h ≤ i + 1 ∧ j < h ∧ h ≠ j + 1} ⟹ (case case x of (h, j) ⇒ (j + 1, h - 1) of (h, j) ⇒ coeff f (j + 1) * coeff g (i - j) * coeff f (h - 1) * coeff g (i + 2 - h)) = (case x of (h, j) ⇒ coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j))" by fastforce qed have 2: "(∑h = 1..i + 1. coeff f h * coeff g (i + 1 - h) * coeff f (h - 1) * coeff g (i + 2 - h)) = (∑(h, j)∈{(h, j). h ≤ i + 1 ∧ j < h ∧ h = j + 1}. coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j))" proof (rule sum.reindex_cong) show "{1..i + 1} = fst ` {(h, j). h ≤ i + 1 ∧ j < h ∧ h = j + 1}" proof show "{1..i + 1} ⊆ fst ` {(h, j). h ≤ i + 1 ∧ j < h ∧ h = j + 1}" proof fix x assume "x ∈ {1..i + 1}" hence "x ≤ i + 1 ∧ x - 1 < x ∧ x = x - 1 + 1 ∧ x = fst (x, x-1)" by auto thus "x ∈ fst ` {(h, j). h ≤ i + 1 ∧ j < h ∧ h = j + 1}" by blast qed show "fst ` {(h, j). h ≤ i + 1 ∧ j < h ∧ h = j + 1} ⊆ {1..i + 1}" by force qed show "inj_on fst {(h, j). h ≤ i + 1 ∧ j < h ∧ h = j + 1}" proof fix x y assume "x ∈ {(h, j). h ≤ i + 1 ∧ j < h ∧ h = j + 1}" "y ∈ {(h, j). h ≤ i + 1 ∧ j < h ∧ h = j + 1}" hence "x = (fst x, fst x - 1)" "y = (fst y, fst y - 1)" "fst x > 0" "fst y > 0" by auto thus "fst x = fst y ⟹ x = y" by presburger qed show "⋀x. x ∈ {(h, j). h ≤ i + 1 ∧ j < h ∧ h = j + 1} ⟹ coeff f (fst x) * coeff g (i + 1 - fst x) * coeff f (fst x - 1) * coeff g (i + 2 - fst x) = (case x of (h, j) ⇒ coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j))" by fastforce qed have H: "{(h, j). h ≤ i + 1 ∧ j < h ∧ h ≠ j + 1} ⊆ {0..i+1}×{0..i+1}" "{(h, j). h ≤ i + 1 ∧ j < h ∧ h = j + 1} ⊆ {0..i+1}×{0..i+1}" "finite ({0..i+1}×{0..i+1})" by (fastforce, fastforce, fastforce) have "finite {(h, j). h ≤ i + 1 ∧ j < h ∧ h ≠ j + 1}" "finite {(h, j). h ≤ i + 1 ∧ j < h ∧ h = j + 1}" apply (rule finite_subset) using H apply (simp, simp) apply (rule finite_subset) using H apply (simp, simp) done thus ?thesis apply (subst 1, subst 2, subst sum.union_disjoint[symmetric]) apply auto[3] apply (rule sum.cong) by auto qed moreover have "(∑(h, j)∈{(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i}. coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j)) = (∑(h, j)∈{(h, j). j ≤ i + 1 ∧ h ≤ j ∧ 0 < h}. coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)) + (∑h = 1..i + 1. coeff f h * coeff g (i + 2 - h) * coeff f (h - 1) * coeff g (i + 1 - h))" proof - have 1: "(∑(h, j)∈{(h, j). j ≤ i + 1 ∧ h ≤ j ∧ 0 < h}. coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)) = (∑(h, j)∈{(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h ≠ j + 1}. coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j))" proof (rule sum.reindex_cong) show "{(h, j). j ≤ i + 1 ∧ h ≤ j ∧ 0 < h} = (λ(h, j). (j+1, h-1)) ` {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h ≠ j + 1}" proof show "(λ(h, j). (j + 1, h - 1)) ` {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h ≠ j + 1} ⊆ {(h, j). j ≤ i + 1 ∧ h ≤ j ∧ 0 < h}" by fastforce show "{(h, j). j ≤ i + 1 ∧ h ≤ j ∧ 0 < h} ⊆ (λ(h, j). (j + 1, h - 1)) ` {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h ≠ j + 1}" proof fix x assume "x ∈ {(h, j). j ≤ i + 1 ∧ h ≤ j ∧ 0 < h}" then obtain h j where "x = (h, j)" "j ≤ i + 1" "h ≤ j" "0 < h" by blast hence "j + 1 ≤ i + 2 ∧ h - 1 < j + 1 ∧ h - 1 ≤ i ∧ j + 1 ≠ h - 1 + 1 ∧ x = ((h - 1) + 1, (j + 1) - 1)" by auto thus "x ∈ (λ(h, j). (j + 1, h - 1)) ` {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h ≠ j + 1}" by (auto simp: image_iff) qed qed show "inj_on (λ(h, j). (j + 1, h - 1)) {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h ≠ j + 1}" proof fix x y::"nat×nat" assume "x ∈ {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h ≠ j + 1}" "y ∈ {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h ≠ j + 1}" thus "(case x of (h, j) ⇒ (j + 1, h - 1)) = (case y of (h, j) ⇒ (j + 1, h - 1)) ⟹ x = y" by auto qed show "⋀x. x ∈ {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h ≠ j + 1} ⟹ (case case x of (h, j) ⇒ (j + 1, h - 1) of (h, j) ⇒ coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)) = (case x of (h, j) ⇒ coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j))" by fastforce qed have 2: "(∑h = 1..i + 1. coeff f h * coeff g (i + 2 - h) * coeff f (h - 1) * coeff g (i + 1 - h)) = (∑(h, j)∈{(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h = j + 1}. coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j))" proof (rule sum.reindex_cong) show "{1..i + 1} = fst ` {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h = j + 1}" proof show "{1..i + 1} ⊆ fst ` {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h = j + 1}" proof fix x assume "x ∈ {1..i + 1}" hence "x ≤ i + 2 ∧ x - 1 < x ∧ x - 1 ≤ i ∧ x = x - 1 + 1 ∧ x = fst (x, x-1)" by auto thus "x ∈ fst ` {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h = j + 1}" by blast qed show "fst ` {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h = j + 1} ⊆ {1..i + 1}" by force qed show "inj_on fst {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h = j + 1}" proof fix x y assume "x ∈ {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h = j + 1}" "y ∈ {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h = j + 1}" hence "x = (fst x, fst x - 1)" "y = (fst y, fst y - 1)" "fst x > 0" "fst y > 0" by auto thus "fst x = fst y ⟹ x = y" by presburger qed show "⋀x. x ∈ {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h = j + 1} ⟹ coeff f (fst x) * coeff g (i + 2 - fst x) * coeff f (fst x - 1) * coeff g (i + 1 - fst x) = (case x of (h, j) ⇒ coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j))" by fastforce qed have H: "{(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h ≠ j + 1} ⊆ {0..i+2}×{0..i}" "{(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h = j + 1} ⊆ {0..i+2}×{0..i}" "finite ({0..i+2}×{0..i})" by (fastforce, fastforce, fastforce) have "finite {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h ≠ j + 1}" "finite {(h, j). h ≤ i + 2 ∧ j < h ∧ j ≤ i ∧ h = j + 1}" apply (rule finite_subset) using H apply (simp, simp) apply (rule finite_subset) using H apply (simp, simp) done thus ?thesis apply (subst 1, subst 2, subst sum.union_disjoint[symmetric]) apply auto[3] apply (rule sum.cong) by auto qed ultimately show ?thesis by algebra qed text ‹$\dots = \sum_{h \leq j} f_hf_j\left(g_{i+1-h}g_{i+1-j} - g_{i+2-h}g_{i-j}\right) + \sum_{h \leq j} f_{j+1}f_{h-1}\left(g_{i-j}g_{i+2-h} - g_{i+1-j}f_jg_{i+1-h}\right)$ Note we have to also consider the edge cases caused by making these sums finite.› also have "... = (∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) + (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j) - coeff g (i + 2 - h) * coeff g (i - j))) + (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}. coeff f (j+1) * coeff f (h-1) * (coeff g (i - j) * coeff g (i + 2 - h) - coeff g (i + 1 - j) * coeff g (i + 1 - h))) - ((∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j ∧ 0 < h}. coeff f (j+1) * coeff g (i + 1 - j) * coeff f (h-1) * coeff g (i + 1 - h)))" (is "?L = ?R") proof - have "?R = (∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) + ((∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j}. coeff f h * coeff f j * coeff g (i + 1 - h) * coeff g (i + 1 - j)) - (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j}. coeff f h * coeff f j * coeff g (i + 2 - h) * coeff g (i - j))) + ((∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}. coeff f (j+1) * coeff f (h-1) * coeff g (i - j) * coeff g (i + 2 - h)) - (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}. coeff f (j+1) * coeff f (h-1) * coeff g (i + 1 - j) * coeff g (i + 1 - h))) - ((∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j ∧ 0 < h}. coeff f (j+1) * coeff g (i + 1 - j) * coeff f (h-1) * coeff g (i + 1 - h)))" apply (subst sum_subtractf[symmetric], subst sum_subtractf[symmetric]) by (auto simp: algebra_simps split_beta) also have "... = ((∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) + (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j)))) - (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j}. coeff f h * coeff f j * coeff g (i + 2 - h) * coeff g (i - j)) + (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}. coeff f (j + 1) * coeff f (h - 1) * coeff g (i - j) * coeff g (i + 2 - h)) - ((∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}. coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)) + (∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j ∧ 0 < h}. coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)))" by (auto simp: algebra_simps) also have "... = ?L" proof - have "(∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) + (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) = (∑(h, j)∈{(h, j). j ≤ i + 1 ∧ h ≤ j}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j)))" proof (subst sum.union_disjoint[symmetric]) have "{(h, j). j = i + 1 ∧ h ≤ j} ⊆ {..i + 1} × {..i + 1}" "{(h, j). j ≤ i ∧ h ≤ j} ⊆ {..i + 1} × {..i + 1}" by (fastforce, fastforce) thus "finite {(h, j). j = i + 1 ∧ h ≤ j}" "finite {(h, j). j ≤ i ∧ h ≤ j}" by (auto simp: finite_subset) show "{(h, j). j = i + 1 ∧ h ≤ j} ∩ {(h, j). j ≤ i ∧ h ≤ j} = {}" by fastforce qed (rule sum.cong, auto) moreover have "(∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}. coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)) + (∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j ∧ 0 < h}. coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)) = (∑(h, j)∈{(h, j). j ≤ i + 1 ∧ h ≤ j ∧ 0 < h}. coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h))" proof (subst sum.union_disjoint[symmetric]) have "{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h} ⊆ {..i + 1} × {..i + 1}" "{(h, j). j = i + 1 ∧ h ≤ j ∧ 0 < h} ⊆ {..i + 1} × {..i + 1}" by (fastforce, fastforce) thus "finite {(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}" "finite {(h, j). j = i + 1 ∧ h ≤ j ∧ 0 < h}" by (auto simp: finite_subset) show "{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h} ∩ {(h, j). j = i + 1 ∧ h ≤ j ∧ 0 < h} = {}" by fastforce qed (rule sum.cong, auto) ultimately show ?thesis by (auto simp: algebra_simps) qed finally show ?thesis by presburger qed text ‹$\dots = \sum_{h \leq j} \left(f_hf_j - f_{j+1}f_{h-1}\right) \left(g_{i+1-h}g_{i+1-j} - g_{i+2-h}g_{i-j}\right)$› also have "... = (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}. -(coeff f h * coeff f j - coeff f (j+1) * coeff f (h-1)) * (coeff g (i - j) * coeff g (i + 2 - h) - coeff g (i + 1 - j) * coeff g (i + 1 - h))) + (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ h = 0}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j) - coeff g (i + 2 - h) * coeff g (i - j))) + (∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) - ((∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j ∧ 0 < h}. coeff f (j+1) * coeff g (i + 1 - j) * coeff f (h-1) * coeff g (i + 1 - h)))" (is "?L = ?R") proof - have "(∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j) - coeff g (i + 2 - h) * coeff g (i - j))) = (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j) - coeff g (i + 2 - h) * coeff g (i - j))) + (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 = h}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j) - coeff g (i + 2 - h) * coeff g (i - j)))" proof (subst sum.union_disjoint[symmetric]) have "{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h} ⊆ {..i}×{..i}" "{(h, j). j ≤ i ∧ h ≤ j ∧ 0 = h} ⊆ {..i}×{..i}" by (force, force) thus "finite {(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}" "finite {(h, j). j ≤ i ∧ h ≤ j ∧ 0 = h}" by (auto simp: finite_subset) show "{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h} ∩ {(h, j). j ≤ i ∧ h ≤ j ∧ 0 = h} = {}" by fast qed (rule sum.cong, auto) moreover have "(∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}. (-coeff f h * coeff f j + coeff f (j + 1) * coeff f (h - 1)) * (coeff g (i - j) * coeff g (i + 2 - h) - coeff g (i + 1 - j) * coeff g (i + 1 - h))) = (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j) - coeff g (i + 2 - h) * coeff g (i - j))) + (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}. coeff f (j + 1) * coeff f (h - 1) * (coeff g (i - j) * coeff g (i + 2 - h) - coeff g (i + 1 - j) * coeff g (i + 1 - h)))" by (subst sum.distrib[symmetric], rule sum.cong, fast, auto simp: algebra_simps) ultimately show ?thesis by (auto simp: algebra_simps) qed text ‹$\dots \geq 0$ by ‹normal_poly_general_coeff_mult›› also have "... ≥ 0" proof - have "0 ≤ (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}. - (coeff f h * coeff f j - coeff f (j + 1) * coeff f (h - 1)) * (coeff g (i - j) * coeff g (i + 2 - h) - coeff g (i + 1 - j) * coeff g (i + 1 - h)))" proof (rule sum_nonneg) fix x assume "x ∈ {(h, j). j ≤ i ∧ h ≤ j ∧ 0 < h}" then obtain h j where H: "x = (h, j)" "j ≤ i" "h ≤ j" "0 < h" by fast hence "h - 1 ≤ j - 1" by force hence 1: "coeff f h * coeff f j - coeff f (j + 1) * coeff f (h - 1) ≥ 0" using normal_poly_general_coeff_mult[OF hf, of "h-1" "j-1"] H by (auto simp: algebra_simps) from H have "i - j ≤ i - h" by force hence 2: "coeff g (i - j) * coeff g (i + 2 - h) - coeff g (i + 1 - j) * coeff g (i + 1 - h) ≤ 0" using normal_poly_general_coeff_mult[OF hg, of "i - j" "i - h"] H by (smt (verit, del_insts) Nat.add_diff_assoc2 le_trans) show "0 ≤ (case x of (h, j) ⇒ - (coeff f h * coeff f j - coeff f (j + 1) * coeff f (h - 1)) * (coeff g (i - j) * coeff g (i + 2 - h) - coeff g (i + 1 - j) * coeff g (i + 1 - h)))" apply (subst H(1), subst split, rule mult_nonpos_nonpos, subst neg_le_0_iff_le) subgoal using 1 by blast subgoal using 2 by blast done qed moreover have "0 ≤ (∑(h, j)∈{(h, j). j ≤ i ∧ h ≤ j ∧ h = 0}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j) - coeff g (i + 2 - h) * coeff g (i - j)))" proof (rule sum_nonneg) fix x assume "x ∈ {(h, j). j ≤ i ∧ h ≤ j ∧ h = 0}" then obtain h j where H: "x = (h, j)" "j ≤ i" "h ≤ j" "h = 0" by fast have 1: "coeff f h * coeff f j ≥ 0" by (simp add: hf normal_coeff_nonneg) from H have "i - j ≤ i - h" by force hence 2: "coeff g (i - j) * coeff g (i + 2 - h) - coeff g (i + 1 - j) * coeff g (i + 1 - h) ≤ 0" using normal_poly_general_coeff_mult[OF hg, of "i - j" "i - h"] H by (smt (verit, del_insts) Nat.add_diff_assoc2 le_trans) show "0 ≤ (case x of (h, j) ⇒ coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j) - coeff g (i + 2 - h) * coeff g (i - j)))" apply (subst H(1), subst split, rule mult_nonneg_nonneg) subgoal using 1 by blast subgoal using 2 by argo done qed moreover have "0 ≤ (∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) - (∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j ∧ 0 < h}. coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h))" proof - have "(∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) - (∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j ∧ 0 < h}. coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)) = (∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j ∧ h = 0}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) + (∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j ∧ 0 < h}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) - (∑(h, j)∈{(h, j). j = i + 1 ∧ h ≤ j ∧ 0 < h}. coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h))" proof (subst sum.union_disjoint[symmetric]) have "{(h, j). j = i + 1 ∧ h ≤ j ∧ h = 0} = {(0, i + 1)}" "{(h, j). j = i + 1 ∧ h ≤ j