src/HOL/Lim.thy
author huffman
Mon Jun 01 07:57:37 2009 -0700 (2009-06-01)
changeset 31353 14a58e2ca374
parent 31349 2261c8781f73
child 31355 3d18766ddc4b
permissions -rw-r--r--
add [code del] declarations
paulson@10751
     1
(*  Title       : Lim.thy
paulson@10751
     2
    Author      : Jacques D. Fleuriot
paulson@10751
     3
    Copyright   : 1998  University of Cambridge
paulson@14477
     4
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
paulson@10751
     5
*)
paulson@10751
     6
huffman@21165
     7
header{* Limits and Continuity *}
paulson@10751
     8
nipkow@15131
     9
theory Lim
haftmann@29197
    10
imports SEQ
nipkow@15131
    11
begin
paulson@14477
    12
huffman@22641
    13
text{*Standard Definitions*}
paulson@10751
    14
wenzelm@19765
    15
definition
huffman@31349
    16
  at :: "'a::metric_space \<Rightarrow> 'a filter" where
huffman@31353
    17
  [code del]: "at a = Abs_filter (\<lambda>P. \<exists>r>0. \<forall>x. x \<noteq> a \<and> dist x a < r \<longrightarrow> P x)"
huffman@31349
    18
huffman@31349
    19
definition
huffman@31338
    20
  LIM :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a, 'b] \<Rightarrow> bool"
wenzelm@21404
    21
        ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
haftmann@28562
    22
  [code del]: "f -- a --> L =
huffman@31338
    23
     (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
huffman@31338
    24
        --> dist (f x) L < r)"
paulson@10751
    25
wenzelm@21404
    26
definition
huffman@31338
    27
  isCont :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a] \<Rightarrow> bool" where
wenzelm@19765
    28
  "isCont f a = (f -- a --> (f a))"
paulson@10751
    29
wenzelm@21404
    30
definition
huffman@31338
    31
  isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
