src/HOL/Lim.thy
 author hoelzl Fri Mar 22 10:41:43 2013 +0100 (2013-03-22) changeset 51478 270b21f3ae0a parent 51473 1210309fddab permissions -rw-r--r--
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
```     1 (*  Title       : Lim.thy
```
```     2     Author      : Jacques D. Fleuriot
```
```     3     Copyright   : 1998  University of Cambridge
```
```     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
```
```     5 *)
```
```     6
```
```     7 header{* Limits and Continuity *}
```
```     8
```
```     9 theory Lim
```
```    10 imports SEQ
```
```    11 begin
```
```    12
```
```    13 subsection {* Limits of Functions *}
```
```    14
```
```    15 lemma LIM_eq:
```
```    16   fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
```
```    17   shows "f -- a --> L =
```
```    18      (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
```
```    19 by (simp add: LIM_def dist_norm)
```
```    20
```
```    21 lemma LIM_I:
```
```    22   fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
```
```    23   shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
```
```    24       ==> f -- a --> L"
```
```    25 by (simp add: LIM_eq)
```
```    26
```
```    27 lemma LIM_D:
```
```    28   fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
```
```    29   shows "[| f -- a --> L; 0<r |]
```
```    30       ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
```
```    31 by (simp add: LIM_eq)
```
```    32
```
```    33 lemma LIM_offset:
```
```    34   fixes a :: "'a::real_normed_vector"
```
```    35   shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
```
```    36 apply (rule topological_tendstoI)
```
```    37 apply (drule (2) topological_tendstoD)
```
```    38 apply (simp only: eventually_at dist_norm)
```
```    39 apply (clarify, rule_tac x=d in exI, safe)
```
```    40 apply (drule_tac x="x + k" in spec)
```
```    41 apply (simp add: algebra_simps)
```
```    42 done
```
```    43
```
```    44 lemma LIM_offset_zero:
```
```    45   fixes a :: "'a::real_normed_vector"
```
```    46   shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
```
```    47 by (drule_tac k="a" in LIM_offset, simp add: add_commute)
```
```    48
```
```    49 lemma LIM_offset_zero_cancel:
```
```    50   fixes a :: "'a::real_normed_vector"
```
```    51   shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
```
```    52 by (drule_tac k="- a" in LIM_offset, simp)
```
```    53
```
```    54 lemma LIM_zero:
```
```    55   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
```
```    56   shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
```
```    57 unfolding tendsto_iff dist_norm by simp
```
```    58
```
```    59 lemma LIM_zero_cancel:
```
```    60   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
```
```    61   shows "((\<lambda>x. f x - l) ---> 0) F \<Longrightarrow> (f ---> l) F"
```
```    62 unfolding tendsto_iff dist_norm by simp
```
```    63
```
```    64 lemma LIM_zero_iff:
```
```    65   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
```
```    66   shows "((\<lambda>x. f x - l) ---> 0) F = (f ---> l) F"
```
```    67 unfolding tendsto_iff dist_norm by simp
```
```    68
```
```    69 lemma LIM_imp_LIM:
```
```    70   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
```
```    71   fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
```
```    72   assumes f: "f -- a --> l"
```
```    73   assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
```
```    74   shows "g -- a --> m"
```
```    75   by (rule metric_LIM_imp_LIM [OF f],
```
```    76     simp add: dist_norm le)
```
```    77
```
```    78 lemma LIM_equal2:
```
```    79   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
```
```    80   assumes 1: "0 < R"
```
```    81   assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
```
```    82   shows "g -- a --> l \<Longrightarrow> f -- a --> l"
```
```    83 by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
```
```    84
```
```    85 lemma LIM_compose2:
```
```    86   fixes a :: "'a::real_normed_vector"
```
```    87   assumes f: "f -- a --> b"
```
```    88   assumes g: "g -- b --> c"
```
```    89   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
```
```    90   shows "(\<lambda>x. g (f x)) -- a --> c"
```
```    91 by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
```
```    92
```
```    93 lemma real_LIM_sandwich_zero:
```
```    94   fixes f g :: "'a::topological_space \<Rightarrow> real"
```
```    95   assumes f: "f -- a --> 0"
```
```    96   assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
```
```    97   assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
```
```    98   shows "g -- a --> 0"
```
```    99 proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *)
```
```   100   fix x assume x: "x \<noteq> a"
```
```   101   have "norm (g x - 0) = g x" by (simp add: 1 x)
```
```   102   also have "g x \<le> f x" by (rule 2 [OF x])
```
```   103   also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)
```
```   104   also have "\<bar>f x\<bar> = norm (f x - 0)" by simp
```
```   105   finally show "norm (g x - 0) \<le> norm (f x - 0)" .
```
```   106 qed
```
```   107
```
```   108
```
```   109 subsection {* Continuity *}
```
```   110
```
```   111 lemma LIM_isCont_iff:
```
```   112   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
```
```   113   shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
```
```   114 by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
```
```   115
```
```   116 lemma isCont_iff:
```
```   117   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
```
```   118   shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
```
```   119 by (simp add: isCont_def LIM_isCont_iff)
```
```   120
```
```   121 lemma isCont_LIM_compose2:
```
```   122   fixes a :: "'a::real_normed_vector"
```
```   123   assumes f [unfolded isCont_def]: "isCont f a"
```
```   124   assumes g: "g -- f a --> l"
```
```   125   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
```
```   126   shows "(\<lambda>x. g (f x)) -- a --> l"
```
```   127 by (rule LIM_compose2 [OF f g inj])
```
```   128
```
```   129
```
```   130 lemma isCont_norm [simp]:
```
```   131   fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
```
```   132   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
```
```   133   by (fact continuous_norm)
```
```   134
```
```   135 lemma isCont_rabs [simp]:
```
```   136   fixes f :: "'a::t2_space \<Rightarrow> real"
```
```   137   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
```
```   138   by (fact continuous_rabs)
```
```   139
```
```   140 lemma isCont_add [simp]:
```
```   141   fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
```
```   142   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
```
```   143   by (fact continuous_add)
```
```   144
```
```   145 lemma isCont_minus [simp]:
```
```   146   fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
```
```   147   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
```
```   148   by (fact continuous_minus)
```
```   149
```
```   150 lemma isCont_diff [simp]:
```
```   151   fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
```
```   152   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
```
```   153   by (fact continuous_diff)
```
```   154
```
```   155 lemma isCont_mult [simp]:
```
```   156   fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
```
```   157   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
```
```   158   by (fact continuous_mult)
```
```   159
```
```   160 lemma (in bounded_linear) isCont:
```
```   161   "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
```
```   162   by (fact continuous)
```
```   163
```
```   164 lemma (in bounded_bilinear) isCont:
```
```   165   "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
```
```   166   by (fact continuous)
```
```   167
```
```   168 lemmas isCont_scaleR [simp] =
```
```   169   bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
```
```   170
```
```   171 lemmas isCont_of_real [simp] =
```
```   172   bounded_linear.isCont [OF bounded_linear_of_real]
```
```   173
```
```   174 lemma isCont_power [simp]:
```
```   175   fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
```
```   176   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
```
```   177   by (fact continuous_power)
```
```   178
```
```   179 lemma isCont_setsum [simp]:
```
```   180   fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
```
```   181   shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
```
```   182   by (auto intro: continuous_setsum)
```
```   183
```
```   184 lemmas isCont_intros =
```
```   185   isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
```
```   186   isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
```
```   187   isCont_of_real isCont_power isCont_sgn isCont_setsum
```
```   188
```
```   189 subsection {* Uniform Continuity *}
```
```   190
```
```   191 lemma (in bounded_linear) isUCont: "isUCont f"
```
```   192 unfolding isUCont_def dist_norm
```
```   193 proof (intro allI impI)
```
```   194   fix r::real assume r: "0 < r"
```
```   195   obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
```
```   196     using pos_bounded by fast
```
```   197   show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
```
```   198   proof (rule exI, safe)
```
```   199     from r K show "0 < r / K" by (rule divide_pos_pos)
```
```   200   next
```
```   201     fix x y :: 'a
```
```   202     assume xy: "norm (x - y) < r / K"
```
```   203     have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
```
```   204     also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le)
```
```   205     also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq)
```
```   206     finally show "norm (f x - f y) < r" .
```
```   207   qed
```
```   208 qed
```
```   209
```
```   210 lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
```
```   211 by (rule isUCont [THEN isUCont_Cauchy])
```
```   212
```
```   213
```
```   214 lemma LIM_less_bound:
```
```   215   fixes f :: "real \<Rightarrow> real"
```
```   216   assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
```
```   217   shows "0 \<le> f x"
```
```   218 proof (rule tendsto_le_const)
```
```   219   show "(f ---> f x) (at_left x)"
```
```   220     using `isCont f x` by (simp add: filterlim_at_split isCont_def)
```
```   221   show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
```
```   222     using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
```
```   223 qed simp
```
```   224
```
```   225 end
```