Session Winding_Number_Eval

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" "c0"
  shows "open (((*) c) ` S)" 
proof -
  let ?f = "λx. x/c" and ?g="((*) c)"
  have "continuous_on UNIV ?f" using c0 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 c0
    apply auto
    using image_iff by fastforce
  ultimately show ?thesis by auto
qed   
 
lemma image_linear_greaterThan:
  fixes x::"'a::linordered_field"
  assumes "c0"
  shows "((λx. c*x+b) ` {x<..}) = (if c>0 then {c*x+b <..} else {..< c*x+b})"
using c0
  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 "c0"
  shows "((λx. c*x+b) ` {..<x}) = (if c>0 then {..<c*x+b} else {c*x+b<..})"
using c0
  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 "xs. f xy" "continuous_on s f" "connected s"
  shows "(xs. f x>y)  (xs. 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 "bclosure ({..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 "aclosure ({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" "c0"
  shows "F x in F. inverse (f x) * f x = 1"
proof -
  have "F x in F. f x0" 
    using assms tendsto_imp_eventually_ne by blast
  then show ?thesis
    apply (elim eventually_mono)
    by auto
qed  
  
subsection ‹More about @{term filtermap} 

lemma filtermap_linear_at_within:
  assumes "bij f" and cont: "isCont f a" and open_map: "S. open S  open (f`S)"
  shows "filtermap f (at a within S) = at (f a) within f`S"
  unfolding filter_eq_iff
proof safe
  fix P
  assume "eventually P (filtermap f (at a within S))"
  then obtain T where "open T" "a  T" and impP:"xT. xa  xS P (f x)"
    by (auto simp: eventually_filtermap eventually_at_topological)
  then show "eventually P (at (f a) within f ` S)"
    unfolding eventually_at_topological
    apply (intro exI[of _ "f`T"])
    using ‹bij f open_map by (metis bij_pointE imageE imageI)  
next
  fix P
  assume "eventually P (at (f a) within f ` S)"
  then obtain T1 where "open T1" "f a  T1" and impP:"xT1. xf a  xf`S P (x)"
    unfolding eventually_at_topological by auto
  then obtain T2 where "open T2" "a  T2" "(x'T2. f x'  T1)" 
    using cont[unfolded continuous_at_open,rule_format,of T1] by blast 
  then have "xT2. xa  xS 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 "c0"
  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 c0 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 "c0"
  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 c0 
      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 _ c0,THEN open_translation,of _ b]  
      by (simp add:image_image add.commute)
    show "at (?f x) within ?f ` {..<x} = at (?f x) within ?f ` {..<x}" by simp
  qed
  moreover have "?f ` {..<x} =  {..<?f x}" when "c>0" 
    using image_linear_lessThan[OF c0,of b x] that by auto
  moreover have "?f ` {..<x} =  {?f x<..}" when "¬ c>0" 
    using image_linear_lessThan[OF c0,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 "c0"
  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 c0 
      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 _ c0,THEN open_translation,of _ b]  
      by (simp add:image_image add.commute)
    show "at (?f x) within ?f ` {x<..} = at (?f x) within ?f ` {x<..}" by simp
  qed
  moreover have "?f ` {x<..} =  {?f x<..}" when "c>0" 
    using image_linear_greaterThan[OF c0,of b x] that by auto
  moreover have "?f ` {x<..} =  {..<?f x}" when "¬ c>0" 
    using image_linear_greaterThan[OF c0,of b x] that by auto
  ultimately show ?thesis by auto
qed
 
lemma filtermap_at_top_linear_eq:
  fixes c::"'a::linordered_field"
  assumes "c0"
  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 c0 by auto
  then have "filtermap (λx. x * c + b) at_top = at_bot"
    apply (intro filtermap_fun_inverse[of "λx. (x-b) / c"])
    subgoal unfolding eventually_at_bot_linorder filterlim_at_top
      by (auto simp add: field_simps)
    subgoal unfolding eventually_at_top_linorder filterlim_at_bot
      by (meson le_diff_eq neg_divide_le_eq)
    by auto
  then show ?thesis using c<0 by auto
qed

  
lemma filtermap_nhds_open_map:
  assumes cont: "isCont f a"
    and open_map: "S. open S  open (f`S)"
  shows "filtermap f (nhds a) = nhds (f a)"
  unfolding filter_eq_iff
proof safe
  fix P
  assume "eventually P (filtermap f (nhds a))"
  then obtain S where "open S" "a  S" "xS. P (f x)"
    by (auto simp: eventually_filtermap eventually_nhds)
  then show "eventually P (nhds (f a))"
    unfolding eventually_nhds 
    apply (intro exI[of _ "f`S"]) 
    by (auto intro!: open_map)
qed (metis filterlim_iff tendsto_at_iff_tendsto_nhds isCont_def eventually_filtermap cont)
  
subsection ‹More about @{term filterlim}
  
lemma filterlim_at_infinity_times:
  fixes f :: "'a  'b::real_normed_field"
  assumes "filterlim f at_infinity F" "filterlim g at_infinity F"
  shows "filterlim (λx. f x * g x) at_infinity F"  
proof -
  have "((λx. inverse (f x) * inverse (g x))  0 * 0) F"
    by (intro tendsto_mult tendsto_inverse assms filterlim_compose[OF tendsto_inverse_0])
  then have "filterlim (λx. inverse (f x) * inverse (g x)) (at 0) F"
    unfolding filterlim_at using assms
    by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj)
  then show ?thesis
    by (subst filterlim_inverse_at_iff[symmetric]) simp_all