huffman@31338
    32
  [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
paulson@10751
    33
huffman@31349
    34
subsection {* Neighborhood Filter *}
huffman@31349
    35
huffman@31349
    36
lemma eventually_at:
huffman@31349
    37
  "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
huffman@31349
    38
unfolding at_def
huffman@31349
    39
apply (rule eventually_Abs_filter)
huffman@31349
    40
apply (rule_tac x=1 in exI, simp)
huffman@31349
    41
apply (clarify, rule_tac x=r in exI, simp)
huffman@31349
    42
apply (clarify, rename_tac r s)
huffman@31349
    43
apply (rule_tac x="min r s" in exI, simp)
huffman@31349
    44
done
huffman@31349
    45
huffman@31349
    46
lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> tendsto f L (at a)"
huffman@31349
    47
unfolding LIM_def tendsto_def eventually_at ..
paulson@10751
    48
huffman@20755
    49
subsection {* Limits of Functions *}
paulson@14477
    50
huffman@31338
    51
lemma metric_LIM_I:
huffman@31338
    52
  "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
huffman@31338
    53
    \<Longrightarrow> f -- a --> L"
huffman@31338
    54
by (simp add: LIM_def)
huffman@31338
    55
huffman@31338
    56
lemma metric_LIM_D:
huffman@31338
    57
  "\<lbrakk>f -- a --> L; 0 < r\<rbrakk>
huffman@31338
    58
    \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r"
huffman@31338
    59
by (simp add: LIM_def)
paulson@14477
    60
paulson@14477
    61
lemma LIM_eq:
huffman@31338
    62
  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
huffman@31338
    63
  shows "f -- a --> L =
huffman@20561
    64
     (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
huffman@31338
    65
by (simp add: LIM_def dist_norm)
paulson@14477
    66
huffman@20552
    67
lemma LIM_I:
huffman@31338
    68
  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
huffman@31338
    69
  shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
huffman@20552
    70
      ==> f -- a --> L"
huffman@20552
    71
by (simp add: LIM_eq)
huffman@20552
    72
paulson@14477
    73
lemma LIM_D:
huffman@31338
    74
  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
huffman@31338
    75
  shows "[| f -- a --> L; 0<r |]
huffman@20561
    76
      ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
paulson@14477
    77
by (simp add: LIM_eq)
paulson@14477
    78
huffman@31338
    79
lemma LIM_offset:
huffman@31338
    80
  fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"
huffman@31338
    81
  shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
huffman@31338
    82
unfolding LIM_def dist_norm
huffman@31338
    83
apply clarify
huffman@31338
    84
apply (drule_tac x="r" in spec, safe)
huffman@20756
    85
apply (rule_tac x="s" in exI, safe)
huffman@20756
    86
apply (drule_tac x="x + k" in spec)
nipkow@29667
    87
apply (simp add: algebra_simps)
huffman@20756
    88
done
huffman@20756
    89
huffman@31338
    90
lemma LIM_offset_zero:
huffman@31338
    91
  fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"
huffman@31338
    92
  shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
huffman@21239
    93
by (drule_tac k="a" in LIM_offset, simp add: add_commute)
huffman@21239
    94
huffman@31338
    95
lemma LIM_offset_zero_cancel:
huffman@31338
    96
  fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"
huffman@31338
    97
  shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
huffman@21239
    98
by (drule_tac k="- a" in LIM_offset, simp)
huffman@21239
    99
paulson@15228
   100
lemma LIM_const [simp]: "(%x. k) -- x --> k"
paulson@14477
   101
by (simp add: LIM_def)
paulson@14477
   102
paulson@14477
   103
lemma LIM_add:
huffman@31338
   104
  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
paulson@14477
   105
  assumes f: "f -- a --> L" and g: "g -- a --> M"
huffman@31338
   106
  shows "(\<lambda>x. f x + g x) -- a --> (L + M)"
huffman@31349
   107
using assms unfolding LIM_conv_tendsto by (rule tendsto_add)
paulson@14477
   108
huffman@21257
   109
lemma LIM_add_zero:
huffman@31338
   110
  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   111
  shows "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0"
huffman@21257
   112
by (drule (1) LIM_add, simp)
huffman@21257
   113
huffman@20552
   114
lemma minus_diff_minus:
huffman@20552
   115
  fixes a b :: "'a::ab_group_add"
huffman@20552
   116
  shows "(- a) - (- b) = - (a - b)"
huffman@20552
   117
by simp
huffman@20552
   118
huffman@31338
   119
lemma LIM_minus:
huffman@31338
   120
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   121
  shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L"
huffman@31349
   122
unfolding LIM_conv_tendsto by (rule tendsto_minus)
paulson@14477
   123
huffman@31338
   124
(* TODO: delete *)
paulson@14477
   125
lemma LIM_add_minus:
huffman@31338
   126
  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   127
  shows "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
huffman@20552
   128
by (intro LIM_add LIM_minus)
paulson@14477
   129
paulson@14477
   130
lemma LIM_diff:
huffman@31338
   131
  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   132
  shows "\<lbrakk>f -- x --> l; g -- x --> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --> l - m"
huffman@31349
   133
unfolding LIM_conv_tendsto by (rule tendsto_diff)
paulson@14477
   134
huffman@31338
   135
lemma LIM_zero:
huffman@31338
   136
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   137
  shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"
huffman@31338
   138
by (simp add: LIM_def dist_norm)
huffman@21239
   139
huffman@31338
   140
lemma LIM_zero_cancel:
huffman@31338
   141
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   142
  shows "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l"
huffman@31338
   143
by (simp add: LIM_def dist_norm)
huffman@21239
   144
huffman@31338
   145
lemma LIM_zero_iff:
huffman@31338
   146
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   147
  shows "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l"
huffman@31338
   148
by (simp add: LIM_def dist_norm)
huffman@21399
   149
huffman@31338
   150
lemma metric_LIM_imp_LIM:
huffman@21257
   151
  assumes f: "f -- a --> l"
huffman@31338
   152
  assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
huffman@21257
   153
  shows "g -- a --> m"
huffman@31338
   154
apply (rule metric_LIM_I, drule metric_LIM_D [OF f], safe)
huffman@21257
   155
apply (rule_tac x="s" in exI, safe)
huffman@21257
   156
apply (drule_tac x="x" in spec, safe)
huffman@21257
   157
apply (erule (1) order_le_less_trans [OF le])
huffman@21257
   158
done
huffman@21257
   159
huffman@31338
   160
lemma LIM_imp_LIM:
huffman@31338
   161
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   162
  fixes g :: "'a::metric_space \<Rightarrow> 'c::real_normed_vector"
huffman@31338
   163
  assumes f: "f -- a --> l"
huffman@31338
   164
  assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
huffman@31338
   165
  shows "g -- a --> m"
huffman@31338
   166
apply (rule metric_LIM_imp_LIM [OF f])
huffman@31338
   167
apply (simp add: dist_norm le)
huffman@31338
   168
done
huffman@31338
   169
huffman@31338
   170
lemma LIM_norm:
huffman@31338
   171
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   172
  shows "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l"
huffman@31349
   173
unfolding LIM_conv_tendsto by (rule tendsto_norm)
huffman@21257
   174
huffman@31338
   175
lemma LIM_norm_zero:
huffman@31338
   176
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   177
  shows "f -- a --> 0 \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> 0"
huffman@21257
   178
by (drule LIM_norm, simp)
huffman@21257
   179
huffman@31338
   180
lemma LIM_norm_zero_cancel:
huffman@31338
   181
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   182
  shows "(\<lambda>x. norm (f x)) -- a --> 0 \<Longrightarrow> f -- a --> 0"
huffman@21257
   183
by (erule LIM_imp_LIM, simp)
huffman@21257
   184
huffman@31338
   185
lemma LIM_norm_zero_iff:
huffman@31338
   186
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   187
  shows "(\<lambda>x. norm (f x)) -- a --> 0 = f -- a --> 0"
huffman@21399
   188
by (rule iffI [OF LIM_norm_zero_cancel LIM_norm_zero])
huffman@21399
   189
huffman@22627
   190
lemma LIM_rabs: "f -- a --> (l::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) -- a --> \<bar>l\<bar>"
huffman@22627
   191
by (fold real_norm_def, rule LIM_norm)
huffman@22627
   192
huffman@22627
   193
lemma LIM_rabs_zero: "f -- a --> (0::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) -- a --> 0"
huffman@22627
   194
by (fold real_norm_def, rule LIM_norm_zero)
huffman@22627
   195
huffman@22627
   196
lemma LIM_rabs_zero_cancel: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) \<Longrightarrow> f -- a --> 0"
huffman@22627
   197
by (fold real_norm_def, rule LIM_norm_zero_cancel)
huffman@22627
   198
huffman@22627
   199
lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) = f -- a --> 0"
huffman@22627
   200
by (fold real_norm_def, rule LIM_norm_zero_iff)
huffman@22627
   201
huffman@20561
   202
lemma LIM_const_not_eq:
huffman@23076
   203
  fixes a :: "'a::real_normed_algebra_1"
huffman@23076
   204
  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
huffman@31338
   205
apply (simp add: LIM_def)
huffman@31338
   206
apply (rule_tac x="dist k L" in exI, simp add: zero_less_dist_iff, safe)
huffman@31338
   207
