# Theory Cauchy_Index_Theorem

theory Cauchy_Index_Theorem
imports Missing_Transcendental Missing_Analysis
```(*
Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
*)

section ‹Cauchy's index theorem›

theory Cauchy_Index_Theorem imports
"HOL-Complex_Analysis.Complex_Analysis"
"Sturm_Tarski.Sturm_Tarski"
"HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
Missing_Transcendental
Missing_Algebraic
Missing_Analysis
begin

text ‹This theory formalises Cauchy indices on the complex plane and relate them to winding numbers›

subsection ‹Misc›

(*refined version of the library one with the same name by dropping unnecessary assumptions*)
lemma atMostAtLeast_subset_convex:
fixes C :: "real set"
assumes "convex C"
and "x ∈ C" "y ∈ C"
shows "{x .. y} ⊆ C"
proof safe
fix z assume z: "z ∈ {x .. y}"
have "z ∈ C" if *: "x < z" "z < y"
proof -
let ?μ = "(y - z) / (y - x)"
have "0 ≤ ?μ" "?μ ≤ 1"
using assms * by (auto simp: field_simps)
then have comb: "?μ * x + (1 - ?μ) * y ∈ C"
using assms iffD1[OF convex_alt, rule_format, of C y x ?μ]
have "?μ * x + (1 - ?μ) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y"
by (auto simp: field_simps)
also have "… = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)"
using * by (simp only: add_divide_distrib) (auto simp: field_simps)
also have "… = z"
using assms * by (auto simp: field_simps)
finally show ?thesis
using comb by auto
qed
then show "z ∈ C"
using z assms by (auto simp: le_less)
qed

lemma arg_elim:
"f x ⟹ x= y ⟹ f y"
by auto

lemma arg_elim2:
"f x1 x2 ⟹ x1= y1 ⟹x2=y2 ⟹ f y1 y2"
by auto

lemma arg_elim3:
"⟦f x1 x2 x3;x1= y1;x2=y2;x3=y3 ⟧ ⟹ f y1 y2 y3"
by auto

lemma IVT_strict:
fixes f :: "'a::linear_continuum_topology ⇒ 'b::linorder_topology"
assumes "(f a > y ∧ y > f b) ∨ (f a < y ∧ y < f b)" "a<b" "continuous_on {a .. b} f"
shows "∃x. a < x ∧ x < b ∧ f x = y"
by (metis IVT' IVT2' assms(1) assms(2) assms(3) linorder_neq_iff order_le_less order_less_imp_le)

lemma (in dense_linorder) atLeastAtMost_subseteq_greaterThanLessThan_iff:
"{a .. b} ⊆ { c <..< d } ⟷ (a ≤ b ⟶ c < a ∧ b < d)"
using dense[of "a" "min c b"] dense[of "max a d" "b"]
by (force simp: subset_eq Ball_def not_less[symmetric])

lemma Re_winding_number_half_right:
assumes "∀p∈path_image γ. Re p ≥ Re z" and "valid_path γ" and  "z∉path_image γ"
shows "Re(winding_number γ z) = (Im (Ln (pathfinish γ - z)) - Im (Ln (pathstart γ - z)))/(2*pi)"
proof -
define g where "g=(λt. γ t - z)"
define st fi where "st≡pathstart g" and "fi≡pathfinish g"
have "valid_path g" "0∉path_image g" and pos_img:"∀p∈path_image g. Re p ≥ 0" unfolding g_def
subgoal using assms(2) by auto
subgoal using assms(3) by auto
subgoal using assms(1) by fastforce
done
have "(inverse has_contour_integral Ln fi - Ln st) g"
unfolding fi_def st_def
proof (rule contour_integral_primitive[OF _ ‹valid_path g›,of " - ℝ⇩≤⇩0"])
fix x::complex assume "x ∈ - ℝ⇩≤⇩0"
then have "(Ln has_field_derivative inverse x) (at x)" using has_field_derivative_Ln
by auto
then show "(Ln has_field_derivative inverse x) (at x within - ℝ⇩≤⇩0)"
using has_field_derivative_at_within by auto
next
show "path_image g ⊆ - ℝ⇩≤⇩0" using pos_img ‹0∉path_image g›
by (metis ComplI antisym assms(3) complex_nonpos_Reals_iff complex_surj
subsetI zero_complex.code)
qed
then have winding_eq:"2*pi*𝗂*winding_number g 0 = (Ln fi - Ln st)"
using has_contour_integral_winding_number[OF ‹valid_path g› ‹0∉path_image g›
,simplified,folded inverse_eq_divide] has_contour_integral_unique
by auto
have "Re(winding_number g 0)
= (Im (Ln fi) - Im (Ln st))/(2*pi)"
(is "?L=?R")
proof -
have "?L = Re((Ln fi - Ln st)/(2*pi*𝗂))"
using winding_eq[symmetric] by auto
also have "... = ?R"
by (metis Im_divide_of_real Im_i_times complex_i_not_zero minus_complex.simps(2)
mult.commute mult_divide_mult_cancel_left_if times_divide_eq_right)
finally show ?thesis .
qed
then show ?thesis unfolding g_def fi_def st_def using winding_number_offset by simp
qed

lemma Re_winding_number_half_upper:
assumes pimage:"∀p∈path_image γ. Im p ≥ Im z" and "valid_path γ" and "z∉path_image γ"
shows "Re(winding_number γ z) =
(Im (Ln (𝗂*z - 𝗂*pathfinish γ)) - Im (Ln (𝗂*z - 𝗂*pathstart γ )))/(2*pi)"
proof -
define γ' where "γ'=(λt. - 𝗂 * (γ t - z) + z)"
have "Re (winding_number γ' z) = (Im (Ln (pathfinish γ' - z)) - Im (Ln (pathstart γ' - z))) / (2 * pi)"
unfolding γ'_def
apply (rule Re_winding_number_half_right)
subgoal using pimage unfolding path_image_def by auto
subgoal
apply (rule valid_path_compose_holomorphic[OF ‹valid_path γ›,of "λx. -𝗂 * (x-z) + z" UNIV
, unfolded comp_def])
by (auto intro!:holomorphic_intros)
subgoal using ‹z∉path_image γ› unfolding path_image_def by auto
done
moreover have "winding_number γ' z = winding_number γ z"
proof -
define f where "f=(λx. -𝗂 * (x-z) + z)"
define c where "c= 1 / (complex_of_real (2 * pi) * 𝗂)"
have "winding_number γ' z = winding_number (f o γ) z"
unfolding γ'_def comp_def f_def by auto
also have "... = c * contour_integral γ (λw. deriv f w / (f w - z))" unfolding c_def
proof (rule winding_number_comp[of UNIV])
show "z ∉ path_image (f ∘ γ)" using ‹z∉path_image γ› unfolding f_def path_image_def by auto
qed (auto simp add:f_def ‹valid_path γ› intro!:holomorphic_intros)
also have "... = c * contour_integral γ (λw.  1 / (w - z))"
proof -
have "deriv f x = -𝗂" for x
unfolding f_def
by (auto intro!:derivative_eq_intros DERIV_imp_deriv)
then show ?thesis
unfolding f_def c_def
by (auto simp add:field_simps divide_simps intro!:arg_cong2[where f=contour_integral])
qed
also have "... = winding_number γ z"
using winding_number_valid_path[OF ‹valid_path γ› ‹z∉path_image γ›,folded c_def] by simp
finally show ?thesis .
qed
moreover have "pathfinish γ' = z+ 𝗂*z -𝗂* pathfinish γ" "pathstart γ' = z+ 𝗂*z -𝗂*pathstart γ"
unfolding γ'_def path_defs by (auto simp add:algebra_simps)
ultimately show ?thesis by auto
qed

lemma Re_winding_number_half_lower:
assumes pimage:"∀p∈path_image γ. Im p ≤ Im z" and "valid_path γ" and "z∉path_image γ"
shows "Re(winding_number γ z) =
(Im (Ln ( 𝗂*pathfinish γ - 𝗂*z)) - Im (Ln (𝗂*pathstart γ - 𝗂*z)))/(2*pi)"
proof -
define γ' where "γ'=(λt. 𝗂 * (γ t - z) + z)"
have "Re (winding_number γ' z) = (Im (Ln (pathfinish γ' - z)) - Im (Ln (pathstart γ' - z))) / (2 * pi)"
unfolding γ'_def
apply (rule Re_winding_number_half_right)
subgoal using pimage unfolding path_image_def by auto
subgoal
apply (rule valid_path_compose_holomorphic[OF ‹valid_path γ›,of "λx. 𝗂 * (x-z) + z" UNIV
, unfolded comp_def])
by (auto intro!:holomorphic_intros)
subgoal using ‹z∉path_image γ› unfolding path_image_def by auto
done
moreover have "winding_number γ' z = winding_number γ z"
proof -
define f where "f=(λx. 𝗂 * (x-z) + z)"
define c where "c= 1 / (complex_of_real (2 * pi) * 𝗂)"
have "winding_number γ' z = winding_number (f o γ) z"
unfolding γ'_def comp_def f_def by auto
also have "... = c * contour_integral γ (λw. deriv f w / (f w - z))" unfolding c_def
proof (rule winding_number_comp[of UNIV])
show "z ∉ path_image (f ∘ γ)" using ‹z∉path_image γ› unfolding f_def path_image_def by auto
qed (auto simp add:f_def ‹valid_path γ› intro!:holomorphic_intros)
also have "... = c * contour_integral γ (λw.  1 / (w - z))"
proof -
have "deriv f x = 𝗂" for x
unfolding f_def
by (auto intro!:derivative_eq_intros DERIV_imp_deriv)
then show ?thesis
unfolding f_def c_def
by (auto simp add:field_simps divide_simps intro!:arg_cong2[where f=contour_integral])
qed
also have "... = winding_number γ z"
using winding_number_valid_path[OF ‹valid_path γ› ‹z∉path_image γ›,folded c_def] by simp
finally show ?thesis .
qed
moreover have "pathfinish γ' = z+ 𝗂* pathfinish γ - 𝗂*z" "pathstart γ' = z+ 𝗂*pathstart γ - 𝗂*z"
unfolding γ'_def path_defs by (auto simp add:algebra_simps)
ultimately show ?thesis by auto
qed

lemma Re_winding_number_half_left:
assumes neg_img:"∀p∈path_image γ. Re p ≤ Re z" and "valid_path γ" and "z∉path_image γ"
shows "Re(winding_number γ z) = (Im (Ln (z - pathfinish γ)) - Im (Ln (z - pathstart γ )))/(2*pi)"
proof -
define γ' where "γ'≡(λt. 2*z - γ t)"
have "Re (winding_number γ' z) = (Im (Ln (pathfinish γ' - z)) - Im (Ln (pathstart γ' - z))) / (2 * pi)"
unfolding γ'_def
apply (rule Re_winding_number_half_right)
subgoal using neg_img unfolding path_image_def by auto
subgoal
apply (rule valid_path_compose_holomorphic[OF ‹valid_path γ›,of "λt. 2*z-t" UNIV,
unfolded comp_def])
by (auto intro:holomorphic_intros)
subgoal using ‹z∉path_image γ› unfolding path_image_def by auto
done
moreover have "winding_number γ' z = winding_number γ z"
proof -
define f where "f=(λt. 2*z-t)"
define c where "c= 1 / (complex_of_real (2 * pi) * 𝗂)"
have "winding_number γ' z = winding_number (f o γ) z"
unfolding γ'_def comp_def f_def by auto
also have "... = c * contour_integral γ (λw. deriv f w / (f w - z))" unfolding c_def
proof (rule winding_number_comp[of UNIV])
show "z ∉ path_image (f ∘ γ)" using ‹z∉path_image γ› unfolding f_def path_image_def by auto
qed (auto simp add:f_def ‹valid_path γ› intro:holomorphic_intros)
also have "... = c * contour_integral γ (λw.  1 / (w - z))"
unfolding f_def c_def
by (auto simp add:field_simps divide_simps intro!:arg_cong2[where f=contour_integral])
also have "... = winding_number γ z"
using winding_number_valid_path[OF ‹valid_path γ› ‹z∉path_image γ›,folded c_def] by simp
finally show ?thesis .
qed
moreover have "pathfinish γ' = 2*z - pathfinish γ" "pathstart γ' = 2*z - pathstart γ"
unfolding γ'_def path_defs by auto
ultimately show ?thesis by auto
qed

lemma continuous_on_open_Collect_neq:
fixes f g :: "'a::topological_space ⇒ 'b::t2_space"
assumes f: "continuous_on S f" and g: "continuous_on S g" and "open S"
shows "open {x∈S. f x ≠ g x}"
proof (rule topological_space_class.openI)
fix t
assume "t ∈ {x∈S. f x ≠ g x}"
then obtain U0 V0 where "open U0" "open V0" "f t ∈ U0" "g t ∈ V0" "U0 ∩ V0 = {}" "t∈S"
obtain U1 where "open U1" "t ∈ U1" "∀y∈(S ∩ U1). f y ∈ U0"
using f[unfolded continuous_on_topological,rule_format,OF ‹t∈S› ‹open U0› ‹f t ∈U0›] by auto
obtain V1 where "open V1" "t ∈ V1" "∀y∈(S ∩ V1). g y ∈ V0"
using g[unfolded continuous_on_topological,rule_format,OF ‹t∈S› ‹open V0› ‹g t ∈V0›] by auto
define T where "T=V1 ∩ U1 ∩ S"
have "open T" unfolding T_def using ‹open U1› ‹open V1› ‹open S› by auto
moreover have "t ∈ T" unfolding T_def using ‹t∈U1› ‹t∈V1› ‹t∈S› by auto
moreover have "T ⊆ {x ∈ S. f x ≠ g x}" unfolding T_def
using ‹U0 ∩ V0 = {}› ‹∀y∈S ∩ U1. f y ∈ U0› ‹∀y∈S ∩ V1. g y ∈ V0› by auto
ultimately show "∃T. open T ∧ t ∈ T ∧ T ⊆ {x ∈ S. f x ≠ g x}" by auto
qed

subsection ‹Sign at a filter›

(*Relaxation in types could be done in the future.*)
definition has_sgnx::"(real ⇒ real) ⇒ real ⇒ real filter ⇒ bool"
(infixr "has'_sgnx" 55) where
"(f has_sgnx c) F= (eventually (λx. sgn(f x) = c) F)"

definition sgnx_able (infixr "sgnx'_able" 55) where
"(f sgnx_able F) = (∃c. (f has_sgnx c) F)"

definition sgnx where
"sgnx f F = (SOME c. (f has_sgnx c) F)"

lemma has_sgnx_eq_rhs: "(f has_sgnx x) F ⟹ x = y ⟹ (f has_sgnx y) F"
by simp

named_theorems sgnx_intros "introduction rules for has_sgnx"
setup ‹
fn context =>
Named_Theorems.get (Context.proof_of context) @{named_theorems sgnx_intros}
|> map_filter (try (fn thm => @{thm has_sgnx_eq_rhs} OF [thm])))
›

lemma sgnx_able_sgnx:"f sgnx_able F ⟹ (f has_sgnx (sgnx f F)) F"
unfolding sgnx_able_def sgnx_def using someI_ex by metis

lemma has_sgnx_imp_sgnx_able[elim]:
"(f has_sgnx c) F ⟹ f sgnx_able F"
unfolding sgnx_able_def by auto

lemma has_sgnx_unique:
assumes "F≠bot" "(f has_sgnx c1) F" "(f has_sgnx c2) F"
shows "c1=c2"
proof (rule ccontr)
assume "c1 ≠ c2 "
have "eventually (λx. sgn(f x) = c1 ∧ sgn(f x) = c2) F"
using assms  unfolding has_sgnx_def eventually_conj_iff by simp
then have "eventually (λ_. c1 = c2) F" by (elim eventually_mono,auto)
then have "eventually (λ_. False) F" using ‹c1 ≠ c2› by auto
then show False using ‹F ≠ bot› eventually_False by auto
qed

lemma has_sgnx_imp_sgnx[elim]:
"(f has_sgnx c) F ⟹F≠bot ⟹ sgnx f F = c"
using has_sgnx_unique sgnx_def by auto

lemma has_sgnx_const[simp,sgnx_intros]:
"((λ_. c) has_sgnx sgn c) F"

lemma finite_sgnx_at_left_at_right:
assumes "finite {t. f t=0 ∧ a<t ∧ t<b}" "continuous_on ({a<..<b} - s) f" "finite s"
and x:"x∈{a<..<b}"
shows "f sgnx_able (at_left x)" "sgnx f (at_left x)≠0"
"f sgnx_able (at_right x)" "sgnx f (at_right x)≠0"
proof -
define ls where "ls ≡ {t. (f t=0 ∨ t∈s) ∧ a<t ∧t<x }"
define l where "l≡(if ls = {} then (a+x)/2 else (Max ls + x)/2)"
have "finite ls"
proof -
have "{t. f t=0 ∧ a<t ∧ t<x} ⊆ {t. f t=0 ∧ a<t ∧ t<b}" using x by auto
then have "finite {t. f t=0 ∧ a<t ∧ t<x}" using assms(1)
using finite_subset by blast
moreover have "finite {t. t∈s ∧ a<t ∧ t<x}" using assms(3) by auto
moreover have "ls = {t. f t=0 ∧ a<t ∧ t<x} ∪ {t. t∈s ∧ a<t ∧ t<x}"
unfolding ls_def by auto
ultimately show ?thesis by auto
qed
have [simp]: "l<x" "a<l" "l<b"
proof -
have "l<x ∧ a<l ∧ l<b" when "ls = {}"
using that x unfolding l_def by auto
moreover have "l<x ∧ a<l ∧ l<b" when "ls ≠{}"
proof -
have "Max ls ∈ ls" using assms(1,3) that ‹finite ls›
apply (intro linorder_class.Max_in)
by auto
then have "a<Max ls ∧ Max ls < x" unfolding ls_def by auto
then show ?thesis unfolding l_def using that x by auto
qed
ultimately show "l<x" "a<l" "l<b" by auto
qed
have noroot:"f t≠0" when t:"t∈{l..<x}" for t
proof (cases "ls = {}")
case True
have False when "f t=0"
proof -
have "t>a" using t ‹l>a› by (meson atLeastLessThan_iff less_le_trans)
then have "t∈ls" using that t unfolding ls_def by auto
then show False using True by auto
qed
then show ?thesis by auto
next
case False
have "t>Max ls" using that False ‹l<x› unfolding l_def by auto
have False when "f t=0"
proof -
have "t>a" using t ‹l>a› by (meson atLeastLessThan_iff less_le_trans)
then have "t∈ls" using that t unfolding ls_def by auto
then have "t≤Max ls" using ‹finite ls› by auto
then show False using ‹t>Max ls› by auto
qed
then show ?thesis by auto
qed
have "(f has_sgnx sgn (f l)) (at_left x)" unfolding has_sgnx_def
proof (rule eventually_at_leftI[OF _ ‹l<x›])
fix t assume t:"t∈{l<..<x}"
then have [simp]:"t>a" "t<b" using ‹l>a› x
by (meson greaterThanLessThan_iff less_trans)+
have False when "f t = 0"
using noroot t that by auto
moreover have False when "f l=0"
using noroot t that by auto
moreover have False when "f l>0 ∧ f t<0 ∨ f l <0 ∧ f t >0"
proof -
have False when "{l..t} ∩ s ≠{}"
proof -
obtain t' where t':"t'∈{l..t}" "t'∈s"
using ‹{l..t} ∩ s ≠ {}› by blast
then have "a<t' ∧ t'<x"
by (metis ‹a < l› atLeastAtMost_iff greaterThanLessThan_iff le_less less_trans t)
then have "t'∈ls" unfolding ls_def using ‹t'∈s› by auto
then have "t'≤Max ls" using ‹finite ls› by auto
moreover have "Max ls<l"
using ‹l<x› ‹t'∈ls› ‹finite ls› unfolding l_def by (auto simp add:ls_def )
ultimately show False using t'(1) by auto
qed
moreover have "{l..t} ⊆ {a<..<b}"
by (intro atMostAtLeast_subset_convex,auto)
ultimately have "continuous_on {l..t} f" using assms(2)
by (elim continuous_on_subset,auto)
then have "∃x>l. x < t ∧ f x = 0"
apply (intro IVT_strict)
using that t assms(2) by auto
then obtain t' where "l<t'" "t'<t" "f t'=0" by auto
then have "t'∈{l..<x}" unfolding ls_def using t by auto
then show False using noroot ‹f t'=0› by auto
qed
ultimately show "sgn (f t) = sgn (f l)"
by (metis le_less not_less sgn_if)
qed
then show "f sgnx_able (at_left x)" by auto
show "sgnx f (at_left x)≠0"
using noroot[of l,simplified] ‹(f has_sgnx sgn (f l)) (at_left x)›
next
define rs where "rs ≡ {t. (f t=0 ∨ t∈s) ∧ x<t ∧ t<b}"
define r where "r≡(if rs = {} then (x+b)/2 else (Min rs + x)/2)"
have "finite rs"
proof -
have "{t. f t=0 ∧ x<t ∧ t<b} ⊆ {t. f t=0 ∧ a<t ∧ t<b}" using x by auto
then have "finite {t. f t=0 ∧ x<t ∧ t<b}" using assms(1)
using finite_subset by blast
moreover have "finite {t. t∈s ∧ x<t ∧ t<b}" using assms(3) by auto
moreover have "rs = {t. f t=0 ∧ x<t ∧ t<b} ∪ {t. t∈s ∧ x<t ∧ t<b}"
unfolding rs_def by auto
ultimately show ?thesis by auto
qed

have [simp]: "r>x" "a<r" "r<b"
proof -
have "r>x ∧ a<r ∧ r<b" when "rs = {}"
using that x unfolding r_def by auto
moreover have "r>x ∧ a<r ∧ r<b" when "rs ≠{}"
proof -
have "Min rs ∈ rs" using assms(1,3) that ‹finite rs›
apply (intro linorder_class.Min_in)
by auto
then have "x<Min rs ∧ Min rs < b" unfolding rs_def by auto
then show ?thesis unfolding r_def using that x by auto
qed
ultimately show "r>x" "a<r" "r<b" by auto
qed
have noroot:"f t≠0" when t:"t∈{x<..r}" for t
proof (cases "rs = {}")
case True
have False when "f t=0"
proof -
have "t<b" using t ‹r<b›
using greaterThanAtMost_iff by fastforce
then have "t∈rs" using that t unfolding rs_def by auto
then show False using True by auto
qed
then show ?thesis by auto
next
case False
have "t<Min rs" using that False ‹r>x› unfolding r_def by auto
have False when "f t=0"
proof -
have "t<b" using t ‹r<b› by (metis greaterThanAtMost_iff le_less less_trans)
then have "t∈rs" using that t unfolding rs_def by auto
then have "t≥Min rs" using ‹finite rs› by auto
then show False using ‹t<Min rs› by auto
qed
then show ?thesis by auto
qed
have "(f has_sgnx sgn (f r)) (at_right x)" unfolding has_sgnx_def
proof (rule eventually_at_rightI[OF _ ‹r>x›])
fix t assume t:"t∈{x<..<r}"
then have [simp]:"t>a" "t<b" using ‹r<b› x
by (meson greaterThanLessThan_iff less_trans)+
have False when "f t = 0"
using noroot t that by auto
moreover have False when "f r=0"
using noroot t that by auto
moreover have False when "f r>0 ∧ f t<0 ∨ f r <0 ∧ f t >0"
proof -
have False when "{t..r} ∩ s ≠{}"
proof -
obtain t' where t':"t'∈{t..r}" "t'∈s"
using ‹{t..r} ∩ s ≠ {}› by blast
then have "x<t' ∧ t'<b"
by (meson ‹r < b› atLeastAtMost_iff greaterThanLessThan_iff less_le_trans not_le t)
then have "t'∈rs" unfolding rs_def using t ‹t'∈s› by auto
then have "t'≥Min rs" using ‹finite rs› by auto
moreover have "Min rs>r"
using ‹r>x› ‹t'∈rs› ‹finite rs› unfolding r_def by (auto simp add:rs_def )
ultimately show False using t'(1) by auto
qed
moreover have "{t..r} ⊆ {a<..<b}"
by (intro atMostAtLeast_subset_convex,auto)
ultimately have "continuous_on {t..r} f" using assms(2) by (elim continuous_on_subset,auto)
then have "∃x>t. x < r ∧ f x = 0"
apply (intro IVT_strict)
using that t assms(2) by auto
then obtain t' where "t<t'" "t'<r" "f t'=0" by auto
then have "t'∈{x<..r}" unfolding rs_def using t by auto
then show False using noroot ‹f t'=0› by auto
qed
ultimately show "sgn (f t) = sgn (f r)"
by (metis le_less not_less sgn_if)
qed
then show "f sgnx_able (at_right x)" by auto
show "sgnx f (at_right x)≠0"
using noroot[of r,simplified] ‹(f has_sgnx sgn (f r)) (at_right x)›
qed

lemma sgnx_able_poly[simp]:
"(poly p) sgnx_able (at_right a)"
"(poly p) sgnx_able (at_left a)"
"(poly p) sgnx_able at_top"
"(poly p) sgnx_able at_bot"
proof -
show "(poly p) sgnx_able at_top"
using has_sgnx_def poly_sgn_eventually_at_top sgnx_able_def by blast
show "(poly p) sgnx_able at_bot"
using has_sgnx_def poly_sgn_eventually_at_bot sgnx_able_def by blast
show "(poly p) sgnx_able (at_right a)"
proof (cases "p=0")
case True
then show ?thesis unfolding sgnx_able_def has_sgnx_def eventually_at_right
using linordered_field_no_ub by force
next
case False
obtain ub where "ub>a" and ub:"∀z. a<z∧z≤ub⟶poly p z≠0"
using next_non_root_interval[OF False] by auto
have "∀z. a<z∧z≤ub⟶sgn(poly p z) = sgn (poly p ub)"
proof (rule ccontr)
assume "¬ (∀z. a < z ∧ z ≤ ub ⟶ sgn (poly p z) = sgn (poly p ub))"
then obtain z where "a<z" "z≤ub" "sgn(poly p z) ≠ sgn (poly p ub)" by auto
moreover then have "poly p z≠0" "poly p ub≠0" "z≠ub" using ub ‹ub>a› by blast+
ultimately have "(poly p z>0 ∧ poly p ub<0) ∨ (poly p z<0 ∧ poly p ub>0)"
by (metis linorder_neqE_linordered_idom sgn_neg sgn_pos)
then have "∃x>z. x < ub ∧ poly p x = 0"
using poly_IVT_neg[of z ub p] poly_IVT_pos[of z ub p] ‹z≤ub› ‹z≠ub› by argo
then show False using ub ‹a < z› by auto
qed
then show ?thesis unfolding sgnx_able_def has_sgnx_def eventually_at_right
apply (rule_tac exI[where x="sgn(poly p ub)"])
apply (rule_tac exI[where x="ub"])
using less_eq_real_def ‹ub>a› by blast
qed
show "(poly p) sgnx_able (at_left a)"
proof (cases "p=0")
case True
then show ?thesis unfolding sgnx_able_def has_sgnx_def eventually_at_right
using linordered_field_no_ub by force
next
case False
obtain lb where "lb<a" and ub:"∀z. lb≤z∧z<a⟶poly p z≠0"
using last_non_root_interval[OF False] by auto
have "∀z. lb≤z∧z<a⟶sgn(poly p z) = sgn (poly p lb)"
proof (rule ccontr)
assume "¬ (∀z. lb≤z∧z<a ⟶ sgn (poly p z) = sgn (poly p lb))"
then obtain z where "lb≤z" "z<a" "sgn(poly p z) ≠ sgn (poly p lb)" by auto
moreover then have "poly p z≠0" "poly p lb≠0" "z≠lb" using ub ‹lb<a› by blast+
ultimately have "(poly p z>0 ∧ poly p lb<0) ∨ (poly p z<0 ∧ poly p lb>0)"
by (metis linorder_neqE_linordered_idom sgn_neg sgn_pos)
then have "∃x>lb. x < z ∧ poly p x = 0"
using poly_IVT_neg[of lb z p] poly_IVT_pos[of lb z p] ‹lb≤z› ‹z≠lb› by argo
then show False using ub ‹z < a› by auto
qed
then show ?thesis unfolding sgnx_able_def has_sgnx_def eventually_at_left
apply (rule_tac exI[where x="sgn(poly p lb)"])
apply (rule_tac exI[where x="lb"])
using less_eq_real_def ‹lb<a› by blast
qed
qed

lemma has_sgnx_identity[intro,sgnx_intros]:
shows "x≥0 ⟹((λx. x) has_sgnx 1) (at_right x)"
"x≤0 ⟹ ((λx. x) has_sgnx -1) (at_left x)"
proof -
show "x≥0 ⟹ ((λx. x) has_sgnx 1) (at_right x)"
unfolding has_sgnx_def eventually_at_right
apply (intro exI[where x="x+1"])
by auto
show "x≤0 ⟹ ((λx. x) has_sgnx -1) (at_left x)"
unfolding has_sgnx_def eventually_at_left
apply (intro exI[where x="x-1"])
by auto
qed

lemma has_sgnx_divide[sgnx_intros]:
assumes "(f has_sgnx c1) F" "(g has_sgnx c2) F"
shows "((λx. f x / g x) has_sgnx c1 / c2) F"
proof -
have "∀⇩F x in F. sgn (f x) = c1 ∧ sgn (g x) = c2"
using assms unfolding has_sgnx_def by (intro eventually_conj,auto)
then have "∀⇩F x in F. sgn (f x / g x) = c1 / c2"
apply (elim eventually_mono)
then show "((λx. f x / g x) has_sgnx c1 / c2) F" unfolding has_sgnx_def by auto
qed

lemma sgnx_able_divide[sgnx_intros]:
assumes "f sgnx_able F" "g sgnx_able F"
shows "(λx. f x / g x) sgnx_able F"
using has_sgnx_divide by (meson assms(1) assms(2) sgnx_able_def)

lemma sgnx_divide:
assumes "F≠bot" "f sgnx_able F" "g sgnx_able F"
shows "sgnx (λx. f x / g x) F =sgnx f F / sgnx g F"
proof -
obtain c1 c2 where c1:"(f has_sgnx c1) F" and c2:"(g has_sgnx c2) F"
using assms unfolding sgnx_able_def by auto
have "sgnx f F=c1" "sgnx g F=c2" using c1 c2 ‹F≠bot› by auto
moreover have "((λx. f x / g x) has_sgnx c1 / c2) F"
using has_sgnx_divide[OF c1 c2] .
ultimately show ?thesis using assms(1) has_sgnx_imp_sgnx by blast
qed

lemma has_sgnx_times[sgnx_intros]:
assumes "(f has_sgnx c1) F" "(g has_sgnx c2) F"
shows "((λx. f x* g x) has_sgnx c1 * c2) F"
proof -
have "∀⇩F x in F. sgn (f x) = c1 ∧ sgn (g x) = c2"
using assms unfolding has_sgnx_def by (intro eventually_conj,auto)
then have "∀⇩F x in F. sgn (f x * g x) = c1 * c2"
apply (elim eventually_mono)
then show "((λx. f x* g x) has_sgnx c1 * c2) F" unfolding has_sgnx_def by auto
qed

lemma sgnx_able_times[sgnx_intros]:
assumes "f sgnx_able F" "g sgnx_able F"
shows "(λx. f x * g x) sgnx_able F"
using has_sgnx_times by (meson assms(1) assms(2) sgnx_able_def)

lemma sgnx_times:
assumes "F≠bot" "f sgnx_able F" "g sgnx_able F"
shows "sgnx (λx. f x * g x) F =sgnx f F * sgnx g F"
proof -
obtain c1 c2 where c1:"(f has_sgnx c1) F" and c2:"(g has_sgnx c2) F"
using assms unfolding sgnx_able_def by auto
have "sgnx f F=c1" "sgnx g F=c2" using c1 c2 ‹F≠bot› by auto
moreover have "((λx. f x* g x) has_sgnx c1 * c2) F"
using has_sgnx_times[OF c1 c2] .
ultimately show ?thesis using assms(1) has_sgnx_imp_sgnx by blast
qed

lemma tendsto_nonzero_has_sgnx:
assumes "(f ⤏ c) F" "c≠0"
shows "(f has_sgnx sgn c) F"
proof (cases rule:linorder_cases[of c 0])
case less
then have "∀⇩F x in F. f x<0"
using order_topology_class.order_tendstoD[OF assms(1),of 0] by auto
then show ?thesis
unfolding has_sgnx_def
apply (elim eventually_mono)
using less by auto
next
case equal
then show ?thesis using ‹c≠0› by auto
next
case greater
then have "∀⇩F x in F. f x>0"
using order_topology_class.order_tendstoD[OF assms(1),of 0] by auto
then show ?thesis
unfolding has_sgnx_def
apply (elim eventually_mono)
using greater by auto
qed

lemma tendsto_nonzero_sgnx:
assumes "(f ⤏ c) F" "F≠bot" "c≠0"
shows "sgnx f F = sgn c"
using tendsto_nonzero_has_sgnx

lemma filterlim_divide_at_bot_at_top_iff:
assumes "(f ⤏ c) F" "c≠0"
shows
"(LIM x F. f x / g x :> at_bot) ⟷ (g ⤏ 0) F
∧ ((λx. g x) has_sgnx - sgn c) F"
"(LIM x F. f x / g x :> at_top) ⟷ (g ⤏ 0) F
∧ ((λx. g x) has_sgnx sgn c) F"
proof -
show "(LIM x F. f x / g x :> at_bot) ⟷ ((g ⤏ 0) F )
∧ ((λx. g x) has_sgnx - sgn c) F"
proof
assume asm:"LIM x F. f x / g x :> at_bot"
then have "filterlim g (at 0) F"
using filterlim_at_infinity_divide_iff[OF assms(1,2),of g]
at_bot_le_at_infinity filterlim_mono by blast
then have "(g ⤏ 0) F" using filterlim_at by blast
moreover have "(g has_sgnx - sgn c) F"
proof -
have "((λx. sgn c * inverse (f x)) ⤏ sgn c * inverse c) F"
using assms(1,2) by (auto intro:tendsto_intros)
then have "LIM x F. sgn c * inverse (f x) * (f x / g x) :> at_bot"
apply (elim filterlim_tendsto_pos_mult_at_bot[OF _ _ asm])
using ‹c≠0› sgn_real_def by auto
then have "LIM x F. sgn c / g x :> at_bot"
apply (elim filterlim_mono_eventually)
using eventually_times_inverse_1[OF assms] by (auto elim:eventually_mono)
then have "∀⇩F x in F. sgn c / g x < 0"
using filterlim_at_bot_dense[of "λx. sgn c/g x" F] by auto
then show ?thesis unfolding has_sgnx_def
apply (elim eventually_mono)
by (metis add.inverse_inverse divide_less_0_iff sgn_neg sgn_pos sgn_sgn)
qed
ultimately show "(g ⤏ 0) F ∧ (g has_sgnx - sgn c) F" by auto
next
assume "(g ⤏ 0) F ∧ (g has_sgnx - sgn c) F"
then have asm:"(g ⤏ 0) F" "(g has_sgnx - sgn c) F" by auto
have "LIM x F. inverse (g x * sgn c) :> at_bot"
proof (rule filterlim_inverse_at_bot)
show "((λx. g x * sgn c) ⤏ 0) F"
apply (rule tendsto_mult_left_zero)
using asm(1) by blast
next
show "∀⇩F x in F. g x * sgn c < 0" using asm(2) unfolding has_sgnx_def
apply (elim eventually_mono)
by (metis add.inverse_inverse assms(2) linorder_neqE_linordered_idom mult_less_0_iff
neg_0_less_iff_less sgn_greater sgn_zero_iff)
qed
moreover have "((λx. f x * sgn c) ⤏ c * sgn c) F"
using ‹(f ⤏ c) F› ‹c≠0›
apply (intro tendsto_intros)
moreover have "c * sgn c >0" using ‹c≠0› by (simp add: sgn_real_def)
ultimately have "LIM x F. (f x * sgn c) *inverse (g x * sgn c) :> at_bot"
using filterlim_tendsto_pos_mult_at_bot by blast
then show "LIM x F. f x / g x :> at_bot"
using ‹c≠0› by (auto simp add:field_simps sgn_zero_iff)
qed
show "(LIM x F. f x / g x :> at_top) ⟷ ((g ⤏ 0) F )
∧ ((λx. g x) has_sgnx sgn c) F"
proof
assume asm:"LIM x F. f x / g x :> at_top"
then have "filterlim g (at 0) F"
using filterlim_at_infinity_divide_iff[OF assms(1,2),of g]
at_top_le_at_infinity filterlim_mono by blast
then have "(g ⤏ 0) F" using filterlim_at by blast
moreover have "(g has_sgnx sgn c) F"
proof -
have "((λx. sgn c * inverse (f x)) ⤏ sgn c * inverse c) F"
using assms(1,2) by (auto intro:tendsto_intros)
then have "LIM x F. sgn c * inverse (f x) * (f x / g x) :> at_top"
apply (elim filterlim_tendsto_pos_mult_at_top[OF _ _ asm])
using ‹c≠0› sgn_real_def by auto
then have "LIM x F. sgn c / g x :> at_top"
apply (elim filterlim_mono_eventually)
using eventually_times_inverse_1[OF assms] by (auto elim:eventually_mono)
then have "∀⇩F x in F. sgn c / g x > 0"
using filterlim_at_top_dense[of "λx. sgn c/g x" F] by auto
then show ?thesis unfolding has_sgnx_def
apply (elim eventually_mono)
by (metis sgn_greater sgn_less sgn_neg sgn_pos zero_less_divide_iff)
qed
ultimately show "(g ⤏ 0) F ∧ (g has_sgnx sgn c) F" by auto
next
assume "(g ⤏ 0) F ∧ (g has_sgnx sgn c) F"
then have asm:"(g ⤏ 0) F" "(g has_sgnx sgn c) F" by auto
have "LIM x F. inverse (g x * sgn c) :> at_top"
proof (rule filterlim_inverse_at_top)
show "((λx. g x * sgn c) ⤏ 0) F"
apply (rule tendsto_mult_left_zero)
using asm(1) by blast
next
show "∀⇩F x in F. g x * sgn c > 0" using asm(2) unfolding has_sgnx_def
apply (elim eventually_mono)
by (metis assms(2) sgn_1_neg sgn_greater sgn_if zero_less_mult_iff)
qed
moreover have "((λx. f x * sgn c) ⤏ c * sgn c) F"
using ‹(f ⤏ c) F› ‹c≠0›
apply (intro tendsto_intros)
moreover have "c * sgn c >0" using ‹c≠0› by (simp add: sgn_real_def)
ultimately have "LIM x F. (f x * sgn c) *inverse (g x * sgn c) :> at_top"
using filterlim_tendsto_pos_mult_at_top by blast
then show "LIM x F. f x / g x :> at_top"
using ‹c≠0› by (auto simp add:field_simps sgn_zero_iff)
qed
qed

lemma poly_sgnx_left_right:
fixes c a::real and p::"real poly"
assumes "p≠0"
shows "sgnx (poly p) (at_left a) = (if even (order a p)
then sgnx (poly p) (at_right a)
else -sgnx (poly p) (at_right a))"
using assms
proof (induction "degree p" arbitrary: p rule: less_induct)
case less
have ?case when "poly p a≠0"
proof -
have "sgnx (poly p) (at_left a) = sgn (poly p a)"
by (simp add: has_sgnx_imp_sgnx tendsto_nonzero_has_sgnx that)
moreover have "sgnx (poly p) (at_right a) = sgn (poly p a)"
by (simp add: has_sgnx_imp_sgnx tendsto_nonzero_has_sgnx that)
moreover have "order a p = 0" using that by (simp add: order_0I)
ultimately show ?thesis by auto
qed
moreover have ?case when "poly p a=0"
proof -
obtain q where pq:"p= [:-a,1:] * q"
using ‹poly p a=0› by (meson dvdE poly_eq_0_iff_dvd)
then have "q≠0" using ‹p≠0› by auto
then have "degree q < degree p" unfolding pq by (subst degree_mult_eq,auto)
have "sgnx (poly p) (at_left a) = - sgnx (poly q) (at_left a)"
proof -
have "sgnx (λx. poly p x) (at_left a)
= sgnx (poly q) (at_left a) * sgnx (poly [:-a,1:]) (at_left a)"
unfolding pq
apply (subst poly_mult)
apply (subst sgnx_times)
by auto
moreover have "sgnx (λx. poly [:-a,1:] x) (at_left a) = -1"
apply (intro has_sgnx_imp_sgnx)
unfolding has_sgnx_def eventually_at_left
ultimately show ?thesis by auto
qed
moreover have "sgnx (poly p) (at_right a) = sgnx (poly q) (at_right a)"
proof -
have "sgnx (λx. poly p x) (at_right a)
= sgnx (poly q) (at_right a) * sgnx (poly [:-a,1:]) (at_right a)"
unfolding pq
apply (subst poly_mult)
apply (subst sgnx_times)
by auto
moreover have "sgnx (λx. poly [:-a,1:] x) (at_right a) = 1"
apply (intro has_sgnx_imp_sgnx)
unfolding has_sgnx_def eventually_at_right
ultimately show ?thesis by auto
qed
moreover have "even (order a p) ⟷ odd (order a q)"
unfolding pq
apply (subst order_mult[OF ‹p ≠ 0›[unfolded pq]])
using  ‹q≠0› by (auto simp add:order_power_n_n[of _ 1, simplified])
moreover note less.hyps[OF ‹degree q < degree p› ‹q≠0›]
ultimately show ?thesis by auto
qed
ultimately show ?case by blast
qed

lemma poly_has_sgnx_left_right:
fixes c a::real and p::"real poly"
assumes "p≠0"
shows "(poly p has_sgnx c) (at_left a) ⟷ (if even (order a p)
then (poly p has_sgnx c) (at_right a)
else (poly p has_sgnx -c) (at_right a))"
using poly_sgnx_left_right
by (metis (no_types, hide_lams) add.inverse_inverse assms has_sgnx_unique
sgnx_able_poly sgnx_able_sgnx trivial_limit_at_left_real trivial_limit_at_right_real)

lemma sign_r_pos_sgnx_iff:
"sign_r_pos p a ⟷ sgnx (poly p) (at_right a) > 0"
proof
assume asm:"0 < sgnx (poly p) (at_right a)"
obtain c where c_def:"(poly p has_sgnx c) (at_right a)"
using sgnx_able_poly(1) sgnx_able_sgnx by blast
then have "c>0" using asm
using has_sgnx_imp_sgnx trivial_limit_at_right_real by blast
then show "sign_r_pos p a" using c_def unfolding sign_r_pos_def has_sgnx_def
apply (elim eventually_mono)
by force
next
assume asm:"sign_r_pos p a"
define c where "c = sgnx (poly p) (at_right a)"
then have "(poly p has_sgnx c) (at_right a)"
then have "(∀⇩F x in (at_right a). poly p x>0 ∧ sgn (poly p x) = c)"
using asm unfolding has_sgnx_def sign_r_pos_def
then have "∀⇩F x in (at_right a). c > 0"
apply (elim eventually_mono)
by fastforce
then show "c>0" by auto
qed

lemma sgnx_values:
assumes "f sgnx_able F" "F ≠ bot"
shows "sgnx f F = -1 ∨ sgnx f F = 0 ∨ sgnx f F = 1"
proof -
obtain c where c_def:"(f has_sgnx c) F"
using assms(1) unfolding sgnx_able_def by auto
then obtain x where "sgn(f x) = c"
unfolding has_sgnx_def using assms(2) eventually_happens
by blast
then have "c=-1 ∨ c=0 ∨ c=1" using sgn_if by metis
moreover have "sgnx f F = c" using c_def by (simp add: assms(2) has_sgnx_imp_sgnx)
ultimately show ?thesis by auto
qed

lemma has_sgnx_poly_at_top:
"(poly p has_sgnx  sgn_pos_inf p) at_top"
using has_sgnx_def poly_sgn_eventually_at_top by blast

lemma has_sgnx_poly_at_bot:
"(poly p has_sgnx  sgn_neg_inf p) at_bot"
using has_sgnx_def poly_sgn_eventually_at_bot by blast

lemma sgnx_poly_at_top:
"sgnx (poly p) at_top = sgn_pos_inf p"
by (simp add: has_sgnx_def has_sgnx_imp_sgnx poly_sgn_eventually_at_top)

lemma sgnx_poly_at_bot:
"sgnx (poly p) at_bot = sgn_neg_inf p"
by (simp add: has_sgnx_def has_sgnx_imp_sgnx poly_sgn_eventually_at_bot)

lemma poly_has_sgnx_values:
assumes "p≠0"
shows
"(poly p has_sgnx 1) (at_left a) ∨ (poly p has_sgnx - 1) (at_left a)"
"(poly p has_sgnx 1) (at_right a) ∨ (poly p has_sgnx - 1) (at_right a)"
"(poly p has_sgnx 1) at_top ∨ (poly p has_sgnx - 1) at_top"
"(poly p has_sgnx 1) at_bot ∨ (poly p has_sgnx - 1) at_bot"
proof -
have "sgn_pos_inf p = 1 ∨ sgn_pos_inf p = -1"
unfolding sgn_pos_inf_def by (simp add: assms sgn_if)
then show "(poly p has_sgnx 1) at_top ∨ (poly p has_sgnx - 1) at_top"
using has_sgnx_poly_at_top by metis
next
have "sgn_neg_inf p = 1 ∨ sgn_neg_inf p = -1"
unfolding sgn_neg_inf_def by (simp add: assms sgn_if)
then show "(poly p has_sgnx 1) at_bot ∨ (poly p has_sgnx - 1) at_bot"
using has_sgnx_poly_at_bot by metis
next
obtain c where c_def:"(poly p has_sgnx c) (at_left a)"
using sgnx_able_poly(2) sgnx_able_sgnx by blast
then have "sgnx (poly p) (at_left a) = c" using assms by auto
then have "c=-1 ∨ c=0 ∨ c=1"
using sgnx_values sgnx_able_poly(2) trivial_limit_at_left_real by blast
moreover have False when "c=0"
proof -
have "(poly p has_sgnx 0) (at_left a)" using c_def that by auto
then obtain lb where "lb<a" "∀y. (lb<y ∧ y < a) ⟶ poly p y = 0"
unfolding has_sgnx_def eventually_at_left sgn_if
by (metis one_neq_zero zero_neq_neg_one)
then have "{lb<..<a} ⊆ proots p" unfolding proots_within_def by auto
then have "infinite (proots p)"
apply (elim infinite_super)
using ‹lb<a› by auto
moreover have "finite (proots p)" using finite_proots[OF ‹p≠0›] by auto
ultimately show False by auto
qed
ultimately have "c=-1 ∨ c=1" by auto
then show "(poly p has_sgnx 1) (at_left a) ∨ (poly p has_sgnx - 1) (at_left a)"
using c_def by auto
next
obtain c where c_def:"(poly p has_sgnx c) (at_right a)"
using sgnx_able_poly(1) sgnx_able_sgnx by blast
then have "sgnx (poly p) (at_right a) = c" using assms by auto
then have "c=-1 ∨ c=0 ∨ c=1"
using sgnx_values sgnx_able_poly(1) trivial_limit_at_right_real by blast
moreover have False when "c=0"
proof -
have "(poly p has_sgnx 0) (at_right a)" using c_def that by auto
then obtain ub where "ub>a" "∀y. (a<y ∧ y < ub) ⟶ poly p y = 0"
unfolding has_sgnx_def eventually_at_right sgn_if
by (metis one_neq_zero zero_neq_neg_one)
then have "{a<..<ub} ⊆ proots p" unfolding proots_within_def by auto
then have "infinite (proots p)"
apply (elim infinite_super)
using ‹ub>a› by auto
moreover have "finite (proots p)" using finite_proots[OF ‹p≠0›] by auto
ultimately show False by auto
qed
ultimately have "c=-1 ∨ c=1" by auto
then show "(poly p has_sgnx 1) (at_right a) ∨ (poly p has_sgnx - 1) (at_right a)"
using c_def by auto
qed

lemma poly_sgnx_values:
assumes "p≠0"
shows "sgnx (poly p) (at_left a) = 1 ∨ sgnx (poly p) (at_left a) = -1"
"sgnx (poly p) (at_right a) = 1 ∨ sgnx (poly p) (at_right a) = -1"
using poly_has_sgnx_values[OF ‹p≠0›] has_sgnx_imp_sgnx trivial_limit_at_left_real
trivial_limit_at_right_real by blast+

lemma has_sgnx_inverse: "(f has_sgnx c) F ⟷ ((inverse o f) has_sgnx (inverse c)) F"
unfolding has_sgnx_def comp_def
apply (rule eventually_subst)
apply (rule always_eventually)
by (metis inverse_inverse_eq sgn_inverse)

lemma has_sgnx_derivative_at_left:
assumes g_deriv:"(g has_field_derivative c) (at x)" and "g x=0" and "c≠0"
shows "(g has_sgnx - sgn c) (at_left x)"
proof -
have "(g has_sgnx -1) (at_left x)" when "c>0"
proof -
obtain d1 where "d1>0" and d1_def:"∀h>0. h < d1 ⟶ g (x - h) < g x"
using DERIV_pos_inc_left[OF g_deriv ‹c>0›] ‹g x=0› by auto
have "(g has_sgnx -1) (at_left x)"
unfolding has_sgnx_def eventually_at_left
apply (intro exI[where x="x-d1"])
using ‹d1>0› d1_def
diff_strict_left_mono diff_zero minus_diff_eq sgn_neg)
thus ?thesis by auto
qed
moreover have "(g has_sgnx 1) (at_left x)" when "c<0"
proof -
obtain d1 where "d1>0" and d1_def:"∀h>0. h < d1 ⟶ g (x - h) > g x"
using DERIV_neg_dec_left[OF g_deriv ‹c<0›] ‹g x=0› by auto
have "(g has_sgnx 1) (at_left x)"
unfolding has_sgnx_def eventually_at_left
apply (intro exI[where x="x-d1"])
using ‹d1>0› d1_def
diff_zero less_diff_eq minus_diff_eq sgn_pos)
thus ?thesis using ‹c<0›  by auto
qed
ultimately show ?thesis using ‹c≠0› using sgn_real_def by auto
qed

lemma has_sgnx_derivative_at_right:
assumes g_deriv:"(g has_field_derivative c) (at x)" and "g x=0" and "c≠0"
shows "(g has_sgnx sgn c) (at_right x)"
proof -
have "(g has_sgnx 1) (at_right x)" when "c>0"
proof -
obtain d2 where "d2>0" and d2_def:"∀h>0. h < d2 ⟶ g x < g (x + h)"
using DERIV_pos_inc_right[OF g_deriv ‹c>0›] ‹g x=0› by auto
have "(g has_sgnx 1) (at_right x)"
unfolding has_sgnx_def eventually_at_right
apply (intro exI[where x="x+d2"])
using ‹d2>0› d2_def
thus ?thesis using ‹c>0› by auto
qed
moreover have "(g has_sgnx -1) (at_right x)" when "c<0"
proof -
obtain d2 where "d2>0" and d2_def:"∀h>0. h < d2 ⟶ g x > g (x + h)"
using DERIV_neg_dec_right[OF g_deriv ‹c<0›] ‹g x=0› by auto
have "(g has_sgnx -1) (at_right x)"
unfolding has_sgnx_def eventually_at_right
apply (intro exI[where x="x+d2"])
using ‹d2>0› d2_def
thus ?thesis using ‹c<0› by auto
qed
ultimately show ?thesis using ‹c≠0› using sgn_real_def by auto
qed

lemma has_sgnx_split:
"(f has_sgnx c) (at x) ⟷ (f has_sgnx c) (at_left x) ∧ (f has_sgnx c) (at_right x)"
unfolding has_sgnx_def using eventually_at_split by auto

lemma sgnx_at_top_IVT:
assumes "sgnx (poly p) (at_right a) ≠ sgnx (poly p) at_top"
shows "∃x>a. poly p x=0"
proof (cases "p=0")
case True
then show ?thesis using gt_ex[of a] by simp
next
case False
from poly_has_sgnx_values[OF this]
have "(poly p has_sgnx 1) (at_right a) ∨ (poly p has_sgnx - 1) (at_right a)"
"(poly p has_sgnx 1) at_top ∨ (poly p has_sgnx - 1) at_top"
by auto
moreover have ?thesis when has_r:"(poly p has_sgnx 1) (at_right a)"
and has_top:"(poly p has_sgnx -1) at_top"
proof -
obtain b where "b>a" "poly p b>0"
proof -
obtain a' where "a'>a" and a'_def:"∀y>a. y < a' ⟶ sgn (poly p y) = 1"
using has_r[unfolded has_sgnx_def eventually_at_right] by auto
define b where "b=(a+a')/2"
have "a<b" "b<a'" unfolding b_def using ‹a'>a› by auto
moreover have "poly p b>0"
using a'_def[rule_format,OF ‹b>a› ‹b<a'›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
moreover obtain c where "c>b" "poly p c<0"
proof -
obtain b' where b'_def:"∀n≥b'. sgn (poly p n) = - 1"
using has_top[unfolded has_sgnx_def eventually_at_top_linorder] by auto
define c where "c=1+max b b'"
have "c>b" "c≥b'" unfolding c_def using ‹b>a› by auto
moreover have "poly p c<0"
using b'_def[rule_format,OF ‹b'≤c›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
ultimately show ?thesis using poly_IVT_neg[of b c p] not_less by fastforce
qed
moreover have ?thesis when has_r:"(poly p has_sgnx -1) (at_right a)"
and has_top:"(poly p has_sgnx 1) at_top"
proof -
obtain b where "b>a" "poly p b<0"
proof -
obtain a' where "a'>a" and a'_def:"∀y>a. y < a' ⟶ sgn (poly p y) = -1"
using has_r[unfolded has_sgnx_def eventually_at_right] by auto
define b where "b=(a+a')/2"
have "a<b" "b<a'" unfolding b_def using ‹a'>a› by auto
moreover have "poly p b<0"
using a'_def[rule_format,OF ‹b>a› ‹b<a'›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
moreover obtain c where "c>b" "poly p c>0"
proof -
obtain b' where b'_def:"∀n≥b'. sgn (poly p n) = 1"
using has_top[unfolded has_sgnx_def eventually_at_top_linorder] by auto
define c where "c=1+max b b'"
have "c>b" "c≥b'" unfolding c_def using ‹b>a› by auto
moreover have "poly p c>0"
using b'_def[rule_format,OF ‹b'≤c›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
ultimately show ?thesis using poly_IVT_pos[of b c p] not_less by fastforce
qed
moreover have ?thesis when
"(poly p has_sgnx 1) (at_right a) ∧ (poly p has_sgnx 1) at_top
∨ (poly p has_sgnx - 1) (at_right a) ∧ (poly p has_sgnx -1) at_top"
proof -
have "sgnx (poly p) (at_right a) = sgnx (poly p) at_top"
using that has_sgnx_imp_sgnx by auto
then have False using assms by simp
then show ?thesis by auto
qed
ultimately show ?thesis by blast
qed

lemma sgnx_at_left_at_right_IVT:
assumes "sgnx (poly p) (at_right a) ≠ sgnx (poly p) (at_left b)" "a<b"
shows "∃x. a<x ∧ x<b ∧ poly p x=0"
proof (cases "p=0")
case True
then show ?thesis using ‹a<b› by (auto intro:exI[where x="(a+b)/2"])
next
case False
from poly_has_sgnx_values[OF this]
have "(poly p has_sgnx 1) (at_right a) ∨ (poly p has_sgnx - 1) (at_right a)"
"(poly p has_sgnx 1) (at_left b) ∨ (poly p has_sgnx - 1) (at_left b)"
by auto
moreover have ?thesis when has_r:"(poly p has_sgnx 1) (at_right a)"
and has_l:"(poly p has_sgnx -1) (at_left b)"
proof -
obtain c where "a<c" "c<b" "poly p c>0"
proof -
obtain a' where "a'>a" and a'_def:"∀y>a. y < a' ⟶ sgn (poly p y) = 1"
using has_r[unfolded has_sgnx_def eventually_at_right] by auto
define c where "c=(a+min a' b)/2"
have "a<c" "c<a'" "c<b" unfolding c_def using ‹a'>a› ‹b>a› by auto
moreover have "poly p c>0"
using a'_def[rule_format,OF ‹c>a› ‹c<a'›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
moreover obtain d where "c<d""d<b" "poly p d<0"
proof -
obtain b' where "b'<b" and b'_def:"∀y>b'. y < b ⟶ sgn (poly p y) = - 1"
using has_l[unfolded has_sgnx_def eventually_at_left] by auto
define d where "d=(b+max b' c)/2"
have "b'<d" "d<b" "d>c"
unfolding d_def using ‹b>b'› ‹b>c› by auto
moreover have "poly p d<0"
using b'_def[rule_format, OF ‹b'<d› ‹d<b›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
ultimately obtain x where "c<x" "x<d" "poly p x=0"
using poly_IVT_neg[of c d p] by auto
then show ?thesis using ‹c>a› ‹d<b› by (auto intro: exI[where x=x])
qed
moreover have ?thesis when has_r:"(poly p has_sgnx -1) (at_right a)"
and has_l:"(poly p has_sgnx 1) (at_left b)"
proof -
obtain c where "a<c" "c<b" "poly p c<0"
proof -
obtain a' where "a'>a" and a'_def:"∀y>a. y < a' ⟶ sgn (poly p y) = -1"
using has_r[unfolded has_sgnx_def eventually_at_right] by auto
define c where "c=(a+min a' b)/2"
have "a<c" "c<a'" "c<b" unfolding c_def using ‹a'>a› ‹b>a› by auto
moreover have "poly p c<0"
using a'_def[rule_format,OF ‹c>a› ‹c<a'›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
moreover obtain d where "c<d""d<b" "poly p d>0"
proof -
obtain b' where "b'<b" and b'_def:"∀y>b'. y < b ⟶ sgn (poly p y) = 1"
using has_l[unfolded has_sgnx_def eventually_at_left] by auto
define d where "d=(b+max b' c)/2"
have "b'<d" "d<b" "d>c"
unfolding d_def using ‹b>b'› ‹b>c› by auto
moreover have "poly p d>0"
using b'_def[rule_format, OF ‹b'<d› ‹d<b›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
ultimately obtain x where "c<x" "x<d" "poly p x=0"
using poly_IVT_pos[of c d p] by auto
then show ?thesis using ‹c>a› ‹d<b› by (auto intro: exI[where x=x])
qed
moreover have ?thesis when
"(poly p has_sgnx 1) (at_right a) ∧ (poly p has_sgnx 1) (at_left b)
∨ (poly p has_sgnx - 1) (at_right a) ∧ (poly p has_sgnx -1) (at_left b)"
proof -
have "sgnx (poly p) (at_right a) = sgnx (poly p) (at_left b)"
using that has_sgnx_imp_sgnx by auto
then have False using assms by simp
then show ?thesis by auto
qed
ultimately show ?thesis by blast
qed

lemma sgnx_at_bot_IVT:
assumes "sgnx (poly p) (at_left a) ≠ sgnx (poly p) at_bot"
shows "∃x<a. poly p x=0"
proof (cases "p=0")
case True
then show ?thesis using lt_ex[of a] by simp
next
case False
from poly_has_sgnx_values[OF this]
have "(poly p has_sgnx 1) (at_left a) ∨ (poly p has_sgnx - 1) (at_left a)"
"(poly p has_sgnx 1) at_bot ∨ (poly p has_sgnx - 1) at_bot"
by auto
moreover have ?thesis when has_l:"(poly p has_sgnx 1) (at_left a)"
and has_bot:"(poly p has_sgnx -1) at_bot"
proof -
obtain b where "b<a" "poly p b>0"
proof -
obtain a' where "a'<a" and a'_def:"∀y>a'. y < a ⟶ sgn (poly p y) = 1"
using has_l[unfolded has_sgnx_def eventually_at_left] by auto
define b where "b=(a+a')/2"
have "a>b" "b>a'" unfolding b_def using ‹a'<a› by auto
moreover have "poly p b>0"
using a'_def[rule_format,OF ‹b>a'› ‹b<a›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
moreover obtain c where "c<b" "poly p c<0"
proof -
obtain b' where b'_def:"∀n≤b'. sgn (poly p n) = - 1"
using has_bot[unfolded has_sgnx_def eventually_at_bot_linorder] by auto
define c where "c=min b b'- 1"
have "c<b" "c≤b'" unfolding c_def using ‹b<a› by auto
moreover have "poly p c<0"
using b'_def[rule_format,OF ‹b'≥c›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
ultimately show ?thesis using poly_IVT_pos[of c b p] using not_less by fastforce
qed
moreover have ?thesis when has_l:"(poly p has_sgnx -1) (at_left a)"
and has_bot:"(poly p has_sgnx 1) at_bot"
proof -
obtain b where "b<a" "poly p b<0"
proof -
obtain a' where "a'<a" and a'_def:"∀y>a'. y < a ⟶ sgn (poly p y) = -1"
using has_l[unfolded has_sgnx_def eventually_at_left] by auto
define b where "b=(a+a')/2"
have "a>b" "b>a'" unfolding b_def using ‹a'<a› by auto
moreover have "poly p b<0"
using a'_def[rule_format,OF ‹b>a'› ‹b<a›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
moreover obtain c where "c<b" "poly p c>0"
proof -
obtain b' where b'_def:"∀n≤b'. sgn (poly p n) = 1"
using has_bot[unfolded has_sgnx_def eventually_at_bot_linorder] by auto
define c where "c=min b b'- 1"
have "c<b" "c≤b'" unfolding c_def using ‹b<a› by auto
moreover have "poly p c>0"
using b'_def[rule_format,OF ‹b'≥c›] unfolding sgn_if by argo
ultimately show ?thesis using that by auto
qed
ultimately show ?thesis using poly_IVT_neg[of c b p] using not_less by fastforce
qed
moreover have ?thesis when
"(poly p has_sgnx 1) (at_left a) ∧ (poly p has_sgnx 1) at_bot
∨ (poly p has_sgnx - 1) (at_left a) ∧ (poly p has_sgnx -1) at_bot"
proof -
have "sgnx (poly p) (at_left a) = sgnx (poly p) at_bot"
using that has_sgnx_imp_sgnx by auto
then have False using assms by simp
then show ?thesis by auto
qed
ultimately show ?thesis by blast
qed

lemma sgnx_poly_nz:
assumes "poly p x≠0"
shows "sgnx (poly p) (at_left x) = sgn (poly p x)"
"sgnx (poly p) (at_right x) = sgn (poly p x)"
proof -
have "(poly p has_sgnx sgn(poly p x)) (at x)"
apply (rule tendsto_nonzero_has_sgnx)
using assms by auto
then show "sgnx (poly p) (at_left x) = sgn (poly p x)"
"sgnx (poly p) (at_right x) = sgn (poly p x)"
unfolding has_sgnx_split by auto
qed

subsection ‹Finite predicate segments over an interval›

inductive finite_Psegments::"(real ⇒ bool) ⇒ real ⇒ real ⇒ bool" for P where
emptyI: "a≥b ⟹ finite_Psegments P a b"|
insertI_1: "⟦s∈{a..<b};s=a∨P s;∀t∈{s<..<b}. P t; finite_Psegments P a s⟧
⟹ finite_Psegments P a b"|
insertI_2: "⟦s∈{a..<b};s=a∨P s;(∀t∈{s<..<b}. ¬P t);finite_Psegments P a s⟧
⟹ finite_Psegments P a b"

lemma finite_Psegments_pos_linear:
assumes "finite_Psegments P (b*lb+c) (b*ub+c) " and "b>0"
shows "finite_Psegments (P o (λt. b*t+c)) lb ub"
proof -
have [simp]:"b≠0" using ‹b>0› by auto
show ?thesis
proof (rule finite_Psegments.induct[OF assms(1),
of "λlb' ub'. finite_Psegments (P o (λt. b*t+c)) ((lb'-c)/b) ((ub'-c)/b)",simplified])
(*really weird application of the induction rule, is there an alternative?*)
fix lb ub f assume "(lb::real)≤ub"
then have "(lb - c) / b ≤ (ub - c) / b"
using ‹b>0› by (auto simp add:field_simps)
then show "finite_Psegments (f ∘ (λt. b * t + c)) ((ub - c) / b) ((lb - c) / b)"
by (rule finite_Psegments.emptyI)
next
fix s lb ub P
assume asm: "lb ≤ s ∧ s < ub"
"∀t∈{s<..<ub}. P t"
"finite_Psegments (P ∘ (λt. b * t + c)) ((lb - c) / b) ((s - c) / b)"
"s = lb ∨ P s"
show "finite_Psegments (P ∘ (λt. b * t + c)) ((lb - c) / b) ((ub - c) / b)"
apply (rule finite_Psegments.insertI_1[of "(s-c)/b"])
using asm ‹b>0›  by (auto simp add:field_simps)
next
fix s lb ub P
assume asm: "lb ≤ s ∧ s < ub"
"∀t∈{s<..<ub}. ¬ P t"
"finite_Psegments (P ∘ (λt. b * t + c)) ((lb - c) / b) ((s - c) / b)"
"s=lb ∨ P s"
show "finite_Psegments (P ∘ (λt. b * t + c)) ((lb - c) / b) ((ub - c) / b)"
apply (rule finite_Psegments.insertI_2[of "(s-c)/b"])
using asm ‹b>0›  by (auto simp add:field_simps)
qed
qed

lemma finite_Psegments_congE:
assumes "finite_Psegments Q lb ub"
"⋀t. ⟦lb<t;t<ub⟧ ⟹ Q t ⟷ P t "
shows "finite_Psegments P lb ub" using assms
proof (induct rule:finite_Psegments.induct)
case (emptyI a b)
then show ?case using finite_Psegments.emptyI by auto
next
case (insertI_1 s a b)
show ?case
proof (rule finite_Psegments.insertI_1[of s])
have "P s" when "s≠a"
proof -
have "s∈{a<..<b}" using ‹s ∈ {a..<b}› that by auto
then show ?thesis using insertI_1 by auto
qed
then show "s = a ∨ P s" by auto
next
show "s ∈ {a..<b}" " ∀t∈{s<..<b}. P t" "finite_Psegments P a s" using insertI_1 by auto
qed
next
case (insertI_2 s a b)
show ?case
proof (rule finite_Psegments.insertI_2[of s])
have "P s" when "s≠a"
proof -
have "s∈{a<..<b}" using ‹s ∈ {a..<b}› that by auto
then show ?thesis using insertI_2 by auto
qed
then show "s = a ∨ P s" by auto
next
show "s ∈ {a..<b}" " ∀t∈{s<..<b}. ¬ P t" "finite_Psegments P a s" using insertI_2 by auto
qed
qed

lemma finite_Psegments_constI:
assumes "⋀t. ⟦a<t;t<b⟧ ⟹ P t = c"
shows "finite_Psegments P a b"
proof -
have "finite_Psegments (λ_. c) a b"
proof -
have ?thesis when "a≥b"
using that finite_Psegments.emptyI by auto
moreover have ?thesis when "a<b" "c"
apply (rule finite_Psegments.insertI_1[of a])
using that by (auto intro: finite_Psegments.emptyI)
moreover have ?thesis when "a<b" "¬c"
apply (rule finite_Psegments.insertI_2[of a])
using that by (auto intro: finite_Psegments.emptyI)
ultimately show ?thesis by argo
qed
then show ?thesis
apply (elim finite_Psegments_congE)
using assms by auto
qed

context
begin

private lemma finite_Psegments_less_eq1:
assumes "finite_Psegments P a c" "b≤c"
shows "finite_Psegments P a b" using assms
proof (induct arbitrary: b rule:finite_Psegments.induct)
case (emptyI a c)
then show ?case using finite_Psegments.emptyI by auto
next
case (insertI_1 s a c)
have ?case when "b≤s" using insertI_1 that by auto
moreover have ?case when "b>s"
proof -
have "s ∈ {a..<b}" using that ‹s ∈ {a..<c}› ‹b ≤ c› by auto
moreover have "∀t∈{s<..<b}. P t" using ‹∀t∈{s<..<c}. P t› that ‹b ≤ c› by auto
ultimately show ?case
using finite_Psegments.insertI_1[OF _ _ _ ‹finite_Psegments P a s›] ‹ s = a ∨ P s› by auto
qed
ultimately show ?case by fastforce
next
case (insertI_2 s a c)
have ?case when "b≤s" using insertI_2 that by auto
moreover have ?case when "b>s"
proof -
have "s ∈ {a..<b}" using that ‹s ∈ {a..<c}› ‹b ≤ c› by auto
moreover have "∀t∈{s<..<b}. ¬ P t" using ‹∀t∈{s<..<c}. ¬ P t› that ‹b ≤ c› by auto
ultimately show ?case
using finite_Psegments.insertI_2[OF _ _ _ ‹finite_Psegments P a s›] ‹ s = a ∨ P s› by auto
qed
ultimately show ?case by fastforce
qed

private lemma finite_Psegments_less_eq2:
assumes "finite_Psegments P a c" "a≤b"
shows "finite_Psegments P b c" using assms
proof (induct arbitrary:  rule:finite_Psegments.induct)
case (emptyI a c)
then show ?case using finite_Psegments.emptyI by auto
next
case (insertI_1 s a c)
have ?case when "s≤b"
proof -
have "∀t∈{b<..<c}. P t" using insertI_1 that by auto
then show ?thesis by (simp add: finite_Psegments_constI)
qed
moreover have ?case when "s>b"
apply (rule finite_Psegments.insertI_1[where s=s])
using insertI_1 that by auto
ultimately show ?case by linarith
next
case (insertI_2 s a c)
have ?case when "s≤b"
proof -
have "∀t∈{b<..<c}. ¬ P t" using insertI_2 that by auto
then show ?thesis by (metis finite_Psegments_constI greaterThanLessThan_iff)
qed
moreover have ?case when "s>b"
apply (rule finite_Psegments.insertI_2[where s=s])
using insertI_2 that by auto
ultimately show ?case by linarith
qed

lemma finite_Psegments_included:
assumes "finite_Psegments P a d" "a≤b" "c≤d"
shows "finite_Psegments P b c"
using finite_Psegments_less_eq2 finite_Psegments_less_eq1 assms by blast
end

lemma finite_Psegments_combine:
assumes "finite_Psegments P a b" "finite_Psegments P b c" "b∈{a..c}" "closed ({x. P x} ∩ {a..c})"
shows "finite_Psegments P a c"  using assms(2,1,3,4)
proof (induct rule:finite_Psegments.induct)
case (emptyI b c)
then show ?case using finite_Psegments_included by auto
next
case (insertI_1 s b c)
have "P s"
proof -
have "s<c" using insertI_1 by auto
define S where "S = {x. P x} ∩ {s..(s+c)/2}"
have "closed S"
proof -
have "closed ({a. P a} ∩ {a..c})" using insertI_1(8) .
moreover have "S = ({a. P a} ∩ {a..c}) ∩ {s..(s+c)/2}"
using insertI_1(1,7) unfolding S_def by (auto simp add:field_simps)
ultimately show ?thesis
using closed_Int[of "{a. P a} ∩ {a..c}" "{s..(s+c)/2}"] by blast
qed
moreover have "∃y∈S. dist y s < e" when "e>0" for e
proof -
define y where "y = min ((s+c)/2) (e/2+s)"
have "y∈S"
proof -
have "y∈{s..(s+c)/2}" unfolding y_def
using ‹e>0› ‹s<c› by (auto simp add:min_mult_distrib_left algebra_simps)
moreover have "P y"
apply (rule insertI_1(3)[rule_format])
unfolding y_def
using ‹e>0› ‹s<c›
by (auto simp add:algebra_simps min_mult_distrib_left min_less_iff_disj)
ultimately show ?thesis unfolding S_def by auto
qed
moreover have "dist y s <e"
unfolding y_def using ‹e>0› ‹s<c›
by (auto simp add:algebra_simps min_mult_distrib_left min_less_iff_disj dist_real_def)
ultimately show ?thesis by auto
qed
ultimately have "s∈S" using closed_approachable by auto
then show ?thesis unfolding S_def by auto
qed
show ?case
proof (rule finite_Psegments.insertI_1[of s])
show " s ∈ {a..<c}" "s = a ∨ P s" "∀t∈{s<..<c}. P t"
using insertI_1 ‹P s› by auto
next
have "closed ({a. P a} ∩ {a..s})"
using closed_Int[OF ‹closed ({a. P a} ∩ {a..c})›,of "{a..s}",simplified]
apply (elim arg_elim[of closed])
using ‹s ∈ {b..<c}› ‹b ∈ {a..c}› by auto
then show "finite_Psegments P a s" using insertI_1 by auto
qed
next
case (insertI_2 s b c)
have ?case when "P s"
proof (rule finite_Psegments.insertI_2[of s])
show "s ∈ {a..<c}" "s = a ∨ P s" "∀t∈{s<..<c}. ¬ P t" using that insertI_2 by auto
next
have "closed ({a. P a} ∩ {a..s})"
using closed_Int[OF ‹closed ({a. P a} ∩ {a..c})›,of "{a..s}",simplified]
apply (elim arg_elim[of closed])
using  ‹s ∈ {b..<c}› ‹b ∈ {a..c}› by auto
then show "finite_Psegments P a s" using insertI_2 by auto
qed
moreover have ?case when "¬ P s" "s=b" using ‹finite_Psegments P a b›
proof (cases rule:finite_Psegments.cases)
case emptyI
then show ?thesis using insertI_2 that
by (metis antisym_conv atLeastAtMost_iff finite_Psegments.insertI_2)
next
case (insertI_1 s0)
have "P s"
proof -
have "s0<s" using insertI_1 atLeastLessThan_iff that(2) by blast
define S where "S = {x. P x} ∩ {(s0+s)/2..s}"
have "closed S"
using closed_Int[OF ‹closed ({a. P a} ∩ {a..c})›,of "{(s0+s)/2..s}",simplified]
apply (elim arg_elim[of closed])
unfolding S_def using ‹s0 ∈ {a..<b}› ‹ s ∈ {b..<c}› ‹b ∈ {a..c}› by auto
moreover have "∃y∈S. dist y s < e" when "e>0" for e
proof -
define y where "y = max ((s+s0)/2) (s-e/2)"
have "y∈S"
proof -
have "y∈{(s0+s)/2..s}" unfolding y_def
using ‹e>0› ‹s0<s› by (auto simp add:field_simps min_mult_distrib_left)
moreover have "P y"
apply (rule insertI_1(3)[rule_format])
unfolding y_def
using ‹e>0› ‹s0<s› ‹s=b›
by (auto simp add:field_simps max_mult_distrib_left less_max_iff_disj)
ultimately show ?thesis unfolding S_def by auto
qed
moreover have "dist y s <e"
unfolding y_def using ‹e>0› ‹s0<s›
by (auto simp add:algebra_simps max_mult_distrib_left less_max_iff_disj dist_real_def
ultimately show ?thesis by auto
qed
ultimately have "s∈S" using closed_approachable by auto
then show ?thesis unfolding S_def by auto
qed
then have False using ‹¬ P s› by auto
then show ?thesis by simp
next
case (insertI_2 s0)
have *: "∀t∈{s0<..<c}. ¬ P t"
using ‹ ∀t∈{s<..<c}. ¬ P t› that ‹∀t∈{s0<..<b}. ¬ P t›
by force
show ?thesis
apply (rule finite_Psegments.insertI_2[of s0])
subgoal using insertI_2.prems(2) local.insertI_2(1) by auto
subgoal using ‹s0 = a ∨ P s0› .
subgoal using * .
subgoal using ‹finite_Psegments P a s0› .
done
qed
moreover note ‹s = b ∨ P s›
ultimately show ?case by auto
qed

subsection ‹Finite segment intersection of a path with the imaginary axis›

definition finite_ReZ_segments::"(real ⇒ complex) ⇒ complex ⇒ bool" where
"finite_ReZ_segments g z = finite_Psegments (λt. Re (g t - z) = 0) 0 1"

lemma finite_ReZ_segments_joinpaths:
assumes g1:"finite_ReZ_segments g1 z" and g2: "finite_ReZ_segments g2 z" and
"path g1" "path g2" "pathfinish g1=pathstart g2"
shows "finite_ReZ_segments (g1+++g2) z"
proof -
define P where "P = (λt. (Re ((g1 +++ g2) t - z) = 0 ∧ 0<t ∧ t<1) ∨ t=0 ∨ t=1)"
have "finite_Psegments P 0 (1/2)"
proof -
have "finite_Psegments (λt. Re (g1 t - z) = 0) 0 1"
using g1 unfolding finite_ReZ_segments_def .
then have "finite_Psegments (λt. Re (g1 (2 * t) - z) = 0) 0 (1/2)"
apply (drule_tac finite_Psegments_pos_linear[of _ 2 0 0 "1/2",simplified])
then show ?thesis
unfolding P_def joinpaths_def
by (elim finite_Psegments_congE,auto)
qed
moreover have "finite_Psegments P (1/2) 1"
proof -
have "finite_Psegments (λt. Re (g2 t - z) = 0) 0 1"
using g2 unfolding finite_ReZ_segments_def .
then have "finite_Psegments (λt. Re (g2 (2 * t-1) - z) = 0) (1/2) 1"
apply (drule_tac finite_Psegments_pos_linear[of _ 2 "1/2" "-1" 1,simplified])
then show ?thesis
unfolding P_def joinpaths_def
apply (elim finite_Psegments_congE)
by auto
qed
moreover have "closed {x. P x}"
proof -
define Q where "Q=(λt. Re ((g1 +++ g2) t - z) = 0)"
have "continuous_on {0<..<1} (g1+++g2)"
using path_join_imp[OF ‹path g1› ‹path g2› ‹pathfinish g1=pathstart g2›]
unfolding path_def by (auto elim:continuous_on_subset)
from continuous_on_Re[OF this] have "continuous_on {0<..<1} (λx. Re ((g1 +++ g2) x))" .
from continuous_on_open_Collect_neq[OF this,of "λ_. Re z",OF continuous_on_const,simplified]
have "open {t. Re ((g1 +++ g2) t - z) ≠ 0 ∧ 0<t ∧ t<1}"
by (elim arg_elim[where f="open"],auto)
from closed_Diff[of "{0::real..1}",OF _ this,simplified]
show "closed {x. P x}"
apply (elim arg_elim[where f=closed])
qed
ultimately have "finite_Psegments P 0 1"
using finite_Psegments_combine[of _ 0 "1/2" 1] by auto
then show ?thesis
unfolding finite_ReZ_segments_def P_def
by (elim finite_Psegments_congE,auto)
qed

lemma finite_ReZ_segments_congE:
assumes "finite_ReZ_segments p1 z1"
"⋀t. ⟦0<t;t<1⟧ ⟹  Re(p1 t- z1) = Re(p2 t - z2)"
shows "finite_ReZ_segments p2 z2"
using assms unfolding finite_ReZ_segments_def
apply (elim finite_Psegments_congE)
by auto

lemma finite_ReZ_segments_constI:
assumes "∀t. 0<t∧t<1 ⟶ g t = c"
shows "finite_ReZ_segments g z"
proof -
have "finite_ReZ_segments (λ_. c) z"
unfolding finite_ReZ_segments_def
by (rule finite_Psegments_constI,auto)
then show ?thesis using assms
by (elim finite_ReZ_segments_congE,auto)
qed

lemma finite_ReZ_segment_cases [consumes 1, case_names subEq subNEq,cases pred:finite_ReZ_segments]:
assumes "finite_ReZ_segments g z"
and subEq:"(⋀s. ⟦s ∈ {0..<1};s=0∨Re (g s) = Re z;
∀t∈{s<..<1}. Re (g t) = Re z;finite_ReZ_segments (subpath 0 s g) z⟧ ⟹ P)"
and subNEq:"(⋀s. ⟦s ∈ {0..<1};s=0∨Re (g s) = Re z;
∀t∈{s<..<1}. Re (g t) ≠ Re z;finite_ReZ_segments (subpath 0 s g) z⟧ ⟹ P)"
shows "P"
using assms(1) unfolding finite_ReZ_segments_def
proof (cases rule:finite_Psegments.cases)
case emptyI
then show ?thesis by auto
next
case (insertI_1 s)
have "finite_ReZ_segments (subpath 0 s g) z"
proof (cases "s=0")
case True
show ?thesis
apply (rule finite_ReZ_segments_constI)
using True unfolding subpath_def by auto
next
case False
then have "s>0" using ‹s∈{0..<1}› by auto
from finite_Psegments_pos_linear[OF _ this,of _ 0 0 1] insertI_1(4)
show "finite_ReZ_segments (subpath 0 s g) z"
unfolding finite_ReZ_segments_def comp_def subpath_def by auto
qed
then show ?thesis using subEq insertI_1 by force
next
case (insertI_2 s)
have "finite_ReZ_segments (subpath 0 s g) z"
proof (cases "s=0")
case True
show ?thesis
apply (rule finite_ReZ_segments_constI)
using True unfolding subpath_def by auto
next
case False
then have "s>0" using ‹s∈{0..<1}› by auto
from finite_Psegments_pos_linear[OF _ this,of _ 0 0 1] insertI_2(4)
show "finite_ReZ_segments (subpath 0 s g) z"
unfolding finite_ReZ_segments_def comp_def subpath_def by auto
qed
then show ?thesis using subNEq insertI_2 by force
qed

lemma finite_ReZ_segments_induct [case_names sub0 subEq subNEq, induct pred:finite_ReZ_segments]:
assumes "finite_ReZ_segments g z"
assumes  sub0:"⋀g z. (P (subpath 0 0 g) z)"
and subEq:"(⋀s g z. ⟦s ∈ {0..<1};s=0∨Re (g s) = Re z;
∀t∈{s<..<1}. Re (g t) = Re z;finite_ReZ_segments (subpath 0 s g) z;
P (subpath 0 s g) z⟧ ⟹ P g z)"
and subNEq:"(⋀s g z. ⟦s ∈ {0..<1};s=0∨Re (g s) = Re z;
∀t∈{s<..<1}. Re (g t) ≠ Re z;finite_ReZ_segments (subpath 0 s g) z;
P (subpath 0 s g) z⟧ ⟹ P g z)"
shows "P g z"
proof -
have "finite_Psegments (λt. Re (g t - z) = 0) 0 1"
using assms(1) unfolding finite_ReZ_segments_def by auto
then have "(0::real)≤1 ⟶ P (subpath 0 1 g) z"
proof (induct rule: finite_Psegments.induct[of _ 0 1 "λa b. b≥a ⟶ P (subpath a b g) z"] )
case (emptyI a b)
then show ?case using sub0[of "subpath a b g"] unfolding subpath_def by auto
next
case (insertI_1 s a b)
have ?case when "a=b"
using sub0[of "subpath a b g"] that unfolding subpath_def by auto
moreover have ?case when "a≠b"
proof -
have "b>a" using that ‹s ∈ {a..<b}› by auto
define s'::real where "s'=(s-a)/(b-a)"
have "P (subpath a b g) z"
proof (rule subEq[of s' "subpath a b g"])
show "∀t∈{s'<..<1}. Re (subpath a b g t) = Re z"
proof
fix t assume "t ∈ {s'<..<1}"
then have "(b - a) * t + a∈{s<..<b}"
unfolding s'_def using ‹b>a› ‹s ∈ {a..<b}›
by (sos "((((A<0 * (A<1 * A<2)) * R<1) + (((A<=1 * (A<0 * R<1)) * (R<1 * [1]^2))
+ ((A<=0 * (A<0 * (A<1 * R<1))) * (R<1 * [1]^2)))))")
then have "Re (g ((b - a) * t + a) - z) = 0"
using insertI_1(3)[rule_format,of "(b - a) * t + a"] by auto
then show "Re (subpath a b g t) = Re z"
unfolding subpath_def by auto
qed
show "finite_ReZ_segments (subpath 0 s' (subpath a b g)) z"
proof (cases "s=a")
case True
then show ?thesis unfolding s'_def subpath_def
by (auto intro:finite_ReZ_segments_constI)
next
case False
have "finite_Psegments (λt. Re (g t - z) = 0) a s"
using insertI_1(4) unfolding finite_ReZ_segments_def by auto
then have "finite_Psegments ((λt. Re (g t - z) = 0) ∘ (λt. (s - a) * t + a)) 0 1"
apply (elim finite_Psegments_pos_linear[of _ "s-a" 0 a 1,simplified])
using False ‹s∈{a..<b}› by auto
then show ?thesis
using ‹b>a› unfolding finite_ReZ_segments_def subpath_def s'_def comp_def
by auto
qed
show "s' ∈ {0..<1}"
using ‹b>a› ‹s∈{a..<b}› unfolding s'_def
show "P (subpath 0 s' (subpath a b g)) z"
proof -
have "P (subpath a s g) z" using insertI_1(1,5) by auto
then show ?thesis
using ‹b>a› unfolding s'_def subpath_def  by simp
qed
show "s' = 0 ∨ Re (subpath a b g s') = Re z"
proof -
have ?thesis when "s=a"
using that unfolding s'_def by auto
moreover have ?thesis when "Re (g s - z) = 0"
using that unfolding s'_def subpath_def by auto
ultimately show ?thesis using ‹s = a ∨ Re (g s - z) = 0› by auto
qed
qed
then show ?thesis using ‹b>a› by auto
qed
ultimately show ?case by auto
next
case (insertI_2 s a b)
have ?case when "a=b"
using sub0[of "subpath a b g"] that unfolding subpath_def by auto
moreover have ?case when "a≠b"
proof -
have "b>a" using that ‹s ∈ {a..<b}› by auto
define s'::real where "s'=(s-a)/(b-a)"
have "P (subpath a b g) z"
proof (rule subNEq[of s' "subpath a b g"])
show "∀t∈{s'<..<1}. Re (subpath a b g t) ≠ Re z"
proof
fix t assume "t ∈ {s'<..<1}"
then have "(b - a) * t + a∈{s<..<b}"
unfolding s'_def using ‹b>a› ‹s ∈ {a..<b}›
by (sos "((((A<0 * (A<1 * A<2)) * R<1) + (((A<=1 * (A<0 * R<1)) * (R<1 * [1]^2)) +
((A<=0 * (A<0 * (A<1 * R<1))) * (R<1 * [1]^2)))))")
then have "Re (g ((b - a) * t + a) - z) ≠ 0"
using insertI_2(3)[rule_format,of "(b - a) * t + a"] by auto
then show "Re (subpath a b g t) ≠ Re z"
unfolding subpath_def by auto
qed
show "finite_ReZ_segments (subpath 0 s' (subpath a b g)) z"
proof (cases "s=a")
case True
then show ?thesis unfolding s'_def subpath_def
by (auto intro:finite_ReZ_segments_constI)
next
case False
have "finite_Psegments (λt. Re (g t - z) = 0) a s"
using insertI_2(4) unfolding finite_ReZ_segments_def by auto
then have "finite_Psegments ((λt. Re (g t - z) = 0) ∘ (λt. (s - a) * t + a)) 0 1"
apply (elim finite_Psegments_pos_linear[of _ "s-a" 0 a 1,simplified])
using False ‹s∈{a..<b}› by auto
then show ?thesis
using ‹b>a› unfolding finite_ReZ_segments_def subpath_def s'_def comp_def
by auto
qed
show "s' ∈ {0..<1}"
using ‹b>a› ‹s∈{a..<b}› unfolding s'_def
show "P (subpath 0 s' (subpath a b g)) z"
proof -
have "P (subpath a s g) z" using insertI_2(1,5) by auto
then show ?thesis
using ‹b>a› unfolding s'_def subpath_def  by simp
qed
show "s' = 0 ∨ Re (subpath a b g s') = Re z"
proof -
have ?thesis when "s=a"
using that unfolding s'_def by auto
moreover have ?thesis when "Re (g s - z) = 0"
using that unfolding s'_def subpath_def by auto
ultimately show ?thesis using ‹s = a ∨ Re (g s - z) = 0› by auto
qed
qed
then show ?thesis using ‹b>a› by auto
qed
ultimately show ?case by auto
qed
then show ?thesis by auto
qed

lemma finite_ReZ_segments_shiftpah:
assumes "finite_ReZ_segments g z" "s∈{0..1}" "path g" and loop:"pathfinish g = pathstart g"
shows "finite_ReZ_segments (shiftpath s g) z"
proof -
have "finite_Psegments (λt. Re (shiftpath s g t - z) = 0) 0 (1-s)"
proof -
have "finite_Psegments (λt. Re (g t) = Re z) s 1"
using assms finite_Psegments_included[of _ 0 1 s] unfolding finite_ReZ_segments_def
by force
then have "finite_Psegments (λt. Re (g (s + t) - z) = 0) 0 (1-s)"
using finite_Psegments_pos_linear[of "λt. Re (g t - z) =0" 1 0 s "1-s",simplified]
unfolding comp_def by (auto simp add:algebra_simps)
then show ?thesis unfolding shiftpath_def
apply (elim finite_Psegments_congE)
using ‹s∈{0..1}› by auto
qed
moreover have "finite_Psegments (λt. Re (shiftpath s g t - z) = 0) (1-s) 1"
proof -
have "finite_Psegments (λt. Re (g t) = Re z) 0 s "
using assms finite_Psegments_included unfolding finite_ReZ_segments_def
by force
then have "finite_Psegments (λt. Re (g (s + t - 1) - z) = 0) (1-s) 1"
using finite_Psegments_pos_linear[of "λt. Re (g t - z) =0" 1 "1-s" "s-1" 1,simplified]
unfolding comp_def by (auto simp add:algebra_simps)
then show ?thesis unfolding shiftpath_def
apply (elim finite_Psegments_congE)
using ‹s∈{0..1}› by auto
qed
moreover have "1 - s ∈ {0..1}" using ‹s∈{0..1}› by auto
moreover have "closed ({x. Re (shiftpath s g x - z) = 0} ∩ {0..1})"
proof -
let ?f = "λx. Re (shiftpath s g x - z)"
have "continuous_on {0..1} ?f"
using path_shiftpath[OF ‹path g› loop ‹s∈{0..1}›] unfolding path_def
by (auto intro: continuous_intros)
from continuous_closed_preimage_constant[OF this,of 0,simplified]
show ?thesis
apply (elim arg_elim[of closed])
by force
qed
ultimately show ?thesis unfolding finite_ReZ_segments_def
by (rule finite_Psegments_combine[where b="1-s"])
qed

lemma finite_imp_finite_ReZ_segments:
assumes "finite {t. Re (g t - z) = 0 ∧ 0 ≤ t ∧ t≤1}"
shows "finite_ReZ_segments g z"
proof -
define P where "P = (λt. Re (g t - z) = 0)"
define rs where "rs=(λb. {t. P t ∧ 0 < t ∧ t<b})"
have "finite_Psegments P 0 b" when "finite (rs b)" "b>0" for b
using that
proof (induct "card (rs b)" arbitrary:b rule:nat_less_induct)
case ind:1
have ?case when "rs b= {}"
apply (rule finite_Psegments.intros(3)[of 0])
using that ‹0 < b› unfolding rs_def by (auto intro:finite_Psegments.intros)
moreover have ?case when "rs b≠{}"
proof -
define lj where "lj = Max (rs b)"
have "0<lj" "lj<b" "P lj"
using Max_in[OF ‹finite (rs b)› ‹rs b≠{}›,folded lj_def]
unfolding rs_def by auto
show ?thesis
proof (rule finite_Psegments.intros(3)[of lj])
show "lj ∈ {0..<b}" " lj = 0 ∨ P lj"
using ‹0<lj› ‹lj<b› ‹P lj› by auto
show "∀t∈{lj<..<b}. ¬ P t"
proof (rule ccontr)
assume " ¬ (∀t∈{lj<..<b}. ¬ P t) "
then obtain t where t:"P t" "lj < t" "t < b" by auto
then have "t∈rs b" unfolding rs_def using ‹lj>0› by auto
then have "t≤lj" using Max_ge[OF ‹finite (rs b)›,of t] unfolding lj_def by auto
then show False using ‹t>lj› by auto
qed
show "finite_Psegments P 0 lj"
proof (rule ind.hyps[rule_format,of "card (rs lj)" lj,simplified])
show "finite (rs lj)"
using ‹finite (rs b)› unfolding rs_def using ‹lj<b›
by (auto elim!:rev_finite_subset )
show "card (rs lj) < card (rs b)"
apply (rule psubset_card_mono[OF ‹finite (rs b)›])
using Max_in ‹finite (rs lj)› ‹lj < b› lj_def rs_def that by fastforce
show "0 < lj" using ‹0<lj› .
qed
qed
qed
ultimately show ?case by auto
qed
moreover have "finite (rs 1)"
using assms unfolding rs_def P_def
by (auto elim:rev_finite_subset)
ultimately have "finite_Psegments P 0 1" by auto
then show ?thesis unfolding P_def finite_ReZ_segments_def .
qed

lemma finite_ReZ_segments_poly_linepath:
shows "finite_ReZ_segments (poly p o linepath a b) z"
proof -
define P where "P=map_poly Re (pcompose (p-[:z:]) [:a,b-a:])"
have *:"Re ((poly p ∘ linepath a b) t - z) = 0 ⟷ poly P t=0" for t
unfolding inner_complex_def P_def linepath_def comp_def
apply (subst Re_poly_of_real[symmetric])
by (auto simp add: algebra_simps poly_pcompose scaleR_conv_of_real)
have ?thesis when "P≠0"
proof -
have "finite {t. poly P t=0}" using that poly_roots_finite by auto
then have "finite {t. Re ((poly p ∘ linepath a b) t - z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}"
using *
by auto
then show ?thesis
using finite_imp_finite_ReZ_segments[of "poly p o linepath a b" z] by auto
qed
moreover have ?thesis when "P=0"
unfolding finite_ReZ_segments_def
apply (rule finite_Psegments_constI[where c=True])
apply (subst *)
using that by auto
ultimately show ?thesis by auto
qed

lemma part_circlepath_half_finite_inter:
assumes "st≠tt" "r≠0" "c≠0"
shows "finite {t. part_circlepath z0 r st tt t ∙ c = d ∧ 0≤ t ∧ t≤1}" (is "finite ?T")
proof -
let ?S = "{θ. (z0+r*exp (𝗂 * θ )) ∙ c = d ∧ θ ∈ closed_segment st tt}"
define S where "S ≡ {θ. (z0+r*exp (𝗂 * θ )) ∙ c = d ∧ θ ∈ closed_segment st tt}"
have "S = linepath st tt ` ?T"
proof
define g where "g≡(λt. (t-st)/(tt -st))"
have "0≤g t" "g t≤1" when "t ∈ closed_segment st tt " for t
using that ‹st≠tt› closed_segment_eq_real_ivl unfolding  g_def real_scaleR_def
moreover have "linepath st tt (g t) =t" "g (linepath st tt t) = t" for t
unfolding linepath_def g_def real_scaleR_def using ‹st≠tt›
ultimately have "x∈linepath st tt ` ?T" when "x∈S" for x
using that unfolding S_def
by (auto intro!:image_eqI[where x="g x"] simp add:part_circlepath_def)
then show "S ⊆ linepath st tt ` ?T" by auto
next
have "x∈S" when "x∈linepath st tt ` ?T" for x
using that unfolding part_circlepath_def S_def
then show "linepath st tt ` ?T ⊆ S" by auto
qed
moreover have "finite S"
proof -
define a' b' c' where "a'=r * Re c" and "b' = r* Im c" and "c'=Im c * Im z0 + Re z0 * Re c - d"
define f where "f θ= a' * cos θ + b' * sin θ + c'" for θ
have "(z0+r*exp (𝗂 * θ )) ∙ c = d ⟷ f θ = 0" for θ
unfolding exp_Euler inner_complex_def f_def a'_def b'_def c'_def
by (auto simp add:algebra_simps cos_of_real sin_of_real)
then have *:"S = roots f ∩ closed_segment st tt"
unfolding S_def roots_within_def by auto
have "uniform_discrete S"
proof -
have "a' ≠ 0 ∨ b' ≠ 0 ∨ c' ≠ 0"
using assms complex_eq_iff unfolding a'_def b'_def c'_def
by auto
then have "periodic_set (roots f) (4 * pi)"
using periodic_set_sin_cos_linear[of a' b' c',folded f_def] by auto
then have "uniform_discrete (roots f)" using periodic_imp_uniform_discrete by auto
then show ?thesis unfolding * by auto
qed
moreover have "bounded S" unfolding *
ultimately show ?thesis using uniform_discrete_finite_iff by auto
qed
moreover have "inj_on (linepath st tt) ?T"
proof -
have "inj (linepath st tt)"
unfolding linepath_def using assms inj_segment by blast
then show ?thesis by (auto elim:subset_inj_on)
qed
ultimately show ?thesis by (auto elim!: finite_imageD)
qed

lemma linepath_half_finite_inter:
assumes "a ∙ c ≠ d ∨ b ∙ c ≠ d"
shows "finite {t. linepath a b t ∙ c = d ∧ 0≤ t ∧ t≤1}" (is "finite ?S")
proof (rule ccontr)
assume asm:"infinite ?S"
obtain t1 t2 where u1u2:"t1≠t2" "t1∈?S" "t2∈?S"
proof -
obtain t1 where "t1∈?S" using not_finite_existsD asm by blast
moreover have "∃u2. u2∈?S-{t1}"
using infinite_remove[OF asm,of t1]
by (meson finite.emptyI rev_finite_subset subsetI)
ultimately show ?thesis using that by auto
qed
have t1:"(1-t1)*(a ∙ c) + t1 * (b ∙ c) = d"
using ‹t1∈?S› unfolding linepath_def by (simp add: inner_left_distrib)
have t2:"(1-t2)*(a ∙ c) + t2 * (b ∙ c) = d"
using ‹t2∈?S› unfolding linepath_def by (simp add: inner_left_distrib)
have "a ∙ c = d"
proof -
have "t2*((1-t1)*(a ∙ c) + t1 * (b ∙ c)) = t2*d" using t1 by auto
then have *:"(t2-t1*t2)*(a ∙ c) + t1*t2 * (b ∙ c) = t2*d" by (auto simp add:algebra_simps)
have "t1*((1-t2)*(a ∙ c) + t2 * (b ∙ c)) = t1*d" using t2 by auto
then have **:"(t1-t1*t2)*(a ∙ c) + t1*t2 * (b ∙ c) = t1*d" by (auto simp add:algebra_simps)
have "(t2-t1)*(a ∙ c) = (t2-t1)*d" using arg_cong2[OF * **,of minus]
then show ?thesis using ‹t1≠t2› by auto
qed
moreover have "b ∙ c = d"
proof -
have "(1-t2)*((1-t1)*(a ∙ c) + t1 * (b ∙ c)) = (1-t2)*d" using t1 by auto
then have *:"(1-t1)*(1-t2)*(a ∙ c) + (t1-t1*t2) * (b ∙ c) = (1-t2)*d" by (auto simp add:algebra_simps)
have "(1-t1)*((1-t2)*(a ∙ c) + t2 * (b ∙ c)) = (1-t1)*d" using t2 by auto
then have **:"(1-t1)*(1-t2)*(a ∙ c) + (t2-t1*t2) * (b ∙ c) = (1-t1)*d" by (auto simp add:algebra_simps)
have "(t2-t1)*(b ∙ c) = (t2-t1)*d" using arg_cong2[OF ** *,of minus]
then show ?thesis using ‹t1≠t2› by auto
qed
ultimately show False using assms by auto
qed

lemma finite_half_joinpaths_inter:
assumes "finite {t. l1 t ∙ c = d ∧ 0≤ t ∧ t≤1}" "finite {t. l2 t ∙ c = d ∧ 0≤ t ∧ t≤1}"
shows "finite {t. (l1+++l2) t ∙ c = d ∧ 0≤ t ∧ t≤1}"
proof -
let ?l1s = "{t. l1 (2*t) ∙ c = d ∧ 0≤ t ∧ t≤1/2}"
let ?l2s = "{t. l2 (2 * t - 1) ∙ c = d ∧ 1/2< t ∧ t≤1}"
let ?ls = "λl. {t. l t ∙ c = d ∧ 0≤ t ∧ t≤1}"
have "{t. (l1+++l2) t ∙ c = d ∧ 0≤ t ∧ t≤1} = ?l1s ∪ ?l2s"
unfolding joinpaths_def by auto
moreover have "finite ?l1s"
proof -
have "?l1s = ((*) (1/2)) ` ?ls l1" by (auto intro:rev_image_eqI)
thus ?thesis using assms by simp
qed
moreover have "finite ?l2s"
proof -
have "?l2s ⊆ (λx. x/2 + 1/2) ` ?ls l2" by (auto intro:rev_image_eqI simp add:field_simps)
thus ?thesis using assms
by (auto elim:finite_subset)
qed
ultimately show ?thesis by simp
qed

lemma finite_ReZ_segments_linepath:
"finite_ReZ_segments (linepath a b) z"
proof -
have ?thesis when "Re a≠Re z ∨ Re b ≠Re z"
proof -
let ?S1="{t. Re (linepath a b t-z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}"
have "finite ?S1"
using linepath_half_finite_inter[of a "Complex 1 0" "Re z" b] that
using one_complex.code by auto
from finite_imp_finite_ReZ_segments[OF this] show ?thesis .
qed
moreover have ?thesis when "Re a=Re z" "Re b=Re z"
unfolding finite_ReZ_segments_def
apply (rule finite_Psegments.intros(2)[of 0])
using that unfolding linepath_def by (auto simp add:algebra_simps intro:finite_Psegments.intros)
ultimately show ?thesis by blast
qed

lemma finite_ReZ_segments_part_circlepath:
"finite_ReZ_segments (part_circlepath z0 r st tt) z"
proof -
have ?thesis when "st ≠ tt" "r ≠ 0"
proof -
let ?S1="{t. Re (part_circlepath z0 r st tt t-z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}"
have "finite ?S1"
using part_circlepath_half_finite_inter[of st tt r "Complex 1 0" z0 "Re z"] that one_complex.code
from finite_imp_finite_ReZ_segments[OF this] show ?thesis .
qed
moreover have ?thesis when "st =tt ∨ r=0"
proof -
define c where "c = z0 + r * exp (𝗂 *  tt)"
have "part_circlepath z0 r st tt = (λt. c)"
unfolding part_circlepath_def c_def using that linepath_refl by auto
then show ?thesis
using finite_ReZ_segments_linepath[of c c z] linepath_refl[of c]
by auto
qed
ultimately show ?thesis by blast
qed

lemma finite_ReZ_segments_poly_of_real:
shows "finite_ReZ_segments (poly p o of_real) z"
using finite_ReZ_segments_poly_linepath[of p 0 1 z] unfolding linepath_def

lemma finite_ReZ_segments_subpath:
assumes "finite_ReZ_segments g z"
"0≤u" "u≤v" "v≤1"
shows "finite_ReZ_segments (subpath u v g) z"
proof (cases "u=v")
case True
then show ?thesis
unfolding subpath_def by (auto intro:finite_ReZ_segments_constI)
next
case False
then have "u<v" using ‹u≤v› by auto
define P where "P=(λt. Re (g t - z) = 0)"
have "finite_ReZ_segments (subpath u v g) z
= finite_Psegments (P o (λt. (v - u) * t + u)) 0 1"
unfolding finite_ReZ_segments_def subpath_def P_def comp_def by auto
also have "..."
apply (rule finite_Psegments_pos_linear)
using assms False unfolding finite_ReZ_segments_def
by (fold P_def,auto elim:finite_Psegments_included)
finally show ?thesis .
qed

subsection ‹jump and jumpF›

definition jump::"(real ⇒ real) ⇒ real ⇒ int" where
"jump f a = (if
(LIM x (at_left a). f x :> at_bot) ∧ (LIM x (at_right a). f x :> at_top)
then 1 else if
(LIM x (at_left a). f x :> at_top) ∧ (LIM x (at_right a). f x :> at_bot)
then -1 else 0)"

