# Theory Missing_Topology

(* Author: Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> *) section ‹Some useful lemmas in topology› theory Missing_Topology imports "HOL-Analysis.Multivariate_Analysis" begin subsection ‹Misc› lemma open_times_image: fixes S::"'a::real_normed_field set" assumes "open S" "c≠0" shows "open (((*) c) ` S)" proof - let ?f = "λx. x/c" and ?g="((*) c)" have "continuous_on UNIV ?f" using ‹c≠0› by (auto intro:continuous_intros) then have "open (?f -` S)" using ‹open S› by (auto elim:open_vimage) moreover have "?g ` S = ?f -` S" using ‹c≠0› apply auto using image_iff by fastforce ultimately show ?thesis by auto qed lemma image_linear_greaterThan: fixes x::"'a::linordered_field" assumes "c≠0" shows "((λx. c*x+b) ` {x<..}) = (if c>0 then {c*x+b <..} else {..< c*x+b})" using ‹c≠0› apply (auto simp add:image_iff field_simps) subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps) subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps) done lemma image_linear_lessThan: fixes x::"'a::linordered_field" assumes "c≠0" shows "((λx. c*x+b) ` {..<x}) = (if c>0 then {..<c*x+b} else {c*x+b<..})" using ‹c≠0› apply (auto simp add:image_iff field_simps) subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps) subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps) done lemma continuous_on_neq_split: fixes f :: "'a::linear_continuum_topology ⇒ 'b::linorder_topology" assumes "∀x∈s. f x≠y" "continuous_on s f" "connected s" shows "(∀x∈s. f x>y) ∨ (∀x∈s. f x<y)" proof - { fix aa :: 'a and aaa :: 'a have "y ∉ f ` s" using assms(1) by blast then have "(aa ∉ s ∨ y < f aa) ∨ aaa ∉ s ∨ f aaa < y" by (meson Topological_Spaces.connected_continuous_image assms(2) assms(3) connectedD_interval image_eqI linorder_not_le) } then show ?thesis by blast qed lemma fixes f::"'a::linorder_topology ⇒ 'b::topological_space" assumes "continuous_on {a..b} f" "a<b" shows continuous_on_at_left:"continuous (at_left b) f" and continuous_on_at_right:"continuous (at_right a) f" proof - have "at b within {..a} = bot" proof - have "closed {..a}" by auto then have "closure ({..a} - {b}) = {..a}" by (simp add: assms(2) not_le) then have "b∉closure ({..a} - {b})" using ‹a<b› by auto then show ?thesis using at_within_eq_bot_iff by auto qed then have "(f ⤏ f b) (at b within {..a})" by auto moreover have "(f ⤏ f b) (at b within {a..b})" using assms unfolding continuous_on by auto moreover have "{..a} ∪ {a..b} = {..b}" using ‹a<b› by auto ultimately have "(f ⤏ f b) (at b within {..b})" using Lim_Un[of f "f b" b "{..a}" "{a..b}"] by presburger then have "(f ⤏ f b) (at b within {..<b})" apply (elim tendsto_within_subset) by auto then show "continuous (at_left b) f" using continuous_within by auto next have "at a within {b..} = bot" proof - have "closed {b..}" by auto then have "closure ({b..} - {a}) = {b..}" by (simp add: assms(2) not_le) then have "a∉closure ({b..} - {a})" using ‹a<b› by auto then show ?thesis using at_within_eq_bot_iff by auto qed then have "(f ⤏ f a) (at a within {b..})" by auto moreover have "(f ⤏ f a) (at a within {a..b})" using assms unfolding continuous_on by auto moreover have "{b..} ∪ {a..b} = {a..}" using ‹a<b› by auto ultimately have "(f ⤏ f a) (at a within {a..})" using Lim_Un[of f "f a" a "{b..}" "{a..b}"] by presburger then have "(f ⤏ f a) (at a within {a<..})" apply (elim tendsto_within_subset) by auto then show "continuous (at_right a) f" using continuous_within by auto qed subsection ‹More about @{term eventually}› lemma eventually_comp_filtermap: "eventually (P o f) F ⟷ eventually P (filtermap f F)" unfolding comp_def using eventually_filtermap by auto lemma eventually_uminus_at_top_at_bot: fixes P::"'a::{ordered_ab_group_add,linorder} ⇒ bool" shows "eventually (P o uminus) at_bot ⟷ eventually P at_top" "eventually (P o uminus) at_top ⟷ eventually P at_bot" unfolding eventually_comp_filtermap by (fold at_top_mirror at_bot_mirror,auto) lemma eventually_at_infinityI: fixes P::"'a::real_normed_vector ⇒ bool" assumes "⋀x. c ≤ norm x ⟹ P x" shows "eventually P at_infinity" unfolding eventually_at_infinity using assms by auto lemma eventually_at_bot_linorderI: fixes c::"'a::linorder" assumes "⋀x. x ≤ c ⟹ P x" shows "eventually P at_bot" using assms by (auto simp: eventually_at_bot_linorder) lemma eventually_times_inverse_1: fixes f::"'a ⇒ 'b::{field,t2_space}" assumes "(f ⤏ c) F" "c≠0" shows "∀⇩_{F}x in F. inverse (f x) * f x = 1" proof - have "∀⇩_{F}x in F. f x≠0" using assms tendsto_imp_eventually_ne by blast then show ?thesis apply (elim eventually_mono) by auto qed subsection ‹More about @{term filtermap}› lemma filtermap_linear_at_within: assumes "bij f" and cont: "isCont f a" and open_map: "⋀S. open S ⟹ open (f`S)" shows "filtermap f (at a within S) = at (f a) within f`S" unfolding filter_eq_iff proof safe fix P assume "eventually P (filtermap f (at a within S))" then obtain T where "open T" "a ∈ T" and impP:"∀x∈T. x≠a ⟶ x∈S⟶ P (f x)" by (auto simp: eventually_filtermap eventually_at_topological) then show "eventually P (at (f a) within f ` S)" unfolding eventually_at_topological apply (intro exI[of _ "f`T"]) using ‹bij f› open_map by (metis bij_pointE imageE imageI) next fix P assume "eventually P (at (f a) within f ` S)" then obtain T1 where "open T1" "f a ∈ T1" and impP:"∀x∈T1. x≠f a ⟶ x∈f`S⟶ P (x)" unfolding eventually_at_topological by auto then obtain T2 where "open T2" "a ∈ T2" "(∀x'∈T2. f x' ∈ T1)" using cont[unfolded continuous_at_open,rule_format,of T1] by blast then have "∀x∈T2. x≠a ⟶ x∈S⟶ P (f x)" using impP by (metis assms(1) bij_pointE imageI) then show "eventually P (filtermap f (at a within S))" unfolding eventually_filtermap eventually_at_topological apply (intro exI[of _ T2]) using ‹open T2› ‹a ∈ T2› by auto qed lemma filtermap_at_bot_linear_eq: fixes c::"'a::linordered_field" assumes "c≠0" shows "filtermap (λx. x * c + b) at_bot = (if c>0 then at_bot else at_top)" proof (cases "c>0") case True then have "filtermap (λx. x * c + b) at_bot = at_bot" apply (intro filtermap_fun_inverse[of "λx. (x-b) / c"]) subgoal unfolding eventually_at_bot_linorder filterlim_at_bot by (auto simp add: field_simps) subgoal unfolding eventually_at_bot_linorder filterlim_at_bot by (metis mult.commute real_affinity_le) by auto then show ?thesis using ‹c>0› by auto next case False then have "c<0" using ‹c≠0› by auto then have "filtermap (λx. x * c + b) at_bot = at_top" apply (intro filtermap_fun_inverse[of "λx. (x-b) / c"]) subgoal unfolding eventually_at_top_linorder filterlim_at_bot by (meson le_diff_eq neg_divide_le_eq) subgoal unfolding eventually_at_bot_linorder filterlim_at_top using ‹c < 0› by (meson False diff_le_eq le_divide_eq) by auto then show ?thesis using ‹c<0› by auto qed lemma filtermap_linear_at_left: fixes c::"'a::{linordered_field,linorder_topology,real_normed_field}" assumes "c≠0" shows "filtermap (λx. c*x+b) (at_left x) = (if c>0 then at_left (c*x+b) else at_right (c*x+b))" proof - let ?f = "λx. c*x+b" have "filtermap (λx. c*x+b) (at_left x) = (at (?f x) within ?f ` {..<x})" proof (subst filtermap_linear_at_within) show "bij ?f" using ‹c≠0› by (auto intro!: o_bij[of "λx. (x-b)/c"]) show "isCont ?f x" by auto show "⋀S. open S ⟹ open (?f ` S)" using open_times_image[OF _ ‹c≠0›,THEN open_translation,of _ b] by (simp add:image_image add.commute) show "at (?f x) within ?f ` {..<x} = at (?f x) within ?f ` {..<x}" by simp qed moreover have "?f ` {..<x} = {..<?f x}" when "c>0" using image_linear_lessThan[OF ‹c≠0›,of b x] that by auto moreover have "?f ` {..<x} = {?f x<..}" when "¬ c>0" using image_linear_lessThan[OF ‹c≠0›,of b x] that by auto ultimately show ?thesis by auto qed lemma filtermap_linear_at_right: fixes c::"'a::{linordered_field,linorder_topology,real_normed_field}" assumes "c≠0" shows "filtermap (λx. c*x+b) (at_right x) = (if c>0 then at_right (c*x+b) else at_left (c*x+b))" proof - let ?f = "λx. c*x+b" have "filtermap ?f (at_right x) = (at (?f x) within ?f ` {x<..})" proof (subst filtermap_linear_at_within) show "bij ?f" using ‹c≠0› by (auto intro!: o_bij[of "λx. (x-b)/c"]) show "isCont ?f x" by auto show "⋀S. open S ⟹ open (?f ` S)" using open_times_image[OF _ ‹c≠0›,THEN open_translation,of _ b] by (simp add:image_image add.commute) show "at (?f x) within ?f ` {x<..} = at (?f x) within ?f ` {x<..}" by simp qed moreover have "?f ` {x<..} = {?f x<..}" when "c>0" using image_linear_greaterThan[OF ‹c≠0›,of b x] that by auto moreover have "?f ` {x<..} = {..<?f x}" when "¬ c>0" using image_linear_greaterThan[OF ‹c≠0›,of b x] that by auto ultimately show ?thesis by auto qed lemma filtermap_at_top_linear_eq: fixes c::"'a::linordered_field" assumes "c≠0" shows "filtermap (λx. x * c + b) at_top = (if c>0 then at_top else at_bot)" proof (cases "c>0") case True then have "filtermap (λx. x * c + b) at_top = at_top" apply (intro filtermap_fun_inverse[of "λx. (x-b) / c"]) subgoal unfolding eventually_at_top_linorder filterlim_at_top by (meson le_diff_eq pos_le_divide_eq) subgoal unfolding eventually_at_top_linorder filterlim_at_top apply auto by (metis mult.commute real_le_affinity) by auto then show ?thesis using ‹c>0› by auto next case False then have "c<0" using ‹c≠0› by auto then have "filtermap (λx. x * c + b) at_top = at_bot" apply (intro filtermap_fun_inverse[of "λx. (x-b) / c"]) subgoal unfolding eventually_at_bot_linorder filterlim_at_top by (auto simp add: field_simps) subgoal unfolding eventually_at_top_linorder filterlim_at_bot by (meson le_diff_eq neg_divide_le_eq) by auto then show ?thesis using ‹c<0› by auto qed lemma filtermap_nhds_open_map: assumes cont: "isCont f a" and open_map: "⋀S. open S ⟹ open (f`S)" shows "filtermap f (nhds a) = nhds (f a)" unfolding filter_eq_iff proof safe fix P assume "eventually P (filtermap f (nhds a))" then obtain S where "open S" "a ∈ S" "∀x∈S. P (f x)" by (auto simp: eventually_filtermap eventually_nhds) then show "eventually P (nhds (f a))" unfolding eventually_nhds apply (intro exI[of _ "f`S"]) by (auto intro!: open_map) qed (metis filterlim_iff tendsto_at_iff_tendsto_nhds isCont_def eventually_filtermap cont) subsection ‹More about @{term filterlim}› lemma filterlim_at_infinity_times: fixes f :: "'a ⇒ 'b::real_normed_field" assumes "filterlim f at_infinity F" "filterlim g at_infinity F" shows "filterlim (λx. f x * g x) at_infinity F" proof - have "((λx. inverse (f x) * inverse (g x)) ⤏ 0 * 0) F" by (intro tendsto_mult tendsto_inverse assms filterlim_compose[OF tendsto_inverse_0]) then have "filterlim (λx. inverse (f x) * inverse (g x)) (at 0) F" unfolding filterlim_at using assms by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj) then show ?thesis by (subst filterlim_inverse_at_iff[symmetric]) simp_all qed lemma filterlim_at_top_at_bot[elim]: fixes f::"'a ⇒ 'b::unbounded_dense_linorder" and F::"'a filter" assumes top:"filterlim f at_top F" and bot: "filterlim f at_bot F" and "F≠bot" shows False proof - obtain c::'b where True by auto have "∀⇩_{F}x in F. c < f x" using top unfolding filterlim_at_top_dense by auto moreover have "∀⇩_{F}x in F. f x < c" using bot unfolding filterlim_at_bot_dense by auto ultimately have "∀⇩_{F}x in F. c < f x ∧ f x < c" using eventually_conj by auto then have "∀⇩_{F}x in F. False" by (auto elim:eventually_mono) then show False using ‹F≠bot› by auto qed lemma filterlim_at_top_nhds[elim]: fixes f::"'a ⇒ 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter" assumes top:"filterlim f at_top F" and tendsto: "(f ⤏ c) F" and "F≠bot" shows False proof - obtain c'::'b where "c'>c" using gt_ex by blast have "∀⇩_{F}x in F. c' < f x" using top unfolding filterlim_at_top_dense by auto moreover have "∀⇩_{F}x in F. f x < c'" using order_tendstoD[OF tendsto,of c'] ‹c'>c› by auto ultimately have "∀⇩_{F}x in F. c' < f x ∧ f x < c'" using eventually_conj by auto then have "∀⇩_{F}x in F. False" by (auto elim:eventually_mono) then show False using ‹F≠bot› by auto qed lemma filterlim_at_bot_nhds[elim]: fixes f::"'a ⇒ 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter" assumes top:"filterlim f at_bot F" and tendsto: "(f ⤏ c) F" and "F≠bot" shows False proof - obtain c'::'b where "c'<c" using lt_ex by blast have "∀⇩_{F}x in F. c' > f x" using top unfolding filterlim_at_bot_dense by auto moreover have "∀⇩_{F}x in F. f x > c'" using order_tendstoD[OF tendsto,of c'] ‹c'<c› by auto ultimately have "∀⇩_{F}x in F. c' < f x ∧ f x < c'" using eventually_conj by auto then have "∀⇩_{F}x in F. False" by (auto elim:eventually_mono) then show False using ‹F≠bot› by auto qed lemma filterlim_at_top_linear_iff: fixes f::"'a::linordered_field ⇒ 'b" assumes "c≠0" shows "(LIM x at_top. f (x * c + b) :> F2) ⟷ (if c>0 then (LIM x at_top. f x :> F2) else (LIM x at_bot. f x :> F2))" unfolding filterlim_def apply (subst filtermap_filtermap[of f "λx. x * c + b",symmetric]) using assms by (auto simp add:filtermap_at_top_linear_eq) lemma filterlim_at_bot_linear_iff: fixes f::"'a::linordered_field ⇒ 'b" assumes "c≠0" shows "(LIM x at_bot. f (x * c + b) :> F2) ⟷ (if c>0 then (LIM x at_bot. f x :> F2) else (LIM x at_top. f x :> F2)) " unfolding filterlim_def apply (subst filtermap_filtermap[of f "λx. x * c + b",symmetric]) using assms by (auto simp add:filtermap_at_bot_linear_eq) lemma filterlim_tendsto_add_at_top_iff: assumes f: "(f ⤏ c) F" shows "(LIM x F. (f x + g x :: real) :> at_top) ⟷ (LIM x F. g x :> at_top)" proof assume "LIM x F. f x + g x :> at_top" moreover have "((λx. - f x) ⤏ - c) F" using f by (intro tendsto_intros,simp) ultimately show "filterlim g at_top F" using filterlim_tendsto_add_at_top by fastforce qed (auto simp add:filterlim_tendsto_add_at_top[OF f]) lemma filterlim_tendsto_add_at_bot_iff: fixes c::real assumes f: "(f ⤏ c) F" shows "(LIM x F. f x + g x :> at_bot) ⟷ (LIM x F. g x :> at_bot)" proof - have "(LIM x F. f x + g x :> at_bot) ⟷ (LIM x F. - f x + (- g x) :> at_top)" apply (subst filterlim_uminus_at_top) by (rule filterlim_cong,auto) also have "... = (LIM x F. - g x :> at_top)" apply (subst filterlim_tendsto_add_at_top_iff[of _ "-c"]) by (auto intro:tendsto_intros simp add:f) also have "... = (LIM x F. g x :> at_bot)" apply (subst filterlim_uminus_at_top) by (rule filterlim_cong,auto) finally show ?thesis . qed lemma tendsto_inverse_0_at_infinity: "LIM x F. f x :> at_infinity ⟹ ((λx. inverse (f x) :: real) ⤏ 0) F" by (metis filterlim_at filterlim_inverse_at_iff) lemma filterlim_at_infinity_divide_iff: fixes f::"'a ⇒ 'b::real_normed_field" assumes "(f ⤏ c) F" "c≠0" shows "(LIM x F. f x / g x :> at_infinity) ⟷ (LIM x F. g x :> at 0)" proof assume asm:"LIM x F. f x / g x :> at_infinity" have "LIM x F. inverse (f x) * (f x / g x) :> at_infinity" apply (rule tendsto_mult_filterlim_at_infinity[of _ "inverse c", OF _ _ asm]) by (auto simp add: assms(1) assms(2) tendsto_inverse) then have "LIM x F. inverse (g x) :> at_infinity" apply (elim filterlim_mono_eventually) using eventually_times_inverse_1[OF assms] by (auto elim:eventually_mono simp add:field_simps) then show "filterlim g (at 0) F" using filterlim_inverse_at_iff[symmetric] by force next assume "filterlim g (at 0) F" then have "filterlim (λx. inverse (g x)) at_infinity F" using filterlim_compose filterlim_inverse_at_infinity by blast then have "LIM x F. f x * inverse (g x) :> at_infinity" using tendsto_mult_filterlim_at_infinity[OF assms, of "λx. inverse(g x)"] by simp then show "LIM x F. f x / g x :> at_infinity" by (simp add: divide_inverse) qed lemma filterlim_tendsto_pos_mult_at_top_iff: fixes f::"'a ⇒ real" assumes "(f ⤏ c) F" and "0 < c" shows "(LIM x F. (f x * g x) :> at_top) ⟷ (LIM x F. g x :> at_top)" proof assume "filterlim g at_top F" then show "LIM x F. f x * g x :> at_top" using filterlim_tendsto_pos_mult_at_top[OF assms] by auto next assume asm:"LIM x F. f x * g x :> at_top" have "((λx. inverse (f x)) ⤏ inverse c) F" using tendsto_inverse[OF assms(1)] ‹0<c› by auto moreover have "inverse c >0" using assms(2) by auto ultimately have "LIM x F. inverse (f x) * (f x * g x) :> at_top" using filterlim_tendsto_pos_mult_at_top[OF _ _ asm,of "λx. inverse (f x)" "inverse c"] by auto then show "LIM x F. g x :> at_top" apply (elim filterlim_mono_eventually) apply simp_all[2] using eventually_times_inverse_1[OF assms(1)] ‹c>0› eventually_mono by fastforce qed lemma filterlim_tendsto_pos_mult_at_bot_iff: fixes c :: real assumes "(f ⤏ c) F" "0 < c" shows "(LIM x F. f x * g x :> at_bot) ⟷ filterlim g at_bot F" using filterlim_tendsto_pos_mult_at_top_iff[OF assms(1,2), of "λx. - g x"] unfolding filterlim_uminus_at_bot by simp lemma filterlim_tendsto_neg_mult_at_top_iff: fixes f::"'a ⇒ real" assumes "(f ⤏ c) F" and "c < 0" shows "(LIM x F. (f x * g x) :> at_top) ⟷ (LIM x F. g x :> at_bot)" proof - have "(LIM x F. f x * g x :> at_top) = (LIM x F. - g x :> at_top)" apply (rule filterlim_tendsto_pos_mult_at_top_iff[of "λx. - f x" "-c" F "λx. - g x", simplified]) using assms by (auto intro: tendsto_intros ) also have "... = (LIM x F. g x :> at_bot)" using filterlim_uminus_at_bot[symmetric] by auto finally show ?thesis . qed lemma filterlim_tendsto_neg_mult_at_bot_iff: fixes c :: real assumes "(f ⤏ c) F" "0 > c" shows "(LIM x F. f x * g x :> at_bot) ⟷ filterlim g at_top F" using filterlim_tendsto_neg_mult_at_top_iff[OF assms(1,2), of "λx. - g x"] unfolding filterlim_uminus_at_top by simp lemma Lim_add: fixes f g::"_ ⇒ 'a::{t2_space,topological_monoid_add}" assumes "∃y. (f ⤏ y) F" and "∃y. (g ⤏ y) F" and "F≠bot" shows "Lim F f + Lim F g = Lim F (λx. f x+g x)" apply (rule tendsto_Lim[OF ‹F≠bot›, symmetric]) apply (auto intro!:tendsto_eq_intros) using assms tendsto_Lim by blast+ (* lemma filterlim_at_top_tendsto[elim]: fixes f::"'a ⇒ 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter" assumes top:"filterlim f at_top F" and tendsto: "(f ⤏ c) F" and "F≠bot" shows False proof - obtain cc where "cc>c" using gt_ex by blast have "∀⇩_{F}x in F. cc < f x" using top unfolding filterlim_at_top_dense by auto moreover have "∀⇩_{F}x in F. f x < cc" using tendsto order_tendstoD(2)[OF _ ‹cc>c›] by auto ultimately have "∀⇩_{F}x in F. cc < f x ∧ f x < cc" using eventually_conj by auto then have "∀⇩_{F}x in F. False" by (auto elim:eventually_mono) then show False using ‹F≠bot› by auto qed lemma filterlim_at_bot_tendsto[elim]: fixes f::"'a ⇒ 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter" assumes top:"filterlim f at_bot F" and tendsto: "(f ⤏ c) F" and "F≠bot" shows False proof - obtain cc where "cc<c" using lt_ex by blast have "∀⇩_{F}x in F. cc > f x" using top unfolding filterlim_at_bot_dense by auto moreover have "∀⇩_{F}x in F. f x > cc" using tendsto order_tendstoD(1)[OF _ ‹cc<c›] by auto ultimately have "∀⇩_{F}x in F. cc < f x ∧ f x < cc" using eventually_conj by auto then have "∀⇩_{F}x in F. False" by (auto elim:eventually_mono) then show False using ‹F≠bot› by auto qed *) subsection ‹Isolate and discrete› definition (in topological_space) isolate:: "'a ⇒ 'a set ⇒ bool" (infixr "isolate" 60) where "x isolate S ⟷ (x∈S ∧ (∃T. open T ∧ T ∩ S = {x}))" definition (in topological_space) discrete:: "'a set ⇒ bool" where "discrete S ⟷ (∀x∈S. x isolate S)" definition (in metric_space) uniform_discrete :: "'a set ⇒ bool" where "uniform_discrete S ⟷ (∃e>0. ∀x∈S. ∀y∈S. dist x y < e ⟶ x = y)" lemma uniformI1: assumes "e>0" "⋀x y. ⟦x∈S;y∈S;dist x y<e⟧ ⟹ x =y " shows "uniform_discrete S" unfolding uniform_discrete_def using assms by auto lemma uniformI2: assumes "e>0" "⋀x y. ⟦x∈S;y∈S;x≠y⟧ ⟹ dist x y≥e " shows "uniform_discrete S" unfolding uniform_discrete_def using assms not_less by blast lemma isolate_islimpt_iff:"(x isolate S) ⟷ (¬ (x islimpt S) ∧ x∈S)" unfolding isolate_def islimpt_def by auto lemma isolate_dist_Ex_iff: fixes x::"'a::metric_space" shows "x isolate S ⟷ (x∈S ∧ (∃e>0. ∀y∈S. dist x y < e ⟶ y=x))" unfolding isolate_islimpt_iff islimpt_approachable by (metis dist_commute) lemma discrete_empty[simp]: "discrete {}" unfolding discrete_def by auto lemma uniform_discrete_empty[simp]: "uniform_discrete {}" unfolding uniform_discrete_def by (simp add: gt_ex) lemma isolate_insert: fixes x :: "'a::t1_space" shows "x isolate (insert a S) ⟷ x isolate S ∨ (x=a ∧ ¬ (x islimpt S))" by (meson insert_iff islimpt_insert isolate_islimpt_iff) (* TODO. Other than uniform_discrete S ⟶ discrete S uniform_discrete S ⟶ closed S , we should be able to prove discrete S ∧ closed S ⟶ uniform_discrete S but the proof (based on Tietze Extension Theorem) seems not very trivial to me. Informal proofs can be found in http://topology.auburn.edu/tp/reprints/v30/tp30120.pdf http://msp.org/pjm/1959/9-2/pjm-v9-n2-p19-s.pdf *) lemma uniform_discrete_imp_closed: "uniform_discrete S ⟹ closed S" by (meson discrete_imp_closed uniform_discrete_def) lemma uniform_discrete_imp_discrete: "uniform_discrete S ⟹ discrete S" by (metis discrete_def isolate_dist_Ex_iff uniform_discrete_def) lemma isolate_subset:"x isolate S ⟹ T ⊆ S ⟹ x∈T ⟹ x isolate T" unfolding isolate_def by fastforce lemma discrete_subset[elim]: "discrete S ⟹ T ⊆ S ⟹ discrete T" unfolding discrete_def using islimpt_subset isolate_islimpt_iff by blast lemma uniform_discrete_subset[elim]: "uniform_discrete S ⟹ T ⊆ S ⟹ uniform_discrete T" by (meson subsetD uniform_discrete_def) lemma continuous_on_discrete: "discrete S ⟹ continuous_on S f" unfolding continuous_on_topological by (metis discrete_def islimptI isolate_islimpt_iff) (* Is euclidean_space really necessary?*) lemma uniform_discrete_insert: fixes S :: "'a::euclidean_space set" shows "uniform_discrete (insert a S) ⟷ uniform_discrete S" proof assume asm:"uniform_discrete S" let ?thesis = "uniform_discrete (insert a S)" have ?thesis when "a∈S" using that asm by (simp add: insert_absorb) moreover have ?thesis when "S={}" using that asm by (simp add: uniform_discrete_def) moreover have ?thesis when "a∉S" "S≠{}" proof - obtain e1 where "e1>0" and e1_dist:"∀x∈S. ∀y∈S. dist y x < e1 ⟶ y = x" using asm unfolding uniform_discrete_def by auto define e2 where "e2 ≡ min (setdist {a} S) e1" have "closed S" using asm uniform_discrete_imp_closed by auto then have "e2>0" by (simp add: ‹0 < e1› e2_def setdist_gt_0_compact_closed that(1) that(2)) moreover have "x = y" when "x∈insert a S" "y∈insert a S" "dist x y < e2 " for x y proof - have ?thesis when "x=a" "y=a" using that by auto moreover have ?thesis when "x=a" "y∈S" using that setdist_le_dist[of x "{a}" y S] ‹dist x y < e2› unfolding e2_def by fastforce moreover have ?thesis when "y=a" "x∈S" using that setdist_le_dist[of y "{a}" x S] ‹dist x y < e2› unfolding e2_def by (simp add: dist_commute) moreover have ?thesis when "x∈S" "y∈S" using e1_dist[rule_format, OF that] ‹dist x y < e2› unfolding e2_def by (simp add: dist_commute) ultimately show ?thesis using that by auto qed ultimately show ?thesis unfolding uniform_discrete_def by meson qed ultimately show ?thesis by auto qed (simp add: subset_insertI uniform_discrete_subset) lemma discrete_compact_finite_iff: fixes S :: "'a::t1_space set" shows "discrete S ∧ compact S ⟷ finite S" proof assume "finite S" then have "compact S" using finite_imp_compact by auto moreover have "discrete S" unfolding discrete_def using isolate_islimpt_iff islimpt_finite[OF ‹finite S›] by auto ultimately show "discrete S ∧ compact S" by auto next assume "discrete S ∧ compact S" then show "finite S" by (meson discrete_def Heine_Borel_imp_Bolzano_Weierstrass isolate_islimpt_iff order_refl) qed lemma uniform_discrete_finite_iff: fixes S :: "'a::heine_borel set" shows "uniform_discrete S ∧ bounded S ⟷ finite S" proof assume "uniform_discrete S ∧ bounded S" then have "discrete S" "compact S" using uniform_discrete_imp_discrete uniform_discrete_imp_closed compact_eq_bounded_closed by auto then show "finite S" using discrete_compact_finite_iff by auto next assume asm:"finite S" let ?thesis = "uniform_discrete S ∧ bounded S" have ?thesis when "S={}" using that by auto moreover have ?thesis when "S≠{}" proof - have "∀x. ∃d>0. ∀y∈S. y ≠ x ⟶ d ≤ dist x y" using finite_set_avoid[OF ‹finite S›] by auto then obtain f where f_pos:"f x>0" and f_dist: "∀y∈S. y ≠ x ⟶ f x ≤ dist x y" if "x∈S" for x by metis define f_min where "f_min ≡ Min (f ` S)" have "f_min > 0" unfolding f_min_def by (simp add: asm f_pos that) moreover have "∀x∈S. ∀y∈S. f_min > dist x y ⟶ x=y" using f_dist unfolding f_min_def by (metis Min_gr_iff all_not_in_conv asm dual_order.irrefl eq_iff finite_imageI imageI less_eq_real_def) ultimately have "uniform_discrete S" unfolding uniform_discrete_def by auto moreover have "bounded S" using ‹finite S› by auto ultimately show ?thesis by auto qed ultimately show ?thesis by blast qed lemma uniform_discrete_image_scale: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "uniform_discrete S" and dist:"∀x∈S. ∀y∈S. dist x y = c * dist (f x) (f y)" shows "uniform_discrete (f ` S)" proof - have ?thesis when "S={}" using that by auto moreover have ?thesis when "S≠{}" "c≤0" proof - obtain x1 where "x1∈S" using ‹S≠{}› by auto have ?thesis when "S-{x1} = {}" proof - have "S={x1}" using that ‹S≠{}› by auto then show ?thesis using uniform_discrete_insert[of "f x1"] by auto qed moreover have ?thesis when "S-{x1} ≠ {}" proof - obtain x2 where "x2∈S-{x1}" using ‹S-{x1} ≠ {}› by auto then have "x2∈S" "x1≠x2" by auto then have "dist x1 x2 > 0" by auto moreover have "dist x1 x2 = c * dist (f x1) (f x2)" using dist[rule_format, OF ‹x1∈S› ‹x2∈S›] . moreover have "dist (f x2) (f x2) ≥ 0" by auto ultimately have False using ‹c≤0› by (simp add: zero_less_mult_iff) then show ?thesis by auto qed ultimately show ?thesis by auto qed moreover have ?thesis when "S≠{}" "c>0" proof - obtain e1 where "e1>0" and e1_dist:"∀x∈S. ∀y∈S. dist y x < e1 ⟶ y = x" using ‹uniform_discrete S› unfolding uniform_discrete_def by auto define e where "e= e1/c" have "x1 = x2" when "x1∈ f ` S" "x2∈ f ` S" "dist x1 x2 < e " for x1 x2 proof - obtain y1 where y1:"y1∈S" "x1=f y1" using ‹x1∈ f ` S› by auto obtain y2 where y2:"y2∈S" "x2=f y2" using ‹x2∈ f ` S› by auto have "dist y1 y2 < e1" using dist[rule_format, OF y1(1) y2(1)] ‹c>0› ‹dist x1 x2 < e› unfolding e_def apply (fold y1(2) y2(2)) by (auto simp add:divide_simps mult.commute) then have "y1=y2" using e1_dist[rule_format, OF y2(1) y1(1)] by simp then show "x1=x2" using y1(2) y2(2) by auto qed moreover have "e>0" using ‹e1>0› ‹c>0› unfolding e_def by auto ultimately show ?thesis unfolding uniform_discrete_def by meson qed ultimately show ?thesis by fastforce qed end