qed   
  
lemma filterlim_at_top_at_bot[elim]:
  fixes f::"'a  'b::unbounded_dense_linorder" and F::"'a filter"
  assumes top:"filterlim f at_top F" and bot: "filterlim f at_bot F" and "Fbot"
  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 Fbot› 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 "Fbot"
  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 Fbot› 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 "Fbot"
  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 Fbot› by auto
qed  
  
lemma filterlim_at_top_linear_iff:
  fixes f::"'a::linordered_field  'b"
  assumes "c0"
  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 "c0"
  shows "(LIM x at_bot. f (x * c + b) :> F2)  (if c>0 then (LIM x at_bot. f x :> F2) 
            else (LIM x at_top. f x :> F2)) "
  unfolding filterlim_def 
  apply (subst filtermap_filtermap[of f "λx. x * c + b",symmetric])
  using assms by (auto simp add:filtermap_at_bot_linear_eq)      
  
  
lemma filterlim_tendsto_add_at_top_iff:
  assumes f: "(f  c) F"
  shows "(LIM x F. (f x + g x :: real) :> at_top)  (LIM x F. g x :> at_top)"
proof     
  assume "LIM x F. f x + g x :> at_top" 
  moreover have "((λx. - f x)  - c) F"
    using f by (intro tendsto_intros,simp)
  ultimately show "filterlim g at_top F" using filterlim_tendsto_add_at_top 
    by fastforce
qed (auto simp add:filterlim_tendsto_add_at_top[OF f])    
    
  
lemma filterlim_tendsto_add_at_bot_iff:
  fixes c::real
  assumes f: "(f  c) F"
  shows "(LIM x F. f x + g x :> at_bot)  (LIM x F. g x :> at_bot)" 
proof -
  have "(LIM x F. f x + g x :> at_bot) 
          (LIM x F. - f x + (- g x)  :> at_top)"
    apply (subst filterlim_uminus_at_top)
    by (rule filterlim_cong,auto)
  also have "... = (LIM x F. - g x  :> at_top)"
    apply (subst filterlim_tendsto_add_at_top_iff[of _ "-c"])
    by (auto intro:tendsto_intros simp add:f)
  also have "... = (LIM x F. g x  :> at_bot)"
    apply (subst filterlim_uminus_at_top)
    by (rule filterlim_cong,auto)
  finally show ?thesis .
qed
  
lemma tendsto_inverse_0_at_infinity: 
    "LIM x F. f x :> at_infinity  ((λx. inverse (f x) :: real)  0) F"
  by (metis filterlim_at filterlim_inverse_at_iff)

lemma filterlim_at_infinity_divide_iff:
  fixes f::"'a  'b::real_normed_field"
  assumes "(f  c) F" "c0"
  shows "(LIM x F. f x / g x :> at_infinity)  (LIM x F. g x :> at 0)"
proof 
  assume asm:"LIM x F. f x / g x :> at_infinity"
  have "LIM x F. inverse (f x) * (f x / g x) :> at_infinity"
    apply (rule tendsto_mult_filterlim_at_infinity[of _ "inverse c", OF _ _ asm])
    by (auto simp add: assms(1) assms(2) tendsto_inverse)
  then have "LIM x F. inverse (g x) :> at_infinity"
    apply (elim filterlim_mono_eventually)
    using eventually_times_inverse_1[OF assms] 
    by (auto elim:eventually_mono simp add:field_simps)
  then show "filterlim g (at 0) F" using filterlim_inverse_at_iff[symmetric] by force 
next
  assume "filterlim g (at 0) F" 
  then have "filterlim (λx. inverse (g x)) at_infinity F"
    using filterlim_compose filterlim_inverse_at_infinity by blast
  then have "LIM x F. f x * inverse (g x) :> at_infinity"
    using tendsto_mult_filterlim_at_infinity[OF assms, of "λx. inverse(g x)"] 
    by simp
  then show "LIM x F. f x / g x :> at_infinity" by (simp add: divide_inverse)
qed  
  
lemma filterlim_tendsto_pos_mult_at_top_iff:
  fixes f::"'a  real"
  assumes "(f  c) F" and "0 < c"
  shows "(LIM x F. (f x * g x) :> at_top)  (LIM x F. g x :> at_top)"
proof 
  assume "filterlim g at_top F"
  then show "LIM x F. f x * g x :> at_top" 
    using filterlim_tendsto_pos_mult_at_top[OF assms] by auto