definition jumpF::"(real ⇒ real) ⇒ real filter ⇒ real" where
"jumpF f F ≡ (if filterlim f at_top F then 1/2 else
if filterlim f at_bot F then -1/2 else (0::real))"

lemma jumpF_const[simp]:
assumes "F≠bot"
shows "jumpF (λ_. c) F = 0"
proof -
have False when "LIM x F. c :> at_bot"
using filterlim_at_bot_nhds[OF that _ ‹F≠bot›] by auto
moreover have False when "LIM x F. c :> at_top"
using filterlim_at_top_nhds[OF that _ ‹F≠bot›] by auto
ultimately show ?thesis unfolding jumpF_def by auto
qed

lemma jumpF_not_infinity:
assumes "continuous F g" "F≠bot"
shows "jumpF g F = 0"
proof -
have "¬ filterlim g at_infinity F"
using not_tendsto_and_filterlim_at_infinity[OF ‹F ≠bot› assms(1)[unfolded continuous_def]]
by auto
then have "¬ filterlim g at_bot F" "¬ filterlim g at_top F"
using at_bot_le_at_infinity at_top_le_at_infinity filterlim_mono by blast+
then show ?thesis unfolding jumpF_def by auto
qed

lemma jumpF_linear_comp:
assumes "c≠0"
shows
"jumpF (f o (λx. c*x+b)) (at_left x) =
(if c>0 then jumpF f (at_left (c*x+b)) else jumpF f (at_right (c*x+b)))"
(is ?case1)
"jumpF (f o (λx. c*x+b)) (at_right x) =
(if c>0 then jumpF f (at_right (c*x+b)) else jumpF f (at_left (c*x+b)))"
(is ?case2)
proof -
let ?g = "λx. c*x+b"
have ?case1 ?case2 when "¬ c>0"
proof -
have "c<0" using ‹c≠0› that by auto
have "filtermap ?g (at_left x) = at_right (?g x)"
"filtermap ?g (at_right x) = at_left (?g x)"
using ‹c<0›
filtermap_linear_at_left[OF ‹c≠0›, of b x]
filtermap_linear_at_right[OF ‹c≠0›, of b x] by auto
then have
"jumpF (f ∘ ?g) (at_left x) = jumpF f (at_right (?g x))"
"jumpF (f ∘ ?g) (at_right x) = jumpF f (at_left (?g x))"
unfolding jumpF_def filterlim_def comp_def
by (auto simp add: filtermap_filtermap[of f ?g,symmetric])
then show ?case1 ?case2 using ‹c<0› by auto
qed
moreover have ?case1 ?case2 when "c>0"
proof -
have "filtermap ?g (at_left x) = at_left (?g x)"
"filtermap ?g (at_right x) = at_right (?g x)"
using that
filtermap_linear_at_left[OF ‹c≠0›, of b x]
filtermap_linear_at_right[OF ‹c≠0›, of b x] by auto
then have
"jumpF (f ∘ ?g) (at_left x) = jumpF f (at_left (?g x))"
"jumpF (f ∘ ?g) (at_right x) = jumpF f (at_right (?g x))"
unfolding jumpF_def filterlim_def comp_def
by (auto simp add: filtermap_filtermap[of f ?g,symmetric])
then show ?case1 ?case2 using that by auto
qed
ultimately show ?case1 ?case2 by auto
qed

