# Theory Extended_Sturm

(*
Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
*)

section ‹An alternative Sturm sequences›

theory Extended_Sturm imports
"Sturm_Tarski.Sturm_Tarski"
"Winding_Number_Eval.Cauchy_Index_Theorem"
begin

text ‹The main purpose of this theory is to provide an effective way to compute
@{term "cindexE a b f"} when @{term f} is a rational function. The idea is similar to and based
on the evaluation of @{term cindex_poly} through @{thm cindex_poly_changes_itv_mods}.›

text ‹
This alternative version of remainder sequences is inspired by the paper
"The Fundamental Theorem of Algebra made effective:
an elementary real-algebraic proof via Sturm chains"
by Michael Eisermann.
›

hide_const Permutations.sign

subsection ‹Misc›

lemma is_unit_pCons_ex_iff:
fixes p::"'a::field poly"
shows "is_unit p ⟷ (∃a. a≠0 ∧ p=[:a:])"
using is_unit_poly_iff is_unit_triv by auto

lemma poly_gcd_iff:
"poly (gcd p q) x=0 ⟷ poly p x=0 ∧ poly q x=0 "

lemma eventually_poly_nz_at_within:
fixes x :: "'a::{idom,euclidean_space} "
assumes "p≠0"
shows "eventually (λx. poly p x≠0) (at x within S)"
proof -
have "eventually (λx. poly p x≠0) (at x within S)
= (∀⇩F x in (at x within S). ∀y∈proots p. x ≠ y)"
apply (rule eventually_subst,rule eventuallyI)
also have "... = (∀y∈proots p. ∀⇩F x in (at x within S). x ≠ y)"
apply (subst eventually_ball_finite_distrib)
using ‹p≠0› by auto
also have "..."
unfolding eventually_at
by (metis gt_ex not_less_iff_gr_or_eq zero_less_dist_iff)
finally show ?thesis .
qed

lemma sgn_power:
fixes x::"'a::linordered_idom"
shows "sgn (x^n) = (if n=0 then 1 else if even n then ¦sgn x¦ else sgn x)"
apply (induct n)

lemma poly_divide_filterlim_at_top:
fixes p q::"real poly"
defines "ll≡( if degree q<degree p then
at 0
else if degree q=degree p then
else if sgn_pos_inf q * sgn_pos_inf p > 0 then
at_top
else
at_bot)"
assumes "p≠0" "q≠0"
shows "filterlim (λx. poly q x / poly p x) ll at_top"
proof -
define pp where "pp=(λx. poly p x / x^(degree p))"
define qq where "qq=(λx. poly q x / x^(degree q))"
define dd where "dd=(λx::real. if degree p>degree q then 1/x^(degree p - degree q) else
x^(degree q - degree p))"
have divide_cong:"∀⇩Fx in at_top. poly q x / poly p x = qq x / pp x * dd x"
proof (rule eventually_at_top_linorderI[of 1])
fix x assume "(x::real)≥1"
then have "x≠0" by auto
then show "poly q x / poly p x = qq x / pp x * dd x"
unfolding qq_def pp_def dd_def using assms
qed
have qqpp_tendsto:"((λx. qq x / pp x) ⤏ lead_coeff q / lead_coeff p) at_top"
proof -
have "(qq ⤏ lead_coeff q) at_top"
unfolding qq_def using poly_divide_tendsto_aux[of q]
by (auto elim!:filterlim_mono simp:at_top_le_at_infinity)
moreover have "(pp ⤏ lead_coeff p) at_top"
unfolding pp_def using poly_divide_tendsto_aux[of p]
by (auto elim!:filterlim_mono simp:at_top_le_at_infinity)
ultimately show ?thesis using ‹p≠0› by (auto intro!:tendsto_eq_intros)
qed

have ?thesis when "degree q<degree p"
proof -
have "filterlim (λx. poly q x / poly p x) (at 0) at_top"
proof (rule filterlim_atI)
show "((λx. poly q x / poly p x) ⤏ 0) at_top"
using poly_divide_tendsto_0_at_infinity[OF that]
by (auto elim:filterlim_mono simp:at_top_le_at_infinity)
have "∀⇩F x in at_top. poly q x ≠0" "∀⇩F x in at_top. poly p x ≠0"
using poly_eventually_not_zero[OF ‹q≠0›] poly_eventually_not_zero[OF ‹p≠0›]
filter_leD[OF at_top_le_at_infinity]
by auto
then show "∀⇩F x in at_top. poly q x / poly p x ≠ 0"
apply eventually_elim
by auto
qed
then show ?thesis unfolding ll_def using that by auto
qed
moreover have ?thesis when "degree q=degree p"
proof -
have "((λx. poly q x / poly p x) ⤏ lead_coeff q / lead_coeff p) at_top"
using divide_cong qqpp_tendsto that unfolding dd_def
by (auto dest:tendsto_cong)
then show ?thesis unfolding ll_def using that by auto
qed
moreover have ?thesis when "degree q>degree p" "sgn_pos_inf q * sgn_pos_inf p > 0"
proof -
have "filterlim (λx. (qq x / pp x) * dd x) at_top at_top"
proof (subst filterlim_tendsto_pos_mult_at_top_iff[OF qqpp_tendsto])
show "0 < lead_coeff q / lead_coeff p" using that(2) unfolding sgn_pos_inf_def
show "filterlim dd at_top at_top"
unfolding dd_def using that(1)
by (auto intro!:filterlim_pow_at_top simp:filterlim_ident)
qed
then have "LIM x at_top. poly q x / poly p x :> at_top"
using filterlim_cong[OF _ _ divide_cong] by blast
then show ?thesis unfolding ll_def using that by auto
qed
moreover have ?thesis  when "degree q>degree p" "¬ sgn_pos_inf q * sgn_pos_inf p > 0"
proof -
have "filterlim (λx. (qq x / pp x) * dd x) at_bot at_top"
proof (subst filterlim_tendsto_neg_mult_at_bot_iff[OF qqpp_tendsto])
using that(2) ‹p≠0› ‹q≠0› unfolding sgn_pos_inf_def
linorder_neqE_linordered_idom sgn_divide sgn_greater)
show "filterlim dd at_top at_top"
unfolding dd_def using that(1)
by (auto intro!:filterlim_pow_at_top simp:filterlim_ident)
qed
then have "LIM x at_top. poly q x / poly p x :> at_bot"
using filterlim_cong[OF _ _ divide_cong] by blast
then show ?thesis unfolding ll_def using that by auto
qed
ultimately show ?thesis by linarith
qed

lemma poly_divide_filterlim_at_bot:
fixes p q::"real poly"
defines "ll≡( if degree q<degree p then
at 0
else if degree q=degree p then
else if sgn_neg_inf q * sgn_neg_inf p > 0 then
at_top
else
at_bot)"
assumes "p≠0" "q≠0"
shows "filterlim (λx. poly q x / poly p x) ll at_bot"
proof -
define pp where "pp=(λx. poly p x / x^(degree p))"
define qq where "qq=(λx. poly q x / x^(degree q))"
define dd where "dd=(λx::real. if degree p>degree q then 1/x^(degree p - degree q) else
x^(degree q - degree p))"
have divide_cong:"∀⇩Fx in at_bot. poly q x / poly p x = qq x / pp x * dd x"
proof (rule eventually_at_bot_linorderI[of "-1"])
fix x assume "(x::real)≤-1"
then have "x≠0" by auto
then show "poly q x / poly p x = qq x / pp x * dd x"
unfolding qq_def pp_def dd_def using assms
qed
have qqpp_tendsto:"((λx. qq x / pp x) ⤏ lead_coeff q / lead_coeff p) at_bot"
proof -
have "(qq ⤏ lead_coeff q) at_bot"
unfolding qq_def using poly_divide_tendsto_aux[of q]
by (auto elim!:filterlim_mono simp:at_bot_le_at_infinity)
moreover have "(pp ⤏ lead_coeff p) at_bot"
unfolding pp_def using poly_divide_tendsto_aux[of p]
by (auto elim!:filterlim_mono simp:at_bot_le_at_infinity)
ultimately show ?thesis using ‹p≠0› by (auto intro!:tendsto_eq_intros)
qed

have ?thesis when "degree q<degree p"
proof -
have "filterlim (λx. poly q x / poly p x) (at 0) at_bot"
proof (rule filterlim_atI)
show "((λx. poly q x / poly p x) ⤏ 0) at_bot"
using poly_divide_tendsto_0_at_infinity[OF that]
by (auto elim:filterlim_mono simp:at_bot_le_at_infinity)
have "∀⇩F x in at_bot. poly q x ≠0" "∀⇩F x in at_bot. poly p x ≠0"
using poly_eventually_not_zero[OF ‹q≠0›] poly_eventually_not_zero[OF ‹p≠0›]
filter_leD[OF at_bot_le_at_infinity]
by auto
then show "∀⇩F x in at_bot. poly q x / poly p x ≠ 0"
by eventually_elim auto
qed
then show ?thesis unfolding ll_def using that by auto
qed
moreover have ?thesis when "degree q=degree p"
proof -
have "((λx. poly q x / poly p x) ⤏ lead_coeff q / lead_coeff p) at_bot"
using divide_cong qqpp_tendsto that unfolding dd_def
by (auto dest:tendsto_cong)
then show ?thesis unfolding ll_def using that by auto
qed
moreover have ?thesis when "degree q>degree p" "sgn_neg_inf q * sgn_neg_inf p > 0"
proof -
have "(cc > 0 ∧ even (degree q - degree p)) ∨ (cc<0 ∧ odd (degree q - degree p))"
proof -
have "even (degree q - degree p) ⟷
(even (degree q) ∧ even (degree p)) ∨ (odd (degree q) ∧ odd (degree p))"
using ‹degree q>degree p› by auto
then show ?thesis
using that ‹p≠0› ‹q≠0› unfolding sgn_neg_inf_def cc_def zero_less_mult_iff
divide_less_0_iff zero_less_divide_iff
apply (simp add:if_split[of "(<) 0"] if_split[of "(>) 0"])
by argo
qed
moreover have "filterlim (λx. (qq x / pp x) * dd x) at_top at_bot"
when "cc>0" "even (degree q - degree p)"
proof (subst filterlim_tendsto_pos_mult_at_top_iff[OF qqpp_tendsto])
show "0 < lead_coeff q / lead_coeff p" using ‹cc>0› unfolding cc_def by auto
show "filterlim dd at_top at_bot"
unfolding dd_def using ‹degree q>degree p› that(2)
by (auto intro!:filterlim_pow_at_bot_even simp:filterlim_ident)
qed
moreover have "filterlim (λx. (qq x / pp x) * dd x) at_top at_bot"
when "cc<0" "odd (degree q - degree p)"
proof (subst filterlim_tendsto_neg_mult_at_top_iff[OF qqpp_tendsto])
show "0 > lead_coeff q / lead_coeff p" using ‹cc<0› unfolding cc_def by auto
show "filterlim dd at_bot at_bot"
unfolding dd_def using ‹degree q>degree p› that(2)
by (auto intro!:filterlim_pow_at_bot_odd simp:filterlim_ident)
qed
ultimately have "filterlim (λx. (qq x / pp x) * dd x) at_top at_bot"
by blast
then have "LIM x at_bot. poly q x / poly p x :> at_top"
using filterlim_cong[OF _ _ divide_cong] by blast
then show ?thesis unfolding ll_def using that by auto
qed
moreover have ?thesis  when "degree q>degree p" "¬ sgn_neg_inf q * sgn_neg_inf p > 0"
proof -
have "(cc < 0 ∧ even (degree q - degree p)) ∨ (cc > 0 ∧ odd (degree q - degree p))"
proof -
have "even (degree q - degree p) ⟷
(even (degree q) ∧ even (degree p)) ∨ (odd (degree q) ∧ odd (degree p))"
using ‹degree q>degree p› by auto
then show ?thesis
using that ‹p≠0› ‹q≠0› unfolding sgn_neg_inf_def cc_def zero_less_mult_iff
divide_less_0_iff zero_less_divide_iff
apply (simp add:if_split[of "(<) 0"] if_split[of "(>) 0"])
qed
moreover have "filterlim (λx. (qq x / pp x) * dd x) at_bot at_bot"
when "cc<0" "even (degree q - degree p)"
proof (subst filterlim_tendsto_neg_mult_at_bot_iff[OF qqpp_tendsto])
show "0 > lead_coeff q / lead_coeff p" using ‹cc<0› unfolding cc_def by auto
show "filterlim dd at_top at_bot"
unfolding dd_def using ‹degree q>degree p› that(2)
by (auto intro!:filterlim_pow_at_bot_even simp:filterlim_ident)
qed
moreover have "filterlim (λx. (qq x / pp x) * dd x) at_bot at_bot"
when "cc>0" "odd (degree q - degree p)"
proof (subst filterlim_tendsto_pos_mult_at_bot_iff[OF qqpp_tendsto])
show "0 < lead_coeff q / lead_coeff p" using ‹cc>0› unfolding cc_def by auto
show "filterlim dd at_bot at_bot"
unfolding dd_def using ‹degree q>degree p› that(2)
by (auto intro!:filterlim_pow_at_bot_odd simp:filterlim_ident)
qed
ultimately have "filterlim (λx. (qq x / pp x) * dd x) at_bot at_bot"
by blast
then have "LIM x at_bot. poly q x / poly p x :> at_bot"
using filterlim_cong[OF _ _ divide_cong] by blast
then show ?thesis unfolding ll_def using that by auto
qed
ultimately show ?thesis by linarith
qed

subsection ‹Alternative definition of cross›

definition cross_alt :: "real poly ⇒real poly ⇒ real ⇒ real ⇒ int" where
"cross_alt p q a b=¦sign (poly p a) - sign (poly q a)¦ - ¦sign (poly p b) - sign(poly q b)¦"

lemma cross_alt_coprime_0:
assumes "coprime p q" "p=0∨q=0"
shows "cross_alt p q a b=0"
proof -
have ?thesis when "p=0"
proof -
have "is_unit q" using that ‹coprime p q›
by simp
then obtain a where "a≠0" "q=[:a:]" using is_unit_pCons_ex_iff by blast
then show ?thesis using that unfolding cross_alt_def by auto
qed
moreover have ?thesis when "q=0"
proof -
have "is_unit p" using that ‹coprime p q›
by simp
then obtain a where "a≠0" "p=[:a:]" using is_unit_pCons_ex_iff by blast
then show ?thesis using that unfolding cross_alt_def by auto
qed
ultimately show ?thesis using ‹p=0∨q=0› by auto
qed

lemma cross_alt_0[simp]: "cross_alt 0 0 a b=0" unfolding cross_alt_def by auto

lemma cross_alt_poly_commute:
"cross_alt p q a b = cross_alt q p a b"
unfolding cross_alt_def by auto

lemma cross_alt_clear_n:
assumes "coprime p q"
shows "cross_alt p q a b = cross_alt 1 (p*q) a b"
proof -
have "¦sign (poly p a) - sign (poly q a)¦  = ¦1 - sign (poly p a) * sign (poly q a)¦"
proof (cases "poly p a=0 ∧ poly q a=0")
case True
then have False using assms using coprime_poly_0 by blast
then show ?thesis by auto
next
case False
then show ?thesis
unfolding Sturm_Tarski.sign_def
by force
qed
moreover have "¦sign (poly p b) - sign (poly q b)¦  = ¦1 - sign (poly p b) * sign (poly q b)¦"
proof (cases "poly p b=0 ∧ poly q b=0")
case True
then have False using assms using coprime_poly_0 by blast
then show ?thesis by auto
next
case False
then show ?thesis
unfolding Sturm_Tarski.sign_def
by force
qed
ultimately show ?thesis
qed

subsection ‹Alternative sign variation sequencse›

fun changes_alt:: "('a ::linordered_idom) list ⇒ int" where
"changes_alt [] = 0"|
"changes_alt [_] = 0" |
"changes_alt (x1#x2#xs) = abs(sign x1 - sign x2) + changes_alt (x2#xs)"

definition changes_alt_poly_at::"('a ::linordered_idom) poly list ⇒ 'a ⇒ int" where
"changes_alt_poly_at ps a= changes_alt (map (λp. poly p a) ps)"

definition changes_alt_itv_smods:: "real ⇒ real ⇒real poly ⇒ real poly ⇒  int" where
"changes_alt_itv_smods a b p q= (let ps= smods p q
in changes_alt_poly_at ps a - changes_alt_poly_at ps b)"