next
  assume asm:"LIM x F. f x * g x :> at_top"
  have "((λx. inverse (f x))  inverse c) F" 
    using tendsto_inverse[OF assms(1)] 0<c by auto
  moreover have "inverse c >0" using assms(2) by auto
  ultimately have "LIM x F. inverse (f x) * (f x * g x) :> at_top"
    using filterlim_tendsto_pos_mult_at_top[OF _ _ asm,of "λx. inverse (f x)" "inverse c"] by auto
  then show "LIM x F. g x :> at_top"
    apply (elim filterlim_mono_eventually)
      apply simp_all[2]
    using eventually_times_inverse_1[OF assms(1)] c>0 eventually_mono by fastforce
qed  

lemma filterlim_tendsto_pos_mult_at_bot_iff:
  fixes c :: real
  assumes "(f  c) F" "0 < c" 
  shows "(LIM x F. f x * g x :> at_bot)  filterlim g at_bot F"
  using filterlim_tendsto_pos_mult_at_top_iff[OF assms(1,2), of "λx. - g x"] 
  unfolding filterlim_uminus_at_bot by simp    

lemma filterlim_tendsto_neg_mult_at_top_iff:
  fixes f::"'a  real"
  assumes "(f  c) F" and "c < 0"
  shows "(LIM x F. (f x * g x) :> at_top)  (LIM x F. g x :> at_bot)"  
proof -
  have "(LIM x F. f x * g x :> at_top) = (LIM x F. - g x :> at_top)"
    apply (rule filterlim_tendsto_pos_mult_at_top_iff[of "λx. - f x" "-c" F "λx. - g x", simplified])
    using assms by (auto intro: tendsto_intros )
  also have "... = (LIM x F. g x :> at_bot)" 
    using filterlim_uminus_at_bot[symmetric] by auto
  finally show ?thesis .
qed

lemma filterlim_tendsto_neg_mult_at_bot_iff:
  fixes c :: real
  assumes "(f  c) F" "0 > c" 
  shows "(LIM x F. f x * g x :> at_bot)  filterlim g at_top F"
  using filterlim_tendsto_neg_mult_at_top_iff[OF assms(1,2), of "λx. - g x"] 
  unfolding filterlim_uminus_at_top by simp    