lemma jump_const[simp]:"jump (λ_. c) a = 0"
proof -
have False when "LIM x (at_left a). c :> at_bot"
apply (rule not_tendsto_and_filterlim_at_infinity[of "at_left a" "λ_. c" c])
apply auto
using at_bot_le_at_infinity filterlim_mono that by blast
moreover have False when "LIM x (at_left a). c :> at_top"
apply (rule not_tendsto_and_filterlim_at_infinity[of "at_left a" "λ_. c" c])
apply auto
using at_top_le_at_infinity filterlim_mono that by blast
ultimately show ?thesis unfolding jump_def by auto
qed

lemma jump_not_infinity:
"isCont f a ⟹ jump f a =0"
by (meson at_bot_le_at_infinity at_top_le_at_infinity filterlim_at_split
filterlim_def isCont_def jump_def not_tendsto_and_filterlim_at_infinity
order_trans trivial_limit_at_left_real)

lemma jump_jump_poly_aux:
assumes "p≠0" "coprime p q"
shows "jump (λx. poly q x / poly p x) a = jump_poly q p a"
proof (cases "q=0")
case True
then show ?thesis by auto
next
case False
define f where "f ≡ (λx. poly q x / poly p x)"
have ?thesis when "poly q a = 0"
proof -
have "poly p a≠0" using coprime_poly_0[OF ‹coprime p q›] that by blast
then have "isCont f a" unfolding f_def by simp
then have "jump f a=0" using jump_not_infinity by auto
moreover have "jump_poly q p a=0"
using jump_poly_not_root[OF ‹poly p a≠0›] by auto
ultimately show ?thesis unfolding f_def by auto
qed
moreover have ?thesis when "poly q a≠0"
proof (cases "even(order a p)")
case True
define c where "c≡sgn (poly q a)"
note
filterlim_divide_at_bot_at_top_iff
[OF _ that,of "poly q"  "at_left a" "poly p",folded f_def c_def,simplified]
filterlim_divide_at_bot_at_top_iff
[OF _ that,of "poly q"  "at_right a" "poly p",folded f_def c_def,simplified]
moreover have "(poly p has_sgnx - c) (at_left a) = (poly p has_sgnx - c) (at_right a)"
"(poly p has_sgnx c) (at_left a) = (poly p has_sgnx c) (at_right a)"
using poly_has_sgnx_left_right[OF ‹p≠0›] True by auto
moreover have "c≠0" by (simp add: c_def sgn_if that)
then have False when
"(poly p has_sgnx - c) (at_right a)"
"(poly p has_sgnx c) (at_right a)"
using has_sgnx_unique[OF _ that] by auto
ultimately have "jump f a = 0"
unfolding jump_def by auto
moreover have "jump_poly q p a = 0" unfolding jump_poly_def
using True by (simp add: order_0I that)
ultimately show ?thesis unfolding f_def by auto
next
case False
define c where "c≡sgn (poly q a)"
have "(poly p ⤏ 0) (at a)" using False
by (metis even_zero order_0I poly_tendsto(1))
then have "(poly p ⤏ 0) (at_left a)" and "(poly p ⤏ 0) (at_right a)"
moreover note
filterlim_divide_at_bot_at_top_iff
[OF _ that,of "poly q" _ "poly p",folded f_def c_def]
moreover have "(poly p has_sgnx c) (at_left a) = (poly p has_sgnx - c) (at_right a)"
"(poly p has_sgnx - c) (at_left a) = (poly p has_sgnx c) (at_right a)"
using poly_has_sgnx_left_right[OF ‹p≠0›] False by auto
ultimately have "jump f a = (if (poly p has_sgnx c) (at_right a) then 1
else if (poly p has_sgnx - c) (at_right a) then -1 else 0)"
unfolding jump_def by auto
also have "... = (if sign_r_pos (q * p) a then 1 else - 1)"
proof -
have "(poly p has_sgnx c) (at_right a) ⟷  sign_r_pos (q * p) a "
proof
assume "(poly p has_sgnx c) (at_right a)"
then have "sgnx (poly p) (at_right a) = c" by auto
moreover have "sgnx (poly q) (at_right a) = c"
unfolding c_def using that by (auto intro!: tendsto_nonzero_sgnx)
ultimately have "sgnx (λx. poly (q*p) x) (at_right a) = c * c"
moreover have "c≠0" by (simp add: c_def sgn_if that)
ultimately have "sgnx (λx. poly (q*p) x) (at_right a) > 0"
using not_real_square_gt_zero by fastforce
then show "sign_r_pos (q * p) a" using sign_r_pos_sgnx_iff
by blast
next
assume asm:"sign_r_pos (q * p) a"
let ?c1 = "sgnx (poly p) (at_right a)"
let ?c2 = "sgnx (poly q) (at_right a)"
have "0 < sgnx (λx. poly (q * p) x) (at_right a)"
using asm sign_r_pos_sgnx_iff by blast
then have "?c2 * ?c1 >0"
apply (subst (asm) poly_mult)
apply (subst (asm) sgnx_times)
by auto
then have "?c2>0 ∧ ?c1>0 ∨ ?c2<0 ∧ ?c1<0"
then have "?c1=?c2"
using sgnx_values[OF sgnx_able_poly(1), of a,simplified]
moreover have "sgnx (poly q) (at_right a) = c"
unfolding c_def using that by (auto intro!: tendsto_nonzero_sgnx)
ultimately have "?c1 = c" by auto
then show "(poly p has_sgnx c) (at_right a)"
using sgnx_able_poly(1) sgnx_able_sgnx by blast
qed
then show ?thesis
unfolding jump_poly_def using poly_has_sgnx_values[OF ‹p≠0›]
by (metis add.inverse_inverse c_def sgn_if that)
qed
also have "... = jump_poly q p a"
unfolding jump_poly_def using False order_root that by (simp add: order_root assms(1))
finally show ?thesis unfolding f_def by auto
qed
ultimately show ?thesis by auto
qed