lemma changes_alt_itv_smods_rec:
assumes "a<b" "coprime p q"
shows "changes_alt_itv_smods a b p q  = cross_alt p q a b + changes_alt_itv_smods a b q (-(p mod q))"
proof (cases "p = 0 ∨ q = 0 ∨ q dvd p")
case True
moreover have "p=0 ∨ q=0 ⟹ ?thesis"
using cross_alt_coprime_0[OF ‹coprime p q›]
unfolding changes_alt_itv_smods_def changes_alt_poly_at_def by fastforce
moreover have "⟦p≠0;q≠0;p mod q = 0⟧ ⟹ ?thesis"
unfolding changes_alt_itv_smods_def changes_alt_poly_at_def cross_alt_def
ultimately show ?thesis
by auto (auto elim: dvdE)
next
case False
hence "p≠0" "q≠0" "p mod q≠0" by auto
then obtain ps where ps:"smods p q=p#q#-(p mod q)#ps" "smods q (-(p mod q)) = q#-(p mod q)#ps"
by auto
define changes_diff where "changes_diff≡λx. changes_alt_poly_at (p#q#-(p mod q)#ps) x
- changes_alt_poly_at (q#-(p mod q)#ps) x"
have "changes_diff a - changes_diff b=cross_alt p q a b"
unfolding changes_diff_def changes_alt_poly_at_def cross_alt_def by simp
thus ?thesis unfolding changes_alt_itv_smods_def changes_diff_def changes_alt_poly_at_def ps
by force
qed

subsection ‹jumpF on polynomials›

definition jumpF_polyR:: "real poly ⇒ real poly ⇒ real ⇒ real" where
"jumpF_polyR q p a = jumpF (λx. poly q x / poly p x) (at_right a)"

definition jumpF_polyL:: "real poly ⇒ real poly ⇒ real ⇒ real" where
"jumpF_polyL q p a = jumpF (λx. poly q x / poly p x) (at_left a)"

definition jumpF_poly_top:: "real poly ⇒ real poly ⇒ real" where
"jumpF_poly_top q p = jumpF (λx. poly q x / poly p x) at_top"

definition jumpF_poly_bot:: "real poly ⇒ real poly ⇒ real" where
"jumpF_poly_bot q p = jumpF (λx. poly q x / poly p x) at_bot"

lemma jumpF_polyR_0[simp]: "jumpF_polyR 0 p a = 0" "jumpF_polyR q 0 a = 0"
unfolding jumpF_polyR_def by auto

lemma jumpF_polyL_0[simp]: "jumpF_polyL 0 p a = 0" "jumpF_polyL q 0 a = 0"
unfolding jumpF_polyL_def by auto

lemma jumpF_polyR_mult_cancel:
assumes "p'≠0"
shows "jumpF_polyR (p' * q) (p' * p) a = jumpF_polyR q p a"
unfolding jumpF_polyR_def
proof (rule jumpF_cong)
obtain ub where "a < ub" "∀z. a < z ∧ z ≤ ub ⟶ poly p' z ≠ 0"
using next_non_root_interval[OF ‹p'≠0›,of a] by auto
then show "∀⇩F x in at_right a. poly (p' * q) x / poly (p' * p) x = poly q x / poly p x"
apply (unfold eventually_at_right)
apply (intro exI[where x=ub])
by auto
qed simp

lemma jumpF_polyL_mult_cancel:
assumes "p'≠0"
shows "jumpF_polyL (p' * q) (p' * p) a = jumpF_polyL q p a"
unfolding jumpF_polyL_def
proof (rule jumpF_cong)
obtain lb where "lb < a" "∀z. lb ≤ z ∧ z < a ⟶ poly p' z ≠ 0 "
using last_non_root_interval[OF ‹p'≠0›,of a] by auto
then show "∀⇩F x in at_left a. poly (p' * q) x / poly (p' * p) x = poly q x / poly p x"
apply (unfold eventually_at_left)
apply (intro exI[where x=lb])
by auto
qed simp

lemma jumpF_poly_noroot:
assumes "poly p a≠0"
shows "jumpF_polyL q p a = 0" "jumpF_polyR q p a = 0"
subgoal unfolding jumpF_polyL_def using assms
apply (intro jumpF_not_infinity)
by (auto intro!:continuous_intros)
subgoal unfolding jumpF_polyR_def using assms
apply (intro jumpF_not_infinity)
by (auto intro!:continuous_intros)
done

lemma jumpF_polyR_coprime:
assumes "coprime p q"
shows "jumpF_polyR q p x = (if p ≠ 0 ∧ q ≠ 0 ∧ poly p x=0 then
if sign_r_pos p x ⟷ poly q x>0 then 1/2 else - 1/2 else 0)"
proof (cases "p=0 ∨ q=0 ∨ poly p x≠0")
case True
then show ?thesis using jumpF_poly_noroot by fastforce
next
case False
then have asm:"p≠0" "q≠0" "poly p x=0" by auto
then have "poly q x≠0" using assms using coprime_poly_0 by blast
have ?thesis when "sign_r_pos p x ⟷ poly q x>0"
proof -
have "(poly p has_sgnx sgn (poly q x)) (at_right x)"
by (metis False ‹poly q x ≠ 0› add.inverse_neutral has_sgnx_imp_sgnx less_not_sym
neg_less_iff_less poly_has_sgnx_values(2) sgn_if sign_r_pos_sgnx_iff that
trivial_limit_at_right_real zero_less_one)
then have "LIM x at_right x. poly q x / poly p x :> at_top"
apply (subst filterlim_divide_at_bot_at_top_iff[of _ "poly q x"])
apply (auto simp add:‹poly q x≠0›)
by (metis asm(3) poly_tendsto(3))
then have "jumpF_polyR q p x = 1/2"
unfolding jumpF_polyR_def jumpF_def by auto
then show ?thesis using that False by auto
qed
moreover have ?thesis when "¬ (sign_r_pos p x ⟷ poly q x>0)"
proof -
have "(poly p has_sgnx - sgn (poly q x)) (at_right x)"
proof -
have "(0::real) < 1 ∨ ¬ (1::real) < 0 ∧ sign_r_pos p x
∨ (poly p has_sgnx - sgn (poly q x)) (at_right x)"
by simp
then show ?thesis
by (metis (no_types) False ‹poly q x ≠ 0› add.inverse_inverse has_sgnx_imp_sgnx
neg_less_0_iff_less poly_has_sgnx_values(2) sgn_if sgn_less sign_r_pos_sgnx_iff
that trivial_limit_at_right_real)
qed
then have "LIM x at_right x. poly q x / poly p x :> at_bot"
apply (subst filterlim_divide_at_bot_at_top_iff[of _ "poly q x"])
apply (auto simp add:‹poly q x≠0›)
by (metis asm(3) poly_tendsto(3))
then have "jumpF_polyR q p x = - 1/2"
unfolding jumpF_polyR_def jumpF_def by auto
then show ?thesis using that False by auto
qed
ultimately show ?thesis by auto
qed

lemma jumpF_polyL_coprime:
assumes "coprime p q"
shows "jumpF_polyL q p x = (if p ≠ 0 ∧ q ≠ 0 ∧ poly p x=0 then
if even (order x p) ⟷ sign_r_pos p x ⟷ poly q x>0 then 1/2 else - 1/2 else 0)"
proof (cases "p=0 ∨ q=0 ∨ poly p x≠0")
case True
then show ?thesis using jumpF_poly_noroot by fastforce
next
case False
then have asm:"p≠0" "q≠0" "poly p x=0" by auto
then have "poly q x≠0" using assms using coprime_poly_0 by blast
have ?thesis when "even (order x p) ⟷ sign_r_pos p x ⟷ poly q x>0"
proof -
consider (lt) "poly q x>0" | (gt) " poly q x<0" using ‹poly q x≠0› by linarith
then have "sgnx (poly p) (at_left x) = sgn (poly q x)"
apply cases
subgoal using that sign_r_pos_sgnx_iff poly_sgnx_values[OF ‹p≠0›,of x]
apply (subst poly_sgnx_left_right[OF ‹p≠0›])
by auto
subgoal using that sign_r_pos_sgnx_iff poly_sgnx_values[OF ‹p≠0›,of x]
apply (subst poly_sgnx_left_right[OF ‹p≠0›])
by auto
done
then have "(poly p has_sgnx sgn (poly q x)) (at_left x)"
by (metis sgnx_able_poly(2) sgnx_able_sgnx)
then have "LIM x at_left x. poly q x / poly p x :> at_top"
apply (subst filterlim_divide_at_bot_at_top_iff[of _ "poly q x"])
apply (auto simp add:‹poly q x≠0›)
by (metis asm(3) poly_tendsto(2))
then have "jumpF_polyL q p x = 1/2"
unfolding jumpF_polyL_def jumpF_def by auto
then show ?thesis using that False by auto
qed
moreover have ?thesis when "¬ (even (order x p) ⟷ sign_r_pos p x ⟷ poly q x>0)"
proof -
consider (lt) "poly q x>0" | (gt) " poly q x<0" using ‹poly q x≠0› by linarith
then have "sgnx (poly p) (at_left x) = - sgn (poly q x)"
apply cases
subgoal using that sign_r_pos_sgnx_iff poly_sgnx_values[OF ‹p≠0›,of x]
apply (subst poly_sgnx_left_right[OF ‹p≠0›])
by auto
subgoal using that sign_r_pos_sgnx_iff poly_sgnx_values[OF ‹p≠0›,of x]
apply (subst poly_sgnx_left_right[OF ‹p≠0›])
by auto
done
then have "(poly p has_sgnx - sgn (poly q x)) (at_left x)"
by (metis sgnx_able_poly(2) sgnx_able_sgnx)
then have "LIM x at_left x. poly q x / poly p x :> at_bot"
apply (subst filterlim_divide_at_bot_at_top_iff[of _ "poly q x"])
apply (auto simp add:‹poly q x≠0›)
by (metis asm(3) poly_tendsto(2))
then have "jumpF_polyL q p x = - 1/2"
unfolding jumpF_polyL_def jumpF_def by auto
then show ?thesis using that False by auto
qed
ultimately show ?thesis by auto
qed

lemma jumpF_times:
assumes tendsto:"(f ⤏ c) F" and "c≠0" "F≠bot"
shows "jumpF (λx. f x * g x) F = sgn c * jumpF g F"
proof -
have "c>0 ∨ c<0" using ‹c≠0› by auto
moreover have ?thesis when "c>0"
proof -
note filterlim_tendsto_pos_mult_at_top_iff[OF tendsto ‹c>0›,of g]
moreover note filterlim_tendsto_pos_mult_at_bot_iff[OF tendsto ‹c>0›,of g]
moreover have "sgn c = 1" using ‹c>0› by auto
ultimately show ?thesis unfolding jumpF_def by auto
qed
moreover have ?thesis when "c<0"
proof -
define atbot where "atbot = filterlim g at_bot F"
define attop where "attop = filterlim g at_top F"
have "jumpF (λx. f x * g x) F = (if atbot then 1 / 2 else if attop then - 1 / 2 else 0)"
proof -
note filterlim_tendsto_neg_mult_at_top_iff[OF tendsto ‹c<0›,of g]
moreover note filterlim_tendsto_neg_mult_at_bot_iff[OF tendsto ‹c<0›,of g]
ultimately show ?thesis unfolding jumpF_def atbot_def attop_def by auto
qed
also have "... = - (if attop then 1 / 2 else if atbot then - 1 / 2 else 0)"
proof -
have False when atbot attop
using filterlim_at_top_at_bot[OF _ _ ‹F≠bot›] that unfolding atbot_def attop_def by auto
then show ?thesis by fastforce
qed
also have "... = sgn c * jumpF g F"
using ‹c<0› unfolding jumpF_def attop_def atbot_def by auto
finally show ?thesis .
qed
ultimately show ?thesis by auto
qed

assumes "coprime p q"
shows "jumpF_polyR q p x + jumpF_polyR p q x = jumpF_polyR 1 (q*p) x"
proof (cases "p=0 ∨ q=0")
case True
then show ?thesis by auto
next
case False
"jumpF_polyR q p x= jumpF_polyR 1 (q*p) x" when "poly p x=0" "coprime p q" for p q
proof (cases "p=0")
case True
then show ?thesis by auto
next
case False
have "poly q x≠0" using that coprime_poly_0 by blast
then have "q≠0" by auto
moreover have "sign_r_pos p x = (0 < poly q x) ⟷ sign_r_pos (q * p) x"
using sign_r_pos_mult[OF ‹q≠0› ‹p≠0›] sign_r_pos_rec[OF ‹q≠0›] ‹poly q x≠0›
by auto
ultimately show ?thesis using ‹poly p x=0›
unfolding jumpF_polyR_coprime[OF ‹coprime p q›,of x] jumpF_polyR_coprime[of "q*p" 1 x,simplified]
by auto
qed
have False when "poly p x=0" "poly q x=0"
using ‹coprime p q› that coprime_poly_0 by blast
moreover have ?thesis when "poly p x=0" "poly q x≠0"
proof -
have "jumpF_polyR p q x = 0" using jumpF_poly_noroot[OF ‹poly q x≠0›] by auto
then show ?thesis using jumpF_add[OF ‹poly p x=0› ‹coprime p q›] by auto
qed
moreover have ?thesis when "poly p x≠0" "poly q x=0"
proof -
have "jumpF_polyR q p x = 0" using jumpF_poly_noroot[OF ‹poly p x≠0›] by auto
then show ?thesis using jumpF_add[OF ‹poly q x=0›,of p] ‹coprime p q›
qed
moreover have ?thesis when "poly p x≠0" "poly q x≠0"
by (simp add: jumpF_poly_noroot(2) that(1) that(2))
ultimately show ?thesis by auto
qed

assumes "coprime p q"
shows "jumpF_polyL q p x + jumpF_polyL p q x = jumpF_polyL 1 (q*p) x"
proof (cases "p=0 ∨ q=0")
case True
then show ?thesis by auto
next
case False
"jumpF_polyL q p x= jumpF_polyL 1 (q*p) x" when "poly p x=0" "coprime p q" for p q
proof (cases "p=0")
case True
then show ?thesis by auto
next
case False
have "poly q x≠0" using that coprime_poly_0 by blast
then have "q≠0" by auto
moreover have "sign_r_pos p x = (0 < poly q x) ⟷ sign_r_pos (q * p) x"
using sign_r_pos_mult[OF ‹q≠0› ‹p≠0›] sign_r_pos_rec[OF ‹q≠0›] ‹poly q x≠0›
by auto
moreover have "order x p = order x (q * p)"
by (metis ‹poly q x ≠ 0› add_cancel_right_left divisors_zero order_mult order_root)
ultimately show ?thesis using ‹poly p x=0›
unfolding jumpF_polyL_coprime[OF ‹coprime p q›,of x] jumpF_polyL_coprime[of "q*p" 1 x,simplified]
by auto
qed
have False when "poly p x=0" "poly q x=0"
using ‹coprime p q› that coprime_poly_0 by blast
moreover have ?thesis when "poly p x=0" "poly q x≠0"
proof -
have "jumpF_polyL p q x = 0" using jumpF_poly_noroot[OF ‹poly q x≠0›] by auto
then show ?thesis using jumpF_add[OF ‹poly p x=0› ‹coprime p q›] by auto
qed
moreover have ?thesis when "poly p x≠0" "poly q x=0"
proof -
have "jumpF_polyL q p x = 0" using jumpF_poly_noroot[OF ‹poly p x≠0›] by auto
then show ?thesis using jumpF_add[OF ‹poly q x=0›,of p] ‹coprime p q›
qed
moreover have ?thesis when "poly p x≠0" "poly q x≠0"
by (simp add: jumpF_poly_noroot that(1) that(2))
ultimately show ?thesis by auto
qed

lemma jumpF_polyL_smult_1:
"jumpF_polyL (smult c q) p x = sgn c * jumpF_polyL q p x"
proof (cases "c=0")
case True
then show ?thesis by auto
next
case False
then show ?thesis
unfolding jumpF_polyL_def
apply (subst jumpF_times[of "λ_. c",symmetric])
by auto
qed

lemma jumpF_polyR_smult_1:
"jumpF_polyR (smult c q) p x = sgn c * jumpF_polyR q p x"
proof (cases "c=0")
case True
then show ?thesis by auto
next
case False
then show ?thesis
unfolding jumpF_polyR_def using False
apply (subst jumpF_times[of "λ_. c",symmetric])
by auto
qed

lemma
shows jumpF_polyR_mod:"jumpF_polyR q p x = jumpF_polyR (q mod p) p x" and
jumpF_polyL_mod:"jumpF_polyL q p x = jumpF_polyL (q mod p) p x"
proof -
define f where "f=(λx. poly (q div p) x)"
define g where "g=(λx. poly (q mod p) x / poly p x)"
have jumpF_eq:"jumpF (λx. poly q x / poly p x) (at y within S) = jumpF g (at y within S)"
when "p≠0" for y S
proof -
let ?F = "at y within S"
have "∀⇩F x in at y within S. poly p x ≠ 0"
using eventually_poly_nz_at_within[OF ‹p≠0›,of y S] .
then have "eventually (λx. (poly q x / poly p x) = (f x+ g x)) ?F"
proof (rule eventually_mono)
fix x
assume P: "poly p x ≠ 0"
have "poly q x = poly (q div p * p + q mod p) x"
by simp
also have "… = f x * poly p x + poly (q mod p) x"
by (simp only: poly_add poly_mult f_def g_def)
moreover have "poly (q mod p) x = g x * poly p x"
using P by (simp add: g_def)
ultimately show "poly q x / poly p x = f x + g x"
using P by simp
qed
then have "jumpF (λx. poly q x / poly p x) ?F = jumpF (λx. f x+ g x) ?F"
by (intro jumpF_cong,auto)
also have "... = jumpF g ?F"
proof -
have "(f ⤏ f y) (at y within S)"
unfolding f_def by (intro tendsto_intros)
show ?thesis unfolding jumpF_def by auto
qed
finally show ?thesis .
qed
show "jumpF_polyR q p x = jumpF_polyR (q mod p) p x"
apply (cases "p=0")
subgoal by auto
subgoal using jumpF_eq unfolding g_def jumpF_polyR_def by auto
done
show "jumpF_polyL q p x = jumpF_polyL (q mod p) p x"
apply (cases "p=0")
subgoal by auto
subgoal using jumpF_eq unfolding g_def jumpF_polyL_def by auto
done
qed

lemma jumpF_poly_top_0[simp]: "jumpF_poly_top 0 p = 0" "jumpF_poly_top q 0 = 0"
unfolding jumpF_poly_top_def by auto

lemma jumpF_poly_bot_0[simp]: "jumpF_poly_bot 0 p = 0" "jumpF_poly_bot q 0 = 0"
unfolding jumpF_poly_bot_def by auto

lemma jumpF_poly_top_code:
"jumpF_poly_top q p = (if p≠0 ∧ q≠0 ∧ degree q>degree p then
if sgn_pos_inf q * sgn_pos_inf p > 0 then 1/2 else -1/2 else 0)"
proof (cases "p≠0 ∧ q≠0 ∧ degree q>degree p")
case True
have ?thesis when "sgn_pos_inf q * sgn_pos_inf p > 0"
proof -
have "LIM x at_top. poly q x / poly p x :> at_top"
using poly_divide_filterlim_at_top[of p q] True that by auto
then have "jumpF (λx. poly q x / poly p x) at_top = 1/2"
unfolding jumpF_def by auto
then show ?thesis unfolding jumpF_poly_top_def using that True by auto
qed
moreover have ?thesis when "¬ sgn_pos_inf q * sgn_pos_inf p > 0"
proof -
have "LIM x at_top. poly q x / poly p x :> at_bot"
using poly_divide_filterlim_at_top[of p q] True that by auto
then have "jumpF (λx. poly q x / poly p x) at_top = - 1/2"
unfolding jumpF_def by auto
then show ?thesis unfolding jumpF_poly_top_def using that True by auto
qed
ultimately show ?thesis by auto
next
case False
define P where "P= (¬ (LIM x at_top. poly q x / poly p x :> at_bot)
∧ ¬ (LIM x at_top. poly q x / poly p x :> at_top))"
have P when "p=0 ∨ q=0"
unfolding P_def using that
by (auto elim!:filterlim_at_bot_nhds filterlim_at_top_nhds)
moreover have P when "p≠0" "q≠0" "degree p> degree q"
proof -
have "LIM x at_top. poly q x / poly p x :> at 0"
using poly_divide_filterlim_at_top[OF that(1,2)] that(3) by auto
then show ?thesis unfolding P_def
by (auto elim!:filterlim_at_bot_nhds filterlim_at_top_nhds simp:filterlim_at)
qed
moreover have P when "p≠0" "q≠0" "degree p = degree q"
proof -
have "((λx. poly q x / poly p x) ⤏ lead_coeff q / lead_coeff p) at_top"
using poly_divide_filterlim_at_top[OF that(1,2)] using that by auto
then show ?thesis unfolding P_def
by (auto elim!:filterlim_at_bot_nhds filterlim_at_top_nhds)
qed
ultimately have P using False by fastforce
then have "jumpF (λx. poly q x / poly p x) at_top = 0"
unfolding jumpF_def P_def by auto
then show ?thesis unfolding jumpF_poly_top_def using False by presburger
qed