apply (rule_tac x="a + of_real (s/2)" in exI, simp add: dist_norm)
huffman@20552
   208
done
paulson@14477
   209
huffman@21786
   210
lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
huffman@21786
   211
huffman@20561
   212
lemma LIM_const_eq:
huffman@23076
   213
  fixes a :: "'a::real_normed_algebra_1"
huffman@23076
   214
  shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
paulson@14477
   215
apply (rule ccontr)
kleing@19023
   216
apply (blast dest: LIM_const_not_eq)
paulson@14477
   217
done
paulson@14477
   218
huffman@20561
   219
lemma LIM_unique:
huffman@31338
   220
  fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}
huffman@23076
   221
  shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
huffman@31338
   222
apply (rule ccontr)
huffman@31338
   223
apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff)
huffman@31338
   224
apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff)
huffman@31338
   225
apply (clarify, rename_tac r s)
huffman@31338
   226
apply (subgoal_tac "min r s \<noteq> 0")
huffman@31338
   227
apply (subgoal_tac "dist L M < dist L M / 2 + dist L M / 2", simp)
huffman@31338
   228
apply (subgoal_tac "dist L M \<le> dist (f (a + of_real (min r s / 2))) L +
huffman@31338
   229
                               dist (f (a + of_real (min r s / 2))) M")
huffman@31338
   230
apply (erule le_less_trans, rule add_strict_mono)
huffman@31338
   231
apply (drule spec, erule mp, simp add: dist_norm)
huffman@31338
   232
apply (drule spec, erule mp, simp add: dist_norm)
huffman@31338
   233
apply (subst dist_commute, rule dist_triangle)
huffman@31338
   234
apply simp
paulson@14477
   235
done
paulson@14477
   236
huffman@23069
   237
lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"
paulson@14477
   238
by (auto simp add: LIM_def)
paulson@14477
   239
paulson@14477
   240
text{*Limits are equal for functions equal except at limit point*}
paulson@14477
   241
lemma LIM_equal:
paulson@14477
   242
     "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"
paulson@14477
   243
by (simp add: LIM_def)
paulson@14477
   244
huffman@20796
   245
lemma LIM_cong:
huffman@20796
   246
  "\<lbrakk>a = b; \<And>x. x \<noteq> b \<Longrightarrow> f x = g x; l = m\<rbrakk>
huffman@21399
   247
   \<Longrightarrow> ((\<lambda>x. f x) -- a --> l) = ((\<lambda>x. g x) -- b --> m)"
huffman@20796
   248
by (simp add: LIM_def)
huffman@20796
   249
huffman@31338
   250
lemma metric_LIM_equal2:
huffman@21282
   251
  assumes 1: "0 < R"
huffman@31338
   252
  assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x"
huffman@21282
   253
  shows "g -- a --> l \<Longrightarrow> f -- a --> l"
huffman@21282
   254
apply (unfold LIM_def, safe)
huffman@21282
   255
apply (drule_tac x="r" in spec, safe)
huffman@21282
   256
apply (rule_tac x="min s R" in exI, safe)
huffman@21282
   257
apply (simp add: 1)
huffman@21282
   258
apply (simp add: 2)
huffman@21282
   259
done
huffman@21282
   260
huffman@31338
   261
lemma LIM_equal2:
huffman@31338
   262
  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space"
huffman@31338
   263
  assumes 1: "0 < R"
huffman@31338
   264
  assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
huffman@31338
   265
  shows "g -- a --> l \<Longrightarrow> f -- a --> l"
huffman@31338
   266
apply (unfold LIM_def dist_norm, safe)
huffman@31338
   267
apply (drule_tac x="r" in spec, safe)
huffman@31338
   268
apply (rule_tac x="min s R" in exI, safe)
huffman@31338
   269
apply (simp add: 1)
huffman@31338
   270
apply (simp add: 2)
huffman@31338
   271
done
huffman@31338
   272
huffman@31338
   273
text{*Two uses in Transcendental.ML*}
paulson@14477
   274
lemma LIM_trans:
huffman@31338
   275
  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   276
  shows "[| (%x. f(x) + -g(x)) -- a --> 0;  g -- a --> l |] ==> f -- a --> l"
paulson@14477
   277
apply (drule LIM_add, assumption)
paulson@14477
   278
apply (auto simp add: add_assoc)
paulson@14477
   279
done
paulson@14477
   280
huffman@21239
   281
lemma LIM_compose:
huffman@21239
   282
  assumes g: "g -- l --> g l"
huffman@21239
   283
  assumes f: "f -- a --> l"
huffman@21239
   284
  shows "(\<lambda>x. g (f x)) -- a --> g l"
huffman@31338
   285
proof (rule metric_LIM_I)
huffman@21239
   286
  fix r::real assume r: "0 < r"
huffman@21239
   287
  obtain s where s: "0 < s"
huffman@31338
   288
    and less_r: "\<And>y. \<lbrakk>y \<noteq> l; dist y l < s\<rbrakk> \<Longrightarrow> dist (g y) (g l) < r"
huffman@31338
   289
    using metric_LIM_D [OF g r] by fast
huffman@21239
   290
  obtain t where t: "0 < t"
huffman@31338
   291
    and less_s: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> dist (f x) l < s"
huffman@31338
   292
    using metric_LIM_D [OF f s] by fast
huffman@21239
   293
huffman@31338
   294
  show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> dist x a < t \<longrightarrow> dist (g (f x)) (g l) < r"
huffman@21239
   295
  proof (rule exI, safe)
huffman@21239
   296
    show "0 < t" using t .
huffman@21239
   297
  next
huffman@31338
   298
    fix x assume "x \<noteq> a" and "dist x a < t"
huffman@31338
   299
    hence "dist (f x) l < s" by (rule less_s)
huffman@31338
   300
    thus "dist (g (f x)) (g l) < r"
huffman@21239
   301
      using r less_r by (case_tac "f x = l", simp_all)
huffman@21239
   302
  qed
huffman@21239
   303
qed
huffman@21239
   304
huffman@31338
   305
lemma metric_LIM_compose2:
huffman@31338
   306
  assumes f: "f -- a --> b"
huffman@31338
   307
  assumes g: "g -- b --> c"
huffman@31338
   308
  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
huffman@31338
   309
  shows "(\<lambda>x. g (f x)) -- a --> c"
huffman@31338
   310
proof (rule metric_LIM_I)
huffman@31338
   311
  fix r :: real
huffman@31338
   312
  assume r: "0 < r"
huffman@31338
   313
  obtain s where s: "0 < s"
huffman@31338
   314
    and less_r: "\<And>y. \<lbrakk>y \<noteq> b; dist y b < s\<rbrakk> \<Longrightarrow> dist (g y) c < r"
huffman@31338
   315
    using metric_LIM_D [OF g r] by fast
huffman@31338
   316
  obtain t where t: "0 < t"
huffman@31338
   317
    and less_s: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> dist (f x) b < s"
huffman@31338
   318
    using metric_LIM_D [OF f s] by fast
huffman@31338
   319
  obtain d where d: "0 < d"
huffman@31338
   320
    and neq_b: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < d\<rbrakk> \<Longrightarrow> f x \<noteq> b"
huffman@31338
   321
    using inj by fast
huffman@31338
   322
huffman@31338
   323
  show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> dist x a < t \<longrightarrow> dist (g (f x)) c < r"
huffman@31338
   324
  proof (safe intro!: exI)
huffman@31338
   325
    show "0 < min d t" using d t by simp
huffman@31338
   326
  next
huffman@31338
   327
    fix x
huffman@31338
   328
    assume "x \<noteq> a" and "dist x a < min d t"
huffman@31338
   329
    hence "f x \<noteq> b" and "dist (f x) b < s"
huffman@31338
   330
      using neq_b less_s by simp_all
huffman@31338
   331
    thus "dist (g (f x)) c < r"
huffman@31338
   332
      by (rule less_r)
huffman@31338
   333
  qed
huffman@31338
   334
qed
huffman@31338
   335
huffman@23040
   336
lemma LIM_compose2:
huffman@31338
   337
  fixes a :: "'a::real_normed_vector"
huffman@23040
   338
  assumes f: "f -- a --> b"
huffman@23040
   339
  assumes g: "g -- b --> c"
huffman@23040
   340
  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
huffman@23040
   341
  shows "(\<lambda>x. g (f x)) -- a --> c"
huffman@31338
   342
by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
huffman@23040
   343
huffman@21239
   344
lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
huffman@21239
   345
unfolding o_def by (rule LIM_compose)
huffman@21239
   346
huffman@21282
   347
lemma real_LIM_sandwich_zero:
huffman@31338
   348
  fixes f g :: "'a::metric_space \<Rightarrow> real"
huffman@21282
   349
  assumes f: "f -- a --> 0"
huffman@21282
   350
  assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
huffman@21282
   351
  assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
huffman@21282
   352
  shows "g -- a --> 0"
huffman@21282
   353
proof (rule LIM_imp_LIM [OF f])
huffman@21282
   354
  fix x assume x: "x \<noteq> a"
huffman@21282
   355
  have "norm (g x - 0) = g x" by (simp add: 1 x)
huffman@21282
   356
  also have "g x \<le> f x" by (rule 2 [OF x])
huffman@21282
   357
  also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)
