src/HOL/Limits.thy
changeset 51478 270b21f3ae0a
parent 51474 1e9e68247ad1
child 51524 7cb5ac44ca9e
     1.1 --- a/src/HOL/Limits.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Limits.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -236,6 +236,14 @@
     1.4    "(f ---> a) F \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) F"
     1.5    unfolding norm_conv_dist by (intro tendsto_intros)
     1.6  
     1.7 +lemma continuous_norm [continuous_intros]:
     1.8 +  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
     1.9 +  unfolding continuous_def by (rule tendsto_norm)
    1.10 +
    1.11 +lemma continuous_on_norm [continuous_on_intros]:
    1.12 +  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))"
    1.13 +  unfolding continuous_on_def by (auto intro: tendsto_norm)
    1.14 +
    1.15  lemma tendsto_norm_zero:
    1.16    "(f ---> 0) F \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> 0) F"
    1.17    by (drule tendsto_norm, simp)
    1.18 @@ -252,6 +260,14 @@
    1.19    "(f ---> (l::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> \<bar>l\<bar>) F"
    1.20    by (fold real_norm_def, rule tendsto_norm)
    1.21  
    1.22 +lemma continuous_rabs [continuous_intros]:
    1.23 +  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. \<bar>f x :: real\<bar>)"
    1.24 +  unfolding real_norm_def[symmetric] by (rule continuous_norm)
    1.25 +
    1.26 +lemma continuous_on_rabs [continuous_on_intros]:
    1.27 +  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. \<bar>f x :: real\<bar>)"
    1.28 +  unfolding real_norm_def[symmetric] by (rule continuous_on_norm)
    1.29 +
    1.30  lemma tendsto_rabs_zero:
    1.31    "(f ---> (0::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> 0) F"
    1.32    by (fold real_norm_def, rule tendsto_norm_zero)
    1.33 @@ -271,8 +287,18 @@
    1.34    shows "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) F"
    1.35    by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
    1.36  
    1.37 +lemma continuous_add [continuous_intros]:
    1.38 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    1.39 +  shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
    1.40 +  unfolding continuous_def by (rule tendsto_add)
    1.41 +
    1.42 +lemma continuous_on_add [continuous_on_intros]:
    1.43 +  fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
    1.44 +  shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
    1.45 +  unfolding continuous_on_def by (auto intro: tendsto_add)
    1.46 +
    1.47  lemma tendsto_add_zero:
    1.48 -  fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
    1.49 +  fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
    1.50    shows "\<lbrakk>(f ---> 0) F; (g ---> 0) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> 0) F"
    1.51    by (drule (1) tendsto_add, simp)
    1.52  
    1.53 @@ -281,6 +307,16 @@
    1.54    shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. - f x) ---> - a) F"
    1.55    by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus)
    1.56  
    1.57 +lemma continuous_minus [continuous_intros]:
    1.58 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    1.59 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)"
    1.60 +  unfolding continuous_def by (rule tendsto_minus)
    1.61 +
    1.62 +lemma continuous_on_minus [continuous_on_intros]:
    1.63 +  fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
    1.64 +  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
    1.65 +  unfolding continuous_on_def by (auto intro: tendsto_minus)
    1.66 +
    1.67  lemma tendsto_minus_cancel:
    1.68    fixes a :: "'a::real_normed_vector"
    1.69    shows "((\<lambda>x. - f x) ---> - a) F \<Longrightarrow> (f ---> a) F"
    1.70 @@ -296,6 +332,16 @@
    1.71    shows "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) F"
    1.72    by (simp add: diff_minus tendsto_add tendsto_minus)
    1.73  
    1.74 +lemma continuous_diff [continuous_intros]:
    1.75 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    1.76 +  shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x - g x)"
    1.77 +  unfolding continuous_def by (rule tendsto_diff)
    1.78 +
    1.79 +lemma continuous_on_diff [continuous_on_intros]:
    1.80 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    1.81 +  shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
    1.82 +  unfolding continuous_on_def by (auto intro: tendsto_diff)
    1.83 +
    1.84  lemma tendsto_setsum [tendsto_intros]:
    1.85    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
    1.86    assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> a i) F"
    1.87 @@ -308,6 +354,16 @@
    1.88      by (simp add: tendsto_const)
    1.89  qed
    1.90  
    1.91 +lemma continuous_setsum [continuous_intros]:
    1.92 +  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
    1.93 +  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>S. f i x)"
    1.94 +  unfolding continuous_def by (rule tendsto_setsum)
    1.95 +
    1.96 +lemma continuous_on_setsum [continuous_intros]:
    1.97 +  fixes f :: "'a \<Rightarrow> _ \<Rightarrow> 'c::real_normed_vector"
    1.98 +  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Sum>i\<in>S. f i x)"
    1.99 +  unfolding continuous_on_def by (auto intro: tendsto_setsum)
   1.100 +
   1.101  lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
   1.102  
   1.103  subsubsection {* Linear operators and multiplication *}
   1.104 @@ -316,6 +372,14 @@
   1.105    "(g ---> a) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) F"
   1.106    by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
   1.107  
   1.108 +lemma (in bounded_linear) continuous:
   1.109 +  "continuous F g \<Longrightarrow> continuous F (\<lambda>x. f (g x))"
   1.110 +  using tendsto[of g _ F] by (auto simp: continuous_def)
   1.111 +
   1.112 +lemma (in bounded_linear) continuous_on:
   1.113 +  "continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))"
   1.114 +  using tendsto[of g] by (auto simp: continuous_on_def)
   1.115 +
   1.116  lemma (in bounded_linear) tendsto_zero:
   1.117    "(g ---> 0) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> 0) F"
   1.118    by (drule tendsto, simp only: zero)
   1.119 @@ -325,6 +389,14 @@
   1.120    by (simp only: tendsto_Zfun_iff prod_diff_prod
   1.121                   Zfun_add Zfun Zfun_left Zfun_right)
   1.122  
   1.123 +lemma (in bounded_bilinear) continuous:
   1.124 +  "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x ** g x)"
   1.125 +  using tendsto[of f _ F g] by (auto simp: continuous_def)
   1.126 +
   1.127 +lemma (in bounded_bilinear) continuous_on:
   1.128 +  "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x ** g x)"
   1.129 +  using tendsto[of f _ _ g] by (auto simp: continuous_on_def)
   1.130 +
   1.131  lemma (in bounded_bilinear) tendsto_zero:
   1.132    assumes f: "(f ---> 0) F"
   1.133    assumes g: "(g ---> 0) F"
   1.134 @@ -348,6 +420,24 @@
   1.135  lemmas tendsto_mult [tendsto_intros] =
   1.136    bounded_bilinear.tendsto [OF bounded_bilinear_mult]
   1.137  
   1.138 +lemmas continuous_of_real [continuous_intros] =
   1.139 +  bounded_linear.continuous [OF bounded_linear_of_real]
   1.140 +
   1.141 +lemmas continuous_scaleR [continuous_intros] =
   1.142 +  bounded_bilinear.continuous [OF bounded_bilinear_scaleR]
   1.143 +
   1.144 +lemmas continuous_mult [continuous_intros] =
   1.145 +  bounded_bilinear.continuous [OF bounded_bilinear_mult]
   1.146 +
   1.147 +lemmas continuous_on_of_real [continuous_on_intros] =
   1.148 +  bounded_linear.continuous_on [OF bounded_linear_of_real]
   1.149 +
   1.150 +lemmas continuous_on_scaleR [continuous_on_intros] =
   1.151 +  bounded_bilinear.continuous_on [OF bounded_bilinear_scaleR]
   1.152 +
   1.153 +lemmas continuous_on_mult [continuous_on_intros] =
   1.154 +  bounded_bilinear.continuous_on [OF bounded_bilinear_mult]
   1.155 +
   1.156  lemmas tendsto_mult_zero =
   1.157    bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult]
   1.158  
   1.159 @@ -362,6 +452,16 @@
   1.160    shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) ---> a ^ n) F"
   1.161    by (induct n) (simp_all add: tendsto_const tendsto_mult)
   1.162  
   1.163 +lemma continuous_power [continuous_intros]:
   1.164 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   1.165 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x)^n)"
   1.166 +  unfolding continuous_def by (rule tendsto_power)
   1.167 +
   1.168 +lemma continuous_on_power [continuous_on_intros]:
   1.169 +  fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}"
   1.170 +  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. (f x)^n)"
   1.171 +  unfolding continuous_on_def by (auto intro: tendsto_power)
   1.172 +
   1.173  lemma tendsto_setprod [tendsto_intros]:
   1.174    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
   1.175    assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> L i) F"
   1.176 @@ -374,6 +474,16 @@
   1.177      by (simp add: tendsto_const)
   1.178  qed
   1.179  
   1.180 +lemma continuous_setprod [continuous_intros]:
   1.181 +  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
   1.182 +  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Prod>i\<in>S. f i x)"
   1.183 +  unfolding continuous_def by (rule tendsto_setprod)
   1.184 +
   1.185 +lemma continuous_on_setprod [continuous_intros]:
   1.186 +  fixes f :: "'a \<Rightarrow> _ \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
   1.187 +  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Prod>i\<in>S. f i x)"
   1.188 +  unfolding continuous_on_def by (auto intro: tendsto_setprod)
   1.189 +
   1.190  subsubsection {* Inverse and division *}
   1.191  
   1.192  lemma (in bounded_bilinear) Zfun_prod_Bfun:
   1.193 @@ -483,17 +593,89 @@
   1.194      unfolding tendsto_Zfun_iff by (rule Zfun_ssubst)
   1.195  qed
   1.196  
   1.197 +lemma continuous_inverse:
   1.198 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
   1.199 +  assumes "continuous F f" and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
   1.200 +  shows "continuous F (\<lambda>x. inverse (f x))"
   1.201 +  using assms unfolding continuous_def by (rule tendsto_inverse)
   1.202 +
   1.203 +lemma continuous_at_within_inverse[continuous_intros]:
   1.204 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
   1.205 +  assumes "continuous (at a within s) f" and "f a \<noteq> 0"
   1.206 +  shows "continuous (at a within s) (\<lambda>x. inverse (f x))"
   1.207 +  using assms unfolding continuous_within by (rule tendsto_inverse)
   1.208 +
   1.209 +lemma isCont_inverse[continuous_intros, simp]:
   1.210 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
   1.211 +  assumes "isCont f a" and "f a \<noteq> 0"
   1.212 +  shows "isCont (\<lambda>x. inverse (f x)) a"
   1.213 +  using assms unfolding continuous_at by (rule tendsto_inverse)
   1.214 +
   1.215 +lemma continuous_on_inverse[continuous_on_intros]:
   1.216 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
   1.217 +  assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
   1.218 +  shows "continuous_on s (\<lambda>x. inverse (f x))"
   1.219 +  using assms unfolding continuous_on_def by (fast intro: tendsto_inverse)
   1.220 +
   1.221  lemma tendsto_divide [tendsto_intros]:
   1.222    fixes a b :: "'a::real_normed_field"
   1.223    shows "\<lbrakk>(f ---> a) F; (g ---> b) F; b \<noteq> 0\<rbrakk>
   1.224      \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) F"
   1.225    by (simp add: tendsto_mult tendsto_inverse divide_inverse)
   1.226  
   1.227 +lemma continuous_divide:
   1.228 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_field"
   1.229 +  assumes "continuous F f" and "continuous F g" and "g (Lim F (\<lambda>x. x)) \<noteq> 0"
   1.230 +  shows "continuous F (\<lambda>x. (f x) / (g x))"
   1.231 +  using assms unfolding continuous_def by (rule tendsto_divide)
   1.232 +
   1.233 +lemma continuous_at_within_divide[continuous_intros]:
   1.234 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_field"
   1.235 +  assumes "continuous (at a within s) f" "continuous (at a within s) g" and "g a \<noteq> 0"
   1.236 +  shows "continuous (at a within s) (\<lambda>x. (f x) / (g x))"
   1.237 +  using assms unfolding continuous_within by (rule tendsto_divide)
   1.238 +
   1.239 +lemma isCont_divide[continuous_intros, simp]:
   1.240 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_field"
   1.241 +  assumes "isCont f a" "isCont g a" "g a \<noteq> 0"
   1.242 +  shows "isCont (\<lambda>x. (f x) / g x) a"
   1.243 +  using assms unfolding continuous_at by (rule tendsto_divide)
   1.244 +
   1.245 +lemma continuous_on_divide[continuous_on_intros]:
   1.246 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
   1.247 +  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. g x \<noteq> 0"
   1.248 +  shows "continuous_on s (\<lambda>x. (f x) / (g x))"
   1.249 +  using assms unfolding continuous_on_def by (fast intro: tendsto_divide)
   1.250 +
   1.251  lemma tendsto_sgn [tendsto_intros]:
   1.252    fixes l :: "'a::real_normed_vector"
   1.253    shows "\<lbrakk>(f ---> l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) F"
   1.254    unfolding sgn_div_norm by (simp add: tendsto_intros)
   1.255  
   1.256 +lemma continuous_sgn:
   1.257 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   1.258 +  assumes "continuous F f" and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
   1.259 +  shows "continuous F (\<lambda>x. sgn (f x))"
   1.260 +  using assms unfolding continuous_def by (rule tendsto_sgn)
   1.261 +
   1.262 +lemma continuous_at_within_sgn[continuous_intros]:
   1.263 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   1.264 +  assumes "continuous (at a within s) f" and "f a \<noteq> 0"
   1.265 +  shows "continuous (at a within s) (\<lambda>x. sgn (f x))"
   1.266 +  using assms unfolding continuous_within by (rule tendsto_sgn)
   1.267 +
   1.268 +lemma isCont_sgn[continuous_intros]:
   1.269 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   1.270 +  assumes "isCont f a" and "f a \<noteq> 0"
   1.271 +  shows "isCont (\<lambda>x. sgn (f x)) a"
   1.272 +  using assms unfolding continuous_at by (rule tendsto_sgn)
   1.273 +
   1.274 +lemma continuous_on_sgn[continuous_on_intros]:
   1.275 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   1.276 +  assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
   1.277 +  shows "continuous_on s (\<lambda>x. sgn (f x))"
   1.278 +  using assms unfolding continuous_on_def by (fast intro: tendsto_sgn)
   1.279 +
   1.280  lemma filterlim_at_infinity:
   1.281    fixes f :: "_ \<Rightarrow> 'a\<Colon>real_normed_vector"
   1.282    assumes "0 \<le> c"