author paulson Wed, 09 Oct 2019 15:32:41 +0100 changeset 70994 4eef7c6ef7bf parent 70993 2d658afa1fc0 child 70995 c39bd607203b
More theorems about limits, including cancellation simprules
 src/HOL/Analysis/Cauchy_Integral_Theorem.thy file | annotate | diff | comparison | revisions src/HOL/Limits.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Oct 09 14:39:10 2019 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Oct 09 15:32:41 2019 +0100
@@ -6632,7 +6632,7 @@
by (rule tendsto_mult_left [OF tendstoI])
then have "((\<lambda>u. g u / (u - w)) has_contour_integral 2 * of_real pi * \<i> * g w) (circlepath z r)"
using has_contour_integral_integral [OF g_cint] tendsto_unique [OF F f_tends_cig] w
-      by (force simp: dist_norm)
+      by fastforce
then have "((\<lambda>u. g u / (2 * of_real pi * \<i> * (u - w))) has_contour_integral g w) (circlepath z r)"
using has_contour_integral_div [where c = "2 * of_real pi * \<i>"]
by (force simp: field_simps)```
```--- a/src/HOL/Limits.thy	Wed Oct 09 14:39:10 2019 +0100
+++ b/src/HOL/Limits.thy	Wed Oct 09 15:32:41 2019 +0100
@@ -779,14 +779,26 @@
for c :: "'a::topological_semigroup_mult"
by (rule tendsto_mult [OF _ tendsto_const])

-lemma tendsto_mult_left_iff:
+lemma tendsto_mult_left_iff [simp]:
"c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. c * f x) (c * l) F \<longleftrightarrow> tendsto f l F" for c :: "'a::{topological_semigroup_mult,field}"
by (auto simp: tendsto_mult_left dest: tendsto_mult_left [where c = "1/c"])

-lemma tendsto_mult_right_iff:
+lemma tendsto_mult_right_iff [simp]:
"c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. f x * c) (l * c) F \<longleftrightarrow> tendsto f l F" for c :: "'a::{topological_semigroup_mult,field}"
by (auto simp: tendsto_mult_right dest: tendsto_mult_left [where c = "1/c"])

+lemma tendsto_zero_mult_left_iff [simp]:
+  fixes c::"'a::{topological_semigroup_mult,field}" assumes "c \<noteq> 0" shows "(\<lambda>n. c * a n)\<longlonglongrightarrow> 0 \<longleftrightarrow> a \<longlonglongrightarrow> 0"
+  using assms tendsto_mult_left tendsto_mult_left_iff by fastforce
+
+lemma tendsto_zero_mult_right_iff [simp]:
+  fixes c::"'a::{topological_semigroup_mult,field}" assumes "c \<noteq> 0" shows "(\<lambda>n. a n * c)\<longlonglongrightarrow> 0 \<longleftrightarrow> a \<longlonglongrightarrow> 0"
+  using assms tendsto_mult_right tendsto_mult_right_iff by fastforce
+
+lemma tendsto_zero_divide_iff [simp]:
+  fixes c::"'a::{topological_semigroup_mult,field}" assumes "c \<noteq> 0" shows "(\<lambda>n. a n / c)\<longlonglongrightarrow> 0 \<longleftrightarrow> a \<longlonglongrightarrow> 0"
+  using tendsto_zero_mult_right_iff [of "1/c" a] assms by (simp add: field_simps)
+
lemma lim_const_over_n [tendsto_intros]:
fixes a :: "'a::real_normed_field"
shows "(\<lambda>n. a / of_nat n) \<longlonglongrightarrow> 0"```