huffman@21282
   358
  also have "\<bar>f x\<bar> = norm (f x - 0)" by simp
huffman@21282
   359
  finally show "norm (g x - 0) \<le> norm (f x - 0)" .
huffman@21282
   360
qed
huffman@21282
   361
huffman@22442
   362
text {* Bounded Linear Operators *}
huffman@21282
   363
huffman@21282
   364
lemma (in bounded_linear) LIM:
huffman@21282
   365
  "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
huffman@31349
   366
unfolding LIM_conv_tendsto by (rule tendsto)
huffman@31349
   367
huffman@31349
   368
lemma (in bounded_linear) cont: "f -- a --> f a"
huffman@31349
   369
by (rule LIM [OF LIM_ident])
huffman@21282
   370
huffman@21282
   371
lemma (in bounded_linear) LIM_zero:
huffman@21282
   372
  "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
huffman@21282
   373
by (drule LIM, simp only: zero)
huffman@21282
   374
huffman@22442
   375
text {* Bounded Bilinear Operators *}
huffman@21282
   376
huffman@31349
   377
lemma (in bounded_bilinear) LIM:
huffman@31349
   378
  "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
huffman@31349
   379
unfolding LIM_conv_tendsto by (rule tendsto)
huffman@31349
   380
huffman@21282
   381
lemma (in bounded_bilinear) LIM_prod_zero:
huffman@31338
   382
  fixes a :: "'d::metric_space"
huffman@21282
   383
  assumes f: "f -- a --> 0"
huffman@21282
   384
  assumes g: "g -- a --> 0"
huffman@21282
   385
  shows "(\<lambda>x. f x ** g x) -- a --> 0"
huffman@31349
   386
using LIM [OF f g] by (simp add: zero_left)
huffman@21282
   387
huffman@21282
   388
lemma (in bounded_bilinear) LIM_left_zero:
huffman@21282
   389
  "f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0"
huffman@21282
   390
by (rule bounded_linear.LIM_zero [OF bounded_linear_left])
huffman@21282
   391
