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