lemma jumpF_poly_bot_code:
"jumpF_poly_bot q p = (if p≠0 ∧ q≠0 ∧ degree q>degree p then
if sgn_neg_inf q * sgn_neg_inf p > 0 then 1/2 else -1/2 else 0)"
proof (cases "p≠0 ∧ q≠0 ∧ degree q>degree p")
case True
have ?thesis when "sgn_neg_inf q * sgn_neg_inf p > 0"
proof -
have "LIM x at_bot. poly q x / poly p x :> at_top"
using poly_divide_filterlim_at_bot[of p q] True that by auto
then have "jumpF (λx. poly q x / poly p x) at_bot = 1/2"
unfolding jumpF_def by auto
then show ?thesis unfolding jumpF_poly_bot_def using that True by auto
qed
moreover have ?thesis when "¬ sgn_neg_inf q * sgn_neg_inf p > 0"
proof -
have "LIM x at_bot. poly q x / poly p x :> at_bot"
using poly_divide_filterlim_at_bot[of p q] True that by auto
then have "jumpF (λx. poly q x / poly p x) at_bot = - 1/2"
unfolding jumpF_def by auto
then show ?thesis unfolding jumpF_poly_bot_def using that True by auto
qed
ultimately show ?thesis by auto
next
case False
define P where "P= (¬ (LIM x at_bot. poly q x / poly p x :> at_bot)
∧ ¬ (LIM x at_bot. poly q x / poly p x :> at_top))"
have P when "p=0 ∨ q=0"
unfolding P_def using that
by (auto elim!:filterlim_at_bot_nhds filterlim_at_top_nhds)
moreover have P when "p≠0" "q≠0" "degree p> degree q"
proof -
have "LIM x at_bot. poly q x / poly p x :> at 0"
using poly_divide_filterlim_at_bot[OF that(1,2)] that(3) by auto
then show ?thesis unfolding P_def
by (auto elim!:filterlim_at_bot_nhds filterlim_at_top_nhds simp:filterlim_at)
qed
moreover have P when "p≠0" "q≠0" "degree p = degree q"
proof -
have "((λx. poly q x / poly p x) ⤏ lead_coeff q / lead_coeff p) at_bot"
using poly_divide_filterlim_at_bot[OF that(1,2)] using that by auto
then show ?thesis unfolding P_def
by (auto elim!:filterlim_at_bot_nhds filterlim_at_top_nhds)
qed
ultimately have P using False by fastforce
then have "jumpF (λx. poly q x / poly p x) at_bot = 0"
unfolding jumpF_def P_def by auto
then show ?thesis unfolding jumpF_poly_bot_def using False by presburger
qed

subsection ‹The extended Cauchy index on polynomials›

definition cindex_polyE:: "real ⇒ real ⇒ real poly ⇒ real poly ⇒ real" where
"cindex_polyE a b q p = jumpF_polyR q p a + cindex_poly a b q p - jumpF_polyL q p b"

definition cindex_poly_ubd::"real poly ⇒ real poly ⇒ int" where
"cindex_poly_ubd q p = (THE l. (∀⇩F r in at_top. cindexE (-r) r (λx. poly q x/poly p x) = of_int l))"

lemma cindex_polyE_0[simp]: "cindex_polyE a b 0 p = 0" "cindex_polyE a b q 0 = 0"
unfolding cindex_polyE_def by auto