huffman@21282
   392
lemma (in bounded_bilinear) LIM_right_zero:
huffman@21282
   393
  "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
huffman@21282
   394
by (rule bounded_linear.LIM_zero [OF bounded_linear_right])
huffman@21282
   395
huffman@23127
   396
lemmas LIM_mult = mult.LIM
huffman@21282
   397
huffman@23127
   398
lemmas LIM_mult_zero = mult.LIM_prod_zero
huffman@21282
   399
huffman@23127
   400
lemmas LIM_mult_left_zero = mult.LIM_left_zero
huffman@21282
   401
huffman@23127
   402
lemmas LIM_mult_right_zero = mult.LIM_right_zero
huffman@21282
   403
huffman@23127
   404
lemmas LIM_scaleR = scaleR.LIM
huffman@21282
   405
huffman@23127
   406
lemmas LIM_of_real = of_real.LIM
huffman@22627
   407
huffman@22627
   408
lemma LIM_power:
huffman@31338
   409
  fixes f :: "'a::metric_space \<Rightarrow> 'b::{power,real_normed_algebra}"
huffman@22627
   410
  assumes f: "f -- a --> l"
huffman@22627
   411
  shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
huffman@30273
   412
by (induct n, simp, simp add: LIM_mult f)
huffman@22627
   413
huffman@22641
   414
subsubsection {* Derived theorems about @{term LIM} *}
huffman@22641
   415
huffman@22637
   416
lemma LIM_inverse_lemma:
huffman@22637
   417
  fixes x :: "'a::real_normed_div_algebra"
huffman@22637
   418
  assumes r: "0 < r"
huffman@22637
   419
  assumes x: "norm (x - 1) < min (1/2) (r/2)"
huffman@22637
   420
  shows "norm (inverse x - 1) < r"
huffman@22637
   421
proof -
huffman@22637
   422
  from r have r2: "0 < r/2" by simp
huffman@22637
   423
  from x have 0: "x \<noteq> 0" by clarsimp
huffman@22637
   424
  from x have x': "norm (1 - x) < min (1/2) (r/2)"
huffman@22637
   425
    by (simp only: norm_minus_commute)
huffman@22637
   426
  hence less1: "norm (1 - x) < r/2" by simp
huffman@22637
   427
  have "norm (1::'a) - norm x \<le> norm (1 - x)" by (rule norm_triangle_ineq2)
huffman@22637
   428
  also from x' have "norm (1 - x) < 1/2" by simp
huffman@22637
   429
  finally have "1/2 < norm x" by simp
huffman@22637
   430
  hence "inverse (norm x) < inverse (1/2)"
huffman@22637
   431
    by (rule less_imp_inverse_less, simp)
huffman@22637
   432
  hence less2: "norm (inverse x) < 2"
huffman@22637
   433
    by (simp add: nonzero_norm_inverse 0)
huffman@22637
   434
  from less1 less2 r2 norm_ge_zero
huffman@22637
   435
  have "norm (1 - x) * norm (inverse x) < (r/2) * 2"
huffman@22637
   436
    by (rule mult_strict_mono)
huffman@22637
   437
  thus "norm (inverse x - 1) < r"
huffman@22637
   438
    by (simp only: norm_mult [symmetric] left_diff_distrib, simp add: 0)
huffman@22637
   439
qed
huffman@22637
   440
huffman@22637
   441
lemma LIM_inverse_fun:
huffman@22637
   442
  assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)"
huffman@22637
   443
  shows "inverse -- a --> inverse a"
huffman@22637
   444
proof (rule LIM_equal2)
huffman@22637
   445
  from a show "0 < norm a" by simp
huffman@22637
   446
next
huffman@22637
   447
  fix x assume "norm (x - a) < norm a"
huffman@22637
   448
  hence "x \<noteq> 0" by auto
huffman@22637
   449
  with a show "inverse x = inverse (inverse a * x) * inverse a"
huffman@22637
   450
    by (simp add: nonzero_inverse_mult_distrib
huffman@22637
   451
                  nonzero_imp_inverse_nonzero
huffman@22637
   452
                  nonzero_inverse_inverse_eq mult_assoc)
huffman@22637
   453
next
huffman@22637
   454
  have 1: "inverse -- 1 --> inverse (1::'a)"
huffman@22637
   455
    apply (rule LIM_I)
huffman@22637
   456
    apply (rule_tac x="min (1/2) (r/2)" in exI)
huffman@22637
   457
    apply (simp add: LIM_inverse_lemma)
huffman@22637
   458
    done
huffman@22637
   459
  have "(\<lambda>x. inverse a * x) -- a --> inverse a * a"
huffman@23069
   460
    by (intro LIM_mult LIM_ident LIM_const)
huffman@22637
   461
  hence "(\<lambda>x. inverse a * x) -- a --> 1"
huffman@22637
   462
    by (simp add: a)
huffman@22637
   463
  with 1 have "(\<lambda>x. inverse (inverse a * x)) -- a --> inverse 1"
huffman@22637
   464
    by (rule LIM_compose)
huffman@22637
   465
  hence "(\<lambda>x. inverse (inverse a * x)) -- a --> 1"
huffman@22637
   466
    by simp
huffman@22637
   467
  hence "(\<lambda>x. inverse (inverse a * x) * inverse a) -- a --> 1 * inverse a"
huffman@22637
   468
    by (intro LIM_mult LIM_const)
huffman@22637
   469
  thus "(\<lambda>x. inverse (inverse a * x) * inverse a) -- a --> inverse a"
huffman@22637
   470
    by simp
huffman@22637
   471
qed
huffman@22637
   472
huffman@22637
   473
