# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1674741591 0
# Node ID 780161d4b55c4199b767065af97e0e76791808bd
# Parent  e04536f7c5eab222f381e65204f8a50405c44ab3
Moved in some material from the AFP entry Winding_number_eval

diff -r e04536f7c5ea -r 780161d4b55c src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Wed Jan 25 22:00:21 2023 +0100
+++ b/src/HOL/Analysis/Analysis.thy	Thu Jan 26 13:59:51 2023 +0000
@@ -6,6 +6,7 @@
   (* Topology *)
   Connected
   Abstract_Limits
+  Isolated
   (* Functional Analysis *)
   Elementary_Normed_Spaces
   Norm_Arith
diff -r e04536f7c5ea -r 780161d4b55c src/HOL/Analysis/Isolated.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Isolated.thy	Thu Jan 26 13:59:51 2023 +0000
@@ -0,0 +1,215 @@
+theory Isolated
+  imports "HOL-Analysis.Elementary_Metric_Spaces"
+
+begin
+
+subsection \<open>Isolate and discrete\<close>  
+  
+definition (in topological_space) isolate:: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infixr "isolate" 60)
+  where "x isolate S \<longleftrightarrow> (x\<in>S \<and> (\<exists>T. open T \<and> T \<inter> S = {x}))"  
+    
+definition (in topological_space) discrete:: "'a set \<Rightarrow> bool" 
+  where "discrete S \<longleftrightarrow> (\<forall>x\<in>S. x isolate S)"  
+    
+definition (in metric_space) uniform_discrete :: "'a set \<Rightarrow> bool" where
+  "uniform_discrete S \<longleftrightarrow> (\<exists>e>0. \<forall>x\<in>S. \<forall>y\<in>S. dist x y < e \<longrightarrow> x = y)"
+  
+lemma uniformI1:
+  assumes "e>0" "\<And>x y. \<lbrakk>x\<in>S;y\<in>S;dist x y<e\<rbrakk> \<Longrightarrow> x =y "
+  shows "uniform_discrete S"  
+unfolding uniform_discrete_def using assms by auto
+
+lemma uniformI2:
+  assumes "e>0" "\<And>x y. \<lbrakk>x\<in>S;y\<in>S;x\<noteq>y\<rbrakk> \<Longrightarrow> dist x y\<ge>e "
+  shows "uniform_discrete S"  
+unfolding uniform_discrete_def using assms not_less by blast
+  
+lemma isolate_islimpt_iff:"(x isolate S) \<longleftrightarrow> (\<not> (x islimpt S) \<and> x\<in>S)"
+  unfolding isolate_def islimpt_def by auto
+  
+lemma isolate_dist_Ex_iff:
+  fixes x::"'a::metric_space"
+  shows "x isolate S \<longleftrightarrow> (x\<in>S \<and> (\<exists>e>0. \<forall>y\<in>S. dist x y < e \<longrightarrow> 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) \<longleftrightarrow> x isolate S \<or> (x=a \<and> \<not> (x islimpt S))"
+by (meson insert_iff islimpt_insert isolate_islimpt_iff)
+    
+(*
+TODO. 
+Other than 
+
+  uniform_discrete S \<longrightarrow> discrete S
+  uniform_discrete S \<longrightarrow> closed S
+
+, we should be able to prove
+
+  discrete S \<and> closed S \<longrightarrow> 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 \<Longrightarrow> closed S" 
+  by (meson discrete_imp_closed uniform_discrete_def) 
+    
+lemma uniform_discrete_imp_discrete:
+  "uniform_discrete S \<Longrightarrow> discrete S"
+  by (metis discrete_def isolate_dist_Ex_iff uniform_discrete_def)
+  
+lemma isolate_subset:"x isolate S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> x\<in>T \<Longrightarrow> x isolate T"
+  unfolding isolate_def by fastforce
+
+lemma discrete_subset[elim]: "discrete S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> discrete T"
+  unfolding discrete_def using islimpt_subset isolate_islimpt_iff by blast
+    
+lemma uniform_discrete_subset[elim]: "uniform_discrete S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> uniform_discrete T"
+  by (meson subsetD uniform_discrete_def)
+        
+lemma continuous_on_discrete: "discrete S \<Longrightarrow> continuous_on S f" 
+  unfolding continuous_on_topological by (metis discrete_def islimptI isolate_islimpt_iff)
+   
+lemma uniform_discrete_insert: "uniform_discrete (insert a S) \<longleftrightarrow> uniform_discrete S"
+proof 
+  assume asm:"uniform_discrete S" 
+  let ?thesis = "uniform_discrete (insert a S)"
+  have ?thesis when "a\<in>S" using that asm by (simp add: insert_absorb)
+  moreover have ?thesis when "S={}" using that asm by (simp add: uniform_discrete_def)
+  moreover have ?thesis when "a\<notin>S" "S\<noteq>{}"
+  proof -
+    obtain e1 where "e1>0" and e1_dist:"\<forall>x\<in>S. \<forall>y\<in>S. dist y x < e1 \<longrightarrow> y = x"
+      using asm unfolding uniform_discrete_def by auto
+    define e2 where "e2 \<equiv> min (setdist {a} S) e1"
+    have "closed S" using asm uniform_discrete_imp_closed by auto
+    then have "e2>0"
+      by (smt (verit) \<open>0 < e1\<close> e2_def infdist_eq_setdist infdist_pos_not_in_closed that)
+    moreover have "x = y" when "x\<in>insert a S" "y\<in>insert a S" "dist x y < e2 " for x y
+    proof -
+      have ?thesis when "x=a" "y=a" using that by auto
+      moreover have ?thesis when "x=a" "y\<in>S"
+        using that setdist_le_dist[of x "{a}" y S] \<open>dist x y < e2\<close> unfolding e2_def
+        by fastforce
+      moreover have ?thesis when "y=a" "x\<in>S"
+        using that setdist_le_dist[of y "{a}" x S] \<open>dist x y < e2\<close> unfolding e2_def
+        by (simp add: dist_commute)
+      moreover have ?thesis when "x\<in>S" "y\<in>S"
+        using e1_dist[rule_format, OF that] \<open>dist x y < e2\<close> 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 \<and> compact S \<longleftrightarrow> 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 \<open>finite S\<close>] by auto 
+  ultimately show "discrete S \<and> compact S" by auto
+next
+  assume "discrete S \<and> 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 \<and> bounded S \<longleftrightarrow> finite S"
+proof 
+  assume "uniform_discrete S \<and> 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 \<and> bounded S"
+  have ?thesis when "S={}" using that by auto
+  moreover have ?thesis when "S\<noteq>{}"
+  proof -
+    have "\<forall>x. \<exists>d>0. \<forall>y\<in>S. y \<noteq> x \<longrightarrow> d \<le> dist x y"
+      using finite_set_avoid[OF \<open>finite S\<close>] by auto
+    then obtain f where f_pos:"f x>0" 
+        and f_dist: "\<forall>y\<in>S. y \<noteq> x \<longrightarrow> f x \<le> dist x y"
+        if "x\<in>S" for x 
+      by metis
+    define f_min where "f_min \<equiv> Min (f ` S)" 
+    have "f_min > 0"
+      unfolding f_min_def 
+      by (simp add: asm f_pos that)
+    moreover have "\<forall>x\<in>S. \<forall>y\<in>S. f_min > dist x y \<longrightarrow> 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 \<open>finite S\<close> by auto
+    ultimately show ?thesis by auto
+  qed
+  ultimately show ?thesis by blast
+qed
+  
+lemma uniform_discrete_image_scale:
+  assumes "uniform_discrete S" and dist:"\<forall>x\<in>S. \<forall>y\<in>S. dist x y = c * dist (f x) (f y)"
+  shows "uniform_discrete (f ` S)"  
+proof -
+  have ?thesis when "S={}" using that by auto
+  moreover have ?thesis when "S\<noteq>{}" "c\<le>0"
+  proof -
+    obtain x1 where "x1\<in>S" using \<open>S\<noteq>{}\<close> by auto
+    have ?thesis when "S-{x1} = {}"
+    proof -
+      have "S={x1}" using that \<open>S\<noteq>{}\<close> by auto
+      then show ?thesis using uniform_discrete_insert[of "f x1"] by auto
+    qed
+    moreover have ?thesis when "S-{x1} \<noteq> {}"
+    proof -
+      obtain x2 where "x2\<in>S-{x1}" using \<open>S-{x1} \<noteq> {}\<close> by auto
+      then have "x2\<in>S" "x1\<noteq>x2" by auto
+      then have "dist x1 x2 > 0" by auto
+      moreover have "dist x1 x2 = c * dist (f x1) (f x2)"
+        using dist[rule_format, OF \<open>x1\<in>S\<close> \<open>x2\<in>S\<close>] .
+      moreover have "dist (f x2) (f x2) \<ge> 0" by auto
+      ultimately have False using \<open>c\<le>0\<close> by (simp add: zero_less_mult_iff)
+      then show ?thesis by auto
+    qed
+    ultimately show ?thesis by auto
+  qed
+  moreover have ?thesis when "S\<noteq>{}" "c>0"
+  proof -
+    obtain e1 where "e1>0" and e1_dist:"\<forall>x\<in>S. \<forall>y\<in>S. dist y x < e1 \<longrightarrow> y = x"
+      using \<open>uniform_discrete S\<close> unfolding uniform_discrete_def by auto
+    define e where "e= e1/c"
+    have "x1 = x2" when "x1\<in> f ` S" "x2\<in> f ` S" "dist x1 x2 < e " for x1 x2 
+    proof -
+      obtain y1 where y1:"y1\<in>S" "x1=f y1" using \<open>x1\<in> f ` S\<close> by auto
+      obtain y2 where y2:"y2\<in>S" "x2=f y2" using \<open>x2\<in> f ` S\<close> by auto    
+      have "dist y1 y2 < e1"
+        by (smt (verit) \<open>0 < c\<close> dist divide_right_mono e_def nonzero_mult_div_cancel_left that(3) y1 y2)
+      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 \<open>e1>0\<close> \<open>c>0\<close> unfolding e_def by auto
+    ultimately show ?thesis unfolding uniform_discrete_def by meson
+  qed
+  ultimately show ?thesis by fastforce
+qed
+ 
+end
diff -r e04536f7c5ea -r 780161d4b55c src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Wed Jan 25 22:00:21 2023 +0100
+++ b/src/HOL/Limits.thy	Thu Jan 26 13:59:51 2023 +0000
@@ -11,15 +11,6 @@
   imports Real_Vector_Spaces
 begin
 
