# Theory Sturm_Tarski.Sturm_Tarski

```(*  Title: Sturm-Tarski Theorem
Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
*)

section "Sturm--Tarski Theorem"

theory Sturm_Tarski
imports Complex_Main PolyMisc "HOL-Computational_Algebra.Field_as_Ring"
begin

subsection‹Misc›

lemma eventually_at_right:
fixes x::"'a::{archimedean_field,linorder_topology}"
shows "eventually P (at_right x) ⟷ (∃b>x. ∀y>x. y < b ⟶ P y)"
proof -
obtain y where "y>x" using ex_less_of_int by auto
thus ?thesis using eventually_at_right[OF ‹y>x›] by auto
qed

lemma eventually_at_left:
fixes x::"'a::{archimedean_field,linorder_topology}"
shows "eventually P (at_left x) ⟷ (∃b<x. ∀y>b. y < x ⟶ P y)"
proof -
obtain y where "y<x"
using linordered_field_no_lb by auto
thus ?thesis using eventually_at_left[OF ‹y<x›] by auto
qed

lemma eventually_neg:
assumes "F≠bot"  and eve:"eventually (λx. P x) F"
shows "¬ eventually (λx. ¬ P x) F"
proof (rule ccontr)
assume "¬ ¬ eventually (λx. ¬ P x) F"
hence "eventually (λx. ¬ P x) F" by auto
hence "eventually (λx. False) F" using eventually_conj[OF eve,of "(λx. ¬ P x)"] by auto
thus False using ‹F≠bot› eventually_False by auto
qed

lemma poly_tendsto[simp]:
"(poly p ⤏ poly p x) (at (x::real))"
"(poly p ⤏ poly p x) (at_left (x::real))"
"(poly p ⤏ poly p x) (at_right (x::real))"
using isCont_def[where f="poly p"] by (auto simp add:filterlim_at_split)

lemma not_eq_pos_or_neg_iff_1:
fixes p::"real poly"
shows "(∀z. lb<z∧z≤ub⟶poly p z≠0) ⟷
(∀z. lb<z∧z≤ub⟶poly p z>0)∨(∀z. lb<z∧z≤ub⟶poly p z<0)" (is "?Q ⟷ ?P")
proof (rule,rule ccontr)
assume "?Q" "¬?P"
then obtain z1 z2 where z1:"lb<z1" "z1≤ub" "poly p z1≤0"
and z2:"lb<z2" "z2≤ub" "poly p z2≥0"
by auto
hence "∃z. lb<z∧z≤ub∧poly p z=0"
proof (cases "poly p z1 = 0 ∨ poly p z2 =0 ∨ z1=z2")
case True
thus ?thesis using z1 z2 by auto
next
case False
hence "poly p z1<0" and "poly p z2>0" and "z1≠z2" using z1(3) z2(3) by auto
hence "(∃z>z1. z < z2 ∧ poly p z = 0) ∨ (∃z>z2. z < z1 ∧ poly p z = 0)"
using poly_IVT_neg poly_IVT_pos by (subst (asm) linorder_class.neq_iff,auto)
thus ?thesis using z1(1,2) z2(1,2) by (metis less_eq_real_def order.strict_trans2)
qed
thus False using ‹?Q› by auto
next
assume "?P"
thus ?Q by auto
qed

lemma not_eq_pos_or_neg_iff_2:
fixes p::"real poly"
shows "(∀z. lb≤z∧z<ub⟶poly p z≠0)
⟷(∀z. lb≤z∧z<ub⟶poly p z>0)∨(∀z. lb≤z∧z<ub⟶poly p z<0)" (is "?Q⟷?P")
proof (rule,rule ccontr)
assume "?Q" "¬?P"
then obtain z1 z2 where z1:"lb≤z1" "z1<ub" "poly p z1≤0"
and z2:"lb≤z2" "z2<ub" "poly p z2≥0"
by auto
hence "∃z. lb≤z∧z<ub∧poly p z=0"
proof (cases "poly p z1 = 0 ∨ poly p z2 =0 ∨ z1=z2")
case True
thus ?thesis using z1 z2 by auto
next
case False
hence "poly p z1<0" and "poly p z2>0" and "z1≠z2" using z1(3) z2(3) by auto
hence "(∃z>z1. z < z2 ∧ poly p z = 0) ∨ (∃z>z2. z < z1 ∧ poly p z = 0)"
using poly_IVT_neg poly_IVT_pos by (subst (asm) linorder_class.neq_iff,auto)
thus ?thesis using z1(1,2) z2(1,2) by (meson dual_order.strict_trans not_le)
qed
thus False using ‹?Q› by auto
next
assume "?P"
thus ?Q by auto
qed

lemma next_non_root_interval:
fixes p::"real poly"
assumes "p≠0"
obtains ub where "ub>lb" and "(∀z. lb<z∧z≤ub⟶poly p z≠0)"
proof (cases "(∃ r. poly p r=0 ∧ r>lb)")
case False
thus ?thesis by (intro that[of "lb+1"],auto)
next
case True
define lr where "lr≡Min {r . poly p r=0 ∧ r>lb}"
have "∀z. lb<z∧z<lr⟶poly p z≠0" and "lr>lb"
using True lr_def poly_roots_finite[OF ‹p≠0›] by auto
thus ?thesis using that[of "(lb+lr)/2"] by auto
qed

lemma last_non_root_interval:
fixes p::"real poly"
assumes "p≠0"
obtains lb where "lb<ub" and "(∀z. lb≤z∧z<ub⟶poly p z≠0)"
proof (cases "(∃ r. poly p r=0 ∧ r<ub)")
case False
thus ?thesis by (intro that[of "ub - 1"]) auto
next
case True
define mr where  "mr≡Max {r . poly p r=0 ∧ r<ub}"
have "∀z. mr<z∧z<ub⟶poly p z≠0" and "mr<ub"
using True mr_def poly_roots_finite[OF ‹p≠0›] by auto
thus ?thesis using that[of "(mr+ub)/2"] ‹mr<ub› by auto
qed

subsection‹Sign›

definition sign:: "'a::{zero,linorder} ⇒ int" where
"sign x≡(if x>0 then 1 else if x=0 then 0 else -1)"

lemma sign_simps[simp]:
"x>0 ⟹ sign x=1"
"x=0 ⟹ sign x=0"
"x<0 ⟹ sign x=-1"
unfolding sign_def by auto

lemma sign_cases [case_names neg zero pos]:
"(sign x = -1 ⟹ P) ⟹ (sign x = 0 ⟹ P) ⟹ (sign x =1 ⟹ P) ⟹ P"
unfolding Sturm_Tarski.sign_def by argo

lemma sign_times:
fixes x::"'a::linordered_ring_strict"
shows "sign (x*y) = sign x * sign y"
unfolding Sturm_Tarski.sign_def

lemma sign_power:
fixes x::"'a::linordered_idom"
shows "sign (x^n) = (if n=0 then 1 else if even n then ¦sign x¦ else sign x)"

(*
lemma sgn_sign_eq:
fixes x::"'a::{linordered_idom}"
shows "sgn x = of_int (sign x)"
unfolding sgn_if by auto
*)

lemma sgn_sign_eq:"sgn = sign"
unfolding sign_def sgn_if by auto

lemma sign_sgn[simp]: "sign (sgn x) = sign (x::'b::linordered_idom)"

lemma sign_uminus[simp]:"sign (- x) = - sign (x::'b::linordered_idom)"

subsection‹Bound of polynomials›

definition sgn_pos_inf :: "('a ::linordered_idom) poly ⇒ 'a" where
"sgn_pos_inf p ≡ sgn (lead_coeff p)"
definition sgn_neg_inf :: "('a ::linordered_idom) poly ⇒ 'a" where
"sgn_neg_inf p ≡ if even (degree p) then sgn (lead_coeff p) else -sgn (lead_coeff p)"

lemma sgn_inf_sym:
fixes p::"real poly"
shows "sgn_pos_inf (pcompose p [:0,-1:]) = sgn_neg_inf p" (is "?L=?R")
proof -
have "?L= sgn (lead_coeff p * (- 1) ^ degree p)"
thus ?thesis unfolding sgn_neg_inf_def
by (metis mult.right_neutral mult_minus1_right neg_one_even_power neg_one_odd_power sgn_minus)
qed

lemma poly_pinfty_gt_lc:
fixes p:: "real poly"
shows "∃ n. ∀ x ≥ n. poly p x ≥ lead_coeff p" using assms
proof (induct p)
case 0
thus ?case by auto
next
case (pCons a p)
have "⟦a≠0;p=0⟧ ⟹ ?case" by auto
moreover have "p≠0 ⟹ ?case"
proof -
assume "p≠0"
then obtain n1 where gte_lcoeff:"∀x≥n1. lead_coeff p ≤ poly p x" using that pCons by auto
have gt_0:"lead_coeff p >0" using pCons(3) ‹p≠0› by auto
define n where "n≡max n1 (1+ ¦a¦/(lead_coeff p))"
show ?thesis
proof (rule_tac x=n in exI,rule,rule)
fix x assume "n ≤ x"
hence "lead_coeff p ≤ poly p x"
using gte_lcoeff unfolding n_def by auto
hence " ¦a¦/(lead_coeff p) ≥ ¦a¦/(poly p x)" and "poly p x>0" using gt_0
by (intro frac_le,auto)
hence "x≥1+ ¦a¦/(poly p x)" using ‹n≤x›[unfolded n_def] by auto
thus "lead_coeff (pCons a p) ≤ poly (pCons a p) x"
using ‹lead_coeff p ≤ poly p x› ‹poly p x>0› ‹p≠0›
qed
qed
ultimately show ?case by fastforce
qed

lemma poly_sgn_eventually_at_top:
fixes p::"real poly"
shows "eventually (λx. sgn (poly p x) = sgn_pos_inf p) at_top"
proof (cases "p=0")
case True
thus ?thesis unfolding sgn_pos_inf_def by auto
next
case False
obtain ub where ub:"∀x≥ub. sgn (poly p x) = sgn_pos_inf p"
case True
thus ?thesis
using that poly_pinfty_gt_lc[of p] unfolding sgn_pos_inf_def by fastforce
next
case False
then obtain n where "∀x≥n. lead_coeff p ≥ poly p x"
using poly_pinfty_gt_lc[of "-p"] unfolding lead_coeff_minus by auto
thus ?thesis using ‹lead_coeff p<0› that[of n] unfolding sgn_pos_inf_def by fastforce
qed
thus ?thesis unfolding eventually_at_top_linorder by auto
qed

lemma poly_sgn_eventually_at_bot:
fixes p::"real poly"
shows "eventually (λx. sgn (poly p x) = sgn_neg_inf p) at_bot"
using
poly_sgn_eventually_at_top[of "pcompose p [:0,-1:]",unfolded poly_pcompose sgn_inf_sym,simplified]
eventually_filtermap[of _ uminus "at_bot::real filter",folded at_top_mirror]
by auto

lemma root_ub:
fixes p:: "real poly"
assumes "p≠0"
obtains ub where "∀x. poly p x=0 ⟶ x<ub"
and "∀x≥ub. sgn (poly p x) = sgn_pos_inf p"
proof -
obtain ub1 where ub1:"∀x. poly p x=0 ⟶ x<ub1"
proof (cases "∃ r. poly p r=0")
case False
thus ?thesis using that by auto
next
case True
define max_r where "max_r≡Max {x . poly p x=0}"
hence "∀x. poly p x=0 ⟶ x≤max_r"
using  poly_roots_finite[OF ‹p≠0›] True by auto
thus ?thesis using that[of "max_r+1"]
qed
obtain ub2 where ub2:"∀x≥ub2. sgn (poly p x) = sgn_pos_inf p"
using poly_sgn_eventually_at_top[unfolded eventually_at_top_linorder] by auto
define ub where "ub≡max ub1 ub2"
have "∀x. poly p x=0 ⟶ x<ub" using ub1 ub_def
by (metis eq_iff less_eq_real_def less_linear max.bounded_iff)
thus ?thesis using that[of ub] ub2 ub_def by auto
qed

lemma root_lb:
fixes p:: "real poly"
assumes "p≠0"
obtains lb where "∀x. poly p x=0 ⟶ x>lb"
and "∀x≤lb. sgn (poly p x) = sgn_neg_inf p"
proof -
obtain lb1 where lb1:"∀x. poly p x=0 ⟶ x>lb1"
proof (cases "∃ r. poly p r=0")
case False
thus ?thesis using that by auto
next
case True
define min_r where "min_r≡Min {x . poly p x=0}"
hence "∀x. poly p x=0 ⟶ x≥min_r"
using  poly_roots_finite[OF ‹p≠0›] True by auto
thus ?thesis using that[of "min_r - 1"] by (metis lt_ex order.strict_trans2 that)
qed
obtain lb2 where lb2:"∀x≤lb2. sgn (poly p x) = sgn_neg_inf p"
using poly_sgn_eventually_at_bot[unfolded eventually_at_bot_linorder] by auto
define lb where  "lb≡min lb1 lb2"
have "∀x. poly p x=0 ⟶ x>lb" using lb1 lb_def
by (metis (poly_guards_query) less_not_sym min_less_iff_conj neq_iff)
thus ?thesis using that[of lb] lb2 lb_def by auto
qed

subsection ‹Variation and cross›

definition variation :: "real ⇒  real ⇒ int" where
"variation x y=(if x*y≥0 then 0 else if x<y then 1 else -1)"

definition cross :: "real poly ⇒ real ⇒ real ⇒ int" where
"cross p a b=variation (poly p a) (poly p b)"

lemma variation_0[simp]: "variation 0 y=0" "variation x 0=0"
unfolding variation_def by auto

lemma variation_comm: "variation x y= - variation y x" unfolding variation_def

lemma cross_0[simp]: "cross 0 a b=0" unfolding cross_def by auto

lemma variation_cases:
"⟦x>0;y>0⟧⟹variation x y = 0"
"⟦x>0;y<0⟧⟹variation x y = -1"
"⟦x<0;y>0⟧⟹variation x y = 1"
"⟦x<0;y<0⟧⟹variation x y = 0"
proof -
show "⟦x>0;y>0⟧⟹variation x y = 0"  unfolding variation_def by auto
show "⟦x>0;y<0⟧⟹variation x y = -1" unfolding variation_def
using mult_pos_neg by fastforce
show "⟦x<0;y>0⟧⟹variation x y = 1" unfolding variation_def
using mult_neg_pos by fastforce
show "⟦x<0;y<0⟧⟹variation x y = 0" unfolding variation_def
using mult_neg_neg by fastforce
qed

lemma variation_congr:
assumes "sgn x=sgn x'" "sgn y=sgn y'"
shows "variation x y=variation x' y'" using assms
proof -
have " 0 ≤ x * y =  (0≤ x' * y')" using assms by (metis Real_Vector_Spaces.sgn_mult zero_le_sgn_iff)
moreover hence "¬ 0≤x * y ⟹ x < y = (x' < y')" using assms
by (metis less_eq_real_def mult_nonneg_nonneg mult_nonpos_nonpos not_le order.strict_trans2
zero_le_sgn_iff)
ultimately show ?thesis unfolding variation_def by auto
qed

lemma variation_mult_pos:
assumes "c>0"
shows "variation (c*x) y =variation x y" and "variation x (c*y) =variation x y"
proof -
have "sgn (c*x) = sgn x" using ‹c>0›
thus "variation (c*x) y =variation x y" using variation_congr by blast
next
have "sgn (c*y) = sgn y" using ‹c>0›
thus "variation x (c*y) =variation x y" using variation_congr by blast
qed

lemma variation_mult_neg_1:
assumes "c<0"
shows "variation (c*x) y =variation x y + (if y=0 then 0 else sign x)"
apply (cases x  rule:linorder_cases[of 0] )
apply (cases y  rule:linorder_cases[of 0], auto simp add:
variation_cases mult_neg_pos[OF ‹c<0›,of x]  mult_neg_neg[OF ‹c<0›,of x])+
done

lemma variation_mult_neg_2:
assumes "c<0"
shows "variation x (c*y) = variation x y + (if x=0 then 0 else - sign y)"
unfolding variation_comm[of x "c*y", unfolded variation_mult_neg_1[OF ‹c<0›, of y x] ]
by (auto,subst variation_comm,simp)

lemma cross_no_root:
assumes "a<b" and no_root:"∀x. a<x∧x<b ⟶ poly p x≠0"
shows "cross p a b=0"
proof -
have "⟦poly p a>0;poly p b<0⟧ ⟹ False" using poly_IVT_neg[OF ‹a<b›] no_root by auto
moreover have "⟦poly p a<0;poly p b>0⟧ ⟹ False" using poly_IVT_pos[OF ‹a<b›] no_root by auto
ultimately have "0 ≤ poly p a * poly p b"
by (metis less_eq_real_def linorder_neqE_linordered_idom mult_less_0_iff)
thus ?thesis unfolding cross_def variation_def by simp
qed

subsection ‹Tarski query›

definition taq :: "'a::linordered_idom set ⇒ 'a poly ⇒ int" where
"taq s q ≡ ∑x∈s. sign (poly q x)"

subsection ‹Sign at the right›

definition sign_r_pos :: "real poly ⇒ real ⇒ bool "
where
"sign_r_pos p x≡ (eventually (λx. poly p x>0) (at_right x))"

lemma sign_r_pos_rec:
fixes p:: "real poly"
assumes "p≠0"
shows "sign_r_pos p x= (if poly p x=0 then sign_r_pos (pderiv p) x else poly p x>0 )"
proof (cases "poly p x=0")
case True
have "sign_r_pos (pderiv p) x ⟹ sign_r_pos p x"
proof (rule ccontr)
assume "sign_r_pos (pderiv p) x" "¬ sign_r_pos p x"
obtain b where "b>x" and b:"∀z. x < z ∧ z < b ⟶ 0 < poly (pderiv p) z"
using ‹sign_r_pos (pderiv p) x› unfolding sign_r_pos_def eventually_at_right  by auto
have "∀b>x. ∃z>x. z < b ∧ ¬ 0 < poly p z" using ‹¬ sign_r_pos p x›
unfolding sign_r_pos_def eventually_at_right by auto
then obtain z where "z>x" and "z<b" and "poly p z≤0"
using ‹b>x› b by auto
hence "∃z'>x. z' < z ∧ poly p z = (z - x) * poly (pderiv p) z'"
using poly_MVT[OF ‹z>x›] True by (metis diff_0_right)
hence "∃z'>x. z' < z ∧ poly (pderiv p) z' ≤0"
using ‹poly p z≤0›‹z>x› by (metis leD le_iff_diff_le_0 mult_le_0_iff)
thus False using b by (metis ‹z < b› dual_order.strict_trans not_le)
qed
moreover have "sign_r_pos p x ⟹ sign_r_pos (pderiv p) x"
proof -
assume "sign_r_pos p x"
have "pderiv p≠0" using ‹poly p x=0› ‹p≠0›
pderiv_iszero poly_0 poly_pCons)
obtain ub where "ub>x" and ub: "(∀z. x<z∧z<ub⟶poly (pderiv p) z>0)
∨ (∀z. x<z∧z<ub⟶poly (pderiv p) z<0)"
using next_non_root_interval[OF ‹pderiv p≠0›, of x,unfolded not_eq_pos_or_neg_iff_1]
by (metis order.strict_implies_order)
have "∀z. x<z∧z<ub⟶poly (pderiv p) z<0 ⟹ False"
proof -
assume assm:"∀z. x<z∧z<ub⟶poly (pderiv p) z<0"
obtain ub' where "ub'>x" and ub':"∀z. x < z ∧ z < ub' ⟶ 0 < poly p z"
using ‹sign_r_pos p x› unfolding sign_r_pos_def eventually_at_right by auto
obtain z' where "x<z'" and "z' < (x+(min ub' ub))/2"
and z':"poly p ((x+min ub' ub)/2) = ((x+min ub' ub)/2 - x) * poly (pderiv p) z'"
using poly_MVT[of x "(x+min ub' ub)/2" p] ‹ub'>x› ‹ub>x› True by auto
moreover have "0 < poly p ((x+min ub' ub)/2)"
using ub'[THEN HOL.spec,of "(x+(min ub' ub))/2"] ‹z' < (x+min ub' ub)/2› ‹x<z'›
by auto
moreover have "(x+min ub' ub)/2 - x>0" using ‹ub'>x› ‹ub>x› by auto
ultimately have "poly (pderiv p) z'>0" by (metis zero_less_mult_pos)
thus False using assm[THEN spec,of z'] ‹x<z'› ‹z' < (x+(min ub' ub))/2› by auto
qed
hence "∀z. x<z∧z<ub⟶poly (pderiv p) z>0" using ub by auto
thus "sign_r_pos (pderiv p) x" unfolding sign_r_pos_def eventually_at_right
using ‹ub>x› by auto
qed
ultimately show ?thesis using True by auto
next
case False
have "sign_r_pos p x ⟹ poly p x>0"
proof (rule ccontr)
assume "sign_r_pos p x" "¬ 0 < poly p x"
then obtain  ub where "ub>x" and ub: "∀z. x < z ∧ z < ub ⟶ 0 < poly p z"
unfolding sign_r_pos_def eventually_at_right by auto
hence "poly p ((ub+x)/2) > 0" by auto
moreover have "poly p x<0" using ‹¬ 0 < poly p x› False by auto
ultimately have "∃z>x. z < (ub + x) / 2 ∧ poly p z = 0"
using poly_IVT_pos[of x "((ub + x) / 2)" p] ‹ub>x› by auto
thus False using ub by auto
qed
moreover have "poly p x>0 ⟹ sign_r_pos p x"
unfolding sign_r_pos_def
using order_tendstoD(1)[OF poly_tendsto(1),of 0 p x] eventually_at_split by auto
ultimately show ?thesis using False by auto
qed

lemma sign_r_pos_0[simp]:"¬ sign_r_pos 0 (x::real)"
using eventually_False[of "at_right x"] unfolding sign_r_pos_def by auto

lemma sign_r_pos_minus:
fixes p:: "real poly"
assumes "p≠0"
shows "sign_r_pos p x = (¬ sign_r_pos (-p) x)"
proof -
have "sign_r_pos p x ∨ sign_r_pos (-p) x"
unfolding sign_r_pos_def eventually_at_right
using next_non_root_interval[OF ‹p≠0›,unfolded not_eq_pos_or_neg_iff_1]
by (metis (erased, opaque_lifting) le_less minus_zero neg_less_iff_less poly_minus)
moreover have "sign_r_pos p x ⟹ ¬ sign_r_pos (-p) x" unfolding sign_r_pos_def
using eventually_neg[OF trivial_limit_at_right_real, of "λx. poly p x > 0" x] poly_minus
by (metis (lifting) eventually_mono less_asym neg_less_0_iff_less)
ultimately show ?thesis by auto
qed

lemma sign_r_pos_smult:
fixes p :: "real poly"
assumes "c≠0" "p≠0"
shows "sign_r_pos (smult c p) x= (if c>0 then sign_r_pos p x else ¬ sign_r_pos p x)"
(is "?L=?R")
proof (cases "c>0")
assume "c>0"
hence "∀x. (0 < poly (smult c p) x) = (0 < poly p x)"
by (subst poly_smult,metis mult_pos_pos zero_less_mult_pos)
thus ?thesis unfolding sign_r_pos_def using ‹c>0› by auto
next
assume "¬(c>0)"
hence "∀x. (0 < poly (smult c p) x) = (0 < poly (-p) x)"
by (subst poly_smult, metis assms(1) linorder_neqE_linordered_idom mult_neg_neg mult_zero_right
neg_0_less_iff_less poly_minus zero_less_mult_pos2)
hence "sign_r_pos (smult c p) x=sign_r_pos (-p) x"
unfolding sign_r_pos_def using ‹¬ c>0› by auto
thus ?thesis using sign_r_pos_minus[OF ‹p≠0›, of x] ‹¬ c>0› by auto
qed

lemma sign_r_pos_mult:
fixes p q :: "real poly"
assumes "p≠0" "q≠0"
shows "sign_r_pos (p*q) x= (sign_r_pos p x ⟷ sign_r_pos q x)"
proof -
obtain ub where "ub>x"
and ub:"(∀z. x < z ∧ z < ub ⟶ 0 < poly p z) ∨ (∀z. x < z ∧ z < ub ⟶ poly p z < 0)"
using next_non_root_interval[OF ‹p≠0›,of x,unfolded not_eq_pos_or_neg_iff_1]
by (metis order.strict_implies_order)
obtain ub' where "ub'>x"
and ub':"(∀z. x < z ∧ z < ub' ⟶ 0 < poly q z) ∨ (∀z. x < z ∧ z < ub' ⟶ poly q z < 0)"
using next_non_root_interval[OF ‹q≠0›,unfolded not_eq_pos_or_neg_iff_1]
by (metis order.strict_implies_order)
have "(∀z. x < z ∧ z < ub ⟶ 0 < poly p z) ⟹ (∀z. x < z ∧ z < ub' ⟶ 0 < poly q z) ⟹ ?thesis"
proof -
assume "(∀z. x < z ∧ z < ub ⟶ 0 < poly p z)" "(∀z. x < z ∧ z < ub' ⟶ 0 < poly q z)"
hence "sign_r_pos p x" and "sign_r_pos q x" unfolding sign_r_pos_def eventually_at_right
using ‹ub>x› ‹ub'>x› by auto
moreover hence "eventually (λz. poly p z>0 ∧ poly q z>0) (at_right x)"
unfolding sign_r_pos_def using eventually_conj_iff[of _ _ "at_right x"] by auto
hence "sign_r_pos (p*q) x"
unfolding sign_r_pos_def poly_mult
by (metis (lifting, mono_tags) eventually_mono mult_pos_pos)
ultimately show ?thesis by auto
qed
moreover have "(∀z. x < z ∧ z < ub ⟶ 0 > poly p z) ⟹ (∀z. x < z ∧ z < ub' ⟶ 0 < poly q z)
⟹ ?thesis"
proof -
assume "(∀z. x < z ∧ z < ub ⟶ 0 > poly p z)" "(∀z. x < z ∧ z < ub' ⟶ 0 < poly q z)"
hence "sign_r_pos (-p) x" and "sign_r_pos q x" unfolding sign_r_pos_def eventually_at_right
using ‹ub>x› ‹ub'>x› by auto
moreover hence "eventually (λz. poly (-p) z>0 ∧ poly q z>0) (at_right x)"
unfolding sign_r_pos_def using eventually_conj_iff[of _ _ "at_right x"] by auto
hence "sign_r_pos (- p*q) x"
unfolding sign_r_pos_def poly_mult
by (metis (lifting, mono_tags) eventually_mono mult_pos_pos)
ultimately show ?thesis
using sign_r_pos_minus ‹p≠0› ‹q≠0› by (metis minus_mult_left no_zero_divisors)
qed
moreover have "(∀z. x < z ∧ z < ub ⟶ 0 < poly p z) ⟹ (∀z. x < z ∧ z < ub' ⟶ 0 > poly q z)
⟹ ?thesis"
proof -
assume "(∀z. x < z ∧ z < ub ⟶ 0 < poly p z)" "(∀z. x < z ∧ z < ub' ⟶ 0 > poly q z)"
hence "sign_r_pos p x" and "sign_r_pos (-q) x" unfolding sign_r_pos_def eventually_at_right
using ‹ub>x› ‹ub'>x› by auto
moreover hence "eventually (λz. poly p z>0 ∧ poly (-q) z>0) (at_right x)"
unfolding sign_r_pos_def using eventually_conj_iff[of _ _ "at_right x"] by auto
hence "sign_r_pos ( p * (- q)) x"
unfolding sign_r_pos_def poly_mult
by (metis (lifting, mono_tags) eventually_mono mult_pos_pos)
ultimately show ?thesis
using sign_r_pos_minus ‹p≠0› ‹q≠0›
by (metis minus_mult_right no_zero_divisors)
qed
moreover have "(∀z. x < z ∧ z < ub ⟶ 0 > poly p z) ⟹ (∀z. x < z ∧ z < ub' ⟶ 0 > poly q z)
⟹ ?thesis"
proof -
assume "(∀z. x < z ∧ z < ub ⟶ 0 > poly p z)" "(∀z. x < z ∧ z < ub' ⟶ 0 > poly q z)"
hence "sign_r_pos (-p) x" and "sign_r_pos (-q) x"
unfolding sign_r_pos_def eventually_at_right using ‹ub>x› ‹ub'>x› by auto
moreover hence "eventually (λz. poly (-p) z>0 ∧ poly (-q) z>0) (at_right x)"
unfolding sign_r_pos_def using eventually_conj_iff[of _ _ "at_right x"] by auto
hence "sign_r_pos (p * q) x"
unfolding sign_r_pos_def poly_mult poly_minus
apply (elim eventually_mono[of _ "at_right x"])
by (auto intro:mult_neg_neg)
ultimately show ?thesis
using sign_r_pos_minus ‹p≠0› ‹q≠0› by metis
qed
ultimately show ?thesis using ub ub' by auto
qed

fixes p q :: "real poly"
assumes "poly p x=0" "poly q x≠0"
shows "sign_r_pos (p+q) x=sign_r_pos q x"
proof (cases "poly (p+q) x=0")
case False
hence "p+q≠0" by (metis poly_0)
have "sign_r_pos (p+q) x = (poly q x > 0)"
using sign_r_pos_rec[OF ‹p+q≠0›] False poly_add ‹poly p x=0› by auto
moreover have "sign_r_pos q x=(poly q x > 0)"
using sign_r_pos_rec[of q x] ‹poly q x≠0› poly_0 by force
ultimately show ?thesis by auto
next
case True
hence False using ‹poly p x=0› ‹poly q x≠0› poly_add by auto
thus ?thesis by auto
qed

lemma sign_r_pos_mod:
fixes p q :: "real poly"
assumes "poly p x=0" "poly q x≠0"
shows "sign_r_pos (q mod p) x=sign_r_pos q x"
proof -
have "poly (q div p * p) x=0" using ‹poly p x=0› poly_mult by auto
moreover hence "poly (q mod p) x ≠ 0" using ‹poly q x≠0›
ultimately show ?thesis
qed

lemma sign_r_pos_pderiv:
fixes p:: "real poly"
assumes "poly p x=0" "p≠0"
shows "sign_r_pos (pderiv p * p) x"
proof -
have "pderiv p ≠0"
pderiv_iszero poly_0 poly_pCons)
have "?thesis = (sign_r_pos (pderiv p) x ⟷ sign_r_pos p x)"
using sign_r_pos_mult[OF ‹pderiv p ≠ 0› ‹p≠0›] by auto
also have "...=((sign_r_pos (pderiv p) x ⟷ sign_r_pos (pderiv p) x))"
using sign_r_pos_rec[OF ‹p≠0›] ‹poly p x=0› by auto
finally show ?thesis by auto
qed

lemma sign_r_pos_power:
fixes p:: "real poly" and a::real
shows "sign_r_pos ([:-a,1:]^n) a"
proof (induct n)
case 0
thus ?case unfolding sign_r_pos_def eventually_at_right by (simp,metis gt_ex)
next
case (Suc n)
have "pderiv ([:-a,1:]^Suc n) = smult (Suc n) ([:-a,1:]^n)"
proof -
have "pderiv [:- a, 1::real:] = 1" by (simp add: pderiv.simps)
thus ?thesis unfolding pderiv_power_Suc by (metis mult_cancel_left1)
qed
moreover have " poly ([:- a, 1:] ^ Suc n) a=0" by (metis old.nat.distinct(2) poly_power_n_eq)
hence "sign_r_pos ([:- a, 1:] ^ Suc n) a = sign_r_pos (smult (Suc n) ([:-a,1:]^n)) a"
using sign_r_pos_rec by (metis (erased, opaque_lifting) calculation pderiv_0)
hence "sign_r_pos ([:- a, 1:] ^ Suc n) a = sign_r_pos  ([:-a,1:]^n) a"
using sign_r_pos_smult by auto
ultimately show ?case using Suc.hyps by auto
qed

subsection‹Jump›

definition jump_poly :: "real poly ⇒ real poly ⇒real ⇒ int"
where
" jump_poly q p x≡ (if p≠0 ∧ q≠0 ∧ odd((order x p) - (order x q) ) then
if sign_r_pos (q*p) x then 1 else -1
else 0 )"

lemma jump_poly_not_root:"poly p x≠0⟹ jump_poly q p x=0"
unfolding  jump_poly_def by (metis even_zero order_root zero_diff)

lemma jump_poly0[simp]:
"jump_poly 0 p x = 0"
"jump_poly q 0 x = 0"
unfolding jump_poly_def by auto

lemma jump_poly_smult_1:
fixes p q::"real poly" and c::real
shows "jump_poly (smult c q) p x= sign c * jump_poly q p x" (is "?L=?R")
proof (cases "c=0∨ q=0")
case True
thus ?thesis unfolding jump_poly_def by auto
next
case False
hence "c≠0" and "q≠0" by auto
thus ?thesis unfolding jump_poly_def
using order_smult[OF ‹c≠0›] sign_r_pos_smult[OF ‹c≠0›, of "q*p" x] ‹q≠0›
by auto
qed

lemma jump_poly_mult:
fixes p q p'::"real poly"
assumes "p'≠0"
shows "jump_poly (p'*q) (p'*p) x= jump_poly q p x"
proof (cases "q=0 ∨ p=0")
case True
thus ?thesis unfolding jump_poly_def by fastforce
next
case False
then have "q≠0" "p≠0" by auto
have "sign_r_pos (p' * q * (p' * p)) x=sign_r_pos (q * p) x"
proof (unfold sign_r_pos_def,rule eventually_subst,unfold eventually_at_right)
obtain b where "b>x" and b:"∀z. x < z ∧ z < b ⟶ poly (p' * p') z >0"
proof (cases "∃z. poly p' z=0 ∧ z>x")
case True
define lr where "lr≡Min {r . poly p' r=0 ∧ r>x}"
have "∀z. x<z∧z<lr⟶poly p' z≠0" and "lr>x"
using True lr_def poly_roots_finite[OF ‹p'≠0›] by auto
hence "∀z. x < z ∧ z < lr ⟶ 0 < poly (p' * p') z"
by (metis not_real_square_gt_zero poly_mult)
thus ?thesis using that[OF ‹lr>x›] by auto
next
case False
have "∀z. x<z∧z<x+1⟶poly p' z≠0" and "x+1>x"
using False poly_roots_finite[OF ‹p'≠0›]  by auto
hence "∀z. x < z ∧ z < x+1 ⟶ 0 < poly (p' * p') z"
by (metis not_real_square_gt_zero poly_mult)
thus ?thesis using that[OF ‹x+1>x›] by auto
qed
show "∃b>x. ∀z>x. z < b ⟶ (0 < poly (p' * q * (p' * p)) z) = (0 < poly (q * p) z)"
proof (rule_tac x="b" in exI, rule conjI[OF ‹b>x›],rule allI,rule impI,rule impI)
fix z assume "x < z"  "z < b"
hence "0<poly (p'*p') z" using b by auto
have " (0 < poly (p' * q * (p' * p)) z)=(0<poly (p'*p') z * poly (q*p) z)"
also have "...=(0<poly (q*p) z)"
using ‹0<poly (p'*p') z› by (metis mult_pos_pos zero_less_mult_pos)
finally show "(0 < poly (p' * q * (p' * p)) z) = (0 < poly (q * p) z)" .
qed
qed
moreover have " odd (order x (p' * p) - order x (p' * q)) = odd (order x p - order x q)"
using  False ‹p'≠0› ‹p≠0› mult_eq_0_iff order_mult
moreover have " p' * q ≠ 0 ⟷ q ≠ 0"
by (metis ‹p'≠0› mult_eq_0_iff)
ultimately show "jump_poly (p' * q) (p' * p) x = jump_poly q p x" unfolding jump_poly_def by auto
qed

lemma jump_poly_1_mult:
fixes p1 p2::"real poly"
assumes "poly p1 x≠0 ∨ poly p2 x≠0"
shows "jump_poly 1 (p1*p2) x= sign (poly p2 x) * jump_poly 1 p1 x
+ sign (poly p1 x) * jump_poly 1 p2 x" (is "?L=?R")
proof (cases "p1=0 ∨ p2 =0")
case True
then show ?thesis by auto
next
case False
then have "p1≠0" "p2≠0" "p1*p2≠0" by auto
have ?thesis when "poly p1 x≠0"
proof -
have [simp]:"order x p1 = 0" using that order_root by blast
define simpL where "simpL≡(if p2≠0 ∧ odd (order x p2) then if (poly p1 x>0)
⟷  sign_r_pos p2 x then 1::int else -1 else 0)"
have "?L=simpL"
unfolding simpL_def jump_poly_def
using order_mult[OF ‹p1*p2≠0›]
sign_r_pos_mult[OF ‹p1≠0› ‹p2≠0›] sign_r_pos_rec[OF ‹p1≠0›] ‹poly p1 x≠0›
by auto
moreover have "poly p1 x>0 ⟹ simpL =?R"
unfolding simpL_def jump_poly_def using jump_poly_not_root[OF ‹poly p1 x≠0›]
by auto
moreover have "poly p1 x<0 ⟹ simpL =?R"
unfolding simpL_def jump_poly_def using jump_poly_not_root[OF ‹poly p1 x≠0›]
by auto
ultimately show "?L=?R" using ‹poly p1 x≠0› by (metis linorder_neqE_linordered_idom)
qed
moreover have ?thesis when "poly p2 x≠0"
proof -
have [simp]:"order x p2 = 0" using that order_root by blast
define simpL where "simpL≡(if p1≠0 ∧ odd (order x p1) then if (poly p2 x>0)
⟷  sign_r_pos p1 x then 1::int else -1 else 0)"
have "?L=simpL"
unfolding simpL_def jump_poly_def
using order_mult[OF ‹p1*p2≠0›]
sign_r_pos_mult[OF ‹p1≠0› ‹p2≠0›] sign_r_pos_rec[OF ‹p2≠0›] ‹poly p2 x≠0›
by auto
moreover have "poly p2 x>0 ⟹ simpL =?R"
unfolding simpL_def jump_poly_def using jump_poly_not_root[OF ‹poly p2 x≠0›]
by auto
moreover have "poly p2 x<0 ⟹ simpL =?R"
unfolding simpL_def jump_poly_def using jump_poly_not_root[OF ‹poly p2 x≠0›]
by auto
ultimately show "?L=?R" using ‹poly p2 x≠0› by (metis linorder_neqE_linordered_idom)
qed
ultimately show ?thesis using assms by auto
qed

lemma jump_poly_mod:
fixes p q::"real poly"
shows "jump_poly q p x= jump_poly (q mod p) p x"
proof (cases "q=0 ∨ p=0")
case True
thus ?thesis by fastforce
next
case False
then have "p≠0" "q≠0" by auto
define n where "n≡min (order x q) (order x p)"
obtain q' where q':"q=[:-x,1:]^n * q'"
using n_def  power_le_dvd[OF order_1[of x q], of n]
by (metis dvdE min.cobounded2 min.commute)
obtain p' where p':"p=[:-x,1:]^n * p'"
using n_def  power_le_dvd[OF order_1[of x p], of n]
by (metis dvdE min.cobounded2)
have "q'≠0" and "p'≠0" using q' p' ‹p≠0› ‹q≠0› by auto
have "order x q'=0 ∨ order x p'=0"
proof (rule ccontr)
assume "¬ (order x q' = 0 ∨ order x p' = 0)"
hence "order x q' > 0" and "order x p' > 0" by auto
hence "order x q>n" and "order x p>n" unfolding q' p'
using order_mult[OF ‹q≠0›[unfolded q'],of x] order_mult[OF ‹p≠0›[unfolded p'],of x]
order_power_n_n[of x n]
by auto
thus False using n_def by auto
qed
have cond:"q' ≠ 0 ∧ odd (order x p' - order x q')
= (q' mod p' ≠0 ∧ odd(order x p' - order x (q' mod p')))"
proof (cases "order x p'=0")
case True
thus ?thesis by (metis ‹q' ≠ 0› even_zero zero_diff)
next
case False
hence "order x q'=0" using ‹order x q'=0 ∨ order x p'=0› by auto
hence "¬ [:-x,1:] dvd q'"
by (metis ‹q' ≠ 0› order_root poly_eq_0_iff_dvd)
moreover have "[:-x,1:] dvd p'" using False
by (metis order_root poly_eq_0_iff_dvd)
ultimately have "¬ [:-x,1:] dvd (q' mod p')"
by (metis dvd_mod_iff)
hence "order x (q' mod p') = 0" and "q' mod p' ≠0"
apply (metis order_root poly_eq_0_iff_dvd)
by (metis ‹¬ [:- x, 1:] dvd q' mod p'› dvd_0_right)
thus ?thesis using ‹order x q'=0› by auto
qed
moreover have "q' mod p'≠0 ⟹ poly p' x = 0
⟹ sign_r_pos (q' * p') x= sign_r_pos (q' mod p' * p') x"
proof -
assume "q' mod p'≠0" "poly p' x = 0"
hence "poly q' x≠0" using ‹order x q'=0 ∨ order x p'=0›
by (metis ‹p' ≠ 0› ‹q' ≠ 0› order_root)
hence "sign_r_pos q' x= sign_r_pos (q' mod p') x"
using sign_r_pos_mod[OF ‹poly p' x=0›] by auto
thus ?thesis
unfolding sign_r_pos_mult[OF ‹q'≠0› ‹p'≠0›] sign_r_pos_mult[OF ‹q' mod p'≠0› ‹p'≠0›]
by auto
qed
moreover have "q' mod p' = 0 ∨ poly p' x ≠ 0 ⟹ jump_poly q' p' x = jump_poly (q' mod p') p' x"
proof -
assume assm:"q' mod p' = 0 ∨ poly p' x ≠ 0"
have "q' mod p' = 0 ⟹ ?thesis" unfolding jump_poly_def
using cond by auto
moreover have "poly p' x ≠ 0
⟹ ¬ odd (order x p' - order x q') ∧ ¬ odd(order x p' - order x (q' mod p'))"
by (metis even_zero order_root zero_diff)
hence "poly p' x ≠ 0 ⟹ ?thesis" unfolding jump_poly_def by auto
ultimately show ?thesis using assm by auto
qed
ultimately have " jump_poly q' p' x = jump_poly (q' mod p') p' x" unfolding jump_poly_def by force
thus ?thesis using p' q' jump_poly_mult by auto
qed

lemma jump_poly_coprime:
fixes p q:: "real poly"
assumes "poly p x=0" "coprime p q"
shows "jump_poly q p x= jump_poly 1 (q*p) x"
proof (cases "p=0 ∨ q=0")
case True
then show ?thesis by auto
next
case False
then have "p≠0" "q≠0" by auto
then have "poly p x≠0 ∨ poly q x≠0" using coprime_poly_0[OF ‹coprime p q›] by auto
then have "poly q x≠0" using ‹poly p x=0› by auto
then have "order x q=0" using order_root by blast
then have "order x p - order x q = order x (q * p)"
using ‹p≠0› ‹q≠0› order_mult [of q p x] by auto
then show ?thesis unfolding jump_poly_def using ‹q≠0› by auto
qed

lemma jump_poly_sgn:
fixes p q:: "real poly"
assumes "p≠0" "poly p x=0"
shows "jump_poly (pderiv p * q) p x = sign (poly q x)"
proof (cases "q=0")
case True
thus ?thesis by auto
next
case False
have "pderiv p≠0" using ‹p≠0› ‹poly p x=0›
by (metis mult_poly_0_left sign_r_pos_0 sign_r_pos_pderiv)
have elim_p_order: "order x p - order x (pderiv p * q)=1 - order x q"
proof -
have "order x p - order x (pderiv p * q) = order x p - order x (pderiv p) - order x q"
using order_mult ‹pderiv p≠0› False by (metis diff_diff_left mult_eq_0_iff)
moreover have "order x p - order x (pderiv p) = 1"
using order_pderiv[OF ‹pderiv p≠0›, of x] ‹poly p x=0› order_root[of p x] ‹p≠0› by auto
ultimately show ?thesis by auto
qed
have elim_p_sign_r_pos:"sign_r_pos (pderiv p * q * p) x=sign_r_pos q x"
proof -
have "sign_r_pos (pderiv p * q * p) x = (sign_r_pos (pderiv p* p) x ⟷ sign_r_pos q x)"
by (metis ‹q ≠ 0› ‹pderiv p ≠ 0› assms(1) no_zero_divisors sign_r_pos_mult)
thus ?thesis using sign_r_pos_pderiv[OF ‹poly p x=0› ‹p≠0›] by auto
qed
define simpleL where "simpleL≡if pderiv p * q ≠ 0 ∧ odd (1 - order x q) then
if sign_r_pos q x then 1::int else - 1 else 0"
have " jump_poly (pderiv p * q) p x =simpleL"
unfolding simpleL_def jump_poly_def by (subst elim_p_order, subst elim_p_sign_r_pos,simp)
moreover have "poly q x=0 ⟹ simpleL=sign (poly q x)"
proof -
assume "poly q x=0"
hence "1-order x q = 0" using ‹q≠0› by (metis less_one not_gr0 order_root zero_less_diff)
hence "simpleL=0" unfolding simpleL_def by auto
moreover have "sign (poly q x)=0" using ‹poly q x=0› by auto
ultimately show ?thesis by auto
qed
moreover have "poly q x≠0⟹ simpleL=sign (poly q x)"
proof -
assume "poly q x≠0"
hence "odd (1 - order x q)" by (simp add: order_root)
moreover have "pderiv p * q ≠ 0" by (metis False ‹pderiv p ≠ 0› no_zero_divisors)
moreover have "sign_r_pos q x = (poly q x > 0)"
using sign_r_pos_rec[OF False] ‹poly q x≠0› by auto
ultimately have "simpleL=(if poly q x>0 then 1 else - 1)" unfolding simpleL_def by auto
thus ?thesis using ‹poly q x≠0› by auto
qed
ultimately show ?thesis by force
qed

subsection ‹Cauchy index›

definition cindex_poly:: "real ⇒ real ⇒ real poly ⇒ real poly ⇒ int"
where
"cindex_poly a b q p≡ (∑x∈{x. poly p x=0 ∧ a< x∧ x< b}. jump_poly q p x)"

lemma cindex_poly_0[simp]: "cindex_poly a b 0 p = 0" "cindex_poly a b q 0 = 0"
unfolding cindex_poly_def by auto

lemma cindex_poly_cross:
fixes p::"real poly" and a b::real
assumes  "a<b" "poly p a≠0" "poly p b≠0"
shows "cindex_poly a b 1 p = cross p a b"
using ‹poly p a≠0› ‹poly p b≠0›
proof (cases "{x. poly p x=0 ∧ a< x∧ x< b}≠{}", induct "degree p" arbitrary:p rule:nat_less_induct)
case 1
then have "p≠0" by force
define roots where "roots≡{x.  poly p x=0 ∧ a< x∧ x< b}"
have "finite roots" unfolding roots_def using poly_roots_finite[OF ‹p≠0›] by auto
define max_r where "max_r≡Max roots"
hence "poly p max_r=0" and "a<max_r" and "max_r<b"
using Max_in[OF ‹finite roots›] "1.prems"  unfolding roots_def by auto
define max_rp where "max_rp≡[:-max_r,1:]^order max_r p"
then obtain p' where p':"p=p'*max_rp" and not_dvd:"¬ [:-max_r,1:] dvd p'"
by (metis ‹p≠0› mult.commute order_decomp)
hence "p'≠0" and "max_rp≠0" and "poly p' a≠0" and "poly p' b≠0"
and  "poly max_rp a≠0" and "poly max_rp b≠0"
using ‹p≠0› ‹poly p a≠0› ‹poly p b≠0›  by auto
define max_r_sign where "max_r_sign≡if odd(order max_r p) then -1 else 1::int"
define roots' where "roots'≡{x.  a< x∧ x< b ∧ poly p' x=0}"
have "(∑x∈roots. jump_poly 1 p x)= (∑x∈roots'. jump_poly 1 p x)+ jump_poly 1 p max_r"
proof -
have "roots=roots' ∪ {x.  a< x∧ x< b ∧ poly max_rp x=0 }"
unfolding roots_def roots'_def p' by auto
moreover have "{x.  a < x ∧ x < b ∧  poly max_rp x = 0 }={max_r}"
unfolding max_rp_def using ‹poly p max_r=0›
by (auto simp add: ‹a<max_r› ‹max_r<b›,metis "1.prems"(1) neq0_conv order_root)
moreover hence "roots' ∩ {x. a< x∧ x< b ∧ poly max_rp x=0} ={}"
unfolding roots'_def  using ‹¬ [:-max_r,1:] dvd p'›
by (metis (mono_tags) Int_insert_right_if0 inf_bot_right mem_Collect_eq poly_eq_0_iff_dvd)
moreover have "finite roots'"
using  p' ‹p≠0› by (metis ‹finite roots› calculation(1) calculation(2) finite_Un)
ultimately show ?thesis using sum.union_disjoint by auto
qed
moreover have "(∑x∈roots'. jump_poly 1 p x) = max_r_sign * cross p' a b"
proof -
have "(∑x∈roots'. jump_poly 1 p x) = (∑x∈roots'. max_r_sign * jump_poly 1 p' x)"
proof (rule sum.cong,rule refl)
fix x assume "x ∈ roots'"
hence "x≠max_r" using not_dvd unfolding roots'_def
by (metis (mono_tags, lifting) mem_Collect_eq poly_eq_0_iff_dvd )
hence "poly max_rp x≠0" using poly_power_n_eq unfolding max_rp_def by auto
hence "order x max_rp=0"  by (metis order_root)
moreover have "jump_poly 1 max_rp x=0"
using ‹poly max_rp x≠0› by (metis jump_poly_not_root)
moreover have "x∈roots"
using ‹x ∈ roots'› unfolding roots_def roots'_def p' by auto
hence "x<max_r"
using Max_ge[OF ‹finite roots›,of x] ‹x≠max_r› by (fold max_r_def,auto)
hence "sign (poly max_rp x) = max_r_sign"
using ‹poly max_rp x ≠ 0› unfolding max_r_sign_def max_rp_def sign_def
ultimately show "jump_poly 1 p x = max_r_sign * jump_poly 1 p' x"
using jump_poly_1_mult[of p' x max_rp]  unfolding p'
by (simp add: ‹poly max_rp x ≠ 0›)
qed
also have "... = max_r_sign * (∑x∈roots'. jump_poly 1 p' x)"
also have "... = max_r_sign * cross p' a b"
proof (cases "roots'={}")
case True
hence "cross p' a b=0" unfolding roots'_def using cross_no_root[OF ‹a<b›] by auto
thus ?thesis using True by simp
next
case False
moreover have "degree max_rp≠0"
unfolding max_rp_def degree_linear_power
by (metis "1.prems"(1) ‹poly p max_r = 0› order_root)
hence  "degree p' < degree p" unfolding p' degree_mult_eq[OF ‹p'≠0› ‹max_rp≠0›]
by auto
ultimately have "cindex_poly a b 1 p' = cross p' a b"
unfolding roots'_def
using "1.hyps"[rule_format,of "degree p'" p'] ‹p'≠0› ‹poly p' a≠0› ‹poly p' b≠0›
by auto
moreover have "cindex_poly a b 1 p' = sum (jump_poly 1 p') roots'"
unfolding cindex_poly_def roots'_def
apply simp
by (metis (no_types, lifting) )
ultimately show ?thesis by auto
qed
finally show ?thesis .
qed
moreover have "max_r_sign * cross p' a b + jump_poly 1 p max_r = cross p a b" (is "?L=?R")
proof (cases "odd (order max_r p)")
case True
have "poly max_rp a < 0"
using poly_power_n_odd[OF True,of max_r a] ‹poly max_rp a≠0› ‹max_r>a›
unfolding max_rp_def by linarith
moreover have "poly max_rp b>0 "
using poly_power_n_odd[OF True,of max_r b] ‹max_r<b›
unfolding max_rp_def by linarith
ultimately have "?R=cross p' a b + sign (poly p' a)"
unfolding p' cross_def poly_mult
using variation_mult_neg_1[of "poly max_rp a", simplified mult.commute]
variation_mult_pos(2)[of "poly max_rp b", simplified mult.commute] ‹poly p' b≠0›
by auto
moreover have "?L=- cross p' a b + sign (poly p' b)"
proof -
have " sign_r_pos p' max_r = (poly p' max_r >0)"
using sign_r_pos_rec[OF ‹p'≠0›] not_dvd by (metis poly_eq_0_iff_dvd)
moreover have "(poly p' max_r>0) = (poly p' b>0)"
proof (rule ccontr)
assume "(0 < poly p' max_r) ≠ (0 < poly p' b)"
hence "poly p' max_r * poly p' b <0"
using ‹poly p' b≠0› not_dvd[folded poly_eq_0_iff_dvd]
by (metis (poly_guards_query) linorder_neqE_linordered_idom mult_less_0_iff)
then obtain r where "r>max_r" and "r<b" and "poly p' r=0"
using poly_IVT[OF ‹max_r<b›] by auto
hence "r∈roots" unfolding roots_def p' using ‹max_r>a› by auto
thus False using ‹r>max_r› Max_ge[OF ‹finite roots›,of r] unfolding max_r_def by auto
qed
moreover have "sign_r_pos max_rp max_r"
using sign_r_pos_power unfolding max_rp_def by auto
ultimately show ?thesis
using True ‹poly p' b≠0› ‹max_rp≠0› ‹p'≠0› sign_r_pos_mult[OF ‹p'≠0› ‹max_rp≠0›]
unfolding max_r_sign_def  p' jump_poly_def
by simp
qed
moreover have "variation (poly p' a) (poly p' b) + sign (poly p' a)
= - variation (poly p' a) (poly p' b) + sign (poly p' b)" unfolding cross_def
by (cases "poly p' b" rule:linorder_cases[of 0], (cases "poly p' a" rule:linorder_cases[of 0],
auto simp add:variation_cases ‹poly p' a ≠ 0› ‹poly p' b ≠ 0›)+)
ultimately show ?thesis unfolding cross_def by auto
next
case False
hence "poly max_rp a > 0" and "poly max_rp b > 0"
unfolding max_rp_def poly_power
using ‹poly max_rp a≠0› ‹poly max_rp b ≠ 0›  "1.prems"(1-2) ‹poly p max_r = 0›
apply (unfold zero_less_power_eq)
by auto
moreover have "poly max_rp b > 0"
unfolding max_rp_def poly_power
using ‹poly max_rp b ≠ 0› False max_rp_def poly_power
zero_le_even_power[of "order max_r p" "b - max_r"]
ultimately have "?R=cross p' a b"
apply (simp only: p' mult.commute cross_def) using variation_mult_pos
by auto
thus ?thesis unfolding max_r_sign_def jump_poly_def using False by auto
qed
ultimately have "sum (jump_poly 1 p) roots = cross p a b " by auto
then show ?case unfolding roots_def cindex_poly_def by simp
next
case False
hence "cross p a b=0" using cross_no_root[OF ‹a<b›] by auto
thus ?thesis using False unfolding cindex_poly_def by (metis sum.empty)
qed

lemma cindex_poly_mult:
fixes p q p'::"real poly"
assumes "p'≠ 0"
shows "cindex_poly a b (p' * q ) (p' * p) = cindex_poly a b q p"
proof (cases "p=0")
case True
then show ?thesis by auto
next
case False
show ?thesis unfolding cindex_poly_def
apply (rule sum.mono_neutral_cong_right)
subgoal using ‹p≠0› ‹p'≠0› by (simp add: poly_roots_finite)
subgoal by auto
subgoal using jump_poly_mult jump_poly_not_root assms by fastforce
subgoal for x using jump_poly_mult[OF ‹p'≠0›] by auto
done
qed

lemma cindex_poly_smult_1:
fixes p q::"real poly" and c::real
shows "cindex_poly a b (smult c q) p =  (sign c) * cindex_poly a b q p"
unfolding cindex_poly_def
using sum_distrib_left[THEN sym, of "sign c" "λx. jump_poly q p x"
"{x. poly p x = (0::real) ∧ a < x ∧ x < b}"] jump_poly_smult_1
by auto

lemma cindex_poly_mod:
fixes p q::"real poly"
shows "cindex_poly a b q p =  cindex_poly a b (q mod p) p"
unfolding cindex_poly_def using jump_poly_mod by auto

fixes p q::"real poly"
assumes "coprime p q"
shows "cindex_poly a b q p + cindex_poly a b p q=cindex_poly a b 1 (q*p)"
(is "?L=?R")
proof (cases "p=0 ∨ q=0")
case True
then show ?thesis by auto
next
case False
then have "p≠0" "q≠0" by auto
define A where "A≡{x. poly p x = 0 ∧ a < x ∧ x < b}"
define B where "B≡{x. poly q x = 0 ∧ a < x ∧ x < b}"
have "?L = sum (λx. jump_poly 1 (q*p) x) A + sum (λx. jump_poly 1 (q*p) x) B"
proof -
have "cindex_poly a b q p = sum (λx. jump_poly 1 (q*p) x) A" unfolding A_def cindex_poly_def
using jump_poly_coprime[OF _ ‹coprime p q›] by auto
moreover have "coprime q p" using ‹coprime p q›
hence "cindex_poly a b p q = sum (λx. jump_poly 1 (q*p) x) B" unfolding B_def cindex_poly_def
using jump_poly_coprime [of q _ p] by (auto simp add: ac_simps)
ultimately show ?thesis by auto
qed
moreover have "A ∪ B= {x. poly (q*p) x=0 ∧ a<x ∧ x<b }" unfolding poly_mult A_def B_def by auto
moreover have "A ∩ B={}"
proof (rule ccontr)
assume "A ∩ B≠{}"
then obtain x where "x∈A" and "x∈B" by auto
hence "poly p x=0" and "poly q x=0" unfolding A_def B_def by auto
hence "gcd p q≠1" by (metis poly_1 poly_eq_0_iff_dvd gcd_greatest zero_neq_one)
thus False using ‹coprime p q› by auto
qed
moreover have "finite A" and "finite B"
unfolding A_def B_def using poly_roots_finite ‹p≠0› ‹q≠0› by fast+
ultimately have "cindex_poly a b q p + cindex_poly a b p q
= sum (jump_poly 1 (q * p)) {x. poly (q*p) x=0 ∧ a<x ∧ x<b}"
using sum.union_disjoint by metis
then show ?thesis unfolding cindex_poly_def by auto
qed