lemma jump_jumpF:
assumes cont:"isCont (inverse o f) a" and
sgnxl:"(f has_sgnx l) (at_left a)" and sgnxr:"(f has_sgnx r) (at_right a)" and
"l≠0 " "r≠0"
shows "jump f a = jumpF f (at_right a) - jumpF f (at_left a)"
proof -
have ?thesis when "filterlim f at_bot (at_left a)" "filterlim f at_top (at_right a)"
unfolding jump_def jumpF_def
using that filterlim_at_top_at_bot[OF _ _ trivial_limit_at_left_real]
by auto
moreover have ?thesis when "filterlim f at_top (at_left a)" "filterlim f at_bot (at_right a)"
unfolding jump_def jumpF_def
using that filterlim_at_top_at_bot[OF _ _ trivial_limit_at_right_real]
by auto
moreover have ?thesis when
"¬ filterlim f at_bot (at_left a) ∨ ¬ filterlim f at_top (at_right a)"
"¬ filterlim f at_top (at_left a) ∨ ¬ filterlim f at_bot (at_right a)"
proof (cases "f a=0")
case False
have "jumpF f (at_right a) = 0" "jumpF f (at_left a) = 0"
proof -
have "isCont (inverse o inverse o f) a" using cont False unfolding comp_def
by (rule_tac continuous_at_within_inverse, auto)
then have "isCont f a" unfolding comp_def by auto
then have "(f ⤏ f a) (at_right a)" "(f ⤏ f a) (at_left a)"
unfolding continuous_at_split by (auto simp add:continuous_within)
moreover note trivial_limit_at_left_real trivial_limit_at_right_real
ultimately show "jumpF f (at_right a) = 0" "jumpF f (at_left a) = 0"
unfolding jumpF_def using filterlim_at_bot_nhds filterlim_at_top_nhds
by metis+
qed
then show ?thesis unfolding jump_def using that by auto
next
case True
then have tends0:"((λx. inverse (f x)) ⤏ 0) (at a)"
using cont unfolding isCont_def comp_def by auto
have "jump f a = 0" using that unfolding jump_def by auto
have r_lim:"if r>0 then filterlim f at_top (at_right a) else filterlim f at_bot (at_right a)"
proof (cases "r>0")
case True
then have "∀⇩F x in (at_right a). 0 < f x"
using sgnxr unfolding has_sgnx_def
by (auto elim:eventually_mono)
then have "filterlim f at_top (at_right a)"
using filterlim_inverse_at_top[of "λx. inverse (f x)", simplified] tends0
unfolding filterlim_at_split by auto
then show ?thesis using True by presburger
next
case False
then have "∀⇩F x in (at_right a). 0 > f x"
using sgnxr ‹r≠0› False unfolding has_sgnx_def
apply (elim eventually_mono)
by (meson linorder_neqE_linordered_idom sgn_less)
then have "filterlim f at_bot (at_right a)"
using filterlim_inverse_at_bot[of "λx. inverse (f x)", simplified] tends0
unfolding filterlim_at_split by auto
then show ?thesis using False by simp
qed
have l_lim:"if l>0 then filterlim f at_top (at_left a) else filterlim f at_bot (at_left a)"
proof (cases "l>0")
case True
then have "∀⇩F x in (at_left a). 0 < f x"
using sgnxl unfolding has_sgnx_def
by (auto elim:eventually_mono)
then have "filterlim f at_top (at_left a)"
using filterlim_inverse_at_top[of "λx. inverse (f x)", simplified] tends0
unfolding filterlim_at_split by auto
then show ?thesis using True by presburger
next
case False
then have "∀⇩F x in (at_left a). 0 > f x"
using sgnxl ‹l≠0› False unfolding has_sgnx_def
apply (elim eventually_mono)
by (meson linorder_neqE_linordered_idom sgn_less)
then have "filterlim f at_bot (at_left a)"
using filterlim_inverse_at_bot[of "λx. inverse (f x)", simplified] tends0
unfolding filterlim_at_split by auto
then show ?thesis using False by simp
qed

