src/HOL/Limits.thy
changeset 44194 0639898074ae
parent 44081 730f7cced3a6
child 44195 f5363511b212
     1.1 --- a/src/HOL/Limits.thy	Sat Aug 13 18:10:14 2011 -0700
     1.2 +++ b/src/HOL/Limits.thy	Sun Aug 14 07:54:24 2011 -0700
     1.3 @@ -623,6 +623,8 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +subsubsection {* Norms *}
     1.8 +
     1.9  lemma norm_conv_dist: "norm x = dist x 0"
    1.10    unfolding dist_norm by simp
    1.11  
    1.12 @@ -642,11 +644,34 @@
    1.13    "((\<lambda>x. norm (f x)) ---> 0) A \<longleftrightarrow> (f ---> 0) A"
    1.14    unfolding tendsto_iff dist_norm by simp
    1.15  
    1.16 +lemma tendsto_rabs [tendsto_intros]:
    1.17 +  "(f ---> (l::real)) A \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> \<bar>l\<bar>) A"
    1.18 +  by (fold real_norm_def, rule tendsto_norm)
    1.19 +
    1.20 +lemma tendsto_rabs_zero:
    1.21 +  "(f ---> (0::real)) A \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> 0) A"
    1.22 +  by (fold real_norm_def, rule tendsto_norm_zero)
    1.23 +
    1.24 +lemma tendsto_rabs_zero_cancel:
    1.25 +  "((\<lambda>x. \<bar>f x\<bar>) ---> (0::real)) A \<Longrightarrow> (f ---> 0) A"
    1.26 +  by (fold real_norm_def, rule tendsto_norm_zero_cancel)
    1.27 +
    1.28 +lemma tendsto_rabs_zero_iff:
    1.29 +  "((\<lambda>x. \<bar>f x\<bar>) ---> (0::real)) A \<longleftrightarrow> (f ---> 0) A"
    1.30 +  by (fold real_norm_def, rule tendsto_norm_zero_iff)
    1.31 +
    1.32 +subsubsection {* Addition and subtraction *}
    1.33 +
    1.34  lemma tendsto_add [tendsto_intros]:
    1.35    fixes a b :: "'a::real_normed_vector"
    1.36    shows "\<lbrakk>(f ---> a) A; (g ---> b) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) A"
    1.37    by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
    1.38  
    1.39 +lemma tendsto_add_zero:
    1.40 +  fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
    1.41 +  shows "\<lbrakk>(f ---> 0) A; (g ---> 0) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> 0) A"
    1.42 +  by (drule (1) tendsto_add, simp)
    1.43 +
    1.44  lemma tendsto_minus [tendsto_intros]:
    1.45    fixes a :: "'a::real_normed_vector"
    1.46    shows "(f ---> a) A \<Longrightarrow> ((\<lambda>x. - f x) ---> - a) A"
    1.47 @@ -668,29 +693,61 @@
    1.48    shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) A"
    1.49  proof (cases "finite S")
    1.50    assume "finite S" thus ?thesis using assms
    1.51 -  proof (induct set: finite)
    1.52 -    case empty show ?case
    1.53 -      by (simp add: tendsto_const)
    1.54 -  next
    1.55 -    case (insert i F) thus ?case
    1.56 -      by (simp add: tendsto_add)
    1.57 -  qed
    1.58 +    by (induct, simp add: tendsto_const, simp add: tendsto_add)
    1.59  next
    1.60    assume "\<not> finite S" thus ?thesis
    1.61      by (simp add: tendsto_const)
    1.62  qed
    1.63  
    1.64 +subsubsection {* Linear operators and multiplication *}
    1.65 +
    1.66  lemma (in bounded_linear) tendsto [tendsto_intros]:
    1.67    "(g ---> a) A \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) A"
    1.68    by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
    1.69  
    1.70 +lemma (in bounded_linear) tendsto_zero:
    1.71 +  "(g ---> 0) A \<Longrightarrow> ((\<lambda>x. f (g x)) ---> 0) A"
    1.72 +  by (drule tendsto, simp only: zero)
    1.73 +
    1.74  lemma (in bounded_bilinear) tendsto [tendsto_intros]:
    1.75    "\<lbrakk>(f ---> a) A; (g ---> b) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) A"
    1.76    by (simp only: tendsto_Zfun_iff prod_diff_prod
    1.77                   Zfun_add Zfun Zfun_left Zfun_right)
    1.78  
    1.79 +lemma (in bounded_bilinear) tendsto_zero:
    1.80 +  assumes f: "(f ---> 0) A"
    1.81 +  assumes g: "(g ---> 0) A"
    1.82 +  shows "((\<lambda>x. f x ** g x) ---> 0) A"
    1.83 +  using tendsto [OF f g] by (simp add: zero_left)
    1.84  
    1.85 -subsection {* Continuity of Inverse *}
    1.86 +lemma (in bounded_bilinear) tendsto_left_zero:
    1.87 +  "(f ---> 0) A \<Longrightarrow> ((\<lambda>x. f x ** c) ---> 0) A"
    1.88 +  by (rule bounded_linear.tendsto_zero [OF bounded_linear_left])
    1.89 +
    1.90 +lemma (in bounded_bilinear) tendsto_right_zero:
    1.91 +  "(f ---> 0) A \<Longrightarrow> ((\<lambda>x. c ** f x) ---> 0) A"
    1.92 +  by (rule bounded_linear.tendsto_zero [OF bounded_linear_right])
    1.93 +
    1.94 +lemmas tendsto_mult = mult.tendsto
    1.95 +
    1.96 +lemma tendsto_power [tendsto_intros]:
    1.97 +  fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
    1.98 +  shows "(f ---> a) A \<Longrightarrow> ((\<lambda>x. f x ^ n) ---> a ^ n) A"
    1.99 +  by (induct n) (simp_all add: tendsto_const tendsto_mult)
   1.100 +
   1.101 +lemma tendsto_setprod [tendsto_intros]:
   1.102 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
   1.103 +  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> L i) A"
   1.104 +  shows "((\<lambda>x. \<Prod>i\<in>S. f i x) ---> (\<Prod>i\<in>S. L i)) A"
   1.105 +proof (cases "finite S")
   1.106 +  assume "finite S" thus ?thesis using assms
   1.107 +    by (induct, simp add: tendsto_const, simp add: tendsto_mult)
   1.108 +next
   1.109 +  assume "\<not> finite S" thus ?thesis
   1.110 +    by (simp add: tendsto_const)
   1.111 +qed
   1.112 +
   1.113 +subsubsection {* Inverse and division *}
   1.114  
   1.115  lemma (in bounded_bilinear) Zfun_prod_Bfun:
   1.116    assumes f: "Zfun f A"
   1.117 @@ -815,6 +872,13 @@
   1.118      \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) A"
   1.119    by (simp add: mult.tendsto tendsto_inverse divide_inverse)
   1.120  
   1.121 +lemma tendsto_sgn [tendsto_intros]:
   1.122 +  fixes l :: "'a::real_normed_vector"
   1.123 +  shows "\<lbrakk>(f ---> l) A; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) A"
   1.124 +  unfolding sgn_div_norm by (simp add: tendsto_intros)
   1.125 +
   1.126 +subsubsection {* Uniqueness *}
   1.127 +
   1.128  lemma tendsto_unique:
   1.129    fixes f :: "'a \<Rightarrow> 'b::t2_space"
   1.130    assumes "\<not> trivial_limit A"  "(f ---> l) A"  "(f ---> l') A"