lemma LIM_inverse:
huffman@22637
   474
  fixes L :: "'a::real_normed_div_algebra"
huffman@22637
   475
  shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
huffman@22637
   476
by (rule LIM_inverse_fun [THEN LIM_compose])
huffman@22637
   477
huffman@29885
   478
lemma LIM_sgn:
huffman@31338
   479
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   480
  shows "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l"
huffman@29885
   481
unfolding sgn_div_norm
huffman@29885
   482
by (simp add: LIM_scaleR LIM_inverse LIM_norm)
huffman@29885
   483
paulson@14477
   484
huffman@20755
   485
subsection {* Continuity *}
paulson@14477
   486
huffman@31338
   487
lemma LIM_isCont_iff:
huffman@31338
   488
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space"
huffman@31338
   489
  shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
huffman@21239
   490
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
huffman@21239
   491
huffman@31338
   492
lemma isCont_iff:
huffman@31338
   493
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space"
huffman@31338
   494
  shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
huffman@21239
   495
by (simp add: isCont_def LIM_isCont_iff)
huffman@21239
   496
huffman@23069
   497
lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a"
huffman@23069
   498
  unfolding isCont_def by (rule LIM_ident)
huffman@21239
   499
huffman@21786
   500
lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
huffman@21282
   501
  unfolding isCont_def by (rule LIM_const)
huffman@21239
   502
huffman@31338
   503
lemma isCont_norm:
huffman@31338
   504
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   505
  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
huffman@21786
   506
  unfolding isCont_def by (rule LIM_norm)
huffman@21786
   507
huffman@22627
   508
lemma isCont_rabs: "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x :: real\<bar>) a"
huffman@22627
   509
  unfolding isCont_def by (rule LIM_rabs)
huffman@22627
   510
huffman@31338
   511
lemma isCont_add:
huffman@31338
   512
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   513
  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
huffman@21282
   514
  unfolding isCont_def by (rule LIM_add)
huffman@21239
   515
huffman@31338
   516
lemma isCont_minus:
huffman@31338
   517
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   518
  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
huffman@21282
   519
  unfolding isCont_def by (rule LIM_minus)
huffman@21239
   520
huffman@31338
   521
lemma isCont_diff:
huffman@31338
   522
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   523
  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
huffman@21282
   524
  unfolding isCont_def by (rule LIM_diff)
huffman@21239
   525
huffman@21239
   526
lemma isCont_mult:
huffman@31338
   527
  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_algebra"
huffman@21786
   528
  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
huffman@21282
   529
  unfolding isCont_def by (rule LIM_mult)
huffman@21239
   530
huffman@21239
   531
lemma isCont_inverse:
huffman@31338
   532
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_div_algebra"
huffman@21786
   533
  shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
huffman@21282
   534
  unfolding isCont_def by (rule LIM_inverse)
huffman@21239
   535
huffman@21239
   536
lemma isCont_LIM_compose:
huffman@21239
   537
  "\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l"
huffman@21282
   538
  unfolding isCont_def by (rule LIM_compose)
huffman@21239
   539
huffman@31338
   540
lemma metric_isCont_LIM_compose2:
huffman@31338
   541
  assumes f [unfolded isCont_def]: "isCont f a"
huffman@31338
   542
  assumes g: "g -- f a --> l"
huffman@31338
   543
  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a"
huffman@31338
   544
  shows "(\<lambda>x. g (f x)) -- a --> l"
huffman@31338
   545
by (rule metric_LIM_compose2 [OF f g inj])
huffman@31338
   546
huffman@23040
   547
lemma isCont_LIM_compose2:
huffman@31338
   548
  fixes a :: "'a::real_normed_vector"
huffman@23040
   549
  assumes f [unfolded isCont_def]: "isCont f a"
huffman@23040
   550
  assumes g: "g -- f a --> l"
huffman@23040
   551
  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
huffman@23040
   552
  shows "(\<lambda>x. g (f x)) -- a --> l"
huffman@23040
   553
by (rule LIM_compose2 [OF f g inj])
huffman@23040
   554
huffman@21239
   555
lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
huffman@21282
   556
  unfolding isCont_def by (rule LIM_compose)
huffman@21239
   557
huffman@21239
   558
lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a"
huffman@21282
   559
  unfolding o_def by (rule isCont_o2)
huffman@21282
   560
huffman@21282
   561
lemma (in bounded_linear) isCont: "isCont f a"
huffman@21282
   562
  unfolding isCont_def by (rule cont)
huffman@21282
   563
huffman@21282
   564
lemma (in bounded_bilinear) isCont:
huffman@21282
   565
  "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
huffman@21282
   566
  unfolding isCont_def by (rule LIM)
huffman@21282
   567
huffman@23127
   568
lemmas isCont_scaleR = scaleR.isCont
huffman@21239
   569
huffman@22627
   570
lemma isCont_of_real:
huffman@31338
   571
  "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a"
huffman@22627
   572
  unfolding isCont_def by (rule LIM_of_real)
huffman@22627
   573
huffman@22627
   574
lemma isCont_power:
huffman@31338
   575
  fixes f :: "'a::metric_space \<Rightarrow> 'b::{power,real_normed_algebra}"
huffman@22627
   576
  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
huffman@22627
   577
  unfolding isCont_def by (rule LIM_power)
huffman@22627
   578
huffman@29885
   579
lemma isCont_sgn:
huffman@31338
   580
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   581
  shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
huffman@29885
   582
  unfolding isCont_def by (rule LIM_sgn)
huffman@29885
   583
huffman@20561
   584
lemma isCont_abs [simp]: "isCont abs (a::real)"
huffman@23069
   585
by (rule isCont_rabs [OF isCont_ident])
paulson@15228
   586