have ?thesis when "l>0" "r>0"
using that l_lim r_lim ‹jump f a=0› unfolding jumpF_def by auto
moreover have ?thesis when "¬ l>0" "¬ r>0"
proof -
have "filterlim f at_bot (at_right a)" "filterlim f at_bot (at_left a)"
using r_lim l_lim that by auto
moreover then have "¬ filterlim f at_top (at_right a)" "¬ filterlim f at_top (at_left a)"
by (auto elim: filterlim_at_top_at_bot)
ultimately have "jumpF f (at_right a) = -1/2 "  "jumpF f (at_left a) = -1/2"
unfolding jumpF_def by auto
then show ?thesis using ‹jump f a=0› by auto
qed
moreover have ?thesis when "l>0" "¬ r>0"
proof -
note ‹¬ filterlim f at_top (at_left a) ∨ ¬ filterlim f at_bot (at_right a)›
moreover have "filterlim f at_bot (at_right a)" "filterlim f at_top (at_left a)"
using r_lim l_lim that by auto
ultimately have False by auto
then show ?thesis by auto
qed
moreover have ?thesis when "¬ l>0" "r>0"
proof -
note ‹¬ filterlim f at_bot (at_left a) ∨ ¬ filterlim f at_top (at_right a)›
moreover have "filterlim f at_bot (at_left a)" "filterlim f at_top (at_right a)"
using r_lim l_lim that by auto
ultimately have False by auto
then show ?thesis by auto
qed
ultimately show ?thesis by auto
qed
ultimately show ?thesis by auto
qed