lemma Lim_add:
  fixes f g::"_  'a::{t2_space,topological_monoid_add}"
  assumes "y. (f  y) F" and "y. (g  y) F" and "Fbot"
  shows "Lim F f + Lim F g = Lim F (λx. f x+g x)"
  apply (rule tendsto_Lim[OF Fbot›, 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  (xS  (T. open T  T  S = {x}))"  
    
definition (in topological_space) discrete:: "'a set  bool" 
  where "discrete S  (xS. x isolate S)"  
    
definition (in metric_space) uniform_discrete :: "'a set  bool" where
  "uniform_discrete S  (e>0. xS. yS. dist x y < e  x = y)"
  
lemma uniformI1:
  assumes "e>0" "x y. xS;yS;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. xS;yS;xy  dist x ye "
  shows "uniform_discrete S"  
unfolding uniform_discrete_def using assms not_less by blast
  
lemma isolate_islimpt_iff:"(x isolate S)  (¬ (x islimpt S)  xS)"
  unfolding isolate_def islimpt_def by auto
  
lemma isolate_dist_Ex_iff:
  fixes x::"'a::metric_space"
  shows "x isolate S  (xS  (e>0. yS. 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  xT  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 "aS" 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 "aS" "S{}"
  proof -
    obtain e1 where "e1>0" and e1_dist:"xS. yS. 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 "xinsert a S" "yinsert 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" "yS"
        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" "xS"
        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 "xS" "yS"
        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. yS. 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: "yS. y  x  f x  dist x y"
        if "xS" 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 "xS. yS. 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:"xS. yS. 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{}" "c0"
  proof -
    obtain x1 where "x1S" 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 "x2S-{x1}" using S-{x1}  {} by auto
      then have "x2S" "x1x2" 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 x1S x2S] .
      moreover have "dist (f x2) (f x2)  0" by auto
      ultimately have False using c0 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:"xS. yS. 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:"y1S" "x1=f y1" using x1 f ` S by auto
      obtain y2 where y2:"y2S" "x2=f y2" using x2 f ` S by auto    
      have "dist y1 y2 < e1"
        using dist[rule_format, OF y1(1) y2(1)] c>0 ‹dist x1 x2 < e unfolding e_def
        apply (fold y1(2) y2(2))
        by (auto simp add:divide_simps mult.commute) 
      then have "y1=y2"    
        using e1_dist[rule_format, OF y2(1) y1(1)] by simp
      then show "x1=x2" using y1(2) y2(2) by auto
    qed
    moreover have "e>0" using e1>0 c>0 unfolding e_def by auto
    ultimately show ?thesis unfolding uniform_discrete_def by meson
  qed
  ultimately show ?thesis by fastforce
qed
 

  
end

Theory Missing_Algebraic

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

section ‹Some useful lemmas in algebra›

theory Missing_Algebraic imports
  "HOL-Computational_Algebra.Polynomial_Factorial"
  "HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
  "HOL-Complex_Analysis.Complex_Analysis"
  Missing_Topology
  "Budan_Fourier.BF_Misc"
begin

subsection ‹Misc›

lemma poly_holomorphic_on[simp]:
  "(poly p) holomorphic_on s"
  apply (rule holomorphic_onI)
  apply (unfold field_differentiable_def)
  apply (rule_tac x="poly (pderiv p) x" in exI)
  by (simp add:has_field_derivative_at_within)

lemma order_zorder:
  fixes p::"complex poly" and z::complex
  assumes "p0"
  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:"(wcball 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 "(wball z r. poly p w = h w * (w - z) ^ n)" 
    and "h z0"
    by auto
  then have "order z p = n" using p0
  proof (induct n arbitrary:p h)
    case 0
    then have "poly p z=h z" using r>0 by auto 
    then have "poly p z0" using h z0 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 "wball 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) wball 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 wball 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 "wball 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' z0" 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 p0 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 p0 by auto
    ultimately show ?case using order_pderiv[OF ‹pderiv p  0] by auto
  qed
  then show ?thesis unfolding n_def .
qed  

lemma pcompose_pCons_0:"pcompose p [:a:] = [:poly p a:]"
  apply (induct p)
  by (auto simp add:pcompose_pCons algebra_simps)       
   
lemma pcompose_coeff_0:
  "coeff (pcompose p q) 0 = poly p (coeff q 0)"
  apply (induct p)
  by (auto simp add:pcompose_pCons coeff_mult)  
    
lemma poly_field_differentiable_at[simp]:
  "poly p field_differentiable (at x within s)"
apply (unfold field_differentiable_def)
apply (rule_tac x="poly (pderiv p) x" in exI)
by (simp add:has_field_derivative_at_within)  
  
lemma deriv_pderiv:
  "deriv (poly p) = poly (pderiv p)"
apply (rule ext)  
apply (rule DERIV_imp_deriv)  
  using poly_DERIV . 
    
lemma lead_coeff_map_poly_nz:
  assumes "f (lead_coeff p) 0" "f 0=0"
  shows "lead_coeff (map_poly f p) = f (lead_coeff p) "
proof -
  have "lead_coeff (Poly (map f (coeffs p))) = f (lead_coeff p)"
    by (metis (mono_tags, lifting) antisym assms(1) assms(2) coeff_0_degree_minus_1 coeff_map_poly 
        degree_Poly degree_eq_length_coeffs le_degree length_map map_poly_def)
  then show ?thesis
    by (simp add: map_poly_def)
qed 

lemma filterlim_poly_at_infinity:
  fixes p::"'a::real_normed_field poly"
  assumes "degree p>0"
  shows "filterlim (poly p) at_infinity at_infinity"
using assms
proof (induct p)
  case 0
  then show ?case by auto
next
  case (pCons a p)
  have ?case when "degree p=0"
  proof -
    obtain c where c_def:"p=[:c:]" using ‹degree p = 0 degree_eq_zeroE by blast
    then have "c0" using 0 < degree (pCons a p) by auto
    then show ?thesis unfolding c_def 
      apply (auto intro!:tendsto_add_filterlim_at_infinity)
      apply (subst mult.commute)
      by (auto intro!:tendsto_mult_filterlim_at_infinity filterlim_ident)
  qed
  moreover have ?case when "degree p0"
  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 "p0"
  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 x1"
      then have "x0" 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 p0 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 "n0"
  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 x1"
    then have "x0" 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 "p0" using assms by auto
      then show ?thesis
        unfolding pp_def using poly_divide_tendsto_aux[of p] 
        apply (drule_tac tendsto_inverse)
        by (auto simp add:inverse_eq_divide)
    qed  
    moreover have "(dd  0) at_infinity" 
      unfolding dd_def
      apply (rule tendsto_divide_0)
      by (auto intro!: filterlim_power_at_infinity simp add:assms)
    ultimately show ?thesis by (auto intro:tendsto_eq_intros)
  qed
  ultimately show ?thesis by (auto dest:tendsto_cong)
qed
    
lemma lead_coeff_list_def:
  "lead_coeff p= (if coeffs p=[] then 0 else last (coeffs p))"
by (simp add: last_coeffs_eq_coeff_degree)
  
lemma poly_linepath_comp: 
  fixes a::"'a::{real_normed_vector,comm_semiring_0,real_algebra_1}"
  shows "poly p o (linepath a b) = poly (p p [:a, b-a:]) o of_real"
  apply rule
  by (auto simp add:poly_pcompose linepath_def scaleR_conv_of_real algebra_simps)

lemma poly_eventually_not_zero:
  fixes p::"real poly"
  assumes "p0"
  shows "eventually (λx. poly p x0) 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 xS" using that unfolding S_def by auto
    moreover have "finite S" using p0 poly_roots_finite unfolding S_def by blast
    ultimately have "norm xMax 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 x0" "degree y0"
  shows "degree (x div y) < degree x"
proof -
  have "x0" "y0" 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 y0 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 "q0" using x0 y0 by auto
    from degree_mult_eq[OF this y0] 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 "q0" using ‹degree r < degree x by auto
    have "degree x = degree q +degree y" 
      using  degree_mult_eq[OF q0 y0] 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 p0"
  shows "degree (map_poly f p) < degree p" 
proof -
  have "length (coeffs p) >1" 
    using ‹degree p0 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 = {xs. 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 "p0" 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 * 𝗂 * 
            (xproots 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 p0] )
  also have "... =  2 * of_real pi * 𝗂 * (xproots p. winding_number g x * of_nat (order x p))"
  proof -
    have "nat (zorder (poly p) x) = order x p" when "xproots p" for x 
      using order_zorder[OF p0] that unfolding proots_def by auto
    then show ?thesis unfolding proots_def 
      apply (auto intro!:comm_monoid_add_class.sum.cong)
      by (metis assms(1) nat_eq_iff2 of_nat_nat order_root)
  qed
  finally show ?thesis . 
qed  
  
end

Theory Missing_Transcendental

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

section ‹Some useful lemmas about transcendental functions›

theory Missing_Transcendental imports
  Missing_Topology
  Missing_Algebraic
begin

subsection ‹Misc›

lemma Im_Ln_eq_pi_half:
    "z  0  (Im(Ln z) = pi/2  0 < Im(z)  Re(z) = 0)"
    "z  0  (Im(Ln z) = -pi/2  Im(z) < 0  Re(z) = 0)"
proof -
  show "z  0  (Im(Ln z) = pi/2  0 < Im(z)  Re(z) = 0)"
    by (metis Im_Ln_eq_pi Im_Ln_le_pi Im_Ln_pos_lt Re_Ln_pos_le Re_Ln_pos_lt
      abs_of_nonneg less_eq_real_def order_less_irrefl pi_half_gt_zero)
next
  assume "z0"
  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 "z0"
  shows "Im (Ln z) = (if Re z0 then
                        if Re z>0 then
                          arctan (Im z/Re z)
                        else if Im z0 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 "z0" 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 z0] θ_def using z0 ‹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 z0] θ_def using z0 ‹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 z0] 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 z0"
  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 z0])
      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 z0])
      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  -1y  y1  (k::int. x = arccos y + 2*k*pi  x = - arccos y + 2*k*pi)"
proof
  assume asm:"-1y  y1  (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*pi0"
  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 "-1y  y1" using asm by auto
  ultimately show "-1y  y1  ?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" "a0a1" "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 a0"
  shows "filtermap tan (at_right a) = at_right (tan a)"
proof -
  obtain k::int and a1 where aa1:"a=k*pi+a1" and "-pi/2a1" "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/2a1 by auto
    then have "cos a = 0" unfolding aa1
      by (metis (no_types, hide_lams) add.commute add_0_left cos_pi_half 
              diff_eq_eq mult.left_neutral mult_minus_right mult_zero_left 
              sin_add sin_pi_half sin_zero_iff_int2 times_divide_eq_left uminus_add_conv_diff)
    then show False using assms by auto
  qed
  have "eventually P (at_right (tan a))" 
    when "eventually P (filtermap tan (at_right a))" for P
  proof -
    obtain b1 where "b1>a" and b1_imp:" y>a. y < b1  P (tan y)"
      using ‹eventually P (filtermap tan (at_right a))
      unfolding eventually_filtermap eventually_at_right 
      by (metis eventually_at_right_field)
    define b2 where "b2=min b1 (k*pi+pi/4+a1/2)"  
    define b3 where "b3=b2 - k*pi"
    have "-pi/2 < b3" "b3<pi/2" 
    proof -
      have "a1<b3"
        using b1>a aa1 a1<pi/2 unfolding b2_def b3_def by (auto simp add:field_simps)
      then show "-pi/2 < b3" using -pi/2a1 by auto
      show "b3 < pi/2"
        unfolding b2_def b3_def
        apply (subst min_diff_distrib_left)
        apply (rule min.strict_coboundedI2)
        using b1>a aa1 a1<pi/2 -pi/2<a1 by auto
    qed
    have "tan b2 > tan a" 
    proof -
      have "tan a = tan a1"
        using aa1 by (simp add: add.commute)
      also have "... < tan b3"
      proof -
        have "a1<b3"
          using b1>a aa1 a1<pi/2 unfolding b2_def b3_def by (auto simp add:field_simps)
        then show ?thesis
          using tan_monotone -pi/2 < a1 b3 < pi/2 by simp
      qed
      also have "... = tan b2" unfolding b3_def
        by (metis Groups.mult_ac(2) add_uminus_conv_diff mult_minus_right of_int_minus 
          tan_periodic_int)
      finally show ?thesis .
    qed
    moreover have "P y" when "y>tan a" "y < tan b2" for y
    proof -
      define y1 where "y1=arctan y+ k * pi"
      have "a<y1" 
      proof -
        have "arctan (tan a) < arctan y" using y>tan a arctan_monotone by auto
        then have "a1<arctan y"
          using arctan_tan -pi/2 < a1 a1<pi/2 unfolding aa1 by (simp add: add.commute)
        then show ?thesis unfolding y1_def aa1 by auto
      qed
      moreover have "y1<b2"
      proof - 
        have "arctan y < arctan (tan b2)"
          using y < tan b2 arctan_monotone by auto
        moreover have "arctan (tan b2) = b3"
          using arctan_tan[of b3] -pi/2 < b3 b3<pi/2 unfolding b3_def 
          by (metis add.inverse_inverse diff_minus_eq_add divide_minus_left mult.commute 
            mult_minus_right of_int_minus tan_periodic_int)
        ultimately have "arctan y < b3" by auto
        then show ?thesis unfolding y1_def b3_def by auto
      qed
      moreover have "y>a. y < b2  P (tan y)"
        using b1_imp unfolding b2_def by auto
      moreover have "tan y1=y" unfolding y1_def by (auto simp add:tan_arctan)
      ultimately show ?thesis by auto
    qed
    ultimately show "eventually P (at_right (tan a))" 
      unfolding eventually_at_right by (metis eventually_at_right_field)
  qed
  moreover have "eventually P (filtermap tan (at_right a))" 
    when "eventually P (at_right (tan a))" for P
  proof -
    obtain b1 where "b1>tan a" and b1_imp:"y>tan a. y < b1  P y" 
      using ‹eventually P (at_right (tan a)) unfolding eventually_at_right 
      by (metis eventually_at_right_field)
    define b2 where "b2=arctan b1 + k*pi" 
    have "a1 < arctan b1" 
      by (metis - pi / 2 < a1 a1 < pi / 2 ‹tan a < b1 aa1 add.commute arctan_less_iff 
            arctan_tan divide_minus_left tan_periodic_int)
    then have "b2>a" unfolding aa1 b2_def by auto
    moreover have "P (tan y)" when "y>a" "y < b2" for y
    proof -
      define y1 where "y1 = y - k*pi"
      have "a1 < y1" "y1 < arctan b1" unfolding y1_def
        subgoal using y>a unfolding aa1 by auto
        subgoal using b2_def that(2) by linarith
        done
      then have "tan a1 < tan y1" "tan y1< b1"
        subgoal using a1>-pi/2
          apply (intro tan_monotone,simp,simp)
          using arctan_ubound less_trans by blast
        subgoal 
          by (metis - pi / 2 < a1 a1 < y1 y1 < arctan b1 arctan_less_iff arctan_tan 
              arctan_ubound divide_minus_left less_trans)
        done
      have "tan y>tan a" 
        by (metis ‹tan a1 < tan y1 aa1 add.commute add_uminus_conv_diff mult.commute 
            mult_minus_right of_int_minus tan_periodic_int y1_def)
      moreover have "tan y<b1" 
        by (metis ‹tan y1 < b1 add_uminus_conv_diff mult.commute mult_minus_right 
            of_int_minus tan_periodic_int y1_def)
      ultimately show ?thesis using b1_imp by auto
    qed
    ultimately show ?thesis unfolding eventually_filtermap eventually_at_right 
      by (metis eventually_at_right_field)
  qed
  ultimately show ?thesis unfolding filter_eq_iff by blast
qed

lemma filtermap_tan_at_left:
  fixes a::real
  assumes "cos a0"
  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  (xS. bB. k::int. x =b + k * δ ))"

lemma periodic_set_multiple:
  assumes "k0"
  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:"xS. bB1. (k::int. x = b + k * δ)"
    unfolding periodic_set_def by metis
  define B where "B = B1  {b+i*δ | b i. bB1  i{0..<¦k¦}}"
  have "bB. k'. x = b + real_of_int k' * (real_of_int k * δ)" when "xS" for x
  proof -
    obtain b1 and k1::int where "b1B1" and x_δ:"x = b1 + k1 * δ"
      using B1_def[rule_format, OF xS] 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 k0
      by (auto simp add:algebra_simps)
    moreover have "bB"
    proof -
      have "r  {0..<¦k¦}" unfolding r_def by (simp add: k0)
      then show ?thesis unfolding b_def B_def using b1B1 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:"xS. g xB  (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.  xB  yB} - 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 "xS" "yS" "dist x y<e" for x y
    proof -
      obtain k1::int where k1:"x = g x + k1 * δ" and "g xB" using g_def xS by auto
      obtain k2::int where k2:"y = g y + k2 * δ" and "g yB" using g_def yS 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 xB g yB 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 xB g yB 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 xB g yB 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 ye" .
        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:"xS. g xB  (k::int. x = g x + k * δ)"
      using assms unfolding periodic_set_def by metis
    then have "xS. g xB  (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 "a0" "c0"
  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 "bB. k::int. x = b + k * (c*pi)" when "xroots (λ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 a0 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"]  c0
      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 "a0" "c0"
  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 "bB. k::int. x = b + k * (2*c*pi)"
    when "xroots (λ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 a0 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 c0
      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 "p0" "c0"
  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 _ c0 ,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 "a0  b0  c0"
  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 "tt0" 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 "p0" 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 "zpath_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 "c0" 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 c0
    by (meson mult_cancel_left of_real_eq_iff)
  then show "x=y" using asm(1,2) by auto
qed

subsection ‹More lemmas related to @{term winding_number}  
  
lemma winding_number_comp:
  assumes "open s" "f holomorphic_on s" "path_image γ  s"  
    "valid_path γ" "z  path_image (f  γ)" 
  shows "winding_number (f  γ) z = 1/(2*pi*𝗂)* contour_integral γ (λw. deriv f w / (f w - z))"
proof -
  obtain spikes where "finite spikes" and γ_diff: "γ C1_differentiable_on {0..1} - spikes"
    using ‹valid_path γ unfolding valid_path_def piecewise_C1_differentiable_on_def by auto  
  have "valid_path (f  γ)" 
    using valid_path_compose_holomorphic assms by blast
  moreover have "contour_integral (f  γ) (λw. 1 / (w - z)) 
      = contour_integral γ (λw. deriv f w / (f w - z))"
    unfolding contour_integral_integral
  proof (rule integral_spike[rule_format,OF negligible_finite[OF ‹finite spikes]])
    fix t::real assume t:"t  {0..1} - spikes"
    then have "γ differentiable at t" 
      using γ_diff unfolding C1_differentiable_on_eq by auto
    moreover have "f field_differentiable at (γ t)" 
    proof -
      have "γ t  s" using ‹path_image γ  s t unfolding path_image_def by auto 
      thus ?thesis 
        using ‹open s f holomorphic_on s  holomorphic_on_imp_differentiable_at by blast
    qed
    ultimately show " deriv f (γ t) / (f (γ t) - z) * vector_derivative γ (at t) =
         1 / ((f  γ) t - z) * vector_derivative (f  γ) (at t)"
      apply (subst vector_derivative_chain_at_general)
      by (simp_all add:field_simps)
  qed
  moreover note z  path_image (f  γ) 
  ultimately show ?thesis
    apply (subst winding_number_valid_path)
    by simp_all
qed  
  
lemma winding_number_uminus_comp:
  assumes "valid_path γ" "- z  path_image γ" 
  shows "winding_number (uminus  γ) z = winding_number γ (-z)"
proof -
  define c where "c= 2 * pi * 𝗂"
  have "winding_number (uminus  γ) z = 1/c * contour_integral γ (λw. deriv uminus w / (-w-z)) "
  proof (rule winding_number_comp[of UNIV, folded c_def])
    show "open UNIV" "uminus holomorphic_on UNIV" "path_image γ  UNIV" "valid_path γ"
      using ‹valid_path γ by (auto intro:holomorphic_intros)
    show "z  path_image (uminus  γ)" 
      unfolding path_image_compose using - z  path_image γ by auto
  qed
  also have " = 1/c * contour_integral γ (λw. 1 / (w- (-z)))"
    by (auto intro!:contour_integral_eq simp add:field_simps minus_divide_right)
  also have " = winding_number γ (-z)"
    using winding_number_valid_path[OF ‹valid_path γ - z  path_image γ,folded c_def]
    by simp
  finally show ?thesis by auto
qed  
  
lemma winding_number_comp_linear:
  assumes "c0" "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 c0 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 c0
      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 "ppath_image γ. Re p  Re z" and "valid_path γ" and  "zpath_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 "stpathstart g" and "fipathfinish g"
  have "valid_path g" "0path_image g" and pos_img:"ppath_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 0path_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 0path_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:"ppath_image γ. Im p  Im z" and "valid_path γ" and "zpath_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 zpath_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 zpath_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 γ zpath_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:"ppath_image γ. Im p  Im z" and "valid_path γ" and "zpath_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 zpath_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 zpath_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 γ zpath_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:"ppath_image γ. Re p  Re z" and "valid_path γ" and "zpath_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 zpath_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 zpath_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 γ zpath_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 {xS. f x  g x}"
proof (rule topological_space_class.openI)
  fix t
  assume "t  {xS. f x  g x}"
  then obtain U0 V0 where "open U0" "open V0" "f t  U0" "g t  V0" "U0  V0 = {}" "tS"
    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 tS ‹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 tS ‹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 tU1 tV1 tS by auto
  moreover have "T  {x  S. f x  g x}" unfolding T_def
    using U0  V0 = {} yS  U1. f y  U0 yS  V1. g y  V0 by auto
  ultimately show "T. open T  t  T  T  {x  S. f x  g x}" by auto
qed  
    
subsection ‹Sign at a filter›    
 
(*Relaxation in types could be done in the future.*)
definition has_sgnx::"(real  real)  real  real filter  bool" 
    (infixr "has'_sgnx" 55) where
  "(f has_sgnx c) F= (eventually (λx. sgn(f x) = c) F)"    
  
definition sgnx_able (infixr "sgnx'_able" 55) where
  "(f sgnx_able F) = (c. (f has_sgnx c) F)"
  
definition sgnx where
  "sgnx f F = (SOME c. (f has_sgnx c) F)"
  
lemma has_sgnx_eq_rhs: "(f has_sgnx x) F  x = y  (f has_sgnx y) F"
  by simp

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

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

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

lemma has_sgnx_unique:
  assumes "Fbot" "(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 Fbot  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  ts)  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. ts  a<t  t<x}" using assms(3) by auto
    moreover have "ls = {t. f t=0  a<t  t<x}  {t. ts  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 t0" 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 "tls" 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 "tls" using that t unfolding ls_def by auto
      then have "tMax 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  ts)  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. ts  x<t  t<b}" using assms(3) by auto
    moreover have "rs = {t. f t=0  x<t  t<b}  {t. ts  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 t0" 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 "trs" 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 "trs" using that t unfolding rs_def by auto
      then have "tMin 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<zzubpoly p z0" 
      using next_non_root_interval[OF False] by auto 
    have "z. a<zzubsgn(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" "zub" "sgn(poly p z)  sgn (poly p ub)" by auto
      moreover then have "poly p z0" "poly p ub0" "zub" 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] zub zub 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. lbzz<apoly p z0" 
      using last_non_root_interval[OF False] by auto 
    have "z. lbzz<asgn(poly p z) = sgn (poly p lb)"
    proof (rule ccontr)
      assume "¬ (z. lbzz<a  sgn (poly p z) = sgn (poly p lb))"
      then obtain z where "lbz" "z<a" "sgn(poly p z)  sgn (poly p lb)" by auto
      moreover then have "poly p z0" "poly p lb0" "zlb" 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] lbz zlb 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 "x0 ((λx. x) has_sgnx 1) (at_right x)" 
        "x0  ((λx. x) has_sgnx -1) (at_left x)"  
proof -
  show "x0  ((λ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 "x0  ((λ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 "Fbot" "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 Fbot› 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 "Fbot" "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 Fbot› 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" "c0"
  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 c0 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" "Fbot" "c0"
  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" "c0" 
  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 c0 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 c0
      apply (intro tendsto_intros)
      by (auto simp add:sgn_zero_iff)
    moreover have "c * sgn c >0" using c0 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 c0 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 c0 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 c0
      apply (intro tendsto_intros)
      by (auto simp add:sgn_zero_iff)
    moreover have "c * sgn c >0" using c0 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 c0 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 "p0"
  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 a0" 
  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 "q0" using p0 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  q0 by (auto simp add:order_power_n_n[of _ 1, simplified])
    moreover note less.hyps[OF ‹degree q < degree p q0]
    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 "p0"
  shows "(poly p has_sgnx c) (at_left a)  (if even (order a p) 
            then (poly p has_sgnx c) (at_right a)
            else (poly p has_sgnx -c) (at_right a))"
using poly_sgnx_left_right 
by (metis (no_types, hide_lams) add.inverse_inverse assms has_sgnx_unique 
     sgnx_able_poly sgnx_able_sgnx trivial_limit_at_left_real trivial_limit_at_right_real)    
    
    
lemma sign_r_pos_sgnx_iff:
  "sign_r_pos p a  sgnx (poly p) (at_right a) > 0"
proof 
  assume asm:"0 < sgnx (poly p) (at_right a)"
  obtain c where c_def:"(poly p has_sgnx c) (at_right a)"
    using sgnx_able_poly(1) sgnx_able_sgnx by blast
  then have "c>0" using asm 
    using has_sgnx_imp_sgnx trivial_limit_at_right_real by blast
  then show "sign_r_pos p a" using c_def unfolding sign_r_pos_def has_sgnx_def
    apply (elim eventually_mono)
    by force
next
  assume asm:"sign_r_pos p a"
  define c where "c = sgnx (poly p) (at_right a)"
  then have "(poly p has_sgnx c) (at_right a)" 
    by (simp add: sgnx_able_sgnx)
  then have "(F x in (at_right a). poly p x>0  sgn (poly p x) = c)"
    using asm unfolding has_sgnx_def sign_r_pos_def
    by (simp add:eventually_conj_iff)
  then have "F x in (at_right a). c > 0"
    apply (elim eventually_mono)
    by fastforce
  then show "c>0" by auto
qed

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

lemma has_sgnx_poly_at_bot:
    "(poly p has_sgnx  sgn_neg_inf p) at_bot"
  using has_sgnx_def poly_sgn_eventually_at_bot by blast
    
lemma sgnx_poly_at_top:
  "sgnx (poly p) at_top = sgn_pos_inf p"
by (simp add: has_sgnx_def has_sgnx_imp_sgnx poly_sgn_eventually_at_top)
    
lemma sgnx_poly_at_bot:
  "sgnx (poly p) at_bot = sgn_neg_inf p"
by (simp add: has_sgnx_def has_sgnx_imp_sgnx poly_sgn_eventually_at_bot)  
  
lemma poly_has_sgnx_values:
  assumes "p0"
  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 p0] 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 p0] 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 "p0"
  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 p0] 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 "c0" 
  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