# Theory Missing_Algebraic

(* Author: Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> *) section ‹Some useful lemmas in algebra› theory Missing_Algebraic imports "HOL-Computational_Algebra.Polynomial_Factorial" "HOL-Computational_Algebra.Fundamental_Theorem_Algebra" "HOL-Complex_Analysis.Complex_Analysis" Missing_Topology "Budan_Fourier.BF_Misc" begin subsection ‹Misc› lemma poly_holomorphic_on[simp]: "(poly p) holomorphic_on s" apply (rule holomorphic_onI) apply (unfold field_differentiable_def) apply (rule_tac x="poly (pderiv p) x" in exI) by (simp add:has_field_derivative_at_within) lemma order_zorder: fixes p::"complex poly" and z::complex assumes "p≠0" shows "order z p = nat (zorder (poly p) z)" proof - define n where "n=nat (zorder (poly p) z)" define h where "h=zor_poly (poly p) z" have "∃w. poly p w ≠ 0" using assms poly_all_0_iff_0 by auto then obtain r where "0 < r" "cball z r ⊆ UNIV" and h_holo: "h holomorphic_on cball z r" and poly_prod:"(∀w∈cball z r. poly p w = h w * (w - z) ^ n ∧ h w ≠ 0)" using zorder_exist_zero[of "poly p" UNIV z,folded h_def] poly_holomorphic_on unfolding n_def by auto then have "h holomorphic_on ball z r" and "(∀w∈ball z r. poly p w = h w * (w - z) ^ n)" and "h z≠0" by auto then have "order z p = n" using ‹p≠0› proof (induct n arbitrary:p h) case 0 then have "poly p z=h z" using ‹r>0› by auto then have "poly p z≠0" using ‹h z≠0› by auto then show ?case using order_root by blast next case (Suc n) define sn where "sn=Suc n" define h' where "h'≡ λw. deriv h w * (w-z)+ sn * h w" have "(poly p has_field_derivative poly (pderiv p) w) (at w)" for w using poly_DERIV[of p w] . moreover have "(poly p has_field_derivative (h' w)*(w-z)^n ) (at w)" when "w∈ball z r" for w proof (subst DERIV_cong_ev[of w w "poly p" "λw. h w * (w - z) ^ Suc n" ],simp_all) show "∀⇩_{F}x in nhds w. poly p x = h x * ((x - z) * (x - z) ^ n)" unfolding eventually_nhds using Suc(3) ‹w∈ball z r› apply (intro exI[where x="ball z r"]) by auto next have "(h has_field_derivative deriv h w) (at w)" using ‹h holomorphic_on ball z r› ‹w∈ball z r› holomorphic_on_imp_differentiable_at by (simp add: holomorphic_derivI) then have "((λw. h w * ((w - z) ^ sn)) has_field_derivative h' w * (w - z) ^ (sn - 1)) (at w)" unfolding h'_def apply (auto intro!: derivative_eq_intros simp add:field_simps) by (auto simp add:field_simps sn_def) then show "((λw. h w * ((w - z) * (w - z) ^ n)) has_field_derivative h' w * (w - z) ^ n) (at w)" unfolding sn_def by auto qed ultimately have "∀w∈ball z r. poly (pderiv p) w = h' w * (w - z) ^ n" using DERIV_unique by blast moreover have "h' holomorphic_on ball z r" unfolding h'_def using ‹h holomorphic_on ball z r› by (auto intro!: holomorphic_intros) moreover have "h' z≠0" unfolding h'_def sn_def using ‹h z ≠ 0› of_nat_neq_0 by auto moreover have "pderiv p ≠ 0" proof assume "pderiv p = 0" obtain c where "p=[:c:]" using ‹pderiv p = 0› using pderiv_iszero by blast then have "c=0" using Suc(3)[rule_format,of z] ‹r>0› by auto then show False using ‹p≠0› using ‹p=[:c:]› by auto qed ultimately have "order z (pderiv p) = n" by (auto elim: Suc.hyps) moreover have "order z p ≠ 0" using Suc(3)[rule_format,of z] ‹r>0› order_root ‹p≠0› by auto ultimately show ?case using order_pderiv[OF ‹pderiv p ≠ 0›] by auto qed then show ?thesis unfolding n_def . qed lemma pcompose_pCons_0:"pcompose p [:a:] = [:poly p a:]" apply (induct p) by (auto simp add:pcompose_pCons algebra_simps) lemma pcompose_coeff_0: "coeff (pcompose p q) 0 = poly p (coeff q 0)" apply (induct p) by (auto simp add:pcompose_pCons coeff_mult) lemma poly_field_differentiable_at[simp]: "poly p field_differentiable (at x within s)" apply (unfold field_differentiable_def) apply (rule_tac x="poly (pderiv p) x" in exI) by (simp add:has_field_derivative_at_within) lemma deriv_pderiv: "deriv (poly p) = poly (pderiv p)" apply (rule ext) apply (rule DERIV_imp_deriv) using poly_DERIV . lemma lead_coeff_map_poly_nz: assumes "f (lead_coeff p) ≠0" "f 0=0" shows "lead_coeff (map_poly f p) = f (lead_coeff p) " proof - have "lead_coeff (Poly (map f (coeffs p))) = f (lead_coeff p)" by (metis (mono_tags, lifting) antisym assms(1) assms(2) coeff_0_degree_minus_1 coeff_map_poly degree_Poly degree_eq_length_coeffs le_degree length_map map_poly_def) then show ?thesis by (simp add: map_poly_def) qed lemma filterlim_poly_at_infinity: fixes p::"'a::real_normed_field poly" assumes "degree p>0" shows "filterlim (poly p) at_infinity at_infinity" using assms proof (induct p) case 0 then show ?case by auto next case (pCons a p) have ?case when "degree p=0" proof - obtain c where c_def:"p=[:c:]" using ‹degree p = 0› degree_eq_zeroE by blast then have "c≠0" using ‹0 < degree (pCons a p)› by auto then show ?thesis unfolding c_def apply (auto intro!:tendsto_add_filterlim_at_infinity) apply (subst mult.commute) by (auto intro!:tendsto_mult_filterlim_at_infinity filterlim_ident) qed moreover have ?case when "degree p≠0" proof - have "filterlim (poly p) at_infinity at_infinity" using that by (auto intro:pCons) then show ?thesis by (auto intro!:tendsto_add_filterlim_at_infinity filterlim_at_infinity_times filterlim_ident) qed ultimately show ?case by auto qed lemma poly_divide_tendsto_aux: fixes p::"'a::real_normed_field poly" shows "((λx. poly p x/x^(degree p)) ⤏ lead_coeff p) at_infinity" proof (induct p) case 0 then show ?case by (auto intro:tendsto_eq_intros) next case (pCons a p) have ?case when "p=0" using that by auto moreover have ?case when "p≠0" proof - define g where "g=(λx. a/(x*x^degree p))" define f where "f=(λx. poly p x/x^degree p)" have "∀⇩_{F}x in at_infinity. poly (pCons a p) x / x ^ degree (pCons a p) = g x + f x" proof (rule eventually_at_infinityI[of 1]) fix x::'a assume "norm x≥1" then have "x≠0" by auto then show "poly (pCons a p) x / x ^ degree (pCons a p) = g x + f x" using that unfolding g_def f_def by (auto simp add:field_simps) qed moreover have "((λx. g x+f x) ⤏ lead_coeff (pCons a p)) at_infinity" proof - have "(g ⤏ 0) at_infinity" unfolding g_def using filterlim_poly_at_infinity[of "monom 1 (Suc (degree p))"] apply (auto intro!:tendsto_intros tendsto_divide_0 simp add: degree_monom_eq) apply (subst filterlim_cong[where g="poly (monom 1 (Suc (degree p)))"]) by (auto simp add:poly_monom) moreover have "(f ⤏ lead_coeff (pCons a p)) at_infinity" using pCons ‹p≠0› unfolding f_def by auto ultimately show ?thesis by (auto intro:tendsto_eq_intros) qed ultimately show ?thesis by (auto dest:tendsto_cong) qed ultimately show ?case by auto qed lemma filterlim_power_at_infinity: assumes "n≠0" shows "filterlim (λx::'a::real_normed_field. x^n) at_infinity at_infinity" using filterlim_poly_at_infinity[of "monom 1 n"] assms apply (subst filterlim_cong[where g="poly (monom 1 n)"]) by (auto simp add:poly_monom degree_monom_eq) lemma poly_divide_tendsto_0_at_infinity: fixes p::"'a::real_normed_field poly" assumes "degree p > degree q" shows "((λx. poly q x / poly p x) ⤏ 0 ) at_infinity" proof - define pp where "pp=(λx. x^(degree p) / poly p x)" define qq where "qq=(λx. poly q x/x^(degree q))" define dd where "dd=(λx::'a. 1/x^(degree p - degree q))" have "∀⇩_{F}x in at_infinity. poly q x / poly p x = qq x * pp x * dd x" proof (rule eventually_at_infinityI[of 1]) fix x::'a assume "norm x≥1" then have "x≠0" by auto then show "poly q x / poly p x = qq x * pp x * dd x" unfolding qq_def pp_def dd_def using assms by (auto simp add:field_simps divide_simps power_diff) qed moreover have "((λx. qq x * pp x * dd x) ⤏ 0) at_infinity" proof - have "(qq ⤏ lead_coeff q) at_infinity" unfolding qq_def using poly_divide_tendsto_aux[of q] . moreover have "(pp ⤏ 1/lead_coeff p) at_infinity" proof - have "p≠0" using assms by auto then show ?thesis unfolding pp_def using poly_divide_tendsto_aux[of p] apply (drule_tac tendsto_inverse) by (auto simp add:inverse_eq_divide) qed moreover have "(dd ⤏ 0) at_infinity" unfolding dd_def apply (rule tendsto_divide_0) by (auto intro!: filterlim_power_at_infinity simp add:assms) ultimately show ?thesis by (auto intro:tendsto_eq_intros) qed ultimately show ?thesis by (auto dest:tendsto_cong) qed lemma lead_coeff_list_def: "lead_coeff p= (if coeffs p=[] then 0 else last (coeffs p))" by (simp add: last_coeffs_eq_coeff_degree) lemma poly_linepath_comp: fixes a::"'a::{real_normed_vector,comm_semiring_0,real_algebra_1}" shows "poly p o (linepath a b) = poly (p ∘⇩_{p}[:a, b-a:]) o of_real" apply rule by (auto simp add:poly_pcompose linepath_def scaleR_conv_of_real algebra_simps) lemma poly_eventually_not_zero: fixes p::"real poly" assumes "p≠0" shows "eventually (λx. poly p x≠0) at_infinity" proof (rule eventually_at_infinityI[of "Max (norm ` {x. poly p x=0}) + 1"]) fix x::real assume asm:"Max (norm ` {x. poly p x=0}) + 1 ≤ norm x" have False when "poly p x=0" proof - define S where "S=norm `{x. poly p x = 0}" have "norm x∈S" using that unfolding S_def by auto moreover have "finite S" using ‹p≠0› poly_roots_finite unfolding S_def by blast ultimately have "norm x≤Max S" by simp moreover have "Max S + 1 ≤ norm x" using asm unfolding S_def by simp ultimately show False by argo qed then show "poly p x ≠ 0" by auto qed subsection ‹More about @{term degree}› lemma degree_div_less: fixes x y::"'a::field poly" assumes "degree x≠0" "degree y≠0" shows "degree (x div y) < degree x" proof - have "x≠0" "y≠0" using assms by auto define q r where "q=x div y" and "r=x mod y" have *:"eucl_rel_poly x y (q, r)" unfolding q_def r_def by (simp add: eucl_rel_poly) then have "r = 0 ∨ degree r < degree y" using ‹y≠0› unfolding eucl_rel_poly_iff by auto moreover have ?thesis when "r=0" proof - have "x = q * y" using * that unfolding eucl_rel_poly_iff by auto then have "q≠0" using ‹x≠0› ‹y≠0› by auto from degree_mult_eq[OF this ‹y≠0›] ‹x = q * y› have "degree x = degree q +degree y" by auto then show ?thesis unfolding q_def using assms by auto qed moreover have ?thesis when "degree r<degree y" proof (cases "degree y>degree x") case True then have "q=0" unfolding q_def using div_poly_less by auto then show ?thesis unfolding q_def using assms(1) by auto next case False then have "degree x>degree r" using that by auto then have "degree x = degree (x-r)" using degree_add_eq_right[of "-r" x] by auto have "x-r = q*y" using * unfolding eucl_rel_poly_iff by auto then have "q≠0" using ‹degree r < degree x› by auto have "degree x = degree q +degree y" using degree_mult_eq[OF ‹q≠0› ‹y≠0›] ‹x-r = q*y› ‹degree x = degree (x-r)› by auto then show ?thesis unfolding q_def using assms by auto qed ultimately show ?thesis by auto qed lemma map_poly_degree_eq: assumes "f (lead_coeff p) ≠0" shows "degree (map_poly f p) = degree p" using assms unfolding map_poly_def degree_eq_length_coeffs coeffs_Poly lead_coeff_list_def by (metis (full_types) last_conv_nth_default length_map no_trailing_unfold nth_default_coeffs_eq nth_default_map_eq strip_while_idem) lemma map_poly_degree_less: assumes "f (lead_coeff p) =0" "degree p≠0" shows "degree (map_poly f p) < degree p" proof - have "length (coeffs p) >1" using ‹degree p≠0› by (simp add: degree_eq_length_coeffs) then obtain xs x where xs_def:"coeffs p=xs@[x]" "length xs>0" by (metis One_nat_def add.commute add_diff_cancel_left' append_Nil assms(2) degree_eq_length_coeffs length_greater_0_conv list.size(3) list.size(4) not_less_zero rev_exhaust) have "f x=0" using assms(1) by (simp add: lead_coeff_list_def xs_def(1)) have "degree (map_poly f p) = length (strip_while ((=) 0) (map f (xs@[x]))) - 1" unfolding map_poly_def degree_eq_length_coeffs coeffs_Poly by (subst xs_def,auto) also have "... = length (strip_while ((=) 0) (map f xs)) - 1" using ‹f x=0› by simp also have "... ≤ length xs -1" using length_strip_while_le by (metis diff_le_mono length_map) also have "... < length (xs@[x]) - 1" using xs_def(2) by auto also have "... = degree p" unfolding degree_eq_length_coeffs xs_def by simp finally show ?thesis . qed lemma map_poly_degree_leq[simp]: shows "degree (map_poly f p) ≤ degree p" unfolding map_poly_def degree_eq_length_coeffs by (metis coeffs_Poly diff_le_mono length_map length_strip_while_le) subsection ‹roots / zeros of a univariate function› definition roots_within::"('a ⇒ 'b::zero) ⇒ 'a set ⇒ 'a set" where "roots_within f s = {x∈s. f x = 0}" abbreviation roots::"('a ⇒ 'b::zero) ⇒ 'a set" where "roots f ≡ roots_within f UNIV" subsection ‹The argument principle specialised to polynomials.› lemma argument_principle_poly: assumes "p≠0" and valid:"valid_path g" and loop: "pathfinish g = pathstart g" and no_proots:"path_image g ⊆ - proots p" shows "contour_integral g (λx. deriv (poly p) x / poly p x) = 2 * of_real pi * 𝗂 * (∑x∈proots p. winding_number g x * of_nat (order x p))" proof - have "contour_integral g (λx. deriv (poly p) x / poly p x) = 2 * of_real pi * 𝗂 * (∑x | poly p x = 0. winding_number g x * of_int (zorder (poly p) x))" apply (rule argument_principle[of UNIV "poly p" "{}" "λ_. 1" g,simplified,OF _ valid loop]) using no_proots[unfolded proots_def] by (auto simp add:poly_roots_finite[OF ‹p≠0›] ) also have "... = 2 * of_real pi * 𝗂 * (∑x∈proots p. winding_number g x * of_nat (order x p))" proof - have "nat (zorder (poly p) x) = order x p" when "x∈proots p" for x using order_zorder[OF ‹p≠0›] that unfolding proots_def by auto then show ?thesis unfolding proots_def apply (auto intro!:comm_monoid_add_class.sum.cong) by (metis assms(1) nat_eq_iff2 of_nat_nat order_root) qed finally show ?thesis . qed end

# Theory Missing_Transcendental

(* Author: Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> *) section ‹Some useful lemmas about transcendental functions› theory Missing_Transcendental imports Missing_Topology Missing_Algebraic begin subsection ‹Misc› lemma Im_Ln_eq_pi_half: "z ≠ 0 ⟹ (Im(Ln z) = pi/2 ⟷ 0 < Im(z) ∧ Re(z) = 0)" "z ≠ 0 ⟹ (Im(Ln z) = -pi/2 ⟷ Im(z) < 0 ∧ Re(z) = 0)" proof - show "z ≠ 0 ⟹ (Im(Ln z) = pi/2 ⟷ 0 < Im(z) ∧ Re(z) = 0)" by (metis Im_Ln_eq_pi Im_Ln_le_pi Im_Ln_pos_lt Re_Ln_pos_le Re_Ln_pos_lt abs_of_nonneg less_eq_real_def order_less_irrefl pi_half_gt_zero) next assume "z≠0" have "Im (Ln z) = - pi / 2 ⟹ Im z < 0 ∧ Re z = 0" by (metis Im_Ln_pos_le Re_Ln_pos_le Re_Ln_pos_lt_imp ‹z ≠ 0› abs_if add.inverse_inverse divide_minus_left less_eq_real_def linorder_not_le minus_pi_half_less_zero) moreover have "Im (Ln z) = - pi / 2" when "Im z < 0" "Re z = 0" proof - obtain r::real where "r>0" "z=r * (-𝗂)" by (metis ‹Im z < 0› ‹Re z = 0› add.commute add.inverse_inverse add.right_neutral complex_eq complex_i_mult_minus diff_0 mult.commute mult.left_commute neg_0_less_iff_less of_real_0 of_real_diff) then have "Im (Ln z) = Im (Ln (r*(-𝗂)))" by auto also have "... = Im (Ln (complex_of_real r) + Ln (- 𝗂)) " apply (subst Ln_times_of_real) using ‹r>0› by auto also have "... = - pi/2" using ‹r>0› by simp finally show "Im (Ln z) = - pi / 2" . qed ultimately show "(Im(Ln z) = -pi/2 ⟷ Im(z) < 0 ∧ Re(z) = 0)" by auto qed lemma Im_Ln_eq: assumes "z≠0" shows "Im (Ln z) = (if Re z≠0 then if Re z>0 then arctan (Im z/Re z) else if Im z≥0 then arctan (Im z/Re z) + pi else arctan (Im z/Re z) - pi else if Im z>0 then pi/2 else -pi/2)" proof - have eq_arctan_pos:"Im (Ln z) = arctan (Im z/Re z)" when "Re z>0" for z proof - define wR where "wR=Re (Ln z)" define θ where "θ = arctan (Im z/Re z)" have "z≠0" using that by auto have "exp (Complex wR θ) = z" proof (rule complex_eqI) have "Im (exp (Complex wR θ)) =exp wR * sin θ " unfolding Im_exp by simp also have "... = Im z" unfolding wR_def Re_Ln[OF ‹z≠0›] θ_def using ‹z≠0› ‹Re z>0› by (auto simp add:sin_arctan divide_simps complex_neq_0 cmod_def real_sqrt_divide) finally show "Im (exp (Complex wR θ)) = Im z" . next have "Re (exp (Complex wR θ)) = exp wR * cos θ " unfolding Re_exp by simp also have "... = Re z" unfolding wR_def Re_Ln[OF ‹z≠0›] θ_def using ‹z≠0› ‹Re z>0› by (auto simp add:cos_arctan divide_simps complex_neq_0 cmod_def real_sqrt_divide) finally show "Re (exp (Complex wR θ)) = Re z" . qed moreover have "-pi<θ" "θ≤pi" using arctan_lbound [of ‹Im z / Re z›] arctan_ubound [of ‹Im z / Re z›] by (simp_all add: θ_def) ultimately have "Ln z = Complex wR θ" using Ln_unique by auto then show ?thesis using that unfolding θ_def by auto qed have ?thesis when "Re z=0" using Im_Ln_eq_pi_half[OF ‹z≠0›] that apply auto using assms complex.expand by auto moreover have ?thesis when "Re z>0" using eq_arctan_pos[OF that] that by auto moreover have ?thesis when "Re z<0" "Im z≥0" proof - have "Im (Ln (- z)) = arctan (Im (- z) / Re (- z))" apply (rule eq_arctan_pos) using that by auto moreover have "Ln (- z) = Ln z - 𝗂 * complex_of_real pi" apply (subst Ln_minus[OF ‹z≠0›]) using that by auto ultimately show ?thesis using that by auto qed moreover have ?thesis when "Re z<0" "Im z<0" proof - have "Im (Ln (- z)) = arctan (Im (- z) / Re (- z))" apply (rule eq_arctan_pos) using that by auto moreover have "Ln (- z) = Ln z + 𝗂 * complex_of_real pi" apply (subst Ln_minus[OF ‹z≠0›]) using that by auto ultimately show ?thesis using that by auto qed ultimately show ?thesis by linarith qed lemma exp_Arg2pi2pi_multivalue: assumes "exp (𝗂* of_real x) = z" shows "∃k::int. x = Arg2pi z + 2*k*pi" proof - define k where "k=floor( x/(2*pi))" define x' where "x'= x - (2*k*pi)" have "x'/(2*pi) ≥0" unfolding x'_def k_def by (simp add: diff_divide_distrib) moreover have "x'/(2*pi) < 1" proof - have "x/(2*pi) - k < 1" unfolding k_def by linarith thus ?thesis unfolding k_def x'_def by (auto simp add:field_simps) qed ultimately have "x'≥0" and "x'<2*pi" by (auto simp add:field_simps) moreover have "exp (𝗂 * complex_of_real x') = z" using assms x'_def by (auto simp add:field_simps ) ultimately have "Arg2pi z = x'" using Arg2pi_unique[of 1 x' z,simplified] by auto hence " x = Arg2pi z + 2*k*pi" unfolding x'_def by auto thus ?thesis by auto qed lemma cos_eq_neg_periodic_intro: assumes "x - y=2*(of_int k)*pi + pi ∨ x + y = 2*(of_int k)*pi + pi" shows "cos x = - cos y" using assms proof assume "x - y = 2 * (of_int k) * pi + pi" then have "cos x = cos ((y+ pi) + (of_int k)*(2*pi))" by (auto simp add:algebra_simps) also have "... = cos (y+pi)" using cos.periodic_simps[of "y+pi"] by (auto simp add:algebra_simps) also have "... = - cos y" by simp finally show "cos x = - cos y" by auto next assume "x + y = 2 * real_of_int k * pi + pi " then have "cos x = cos ((- y+ pi) + (of_int k)*(2*pi))" apply (intro arg_cong[where f=cos]) by (auto simp add:algebra_simps) also have "... = cos (- y +pi)" using cos.periodic_simps[of "-y+pi"] by (auto simp add:algebra_simps) also have "... = - cos y" by simp finally show "cos x = - cos y" by auto qed lemma cos_eq_periodic_intro: assumes "x - y=2*(of_int k)*pi ∨ x + y = 2*(of_int k)*pi" shows "cos x = cos y" using assms proof assume "x - y = 2 * (of_int k) * pi " then have "cos x = cos (y + (of_int k)*(2*pi))" by (auto simp add:algebra_simps) also have "... = cos y" using cos.periodic_simps[of "y"] by (auto simp add:algebra_simps) finally show "cos x = cos y" by auto next assume "x + y = 2 * of_int k * pi" then have "cos x = cos (- y + (of_int k)*(2*pi))" apply (intro arg_cong[where f=cos]) by (auto simp add:algebra_simps) also have "... = cos (- y)" using cos.periodic_simps[of "-y"] by (auto simp add:algebra_simps) also have "... = cos y" by simp finally show "cos x = cos y" by auto qed lemma sin_tan_half: "sin (2*x) = 2 * tan x / (1 + (tan x)^2)" unfolding sin_double tan_def apply (cases "cos x=0") by (auto simp add:field_simps power2_eq_square) lemma cos_tan_half: "cos x ≠0 ⟹ cos (2*x) = (1 - (tan x)^2) / (1+ (tan x)^2)" unfolding cos_double tan_def by (auto simp add:field_simps ) lemma tan_eq_arctan_Ex: shows "tan x = y ⟷ (∃k::int. x = arctan y + k*pi ∨ (x = pi/2 + k*pi ∧ y=0))" proof assume asm:"tan x = y" obtain k::int where k:"-pi/2 < x-k*pi" "x-k*pi ≤ pi/2" proof - define k where "k=ceiling (x/pi - 1/2)" have "(x/pi - 1/2)≤k" unfolding k_def by auto then have "x-k*pi ≤ pi/2" by (auto simp add:field_simps) moreover have "k-1 < x/pi - 1/2" unfolding k_def by linarith then have "-pi/2 < x-k*pi" by (auto simp add:field_simps) ultimately show ?thesis using that by auto qed have "x = arctan y + of_int k * pi" when "x ≠ pi/2 + k*pi" proof - have "tan (x - k * pi) = y" using asm tan_periodic_int[of _ "-k"] by auto then have "arctan y = x - real_of_int k * pi" apply (intro arctan_unique) using k that by (auto simp add:field_simps) then show ?thesis by auto qed moreover have "y=0" when "x = pi/2 + k*pi" using asm that by auto (simp add: tan_def) ultimately show "∃k. x = arctan y + of_int k * pi ∨ (x = pi/2 + k*pi ∧ y=0)" using k by auto next assume "∃k::int. x = arctan y + k * pi ∨ x = pi / 2 + k * pi ∧ y = 0" then show "tan x = y" by (metis arctan_unique cos_pi_half division_ring_divide_zero tan_def tan_periodic_int tan_total) qed lemma arccos_unique: assumes "0 ≤ x" and "x ≤ pi" and "cos x = y" shows "arccos y = x" using arccos_cos assms(1) assms(2) assms(3) by blast lemma cos_eq_arccos_Ex: "cos x = y ⟷ -1≤y ∧ y≤1 ∧ (∃k::int. x = arccos y + 2*k*pi ∨ x = - arccos y + 2*k*pi)" proof assume asm:"-1≤y ∧ y≤1 ∧ (∃k::int. x = arccos y + 2*k*pi ∨ x = - arccos y + 2*k*pi)" then obtain k::int where "x = arccos y + 2*k*pi ∨ x = - arccos y + 2*k*pi" by auto moreover have "cos x = y" when "x = arccos y + 2*k*pi" proof - have "cos x = cos (arccos y + k*(2*pi))" using that by (auto simp add:algebra_simps) also have "... = cos (arccos y)" using cos.periodic_simps(3)[of "arccos y" k] by auto also have "... = y" using asm by auto finally show ?thesis . qed moreover have "cos x = y" when "x = -arccos y + 2*k*pi" proof - have "cos x = cos (- arccos y + k*2*pi)" unfolding that by (auto simp add:algebra_simps) also have "... = cos (arccos y - k*2*pi)" by (metis cos_minus minus_diff_eq uminus_add_conv_diff) also have "... = cos (arccos y)" using cos.periodic_simps(3)[of "arccos y" "-k"] by (auto simp add:algebra_simps) also have "... = y" using asm by auto finally show ?thesis . qed ultimately show "cos x = y" by auto next assume asm:"cos x =y" let ?goal = "(∃k::int. x = arccos y + 2*k*pi ∨ x = - arccos y + 2*k*pi)" obtain k::int where k:"-pi < x-k*2*pi" "x-k*2*pi ≤ pi" proof - define k where "k=ceiling (x/(2*pi) - 1/2)" have "(x/(2*pi) - 1/2)≤k" unfolding k_def by auto then have "x-k*2*pi ≤ pi" by (auto simp add:field_simps) moreover have "k-1 < x/(2*pi) - 1/2" unfolding k_def by linarith then have "-pi < x-k*2*pi" by (auto simp add:field_simps) ultimately show ?thesis using that by auto qed have ?goal when "x-k*2*pi≥0" proof - have "cos (x - k * 2*pi) = y" using cos.periodic_simps(3)[of x "-k"] asm by (auto simp add:field_simps) then have "arccos y = x - k * 2*pi" apply (intro arccos_unique) using k that by auto then show ?goal by auto qed moreover have ?goal when "¬ x-k*2*pi ≥0" proof - have "cos (x - k * 2*pi) = y" using cos.periodic_simps(3)[of x "-k"] asm by (auto simp add:field_simps) then have "cos (k * 2*pi - x) = y" by (metis cos_minus minus_diff_eq) then have "arccos y = k * 2*pi - x" apply (intro arccos_unique) using k that by auto then show ?goal by auto qed ultimately have ?goal by auto moreover have "-1≤y ∧ y≤1" using asm by auto ultimately show "-1≤y ∧ y≤1 ∧ ?goal" by auto qed lemma uniform_discrete_tan_eq: "uniform_discrete {x::real. tan x = y}" proof - have "x1=x2" when dist:"dist x1 x2<pi/2" and "tan x1=y" "tan x2=y" for x1 x2 proof - obtain k1::int where x1:"x1 = arctan y + k1*pi ∨ (x1 = pi/2 + k1*pi ∧ y=0)" using tan_eq_arctan_Ex ‹tan x1=y› by auto obtain k2::int where x2:"x2 = arctan y + k2*pi ∨ (x2 = pi/2 + k2*pi ∧ y=0)" using tan_eq_arctan_Ex ‹tan x2=y› by auto let ?xk1="x1 = arctan y + k1*pi" and ?xk1'="x1 = pi/2 + k1*pi ∧ y=0" let ?xk2="x2 = arctan y + k2*pi" and ?xk2'="x2 = pi/2 + k2*pi ∧ y=0" have ?thesis when "(?xk1 ∧ ?xk2) ∨ (?xk1' ∧ ?xk2')" proof - have "x1-x2= (k1 - k2) *pi" when ?xk1 ?xk2 using arg_cong2[where f=minus,OF ‹?xk1› ‹?xk2›] by (auto simp add:algebra_simps) moreover have "x1-x2= (k1 - k2) *pi" when ?xk1' ?xk2' using arg_cong2[where f=minus,OF conjunct1[OF ‹?xk1'›] conjunct1[OF ‹?xk2'›]] by (auto simp add:algebra_simps) ultimately have "x1-x2= (k1 - k2) *pi" using that by auto then have "¦k1 - k2¦ < 1/2" using dist[unfolded dist_real_def] by (auto simp add:abs_mult) then have "k1=k2" by linarith then show ?thesis using that by auto qed moreover have ?thesis when ?xk1 ?xk2' proof - have "x1 = k1*pi" "x2 = pi / 2 + k2 * pi" using ‹?xk2'› ‹?xk1› by auto from arg_cong2[where f=minus,OF this] have "x1 - x2 = (k1 - k2) * pi -pi/2" by (auto simp add:algebra_simps) then have "¦(k1 - k2) * pi -pi/2¦ < pi/2" using dist[unfolded dist_real_def] by auto then have "0<k1-k2" "k1-k2<1" unfolding abs_less_iff by (auto simp add: zero_less_mult_iff) then have False by simp then show ?thesis by auto qed moreover have ?thesis when ?xk1' ?xk2 proof - have "x1 = pi / 2 + k1*pi" "x2 = k2 * pi" using ‹?xk2› ‹?xk1'› by auto from arg_cong2[where f=minus,OF this] have "x1 - x2 = (k1 - k2) * pi + pi/2" by (auto simp add:algebra_simps) then have "¦(k1 - k2) * pi + pi/2¦ < pi/2" using dist[unfolded dist_real_def] by auto then have "¦(k1 - k2 + 1/2)*pi¦ < pi/2" by (auto simp add:algebra_simps) then have "¦(k1 - k2 + 1/2)¦ < 1/2" by (auto simp add:abs_mult) then have "-1<k1-k2 ∧ k1-k2<0" unfolding abs_less_iff by linarith then have False by auto then show ?thesis by auto qed ultimately show ?thesis using x1 x2 by blast qed then show ?thesis unfolding uniform_discrete_def apply (intro exI[where x="pi/2"]) by auto qed lemma get_norm_value: fixes a::"'a::{floor_ceiling}" assumes "pp>0" obtains k::int and a1 where "a=(of_int k)*pp+a1" "a0≤a1" "a1<a0+pp" proof - define k where "k=floor ((a-a0)/pp)" define a1 where "a1=a-(of_int k)*pp" have "of_int ⌊(a - a0) / pp⌋ * pp ≤ a- a0" using assms by (meson le_divide_eq of_int_floor_le) moreover have "a-a0 < of_int (⌊(a - a0) / pp⌋+1) * pp" using assms by (meson divide_less_eq floor_correct) ultimately show ?thesis apply (intro that[of k a1]) unfolding k_def a1_def using assms by (auto simp add:algebra_simps) qed (*Is it possible to generalise or simplify this messy proof?*) lemma filtermap_tan_at_right: fixes a::real assumes "cos a≠0" shows "filtermap tan (at_right a) = at_right (tan a)" proof - obtain k::int and a1 where aa1:"a=k*pi+a1" and "-pi/2≤a1" "a1<pi/2" using get_norm_value[of pi a "-pi/2"] by auto have "-pi/2 < a1" proof (rule ccontr) assume "¬ - pi / 2 < a1" then have "a1=- pi / 2" using ‹-pi/2≤a1› by auto then have "cos a = 0" unfolding aa1 by (metis (no_types, hide_lams) add.commute add_0_left cos_pi_half diff_eq_eq mult.left_neutral mult_minus_right mult_zero_left sin_add sin_pi_half sin_zero_iff_int2 times_divide_eq_left uminus_add_conv_diff) then show False using assms by auto qed have "eventually P (at_right (tan a))" when "eventually P (filtermap tan (at_right a))" for P proof - obtain b1 where "b1>a" and b1_imp:" ∀y>a. y < b1 ⟶ P (tan y)" using ‹eventually P (filtermap tan (at_right a))› unfolding eventually_filtermap eventually_at_right by (metis eventually_at_right_field) define b2 where "b2=min b1 (k*pi+pi/4+a1/2)" define b3 where "b3=b2 - k*pi" have "-pi/2 < b3" "b3<pi/2" proof - have "a1<b3" using ‹b1>a› aa1 ‹a1<pi/2› unfolding b2_def b3_def by (auto simp add:field_simps) then show "-pi/2 < b3" using ‹-pi/2≤a1› by auto show "b3 < pi/2" unfolding b2_def b3_def apply (subst min_diff_distrib_left) apply (rule min.strict_coboundedI2) using ‹b1>a› aa1 ‹a1<pi/2› ‹-pi/2<a1› by auto qed have "tan b2 > tan a" proof - have "tan a = tan a1" using aa1 by (simp add: add.commute) also have "... < tan b3" proof - have "a1<b3" using ‹b1>a› aa1 ‹a1<pi/2› unfolding b2_def b3_def by (auto simp add:field_simps) then show ?thesis using tan_monotone ‹-pi/2 < a1› ‹b3 < pi/2› by simp qed also have "... = tan b2" unfolding b3_def by (metis Groups.mult_ac(2) add_uminus_conv_diff mult_minus_right of_int_minus tan_periodic_int) finally show ?thesis . qed moreover have "P y" when "y>tan a" "y < tan b2" for y proof - define y1 where "y1=arctan y+ k * pi" have "a<y1" proof - have "arctan (tan a) < arctan y" using ‹y>tan a› arctan_monotone by auto then have "a1<arctan y" using arctan_tan ‹-pi/2 < a1› ‹a1<pi/2› unfolding aa1 by (simp add: add.commute) then show ?thesis unfolding y1_def aa1 by auto qed moreover have "y1<b2" proof - have "arctan y < arctan (tan b2)" using ‹y < tan b2› arctan_monotone by auto moreover have "arctan (tan b2) = b3" using arctan_tan[of b3] ‹-pi/2 < b3› ‹b3<pi/2› unfolding b3_def by (metis add.inverse_inverse diff_minus_eq_add divide_minus_left mult.commute mult_minus_right of_int_minus tan_periodic_int) ultimately have "arctan y < b3" by auto then show ?thesis unfolding y1_def b3_def by auto qed moreover have "∀y>a. y < b2 ⟶ P (tan y)" using b1_imp unfolding b2_def by auto moreover have "tan y1=y" unfolding y1_def by (auto simp add:tan_arctan) ultimately show ?thesis by auto qed ultimately show "eventually P (at_right (tan a))" unfolding eventually_at_right by (metis eventually_at_right_field) qed moreover have "eventually P (filtermap tan (at_right a))" when "eventually P (at_right (tan a))" for P proof - obtain b1 where "b1>tan a" and b1_imp:"∀y>tan a. y < b1 ⟶ P y" using ‹eventually P (at_right (tan a))› unfolding eventually_at_right by (metis eventually_at_right_field) define b2 where "b2=arctan b1 + k*pi" have "a1 < arctan b1" by (metis ‹- pi / 2 < a1› ‹a1 < pi / 2› ‹tan a < b1› aa1 add.commute arctan_less_iff arctan_tan divide_minus_left tan_periodic_int) then have "b2>a" unfolding aa1 b2_def by auto moreover have "P (tan y)" when "y>a" "y < b2" for y proof - define y1 where "y1 = y - k*pi" have "a1 < y1" "y1 < arctan b1" unfolding y1_def subgoal using ‹y>a› unfolding aa1 by auto subgoal using b2_def that(2) by linarith done then have "tan a1 < tan y1" "tan y1< b1" subgoal using ‹a1>-pi/2› apply (intro tan_monotone,simp,simp) using arctan_ubound less_trans by blast subgoal by (metis ‹- pi / 2 < a1› ‹a1 < y1› ‹y1 < arctan b1› arctan_less_iff arctan_tan arctan_ubound divide_minus_left less_trans) done have "tan y>tan a" by (metis ‹tan a1 < tan y1› aa1 add.commute add_uminus_conv_diff mult.commute mult_minus_right of_int_minus tan_periodic_int y1_def) moreover have "tan y<b1" by (metis ‹tan y1 < b1› add_uminus_conv_diff mult.commute mult_minus_right of_int_minus tan_periodic_int y1_def) ultimately show ?thesis using b1_imp by auto qed ultimately show ?thesis unfolding eventually_filtermap eventually_at_right by (metis eventually_at_right_field) qed ultimately show ?thesis unfolding filter_eq_iff by blast qed lemma filtermap_tan_at_left: fixes a::real assumes "cos a≠0" shows "filtermap tan (at_left a) = at_left (tan a)" proof - have "filtermap tan (at_right (- a)) = at_right (tan (- a))" using filtermap_tan_at_right[of "-a"] assms by auto then have "filtermap (uminus o tan) (at_left a) = filtermap uminus (at_left (tan a))" unfolding at_right_minus filtermap_filtermap comp_def by auto then have "filtermap uminus (filtermap (uminus o tan) (at_left a)) = filtermap uminus (filtermap uminus (at_left (tan a)))" by auto then show ?thesis unfolding filtermap_filtermap comp_def by auto qed lemma cos_zero_iff_int2: fixes x::real shows "cos x = 0 ⟷ (∃n::int. x = n * pi + pi/2)" using sin_zero_iff_int2[of "x-pi/2"] unfolding sin_cos_eq by (auto simp add:algebra_simps) lemma filtermap_tan_at_right_inf: fixes a::real assumes "cos a=0" shows "filtermap tan (at_right a) = at_bot" proof - obtain k::int where ak:"a=k*pi + pi/2" using cos_zero_iff_int2 assms by auto have "eventually P at_bot" when "eventually P (filtermap tan (at_right a))" for P proof - obtain b1 where "b1>a" and b1_imp:"∀y>a. y < b1 ⟶ P (tan y)" using ‹eventually P (filtermap tan (at_right a))› unfolding eventually_filtermap eventually_at_right by (metis eventually_at_right_field) define b2 where "b2=min (k*pi+pi) b1" have "P y" when "y<tan b2" for y proof - define y1 where "y1=(k+1)*pi+arctan y" have "a < y1" unfolding ak y1_def using arctan_lbound[of y] by (auto simp add:field_simps) moreover have "y1 < b2" proof - define b3 where "b3=b2-(k+1) * pi" have "-pi/2 < b3" "b3<pi/2" using ‹b1>a› unfolding b3_def b2_def ak by (auto simp add:field_simps min_mult_distrib_left intro!:min.strict_coboundedI1) then have "arctan (tan b3) = b3" by (simp add: arctan_tan) then have "arctan (tan b2) = b3" unfolding b3_def by (metis diff_eq_eq tan_periodic_int) then have "arctan y < b3" using arctan_monotone[OF ‹y<tan b2›] by simp then show ?thesis unfolding y1_def b3_def by auto qed then have "y1<b1" unfolding b2_def by auto ultimately have " P (tan y1)" using b1_imp[rule_format,of y1,simplified] by auto then show ?thesis unfolding y1_def by (metis add.commute arctan tan_periodic_int) qed then show ?thesis unfolding eventually_at_bot_dense by auto qed moreover have "eventually P (filtermap tan (at_right a))" when "eventually P at_bot" for P proof - obtain b1 where b1_imp:"∀n<b1. P n" using ‹eventually P at_bot› unfolding eventually_at_bot_dense by auto define b2 where "b2=arctan b1 + (k+1)*pi" have "b2>a" unfolding ak b2_def using arctan_lbound[of b1] by (auto simp add:algebra_simps) moreover have "P (tan y)" when "a < y" " y < b2 " for y proof - define y1 where "y1=y-(k+1)*pi" have "tan y1 < tan (arctan b1)" apply (rule tan_monotone) subgoal using ‹a<y› unfolding y1_def ak by (auto simp add:algebra_simps) subgoal using ‹y < b2› unfolding y1_def b2_def by (auto simp add:algebra_simps) subgoal using arctan_ubound by auto done then have "tan y1<b1" by (simp add: arctan) then have "tan y < b1" unfolding y1_def by (metis diff_eq_eq tan_periodic_int) then show ?thesis using b1_imp by auto qed ultimately show "eventually P (filtermap tan (at_right a))" unfolding eventually_filtermap eventually_at_right by (metis eventually_at_right_field) qed ultimately show ?thesis unfolding filter_eq_iff by auto qed lemma filtermap_tan_at_left_inf: fixes a::real assumes "cos a=0" shows "filtermap tan (at_left a) = at_top" proof - have "filtermap tan (at_right (- a)) = at_bot" using filtermap_tan_at_right_inf[of "-a"] assms by auto then have "filtermap (uminus o tan) (at_left a) = at_bot" unfolding at_right_minus filtermap_filtermap comp_def by auto then have "filtermap uminus (filtermap (uminus o tan) (at_left a)) = filtermap uminus at_bot" by auto then show ?thesis unfolding filtermap_filtermap comp_def using at_top_mirror[where 'a=real] by auto qed subsection ‹Periodic set› (*Devised to characterize roots of Trigonometric equations, which are usually uniformly discrete.*) definition periodic_set:: "real set ⇒ real ⇒ bool" where "periodic_set S δ ⟷ (∃B. finite B ∧ (∀x∈S. ∃b∈B. ∃k::int. x =b + k * δ ))" lemma periodic_set_multiple: assumes "k≠0" shows "periodic_set S δ ⟷ periodic_set S (of_int k*δ)" proof assume asm:"periodic_set S δ " then obtain B1 where "finite B1" and B1_def:"∀x∈S. ∃b∈B1. (∃k::int. x = b + k * δ)" unfolding periodic_set_def by metis define B where "B = B1 ∪ {b+i*δ | b i. b∈B1 ∧ i∈{0..<¦k¦}}" have "∃b∈B. ∃k'. x = b + real_of_int k' * (real_of_int k * δ)" when "x∈S" for x proof - obtain b1 and k1::int where "b1∈B1" and x_δ:"x = b1 + k1 * δ" using B1_def[rule_format, OF ‹x∈S›] by auto define r d where "r= k1 mod ¦k¦" and "d = k1 div ¦k¦" define b kk where "b=b1+r*δ" and "kk = (if k>0 then d else -d)" have "x = b1 + (r+¦k¦*d)*δ" using x_δ unfolding r_def d_def by auto then have "x = b + kk*(k*δ)" unfolding b_def kk_def using ‹k≠0› by (auto simp add:algebra_simps) moreover have "b∈B" proof - have "r ∈ {0..<¦k¦}" unfolding r_def by (simp add: ‹k≠0›) then show ?thesis unfolding b_def B_def using ‹b1∈B1› by blast qed ultimately show ?thesis by auto qed moreover have "finite B" unfolding B_def using ‹finite B1› by (simp add: finite_image_set2) ultimately show "periodic_set S (real_of_int k * δ)" unfolding periodic_set_def by auto next assume "periodic_set S (real_of_int k * δ)" then show "periodic_set S δ" unfolding periodic_set_def by (metis mult.commute mult.left_commute of_int_mult) qed lemma periodic_set_empty[simp]: "periodic_set {} δ" unfolding periodic_set_def by auto lemma periodic_set_finite: assumes "finite S" shows "periodic_set S δ" unfolding periodic_set_def using assms mult.commute by force lemma periodic_set_subset[elim]: assumes "periodic_set S δ" "T ⊆ S" shows "periodic_set T δ" using assms unfolding periodic_set_def by (meson subsetCE) lemma periodic_set_union: assumes "periodic_set S δ" "periodic_set T δ" shows "periodic_set (S ∪ T) δ" using assms unfolding periodic_set_def by (metis Un_iff infinite_Un) lemma periodic_imp_uniform_discrete: assumes "periodic_set S δ" shows "uniform_discrete S" proof - have ?thesis when "S≠{}" "δ≠0" proof - obtain B g where "finite B" and g_def:"∀x∈S. g x∈B ∧ (∃k::int. x = g x + k * δ)" using assms unfolding periodic_set_def by metis define P where "P = ((*) δ) ` Ints" define B_diff where "B_diff = {¦x-y¦ | x y. x∈B ∧ y∈B} - P" have "finite B_diff" unfolding B_diff_def using ‹finite B› by (simp add: finite_image_set2) define e where "e = (if setdist B_diff P = 0 then ¦δ¦ else min (setdist B_diff P) (¦δ¦))" have "e>0" unfolding e_def using setdist_pos_le[unfolded order_class.le_less] ‹δ≠0› by auto moreover have "x=y" when "x∈S" "y∈S" "dist x y<e" for x y proof - obtain k1::int where k1:"x = g x + k1 * δ" and "g x∈B" using g_def ‹x∈S› by auto obtain k2::int where k2:"y = g y + k2 * δ" and "g y∈B" using g_def ‹y∈S› by auto have ?thesis when "¦g x - g y¦ ∈ P" proof - obtain k::int where k:"g x - g y = k * δ" proof - obtain k' where "k'∈Ints" and *:"¦g x - g y¦ = δ * k'" using ‹¦g x - g y¦ ∈ P› unfolding P_def image_iff by auto then obtain k where **:"k' = of_int k" using Ints_cases by auto show ?thesis apply (cases "g x - g y ≥ 0") subgoal using that[of k] * ** by simp subgoal using that[of "-k"] * ** by (auto simp add:algebra_simps) done qed have "dist x y = ¦(g x - g y)+(k1-k2)*δ¦" unfolding dist_real_def by (subst k1,subst k2,simp add:algebra_simps) also have "... = ¦(k+k1-k2)*δ¦" by (subst k,simp add:algebra_simps) also have "... = ¦k+k1-k2¦*¦δ¦" by (simp add: abs_mult) finally have *:"dist x y = ¦k+k1-k2¦*¦δ¦" . then have "¦k+k1-k2¦*¦δ¦ < e" using ‹dist x y<e› by auto then have "¦k+k1-k2¦*¦δ¦ < ¦δ¦" by (simp add: e_def split: if_splits) then have "¦k+k1-k2¦ = 0" unfolding e_def using ‹δ≠0› by force then have "dist x y=0" using * by auto then show ?thesis by auto qed moreover have ?thesis when "¦g x - g y¦ ∉ P" proof - have "¦g x - g y¦ ∈ B_diff" unfolding B_diff_def using ‹g x∈B› ‹g y∈B› that by auto have "e ≤ ¦¦g x - g y¦ - ¦(k1-k2)*δ¦¦" proof - have "¦g x - g y¦ ∈ B_diff" unfolding B_diff_def using ‹g x∈B› ‹g y∈B› that by auto moreover have "¦(k1-k2)*δ¦ ∈ P" unfolding P_def apply (intro rev_image_eqI[of "(if δ≥0 then ¦of_int(k1-k2)¦ else - ¦of_int(k1-k2)¦)"]) apply (metis Ints_minus Ints_of_int of_int_abs) by (auto simp add:abs_mult) ultimately have "¦¦g x - g y¦ - ¦(k1-k2)*δ¦¦ ≥ setdist B_diff P" using setdist_le_dist[of _ B_diff _ P] dist_real_def by auto moreover have "setdist B_diff P ≠ 0" proof - have "compact B_diff " using ‹finite B_diff› using finite_imp_compact by blast moreover have "closed P" unfolding P_def using closed_scaling[OF closed_Ints[where 'a=real], of δ] by auto moreover have "P ≠ {}" using Ints_0 unfolding P_def by blast moreover have "B_diff ∩ P = {}" unfolding B_diff_def by auto moreover have "B_diff ≠{}" unfolding B_diff_def using ‹g x∈B› ‹g y∈B› that by auto ultimately show ?thesis using setdist_eq_0_compact_closed[of B_diff P] by auto qed ultimately show ?thesis unfolding e_def by argo qed also have "... ≤ ¦(g x - g y) + (k1-k2)*δ¦" proof - define t1 where "t1=g x - g y" define t2 where "t2 = of_int (k1 - k2) * δ" show ?thesis apply (fold t1_def t2_def) by linarith qed also have "... = dist x y" unfolding dist_real_def by (subst (2) k1,subst (2) k2,simp add:algebra_simps) finally have "dist x y≥e" . then have False using ‹dist x y<e› by auto then show ?thesis by auto qed ultimately show ?thesis by auto qed ultimately show ?thesis unfolding uniform_discrete_def by auto qed moreover have ?thesis when "S={}" using that by auto moreover have ?thesis when "δ=0" proof - obtain B g where "finite B" and g_def:"∀x∈S. g x∈B ∧ (∃k::int. x = g x + k * δ)" using assms unfolding periodic_set_def by metis then have "∀x∈S. g x∈B ∧ (x = g x)" using that by fastforce then have "S ⊆ g ` B" by auto then have "finite S" using ‹finite B› by (auto elim:finite_subset) then show ?thesis using uniform_discrete_finite_iff by blast qed ultimately show ?thesis by blast qed lemma periodic_set_tan_linear: assumes "a≠0" "c≠0" shows "periodic_set (roots (λx. a*tan (x/c) + b)) (c*pi)" proof - define B where "B = { c*arctan (- b / a), c*pi/2}" have "∃b∈B. ∃k::int. x = b + k * (c*pi)" when "x∈roots (λx. a * tan (x/c) + b)" for x proof - define C1 where "C1 = (∃k::int. x = c*arctan (- b / a) + k * (c*pi))" define C2 where "C2 = (∃k::int. x = c*pi / 2 + k * (c*pi) ∧ - b / a = 0)" have "tan (x/c) = - b/a" using that ‹a≠0› unfolding roots_within_def by (auto simp add:field_simps) then have "C1 ∨ C2" unfolding C1_def C2_def using tan_eq_arctan_Ex[of "x/c" "-b/a"] ‹c≠0› by (auto simp add:field_simps) moreover have ?thesis when C1 using that unfolding C1_def B_def by blast moreover have ?thesis when C2 using that unfolding C2_def B_def by blast ultimately show ?thesis by auto qed moreover have "finite B" unfolding B_def by auto ultimately show ?thesis unfolding periodic_set_def by auto qed lemma periodic_set_cos_linear: assumes "a≠0" "c≠0" shows "periodic_set (roots (λx. a*cos (x/c) + b)) (2*c*pi)" proof - define B where "B = { c*arccos (- b / a), - c*arccos (- b / a)}" have "∃b∈B. ∃k::int. x = b + k * (2*c*pi)" when "x∈roots (λx. a * cos (x/c) + b)" for x proof - define C1 where "C1 = (∃k::int. x = c*arccos (- b / a) + k * (2*c*pi))" define C2 where "C2 = (∃k::int. x = - c*arccos (- b / a) + k * (2*c*pi))" have "cos (x/c) = - b/a" using that ‹a≠0› unfolding roots_within_def by (auto simp add:field_simps) then have "C1 ∨ C2" unfolding cos_eq_arccos_Ex ex_disj_distrib C1_def C2_def using ‹c≠0› apply (auto simp add:divide_simps) by (auto simp add:algebra_simps) moreover have ?thesis when C1 using that unfolding C1_def B_def by blast moreover have ?thesis when C2 using that unfolding C2_def B_def by blast ultimately show ?thesis by auto qed moreover have "finite B" unfolding B_def by auto ultimately show ?thesis unfolding periodic_set_def by auto qed lemma periodic_set_tan_poly: assumes "p≠0" "c≠0" shows "periodic_set (roots (λx. poly p (tan (x/c)))) (c*pi)" using assms proof (induct rule:poly_root_induct_alt) case 0 then show ?case by simp next case (no_proots p) then show ?case unfolding roots_within_def by simp next case (root a p) have "roots (λx. poly ([:- a, 1:] * p) (tan (x/c))) = roots (λx. tan (x/c) - a) ∪ roots (λx. poly p (tan (x/c)))" unfolding roots_within_def by auto moreover have "periodic_set (roots (λx. tan (x/c) - a)) (c*pi)" using periodic_set_tan_linear[OF _ ‹c≠0› ,of 1 "-a",simplified] . moreover have "periodic_set (roots (λx. poly p (tan (x/c)))) (c*pi)" using root by fastforce ultimately show ?case using periodic_set_union by simp qed lemma periodic_set_sin_cos_linear: fixes a b c ::real assumes "a≠0 ∨ b≠0 ∨ c≠0" shows "periodic_set (roots (λx. a * cos x + b * sin x + c)) (4*pi)" proof - define f where "f x= a * cos x + b * sin x + c" for x have "roots f = (roots f ∩ {x. cos (x/2) = 0}) ∪ (roots f ∩ {x. cos (x/2) ≠ 0})" by auto moreover have "periodic_set (roots f ∩ {x. cos (x/2) = 0}) (4*pi)" proof - have "periodic_set ({x. cos (x/2) = 0}) (4*pi)" using periodic_set_cos_linear[of 1 2 0,unfolded roots_within_def,simplified] by simp then show ?thesis by auto qed moreover have "periodic_set (roots f ∩ {x. cos (x/2) ≠ 0}) (4*pi)" proof - define p where "p=[:a+c,2*b,c-a:]" have "poly p (tan (x/2)) = 0 ⟷ f x=0" when "cos (x/2) ≠0" for x proof - define t where "t=tan (x/2)" define tt where "tt = 1+t^2" have "cos x = (1-t^2) / tt" unfolding tt_def t_def using cos_tan_half[OF that,simplified] by simp moreover have "sin x = 2*t / tt" unfolding tt_def t_def using sin_tan_half[of "x/2",simplified] by simp moreover have "tt≠0" unfolding tt_def by (metis power_one sum_power2_eq_zero_iff zero_neq_one) ultimately show ?thesis unfolding f_def p_def apply (fold t_def) apply simp apply (auto simp add:field_simps) by (auto simp add:algebra_simps tt_def power2_eq_square) qed then have "roots f ∩ {x. cos (x/2) ≠ 0} = roots (λx. poly p (tan (x/2))) ∩ {x. cos (x/2) ≠ 0}" unfolding roots_within_def by auto moreover have "periodic_set (roots (λx. poly p (tan (x/2))) ∩ {x. cos (x/2) ≠ 0}) (4*pi)" proof - have "p≠0" unfolding p_def using assms by auto then have "periodic_set (roots (λx. poly p (tan (x/2)))) (4*pi)" using periodic_set_tan_poly[of p 2,simplified] periodic_set_multiple[of 2 _ "2*pi",simplified] by auto then show ?thesis by auto qed ultimately show ?thesis by auto qed ultimately show "periodic_set (roots f) (4*pi)" using periodic_set_union by metis qed end