-text \<open>Lemmas related to shifting/scaling\<close>
-lemma range_add [simp]:
-  fixes a::"'a::group_add" shows "range ((+) a) = UNIV"
-  by simp
-
-lemma range_diff [simp]:
-  fixes a::"'a::group_add" shows "range ((-) a) = UNIV"
-  by (metis (full_types) add_minus_cancel diff_minus_eq_add surj_def)
-
 lemma range_mult [simp]:
   fixes a::"real" shows "range ((*) a) = (if a=0 then {0} else UNIV)"
   by (simp add: surj_def) (meson dvdE dvd_field_iff)
@@ -2533,6 +2524,147 @@
     by (metis B abs_le_iff add.inverse_inverse neg_le_iff_le)
 qed
 
+subsection \<open>More about @{term filterlim} (thanks to Wenda Li)\<close>
+
+lemma filterlim_at_infinity_times:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_field"
+  assumes "filterlim f at_infinity F" "filterlim g at_infinity F"
+  shows "filterlim (\<lambda>x. f x * g x) at_infinity F"  
+proof -
+  have "((\<lambda>x. inverse (f x) * inverse (g x)) \<longlongrightarrow> 0 * 0) F"
+    by (intro tendsto_mult tendsto_inverse assms filterlim_compose[OF tendsto_inverse_0])
+  then have "filterlim (\<lambda>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 \<Rightarrow> 'b::unbounded_dense_linorder" and F::"'a filter"
+  assumes top:"filterlim f at_top F" and bot: "filterlim f at_bot F" and "F\<noteq>bot"
+  shows False
+proof -
+  obtain c::'b where True by auto
+  have "\<forall>\<^sub>F x in F. c < f x" 
+    using top unfolding filterlim_at_top_dense by auto
+  moreover have "\<forall>\<^sub>F x in F. f x < c" 
+    using bot unfolding filterlim_at_bot_dense by auto
+  ultimately have "\<forall>\<^sub>F x in F. c < f x \<and> f x < c" 
+    using eventually_conj by auto
+  then have "\<forall>\<^sub>F x in F. False" by (auto elim:eventually_mono)
+  then show False using \<open>F\<noteq>bot\<close> by auto
+qed  
+
+lemma filterlim_at_top_nhds[elim]:      
+  fixes f::"'a \<Rightarrow> 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter"
+  assumes top:"filterlim f at_top F" and tendsto: "(f \<longlongrightarrow> c) F" and "F\<noteq>bot"
+  shows False
+proof -
+  obtain c'::'b where "c'>c" using gt_ex by blast
+  have "\<forall>\<^sub>F x in F. c' < f x" 
+    using top unfolding filterlim_at_top_dense by auto
+  moreover have "\<forall>\<^sub>F x in F. f x < c'" 
+    using order_tendstoD[OF tendsto,of c'] \<open>c'>c\<close> by auto
+  ultimately have "\<forall>\<^sub>F x in F. c' < f x \<and> f x < c'" 
+    using eventually_conj by auto
+  then have "\<forall>\<^sub>F x in F. False" by (auto elim:eventually_mono)
+  then show False using \<open>F\<noteq>bot\<close> by auto
+qed
+
+lemma filterlim_at_bot_nhds[elim]:      
+  fixes f::"'a \<Rightarrow> 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter"
+  assumes top:"filterlim f at_bot F" and tendsto: "(f \<longlongrightarrow> c) F" and "F\<noteq>bot"
+  shows False
+proof -
+  obtain c'::'b where "c'<c" using lt_ex by blast
+  have "\<forall>\<^sub>F x in F. c' > f x" 
+    using top unfolding filterlim_at_bot_dense by auto
+  moreover have "\<forall>\<^sub>F x in F. f x > c'" 
+    using order_tendstoD[OF tendsto,of c'] \<open>c'<c\<close> by auto
+  ultimately have "\<forall>\<^sub>F x in F. c' < f x \<and> f x < c'" 
+    using eventually_conj by auto
+  then have "\<forall>\<^sub>F x in F. False" by (auto elim:eventually_mono)
+  then show False using \<open>F\<noteq>bot\<close> by auto
+qed  
+
+lemma eventually_times_inverse_1:
+  fixes f::"'a \<Rightarrow> 'b::{field,t2_space}"
+  assumes "(f \<longlongrightarrow> c) F" "c\<noteq>0"
+  shows "\<forall>\<^sub>F x in F. inverse (f x) * f x = 1"
+  by (smt (verit) assms eventually_mono mult.commute right_inverse tendsto_imp_eventually_ne)
+  
+lemma filterlim_at_infinity_divide_iff:
+  fixes f::"'a \<Rightarrow> 'b::real_normed_field"
+  assumes "(f \<longlongrightarrow> c) F" "c\<noteq>0"
+  shows "(LIM x F. f x / g x :> at_infinity) \<longleftrightarrow> (LIM x F. g x :> at 0)"
+proof 
+  assume "LIM x F. f x / g x :> at_infinity"
+  then have "LIM x F. inverse (f x) * (f x / g x) :> at_infinity"
+    using assms tendsto_inverse tendsto_mult_filterlim_at_infinity by fastforce
+  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 (\<lambda>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 "\<lambda>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 \<Rightarrow> real"
+  assumes "(f \<longlongrightarrow> c) F" and "0 < c"
+  shows "(LIM x F. (f x * g x) :> at_top) \<longleftrightarrow> (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 "((\<lambda>x. inverse (f x)) \<longlongrightarrow> inverse c) F" 
+    using tendsto_inverse[OF assms(1)] \<open>0<c\<close> 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 "\<lambda>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)] \<open>c>0\<close> eventually_mono by fastforce
+qed  
+
+lemma filterlim_tendsto_pos_mult_at_bot_iff:
+  fixes c :: real
+  assumes "(f \<longlongrightarrow> c) F" "0 < c" 
+  shows "(LIM x F. f x * g x :> at_bot) \<longleftrightarrow> filterlim g at_bot F"
+  using filterlim_tendsto_pos_mult_at_top_iff[OF assms(1,2), of "\<lambda>x. - g x"] 
+  unfolding filterlim_uminus_at_bot by simp    
+
+lemma filterlim_tendsto_neg_mult_at_top_iff:
+  fixes f::"'a \<Rightarrow> real"
+  assumes "(f \<longlongrightarrow> c) F" and "c < 0"
+  shows "(LIM x F. (f x * g x) :> at_top) \<longleftrightarrow> (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 "\<lambda>x. - f x" "-c" F "\<lambda>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 \<longlongrightarrow> c) F" "0 > c" 
+  shows "(LIM x F. f x * g x :> at_bot) \<longleftrightarrow> filterlim g at_top F"
+  using filterlim_tendsto_neg_mult_at_top_iff[OF assms(1,2), of "\<lambda>x. - g x"] 
+  unfolding filterlim_uminus_at_top by simp    
+
 subsection \<open>Power Sequences\<close>
 
 lemma Bseq_realpow: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> Bseq (\<lambda>n. x ^ n)"