lemma cindex_polyE_mult_cancel:
fixes p q p'::"real poly"
assumes "p'≠ 0"
shows "cindex_polyE a b (p' * q ) (p' * p) = cindex_polyE a b q p"
unfolding cindex_polyE_def
using cindex_poly_mult[OF ‹p'≠0›] jumpF_polyL_mult_cancel[OF ‹p'≠0›]
jumpF_polyR_mult_cancel[OF ‹p'≠0›]
by simp

lemma cindexE_eq_cindex_polyE:
assumes "a<b"
shows "cindexE a b (λx. poly q x/poly p x) = cindex_polyE a b q p"
proof (cases "p=0 ∨ q=0")
case True
then show ?thesis by (auto simp add: cindexE_constI)
next
case False
then have "p≠0" "q≠0" by auto
define g where "g=gcd p q"
define p' q' where "p'=p div g" and "q' = q div g"
define f' where "f'=(λx. poly q' x / poly p' x)"
have "g≠0" using False g_def by auto
have pq_f:"p=g*p'" "q=g*q'" and "coprime p' q'"
unfolding g_def p'_def q'_def
apply simp_all
using False div_gcd_coprime by blast
have "cindexE a b (λx. poly q x/poly p x) = cindexE a b (λx. poly q' x/poly p' x)"
proof -
define f where "f=(λx. poly q x / poly p x)"
define f' where "f'=(λx. poly q' x / poly p' x)"
have "jumpF f (at_right x) = jumpF f' (at_right x)" for x
proof (rule jumpF_cong)
obtain ub where "x < ub" "∀z. x < z ∧ z ≤ ub ⟶ poly g z ≠ 0"
using next_non_root_interval[OF ‹g≠0›,of x] by auto
then show "∀⇩F x in at_right x. f x = f' x"
unfolding eventually_at_right f_def f'_def pq_f
apply (intro exI[where x=ub])
by auto
qed simp
moreover have "jumpF f (at_left x) = jumpF f' (at_left x)" for x
proof (rule jumpF_cong)
obtain lb where "lb < x" "∀z. lb ≤ z ∧ z < x ⟶ poly g z ≠ 0 "
using last_non_root_interval[OF ‹g≠0›,of x] by auto
then show "∀⇩F x in at_left x. f x = f' x"
unfolding eventually_at_left f_def f'_def pq_f
apply (intro exI[where x=lb])
by auto
qed simp
ultimately show ?thesis unfolding cindexE_def
apply (fold f_def f'_def)
by auto
qed
also have "... = jumpF f' (at_right a) + real_of_int (cindex a b f') - jumpF f' (at_left b)"
unfolding f'_def
apply (rule cindex_eq_cindexE_divide)
subgoal using ‹a<b› .
subgoal using False poly_roots_finite pq_f(1) pq_f(2) by fastforce
subgoal using ‹coprime p' q'› poly_gcd_iff by force
subgoal by (auto intro:continuous_intros)
subgoal by (auto intro:continuous_intros)
done
also have "... = cindex_polyE a b q' p'"
using cindex_eq_cindex_poly unfolding cindex_polyE_def jumpF_polyR_def jumpF_polyL_def f'_def
by auto
also have "... = cindex_polyE a b q p"
using cindex_polyE_mult_cancel[OF ‹g≠0›] unfolding pq_f by auto
finally show ?thesis .
qed

lemma cindex_polyE_cross:
fixes p::"real poly" and a b::real
assumes "a<b"
shows "cindex_polyE a b 1 p = cross_alt 1 p a b / 2"
proof (induct "degree p" arbitrary:p rule:nat_less_induct)
case induct:1
have ?case when "p=0"
using that unfolding cross_alt_def by auto
moreover have ?case when "p≠0" and noroot:"{x.  a< x∧ x< b ∧ poly p x=0 } = {}"
proof -
have "cindex_polyE a b 1 p = jumpF_polyR 1 p a  - jumpF_polyL 1 p b"
proof -
have "cindex_poly a b 1 p = 0" unfolding cindex_poly_def
apply (rule sum.neutral)
using that by auto
then show ?thesis unfolding cindex_polyE_def by auto
qed
also have "... = cross_alt 1 p a b / 2"
proof -
define f where "f = (λx. 1 / poly p x)"
define ja where "ja = jumpF f (at_right a)"
define jb where "jb = jumpF f (at_left b)"
define right where "right = (λR. R ja (0::real) ∨ (continuous (at_right a) f ∧ R (poly p a) 0))"
define left where "left = (λR. R jb (0::real) ∨ (continuous (at_left b) f ∧ R (poly p b) 0))"

note ja_alt=jumpF_polyR_coprime[of p 1 a,unfolded jumpF_polyR_def,simplified,folded f_def ja_def]
note jb_alt=jumpF_polyL_coprime[of p 1 b,unfolded jumpF_polyL_def,simplified,folded f_def jb_def]

have [simp]:"0 < ja ⟷ jumpF_polyR 1 p a = 1/2" "0 > ja ⟷ jumpF_polyR 1 p a = -1/2"
"0 < jb ⟷ jumpF_polyL 1 p b = 1/2" "0 > jb ⟷ jumpF_polyL 1 p b = -1/2"
unfolding ja_def jb_def jumpF_polyR_def jumpF_polyL_def f_def jumpF_def
by auto
have [simp]:
"poly p a ≠0 ⟹ continuous (at_right a) f"
"poly p b ≠0 ⟹ continuous (at_left b) f"
unfolding f_def by (auto intro!: continuous_intros )
have not_right_left: False when "(right greater ∧ left less ∨ right less ∧ left greater)"
proof -
have [simp]: "f a > 0 ⟷ poly p a > 0" "f a < 0 ⟷ poly p a < 0"
"f b > 0 ⟷ poly p b > 0" "f b < 0 ⟷ poly p b < 0"
unfolding f_def by auto
have "continuous_on {a<..<b} f"
unfolding f_def using noroot by (auto intro!: continuous_intros)
then have "∃x>a. x < b ∧ f x = 0"
apply (elim jumpF_IVT[OF ‹a<b›,of f])
using that unfolding right_def left_def by (fold ja_def jb_def,auto)
then show False using noroot using f_def by auto
qed
have ?thesis when "poly p a>0 ∧ poly p b>0 ∨ poly p a<0 ∧ poly p b<0"
using that jumpF_poly_noroot unfolding cross_alt_def by auto
moreover have False when "poly p a>0 ∧ poly p b<0 ∨ poly p a<0 ∧ poly p b>0"
apply (rule not_right_left)
unfolding right_def left_def using that by auto
moreover have ?thesis when "poly p a=0" "poly p b>0 ∨ poly p b <0"
proof -
have "ja>0 ∨ ja < 0" using ja_alt ‹p≠0› ‹poly p a=0› by argo
moreover have False when "ja > 0 ∧ poly p b<0 ∨ ja < 0 ∧ poly p b>0"
apply (rule not_right_left)
unfolding right_def left_def using that by fastforce
moreover have ?thesis when "ja >0 ∧ poly p b>0 ∨ ja < 0 ∧ poly p b<0"
using that jumpF_poly_noroot ‹poly p a=0› unfolding cross_alt_def by auto
ultimately show ?thesis using that jumpF_poly_noroot unfolding cross_alt_def by auto
qed
moreover have ?thesis when "poly p b=0" "poly p a>0 ∨ poly p a <0"
proof -
have "jb>0 ∨ jb < 0" using jb_alt ‹p≠0› ‹poly p b=0› by argo
moreover have False when "jb > 0 ∧ poly p a<0 ∨ jb < 0 ∧ poly p a>0"
apply (rule not_right_left)
unfolding right_def left_def using that by fastforce
moreover have ?thesis when "jb >0 ∧ poly p a>0 ∨ jb < 0 ∧ poly p a<0"
using that jumpF_poly_noroot ‹poly p b=0› unfolding cross_alt_def by auto
ultimately show ?thesis using that jumpF_poly_noroot unfolding cross_alt_def by auto
qed
moreover have ?thesis when "poly p a=0" "poly p b=0"
proof -
have "jb>0 ∨ jb < 0" using jb_alt ‹p≠0› ‹poly p b=0› by argo
moreover have "ja>0 ∨ ja < 0" using ja_alt ‹p≠0› ‹poly p a=0› by argo
moreover have False when "ja>0 ∧ jb<0 ∨ ja<0 ∧ jb>0"
apply (rule not_right_left)
unfolding right_def left_def using that by fastforce
moreover have ?thesis when "ja>0 ∧ jb>0 ∨ ja<0 ∧ jb<0"
using that jumpF_poly_noroot ‹poly p b=0› ‹poly p a=0›
unfolding cross_alt_def by auto
ultimately show ?thesis by blast
qed
ultimately show ?thesis by argo
qed
finally show ?thesis .
qed
moreover have ?case when "p≠0" and no_empty:"{x.  a< x∧ x< b ∧ poly p x=0 } ≠ {}"
proof -
define roots where "roots≡{x.  a< x∧ x< b ∧ poly p x=0 }"
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›] no_empty  unfolding roots_def by auto
define max_rp where "max_rp≡[:-max_r,1:]^order max_r p"
then obtain p' where p'_def:"p=p'*max_rp" and "¬ [:-max_r,1:] dvd p'"
by (metis ‹p≠0› mult.commute order_decomp)
hence "p'≠0" and "max_rp≠0" and max_r_nz:"poly p' max_r≠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› by (auto simp add: dvd_iff_poly_eq_0)

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 "cindex_polyE a b 1 p = jumpF_polyR 1 p a + (∑x∈roots. jump_poly 1 p x) - jumpF_polyL 1 p b"
unfolding cindex_polyE_def cindex_poly_def roots_def by (simp,meson)
also have "... = max_r_sign * cindex_poly a b 1 p' + jump_poly 1 p max_r
+ max_r_sign * jumpF_polyR 1 p' a - jumpF_polyL 1 p' b"
proof -
have "(∑x∈roots. jump_poly 1 p x) = max_r_sign * cindex_poly a b 1 p' + jump_poly 1 p max_r"
proof -
have "(∑x∈roots. jump_poly 1 p x)= (∑x∈roots'. jump_poly 1 p x)+ jump_poly 1 p max_r"
proof -
have "roots = insert max_r roots'"
unfolding roots_def roots'_def p'_def
using ‹poly p max_r=0› ‹a<max_r› ‹max_r<b› ‹p≠0› order_root
apply (subst max_rp_def)
by auto
moreover have "finite roots'"
unfolding roots'_def using poly_roots_finite[OF ‹p'≠0›] by auto
moreover have "max_r ∉ roots'"
unfolding roots'_def using max_r_nz
by auto
ultimately show ?thesis using sum.insert[of roots' max_r] by auto
qed
moreover have "(∑x∈roots'. jump_poly 1 p x) = max_r_sign * cindex_poly a b 1 p'"
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 max_r_nz unfolding roots'_def
by auto
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'_def 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'_def
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 * cindex_poly a b 1 p'"
unfolding cindex_poly_def roots'_def by meson
finally show ?thesis .
qed
ultimately show ?thesis by simp
qed
moreover have "jumpF_polyR 1 p a = max_r_sign * jumpF_polyR 1 p' a"
proof -
define f where "f = (λx. 1 / poly max_rp x)"
define g where "g = (λx. 1 / poly p' x)"
have "jumpF_polyR 1 p a = jumpF (λx. f x * g x) (at_right a)"
unfolding jumpF_polyR_def f_def g_def p'_def
also have "... = sgn (f a) * jumpF g (at_right a)"
proof (rule jumpF_times)
have [simp]: "poly max_rp a ≠0"
unfolding max_rp_def using ‹max_r>a› by auto
show "(f ⤏ f a) (at_right a)" "f a ≠ 0"
unfolding f_def by (auto intro:tendsto_intros)
qed auto
also have "... = max_r_sign * jumpF_polyR 1 p' a"
proof -
have "sgn (f a) = max_r_sign"
unfolding max_r_sign_def f_def max_rp_def using ‹a<max_r›
then show ?thesis unfolding jumpF_polyR_def g_def by auto
qed
finally show ?thesis .
qed
moreover have "jumpF_polyL 1 p b =  jumpF_polyL 1 p' b"
proof -
define f where "f = (λx. 1 / poly max_rp x)"
define g where "g = (λx. 1 / poly p' x)"
have "jumpF_polyL 1 p b = jumpF (λx. f x * g x) (at_left b)"
unfolding jumpF_polyL_def f_def g_def p'_def
also have "... = sgn (f b) * jumpF g (at_left b)"
proof (rule jumpF_times)
have [simp]: "poly max_rp b ≠0"
unfolding max_rp_def using ‹max_r<b› by auto
show "(f ⤏ f b) (at_left b)" "f b ≠ 0"
unfolding f_def by (auto intro:tendsto_intros)
qed auto
also have "... = jumpF_polyL 1 p' b"
proof -
have "sgn (f b) = 1"
unfolding max_r_sign_def f_def max_rp_def using ‹b>max_r›
then show ?thesis unfolding jumpF_polyL_def g_def by auto
qed
finally show ?thesis .
qed
ultimately show ?thesis by auto
qed
also have "... = max_r_sign * cindex_polyE a b 1 p' + jump_poly 1 p max_r
+ (max_r_sign - 1) * jumpF_polyL 1 p' b"
unfolding cindex_polyE_def roots'_def by (auto simp add:algebra_simps)
also have "... = max_r_sign * cross_alt 1 p' a b / 2 + jump_poly 1 p max_r
+ (max_r_sign - 1) * jumpF_polyL 1 p' b"
proof -
have "degree max_rp>0" unfolding max_rp_def degree_linear_power
using ‹poly p max_r=0› order_root ‹p≠0› by blast
then have "degree p'<degree p" unfolding p'_def
using degree_mult_eq[OF ‹p'≠0› ‹max_rp≠0›] by auto
from induct[rule_format, OF this]
have "cindex_polyE a b 1 p' = real_of_int (cross_alt 1 p' a b) / 2" by auto
then show ?thesis by auto
qed
also have "... = real_of_int (cross_alt 1 p a b) / 2"
proof -
have sjump_p:"jump_poly 1 p max_r = (if odd (order max_r p) then sign (poly p' max_r) else 0)"
proof -
note max_r_nz
moreover then have "poly max_rp max_r=0"
using ‹poly p max_r = 0› p'_def by auto
ultimately have "jump_poly 1 p max_r = sign (poly p' max_r) * jump_poly 1 max_rp max_r"
unfolding p'_def using jump_poly_1_mult[of p' max_r max_rp]
by auto
also have "... = (if odd (order max_r max_rp) then sign (poly p' max_r) else 0)"
proof -
have "sign_r_pos max_rp max_r"
unfolding max_rp_def using sign_r_pos_power by auto
then show ?thesis using ‹max_rp≠0› unfolding jump_poly_def by auto
qed
also have "... = (if odd (order max_r p) then sign (poly p' max_r) else 0)"
proof -
have "order max_r p'=0" by (simp add: ‹poly p' max_r ≠ 0› order_0I)
then have "order max_r max_rp = order max_r p"
unfolding p'_def using ‹p'≠0› ‹max_rp≠0›
apply (subst order_mult)
by auto
then show ?thesis by auto
qed
finally show ?thesis .
qed
have ?thesis when "even (order max_r p)"
proof -
have "sign (poly p x) =  sign (poly p' x)" when "x≠max_r" for x
proof -
have "sign (poly max_rp x) = 1"
unfolding max_rp_def using ‹even (order max_r p)› that
then show ?thesis unfolding p'_def by (simp add:sign_times)
qed
from this[of a] this[of b] ‹a<max_r› ‹max_r<b›
have "cross_alt 1 p' a b = cross_alt 1 p a b"
unfolding cross_alt_def by auto
then show ?thesis using that unfolding max_r_sign_def sjump_p by auto
qed
moreover have ?thesis when "odd (order max_r p)"
proof -
let ?thesis2 = "sign (poly p' max_r) * 2 - cross_alt 1 p' a b - 4 * jumpF_polyL 1 p' b
= cross_alt 1 p a b"
have ?thesis2 when "poly p' b=0"
proof -
have "jumpF_polyL 1 p' b = 1/2 ∨ jumpF_polyL 1 p' b=-1/2"
using jumpF_polyL_coprime[of p' 1 b,simplified] ‹p'≠0› ‹poly p' b=0› by auto
moreover have "poly p' max_r>0 ∨ poly p' max_r<0"
using max_r_nz by auto
moreover have False when "poly p' max_r>0 ∧ jumpF_polyL 1 p' b=-1/2
∨ poly p' max_r<0 ∧ jumpF_polyL 1 p' b=1/2"
proof -
define f where "f= (λx. 1/ poly p' x)"
have noroots:"poly p' x≠0" when "x∈{max_r<..<b}" for x
proof (rule ccontr)
assume " ¬ poly p' x ≠ 0"
then have "poly p x =0" unfolding p'_def by auto
then have "x∈roots" unfolding roots_def using that ‹a<max_r› by auto
then have "x≤max_r" using Max_ge[OF ‹finite roots›] unfolding max_r_def by auto
moreover have "x>max_r" using that by auto
ultimately show False by auto
qed
have "continuous_on {max_r<..<b} f"
unfolding f_def using noroots by (auto intro!:continuous_intros)
moreover have "continuous (at_right max_r) f"
unfolding f_def using max_r_nz
by (auto intro!:continuous_intros)
moreover have "f max_r>0 ∧ jumpF f (at_left b)<0
∨ f max_r<0 ∧ jumpF f (at_left b)>0"
using that unfolding f_def jumpF_polyL_def by auto
ultimately have "∃x>max_r. x < b ∧ f x = 0"
apply (intro jumpF_IVT[OF ‹max_r<b›])
by auto
then show False using noroots unfolding f_def by auto
qed
moreover have ?thesis when "poly p' max_r>0 ∧ jumpF_polyL 1 p' b=1/2
∨ poly p' max_r<0 ∧ jumpF_polyL 1 p' b=-1/2"
proof -
have "poly max_rp a < 0" "poly max_rp b>0"
unfolding max_rp_def using ‹odd (order max_r p)› ‹a<max_r› ‹max_r<b›
then have "cross_alt 1 p a b = - cross_alt 1 p' a b"
unfolding cross_alt_def p'_def using ‹poly p' b=0›
with that show ?thesis by auto
qed
ultimately show ?thesis by blast
qed
moreover have ?thesis2 when "poly p' b≠0"
proof -
have [simp]:"jumpF_polyL 1 p' b = 0"
using jumpF_polyL_coprime[of p' 1 b,simplified] ‹poly p' b≠0› by auto
have [simp]:"poly max_rp a < 0" "poly max_rp b>0"
unfolding max_rp_def using ‹odd (order max_r p)› ‹a<max_r› ‹max_r<b›
have "poly p' b>0 ∨ poly p' b<0"
using ‹poly p' b≠0› by auto
moreover have "poly p' max_r>0 ∨ poly p' max_r<0"
using max_r_nz by auto
moreover have ?thesis when "poly p' b>0 ∧ poly p' max_r>0 "
using that unfolding cross_alt_def p'_def
moreover have ?thesis when "poly p' b<0 ∧ poly p' max_r<0"
using that unfolding cross_alt_def p'_def
moreover have False when "poly p' b>0 ∧ poly p' max_r<0 ∨ poly p' b<0 ∧ poly p' max_r>0"
proof -
have "∃x>max_r. x < b ∧ poly p' x = 0"
apply (rule poly_IVT[OF ‹max_r<b›,of p'])
using that mult_less_0_iff by blast
then obtain x where "max_r<x" "x<b" "poly p x=0" unfolding p'_def by auto
then have "x∈roots" using ‹a<max_r› unfolding roots_def by auto
then have "x≤max_r" unfolding max_r_def using Max_ge[OF ‹finite roots›] by auto
then show False using ‹max_r<x› by auto
qed
ultimately show ?thesis by blast
qed
ultimately have ?thesis2 by auto
then show ?thesis unfolding max_r_sign_def sjump_p using that by simp
qed
ultimately show ?thesis by auto
qed
finally show ?thesis .
qed
ultimately show ?case by fast
qed

fixes p q::"real poly"
assumes cp:"coprime p q"
shows "cindex_polyE a b q p + cindex_polyE a b p q=cindex_polyE a b 1 (q*p)"
unfolding cindex_polyE_def
by auto

fixes p q::"real poly"
assumes "a < b" "coprime p q"
shows "cindex_polyE a b q p  + cindex_polyE a b p q = cross_alt p q a b / 2"
apply (subst cindex_polyE_inverse_add[OF ‹coprime p q›])
apply (subst cindex_polyE_cross[OF ‹a<b›])
apply (subst mult.commute)
apply (subst cross_alt_clear_n[OF ‹coprime p q›])
by simp

lemma cindex_polyE_smult_1:
fixes p q::"real poly" and c::real
shows "cindex_polyE a b (smult c q) p =  (sgn c) * cindex_polyE a b q p"
unfolding cindex_polyE_def jumpF_polyL_smult_1 jumpF_polyR_smult_1 cindex_poly_smult_1

lemma cindex_polyE_mod:
fixes p q::"real poly"
shows "cindex_polyE a b q p =  cindex_polyE a b (q mod p) p"
unfolding cindex_polyE_def
apply (subst cindex_poly_mod)
apply (subst jumpF_polyR_mod)
apply (subst jumpF_polyL_mod)
by simp

lemma cindex_polyE_rec:
fixes p q::"real poly"
assumes "a < b" "coprime p q"
shows "cindex_polyE a b q p  = cross_alt q p a b/2  +  cindex_polyE a b (- (p mod q)) q"
proof -
moreover have "cindex_polyE a b (- (p mod q)) q = - cindex_polyE a b p q"
using cindex_polyE_mod cindex_polyE_smult_1[of a b "-1"]
by auto
ultimately show ?thesis by (auto simp add:field_simps cross_alt_poly_commute)
qed

lemma cindex_polyE_changes_alt_itv_mods:
assumes "a<b" "coprime p q"
shows "cindex_polyE a b q p = changes_alt_itv_smods a b p q / 2" using ‹coprime p q›
proof (induct "smods p q" arbitrary:p q)
case Nil
then have "p=0" by (metis smods_nil_eq)
then show ?case by (simp add:changes_alt_itv_smods_def changes_alt_poly_at_def)
next
case (Cons x xs)
then have "p≠0" by auto
have ?case when "q=0"
using that by (simp add:changes_alt_itv_smods_def changes_alt_poly_at_def)
moreover have ?case when "q≠0"
proof -
define r where "r≡- (p mod q)"
obtain ps where ps:"smods p q=p#q#ps" "smods q r=q#ps" and "xs=q#ps"
unfolding r_def using ‹q≠0› ‹p≠0› ‹x # xs = smods p q›
by (metis list.inject smods.simps)
from Cons.prems ‹q ≠ 0› have "coprime q r"
then have "cindex_polyE a b r q = real_of_int (changes_alt_itv_smods a b q r) / 2"
apply (rule_tac Cons.hyps(1))
using ps ‹xs=q#ps› by simp_all
moreover have "changes_alt_itv_smods a b p q = cross_alt p q a b + changes_alt_itv_smods a b q r"
using changes_alt_itv_smods_rec[OF ‹a<b› ‹coprime p q›,folded r_def] .
moreover have "cindex_polyE a b q p = real_of_int (cross_alt q p a b) / 2 + cindex_polyE a b r q"
using cindex_polyE_rec[OF ‹a<b› ‹coprime p q›,folded r_def] .
ultimately show ?case
qed
ultimately show ?case by blast
qed

lemma cindex_poly_ubd_eventually:
shows "∀⇩F r in at_top. cindexE (-r) r (λx. poly q x/poly p x) = of_int (cindex_poly_ubd q p)"
proof -
define f where "f=(λx. poly q x/poly p x)"
obtain R where R_def: "R>0" "proots p ⊆ {-R<..<R}"
if "p≠0"
proof (cases "p=0")
case True
then show ?thesis using that[of 1] by auto
next
case False
then have "finite (proots p)" by auto
from finite_ball_include[OF this,of 0]
obtain r where "r>0" and r_ball:"proots p ⊆ ball 0 r"
by auto
have "proots p ⊆ {-r<..<r}"
proof
fix x assume "x ∈ proots p"
then have "x∈ball 0 r" using r_ball by auto
then have "abs x<r" using mem_ball_0 by auto
then show "x ∈ {- r<..<r}" using ‹r>0› by auto
qed
then show ?thesis using that[of r] False ‹r>0› by auto
qed
define l where "l=(if p=0  then 0 else cindex_poly (-R) R q p)"
define P where "P=(λl. (∀⇩F r in at_top. cindexE (-r) r f = of_int l))"
have "P l "
proof (cases "p=0 ")
case True
then show ?thesis
unfolding P_def f_def l_def using True
by (auto intro!: eventuallyI cindexE_constI)
next
case False
have "P l" unfolding P_def
proof (rule eventually_at_top_linorderI[of R])
fix r assume "R ≤ r"
then have "cindexE (- r) r f =  cindex_polyE (-r) r q p"
unfolding f_def using R_def[OF ‹p≠0›] by (auto intro: cindexE_eq_cindex_polyE)
also have "... = of_int (cindex_poly (- r) r q p)"
proof -
have "jumpF_polyR q p (- r) = 0"
apply (rule jumpF_poly_noroot)
using ‹R≤r› R_def[OF ‹p≠0›] by auto
moreover have "jumpF_polyL q p r = 0"
apply (rule jumpF_poly_noroot)
using ‹R≤r› R_def[OF ‹p≠0›] by auto
ultimately show ?thesis unfolding cindex_polyE_def by auto
qed
also have "... = of_int (cindex_poly (- R) R q p)"
proof -
define rs where "rs={x. poly p x = 0 ∧ - r < x ∧ x < r}"
define Rs where "Rs={x. poly p x = 0 ∧ - R < x ∧ x < R}"
have "rs=Rs"
using R_def[OF ‹p≠0›] ‹R≤r› unfolding rs_def Rs_def by force
then show ?thesis
unfolding cindex_poly_def by (fold rs_def Rs_def,auto)
qed
also have "... = of_int l" unfolding l_def using False by auto
finally show "cindexE (- r) r f = real_of_int l" .
qed
then show ?thesis unfolding P_def by auto
qed
moreover have "x=l" when "P x" for x
proof -
have "∀⇩F r in at_top. cindexE (- r) r f = real_of_int x"
"∀⇩F r in at_top. cindexE (- r) r f = real_of_int l"
using ‹P x› ‹P l› unfolding P_def by auto
from eventually_conj[OF this]
have "∀⇩F r::real in at_top. real_of_int x = real_of_int l"
by (elim eventually_mono,auto)
then have "real_of_int x = real_of_int l" by auto
then show ?thesis by simp
qed
ultimately have "P (THE x. P x)" using theI[of P l] by blast
then show ?thesis unfolding P_def f_def cindex_poly_ubd_def by auto
qed

lemma cindex_poly_ubd_0:
assumes "p=0 ∨ q=0"
shows "cindex_poly_ubd q p = 0"
proof -
have "∀⇩F r in at_top. cindexE (-r) r (λx. poly q x/poly p x) = 0"
apply (rule eventuallyI)
using assms by (auto intro:cindexE_constI)
from eventually_conj[OF this cindex_poly_ubd_eventually[of q p]]
have "∀⇩F r::real in at_top.  (cindex_poly_ubd q p) = (0::int)"
apply (elim eventually_mono)
by auto
then show ?thesis by auto
qed

lemma cindex_poly_ubd_code:
shows "cindex_poly_ubd q p = changes_R_smods p q"
proof (cases "p=0")
case True
then show ?thesis using cindex_poly_ubd_0 by auto
next
case False
define ps where "ps≡smods p q"
have "p∈set ps" using ps_def ‹p≠0› by auto
obtain lb where lb:"∀p∈set ps. ∀x. poly p x=0 ⟶ x>lb"
and lb_sgn:"∀x≤lb. ∀p∈set ps. sgn (poly p x) = sgn_neg_inf p"
and "lb<0"
using root_list_lb[OF no_0_in_smods,of p q,folded ps_def]
by auto
obtain ub where ub:"∀p∈set ps. ∀x. poly p x=0 ⟶ x<ub"
and ub_sgn:"∀x≥ub. ∀p∈set ps. sgn (poly p x) = sgn_pos_inf p"
and "ub>0"
using root_list_ub[OF no_0_in_smods,of p q,folded ps_def]
by auto
define f where "f=(λt. poly q t/ poly p t)"
define P where "P=(λl. (∀⇩F r in at_top. cindexE (-r) r f = of_int l))"
have "P (changes_R_smods p q)" unfolding P_def
proof (rule eventually_at_top_linorderI[of "max ¦lb¦ ¦ub¦ + 1"])
fix r assume r_asm:"r≥max ¦lb¦ ¦ub¦ + 1"
have "cindexE (- r) r f =  cindex_polyE (-r) r q p"
unfolding f_def using r_asm by (auto intro: cindexE_eq_cindex_polyE)
also have "... = of_int (cindex_poly (- r) r q p)"
proof -
have "jumpF_polyR q p (- r) = 0"
apply (rule jumpF_poly_noroot)
using r_asm lb[rule_format,OF ‹p∈set ps›,of "-r"] by linarith
moreover have "jumpF_polyL q p r = 0"
apply (rule jumpF_poly_noroot)
using r_asm ub[rule_format,OF ‹p∈set ps›,of "r"] by linarith
ultimately show ?thesis unfolding cindex_polyE_def by auto
qed
also have "... = of_int (changes_itv_smods (- r) r p q)"
apply (rule cindex_poly_changes_itv_mods[THEN arg_cong])
using r_asm lb[rule_format,OF ‹p∈set ps›,of "-r"] ub[rule_format,OF ‹p∈set ps›,of "r"]
by linarith+
also have "... = of_int (changes_R_smods p q)"
proof -
have "map (sgn ∘ (λp. poly p (-r))) ps = map sgn_neg_inf ps"
and "map (sgn ∘ (λp. poly p r)) ps = map sgn_pos_inf ps"
using lb_sgn[THEN spec,of "-r",simplified] ub_sgn[THEN spec,of r,simplified] r_asm
by auto
hence "changes_poly_at ps (-r)=changes_poly_neg_inf ps
∧ changes_poly_at ps r=changes_poly_pos_inf ps"
unfolding changes_poly_neg_inf_def changes_poly_at_def changes_poly_pos_inf_def
by (subst (1 3)  changes_map_sgn_eq,metis map_map)
thus ?thesis unfolding changes_R_smods_def changes_itv_smods_def ps_def
by metis
qed
finally show "cindexE (- r) r f =  of_int (changes_R_smods p q)" .
qed
moreover have "x = changes_R_smods p q" when "P x" for x
proof -
have "∀⇩F r in at_top. cindexE (- r) r f = real_of_int (changes_R_smods p q)"
"∀⇩F r in at_top. cindexE (- r) r f = real_of_int x"
using ‹P (changes_R_smods p q)› ‹P x› unfolding P_def by auto
from eventually_conj[OF this]
have "∀⇩F (r::real) in at_top. of_int x = of_int (changes_R_smods p q)"
by (elim eventually_mono,auto)
then have "of_int x = of_int (changes_R_smods p q)"
using eventually_const_iff by auto
then show ?thesis using of_int_eq_iff by blast
qed
ultimately have "(THE x. P x) = changes_R_smods p q"
using the_equality[of P "changes_R_smods p q"] by blast
then show ?thesis unfolding cindex_poly_ubd_def P_def f_def by auto
qed

lemma cindexE_ubd_poly: "cindexE_ubd (λx. poly q x/poly p x) = cindex_poly_ubd q p"
proof (cases "p=0")
case True
then show ?thesis using cindex_poly_ubd_0 unfolding cindexE_ubd_def
by auto
next
case False
define mx mn where "mx = Max {x. poly p x = 0}" and "mn = Min {x. poly p x=0}"
define rr where "rr= 1+ (max ¦mx¦ ¦mn¦)"
have rr:"-rr < x ∧ x< rr" when "poly p x = 0 " for x
proof -
have "finite {x. poly p x = 0}" using ‹p≠0› poly_roots_finite by blast
then have "mn ≤ x" "x≤mx"
using Max_ge Min_le that unfolding mn_def mx_def by simp_all
then show ?thesis unfolding rr_def by auto
qed
define f where "f=(λx. poly q x / poly p x)"
have "∀⇩F r in at_top. cindexE (- r) r f = cindexE_ubd f"
proof (rule eventually_at_top_linorderI[of rr])
fix r assume "r≥rr"
define R1 R2 where "R1={x. jumpF f (at_right x) ≠ 0 ∧ - r ≤ x ∧ x < r}"
and "R2 = {x. jumpF f (at_right x) ≠ 0}"
define L1 L2 where "L1={x. jumpF f (at_left x) ≠ 0 ∧ - r < x ∧ x ≤ r}"
and "L2={x. jumpF f (at_left x) ≠ 0}"
have "R1=R2"
proof -
have "jumpF f (at_right x) = 0" when "¬ (- r ≤ x ∧ x < r)" for x
proof -
have "jumpF f (at_right x) = jumpF_polyR q p x"
unfolding f_def jumpF_polyR_def by simp
also have "... = 0"
apply (rule jumpF_poly_noroot)
using  that ‹r≥rr› by (auto dest:rr)
finally show ?thesis .
qed
then show ?thesis unfolding R1_def R2_def by blast
qed
moreover have "L1=L2"
proof -
have "jumpF f (at_left x) = 0" when "¬ (- r < x ∧ x ≤ r)" for x
proof -
have "jumpF f (at_left x) = jumpF_polyL q p x"
unfolding f_def jumpF_polyL_def by simp
also have "... = 0"
apply (rule jumpF_poly_noroot)
using that ‹r≥rr› by (auto dest:rr)
finally show ?thesis .
qed
then show ?thesis unfolding L1_def L2_def by blast
qed
ultimately show "cindexE (- r) r f = cindexE_ubd f"
unfolding cindexE_def cindexE_ubd_def
apply (fold R1_def R2_def L1_def L2_def)
by auto
qed
moreover have "∀⇩F r in at_top. cindexE (- r) r f = cindex_poly_ubd q p"
using cindex_poly_ubd_eventually unfolding f_def by auto
ultimately have "∀⇩F r in at_top. cindexE (- r) r f = cindexE_ubd f
∧ cindexE (- r) r f = cindex_poly_ubd q p"
using eventually_conj by auto
then have "∀⇩F (r::real) in at_top. cindexE_ubd f = cindex_poly_ubd q p"
by (elim eventually_mono) auto
then show ?thesis unfolding f_def by auto
qed

end


# Theory More_Polynomials

(*
Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
*)
section ‹More useful lemmas related polynomials›

theory More_Polynomials imports
Winding_Number_Eval.Missing_Algebraic
Winding_Number_Eval.Missing_Transcendental
Sturm_Tarski.PolyMisc
Budan_Fourier.BF_Misc
begin

lemma order_normalize[simp]:"order x (normalize p) = order x p"
by (metis dvd_normalize_iff normalize_eq_0_iff order_1 order_2 order_unique_lemma)

lemma order_gcd:
assumes "p≠0" "q≠0"
shows "order x (gcd p q) = min (order x p) (order x q)"
proof -
define xx op oq where "xx=[:- x, 1:]" and "op = order x p" and "oq = order x q"
obtain pp where pp:"p = xx ^ op * pp" "¬ xx dvd pp"
using order_decomp[OF ‹p≠0›,of x,folded xx_def op_def] by auto
obtain qq where qq:"q = xx ^ oq * qq" "¬ xx dvd qq"
using order_decomp[OF ‹q≠0›,of x,folded xx_def oq_def] by auto
define pq where "pq = gcd pp qq"

have p_unfold:"p = (pq * xx ^ (min op oq)) * ((pp div pq) * xx ^ (op - min op oq))"
and [simp]:"coprime xx (pp div pq)" and "pp≠0"
proof -
have "xx ^ op = xx ^ (min op oq) * xx ^ (op - min op oq)"
moreover have "pp = pq * (pp div pq)"
unfolding pq_def by simp
ultimately show "p = (pq * xx ^ (min op oq)) * ((pp div pq) * xx ^ (op - min op oq))"
unfolding pq_def pp by(auto simp:algebra_simps)
show "coprime xx (pp div pq)"
apply (rule prime_elem_imp_coprime[OF
prime_elem_linear_poly[of 1 "-x",simplified],folded xx_def])
using ‹pp = pq * (pp div pq)› pp(2) by auto
qed (use pp ‹p≠0› in auto)
have q_unfold:"q = (pq * xx ^ (min op oq)) * ((qq div pq) * xx ^ (oq - min op oq))"
and [simp]:"coprime xx (qq div pq)"
proof -
have "xx ^ oq = xx ^ (min op oq) * xx ^ (oq - min op oq)"
moreover have "qq = pq * (qq div pq)"
unfolding pq_def by simp
ultimately show "q = (pq * xx ^ (min op oq)) * ((qq div pq) * xx ^ (oq - min op oq))"
unfolding pq_def qq by(auto simp:algebra_simps)
show "coprime xx (qq div pq)"
apply (rule prime_elem_imp_coprime[OF
prime_elem_linear_poly[of 1 "-x",simplified],folded xx_def])
using ‹qq = pq * (qq div pq)› qq(2) by auto
qed

have "gcd p q=normalize (pq * xx ^ (min op oq))"
proof -
have "coprime (pp div pq * xx ^ (op - min op oq)) (qq div pq * xx ^ (oq - min op oq))"
proof (cases "op>oq")
case True
then have "oq - min op oq = 0" by auto
moreover have "coprime (xx ^ (op - min op oq)) (qq div pq)" by auto
moreover have "coprime (pp div pq) (qq div pq)"
apply (rule div_gcd_coprime[of pp qq,folded pq_def])
using ‹pp≠0› by auto
ultimately show ?thesis by auto
next
case False
then have "op - min op oq = 0" by auto
moreover have "coprime (pp div pq) (xx ^ (oq - min op oq))"
by (auto simp:coprime_commute)
moreover have "coprime (pp div pq) (qq div pq)"
apply (rule div_gcd_coprime[of pp qq,folded pq_def])
using ‹pp≠0› by auto
ultimately show ?thesis by auto
qed
then show ?thesis unfolding p_unfold q_unfold
apply (subst gcd_mult_left)
by auto
qed
then have "order x (gcd p q) = order x pq + order x (xx ^ (min op oq))"
apply simp
apply (subst order_mult)
using assms(1) p_unfold by auto
also have "... = order x (xx ^ (min op oq))"
using pp(2) qq(2) unfolding pq_def xx_def
by (auto simp add: order_0I poly_eq_0_iff_dvd)
also have "... = min op oq"
unfolding xx_def by (rule order_power_n_n)
also have "... = min (order x p) (order x q)" unfolding op_def oq_def by simp
finally show ?thesis .
qed

lemma pderiv_power: "pderiv (p ^ n) = smult (of_nat n) (p ^ (n-1)) * pderiv p"
apply (cases n)
using pderiv_power_Suc by auto

(*TODO: to replace the one (with the same name) in the library, as this version does
not require 'a to be a field?*)
lemma order_pderiv:
fixes p::"'a::{idom,semiring_char_0} poly"
assumes "p≠0" "poly p x=0"
shows "order x p = Suc (order x (pderiv p))" using assms
proof -
define xx op where "xx=[:- x, 1:]" and "op = order x p"
have "op ≠0" unfolding op_def using assms order_root by blast
obtain pp where pp:"p = xx ^ op * pp" "¬ xx dvd pp"
using order_decomp[OF ‹p≠0›,of x,folded xx_def op_def] by auto
have p_der:"pderiv p = smult (of_nat op) (xx^(op -1)) * pp + xx^op*pderiv pp"
unfolding pp(1) by (auto simp:pderiv_mult pderiv_power xx_def algebra_simps pderiv_pCons)
have "xx^(op -1) dvd (pderiv p)"
unfolding p_der
by (metis One_nat_def Suc_pred assms(1) assms(2) dvd_add dvd_mult_right dvd_triv_left
neq0_conv op_def order_root power_Suc smult_dvd_cancel)
moreover have "¬ xx^op dvd (pderiv p)"
proof
assume "xx ^ op dvd pderiv p"
then have "xx ^ op dvd smult (of_nat op) (xx^(op -1) * pp)"
then have "xx ^ op dvd (xx^(op -1)) * pp"
apply (elim dvd_monic[rotated])
using ‹op≠0› by (auto simp:lead_coeff_power xx_def)
then have "xx ^ (op-1) * xx dvd (xx^(op -1))"
using ‹¬ xx dvd pp› by (simp add: ‹op ≠ 0› mult.commute power_eq_if)
then have "xx dvd 1"
using assms(1) pp(1) by auto
then show False unfolding xx_def by (meson assms(1) dvd_trans one_dvd order_decomp)
qed
ultimately have "op - 1 = order x (pderiv p)"
using order_unique_lemma[of x "op-1" "pderiv p",folded xx_def] ‹op≠0›
by auto
then show ?thesis using ‹op≠0› unfolding op_def by auto
qed

lemma rsquarefree_0[simp]: "¬ rsquarefree 0"
unfolding rsquarefree_def by simp

lemma rsquarefree_times:
assumes "rsquarefree (p*q)"
shows "rsquarefree q" using assms
proof (induct p rule:poly_root_induct_alt)
case 0
then show ?case by simp
next
case (no_proots p)
then have [simp]:"p≠0" "q≠0" "⋀a. order a p = 0"
using order_0I by auto
have "order a (p * q) = 0 ⟷ order a q = 0"
"order a (p * q) = 1 ⟷ order a q = 1"
for a
subgoal by (subst order_mult) auto
subgoal by (subst order_mult) auto
done
then show ?case using ‹rsquarefree (p * q)›
unfolding rsquarefree_def by simp
next
case (root a p)
define pq aa where "pq = p * q" and "aa = [:- a, 1:]"
have [simp]:"pq≠0" "aa≠0" "order a aa=1"
subgoal using pq_def root.prems by auto
subgoal by (metis aa_def order_power_n_n power_one_right)
done
have "rsquarefree (aa * pq)"
unfolding aa_def pq_def using root(2) by (simp add:algebra_simps)
then have "rsquarefree pq"
unfolding rsquarefree_def by (auto simp add:order_mult)
from root(1)[OF this[unfolded pq_def]] show ?case .
qed

lemma rsquarefree_smult_iff:
assumes "s≠0"
shows "rsquarefree (smult s p) ⟷ rsquarefree p"
unfolding rsquarefree_def using assms by (auto simp add:order_smult)

lemma card_proots_within_rsquarefree:
assumes "rsquarefree p"
shows "proots_count p s = card (proots_within p s)" using assms
proof (induct rule:poly_root_induct[of _ "λx. x∈s"])
case 0
then have False by simp
then show ?case by simp
next
case (no_roots p)
then show ?case
by (metis all_not_in_conv card.empty proots_count_def proots_within_iff sum.empty)
next
case (root a p)
have "proots_count ([:a, - 1:] * p) s = 1 + proots_count p s"
apply (subst proots_count_times)
subgoal using root.prems rsquarefree_def by blast
minus_pCons proots_count_pCons_1_iff proots_count_uminus root.hyps(1))
done
also have "... = 1 + card (proots_within p s)"
proof -
have "rsquarefree p" using ‹rsquarefree ([:a, - 1:] * p)›
by (elim rsquarefree_times)
from root(2)[OF this] show ?thesis by simp
qed
also have "... = card (proots_within ([:a, - 1:] * p) s)" unfolding proots_within_times
proof (subst card_Un_disjoint)
have [simp]:"p≠0" using root.prems by auto
show "finite (proots_within [:a, - 1:] s)" "finite (proots_within p s)"
by auto
show " 1 + card (proots_within p s) = card (proots_within [:a, - 1:] s)
+ card (proots_within p s)"
using ‹a ∈ s›
apply (subst proots_within_pCons_1_iff)
by simp
have "poly p a≠0"
proof (rule ccontr)
assume "¬ poly p a ≠ 0"
then have "order a p >0" by (simp add: order_root)
moreover have "order a [:a,-1:] = 1"
order_power_n_n order_uminus power_one_right)
ultimately have "order a  ([:a, - 1:] * p) > 1"
apply (subst order_mult)
subgoal using root.prems by auto
subgoal by auto
done
then show False using ‹rsquarefree ([:a, - 1:] * p)›
unfolding rsquarefree_def using gr_implies_not0 less_not_refl2 by blast
qed
then show " proots_within [:a, - 1:] s ∩ proots_within p s = {}"
using proots_within_pCons_1_iff(2) by auto
qed
finally show ?case .
qed

lemma rsquarefree_gcd_pderiv:
fixes p::"'a::{factorial_ring_gcd,semiring_gcd_mult_normalize,semiring_char_0} poly"
assumes "p≠0"
shows "rsquarefree (p div (gcd p (pderiv p)))"
proof (cases "pderiv p = 0")
case True
have "poly (unit_factor p) x ≠0" for x
using unit_factor_is_unit[OF ‹p≠0›]
by (meson assms dvd_trans order_decomp poly_eq_0_iff_dvd unit_factor_dvd)
then have "order x (unit_factor p) = 0" for x
using order_0I by blast
then show ?thesis using True ‹p≠0› unfolding rsquarefree_def by simp
next
case False
define q where "q = p div (gcd p (pderiv p))"
have "q≠0" unfolding q_def by (simp add: assms dvd_div_eq_0_iff)

have order_pq:"order x p = order x q + min (order x p) (order x (pderiv p))"
for x
proof -
have *:"p = q * gcd p (pderiv p)"
unfolding q_def by simp
show ?thesis
apply (subst *)
using ‹q≠0› ‹p≠0› ‹pderiv p≠0› by (simp add:order_mult order_gcd)
qed
have "order x q = 0 ∨ order x q=1" for x
proof (cases "poly p x=0")
case True
from order_pderiv[OF ‹p≠0› this]
have "order x p = order x (pderiv p) + 1" by simp
then show ?thesis using order_pq[of x] by auto
next
case False
then have "order x p = 0" by (simp add: order_0I)
then have "order x q = 0" using order_pq[of x] by simp
then show ?thesis by simp
qed
then show ?thesis using ‹q≠0› unfolding rsquarefree_def q_def
by auto
qed

lemma poly_gcd_pderiv_iff:
fixes p::"'a::{semiring_char_0,factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
shows "poly (p div (gcd p (pderiv p))) x =0 ⟷ poly p x=0"
proof (cases "pderiv p=0")
case True
then obtain a where "p=[:a:]" using pderiv_iszero by auto
then show ?thesis by (auto simp add: unit_factor_poly_def)
next
case False
then have "p≠0" using pderiv_0 by blast
define q where "q = p div (gcd p (pderiv p))"
have "q≠0" unfolding q_def by (simp add: ‹p≠0› dvd_div_eq_0_iff)

have order_pq:"order x p = order x q + min (order x p) (order x (pderiv p))" for x
proof -
have *:"p = q * gcd p (pderiv p)"
unfolding q_def by simp
show ?thesis
apply (subst *)
using ‹q≠0› ‹p≠0› ‹pderiv p≠0› by (simp add:order_mult order_gcd)
qed

have "order x q =0 ⟷ order x p = 0"
proof (cases "poly p x=0")
case True
from order_pderiv[OF ‹p≠0› this]
have "order x p = order x (pderiv p) + 1" by simp
then show ?thesis using order_pq[of x] by auto
next
case False
then have "order x p = 0" by (simp add: order_0I)
then have "order x q = 0" using order_pq[of x] by simp
then show ?thesis using ‹order x p = 0› by simp
qed
then show ?thesis
apply (fold q_def)
unfolding order_root using ‹p≠0› ‹q≠0› by auto
qed

subsection ‹Composition of a polynomial and a circular path›

lemma poly_circlepath_tan_eq:
fixes z0::complex and r::real and p::"complex poly"
defines "q1≡ fcompose p [:(z0+r)*𝗂,z0-r:] [:𝗂,1:]" and "q2 ≡ [:𝗂,1:] ^ degree p"
assumes "0≤t" "t≤1" "t≠1/2"
shows "poly p (circlepath z0 r t) = poly q1 (tan (pi*t)) / poly q2 (tan (pi*t))"
(is "?L = ?R")
proof -
have "?L = poly p (z0+ r*exp (2 * of_real pi * 𝗂  * t))"
unfolding circlepath by simp
also have "... = ?R"
proof -
define f where "f = (poly p ∘ (λx::real. z0 + r * exp (𝗂 * x)))"
have f_eq:"f t = ((λx::real. poly q1 x / poly q2 x) o  (λx. tan (x/2)) ) t"
when "cos (t / 2) ≠ 0" for t
proof -
have "f t = poly p (z0 + r * (cos t + 𝗂 * sin t)) "
unfolding f_def exp_Euler  by (auto simp add:cos_of_real sin_of_real)
also have "... = poly p ((λx. ((z0-r)*x+(z0+r)*𝗂) / (𝗂+x)) (tan (t/2)))"
proof -
define tt where "tt=complex_of_real (tan (t / 2))"
define rr where "rr = complex_of_real r"
have "cos t = (1-tt*tt) / (1 + tt * tt)"
"sin t = 2*tt  / (1 + tt * tt)"
unfolding sin_tan_half[of "t/2",simplified] cos_tan_half[of "t/2",OF that, simplified] tt_def
moreover have "1 + tt * tt ≠ 0" unfolding tt_def
apply (fold of_real_mult)
by (metis (no_types, hide_lams) mult_numeral_1 numeral_One of_real_add of_real_eq_0_iff
of_real_numeral sum_squares_eq_zero_iff zero_neq_one)
ultimately have "z0 +  r * ( (cos t) + 𝗂 * (sin t))
=(z0*(1+tt*tt)+rr*(1-tt*tt)+𝗂*rr*2*tt ) / (1 + tt * tt) "
also have "... = ((z0-rr)*tt+z0*𝗂+rr*𝗂) / (tt + 𝗂)"
proof -
have "tt + 𝗂 ≠ 0"
using ‹1 + tt * tt ≠ 0›
then show ?thesis
using ‹1 + tt * tt ≠ 0› by (auto simp add:divide_simps algebra_simps)
qed
finally have "z0 +  r * ( (cos t) + 𝗂 * (sin t)) = ((z0-rr)*tt+z0*𝗂+rr*𝗂) / (tt + 𝗂)" .
then show ?thesis unfolding tt_def rr_def
qed
also have "... = (poly p o ((λx. ((z0-r)*x+(z0+r)*𝗂) / (𝗂+x)) o (λx. tan (x/2)) )) t"
unfolding comp_def by (auto simp:tan_of_real)
also have "... = ((λx::real. poly q1 x / poly q2 x) o  (λx. tan (x/2)) ) t"
unfolding q2_def q1_def
apply (subst fcompose_poly[symmetric])
subgoal for x
apply simp
by (metis Re_complex_of_real add_cancel_right_left complex_i_not_zero imaginary_unit.sel(1) plus_complex.sel(1) rcis_zero_arg rcis_zero_mod)
subgoal by (auto simp:tan_of_real algebra_simps)
done
finally show ?thesis .
qed

have "cos (pi * t) ≠0" unfolding cos_zero_iff_int2
proof
assume "∃i. pi * t = real_of_int i * pi + pi / 2"
then obtain i where "pi * t = real_of_int i * pi + pi / 2" by auto
then have "pi * t=pi * (real_of_int i + 1 / 2)" by (simp add:algebra_simps)
then have "t=real_of_int i + 1 / 2" by auto
then show False using ‹0≤t› ‹t≤1› ‹t≠1/2› by auto
qed
from f_eq[of "2*pi*t",simplified,OF this]
show "?thesis"
unfolding f_def comp_def by (auto simp add:algebra_simps)
qed
finally show ?thesis .
qed

end

# Theory Count_Complex_Roots

(*
Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
*)

section ‹Procedures to count the number of complex roots›

theory Count_Complex_Roots imports
Winding_Number_Eval.Winding_Number_Eval
Extended_Sturm
More_Polynomials
Budan_Fourier.Sturm_Multiple_Roots
begin

subsection ‹Misc›

(*refined version of the library one with the same name by dropping unnecessary assumptions*)
corollary path_image_part_circlepath_subset:
assumes "r≥0"
shows "path_image(part_circlepath z r st tt) ⊆ sphere z r"
proof (cases "st≤tt")
case True
then show ?thesis
by (auto simp: assms path_image_part_circlepath sphere_def dist_norm algebra_simps norm_mult)
next
case False
then have "path_image(part_circlepath z r tt st) ⊆ sphere z r"
by (auto simp: assms path_image_part_circlepath sphere_def dist_norm algebra_simps norm_mult)
moreover have "path_image(part_circlepath z r tt st) = path_image(part_circlepath z r st tt)"
using path_image_reversepath by fastforce
ultimately show ?thesis by auto
qed

(*refined version of the library one with the same name by dropping unnecessary assumptions*)
proposition in_path_image_part_circlepath:
assumes "w ∈ path_image(part_circlepath z r st tt)" "0 ≤ r"
shows "norm(w - z) = r"
proof -
have "w ∈ {c. dist z c = r}"
by (metis (no_types) path_image_part_circlepath_subset sphere_def subset_eq assms)
thus ?thesis
qed

lemma infinite_ball:
fixes a :: "'a::euclidean_space"
assumes "r > 0"
shows "infinite (ball a r)"
using uncountable_ball[OF assms, THEN uncountable_infinite] .

lemma infinite_cball:
fixes a :: "'a::euclidean_space"
assumes "r > 0"
shows "infinite (cball a r)"
using uncountable_cball[OF assms, THEN uncountable_infinite,of a] .

(*FIXME: to generalise*)
lemma infinite_sphere:
fixes a :: complex
assumes "r > 0"
shows "infinite (sphere a r)"
proof -
have "uncountable (path_image (circlepath a r))"
apply (rule simple_path_image_uncountable)
using simple_path_circlepath assms by simp
then have "uncountable (sphere a r)"
using assms by simp
from uncountable_infinite[OF this] show ?thesis .
qed

lemma infinite_halfspace_Im_gt: "infinite {x. Im x > b}"
apply (rule connected_uncountable[THEN uncountable_infinite,of _ "(b+1)* 𝗂" "(b+2)*𝗂"])
by (auto intro!:convex_connected simp add: convex_halfspace_Im_gt)

lemma (in ring_1) Ints_minus2: "- a ∈ ℤ ⟹ a ∈ ℤ"
using Ints_minus[of "-a"] by auto

lemma dvd_divide_Ints_iff:
"b dvd a ∨ b=0 ⟷ of_int a / of_int b ∈ (ℤ :: 'a :: {field,ring_char_0} set)"
proof
assume asm:"b dvd a ∨ b=0"
let ?thesis = "of_int a / of_int b ∈ (ℤ :: 'a :: {field,ring_char_0} set)"
have ?thesis when "b dvd a"
proof -
obtain c where "a=b * c" using ‹b dvd a› unfolding dvd_def by auto
then show ?thesis by (auto simp add:field_simps)
qed
moreover have ?thesis when "b=0"
using that by auto
ultimately show ?thesis using asm by auto
next
assume "of_int a / of_int b ∈ (ℤ :: 'a :: {field,ring_char_0} set)"
from Ints_cases[OF this] obtain c where *:"(of_int::_ ⇒ 'a) c= of_int a / of_int b"
by metis
have "b dvd a" when "b≠0"
proof -
have "(of_int::_ ⇒ 'a) a = of_int b * of_int c" using that * by auto
then have "a = b * c" using of_int_eq_iff by fastforce
then show ?thesis unfolding dvd_def by auto
qed
then show " b dvd a ∨ b = 0" by auto
qed

lemma of_int_div_field:
assumes "d dvd n"
shows "(of_int::_⇒'a::field_char_0) (n div d) = of_int n / of_int d"
apply (subst (2) dvd_mult_div_cancel[OF assms,symmetric])

lemma powr_eq_1_iff:
assumes "a>0"
shows "(a::real) powr b =1 ⟷ a=1 ∨ b=0"
proof
assume "a powr b = 1"
have "b * ln a = 0"
using ‹a powr b = 1› ln_powr[of a b] assms by auto
then have "b=0 ∨ ln a =0" by auto
then show "a = 1 ∨ b = 0" using assms by auto
qed (insert assms, auto)

lemma tan_inj_pi:
"- (pi/2) < x ⟹ x < pi/2 ⟹ - (pi/2) < y ⟹ y < pi/2 ⟹ tan x = tan y ⟹ x = y"
by (metis arctan_tan)

(*TODO: can we avoid fcompose in the proof?*)
lemma finite_ReZ_segments_poly_circlepath:
"finite_ReZ_segments (poly p ∘ circlepath z0 r) 0"
proof (cases "∀t∈({0..1} - {1/2}). Re ((poly p ∘ circlepath z0 r) t) = 0")
case True
have "isCont (Re ∘ poly p ∘ circlepath z0 r) (1/2)"
by (auto intro!:continuous_intros simp:circlepath)
moreover have "(Re ∘ poly p ∘ circlepath z0 r)─ 1/2 → 0"
proof -
have "∀⇩F x in at (1 / 2). (Re ∘ poly p ∘ circlepath z0 r) x = 0"
unfolding eventually_at_le
apply (rule exI[where x="1/2"])
unfolding dist_real_def abs_diff_le_iff
by (auto intro!:True[rule_format, unfolded comp_def])
then show ?thesis by (rule tendsto_eventually)
qed
ultimately have "Re ((poly p ∘ circlepath z0 r) (1/2)) = 0"
unfolding comp_def by (simp add: LIM_unique continuous_within)
then have "∀t∈{0..1}. Re ((poly p ∘ circlepath z0 r) t) = 0"
using True by blast
then show ?thesis
apply (rule_tac finite_ReZ_segments_constI[THEN finite_ReZ_segments_congE])
by auto
next
case False
define q1 q2 where "q1=fcompose p [:(z0+r)*𝗂,z0-r:] [:𝗂,1:]" and
"q2=([:𝗂, 1:] ^ degree p)"
define q1R q1I where "q1R=map_poly Re q1" and "q1I=map_poly Im q1"
define q2R q2I where "q2R=map_poly Re q2" and "q2I=map_poly Im q2"
define qq where "qq=q1R*q2R + q1I*q2I"

have poly_eq:"Re ((poly p ∘ circlepath z0 r) t) = 0 ⟷ poly qq (tan (pi * t)) = 0"
when "0≤t" "t≤1" "t≠1/2" for t
proof -
define tt where "tt=tan (pi * t)"
have "Re ((poly p ∘ circlepath z0 r) t) = 0 ⟷ Re (poly q1 tt / poly q2 tt) = 0"
unfolding comp_def
apply (subst poly_circlepath_tan_eq[of t p z0 r,folded q1_def q2_def tt_def])
using that by simp_all
also have "... ⟷ poly q1R tt * poly q2R tt + poly q1I tt * poly q2I tt = 0"
unfolding q1I_def q1R_def q2R_def q2I_def
also have "... ⟷ poly qq tt = 0"
unfolding qq_def by simp
finally show ?thesis unfolding tt_def .
qed

have "finite {t. Re ((poly p ∘ circlepath z0 r) t) = 0 ∧ 0 ≤ t ∧ t ≤ 1}"
proof -
define P where "P=(λt. Re ((poly p ∘ circlepath z0 r) t) = 0)"
define A where "A= ({0..1}::real set)"
define S where "S={t∈A-{1,1/2}. P t}"
have "finite {t. poly qq (tan (pi * t)) = 0 ∧ 0 ≤ t ∧ t < 1 ∧ t≠1/2}"
proof -
define A where "A={t::real. 0 ≤ t ∧ t < 1 ∧ t ≠ 1 / 2}"
have "finite ((λt. tan (pi * t))  -  {x. poly qq x=0} ∩ A)"
proof (rule finite_vimage_IntI)
have "x = y" when "tan (pi * x) = tan (pi * y)" "x∈A" "y∈A" for x y
proof -
define x' where "x'=(if x<1/2 then x else x-1)"
define y' where "y'=(if y<1/2 then y else y-1)"
have "x'*pi = y'*pi"
proof (rule tan_inj_pi)
have *:"- 1 / 2 < x'" "x' < 1 / 2" "- 1 / 2 < y'" "y' < 1 / 2"
using that(2,3) unfolding x'_def y'_def A_def by simp_all
show "- (pi / 2) < x'  * pi" "x'  * pi < pi / 2" "- (pi / 2) < y'  * pi"
"y'*pi < pi / 2"
using mult_strict_right_mono[OF *(1),of pi]
mult_strict_right_mono[OF *(2),of pi]
mult_strict_right_mono[OF *(3),of pi]
mult_strict_right_mono[OF *(4),of pi]
by auto
next
have "tan (x' * pi) = tan (x * pi)"
unfolding x'_def using tan_periodic_int[of _ "- 1",simplified]
also have "... = tan (y * pi)"
using ‹tan (pi * x) = tan (pi * y)› by (auto simp:algebra_simps)
also have "... = tan (y' * pi)"
unfolding y'_def using tan_periodic_int[of _ "- 1",simplified]
finally show "tan (x' * pi) = tan (y' * pi)" .
qed
then have "x'=y'" by auto
then show ?thesis
using that(2,3) unfolding x'_def y'_def A_def by (auto split:if_splits)
qed
then show "inj_on (λt. tan (pi * t)) A"
unfolding inj_on_def by blast
next
have "qq≠0"
proof (rule ccontr)
assume "¬ qq ≠ 0"
then have "Re ((poly p ∘ circlepath z0 r) t) = 0" when "t∈{0..1} - {1/2}" for t
apply (subst poly_eq)
using that by auto
then show False using False by blast
qed
then show "finite {x. poly qq x = 0}" by (simp add: poly_roots_finite)
qed
then show ?thesis by (elim rev_finite_subset) (auto simp:A_def)
qed
moreover have "{t. poly qq (tan (pi * t)) = 0 ∧ 0 ≤ t ∧ t < 1 ∧ t≠1/2} = S"
unfolding S_def P_def A_def using poly_eq by force
ultimately have "finite S" by blast
then have "finite (S ∪ (if P 1 then {1} else {}) ∪ (if P (1/2) then {1/2} else {}))"
by auto
moreover have "(S ∪ (if P 1 then {1} else {}) ∪ (if P (1/2) then {1/2} else {}))
= {t. P t ∧ 0 ≤ t ∧ t ≤ 1}"
proof -
have "1∈A" "1/2 ∈A" unfolding A_def by auto
then have "(S ∪ (if P 1 then {1} else {}) ∪ (if P (1/2) then {1/2} else {}))
= {t∈A. P t}"
unfolding S_def
apply auto
by (metis eq_divide_eq_numeral1(1) zero_neq_numeral)+
also have "... = {t. P t ∧ 0 ≤ t ∧ t ≤ 1}"
unfolding A_def by auto
finally show ?thesis .
qed
ultimately have "finite {t. P t ∧ 0 ≤ t ∧ t ≤ 1}" by auto
then show ?thesis unfolding P_def by simp
qed
then show ?thesis
apply (rule_tac finite_imp_finite_ReZ_segments)
by auto
qed

subsection ‹Some useful conformal/@{term bij_betw} properties›

lemma bij_betw_plane_ball:"bij_betw (λx. (𝗂-x)/(𝗂+x)) {x. Im x>0} (ball 0 1)"
proof (rule bij_betw_imageI)
have neq:"𝗂 + x ≠0" when "Im x>0" for x
using that
imaginary_unit.simps(2) not_one_less_zero uminus_complex.sel(2))
then show "inj_on (λx. (𝗂 - x) / (𝗂 + x)) {x. 0 < Im x}"
unfolding inj_on_def by (auto simp add:divide_simps algebra_simps)
have "cmod ((𝗂 - x) / (𝗂 + x)) < 1" when "0 < Im x " for x
proof -
have "cmod (𝗂 - x) < cmod (𝗂 + x)"
unfolding norm_lt inner_complex_def using that
then show ?thesis
unfolding norm_divide using neq[OF that] by auto
qed
moreover have "x ∈ (λx. (𝗂 - x) / (𝗂 + x))  {x. 0 < Im x}" when "cmod x < 1" for x
proof (rule rev_image_eqI[of "𝗂*(1-x)/(1+x)"])
have "1 + x≠0" "𝗂 * 2 + 𝗂 * (x * 2) ≠0"
subgoal using that by (metis complex_mod_triangle_sub norm_one norm_zero not_le pth_7(1))
subgoal using that by (metis ‹1 + x ≠ 0› complex_i_not_zero div_mult_self4 mult_2
mult_zero_right nonzero_mult_div_cancel_left nonzero_mult_div_cancel_right
done
then show "x = (𝗂 - 𝗂 * (1 - x) / (1 + x)) / (𝗂 + 𝗂 * (1 - x) / (1 + x))"
show " 𝗂 * (1 - x) / (1 + x) ∈ {x. 0 < Im x}"
apply (auto simp:Im_complex_div_gt_0 algebra_simps)
using that unfolding cmod_def by (auto simp:power2_eq_square)
qed
ultimately show "(λx. (𝗂 - x) / (𝗂 + x))  {x. 0 < Im x} = ball 0 1"
by auto
qed

lemma bij_betw_axis_sphere:"bij_betw (λx. (𝗂-x)/(𝗂+x)) {x. Im x=0} (sphere 0 1 - {-1})"
proof (rule bij_betw_imageI)
have neq:"𝗂 + x ≠0" when "Im x=0" for x
using that
right_minus_eq zero_complex.simps(2) zero_neq_one)
then show "inj_on (λx. (𝗂 - x) / (𝗂 + x)) {x. Im x = 0}"
unfolding inj_on_def by (auto simp add:divide_simps algebra_simps)
have "cmod ((𝗂 - x) / (𝗂 + x)) = 1" "(𝗂 - x) / (𝗂 + x) ≠ - 1" when "Im x = 0" for x
proof -
have "cmod (𝗂 + x) = cmod (𝗂 - x)"
using that unfolding cmod_def by auto
then show "cmod ((𝗂 - x) / (𝗂 + x)) = 1"
unfolding norm_divide using neq[OF that] by auto
show "(𝗂 - x) / (𝗂 + x) ≠ - 1" using neq[OF that] by (auto simp add:divide_simps)
qed
moreover have "x ∈ (λx. (𝗂 - x) / (𝗂 + x))  {x. Im x = 0}"
when "cmod x = 1" "x≠-1" for x
proof (rule rev_image_eqI[of "𝗂*(1-x)/(1+x)"])
have "1 + x≠0" "𝗂 * 2 + 𝗂 * (x * 2) ≠0"
subgoal using that(2) by algebra
subgoal using that by (metis ‹1 + x ≠ 0› complex_i_not_zero div_mult_self4 mult_2
mult_zero_right nonzero_mult_div_cancel_left nonzero_mult_div_cancel_right
done
then show "x = (𝗂 - 𝗂 * (1 - x) / (1 + x)) / (𝗂 + 𝗂 * (1 - x) / (1 + x))"
show " 𝗂 * (1 - x) / (1 + x) ∈ {x. Im x = 0}"
apply (auto simp:algebra_simps Im_complex_div_eq_0)
using that(1) unfolding cmod_def by (auto simp:power2_eq_square)
qed
ultimately show "(λx. (𝗂 - x) / (𝗂 + x))  {x. Im x = 0} = sphere 0 1 - {- 1}"
by force
qed

lemma bij_betw_ball_uball:
assumes "r>0"
shows "bij_betw (λx. complex_of_real r*x + z0) (ball 0 1) (ball z0 r)"
proof (rule bij_betw_imageI)
show "inj_on (λx. complex_of_real r * x + z0) (ball 0 1)"
unfolding inj_on_def using assms by simp
have "dist z0 (complex_of_real r * x + z0) < r" when "cmod x<1" for x
using that assms by (auto simp:dist_norm norm_mult abs_of_pos)
moreover have "x ∈ (λx. complex_of_real r * x + z0)  ball 0 1" when "dist z0 x < r" for x
apply (rule rev_image_eqI[of "(x-z0)/r"])
using that assms by (auto simp add: dist_norm norm_divide norm_minus_commute)
ultimately show "(λx. complex_of_real r  * x + z0)  ball 0 1 = ball z0 r"
by auto
qed

lemma bij_betw_sphere_usphere:
assumes "r>0"
shows "bij_betw (λx. complex_of_real r*x + z0) (sphere 0 1) (sphere z0 r)"
proof (rule bij_betw_imageI)
show "inj_on (λx. complex_of_real r * x + z0) (sphere 0 1)"
unfolding inj_on_def using assms by simp
have "dist z0 (complex_of_real r * x + z0) = r" when "cmod x=1" for x
using that assms by (auto simp:dist_norm norm_mult abs_of_pos)
moreover have "x ∈ (λx. complex_of_real r * x + z0)  sphere 0 1" when "dist z0 x = r" for x
apply (rule rev_image_eqI[of "(x-z0)/r"])
using that assms by (auto simp add: dist_norm norm_divide norm_minus_commute)
ultimately show "(λx. complex_of_real r  * x + z0)  sphere 0 1 = sphere z0 r"
by auto
qed

lemma proots_ball_plane_eq:
defines "q1≡[:𝗂,-1:]" and "q2≡[:𝗂,1:]"
assumes "p≠0"
shows "proots_count p (ball 0 1) = proots_count (fcompose p q1 q2) {x. 0 < Im x}"
unfolding q1_def q2_def
proof (rule proots_fcompose_bij_eq[OF _ ‹p≠0›])
show "∀x∈{x. 0 < Im x}. poly [:𝗂, 1:] x ≠ 0"
apply simp
plus_complex.simps(2) zero_complex.simps(2))
show "infinite (UNIV::complex set)" by (simp add: infinite_UNIV_char_0)
qed (use bij_betw_plane_ball in auto)

lemma proots_sphere_axis_eq:
defines "q1≡[:𝗂,-1:]" and "q2≡[:𝗂,1:]"
assumes "p≠0"
shows "proots_count p (sphere 0 1 - {- 1}) = proots_count (fcompose p q1 q2) {x. 0 = Im x}"
unfolding q1_def q2_def
proof (rule proots_fcompose_bij_eq[OF _ ‹p≠0›])
show "∀x∈{x. 0 = Im x}. poly [:𝗂, 1:] x ≠ 0" by (simp add: Complex_eq_0 plus_complex.code)
show "infinite (UNIV::complex set)" by (simp add: infinite_UNIV_char_0)
qed (use bij_betw_axis_sphere in auto)

lemma proots_card_ball_plane_eq:
defines "q1≡[:𝗂,-1:]" and "q2≡[:𝗂,1:]"
assumes "p≠0"
shows "card (proots_within p (ball 0 1)) = card (proots_within (fcompose p q1 q2) {x. 0 < Im x})"
unfolding q1_def q2_def
proof (rule proots_card_fcompose_bij_eq[OF _ ‹p≠0›])
show "∀x∈{x. 0 < Im x}. poly [:𝗂, 1:] x ≠ 0"
apply simp
plus_complex.simps(2) zero_complex.simps(2))
qed (use bij_betw_plane_ball infinite_UNIV_char_0 in auto)

lemma proots_card_sphere_axis_eq:
defines "q1≡[:𝗂,-1:]" and "q2≡[:𝗂,1:]"
assumes "p≠0"
shows "card (proots_within p (sphere 0 1 - {- 1}))
= card (proots_within (fcompose p q1 q2) {x. 0 = Im x})"
unfolding q1_def q2_def
proof (rule proots_card_fcompose_bij_eq[OF _ ‹p≠0›])
show "∀x∈{x. 0 = Im x}. poly [:𝗂, 1:] x ≠ 0" by (simp add: Complex_eq_0 plus_complex.code)
qed (use bij_betw_axis_sphere infinite_UNIV_char_0 in auto)

lemma proots_uball_eq:
fixes z0::complex and r::real
defines "q≡[:z0, of_real r:]"
assumes "p≠0" and "r>0"
shows "proots_count p (ball z0 r) = proots_count (p ∘⇩p q) (ball 0 1)"
proof -
show ?thesis
apply (rule proots_pcompose_bij_eq[OF _ ‹p≠0›])
subgoal unfolding q_def using bij_betw_ball_uball[OF ‹r>0›,of z0] by (auto simp:algebra_simps)
subgoal unfolding q_def using ‹r>0› by auto
done
qed

lemma proots_card_uball_eq:
fixes z0::complex and r::real
defines "q≡[:z0, of_real r:]"
assumes "r>0"
shows "card (proots_within p (ball z0 r)) = card (proots_within (p ∘⇩p q) (ball 0 1))"
proof -
have ?thesis
when "p=0"
proof -
have "card (ball z0 r) = 0" "card (ball (0::complex) 1) = 0"
using infinite_ball[OF ‹r>0›,of z0] infinite_ball[of 1 "0::complex"] by auto
then show ?thesis using that by auto
qed
moreover have ?thesis
when "p≠0"
apply (rule proots_card_pcompose_bij_eq[OF _ ‹p≠0›])
subgoal unfolding q_def using bij_betw_ball_uball[OF ‹r>0›,of z0] by (auto simp:algebra_simps)
subgoal unfolding q_def using ‹r>0› by auto
done
ultimately show ?thesis
by blast
qed

lemma proots_card_usphere_eq:
fixes z0::complex and r::real
defines "q≡[:z0, of_real r:]"
assumes "r>0"
shows "card (proots_within p (sphere z0 r)) = card (proots_within (p ∘⇩p q) (sphere 0 1))"
proof -
have ?thesis
when "p=0"
proof -
have "card (sphere z0 r) = 0" "card (sphere (0::complex) 1) = 0"
using infinite_sphere[OF ‹r>0›,of z0] infinite_sphere[of 1 "0::complex"] by auto
then show ?thesis using that by auto
qed
moreover have ?thesis
when "p≠0"
apply (rule proots_card_pcompose_bij_eq[OF _ ‹p≠0›])
subgoal unfolding q_def using bij_betw_sphere_usphere[OF ‹r>0›,of z0]
by (auto simp:algebra_simps)
subgoal unfolding q_def using ‹r>0› by auto
done
ultimately show "card (proots_within p (sphere z0 r)) = card (proots_within (p ∘⇩p q) (sphere 0 1))"
by blast
qed

subsection ‹Combining two real polynomials into a complex one›

definition cpoly_of:: "real poly ⇒ real poly ⇒ complex poly" where
"cpoly_of pR pI = map_poly of_real pR + smult 𝗂 (map_poly of_real pI)"

lemma cpoly_of_eq_0_iff[iff]:
"cpoly_of pR pI = 0 ⟷ pR = 0 ∧ pI = 0"
proof -
have "pR = 0 ∧ pI = 0" when "cpoly_of pR pI = 0"
proof -
have "complex_of_real (coeff pR n) + 𝗂 * complex_of_real (coeff pI n) = 0" for n
using that unfolding poly_eq_iff cpoly_of_def by (auto simp:coeff_map_poly)
then have "coeff pR n = 0 ∧ coeff pI n = 0" for n
by (metis Complex_eq Im_complex_of_real Re_complex_of_real complex.sel(1) complex.sel(2)
of_real_0)
then show ?thesis unfolding poly_eq_iff by auto
qed
then show ?thesis by (auto simp:cpoly_of_def)
qed

lemma cpoly_of_decompose:
"p = cpoly_of (map_poly Re p) (map_poly Im p)"
unfolding cpoly_of_def
apply (induct p)
by (auto simp add:map_poly_pCons map_poly_map_poly complex_eq)

lemma cpoly_of_dist_right:
"cpoly_of (pR*g) (pI*g) = cpoly_of pR pI * (map_poly of_real g)"
unfolding cpoly_of_def by (simp add: distrib_right)

lemma poly_cpoly_of_real:
"poly (cpoly_of pR pI) (of_real x) = Complex (poly pR x) (poly pI x)"
unfolding cpoly_of_def by (simp add: Complex_eq of_real_poly_map_poly)

lemma poly_cpoly_of_real_iff:
shows "poly (cpoly_of pR pI) (of_real t) =0 ⟷ poly pR t = 0 ∧ poly pI t=0 "
unfolding  poly_cpoly_of_real using Complex_eq_0 by blast

lemma order_cpoly_gcd_eq:
assumes "pR≠0 ∨ pI≠0"
shows "order t (cpoly_of pR pI) = order t (gcd pR pI)"
proof -
define g where "g = gcd pR pI"
have [simp]:"g≠0" unfolding g_def using assms by auto
obtain pr pi where pri: "pR = pr * g" "pI = pi * g" "coprime pr pi"
unfolding g_def using assms(1) gcd_coprime_exists ‹g ≠ 0› g_def by blast
then have "pr ≠0 ∨ pi ≠0" using assms mult_zero_left by blast

have "order t (cpoly_of pR pI) = order t (cpoly_of pr pi * (map_poly of_real g))"
unfolding pri cpoly_of_dist_right by simp
also have "... = order t (cpoly_of pr pi) + order t g"
apply (subst order_mult)
using ‹pr ≠0 ∨ pi ≠0› by (auto simp:map_poly_order_of_real)
also have "... = order t g"
proof -
have "poly (cpoly_of pr pi) t ≠0" unfolding poly_cpoly_of_real_iff
using ‹coprime pr pi› coprime_poly_0 by blast
then have "order t (cpoly_of pr pi) = 0" by (simp add: order_0I)
then show ?thesis by auto
qed
finally show ?thesis unfolding g_def .
qed

subsection ‹Number of roots on a (bounded or unbounded) segment›

― ‹1 dimensional hyperplane›
definition unbounded_line::"'a::real_vector ⇒ 'a ⇒ 'a set" where
"unbounded_line a b = ({x. ∃u::real. x= (1 - u) *⇩R a + u *⇩R b})"

definition proots_line_card:: "complex poly ⇒ complex ⇒ complex ⇒ nat" where
"proots_line_card p st tt = card (proots_within p (open_segment st tt))"

definition proots_unbounded_line_card:: "complex poly ⇒ complex ⇒ complex ⇒ nat" where
"proots_unbounded_line_card p st tt = card (proots_within p (unbounded_line st tt))"

definition proots_unbounded_line :: "complex poly ⇒ complex ⇒ complex ⇒ nat" where
"proots_unbounded_line p st tt = proots_count p (unbounded_line st tt)"

lemma card_proots_open_segments:
assumes "poly p st ≠0" "poly p tt ≠ 0"
shows "card (proots_within p (open_segment st tt)) =
(let pc = pcompose p [:st, tt - st:];
pR = map_poly Re pc;
pI = map_poly Im pc;
g  = gcd pR pI
in changes_itv_smods 0 1 g (pderiv g))" (is "?L = ?R")
proof -
define pc pR pI g where
"pc = pcompose p [:st, tt-st:]" and
"pR = map_poly Re pc" and
"pI = map_poly Im pc" and
"g  = gcd pR pI"
have poly_iff:"poly g t=0 ⟷ poly pc t =0" for t
proof -
have "poly g t = 0 ⟷ poly pR t =0 ∧ poly pI t =0"
unfolding g_def using poly_gcd_iff by auto
also have "... ⟷ poly pc t =0"
proof -
have "cpoly_of pR pI = pc"
unfolding pc_def pR_def pI_def using cpoly_of_decompose by auto
then show ?thesis using poly_cpoly_of_real_iff by blast
qed
finally show ?thesis by auto
qed

have "?R = changes_itv_smods 0 1 g (pderiv g)"
unfolding pc_def g_def pI_def pR_def by (auto simp add:Let_def)
also have "... = card {t. poly g t = 0 ∧ 0 < t ∧ t < 1}"
proof -
have "poly g 0 ≠ 0"
using poly_iff[of 0] assms unfolding pc_def by (auto simp add:poly_pcompose)
moreover have "poly g 1 ≠ 0"
using poly_iff[of 1] assms unfolding pc_def by (auto simp add:poly_pcompose)
ultimately show ?thesis using sturm_interval[of 0 1 g] by auto
qed
also have "... = card {t::real. poly pc t = 0 ∧ 0 < t ∧ t < 1}"
unfolding poly_iff by simp
also have "... = ?L"
proof (cases "st=tt")
case True
then show ?thesis unfolding pc_def poly_pcompose using ‹poly p tt ≠ 0›
by auto
next
case False
define ff where "ff = (λt::real. st + t*(tt-st))"
define ll where "ll = {t. poly pc (complex_of_real t) = 0 ∧ 0 < t ∧ t < 1}"
have "ff  ll = proots_within p (open_segment st tt)"
proof (rule equalityI)
show "ff  ll ⊆ proots_within p (open_segment st tt)"
unfolding ll_def ff_def pc_def poly_pcompose
by (auto simp add:in_segment False scaleR_conv_of_real algebra_simps)
next
show "proots_within p (open_segment st tt) ⊆ ff  ll"
proof clarify
fix x assume asm:"x ∈ proots_within p (open_segment st tt)"
then obtain u where "0<u" and "u < 1" and u:"x = (1 - u) *⇩R st + u *⇩R tt"
then have "poly p ((1 - u) *⇩R st + u *⇩R tt) = 0" using asm by simp
then have "u ∈ ll"
unfolding ll_def pc_def poly_pcompose
by (simp add:scaleR_conv_of_real algebra_simps ‹0<u› ‹u<1›)
moreover have "x = ff u"
unfolding ff_def using u by (auto simp add:algebra_simps scaleR_conv_of_real)
ultimately show "x ∈ ff  ll" by (rule rev_image_eqI[of "u"])
qed
qed
moreover have "inj_on ff ll"
unfolding ff_def using False inj_on_def by fastforce
ultimately show ?thesis unfolding ll_def
using card_image[of ff] by fastforce
qed
finally show ?thesis by simp
qed

lemma unbounded_line_closed_segment: "closed_segment a b ⊆ unbounded_line a b"
unfolding unbounded_line_def closed_segment_def by auto

lemma card_proots_unbounded_line:
assumes "st≠tt"
shows "card (proots_within p (unbounded_line st tt)) =
(let pc = pcompose p [:st, tt - st:];
pR = map_poly Re pc;
pI = map_poly Im pc;
g  = gcd pR pI
in nat (changes_R_smods g (pderiv g)))" (is "?L = ?R")
proof -
define pc pR pI g where
"pc = pcompose p [:st, tt-st:]" and
"pR = map_poly Re pc" and
"pI = map_poly Im pc" and
"g  = gcd pR pI"
have poly_iff:"poly g t=0 ⟷ poly pc t =0" for t
proof -
have "poly g t = 0 ⟷ poly pR t =0 ∧ poly pI t =0"
unfolding g_def using poly_gcd_iff by auto
also have "... ⟷ poly pc t =0"
proof -
have "cpoly_of pR pI = pc"
unfolding pc_def pR_def pI_def using cpoly_of_decompose by auto
then show ?thesis using poly_cpoly_of_real_iff by blast
qed
finally show ?thesis by auto
qed

have "?R = nat (changes_R_smods g (pderiv g))"
unfolding pc_def g_def pI_def pR_def by (auto simp add:Let_def)
also have "... = card {t. poly g t = 0}"
using sturm_R[of g] by simp
also have "... = card {t::real. poly pc t = 0}"
unfolding poly_iff by simp
also have "... = ?L"
proof (cases "st=tt")
case True
then show ?thesis unfolding pc_def poly_pcompose unbounded_line_def using assms
next
case False
define ff where "ff = (λt::real. st + t*(tt-st))"
define ll where "ll = {t. poly pc (complex_of_real t) = 0}"
have "ff  ll = proots_within p (unbounded_line st tt)"
proof (rule equalityI)
show "ff  ll ⊆ proots_within p (unbounded_line st tt)"
unfolding ll_def ff_def pc_def poly_pcompose
by (auto simp add:unbounded_line_def False scaleR_conv_of_real algebra_simps)
next
show "proots_within p (unbounded_line st tt) ⊆ ff  ll"
proof clarify
fix x assume asm:"x ∈ proots_within p (unbounded_line st tt)"
then obtain u where u:"x = (1 - u) *⇩R st + u *⇩R tt"
then have "poly p ((1 - u) *⇩R st + u *⇩R tt) = 0" using asm by simp
then have "u ∈ ll"
unfolding ll_def pc_def poly_pcompose
moreover have "x = ff u"
unfolding ff_def using u by (auto simp add:algebra_simps scaleR_conv_of_real)
ultimately show "x ∈ ff  ll" by (rule rev_image_eqI[of "u"])
qed
qed
moreover have "inj_on ff ll"
unfolding ff_def using False inj_on_def by fastforce
ultimately show ?thesis unfolding ll_def
using card_image[of ff] by metis
qed
finally show ?thesis by simp
qed

lemma proots_unbounded_line:
assumes "st≠tt" "p≠0"
shows "(proots_count p (unbounded_line st tt)) =
(let pc = pcompose p [:st, tt - st:];
pR = map_poly Re pc;
pI = map_poly Im pc;
g  = gcd pR pI
in nat (changes_R_smods_ext g (pderiv g)))" (is "?L = ?R")
proof -
define pc pR pI g where
"pc = pcompose p [:st, tt-st:]" and
"pR = map_poly Re pc" and
"pI = map_poly Im pc" and
"g  = gcd pR pI"
have [simp]: "g≠0" "pc≠0"
proof -
show "pc≠0" using assms(1) assms(2) pc_def pcompose_eq_0 by fastforce
then have "pR≠0 ∨ pI≠0" unfolding pR_def pI_def by (metis cpoly_of_decompose map_poly_0)
then show "g≠0" unfolding g_def by simp
qed
have order_eq:"order t g = order t pc" for t
apply (subst order_cpoly_gcd_eq[of pR pI,folded g_def,symmetric])
subgoal using ‹g≠0› unfolding g_def by simp
subgoal unfolding pR_def pI_def by (simp add:cpoly_of_decompose[symmetric])
done

have "?R = nat (changes_R_smods_ext g (pderiv g))"
unfolding pc_def g_def pI_def pR_def by (auto simp add:Let_def)
also have "... = proots_count g UNIV"
using sturm_ext_R[OF ‹g≠0›] by auto
also have "... = proots_count (map_poly complex_of_real g) (of_real  UNIV)"
apply (subst proots_count_of_real)
by auto
also have "... = proots_count (map_poly complex_of_real g) {x. Im x = 0}"
apply (rule arg_cong2[where f=proots_count])
using Reals_def complex_is_Real_iff by auto
also have "... = proots_count pc {x. Im x = 0}"
apply (rule proots_count_cong)
apply (metis (mono_tags) Im_complex_of_real Re_complex_of_real ‹g ≠ 0› complex_surj
map_poly_order_of_real mem_Collect_eq order_eq)
by auto
also have "... = proots_count p (unbounded_line st tt)"
proof -
have "poly [:st, tt - st:]  {x. Im x = 0} = unbounded_line st tt"
unfolding unbounded_line_def
apply safe
subgoal for _ x
apply (rule_tac x="Re x" in exI)
by (simp add: mult.commute scaleR_complex.code times_complex.code)
subgoal for _ u
apply (rule rev_image_eqI[of "of_real u"])
by (auto simp:scaleR_conv_of_real algebra_simps)
done
then show ?thesis
unfolding pc_def
apply (subst proots_pcompose)
using ‹p≠0› ‹st≠tt› by auto
qed
finally show ?thesis by simp
qed

lemma proots_unbounded_line_card_code[code]:
"proots_unbounded_line_card p st tt =
(if st≠tt then
(let pc = pcompose p [:st, tt - st:];
pR = map_poly Re pc;
pI = map_poly Im pc;
g  = gcd pR pI
in nat (changes_R_smods g (pderiv g)))
else
Code.abort (STR ''proots_unbounded_line_card fails due to invalid hyperplanes.'')
(λ_. proots_unbounded_line_card p st tt))"
unfolding proots_unbounded_line_card_def using card_proots_unbounded_line[of st tt p] by auto

lemma proots_unbounded_line_code[code]:
"proots_unbounded_line p st tt =
( if st≠tt then
if p≠0 then
(let pc = pcompose p [:st, tt - st:];
pR = map_poly Re pc;
pI = map_poly Im pc;
g  = gcd pR pI
in nat (changes_R_smods_ext g (pderiv g)))
else
Code.abort (STR ''proots_unbounded_line fails due to p=0'')
(λ_. proots_unbounded_line p st tt)
else
Code.abort (STR ''proots_unbounded_line fails due to invalid hyperplanes.'')
(λ_. proots_unbounded_line p st tt) )"
unfolding proots_unbounded_line_def using proots_unbounded_line by auto

subsection ‹Checking if there a polynomial root on a closed segment›

definition no_proots_line::"complex poly ⇒ complex ⇒ complex ⇒ bool" where
"no_proots_line p st tt = (proots_within p (closed_segment st tt) = {})"

(*TODO: the proof can probably be simplified using Lemma card_proots_open_segments*)
lemma no_proots_line_code[code]: "no_proots_line p st tt = (if poly p st ≠0 ∧ poly p tt ≠ 0 then
(let pc = pcompose p [:st, tt - st:];
pR = map_poly Re pc;
pI = map_poly Im pc;
g  = gcd pR pI
in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False) else False)"
(is "?L = ?R")
proof (cases "poly p st ≠0 ∧ poly p tt ≠ 0")
case False
thus ?thesis unfolding no_proots_line_def by auto
next
case True
then have "poly p st ≠ 0" "poly p tt ≠ 0" by auto
define pc pR pI g where
"pc = pcompose p [:st, tt-st:]" and
"pR = map_poly Re pc" and
"pI = map_poly Im pc" and
"g  = gcd pR pI"
have poly_iff:"poly g t=0 ⟷ poly pc t =0" for t
proof -
have "poly g t = 0 ⟷ poly pR t =0 ∧ poly pI t =0"
unfolding g_def using poly_gcd_iff by auto
also have "... ⟷ poly pc t =0"
proof -
have "cpoly_of pR pI = pc"
unfolding pc_def pR_def pI_def using cpoly_of_decompose by auto
then show ?thesis using poly_cpoly_of_real_iff by blast
qed
finally show ?thesis by auto
qed
have "?R = (changes_itv_smods 0 1 g (pderiv g) = 0)"
using True unfolding pc_def g_def pI_def pR_def
also have "... = (card {x. poly g x = 0 ∧ 0 < x ∧ x < 1} = 0)"
proof -
have "poly g 0 ≠ 0"
using poly_iff[of 0] True unfolding pc_def by (auto simp add:poly_pcompose)
moreover have "poly g 1 ≠ 0"
using poly_iff[of 1] True unfolding pc_def by (auto simp add:poly_pcompose)
ultimately show ?thesis using sturm_interval[of 0 1 g] by auto
qed
also have "... = ({x. poly g x = 0 ∧ 0 < x ∧ x < 1} = {})"
proof -
have "g≠0"
proof (rule ccontr)
assume "¬ g ≠ 0"
then have "poly pc 0 =0"
using poly_iff[of 0] by auto
then show False using True unfolding pc_def by (auto simp add:poly_pcompose)
qed
from poly_roots_finite[OF this] have "finite {x. poly g x = 0 ∧ 0 < x ∧ x < 1}"
by auto
then show ?thesis using card_eq_0_iff by auto
qed
also have "... = ?L"
proof -
have "(∃t. poly g t = 0 ∧ 0 < t ∧ t < 1) ⟷ (∃t::real. poly pc t = 0 ∧ 0 < t ∧ t < 1)"
using poly_iff by auto
also have "... ⟷ (∃x. x ∈ closed_segment st tt ∧ poly p x = 0)"
proof
assume "∃t. poly pc (complex_of_real t) = 0 ∧ 0 < t ∧ t < 1"
then obtain t where *:"poly pc (of_real t) = 0" and "0 < t" "t < 1" by auto
define x where "x=poly [:st, tt - st:] t"
have "x ∈ closed_segment st tt" using ‹0<t› ‹t<1› unfolding x_def in_segment
by (intro exI[where x=t],auto simp add: algebra_simps scaleR_conv_of_real)
moreover have "poly p x=0" using * unfolding pc_def x_def
ultimately show "∃x. x ∈ closed_segment st tt ∧ poly p x = 0" by auto
next
assume "∃x. x ∈ closed_segment st tt ∧ poly p x = 0"
then obtain x where "x ∈ closed_segment st tt" "poly p x = 0" by auto
then obtain t::real where *:"x = (1 - t) *⇩R st + t *⇩R tt" and "0≤t" "t≤1"
unfolding in_segment by auto
then have "x=poly [:st, tt - st:] t" by (auto simp add: algebra_simps scaleR_conv_of_real)
then have "poly pc (complex_of_real t) = 0"
using ‹poly p x=0› unfolding pc_def by (auto simp add:poly_pcompose)
moreover have "t≠0" "t≠1" using True *  ‹poly p x=0› by auto
then have "0<t" "t<1" using ‹0≤t› ‹t≤1› by auto
ultimately show "∃t. poly pc (complex_of_real t) = 0 ∧ 0 < t ∧ t < 1" by auto
qed
finally show ?thesis
unfolding no_proots_line_def proots_within_def
by blast
qed
finally show ?thesis by simp
qed

subsection ‹Counting roots in a rectangle›

definition proots_rectangle ::"complex poly ⇒ complex ⇒ complex ⇒ nat" where
"proots_rectangle p lb ub = proots_count p (box lb ub)"

lemma closed_segment_imp_Re_Im:
fixes x::complex
assumes "x∈closed_segment lb ub"
shows "Re lb ≤ Re ub ⟹ Re lb ≤ Re x ∧ Re x ≤ Re ub"
"Im lb ≤ Im ub ⟹ Im lb ≤ Im x ∧ Im x ≤ Im ub"
proof -
obtain u where x_u:"x=(1 - u) *⇩R lb + u *⇩R ub " and "0 ≤ u" "u ≤ 1"
using assms unfolding closed_segment_def by auto
have "Re lb ≤ Re x" when "Re lb ≤ Re ub"
proof -
have "Re x = Re ((1 - u) *⇩R lb + u *⇩R ub)"
using x_u by blast
also have "... = Re (lb + u *⇩R (ub - lb))" by (auto simp add:algebra_simps)
also have "... = Re lb + u * (Re ub - Re lb)" by auto
also have "... ≥ Re lb" using ‹u≥0› ‹Re lb ≤ Re ub› by auto
finally show ?thesis .
qed
moreover have "Im lb ≤ Im x" when "Im lb ≤ Im ub"
proof -
have "Im x = Im ((1 - u) *⇩R lb + u *⇩R ub)"
using x_u by blast
also have "... = Im (lb + u *⇩R (ub - lb))" by (auto simp add:algebra_simps)
also have "... = Im lb + u * (Im ub - Im lb)" by auto
also have "... ≥ Im lb" using ‹u≥0› ‹Im lb ≤ Im ub› by auto
finally show ?thesis .
qed
moreover have "Re x ≤ Re ub" when "Re lb ≤ Re ub"
proof -
have "Re x = Re ((1 - u) *⇩R lb + u *⇩R ub)"
using x_u by blast
also have "... = (1 - u) * Re lb + u * Re ub" by auto
also have "... ≤ (1 - u) * Re ub + u * Re ub"
using ‹u≤1› ‹Re lb ≤ Re ub› by (auto simp add: mult_left_mono)
also have "... = Re ub" by (auto simp add:algebra_simps)
finally show ?thesis .
qed
moreover have "Im x ≤ Im ub" when "Im lb ≤ Im ub"
proof -
have "Im x = Im ((1 - u) *⇩R lb + u *⇩R ub)"
using x_u by blast
also have "... = (1 - u) * Im lb + u * Im ub" by auto
also have "... ≤ (1 - u) * Im ub + u * Im ub"
using ‹u≤1› ‹Im lb ≤ Im ub› by (auto simp add: mult_left_mono)
also have "... = Im ub" by (auto simp add:algebra_simps)
finally show ?thesis .
qed
ultimately show
"Re lb ≤ Re ub ⟹ Re lb ≤ Re x ∧ Re x ≤ Re ub"
"Im lb ≤ Im ub ⟹ Im lb ≤ Im x ∧ Im x ≤ Im ub"
by auto
qed

lemma closed_segment_degen_complex:
"⟦Re lb = Re ub; Im lb ≤ Im ub ⟧
⟹ x ∈ closed_segment lb ub ⟷ Re x = Re lb ∧ Im lb ≤ Im x ∧ Im x ≤ Im ub "
"⟦Im lb = Im ub; Re lb ≤ Re ub ⟧
⟹ x ∈ closed_segment lb ub ⟷ Im x = Im lb ∧ Re lb ≤ Re x ∧ Re x ≤ Re ub "
proof -
show "x ∈ closed_segment lb ub ⟷ Re x = Re lb ∧ Im lb ≤ Im x ∧ Im x ≤ Im ub"
when "Re lb = Re ub" "Im lb ≤ Im ub"
proof
show "Re x = Re lb ∧ Im lb ≤ Im x ∧ Im x ≤ Im ub" when "x ∈ closed_segment lb ub"
using closed_segment_imp_Re_Im[OF that] ‹Re lb = Re ub› ‹Im lb ≤ Im ub› by fastforce
next
assume asm:"Re x = Re lb ∧ Im lb ≤ Im x ∧ Im x ≤ Im ub"
define u where "u=(Im x - Im lb)/ (Im ub - Im lb)"
have "x = (1 - u) *⇩R lb + u *⇩R ub"
unfolding u_def using asm ‹Re lb = Re ub› ‹Im lb ≤ Im ub›
apply (intro complex_eqI)
apply (cases "Im ub - Im lb =0")
done
moreover have "0≤u" "u≤1" unfolding u_def
using ‹Im lb ≤ Im ub› asm
by (cases "Im ub - Im lb =0",auto simp add:field_simps)+
ultimately show "x ∈ closed_segment lb ub" unfolding closed_segment_def by auto
qed
show "x ∈ closed_segment lb ub ⟷ Im x = Im lb ∧ Re lb ≤ Re x ∧ Re x ≤ Re ub"
when "Im lb = Im ub" "Re lb ≤ Re ub"
proof
show "Im x = Im lb ∧ Re lb ≤ Re x ∧ Re x ≤ Re ub" when "x ∈ closed_segment lb ub"
using closed_segment_imp_Re_Im[OF that] ‹Im lb = Im ub› ‹Re lb ≤ Re ub› by fastforce
next
assume asm:"Im x = Im lb ∧ Re lb ≤ Re x ∧ Re x ≤ Re ub"
define u where "u=(Re x - Re lb)/ (Re ub - Re lb)"
have "x = (1 - u) *⇩R lb + u *⇩R ub"
unfolding u_def using asm ‹Im lb = Im ub› ‹Re lb ≤ Re ub›
apply (intro complex_eqI)
apply (cases "Re ub - Re lb =0")
done
moreover have "0≤u" "u≤1" unfolding u_def
using ‹Re lb ≤ Re ub› asm
by (cases "Re ub - Re lb =0",auto simp add:field_simps)+
ultimately show "x ∈ closed_segment lb ub" unfolding closed_segment_def by auto
qed
qed

lemma complex_box_ne_empty:
fixes a b::complex
shows
"cbox a b ≠ {} ⟷ (Re a ≤ Re b ∧ Im a ≤ Im b)"
"box a b ≠ {} ⟷ (Re a < Re b ∧ Im a < Im b)"

lemma proots_rectangle_code1:
"proots_rectangle p lb ub = (if Re lb < Re ub ∧ Im lb < Im ub then
if p≠0 then
if no_proots_line p lb (Complex (Re ub) (Im lb))
∧ no_proots_line p (Complex (Re ub) (Im lb)) ub
∧ no_proots_line p ub (Complex (Re lb) (Im ub))
∧ no_proots_line p (Complex (Re lb) (Im ub)) lb then
(
let p1 = pcompose p [:lb,  Complex (Re ub - Re lb) 0:];
pR1 = map_poly Re p1; pI1 = map_poly Im p1; gc1 = gcd pR1 pI1;
p2 = pcompose p [:Complex (Re ub) (Im lb), Complex 0 (Im ub - Im lb):];
pR2 = map_poly Re p2; pI2 = map_poly Im p2; gc2 = gcd pR2 pI2;
p3 = pcompose p [:ub, Complex (Re lb - Re ub) 0:];
pR3 = map_poly Re p3; pI3 = map_poly Im p3; gc3 = gcd pR3 pI3;
p4 = pcompose p [:Complex (Re lb) (Im ub), Complex 0 (Im lb - Im ub):];
pR4 = map_poly Re p4; pI4 = map_poly Im p4; gc4 = gcd pR4 pI4
in
nat (- (changes_alt_itv_smods 0 1 (pR1 div gc1) (pI1 div gc1)
+ changes_alt_itv_smods 0 1 (pR2 div gc2) (pI2 div gc2)
+ changes_alt_itv_smods 0 1 (pR3 div gc3) (pI3 div gc3)
+ changes_alt_itv_smods 0 1 (pR4 div gc4) (pI4 div gc4))  div 4)
)
else Code.abort (STR ''proots_rectangle fails when there is a root on the border.'')
(λ_. proots_rectangle p lb ub)
else Code.abort (STR ''proots_rectangle fails when p=0.'')
(λ_. proots_rectangle p lb ub)
else 0)"
proof -
have ?thesis when "¬ (Re lb < Re ub ∧ Im lb < Im ub)"
proof -
have "box lb ub = {}" using complex_box_ne_empty[of lb ub] that by auto
then have "proots_rectangle p lb ub = 0" unfolding proots_rectangle_def by auto
then show ?thesis by (simp add:that)
qed
moreover have ?thesis when "Re lb < Re ub ∧ Im lb < Im ub" "p=0"
using that by simp
moreover have ?thesis when
"Re lb < Re ub" "Im lb < Im ub" "p≠0"
and no_proots:
"no_proots_line p lb (Complex (Re ub) (Im lb))"
"no_proots_line p (Complex (Re ub) (Im lb)) ub"
"no_proots_line p ub (Complex (Re lb) (Im ub))"
"no_proots_line p (Complex (Re lb) (Im ub)) lb"
proof -
define l1 where "l1 = linepath lb (Complex (Re ub) (Im lb))"
define l2 where "l2 = linepath (Complex (Re ub) (Im lb)) ub"
define l3 where "l3 = linepath ub (Complex (Re lb) (Im ub))"
define l4 where "l4 = linepath (Complex (Re lb) (Im ub)) lb"
define rec where "rec = l1 +++ l2 +++ l3 +++ l4"
have valid[simp]:"valid_path rec" and loop[simp]:"pathfinish rec = pathstart rec"
unfolding rec_def l1_def l2_def l3_def l4_def by auto
have path_no_proots:"path_image rec ∩ proots p = {}"
unfolding rec_def l1_def l2_def l3_def l4_def
apply (subst path_image_join,simp_all del:Complex_eq)+
using no_proots[unfolded no_proots_line_def] by (auto simp del:Complex_eq)

define g1 where "g1 = poly p o l1"
define g2 where "g2 = poly p o l2"
define g3 where "g3 = poly p o l3"
define g4 where "g4 = poly p o l4"
have [simp]: "path g1" "path g2" "path g3" "path g4"
"pathfinish g1 = pathstart g2" "pathfinish g2 = pathstart g3" "pathfinish g3 = pathstart g4"
"pathfinish g4 = pathstart g1"
unfolding g1_def g2_def g3_def g4_def l1_def l2_def l3_def l4_def
by (auto intro!: path_continuous_image continuous_intros
have [simp]: "finite_ReZ_segments g1 0" "finite_ReZ_segments g2 0"
"finite_ReZ_segments g3 0" "finite_ReZ_segments g4 0"
unfolding g1_def l1_def g2_def l2_def g3_def l3_def g4_def l4_def poly_linepath_comp
by (rule finite_ReZ_segments_poly_of_real)+
define p1 pR1 pI1 gc1
p2 pR2 pI2 gc2
p3 pR3 pI3 gc3
p4 pR4 pI4 gc4
where "p1 = pcompose p [:lb,  Complex (Re ub - Re lb) 0:]"
and "pR1 = map_poly Re p1" and "pI1 = map_poly Im p1" and "gc1 = gcd pR1 pI1"
and "p2 = pcompose p [:Complex (Re ub) (Im lb), Complex 0 (Im ub - Im lb):]"
and "pR2 = map_poly Re p2" and "pI2 = map_poly Im p2" and "gc2 = gcd pR2 pI2"
and "p3 = pcompose p [:ub, Complex (Re lb - Re ub) 0:]"
and "pR3 = map_poly Re p3" and "pI3 = map_poly Im p3" and "gc3 = gcd pR3 pI3"
and "p4 = pcompose p [:Complex (Re lb) (Im ub), Complex 0 (Im lb - Im ub):]"
and "pR4 = map_poly Re p4" and "pI4 = map_poly Im p4" and "gc4 = gcd pR4 pI4"
have "gc1≠0" "gc2≠0" "gc3≠0" "gc4≠0"
proof -
show "gc1≠0"
proof (rule ccontr)
assume "¬ gc1 ≠ 0"
then have "pI1 = 0" "pR1 = 0" unfolding gc1_def by auto
then have "p1 = 0" unfolding pI1_def pR1_def
by (metis cpoly_of_decompose map_poly_0)
then have "p=0" unfolding p1_def using ‹Re lb < Re ub›
then show False using ‹p≠0› by simp
qed
show "gc2≠0"
proof (rule ccontr)
assume "¬ gc2 ≠ 0"
then have "pI2 = 0" "pR2 = 0" unfolding gc2_def by auto
then have "p2 = 0" unfolding pI2_def pR2_def
by (metis cpoly_of_decompose map_poly_0)
then have "p=0" unfolding p2_def using ‹Im lb < Im ub›
then show False using ‹p≠0› by simp
qed
show "gc3≠0"
proof (rule ccontr)
assume "¬ gc3 ≠ 0"
then have "pI3 = 0" "pR3 = 0" unfolding gc3_def by auto
then have "p3 = 0" unfolding pI3_def pR3_def
by (metis cpoly_of_decompose map_poly_0)
then have "p=0" unfolding p3_def using ‹Re lb < Re ub›
then show False using ‹p≠0› by simp
qed
show "gc4≠0"
proof (rule ccontr)
assume "¬ gc4 ≠ 0"
then have "pI4 = 0" "pR4 = 0" unfolding gc4_def by auto
then have "p4 = 0" unfolding pI4_def pR4_def
by (metis cpoly_of_decompose map_poly_0)
then have "p=0" unfolding p4_def using ‹Im lb < Im ub›
then show False using ‹p≠0› by simp
qed
qed
define sms where
"sms = (changes_alt_itv_smods 0 1 (pR1 div gc1) (pI1 div gc1)
+ changes_alt_itv_smods 0 1 (pR2 div gc2) (pI2 div gc2)
+ changes_alt_itv_smods 0 1 (pR3 div gc3) (pI3 div gc3)
+ changes_alt_itv_smods 0 1 (pR4 div gc4) (pI4 div gc4))"
have "proots_rectangle p lb ub = (∑r∈proots p. winding_number rec r * (order r p))"
proof -
have "winding_number rec x * of_nat (order x p) = 0"
when "x∈proots p - proots_within p (box lb ub)" for x
proof -
have *:"cbox lb ub = box lb ub ∪ path_image rec"
proof -
have "x∈cbox lb ub" when "x∈box lb ub ∪ path_image rec" for x
using that ‹Re lb<Re ub› ‹Im lb<Im ub›
unfolding box_def cbox_def Basis_complex_def rec_def l1_def l2_def l3_def l4_def
apply (subst (asm) closed_segment_commute,simp add: closed_segment_degen_complex)+
done
moreover have "x∈box lb ub ∪ path_image rec" when "x∈cbox lb ub" for x
using that
unfolding box_def cbox_def Basis_complex_def rec_def l1_def l2_def l3_def l4_def
apply (subst (asm) (1 2) closed_segment_commute,simp add:closed_segment_degen_complex)+
done
ultimately show ?thesis by auto
qed
moreover have "x∉path_image rec"
using path_no_proots that by auto
ultimately have "x∉cbox lb ub" using that by simp
from winding_number_zero_outside[OF valid_path_imp_path[OF valid] _ loop this,simplified] *
have "winding_number rec x = 0" by auto
then show ?thesis by auto
qed
moreover have "of_nat (order x p) = winding_number rec x * of_nat (order x p)" when
"x ∈ proots_within p (box lb ub)" for x
proof -
have "x∈box lb ub" using that unfolding proots_within_def by auto
then have order_asms:"Re lb < Re x" "Re x < Re ub" "Im lb < Im x" "Im x < Im ub"
have "winding_number rec x = 1"
unfolding rec_def l1_def l2_def l3_def l4_def
proof eval_winding
let ?l1 = "linepath lb (Complex (Re ub) (Im lb))"
and ?l2 = "linepath (Complex (Re ub) (Im lb)) ub"
and ?l3 = "linepath ub (Complex (Re lb) (Im ub))"
and ?l4 = "linepath (Complex (Re lb) (Im ub)) lb"
show l1: "x ∉ path_image ?l1" and l2: "x ∉ path_image ?l2" and
l3: "x ∉ path_image ?l3" and l4:"x ∉ path_image ?l4"
using no_proots that unfolding no_proots_line_def by auto
show "- of_real (cindex_pathE ?l1 x + (cindex_pathE ?l2 x +
(cindex_pathE ?l3 x + cindex_pathE ?l4 x))) = 2 * 1"
proof -
have "(Im x - Im ub) * (Re ub - Re lb) < 0"
using mult_less_0_iff order_asms(1) order_asms(2) order_asms(4) by fastforce
then have "cindex_pathE ?l3 x = -1"
apply (subst cindex_pathE_linepath)
using l3 by (auto simp add:algebra_simps order_asms)
moreover have "(Im lb - Im x) * (Re ub - Re lb) <0"
using mult_less_0_iff order_asms(1) order_asms(2) order_asms(3) by fastforce
then have "cindex_pathE ?l1 x = -1"
apply (subst cindex_pathE_linepath)
using l1 by (auto simp add:algebra_simps order_asms)
moreover have "cindex_pathE ?l2 x = 0"
apply (subst cindex_pathE_linepath)
using l2 order_asms by auto
moreover have "cindex_pathE ?l4 x = 0"
apply (subst cindex_pathE_linepath)
using l4 order_asms by auto
ultimately show ?thesis by auto
qed
qed
then show ?thesis by auto
qed
ultimately show ?thesis using ‹p≠0›
unfolding proots_rectangle_def proots_count_def
by (auto intro!: sum.mono_neutral_cong_left[of "proots p" "proots_within p (box lb ub)"])
qed
also have "... = 1/(2 * of_real pi * 𝗂) *contour_integral rec (λx. deriv (poly p) x / poly p x)"
proof -
have "contour_integral rec (λx. deriv (poly p) x / poly p x) = 2 * of_real pi * 𝗂
* (∑x | poly p x = 0. winding_number rec x * of_int (zorder (poly p) x))"
proof (rule argument_principle[of UNIV "poly p" "{}" "λ_. 1" rec,simplified])
show "connected (UNIV::complex set)" using connected_UNIV[where 'a=complex] .
show "path_image rec ⊆ UNIV - {x. poly p x = 0}"
using path_no_proots unfolding proots_within_def by auto
show "finite {x. poly p x = 0}" by (simp add: poly_roots_finite that(3))
qed
also have " ... = 2 * of_real pi * 𝗂 * (∑x∈proots p. winding_number rec x * (order x p))"
unfolding proots_within_def
apply (auto intro!:sum.cong simp add:order_zorder[OF ‹p≠0›] )
by (metis nat_eq_iff2 of_nat_nat order_root order_zorder that(3))
finally show ?thesis by auto
qed
also have "... = winding_number (poly p ∘ rec) 0"
proof -
have "0 ∉ path_image (poly p ∘ rec)"
using path_no_proots unfolding path_image_compose proots_within_def by fastforce
from winding_number_comp[OF _ poly_holomorphic_on _ _ this,of UNIV,simplified]
show ?thesis by auto
qed
also have winding_eq:"... = - cindex_pathE (poly p ∘ rec) 0 / 2"
proof (rule winding_number_cindex_pathE)
show "finite_ReZ_segments (poly p ∘ rec) 0"
unfolding rec_def path_compose_join
apply (fold g1_def g2_def g3_def g4_def)
by (auto intro!: finite_ReZ_segments_joinpaths path_join_imp)
show "valid_path (poly p ∘ rec)"
by (rule valid_path_compose_holomorphic[where S=UNIV]) auto
show "0 ∉ path_image (poly p ∘ rec)"
using path_no_proots unfolding path_image_compose proots_def by fastforce
show "pathfinish (poly p ∘ rec) = pathstart (poly p ∘ rec)"
unfolding rec_def pathstart_compose pathfinish_compose  by (auto simp add:l1_def l4_def)
qed
also have cindex_pathE_eq:"... = of_int (- sms) / of_int 4"
proof -
have "cindex_pathE (poly p ∘ rec) 0 = cindex_pathE (g1+++g2+++g3+++g4) 0"
unfolding rec_def path_compose_join g1_def g2_def g3_def g4_def by simp
also have "... = cindex_pathE g1 0 + cindex_pathE g2 0 + cindex_pathE g3 0`