# Theory Missing_Analysis

(* Author: Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> *) section ‹Some useful lemmas in analysis› theory Missing_Analysis imports "HOL-Complex_Analysis.Complex_Analysis" begin subsection ‹More about paths› lemma pathfinish_offset[simp]: "pathfinish (λt. g t - z) = pathfinish g - z" unfolding pathfinish_def by simp lemma pathstart_offset[simp]: "pathstart (λt. g t - z) = pathstart g - z" unfolding pathstart_def by simp lemma pathimage_offset[simp]: fixes g :: "_ ⇒ 'b::topological_group_add" shows "p ∈ path_image (λt. g t - z) ⟷ p+z ∈ path_image g " unfolding path_image_def by (auto simp:algebra_simps) lemma path_offset[simp]: fixes g :: "_ ⇒ 'b::topological_group_add" shows "path (λt. g t - z) ⟷ path g" unfolding path_def proof assume "continuous_on {0..1} (λt. g t - z)" hence "continuous_on {0..1} (λt. (g t - z) + z)" apply (rule continuous_intros) by (intro continuous_intros) then show "continuous_on {0..1} g" by auto qed (auto intro:continuous_intros) lemma not_on_circlepathI: assumes "cmod (z-z0) ≠ ¦r¦" shows "z ∉ path_image (part_circlepath z0 r st tt)" proof (rule ccontr) assume "¬ z ∉ path_image (part_circlepath z0 r st tt)" then have "z∈path_image (part_circlepath z0 r st tt)" by simp then obtain t where "t∈{0..1}" and *:"z = z0 + r * exp (𝗂 * (linepath st tt t))" unfolding path_image_def image_def part_circlepath_def by blast define θ where "θ = linepath st tt t" then have "z-z0 = r * exp (𝗂 * θ)" using * by auto then have "cmod (z-z0) = cmod (r * exp (𝗂 * θ))" by auto also have "… = ¦r¦ * cmod (exp (𝗂 * θ))" by (simp add: norm_mult) also have "… = ¦r¦" by auto finally have "cmod (z-z0) = ¦r¦" . then show False using assms by auto qed lemma circlepath_inj_on: assumes "r>0" shows "inj_on (circlepath z r) {0..<1}" proof (rule inj_onI) fix x y assume asm: "x ∈ {0..<1}" "y ∈ {0..<1}" "circlepath z r x = circlepath z r y" define c where "c=2 * pi * 𝗂" have "c≠0" unfolding c_def by auto from asm(3) have "exp (c * x) =exp (c * y)" unfolding circlepath c_def using ‹r>0› by auto then obtain n where "c * x =c * (y + of_int n)" by (auto simp add:exp_eq c_def algebra_simps) then have "x=y+n" using ‹c≠0› by (meson mult_cancel_left of_real_eq_iff) then show "x=y" using asm(1,2) by auto qed subsection ‹More lemmas related to @{term winding_number}› lemma winding_number_comp: assumes "open s" "f holomorphic_on s" "path_image γ ⊆ s" "valid_path γ" "z ∉ path_image (f ∘ γ)" shows "winding_number (f ∘ γ) z = 1/(2*pi*𝗂)* contour_integral γ (λw. deriv f w / (f w - z))" proof - obtain spikes where "finite spikes" and γ_diff: "γ C1_differentiable_on {0..1} - spikes" using ‹valid_path γ› unfolding valid_path_def piecewise_C1_differentiable_on_def by auto have "valid_path (f ∘ γ)" using valid_path_compose_holomorphic assms by blast moreover have "contour_integral (f ∘ γ) (λw. 1 / (w - z)) = contour_integral γ (λw. deriv f w / (f w - z))" unfolding contour_integral_integral proof (rule integral_spike[rule_format,OF negligible_finite[OF ‹finite spikes›]]) fix t::real assume t:"t ∈ {0..1} - spikes" then have "γ differentiable at t" using γ_diff unfolding C1_differentiable_on_eq by auto moreover have "f field_differentiable at (γ t)" proof - have "γ t ∈ s" using ‹path_image γ ⊆ s› t unfolding path_image_def by auto thus ?thesis using ‹open s› ‹f holomorphic_on s› holomorphic_on_imp_differentiable_at by blast qed ultimately show " deriv f (γ t) / (f (γ t) - z) * vector_derivative γ (at t) = 1 / ((f ∘ γ) t - z) * vector_derivative (f ∘ γ) (at t)" apply (subst vector_derivative_chain_at_general) by (simp_all add:field_simps) qed moreover note ‹z ∉ path_image (f ∘ γ)› ultimately show ?thesis apply (subst winding_number_valid_path) by simp_all qed lemma winding_number_uminus_comp: assumes "valid_path γ" "- z ∉ path_image γ" shows "winding_number (uminus ∘ γ) z = winding_number γ (-z)" proof - define c where "c= 2 * pi * 𝗂" have "winding_number (uminus ∘ γ) z = 1/c * contour_integral γ (λw. deriv uminus w / (-w-z)) " proof (rule winding_number_comp[of UNIV, folded c_def]) show "open UNIV" "uminus holomorphic_on UNIV" "path_image γ ⊆ UNIV" "valid_path γ" using ‹valid_path γ› by (auto intro:holomorphic_intros) show "z ∉ path_image (uminus ∘ γ)" unfolding path_image_compose using ‹- z ∉ path_image γ› by auto qed also have "… = 1/c * contour_integral γ (λw. 1 / (w- (-z)))" by (auto intro!:contour_integral_eq simp add:field_simps minus_divide_right) also have "… = winding_number γ (-z)" using winding_number_valid_path[OF ‹valid_path γ› ‹- z ∉ path_image γ›,folded c_def] by simp finally show ?thesis by auto qed lemma winding_number_comp_linear: assumes "c≠0" "valid_path γ" and not_image: "(z-b)/c ∉ path_image γ" shows "winding_number ((λx. c*x+b) ∘ γ) z = winding_number γ ((z-b)/c)" (is "?L = ?R") proof - define cc where "cc=1 / (complex_of_real (2 * pi) * 𝗂)" define zz where "zz=(z-b)/c" have "?L = cc * contour_integral γ (λw. deriv (λx. c * x + b) w / (c * w + b - z))" apply (subst winding_number_comp[of UNIV,simplified]) subgoal by (auto intro:holomorphic_intros) subgoal using ‹valid_path γ› . subgoal using not_image ‹c≠0› unfolding path_image_compose by auto subgoal unfolding cc_def by auto done also have "… = cc * contour_integral γ (λw.1 / (w - zz))" proof - have "deriv (λx. c * x + b) = (λx. c)" by (auto intro:derivative_intros) then show ?thesis unfolding zz_def cc_def using ‹c≠0› by (auto simp:field_simps) qed also have "… = winding_number γ zz" using winding_number_valid_path[OF ‹valid_path γ› not_image,folded zz_def cc_def] by simp finally show "winding_number ((λx. c * x + b) ∘ γ) z = winding_number γ zz" . qed end

# Theory Cauchy_Index_Theorem

(* 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