lemma jump_linear_comp:
assumes "c≠0"
shows "jump (f o (λx. c*x+b)) x = (if c>0 then jump f (c*x+b) else -jump f (c*x+b))"
proof (cases "c>0")
case False
then have "c<0" using ‹c≠0› by auto
let ?g = "λx. c*x+b"
have "filtermap ?g (at_left x) = at_right (?g x)"
"filtermap ?g (at_right x) = at_left (?g x)"
using ‹c<0›
filtermap_linear_at_left[OF ‹c≠0›, of b x]
filtermap_linear_at_right[OF ‹c≠0›, of b x] by auto
then have "jump (f ∘ ?g) x = - jump f (c * x + b)"
unfolding jump_def filterlim_def comp_def
apply (auto simp add: filtermap_filtermap[of f ?g,symmetric])
apply (fold filterlim_def)
by (auto elim:filterlim_at_top_at_bot)
then show ?thesis using ‹c<0› by auto
next
case True
let ?g = "λx. c*x+b"
have "filtermap ?g (at_left x) = at_left (?g x)"
"filtermap ?g (at_right x) = at_right (?g x)"
using True
filtermap_linear_at_left[OF ‹c≠0›, of b x]
filtermap_linear_at_right[OF ‹c≠0›, of b x] by auto
then have "jump (f ∘ ?g) x = jump f (c * x + b)"
unfolding jump_def filterlim_def comp_def
by (auto simp add: filtermap_filtermap[of f ?g,symmetric])
then show ?thesis using True by auto
qed

lemma jump_divide_derivative:
assumes "isCont f x" "g x = 0" "f x≠0"
and g_deriv:"(g has_field_derivative c) (at x)" and "c≠0"
shows "jump (λt. f t/g t) x = (if sgn c = sgn ( f x) then 1 else -1)"
proof -
have g_tendsto:"(g ⤏ 0) (at_left x)" "(g ⤏ 0) (at_right x)"
by (metis DERIV_isCont Lim_at_imp_Lim_at_within assms(2) assms(4) continuous_at)+
have f_tendsto:"(f ⤏ f x) (at_left x)" "(f ⤏ f x) (at_right x)"
using Lim_at_imp_Lim_at_within assms(1) continuous_at by blast+

have ?thesis when "c>0" "f x>0"
proof -
have "(g has_sgnx - sgn (f x)) (at_left x)"
using has_sgnx_derivative_at_left[OF g_deriv ‹g x=0›] that by auto
moreover have "(g has_sgnx sgn (f x)) (at_right x)"
using has_sgnx_derivative_at_right[OF g_deriv ‹g x=0›] that by auto
ultimately have "(LIM t at_left x. f t / g t :> at_bot) ∧ (LIM t at_right x. f t / g t :> at_top)"
using filterlim_divide_at_bot_at_top_iff[OF _ ‹f x≠0›, of f]
using f_tendsto(1) f_tendsto(2) g_tendsto(1) g_tendsto(2) by blast
moreover have "sgn c = sgn (f x)" using that by auto
ultimately show ?thesis unfolding jump_def by auto
qed
moreover have ?thesis when "c>0" "f x<0"
proof -
have "(g has_sgnx sgn (f x)) (at_left x)"
using has_sgnx_derivative_at_left[OF g_deriv ‹g x=0›] that by auto
moreover have "(g has_sgnx - sgn (f x)) (at_right x)"
using has_sgnx_derivative_at_right[OF g_deriv ‹g x=0›] that by auto
ultimately have "(LIM t at_left x. f t / g t :> at_top) ∧ (LIM t at_right x. f t / g t :> at_bot)"
using filterlim_divide_at_bot_at_top_iff[OF _ ‹f x≠0›, of f]
using f_tendsto(1) f_tendsto(2) g_tendsto(1) g_tendsto(2) by blast
moreover from this have "¬ (LIM t at_left x. f t / g t :> at_bot)"
using filterlim_at_top_at_bot by fastforce
moreover have "sgn c ≠ sgn (f x)" using that by auto
ultimately show ?thesis unfolding jump_def by auto
qed
moreover have ?thesis when "c<0" "f x>0"
proof -
have "(g has_sgnx sgn (f x)) (at_left x)"
using has_sgnx_derivative_at_left[OF g_deriv ‹g x=0›] that by auto
moreover have "(g has_sgnx - sgn (f x)) (at_right x)"
using has_sgnx_derivative_at_right[OF g_deriv ‹g x=0›] that by auto
ultimately have "(LIM t at_left x. f t / g t :> at_top) ∧ (LIM t at_right x. f t / g t :> at_bot)"
using filterlim_divide_at_bot_at_top_iff[OF _ ‹f x≠0›, of f]
using f_tendsto(1) f_tendsto(2) g_tendsto(1) g_tendsto(2) by blast
moreover from this have "¬ (LIM t at_left x. f t / g t :> at_bot)"
using filterlim_at_top_at_bot by fastforce
moreover have "sgn c ≠ sgn (f x)" using that by auto
ultimately show ?thesis unfolding jump_def by auto
qed
moreover have ?thesis when "c<0" "f x<0"
proof -
have "(g has_sgnx - sgn (f x)) (at_left x)"
using has_sgnx_derivative_at_left[OF g_deriv ‹g x=0›] that by auto
moreover have "(g has_sgnx sgn (f x)) (at_right x)"
using has_sgnx_derivative_at_right[OF g_deriv ‹g x=0›] that by auto
ultimately have "(LIM t at_left x. f t / g t :> at_bot) ∧ (LIM t at_right x. f t / g t :> at_top)"
using filterlim_divide_at_bot_at_top_iff[OF _ ‹f x≠0›, of f]
using f_tendsto(1) f_tendsto(2) g_tendsto(1) g_tendsto(2) by blast
moreover have "sgn c =sgn (f x)" using that by auto
ultimately show ?thesis unfolding jump_def by auto
qed
ultimately show ?thesis using ‹c≠0› ‹f x≠0› by argo
qed

lemma jump_jump_poly: "jump (λx. poly q x / poly p x) a = jump_poly q p a"
proof (cases "p=0")
case True
then show ?thesis by auto
next
case False
obtain p' q' where p':"p= p'*gcd p q" and q':"q=q'*gcd p q"
using gcd_dvd1 gcd_dvd2 dvd_def[of "gcd p q", simplified mult.commute]  by metis
then have "coprime p' q'" "p'≠0" "gcd p q≠0" using gcd_coprime ‹p≠0›  by auto

define f where "f ≡ (λx. poly q' x / poly p' x)"
define g where "g ≡ (λx. if poly (gcd p q) x = 0 then 0::real else 1)"

have g_tendsto:"(g ⤏ 1) (at_left a)" "(g ⤏ 1) (at_right a)"
proof -
have
"(poly (gcd p q) has_sgnx 1) (at_left a)
∨ (poly (gcd p q) has_sgnx - 1) (at_left a)"
"(poly (gcd p q) has_sgnx 1) (at_right a)
∨ (poly (gcd p q) has_sgnx - 1) (at_right a)"
using ‹p≠0› poly_has_sgnx_values by auto
then have " ∀⇩F x in at_left a. g x = 1" " ∀⇩F x in at_right a. g x = 1"
unfolding has_sgnx_def g_def by (auto elim:eventually_mono)
then show "(g ⤏ 1) (at_left a)" "(g ⤏ 1) (at_right a)"
using tendsto_eventually by auto
qed

