# 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 (fS)"
shows "filtermap f (at a within S) = at (f a) within fS"
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 _ "fT"])
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∈fS⟶ 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]
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]
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 (fS)"
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 _ "fS"])
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)

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

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

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)

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)

lemma deriv_pderiv:
"deriv (poly p) = poly (pderiv p)"
apply (rule ext)
apply (rule DERIV_imp_deriv)
using poly_DERIV .

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 (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 "∀⇩Fx 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 "∀⇩Fx 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

"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
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
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"
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
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)
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 ‹
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
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