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 ?μ] by (simp add: algebra_simps) 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" by (auto simp add: separation_t2) 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 ‹ Global_Theory.add_thms_dynamic (@{binding sgnx_eq_intros}, 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" by (simp add: has_sgnx_def) 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)› by (simp add: has_sgnx_imp_sgnx sgn_if) 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)› by (simp add: has_sgnx_imp_sgnx sgn_if) 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) by (simp add: sgn_mult sgn_divide) 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) by (simp add: sgn_mult) 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 by (simp add: assms has_sgnx_imp_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) by (auto simp add:sgn_zero_iff) 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) by (auto simp add:sgn_zero_iff) 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 by (auto simp add: linordered_field_no_lb) 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 by (auto simp add: linordered_field_no_ub) 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)" by (simp add: sgnx_able_sgnx) 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 by (simp add:eventually_conj_iff) 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 by (metis (no_types, hide_lams) add.commute add_uminus_conv_diff assms(2) diff_add_cancel 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 by (metis (no_types, hide_lams) add.commute add_uminus_conv_diff assms(2) diff_add_cancel 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 by (metis add.commute assms(2) diff_add_cancel diff_less_eq less_add_same_cancel1 sgn_pos) 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 by (metis (no_types, hide_lams) add.commute add.right_inverse add_uminus_conv_diff assms(2) diff_add_cancel diff_less_eq sgn_neg) 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 max_add_distrib_right) 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]) by (auto simp add:comp_def) 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]) by (auto simp add:comp_def) 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]) by (auto simp add:P_def) 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}› apply (auto simp add:field_simps) 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 by (auto simp add:field_simps) 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}› apply (auto simp add:field_simps) 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 by (auto simp add:field_simps) 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 by (auto simp add:divide_simps) 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› apply (simp_all add:divide_simps) by (auto simp add:algebra_simps ) 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 by (auto simp add: linepath_in_path) 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 * by (simp add: bounded_Int bounded_closed_segment) 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] by (auto simp add:algebra_simps) 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] by (auto simp add:algebra_simps) 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 by (auto simp add:inner_complex_def ) 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 by (auto simp add:scaleR_conv_of_real) 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)" by (auto simp add: filterlim_at_split) 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" by (simp add:sgnx_times) 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" by (simp add: zero_less_mult_iff) then have "?c1=?c2" using sgnx_values[OF sgnx_able_poly(1), of a,simplified] by (metis add.inverse_neutral less_minus_iff less_not_sym) 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 by (simp add: Lim_ident_at) 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 by (simp add: Lim_ident_at) 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" by (simp_all add: continuous_at_split jumpF_not_infinity) 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"]) by (auto simp add:joinpaths_def) 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"]) by (auto simp add:joinpaths_def) 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) by (auto simp add:sum.union_disjoint) 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 by (simp add: inj_on_def) 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 by (simp add: inj_on_def) 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 by (simp add: inj_on_def) 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 by (simp add: inj_on_def) 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 by (simp add: inj_on_def) 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 by (simp add: inj_on_def) 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