src/HOL/Limits.thy

--- a/src/HOL/Limits.thy	Sun May 04 21:03:04 2025 +0100
+++ b/src/HOL/Limits.thy	Mon May 05 17:04:07 2025 +0100
@@ -26,6 +26,12 @@
   by (subst eventually_INF_base)
      (auto simp: subset_eq eventually_principal intro!: exI[of _ "max a b" for a b])
 
+lemma eventually_at_infinityI:
+  fixes P::"'a::real_normed_vector \<Rightarrow> bool"
+  assumes "\<And>x. c \<le> norm x \<Longrightarrow> P x"
+  shows "eventually P at_infinity"  
+unfolding eventually_at_infinity using assms by auto
+
 corollary eventually_at_infinity_pos:
   "eventually p at_infinity \<longleftrightarrow> (\<exists>b. 0 < b \<and> (\<forall>x. norm x \<ge> b \<longrightarrow> p x))"
   unfolding eventually_at_infinity
@@ -1550,7 +1556,34 @@
   for a :: real
   by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
 
-
+lemma filtermap_linear_at_within:
+  assumes "bij f" and cont: "isCont f a" and open_map: "\<And>S. open S \<Longrightarrow> 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 \<in> T" and impP:"\<forall>x\<in>T. x\<noteq>a \<longrightarrow> x\<in>S\<longrightarrow> 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 \<open>bij f\<close> open_map by (metis bij_pointE image_iff)  
+next
+  fix P
+  assume "eventually P (at (f a) within f ` S)"
+  then obtain T1 where "open T1" "f a \<in> T1" and impP:"\<forall>x\<in>T1. x\<noteq>f a \<longrightarrow> x\<in>f`S\<longrightarrow> P (x)"
+    unfolding eventually_at_topological by auto
+  then obtain T2 where "open T2" "a \<in> T2" "(\<forall>x'\<in>T2. f x' \<in> T1)"
+    using cont[unfolded continuous_at_open,rule_format,of T1] by blast 
+  then have "\<forall>x\<in>T2. x\<noteq>a \<longrightarrow> x\<in>S\<longrightarrow> 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>open T2\<close> \<open>a \<in> T2\<close> by auto
+qed
+  
 lemma filterlim_at_left_to_right:
   "filterlim f F (at_left a) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
   for a :: real
@@ -2015,6 +2048,32 @@
     by eventually_elim simp
 qed
 
+lemma filterlim_tendsto_add_at_top_iff:
+  assumes f: "(f \<longlongrightarrow> c) F"
+  shows "(LIM x F. (f x + g x :: real) :> at_top) \<longleftrightarrow> (LIM x F. g x :> at_top)"
+proof     
+  assume "LIM x F. f x + g x :> at_top" 
+  moreover have "((\<lambda>x. - f x) \<longlongrightarrow> - c) F"
+    by (simp add: f tendsto_minus)
+  ultimately show "filterlim g at_top F" 
+    using filterlim_tendsto_add_at_top  by fastforce
+qed (auto simp: filterlim_tendsto_add_at_top[OF f])    
+
+lemma filterlim_tendsto_add_at_bot_iff:
+  fixes c::real
+  assumes f: "(f \<longlongrightarrow> c) F"
+  shows "(LIM x F. f x + g x :> at_bot) \<longleftrightarrow> (LIM x F. g x :> at_bot)" 
+proof -
+  have "(LIM x F. f x + g x :> at_bot) 
+        \<longleftrightarrow>  (LIM x F. - f x + (- g x)  :> at_top)"
+    by (simp add: filterlim_uminus_at_bot)
+  also have "... = (LIM x F. - g x  :> at_top)"
+    by (metis f filterlim_tendsto_add_at_top_iff tendsto_minus)
+  also have "... = (LIM x F. g x  :> at_bot)"
+    by (simp add: filterlim_uminus_at_bot)
+  finally show ?thesis .
+qed
+
 lemma LIM_at_top_divide:
   fixes f g :: "'a \<Rightarrow> real"
   assumes f: "(f \<longlongrightarrow> a) F" "0 < a"