huffman@31338
   587
lemma isCont_setsum:
huffman@31338
   588
  fixes f :: "'a \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::real_normed_vector"
huffman@31338
   589
  fixes A :: "'a set" assumes "finite A"
hoelzl@29803
   590
  shows "\<forall> i \<in> A. isCont (f i) x \<Longrightarrow> isCont (\<lambda> x. \<Sum> i \<in> A. f i x) x"
hoelzl@29803
   591
  using `finite A`
hoelzl@29803
   592
proof induct
hoelzl@29803
   593
  case (insert a F) show "isCont (\<lambda> x. \<Sum> i \<in> (insert a F). f i x) x" 
hoelzl@29803
   594
    unfolding setsum_insert[OF `finite F` `a \<notin> F`] by (rule isCont_add, auto simp add: insert)
hoelzl@29803
   595
qed auto
hoelzl@29803
   596
hoelzl@29803
   597
lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
hoelzl@29803
   598
  and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"
hoelzl@29803
   599
  shows "0 \<le> f x"
hoelzl@29803
   600
proof (rule ccontr)
hoelzl@29803
   601
  assume "\<not> 0 \<le> f x" hence "f x < 0" by auto
hoelzl@29803
   602
  hence "0 < - f x / 2" by auto
hoelzl@29803
   603
  from isCont[unfolded isCont_def, THEN LIM_D, OF this]
hoelzl@29803
   604
  obtain s where "s > 0" and s_D: "\<And>x'. \<lbrakk> x' \<noteq> x ; \<bar> x' - x \<bar> < s \<rbrakk> \<Longrightarrow> \<bar> f x' - f x \<bar> < - f x / 2" by auto
hoelzl@29803
   605
hoelzl@29803
   606
  let ?x = "x - min (s / 2) ((x - b) / 2)"
hoelzl@29803
   607
  have "?x < x" and "\<bar> ?x - x \<bar> < s"
hoelzl@29803
   608
    using `b < x` and `0 < s` by auto
hoelzl@29803
   609
  have "b < ?x"
hoelzl@29803
   610
  proof (cases "s < x - b")
hoelzl@29803
   611
    case True thus ?thesis using `0 < s` by auto
hoelzl@29803
   612
  next
hoelzl@29803
   613
    case False hence "s / 2 \<ge> (x - b) / 2" by auto
hoelzl@29803
   614
    from inf_absorb2[OF this, unfolded inf_real_def]
hoelzl@29803
   615
    have "?x = (x + b) / 2" by auto
hoelzl@29803
   616
    thus ?thesis using `b < x` by auto
hoelzl@29803
   617
  qed
hoelzl@29803
   618
  hence "0 \<le> f ?x" using all_le `?x < x` by auto
hoelzl@29803
   619
  moreover have "\<bar>f ?x - f x\<bar> < - f x / 2"
hoelzl@29803
   620
    using s_D[OF _ `\<bar> ?x - x \<bar> < s`] `?x < x` by auto
hoelzl@29803
   621
  hence "f ?x - f x < - f x / 2" by auto
hoelzl@29803
   622
  hence "f ?x < f x / 2" by auto
hoelzl@29803
   623
  hence "f ?x < 0" using `f x < 0` by auto
hoelzl@29803
   624
  thus False using `0 \<le> f ?x` by auto
hoelzl@29803
   625
qed
huffman@31338
   626
paulson@14477
   627
huffman@20755
   628
subsection {* Uniform Continuity *}
huffman@20755
   629
paulson@14477
   630
lemma isUCont_isCont: "isUCont f ==> isCont f x"
huffman@23012
   631
by (simp add: isUCont_def isCont_def LIM_def, force)
paulson@14477
   632
huffman@23118
   633
lemma isUCont_Cauchy:
huffman@23118
   634
  "\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
huffman@23118
   635
unfolding isUCont_def
huffman@31338
   636
apply (rule metric_CauchyI)
huffman@23118
   637
apply (drule_tac x=e in spec, safe)
huffman@31338
   638
apply (drule_tac e=s in metric_CauchyD, safe)
huffman@23118
   639
apply (rule_tac x=M in exI, simp)
huffman@23118
   640
done
huffman@23118
   641
huffman@23118
   642
lemma (in bounded_linear) isUCont: "isUCont f"
huffman@31338
   643
unfolding isUCont_def dist_norm
huffman@23118
   644
proof (intro allI impI)
huffman@23118
   645
  fix r::real assume r: "0 < r"
huffman@23118
   646
  obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
huffman@23118
   647
    using pos_bounded by fast
huffman@23118
   648
  show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
huffman@23118
   649
  proof (rule exI, safe)
huffman@23118
   650
    from r K show "0 < r / K" by (rule divide_pos_pos)
huffman@23118
   651
  next
huffman@23118
   652
    fix x y :: 'a
huffman@23118
   653
    assume xy: "norm (x - y) < r / K"
huffman@23118
   654
    have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
huffman@23118
   655
    also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le)
huffman@23118
   656
    also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq)
huffman@23118
   657
    finally show "norm (f x - f y) < r" .
huffman@23118
   658
  qed
huffman@23118
   659
qed
huffman@23118
   660
huffman@23118
   661
lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
huffman@23118
   662
by (rule isUCont [THEN isUCont_Cauchy])
huffman@23118
   663
paulson@14477
   664
huffman@21165
   665
subsection {* Relation of LIM and LIMSEQ *}
kleing@19023
   666
kleing@19023
   667
lemma LIMSEQ_SEQ_conv1:
huffman@31338
   668
  fixes a :: "'a::metric_space"
huffman@21165
   669
  assumes X: "X -- a --> L"
kleing@19023
   670
  shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
