# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1676552064 0
# Node ID e20f5b9ad776211013a40184dad1a21f78ea9110
# Parent  c6b50597abbcb5275da3fb952f4947481657620d
Limit properties for complex exponential

diff -r c6b50597abbc -r e20f5b9ad776 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Thu Feb 16 12:21:21 2023 +0000
+++ b/src/HOL/Complex.thy	Thu Feb 16 12:54:24 2023 +0000
@@ -1001,6 +1001,21 @@
   "continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. cis (f x))"
   by (auto simp: cis_conv_exp intro!: continuous_intros)
 
+lemma tendsto_exp_0_Re_at_bot: "(exp \<longlongrightarrow> 0) (filtercomap Re at_bot)"
+proof -
+  have "((\<lambda>z. cmod (exp z)) \<longlongrightarrow> 0) (filtercomap Re at_bot)"
+    by (auto intro!: filterlim_filtercomapI exp_at_bot)
+  thus ?thesis
+    using tendsto_norm_zero_iff by blast
+qed
+
+lemma filterlim_exp_at_infinity_Re_at_top: "filterlim exp at_infinity (filtercomap Re at_top)"
+proof -
+  have "filterlim (\<lambda>z. norm (exp z)) at_top (filtercomap Re at_top)"
+    by (auto intro!: filterlim_filtercomapI exp_at_top)
+  thus ?thesis
+    using filterlim_norm_at_top_imp_at_infinity by blast
+qed
 
 subsubsection \<open>Complex argument\<close>