have "poly q x / poly p x = g x * f x" for x
unfolding f_def g_def by (subst p',subst q',auto)
then have "jump (λx. poly q x / poly p x) a = jump (λx. g x * f x) a"
by auto
also have "... = jump f a"
unfolding jump_def
apply (subst (1 2) filterlim_tendsto_pos_mult_at_top_iff)
prefer 5
apply (subst (1 2) filterlim_tendsto_pos_mult_at_bot_iff)
using g_tendsto by auto
also have "... = jump_poly q' p' a"
using jump_jump_poly_aux[OF ‹p'≠0› ‹coprime p' q'›] unfolding f_def by auto
also have "... = jump_poly q p a"
using jump_poly_mult[OF ‹gcd p q ≠ 0›, of q'] p' q'
by (metis mult.commute)
finally show ?thesis .
qed

lemma jump_Im_divide_Re_0:
assumes "path g" "Re (g x)≠0" "0<x" "x<1"
shows "jump (λt. Im (g t) / Re (g t)) x = 0"
proof -
have "isCont g x"
using ‹path g›[unfolded path_def] ‹0<x› ‹x<1›
apply (elim continuous_on_interior)
by auto
then have "isCont (λt. Im(g t)/Re(g t)) x" using ‹Re (g x)≠0›
by (auto intro:continuous_intros isCont_Re isCont_Im)
then show "jump (λt. Im(g t)/Re(g t)) x=0"
using jump_not_infinity by auto
qed

lemma jumpF_im_divide_Re_0:
assumes "path g" "Re (g x)≠0"
shows "⟦0≤x;x<1⟧ ⟹ jumpF (λt. Im (g t) / Re (g t)) (at_right x) = 0"
"⟦0<x;x≤1⟧ ⟹ jumpF (λt. Im (g t) / Re (g t)) (at_left x) = 0"
proof -
define g' where "g' = (λt. Im (g t) / Re (g t))"

show "jumpF g' (at_right x) = 0" when "0≤x" "x<1"
proof -
have "(g' ⤏ g' x) (at_right x)"
proof (cases "x=0")
case True
have "continuous (at_right 0) g"
using ‹path g› unfolding path_def
by (auto elim:continuous_on_at_right)
then have "continuous (at_right x) (λt. Im(g t))" "continuous (at_right x) (λt. Re(g t))"
using continuous_Im continuous_Re True by auto
moreover have "Re (g (netlimit (at_right x))) ≠ 0"
using assms(2) by (simp add: Lim_ident_at)
ultimately have "continuous (at_right x) (λt. Im (g t)/Re(g t))"
by (auto intro:continuous_divide)
then show ?thesis unfolding g'_def continuous_def
next
case False
have "isCont (λx. Im (g x)) x" "isCont (λx. Re (g x)) x"
using ‹path g› unfolding path_def
by (metis False atLeastAtMost_iff at_within_Icc_at continuous_Im continuous_Re
continuous_on_eq_continuous_within less_le that)+
then have "isCont g' x"
using assms(2) unfolding g'_def
by (auto intro:continuous_intros)
then show ?thesis unfolding isCont_def using filterlim_at_split by blast
qed
then have "¬ filterlim g' at_top (at_right x)" "¬ filterlim g' at_bot (at_right x)"
using filterlim_at_top_nhds[of g' "at_right x"] filterlim_at_bot_nhds[of g' "at_right x"]
by auto
then show ?thesis unfolding jumpF_def by auto
qed

show "jumpF g' (at_left x) = 0" when "0<x" "x≤1"
proof -
have "(g' ⤏ g' x) (at_left x)"
proof (cases "x=1")
case True
have "continuous (at_left 1) g"
using ‹path g› unfolding path_def
by (auto elim:continuous_on_at_left)
then have "continuous (at_left x) (λt. Im(g t))" "continuous (at_left x) (λt. Re(g t))"
using continuous_Im continuous_Re True by auto
moreover have "Re (g (netlimit (at_left x))) ≠ 0"
using assms(2) by (simp add: Lim_ident_at)
ultimately have "continuous (at_left x) (λt. Im (g t)/Re(g t))"
by (auto intro:continuous_divide)
then show ?thesis unfolding g'_def continuous_def
next
case False
have "isCont (λx. Im (g x)) x" "isCont (λx. Re (g x)) x"
using ‹path g› unfolding path_def
by (metis False atLeastAtMost_iff at_within_Icc_at continuous_Im continuous_Re
continuous_on_eq_continuous_within less_le that)+
then have "isCont g' x"
using assms(2) unfolding g'_def
by (auto)
then show ?thesis unfolding isCont_def using filterlim_at_split by blast
qed
then have "¬ filterlim g' at_top (at_left x)" "¬ filterlim g' at_bot (at_left x)"
using filterlim_at_top_nhds[of g' "at_left x"] filterlim_at_bot_nhds[of g' "at_left x"]
by auto
then show ?thesis unfolding jumpF_def by auto
qed
qed

lemma jump_cong:
assumes "x=y" and "eventually (λx. f x=g x) (at x)"
shows "jump f x = jump g y"
proof -
have left:"eventually (λx. f x=g x) (at_left x)"
and right:"eventually (λx. f x=g x) (at_right x)"
using assms(2) eventually_at_split by blast+
from filterlim_cong[OF _ _ this(1)] filterlim_cong[OF _ _ this(2)]
show ?thesis unfolding jump_def using assms(1) by fastforce
qed

lemma jumpF_cong:
assumes "F=G" and "eventually (λx. f x=g x) F"
shows "jumpF f F = jumpF g G"
proof -
have "∀⇩F r in G. f r = g r"
using assms(1) assms(2) by force
then show ?thesis
by (simp add: assms(1) filterlim_cong jumpF_def)
qed

lemma jump_at_left_at_right_eq:
assumes "isCont f x" and "f x ≠ 0" and sgnx_eq:"sgnx g (at_left x) = sgnx g (at_right x)"
shows "jump (λt. f t/g t) x = 0"
proof -
define c where "c = sgn (f x)"
then have "c≠0" using ‹f x≠0› by (simp add: sgn_zero_iff)
have f_tendsto:"(f ⤏ f x) (at_left x)" " (f ⤏ f x) (at_right x)"
using ‹isCont f x› Lim_at_imp_Lim_at_within isCont_def by blast+
have False when "(g has_sgnx - c) (at_left x)" "(g has_sgnx c) (at_right x)"
proof -
have "sgnx g (at_left x) = -c" using that(1) by auto
moreover have "sgnx g (at_right x) = c" using that(2) by auto
ultimately show False using sgnx_eq ‹c≠0› by force
qed
moreover have False when "(g has_sgnx c) (at_left x)" "(g has_sgnx - c) (at_right x)"
proof -
have "sgnx g (at_left x) = c" using that(1) by auto
moreover have "sgnx g (at_right x) = - c" using that(2) by auto
ultimately show False using sgnx_eq ‹c≠0› by force
qed
ultimately show ?thesis
unfolding jump_def
by (auto simp add:f_tendsto filterlim_divide_at_bot_at_top_iff[OF _ ‹f x ≠ 0›] c_def)
qed

lemma jumpF_pos_has_sgnx:
assumes "jumpF f F > 0"
shows "(f has_sgnx 1) F"
proof -
have "filterlim f at_top F" using assms unfolding jumpF_def by argo
then have "eventually (λx. f x>0) F" using filterlim_at_top_dense[of f F] by blast
then show ?thesis unfolding has_sgnx_def
apply (elim eventually_mono)
by auto
qed

lemma jumpF_neg_has_sgnx:
assumes "jumpF f F < 0"
shows "(f has_sgnx -1) F"
proof -
have "filterlim f at_bot F" using assms unfolding jumpF_def by argo
then have "eventually (λx. f x<0) F" using filterlim_at_bot_dense[of f F] by blast
then show ?thesis unfolding has_sgnx_def
apply (elim eventually_mono)
by auto
qed

lemma jumpF_IVT:
fixes f::"real ⇒ real" and a b::real
defines "right≡(λ(R::real ⇒ real ⇒ bool). R (jumpF f (at_right a)) 0
∨ (continuous (at_right a) f ∧ R (f a) 0))"
and
"left≡(λ(R::real ⇒ real ⇒ bool). R (jumpF f (at_left b)) 0
∨ (continuous (at_left b) f ∧ R (f b) 0))"
assumes "a<b" and cont:"continuous_on {a<..<b} f" and
right_left:"right greater ∧ left less ∨ right less ∧ left greater"
shows "∃x. a<x ∧ x<b ∧ f x =0"
proof -
have ?thesis when "right greater" "left less"
proof -
have "(f has_sgnx 1) (at_right a)"
proof -
have ?thesis when "jumpF f (at_right a)>0" using jumpF_pos_has_sgnx[OF that] .
moreover have ?thesis when "f a > 0" "continuous (at_right a) f"
proof -
have "(f ⤏ f a) (at_right a)" using that(2) by (simp add: continuous_within)
then show ?thesis
using tendsto_nonzero_has_sgnx[of f "f a" "at_right a"] that by auto
qed
ultimately show ?thesis using that(1) unfolding right_def by auto
qed
then obtain a' where "a<a'" and a'_def:"∀y. a<y ∧ y < a' ⟶ f y > 0"
unfolding has_sgnx_def eventually_at_right using sgn_1_pos by auto
have "(f has_sgnx - 1) (at_left b)"
proof -
have ?thesis when "jumpF f (at_left b)<0" using jumpF_neg_has_sgnx[OF that] .
moreover have ?thesis when "f b < 0" "continuous (at_left b) f"
proof -
have "(f ⤏ f b) (at_left b)"
using that(2) by (simp add: continuous_within)
then show ?thesis
using tendsto_nonzero_has_sgnx[of f "f b" "at_left b"] that by auto
qed
ultimately show ?thesis using that(2) unfolding left_def by auto
qed
then obtain b' where "b'<b" and b'_def:"∀y. b'<y ∧ y < b ⟶ f y < 0"
unfolding has_sgnx_def eventually_at_left using sgn_1_neg by auto
have "a' ≤ b'"
proof (rule ccontr)
assume "¬ a' ≤ b'"
then have "{a<..<a'} ∩ {b'<..<b} ≠ {}"
using ‹a<a'› ‹b'<b› ‹a<b› by auto
then obtain c where "c∈{a<..<a'}" "c∈{b'<..<b}" by blast
then have "f c>0" "f c<0"
using a'_def b'_def by auto
then show False by auto
qed
define a0 where "a0=(a+a')/2"
define b0 where "b0=(b+b')/2"
have [simp]:"a<a0" "a0<a'" "a0<b0" "b'<b0" "b0<b"
unfolding a0_def b0_def using ‹a<a'› ‹b'<b› ‹a'≤b'› by auto
have "f a0>0" "f b0<0" using a'_def[rule_format,of a0] b'_def[rule_format,of b0] by auto
moreover have "continuous_on {a0..b0} f"
using cont ‹a < a0› ‹b0 < b›
by (meson atLeastAtMost_subseteq_greaterThanLessThan_iff continuous_on_subset)
ultimately have "∃x>a0. x < b0 ∧ f x = 0"
using IVT_strict[of 0 f a0 b0] by auto
then show ?thesis using ‹a < a0› ‹b0 < b›
by (meson lessThan_strict_subset_iff psubsetE subset_psubset_trans)
qed
moreover have ?thesis when "right less" "left greater"
proof -
have "(f has_sgnx -1) (at_right a)"
proof -
have ?thesis when "jumpF f (at_right a)<0" using jumpF_neg_has_sgnx[OF that] .
moreover have ?thesis when "f a < 0" "continuous (at_right a) f"
proof -
have "(f ⤏ f a) (at_right a)"
using that(2) by (simp add: continuous_within)
then show ?thesis
using tendsto_nonzero_has_sgnx[of f "f a" "at_right a"] that by auto
qed
ultimately show ?thesis using that(1) unfolding right_def by auto
qed
then obtain a' where "a<a'" and a'_def:"∀y. a<y ∧ y < a' ⟶ f y < 0"
unfolding has_sgnx_def eventually_at_right using sgn_1_neg by auto
have "(f has_sgnx  1) (at_left b)"
proof -
have ?thesis when "jumpF f (at_left b)>0" using jumpF_pos_has_sgnx[OF that] .
moreover have ?thesis when "f b > 0" "continuous (at_left b) f"
proof -
have "(f ⤏ f b) (at_left b)"
using that(2) by (simp add: continuous_within)
then show ?thesis
using tendsto_nonzero_has_sgnx[of f "f b" "at_left b"] that by auto
qed
ultimately show ?thesis using that(2) unfolding left_def by auto
qed
then obtain b' where "b'<b" and b'_def:"∀y. b'<y ∧ y < b ⟶ f y > 0"
unfolding has_sgnx_def eventually_at_left using sgn_1_pos by auto
have "a' ≤ b'"
proof (rule ccontr)
assume "¬ a' ≤ b'"
then have "{a<..<a'} ∩ {b'<..<b} ≠ {}"
using ‹a<a'› ‹b'<b› ‹a<b› by auto
then obtain c where "c∈{a<..<a'}" "c∈{b'<..<b}" by blast
then have "f c>0" "f c<0"
using a'_def b'_def by auto
then show False by auto
qed
define a0 where "a0=(a+a')/2"
define b0 where "b0=(b+b')/2"
have [simp]:"a<a0" "a0<a'" "a0<b0" "b'<b0" "b0<b"
unfolding a0_def b0_def using ‹a<a'› ‹b'<b› ‹a'≤b'› by auto
have "f a0<0" "f b0>0" using a'_def[rule_format,of a0] b'_def[rule_format,of b0] by auto
moreover have "continuous_on {a0..b0} f"
using cont  ‹a < a0› ‹b0 < b›
by (meson atLeastAtMost_subseteq_greaterThanLessThan_iff continuous_on_subset)
ultimately have "∃x>a0. x < b0 ∧ f x = 0"
using IVT_strict[of 0 f a0 b0] by auto
then show ?thesis using ‹a < a0› ‹b0 < b›
by (meson lessThan_strict_subset_iff psubsetE subset_psubset_trans)
qed
ultimately show ?thesis using right_left by auto
qed

lemma jumpF_eventually_const:
assumes "eventually (λx. f x=c) F" "F≠bot"
shows "jumpF f F = 0"
proof -
have "jumpF f F = jumpF (λ_. c) F"
apply (rule jumpF_cong)
using assms(1) by auto
also have "... = 0" using jumpF_const[OF ‹F≠bot›] by simp
finally show ?thesis .
qed

lemma jumpF_tan_comp:
"jumpF (f o tan) (at_right x) = (if cos x = 0
then jumpF f at_bot else jumpF f (at_right (tan x)))"
"jumpF (f o tan) (at_left x) = (if cos x =0
then jumpF f at_top else jumpF f (at_left (tan x)))"
proof -
have "filtermap (f ∘ tan) (at_right x) =
(if cos x = 0 then filtermap f at_bot else filtermap f (at_right (tan x)))"
unfolding comp_def
apply (subst filtermap_filtermap[of f tan,symmetric])
using filtermap_tan_at_right_inf filtermap_tan_at_right by auto
then show "jumpF (f o tan) (at_right x) = (if cos x = 0
then jumpF f at_bot else jumpF f (at_right (tan x)))"
unfolding jumpF_def filterlim_def by auto
next
have "filtermap (f ∘ tan) (at_left x) =
(if cos x = 0 then filtermap f at_top else filtermap f (at_left (tan x)))"
unfolding comp_def
apply (subst filtermap_filtermap[of f tan,symmetric])
using filtermap_tan_at_left_inf filtermap_tan_at_left by auto
then show "jumpF (f o tan) (at_left x) = (if cos x = 0
then jumpF f at_top else jumpF f (at_left (tan x)))"
unfolding jumpF_def filterlim_def by auto
qed

subsection ‹Finite jumpFs over an interval›

definition finite_jumpFs::"(real ⇒ real) ⇒ real ⇒ real ⇒  bool" where
"finite_jumpFs f a b = finite {x. (jumpF f (at_left x) ≠0 ∨ jumpF f (at_right x) ≠0) ∧ a≤x ∧ x≤b}"