huffman@31338
   671
proof (safe intro!: metric_LIMSEQ_I)
huffman@21165
   672
  fix S :: "nat \<Rightarrow> 'a"
huffman@21165
   673
  fix r :: real
huffman@21165
   674
  assume rgz: "0 < r"
huffman@21165
   675
  assume as: "\<forall>n. S n \<noteq> a"
huffman@21165
   676
  assume S: "S ----> a"
huffman@31338
   677
  from metric_LIM_D [OF X rgz] obtain s
huffman@21165
   678
    where sgz: "0 < s"
huffman@31338
   679
    and aux: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < s\<rbrakk> \<Longrightarrow> dist (X x) L < r"
huffman@21165
   680
    by fast
huffman@31338
   681
  from metric_LIMSEQ_D [OF S sgz]
huffman@31338
   682
  obtain no where "\<forall>n\<ge>no. dist (S n) a < s" by blast
huffman@31338
   683
  hence "\<forall>n\<ge>no. dist (X (S n)) L < r" by (simp add: aux as)
huffman@31338
   684
  thus "\<exists>no. \<forall>n\<ge>no. dist (X (S n)) L < r" ..
kleing@19023
   685
qed
kleing@19023
   686
huffman@31338
   687
kleing@19023
   688
lemma LIMSEQ_SEQ_conv2:
huffman@20561
   689
  fixes a :: real
kleing@19023
   690
  assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
kleing@19023
   691
  shows "X -- a --> L"
kleing@19023
   692
proof (rule ccontr)
kleing@19023
   693
  assume "\<not> (X -- a --> L)"
huffman@31338
   694
  hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> dist (X x) L < r)"
huffman@31338
   695
    unfolding LIM_def dist_norm .
huffman@31338
   696
  hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x - a\<bar> < s --> dist (X x) L < r)" by simp
huffman@31338
   697
  hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r)" by (simp add: not_less)
huffman@31338
   698
  then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r))" by auto
kleing@19023
   699
huffman@31338
   700
  let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
huffman@31338
   701
  have "\<And>n. \<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
huffman@21165
   702
    using rdef by simp
huffman@31338
   703
  hence F: "\<And>n. ?F n \<noteq> a \<and> \<bar>?F n - a\<bar> < inverse (real (Suc n)) \<and> dist (X (?F n)) L \<ge> r"
huffman@21165
   704
    by (rule someI_ex)
huffman@21165
   705
  hence F1: "\<And>n. ?F n \<noteq> a"
huffman@21165
   706
    and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))"
huffman@31338
   707
    and F3: "\<And>n. dist (X (?F n)) L \<ge> r"
huffman@21165
   708
    by fast+
huffman@21165
   709
kleing@19023
   710
  have "?F ----> a"
huffman@21165
   711
  proof (rule LIMSEQ_I, unfold real_norm_def)
kleing@19023
   712
      fix e::real
kleing@19023
   713
      assume "0 < e"
kleing@19023
   714
        (* choose no such that inverse (real (Suc n)) < e *)
huffman@23441
   715
      then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
kleing@19023
   716
      then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
huffman@21165
   717
      show "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e"
huffman@21165
   718
      proof (intro exI allI impI)
kleing@19023
   719
        fix n
kleing@19023
   720
        assume mlen: "m \<le> n"
huffman@21165
   721
        have "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
huffman@21165
   722
          by (rule F2)
huffman@21165
   723
        also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
huffman@23441
   724
          using mlen by auto
huffman@21165
   725
        also from nodef have
kleing@19023
   726
          "inverse (real (Suc m)) < e" .
huffman@21165
   727
        finally show "\<bar>?F n - a\<bar> < e" .
huffman@21165
   728
      qed
kleing@19023
   729
  qed
kleing@19023
   730
  
kleing@19023
   731
  moreover have "\<forall>n. ?F n \<noteq> a"
huffman@21165
   732
    by (rule allI) (rule F1)
huffman@21165
   733
kleing@19023
   734
  moreover from prems have "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by simp
kleing@19023
   735
  ultimately have "(\<lambda>n. X (?F n)) ----> L" by simp
kleing@19023
   736
  
kleing@19023
   737
  moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
kleing@19023
   738
  proof -
kleing@19023
   739
    {
kleing@19023
   740
      fix no::nat
kleing@19023
   741
      obtain n where "n = no + 1" by simp
kleing@19023
   742
      then have nolen: "no \<le> n" by simp
kleing@19023
   743
        (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
huffman@31338
   744
      have "dist (X (?F n)) L \<ge> r"
huffman@21165
   745
        by (rule F3)
huffman@31338
   746
      with nolen have "\<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r" by fast
kleing@19023
   747
    }
huffman@31338
   748
    then have "(\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r)" by simp
huffman@31338
   749
    with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> e)" by auto
huffman@31338
   750
    thus ?thesis by (unfold LIMSEQ_def, auto simp add: not_less)
kleing@19023
   751
  qed
kleing@19023
   752
  ultimately show False by simp
kleing@19023
   753
qed
kleing@19023
   754
kleing@19023
   755
lemma LIMSEQ_SEQ_conv:
huffman@20561
   756
  "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::real) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
huffman@20561
   757
   (X -- a --> L)"
kleing@19023
   758
proof
kleing@19023
   759
  assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
huffman@23441
   760
  thus "X -- a --> L" by (rule LIMSEQ_SEQ_conv2)
kleing@19023
   761
next
kleing@19023
   762
  assume "(X -- a --> L)"
huffman@23441
   763
  thus "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by (rule LIMSEQ_SEQ_conv1)
kleing@19023
   764
qed
kleing@19023
   765
paulson@10751
   766
end