lemma finite_jumpFs_linear_pos:
assumes "c>0"
shows "finite_jumpFs (f o (λx. c * x + b)) lb ub ⟷ finite_jumpFs f (c * lb +b) (c * ub + b)"
proof -
define left where "left = (λf lb ub. {x. jumpF f (at_left x) ≠ 0 ∧ lb ≤ x ∧ x ≤ ub})"
define right where "right = (λf lb ub. {x. jumpF f (at_right x) ≠ 0 ∧ lb ≤ x ∧ x ≤ ub})"
define g where "g=(λx. c*x+b)"
define gi where "gi = (λx. (x-b)/c)"
have "finite_jumpFs (f o (λx. c * x + b)) lb ub
= finite (left (f o g) lb ub ∪ right (f o g) lb ub)"
unfolding finite_jumpFs_def
apply (rule arg_cong[where f=finite])
by (auto simp add:left_def right_def g_def)
also have "... = finite (gi ` (left f (g lb) (g ub) ∪ right f (g lb) (g ub)))"
proof -
have j_rw:
"jumpF (f o g) (at_left x) = jumpF f (at_left (g x))"
"jumpF (f o g) (at_right x) = jumpF f (at_right (g x))"
for x
using jumpF_linear_comp[of c f b x] ‹c>0› unfolding g_def by auto
then have
"left (f o g) lb ub = gi ` left f (g lb) (g ub)"
"right (f o g) lb ub = gi ` right f (g lb) (g ub)"
unfolding left_def right_def gi_def
using ‹c>0› by (auto simp add:g_def field_simps)
then have "left (f o g) lb ub ∪ right (f o g) lb ub
= gi ` (left f (g lb) (g ub) ∪ right f (g lb) (g ub))"
by auto
then show ?thesis by auto
qed
also have "... = finite (left f (g lb) (g ub) ∪ right f (g lb) (g ub))"
apply (rule finite_image_iff)
unfolding gi_def using ‹c >0›  inj_on_def by fastforce
also have "... =  finite_jumpFs f (c * lb +b) (c * ub + b)"
unfolding finite_jumpFs_def
apply (rule arg_cong[where f=finite])
by (auto simp add:left_def right_def g_def)
finally show ?thesis .
qed

lemma finite_jumpFs_consts:
"finite_jumpFs (λ_ . c) lb ub"
unfolding finite_jumpFs_def using jumpF_const by auto

lemma finite_jumpFs_combine:
assumes "finite_jumpFs f a b" "finite_jumpFs f b c"
shows "finite_jumpFs f a c"
proof -
define P where "P=(λx. jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0)"
have "{x. P x ∧ a ≤ x ∧ x ≤ c} ⊆ {x. P x ∧ a ≤ x ∧ x≤b} ∪ {x. P x ∧ b ≤x ∧ x≤c}"
by auto
moreover have "finite ({x. P x ∧ a ≤ x ∧ x≤b} ∪ {x. P x ∧ b ≤x ∧ x≤c})"
using assms unfolding finite_jumpFs_def P_def by auto
ultimately have "finite {x. P x ∧ a ≤ x ∧ x ≤ c}"
using finite_subset by auto
then show ?thesis unfolding finite_jumpFs_def P_def by auto
qed

lemma finite_jumpFs_subE:
assumes "finite_jumpFs f a b" "a≤a'" "b'≤b"
shows "finite_jumpFs f a' b'"
using assms unfolding finite_jumpFs_def
apply (elim rev_finite_subset)
by auto

lemma finite_Psegments_Re_imp_jumpFs:
assumes "finite_Psegments (λt. Re (g t - z) = 0) a b" "continuous_on {a..b} g"
shows "finite_jumpFs (λt. Im (g t - z)/Re (g t - z)) a b"
using assms
proof (induct rule:finite_Psegments.induct)
case (emptyI a b)
then show ?case unfolding finite_jumpFs_def
by (auto intro:rev_finite_subset[of "{a}"])
next
case (insertI_1 s a b)
define f where "f=(λt. Im (g t - z) / Re (g t - z))"
have "finite_jumpFs f a s"
proof -
have "continuous_on {a..s} g" using ‹continuous_on {a..b} g› ‹s ∈ {a..<b}›
by (auto elim:continuous_on_subset)
then show ?thesis using insertI_1 unfolding f_def by auto
qed
moreover have "finite_jumpFs f s b"
proof -
have "jumpF f (at_left x) =0" "jumpF f (at_right x) = 0" when "x∈{s<..<b}" for x
proof -
show "jumpF f (at_left x) =0"
apply (rule jumpF_eventually_const[of _ 0])
unfolding eventually_at_left
apply (rule exI[where x=s])
using that insertI_1 unfolding f_def by auto
show "jumpF f (at_right x) = 0"
apply (rule jumpF_eventually_const[of _ 0])
unfolding eventually_at_right
apply (rule exI[where x=b])
using that insertI_1 unfolding f_def by auto
qed
then have "{x. (jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0) ∧ s ≤ x ∧ x ≤ b}
= {x. (jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0) ∧ (x=s ∨ x = b)}"
using  ‹s∈{a..<b}› by force
then show ?thesis unfolding finite_jumpFs_def by auto
qed
ultimately show ?case using finite_jumpFs_combine[of _ a s b] unfolding f_def by auto
next
case (insertI_2 s a b)
define f where "f=(λt. Im (g t - z) / Re (g t - z))"
have "finite_jumpFs f a s"
proof -
have "continuous_on {a..s} g" using ‹continuous_on {a..b} g› ‹s ∈ {a..<b}›
by (auto elim:continuous_on_subset)
then show ?thesis using insertI_2 unfolding f_def by auto
qed
moreover have "finite_jumpFs f s b"
proof -
have "jumpF f (at_left x) =0" "jumpF f (at_right x) = 0" when "x∈{s<..<b}" for x
proof -
have "isCont f x"
unfolding f_def
apply (intro continuous_intros isCont_Im isCont_Re
continuous_on_interior[OF ‹continuous_on {a..b} g›])
using insertI_2.hyps(1) that
apply auto[2]
using insertI_2.hyps(3) that by blast
then show "jumpF f (at_left x) =0" "jumpF f (at_right x) = 0"
qed
then have "{x. (jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0) ∧ s ≤ x ∧ x ≤ b}
= {x. (jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0) ∧ (x=s ∨ x = b)}"
using  ‹s∈{a..<b}› by force
then show ?thesis unfolding finite_jumpFs_def by auto
qed
ultimately show ?case using finite_jumpFs_combine[of _ a s b] unfolding f_def by auto
qed

lemma finite_ReZ_segments_imp_jumpFs:
assumes "finite_ReZ_segments g z" "path g"
shows "finite_jumpFs (λt. Im (g t - z)/Re (g t - z)) 0 1"
using assms unfolding finite_ReZ_segments_def path_def
by (rule finite_Psegments_Re_imp_jumpFs)

subsection ‹@{term jumpF} at path ends›

definition jumpF_pathstart::"(real ⇒ complex) ⇒ complex ⇒ real" where
"jumpF_pathstart g z= jumpF (λt. Im(g t- z)/Re(g t - z)) (at_right 0)"

definition jumpF_pathfinish::"(real ⇒ complex) ⇒ complex ⇒ real" where
"jumpF_pathfinish g z= jumpF (λt. Im(g t - z)/Re(g t -z)) (at_left 1)"

lemma jumpF_pathstart_eq_0:
assumes "path g" "Re(pathstart g)≠Re z"
shows "jumpF_pathstart g z = 0"
unfolding jumpF_pathstart_def
apply (rule jumpF_im_divide_Re_0)
using assms[unfolded pathstart_def] by auto

lemma jumpF_pathfinish_eq_0:
assumes "path g" "Re(pathfinish g)≠Re z"
shows "jumpF_pathfinish g z = 0"
unfolding jumpF_pathfinish_def
apply (rule jumpF_im_divide_Re_0)
using assms[unfolded pathfinish_def] by auto

lemma
shows jumpF_pathfinish_reversepath: "jumpF_pathfinish (reversepath g) z = jumpF_pathstart g z"
and jumpF_pathstart_reversepath: "jumpF_pathstart (reversepath g) z = jumpF_pathfinish g z"
proof -
define f where "f=(λt. Im (g t - z) / Re (g t - z))"
define f' where "f'=(λt. Im (reversepath g t - z) / Re (reversepath g t - z))"
have "f o (λt. 1 - t) = f'"
unfolding f_def f'_def comp_def reversepath_def by auto
then show "jumpF_pathfinish (reversepath g) z = jumpF_pathstart g z"
"jumpF_pathstart (reversepath g) z = jumpF_pathfinish g z"
unfolding jumpF_pathstart_def jumpF_pathfinish_def
using jumpF_linear_comp(2)[of "-1" f 1 0,simplified] jumpF_linear_comp(1)[of "-1" f 1 1,simplified]
apply (fold f_def f'_def)
by auto
qed

lemma jumpF_pathstart_joinpaths[simp]:
"jumpF_pathstart (g1+++g2) z = jumpF_pathstart g1 z"
proof -
let ?h="(λt. Im (g1 t - z) / Re (g1 t - z))"
let ?f="λt. Im ((g1 +++ g2) t - z) / Re ((g1 +++ g2) t - z)"
have "jumpF_pathstart g1 z = jumpF ?h (at_right 0)"
unfolding jumpF_pathstart_def by simp
also have "... = jumpF (?h o (λt. 2*t)) (at_right 0)"
using jumpF_linear_comp[of 2 ?h 0 0,simplified] by auto
also have "... = jumpF ?f (at_right 0)"
proof (rule jumpF_cong)
show " ∀⇩F x in at_right 0. (?h ∘ (*) 2) x =?f x"
unfolding eventually_at_right
apply (intro exI[where x="1/2"])
qed simp
also have "... =jumpF_pathstart (g1+++g2) z"
unfolding jumpF_pathstart_def by simp
finally show ?thesis by simp
qed

lemma jumpF_pathfinish_joinpaths[simp]:
"jumpF_pathfinish (g1+++g2) z = jumpF_pathfinish g2 z"
proof -
let ?h="(λt. Im (g2 t - z) / Re (g2 t - z))"
let ?f="λt. Im ((g1 +++ g2) t - z) / Re ((g1 +++ g2) t - z)"
have "jumpF_pathfinish g2 z = jumpF ?h (at_left 1)"
unfolding jumpF_pathfinish_def by simp
also have "... = jumpF (?h o (λt. 2*t-1)) (at_left 1)"
using jumpF_linear_comp[of 2 _ "-1" 1,simplified] by auto
also have "... = jumpF ?f (at_left 1)"
proof (rule jumpF_cong)
show " ∀⇩F x in at_left 1. (?h ∘ (λt. 2 * t - 1)) x =?f x"
unfolding eventually_at_left
apply (intro exI[where x="1/2"])
qed simp
also have "... =jumpF_pathfinish (g1+++g2) z"
unfolding jumpF_pathfinish_def by simp
finally show ?thesis by simp
qed

subsection ‹Cauchy index›

―‹Deprecated, use "cindexE" if possible›
definition cindex::"real ⇒ real ⇒ (real ⇒ real) ⇒ int" where
"cindex a b f = (∑x∈{x. jump f x≠0 ∧ a<x ∧ x<b}. jump f x )"

definition cindexE::"real ⇒ real ⇒ (real ⇒ real) ⇒ real" where
"cindexE a b f = (∑x∈{x. jumpF f (at_right x) ≠0 ∧ a≤x ∧ x<b}. jumpF f (at_right x))
- (∑x∈{x. jumpF f (at_left x) ≠0 ∧ a<x ∧ x≤b}. jumpF f (at_left x))"

definition cindexE_ubd::"(real ⇒ real) ⇒ real" where
"cindexE_ubd f = (∑x∈{x. jumpF f (at_right x) ≠0 }. jumpF f (at_right x))
- (∑x∈{x. jumpF f (at_left x) ≠0}. jumpF f (at_left x))"

lemma cindexE_empty:
"cindexE a a f = 0"
unfolding cindexE_def by (simp add: sum.neutral)

lemma cindex_const: "cindex a b (λ_. c) = 0"
unfolding cindex_def
apply (rule sum.neutral)
by auto

lemma cindex_eq_cindex_poly: "cindex a b (λx. poly q x/poly p x) = cindex_poly a b q p"
proof (cases "p=0")
case True
then show ?thesis using cindex_const by auto
next
case False
have "cindex_poly a b q p =
(∑x |jump_poly q p x ≠0 ∧ a < x ∧ x < b. jump_poly q p x)"
unfolding cindex_poly_def
apply (rule sum.mono_neutral_cong_right)
using jump_poly_not_root by (auto simp add: ‹p≠0› poly_roots_finite)
also have "... = cindex a b (λx. poly q x/poly p x)"
unfolding cindex_def
apply (rule sum.cong)
using jump_jump_poly[of q] by auto
finally show ?thesis by auto
qed

lemma cindex_combine:
assumes finite:"finite {x. jump f x≠0 ∧ a<x ∧ x<c}" and "a<b" "b<c"
shows "cindex a c f = cindex a b f  + jump f b + cindex b c f"
proof -
define ssum where "ssum = (λs. sum (jump f) ({x. jump f x≠0 ∧ a<x ∧ x<c} ∩ s))"
have ssum_union:"ssum (A ∪ B) = ssum A + ssum B" when "A ∩ B ={}" for A B
proof -
define C where "C={x. jump f x ≠ 0 ∧ a<x ∧ x<c}"
have "finite C" using finite unfolding C_def .
then show ?thesis
unfolding ssum_def
apply (fold C_def)
using sum_Un[of "C ∩ A" "C ∩ B"] that
by (simp add: inf_assoc inf_sup_aci(3) inf_sup_distrib1 sum.union_disjoint)
qed
have "cindex a c f = ssum ({a<..<b} ∪ {b} ∪ {b<..<c})"
unfolding ssum_def cindex_def
apply (rule sum.cong[of _ _ "jump f" "jump f",simplified])
using ‹a<b› ‹b<c› by fastforce
moreover have "cindex a b f = ssum {a<..<b}"
unfolding cindex_def ssum_def using ‹a<b› ‹b<c›
by (intro sum.cong,auto)
moreover have "jump f b = ssum {b}"
unfolding ssum_def using ‹a<b› ‹b<c›  by (cases "jump f b=0",auto)
moreover have "cindex b c f = ssum {b<..<c}"
unfolding cindex_def ssum_def using ‹a<b› ‹b<c›  by (intro sum.cong,auto)
ultimately show ?thesis
apply (subst (asm) ssum_union,simp)
by (subst (asm) ssum_union,auto)
qed

lemma cindexE_combine:
assumes finite:"finite_jumpFs f a c" and "a≤b" "b≤c"
shows "cindexE a c f = cindexE a b f + cindexE b c f"
proof -
define S where "S={x. (jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0) ∧ a ≤ x ∧ x ≤ c}"
define A0 where "A0={x. jumpF f (at_right x) ≠ 0 ∧ a ≤ x ∧ x < c}"
define A1 where "A1={x. jumpF f (at_right x) ≠ 0 ∧ a ≤ x ∧ x < b}"
define A2 where "A2={x. jumpF f (at_right x) ≠ 0 ∧ b ≤ x ∧ x < c}"
define B0 where "B0={x. jumpF f (at_left x) ≠ 0 ∧ a < x ∧ x ≤ c}"
define B1 where "B1={x. jumpF f (at_left x) ≠ 0 ∧ a < x ∧ x ≤ b}"
define B2 where "B2={x. jumpF f (at_left x) ≠ 0 ∧ b < x ∧ x ≤ c}"
have [simp]:"finite A1" "finite A2" "finite B1" "finite B2"
proof -
have "finite S" using finite unfolding finite_jumpFs_def S_def by auto
moreover have "A1 ⊆ S" "A2 ⊆ S" "B1 ⊆ S" "B2 ⊆ S"
unfolding A1_def A2_def B1_def B2_def S_def using ‹a≤b› ‹b≤c› by auto
ultimately show "finite A1" "finite A2" "finite B1" "finite B2" by (auto elim:finite_subset)
qed
have "cindexE a c f = sum (λx. jumpF f (at_right x)) A0
- sum (λx. jumpF f (at_left x)) B0"
unfolding cindexE_def A0_def B0_def by auto
also have "... = sum (λx. jumpF f (at_right x)) (A1 ∪ A2)
- sum (λx. jumpF f (at_left x)) (B1 ∪ B2)"
proof -
have "A0=A1∪A2" unfolding A0_def A1_def A2_def using assms by auto
moreover have "B0=B1∪B2" unfolding B0_def B1_def B2_def using assms by auto
ultimately show ?thesis by auto
qed
also have "... = cindexE a b f + cindexE b c f"
proof -
have "A1 ∩ A2 = {}" unfolding A1_def A2_def by auto
moreover have "B1 ∩ B2 = {}" unfolding B1_def B2_def by auto
ultimately show ?thesis
unfolding cindexE_def
apply (fold A1_def A2_def B1_def B2_def)
qed
finally show ?thesis .
qed

lemma cindex_linear_comp:
assumes "c≠0"
shows "cindex lb ub (f o (λx. c*x+b)) = (if c>0
then cindex (c*lb+b) (c*ub+b) f
else - cindex (c*ub+b) (c*lb+b) f)"
proof (cases "c>0")
case False
then have "c<0" using ‹c≠0› by auto
have "cindex lb ub (f o (λx. c*x+b)) = - cindex (c*ub+b) (c*lb+b) f"
unfolding cindex_def
apply (subst sum_negf[symmetric])
apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
subgoal using False
apply (subst jump_linear_comp[OF ‹c≠0›])
by (auto simp add:‹c<0› ‹c≠0› field_simps)
subgoal for x
apply (subst jump_linear_comp[OF ‹c≠0›])
by (auto simp add:‹c<0› ‹c≠0› False field_simps)
done
then show ?thesis using False by auto
next
case True
have "cindex lb ub (f o (λx. c*x+b)) = cindex (c*lb+b) (c*ub+b) f"
unfolding cindex_def
apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
subgoal
apply (subst jump_linear_comp[OF ‹c≠0›])
by (auto simp add: True ‹c≠0› field_simps)
subgoal for x
apply (subst jump_linear_comp[OF ‹c≠0›])
by (auto simp add: ‹c≠0› True field_simps)
done
then show ?thesis using True by auto
qed

lemma cindexE_linear_comp:
assumes "c≠0"
shows "cindexE lb ub (f o (λx. c*x+b)) = (if c>0
then cindexE (c*lb+b) (c*ub+b) f
else - cindexE (c*ub+b) (c*lb+b) f)"
proof -
define cright where "cright = (λlb ub f. (∑x | jumpF f (at_right x) ≠ 0 ∧ lb ≤ x ∧ x < ub.
jumpF f (at_right x)))"
define cleft where "cleft = (λlb ub f. (∑x | jumpF f (at_left x) ≠ 0 ∧ lb < x ∧ x ≤ ub.
jumpF f (at_left x)))"
have cindexE_unfold:"cindexE lb ub f = cright lb ub f - cleft lb ub f"
for lb ub f unfolding cindexE_def cright_def cleft_def by auto
have ?thesis when "c<0"
proof -
have "cright lb ub (f ∘ (λx. c * x + b)) = cleft (c * ub + b) (c * lb + b) f"
unfolding cright_def cleft_def
apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
subgoal using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add:field_simps)
subgoal for x using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add: field_simps)
done
moreover have "cleft lb ub (f ∘ (λx. c * x + b)) = cright (c*ub+b) (c*lb + b) f"
unfolding cright_def cleft_def
apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
subgoal using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add:field_simps)
subgoal for x using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add: field_simps)
done
ultimately show ?thesis unfolding cindexE_unfold using that by auto
qed
moreover have ?thesis when "c>0"
proof -
have "cright lb ub (f ∘ (λx. c * x + b)) = cright (c * lb + b) (c * ub + b) f"
unfolding cright_def cleft_def
apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
subgoal using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add:field_simps)
subgoal for x using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add: field_simps)
done
moreover have "cleft lb ub (f ∘ (λx. c * x + b)) = cleft (c*lb+b) (c*ub + b) f"
unfolding cright_def cleft_def
apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
subgoal using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add:field_simps)
subgoal for x using that
by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add: field_simps)
done
ultimately show ?thesis unfolding cindexE_unfold using that by auto
qed
ultimately show ?thesis using ‹c≠0› by auto
qed

lemma cindexE_cong:
assumes "finite s" and fg_eq:"⋀x. ⟦a<x;x<b;x∉s⟧ ⟹ f x = g x"
shows "cindexE a b f = cindexE a b g"
proof -
define left where
"left=(λf. (∑x | jumpF f (at_left x) ≠ 0 ∧ a < x ∧ x ≤ b. jumpF f (at_left x)))"
define right where
"right=(λf. (∑x | jumpF f (at_right x) ≠ 0 ∧ a ≤ x ∧ x < b. jumpF f (at_right x)))"
have "left f = left g"
proof -
have "jumpF f (at_left x) = jumpF g (at_left x)" when "a<x" "x≤b" for x
proof (rule jumpF_cong)
define cs where "cs ≡ {y∈s. a<y ∧ y<x}"
define c where "c≡ (if cs = {} then (x+a)/2 else Max cs)"
have "finite cs" unfolding cs_def using assms(1) by auto
have "c<x ∧ (∀y. c<y ∧ y<x ⟶ f y=g y)"
proof (cases "cs={}")
case True
then have "∀y. c<y ∧ y<x ⟶ y ∉ s" unfolding cs_def c_def by force
moreover have "c=(x+a)/2" using True unfolding c_def by auto
ultimately show ?thesis using fg_eq using that by auto
next
case False
then have "c∈cs" unfolding c_def using False ‹finite cs› by auto
moreover have "∀y. c<y ∧ y<x ⟶ y ∉ s"
proof (rule ccontr)
assume "¬ (∀y. c < y ∧ y < x ⟶ y ∉ s) "
then obtain y' where "c<y'" "y'<x" "y'∈s" by auto
then have "y'∈cs" using ‹c∈cs› unfolding cs_def by auto
then have "y'≤c" unfolding c_def using False ‹finite cs› by auto
then show False using ‹c<y'› by auto
qed
ultimately show ?thesis unfolding cs_def using that by (auto intro!:fg_eq)
qed
then show "∀⇩F x in at_left x. f x = g x"
unfolding eventually_at_left by auto
qed simp
then show ?thesis
unfolding left_def
by (auto intro: sum.cong)
qed
moreover have "right f = right g"
proof -
have "jumpF f (at_right x) = jumpF g (at_right x)" when "a≤x" "x<b" for x
proof (rule jumpF_cong)
define cs where "cs ≡ {y∈s. x<y ∧ y<b}"
define c where "c≡ (if cs = {} then (x+b)/2 else Min cs)"
have "finite cs" unfolding cs_def using assms(1) by auto
have "x<c ∧ (∀y. x<y ∧ y<c ⟶ f y=g y)"
proof (cases "cs={}")
case True
then have "∀y. x<y ∧ y<c ⟶ y ∉ s" unfolding cs_def c_def by force
moreover have "c=(x+b)/2" using True unfolding c_def by auto
ultimately show ?thesis using fg_eq using that by auto
next
case False
then have "c∈cs" unfolding c_def using False ‹finite cs› by auto
moreover have "∀y. x<y ∧ y<c ⟶ y ∉ s"
proof (rule ccontr)
assume "¬ (∀y. x < y ∧ y < c ⟶ y ∉ s) "
then obtain y' where "x<y'" "y'<c" "y'∈s" by auto
then have "y'∈cs" using ‹c∈cs› unfolding cs_def by auto
then have "y'≥c" unfolding c_def using False ‹finite cs› by auto
then show False using ‹c>y'› by auto
qed
ultimately show ?thesis unfolding cs_def using that by (auto intro!:fg_eq)
qed
then show "∀⇩F x in at_right x. f x = g x"
unfolding eventually_at_right by auto
qed simp
then show ?thesis
unfolding right_def
by (auto intro: sum.cong)
qed
ultimately show ?thesis unfolding cindexE_def left_def right_def by presburger
qed

lemma cindexE_constI:
assumes "⋀t. ⟦a<t;t<b⟧ ⟹ f t=c"
shows "cindexE a b f = 0"
proof -
define left where
"left=(λf. (∑x | jumpF f (at_left x) ≠ 0 ∧ a < x ∧ x ≤ b. jumpF f (at_left x)))"
define right where
"right=(λf. (∑x | jumpF f (at_right x) ≠ 0 ∧ a ≤ x ∧ x < b. jumpF f (at_right x)))"
have "left f = 0"
proof -
have "jumpF f (at_left x) = 0" when "a<x" "x≤b" for x
apply (rule jumpF_eventually_const[of _ c])
unfolding eventually_at_left using assms that by auto
then show ?thesis unfolding left_def by auto
qed
moreover have "right f = 0"
proof -
have "jumpF f (at_right x) = 0" when "a≤x" "x<b" for x
apply (rule jumpF_eventually_const[of _ c])
unfolding eventually_at_right using assms that by auto
then show ?thesis unfolding right_def by auto
qed
ultimately show ?thesis unfolding cindexE_def left_def right_def by auto
qed

lemma cindex_eq_cindexE_divide:
fixes f g::"real ⇒ real"
defines "h ≡ (λx. f x/g x)"
assumes "a<b" and
finite_fg: "finite {x. (f x=0∨g x=0) ∧ a≤x∧x≤b}" and
g_imp_f:"∀x∈{a..b}. g x=0 ⟶ f x≠0" and
f_cont:"continuous_on {a..b} f" and
g_cont:"continuous_on {a..b} g"
shows "cindexE a b h = jumpF h (at_right a) + cindex a ```