src/HOL/Lim.thy
author huffman
Fri Aug 19 15:54:43 2011 -0700 (2011-08-19)
changeset 44314 dbad46932536
parent 44312 471ff02a8574
child 44532 a2e9b39df938
permissions -rw-r--r--
Lim.thy: legacy theorems
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
huffman@36661
    15
abbreviation
huffman@36662
    16
  LIM :: "['a::topological_space \<Rightarrow> 'b::topological_space, 'a, 'b] \<Rightarrow> bool"
wenzelm@21404
    17
        ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
huffman@36661
    18
  "f -- a --> L \<equiv> (f ---> L) (at a)"
paulson@10751
    19
wenzelm@21404
    20
definition
huffman@36662
    21
  isCont :: "['a::topological_space \<Rightarrow> 'b::topological_space, 'a] \<Rightarrow> bool" where
wenzelm@19765
    22
  "isCont f a = (f -- a --> (f a))"
paulson@10751
    23
wenzelm@21404
    24
definition
huffman@31338
    25
  isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
haftmann@37767
    26
  "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
paulson@10751
    27
huffman@31392
    28
subsection {* Limits of Functions *}
huffman@31349
    29
huffman@36661
    30
lemma LIM_def: "f -- a --> L =
huffman@36661
    31
     (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
huffman@36661
    32
        --> dist (f x) L < r)"
huffman@36661
    33
unfolding tendsto_iff eventually_at ..
paulson@10751
    34
huffman@31338
    35
lemma metric_LIM_I:
huffman@31338
    36
  "(\<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
    37
    \<Longrightarrow> f -- a --> L"
huffman@31338
    38
by (simp add: LIM_def)
huffman@31338
    39
huffman@31338
    40
lemma metric_LIM_D:
huffman@31338
    41
  "\<lbrakk>f -- a --> L; 0 < r\<rbrakk>
huffman@31338
    42
    \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r"
huffman@31338
    43
by (simp add: LIM_def)
paulson@14477
    44
paulson@14477
    45
lemma LIM_eq:
huffman@31338
    46
  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
huffman@31338
    47
  shows "f -- a --> L =
huffman@20561
    48
     (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
huffman@31338
    49
by (simp add: LIM_def dist_norm)
paulson@14477
    50
huffman@20552
    51
lemma LIM_I:
huffman@31338
    52
  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
huffman@31338
    53
  shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
huffman@20552
    54
      ==> f -- a --> L"
huffman@20552
    55
by (simp add: LIM_eq)
huffman@20552
    56
paulson@14477
    57
lemma LIM_D:
huffman@31338
    58
  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
huffman@31338
    59
  shows "[| f -- a --> L; 0<r |]
huffman@20561
    60
      ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
paulson@14477
    61
by (simp add: LIM_eq)
paulson@14477
    62
huffman@31338
    63
lemma LIM_offset:
huffman@36662
    64
  fixes a :: "'a::real_normed_vector"
huffman@31338
    65
  shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
huffman@36662
    66
apply (rule topological_tendstoI)
huffman@36662
    67
apply (drule (2) topological_tendstoD)
huffman@36662
    68
apply (simp only: eventually_at dist_norm)
huffman@36662
    69
apply (clarify, rule_tac x=d in exI, safe)
huffman@20756
    70
apply (drule_tac x="x + k" in spec)
nipkow@29667
    71
apply (simp add: algebra_simps)
huffman@20756
    72
done
huffman@20756
    73
huffman@31338
    74
lemma LIM_offset_zero:
huffman@36662
    75
  fixes a :: "'a::real_normed_vector"
huffman@31338
    76
  shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
huffman@21239
    77
by (drule_tac k="a" in LIM_offset, simp add: add_commute)
huffman@21239
    78
huffman@31338
    79
lemma LIM_offset_zero_cancel:
huffman@36662
    80
  fixes a :: "'a::real_normed_vector"
huffman@31338
    81
  shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
huffman@21239
    82
by (drule_tac k="- a" in LIM_offset, simp)
huffman@21239
    83
hoelzl@32650
    84
lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
hoelzl@32650
    85
huffman@31338
    86
lemma LIM_zero:
huffman@36662
    87
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
    88
  shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"
huffman@36662
    89
unfolding tendsto_iff dist_norm by simp
huffman@21239
    90
huffman@31338
    91
lemma LIM_zero_cancel:
huffman@36662
    92
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
    93
  shows "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l"
huffman@36662
    94
unfolding tendsto_iff dist_norm by simp
huffman@21239
    95
huffman@31338
    96
lemma LIM_zero_iff:
huffman@31338
    97
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
    98
  shows "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l"
huffman@36662
    99
unfolding tendsto_iff dist_norm by simp
huffman@21399
   100
huffman@31338
   101
lemma metric_LIM_imp_LIM:
huffman@21257
   102
  assumes f: "f -- a --> l"
huffman@31338
   103
  assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
huffman@21257
   104
  shows "g -- a --> m"
huffman@44251
   105
  by (rule metric_tendsto_imp_tendsto [OF f],
huffman@44251
   106
    auto simp add: eventually_at_topological le)
huffman@21257
   107
huffman@31338
   108
lemma LIM_imp_LIM:
huffman@36662
   109
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
huffman@36662
   110
  fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
huffman@31338
   111
  assumes f: "f -- a --> l"
huffman@31338
   112
  assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
huffman@31338
   113
  shows "g -- a --> m"
huffman@44251
   114
  by (rule metric_LIM_imp_LIM [OF f],
huffman@44251
   115
    simp add: dist_norm le)
huffman@31338
   116
huffman@44205
   117
lemma trivial_limit_at:
huffman@36662
   118
  fixes a :: "'a::real_normed_algebra_1"
huffman@44205
   119
  shows "\<not> trivial_limit (at a)"  -- {* TODO: find a more appropriate class *}
huffman@44205
   120
unfolding trivial_limit_def
huffman@36662
   121
unfolding eventually_at dist_norm
huffman@36662
   122
by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp)
huffman@36662
   123
huffman@20561
   124
lemma LIM_const_not_eq:
huffman@23076
   125
  fixes a :: "'a::real_normed_algebra_1"
huffman@44205
   126
  fixes k L :: "'b::t2_space"
huffman@23076
   127
  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
huffman@44205
   128
by (simp add: tendsto_const_iff trivial_limit_at)
paulson@14477
   129
huffman@21786
   130
lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
huffman@21786
   131
huffman@20561
   132
lemma LIM_const_eq:
huffman@23076
   133
  fixes a :: "'a::real_normed_algebra_1"
huffman@44205
   134
  fixes k L :: "'b::t2_space"
huffman@23076
   135
  shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
huffman@44205
   136
  by (simp add: tendsto_const_iff trivial_limit_at)
paulson@14477
   137
huffman@20561
   138
lemma LIM_unique:
huffman@31338
   139
  fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}
huffman@44205
   140
  fixes L M :: "'b::t2_space"
huffman@23076
   141
  shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
huffman@44205
   142
  using trivial_limit_at by (rule tendsto_unique)
paulson@14477
   143
paulson@14477
   144
text{*Limits are equal for functions equal except at limit point*}
paulson@14477
   145
lemma LIM_equal:
paulson@14477
   146
     "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"
huffman@36662
   147
unfolding tendsto_def eventually_at_topological by simp
paulson@14477
   148
huffman@20796
   149
lemma LIM_cong:
huffman@20796
   150
  "\<lbrakk>a = b; \<And>x. x \<noteq> b \<Longrightarrow> f x = g x; l = m\<rbrakk>
huffman@21399
   151
   \<Longrightarrow> ((\<lambda>x. f x) -- a --> l) = ((\<lambda>x. g x) -- b --> m)"
huffman@36662
   152
by (simp add: LIM_equal)
huffman@20796
   153
huffman@31338
   154
lemma metric_LIM_equal2:
huffman@21282
   155
  assumes 1: "0 < R"
huffman@31338
   156
  assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x"
huffman@21282
   157
  shows "g -- a --> l \<Longrightarrow> f -- a --> l"
huffman@36662
   158
apply (rule topological_tendstoI)
huffman@36662
   159
apply (drule (2) topological_tendstoD)
huffman@36662
   160
apply (simp add: eventually_at, safe)
huffman@36662
   161
apply (rule_tac x="min d R" in exI, safe)
huffman@21282
   162
apply (simp add: 1)
huffman@21282
   163
apply (simp add: 2)
huffman@21282
   164
done
huffman@21282
   165
huffman@31338
   166
lemma LIM_equal2:
huffman@36662
   167
  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
huffman@31338
   168
  assumes 1: "0 < R"
huffman@31338
   169
  assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
huffman@31338
   170
  shows "g -- a --> l \<Longrightarrow> f -- a --> l"
huffman@36662
   171
by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
huffman@31338
   172
huffman@36662
   173
lemma LIM_compose_eventually:
huffman@36662
   174
  assumes f: "f -- a --> b"
huffman@36662
   175
  assumes g: "g -- b --> c"
huffman@36662
   176
  assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)"
huffman@36662
   177
  shows "(\<lambda>x. g (f x)) -- a --> c"
huffman@44253
   178
  using g f inj by (rule tendsto_compose_eventually)
huffman@21239
   179
huffman@31338
   180
lemma metric_LIM_compose2:
huffman@31338
   181
  assumes f: "f -- a --> b"
huffman@31338
   182
  assumes g: "g -- b --> c"
huffman@31338
   183
  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
huffman@31338
   184
  shows "(\<lambda>x. g (f x)) -- a --> c"
huffman@44314
   185
  using g f inj [folded eventually_at]
huffman@44314
   186
  by (rule tendsto_compose_eventually)
huffman@31338
   187
huffman@23040
   188
lemma LIM_compose2:
huffman@31338
   189
  fixes a :: "'a::real_normed_vector"
huffman@23040
   190
  assumes f: "f -- a --> b"
huffman@23040
   191
  assumes g: "g -- b --> c"
huffman@23040
   192
  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
huffman@23040
   193
  shows "(\<lambda>x. g (f x)) -- a --> c"
huffman@31338
   194
by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
huffman@23040
   195
huffman@21239
   196
lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
huffman@44314
   197
  unfolding o_def by (rule tendsto_compose)
huffman@21239
   198
huffman@21282
   199
lemma real_LIM_sandwich_zero:
huffman@36662
   200
  fixes f g :: "'a::topological_space \<Rightarrow> real"
huffman@21282
   201
  assumes f: "f -- a --> 0"
huffman@21282
   202
  assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
huffman@21282
   203
  assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
huffman@21282
   204
  shows "g -- a --> 0"
huffman@21282
   205
proof (rule LIM_imp_LIM [OF f])
huffman@21282
   206
  fix x assume x: "x \<noteq> a"
huffman@21282
   207
  have "norm (g x - 0) = g x" by (simp add: 1 x)
huffman@21282
   208
  also have "g x \<le> f x" by (rule 2 [OF x])
huffman@21282
   209
  also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)
huffman@21282
   210
  also have "\<bar>f x\<bar> = norm (f x - 0)" by simp
huffman@21282
   211
  finally show "norm (g x - 0) \<le> norm (f x - 0)" .
huffman@21282
   212
qed
huffman@21282
   213
huffman@22442
   214
text {* Bounded Linear Operators *}
huffman@21282
   215
huffman@21282
   216
lemma (in bounded_linear) LIM:
huffman@21282
   217
  "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
huffman@36661
   218
by (rule tendsto)
huffman@31349
   219
huffman@21282
   220
lemma (in bounded_linear) LIM_zero:
huffman@21282
   221
  "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
huffman@44194
   222
  by (rule tendsto_zero)
huffman@21282
   223
huffman@22442
   224
text {* Bounded Bilinear Operators *}
huffman@21282
   225
huffman@31349
   226
lemma (in bounded_bilinear) LIM:
huffman@31349
   227
  "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
huffman@36661
   228
by (rule tendsto)
huffman@31349
   229
huffman@21282
   230
lemma (in bounded_bilinear) LIM_prod_zero:
huffman@31338
   231
  fixes a :: "'d::metric_space"
huffman@21282
   232
  assumes f: "f -- a --> 0"
huffman@21282
   233
  assumes g: "g -- a --> 0"
huffman@21282
   234
  shows "(\<lambda>x. f x ** g x) -- a --> 0"
huffman@44194
   235
  using f g by (rule tendsto_zero)
huffman@21282
   236
huffman@21282
   237
lemma (in bounded_bilinear) LIM_left_zero:
huffman@21282
   238
  "f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0"
huffman@44194
   239
  by (rule tendsto_left_zero)
huffman@21282
   240
huffman@21282
   241
lemma (in bounded_bilinear) LIM_right_zero:
huffman@21282
   242
  "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
huffman@44194
   243
  by (rule tendsto_right_zero)
huffman@21282
   244
huffman@44282
   245
lemmas LIM_mult_zero =
huffman@44282
   246
  bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult]
huffman@21282
   247
huffman@44282
   248
lemmas LIM_mult_left_zero =
huffman@44282
   249
  bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult]
huffman@21282
   250
huffman@44282
   251
lemmas LIM_mult_right_zero =
huffman@44282
   252
  bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult]
huffman@21282
   253
huffman@22637
   254
lemma LIM_inverse_fun:
huffman@22637
   255
  assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)"
huffman@22637
   256
  shows "inverse -- a --> inverse a"
huffman@44314
   257
  by (rule tendsto_inverse [OF tendsto_ident_at a])
huffman@29885
   258
paulson@14477
   259
huffman@20755
   260
subsection {* Continuity *}
paulson@14477
   261
huffman@31338
   262
lemma LIM_isCont_iff:
huffman@36665
   263
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
huffman@31338
   264
  shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
huffman@21239
   265
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
huffman@21239
   266
huffman@31338
   267
lemma isCont_iff:
huffman@36665
   268
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
huffman@31338
   269
  shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
huffman@21239
   270
by (simp add: isCont_def LIM_isCont_iff)
huffman@21239
   271
huffman@23069
   272
lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a"
huffman@44314
   273
  unfolding isCont_def by (rule tendsto_ident_at)
huffman@21239
   274
huffman@21786
   275
lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
huffman@44314
   276
  unfolding isCont_def by (rule tendsto_const)
huffman@21239
   277
huffman@44233
   278
lemma isCont_norm [simp]:
huffman@36665
   279
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   280
  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
huffman@44314
   281
  unfolding isCont_def by (rule tendsto_norm)
huffman@21786
   282
huffman@44233
   283
lemma isCont_rabs [simp]:
huffman@44233
   284
  fixes f :: "'a::topological_space \<Rightarrow> real"
huffman@44233
   285
  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
huffman@44314
   286
  unfolding isCont_def by (rule tendsto_rabs)
huffman@22627
   287
huffman@44233
   288
lemma isCont_add [simp]:
huffman@36665
   289
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   290
  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
huffman@44314
   291
  unfolding isCont_def by (rule tendsto_add)
huffman@21239
   292
huffman@44233
   293
lemma isCont_minus [simp]:
huffman@36665
   294
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   295
  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
huffman@44314
   296
  unfolding isCont_def by (rule tendsto_minus)
huffman@21239
   297
huffman@44233
   298
lemma isCont_diff [simp]:
huffman@36665
   299
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   300
  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
huffman@44314
   301
  unfolding isCont_def by (rule tendsto_diff)
huffman@21239
   302
huffman@44233
   303
lemma isCont_mult [simp]:
huffman@36665
   304
  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
huffman@21786
   305
  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
huffman@44314
   306
  unfolding isCont_def by (rule tendsto_mult)
huffman@21239
   307
huffman@44233
   308
lemma isCont_inverse [simp]:
huffman@36665
   309
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
huffman@21786
   310
  shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
huffman@44314
   311
  unfolding isCont_def by (rule tendsto_inverse)
huffman@21239
   312
huffman@44233
   313
lemma isCont_divide [simp]:
huffman@44233
   314
  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
huffman@44233
   315
  shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a"
huffman@44233
   316
  unfolding isCont_def by (rule tendsto_divide)
huffman@44233
   317
huffman@44310
   318
lemma isCont_tendsto_compose:
huffman@44310
   319
  "\<lbrakk>isCont g l; (f ---> l) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
huffman@44310
   320
  unfolding isCont_def by (rule tendsto_compose)
huffman@44310
   321
huffman@31338
   322
lemma metric_isCont_LIM_compose2:
huffman@31338
   323
  assumes f [unfolded isCont_def]: "isCont f a"
huffman@31338
   324
  assumes g: "g -- f a --> l"
huffman@31338
   325
  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a"
huffman@31338
   326
  shows "(\<lambda>x. g (f x)) -- a --> l"
huffman@31338
   327
by (rule metric_LIM_compose2 [OF f g inj])
huffman@31338
   328
huffman@23040
   329
lemma isCont_LIM_compose2:
huffman@31338
   330
  fixes a :: "'a::real_normed_vector"
huffman@23040
   331
  assumes f [unfolded isCont_def]: "isCont f a"
huffman@23040
   332
  assumes g: "g -- f a --> l"
huffman@23040
   333
  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
huffman@23040
   334
  shows "(\<lambda>x. g (f x)) -- a --> l"
huffman@23040
   335
by (rule LIM_compose2 [OF f g inj])
huffman@23040
   336
huffman@21239
   337
lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
huffman@44314
   338
  unfolding isCont_def by (rule tendsto_compose)
huffman@21239
   339
huffman@21239
   340
lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a"
huffman@21282
   341
  unfolding o_def by (rule isCont_o2)
huffman@21282
   342
huffman@44233
   343
lemma (in bounded_linear) isCont:
huffman@44233
   344
  "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
huffman@44314
   345
  unfolding isCont_def by (rule tendsto)
huffman@21282
   346
huffman@21282
   347
lemma (in bounded_bilinear) isCont:
huffman@21282
   348
  "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
huffman@44314
   349
  unfolding isCont_def by (rule tendsto)
huffman@21282
   350
huffman@44282
   351
lemmas isCont_scaleR [simp] =
huffman@44282
   352
  bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
huffman@21239
   353
huffman@44282
   354
lemmas isCont_of_real [simp] =
huffman@44282
   355
  bounded_linear.isCont [OF bounded_linear_of_real]
huffman@22627
   356
huffman@44233
   357
lemma isCont_power [simp]:
huffman@36665
   358
  fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
huffman@22627
   359
  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
huffman@44314
   360
  unfolding isCont_def by (rule tendsto_power)
huffman@22627
   361
huffman@44233
   362
lemma isCont_sgn [simp]:
huffman@36665
   363
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
huffman@31338
   364
  shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
huffman@44314
   365
  unfolding isCont_def by (rule tendsto_sgn)
huffman@29885
   366
huffman@44233
   367
lemma isCont_setsum [simp]:
huffman@44233
   368
  fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
huffman@44233
   369
  fixes A :: "'a set"
huffman@44233
   370
  shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
huffman@44233
   371
  unfolding isCont_def by (simp add: tendsto_setsum)
paulson@15228
   372
huffman@44233
   373
lemmas isCont_intros =
huffman@44233
   374
  isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
huffman@44233
   375
  isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
huffman@44233
   376
  isCont_of_real isCont_power isCont_sgn isCont_setsum
hoelzl@29803
   377
hoelzl@29803
   378
lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
hoelzl@29803
   379
  and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"
hoelzl@29803
   380
  shows "0 \<le> f x"
hoelzl@29803
   381
proof (rule ccontr)
hoelzl@29803
   382
  assume "\<not> 0 \<le> f x" hence "f x < 0" by auto
hoelzl@29803
   383
  hence "0 < - f x / 2" by auto
hoelzl@29803
   384
  from isCont[unfolded isCont_def, THEN LIM_D, OF this]
hoelzl@29803
   385
  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
   386
hoelzl@29803
   387
  let ?x = "x - min (s / 2) ((x - b) / 2)"
hoelzl@29803
   388
  have "?x < x" and "\<bar> ?x - x \<bar> < s"
hoelzl@29803
   389
    using `b < x` and `0 < s` by auto
hoelzl@29803
   390
  have "b < ?x"
hoelzl@29803
   391
  proof (cases "s < x - b")
hoelzl@29803
   392
    case True thus ?thesis using `0 < s` by auto
hoelzl@29803
   393
  next
hoelzl@29803
   394
    case False hence "s / 2 \<ge> (x - b) / 2" by auto
haftmann@32642
   395
    hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2)
hoelzl@29803
   396
    thus ?thesis using `b < x` by auto
hoelzl@29803
   397
  qed
hoelzl@29803
   398
  hence "0 \<le> f ?x" using all_le `?x < x` by auto
hoelzl@29803
   399
  moreover have "\<bar>f ?x - f x\<bar> < - f x / 2"
hoelzl@29803
   400
    using s_D[OF _ `\<bar> ?x - x \<bar> < s`] `?x < x` by auto
hoelzl@29803
   401
  hence "f ?x - f x < - f x / 2" by auto
hoelzl@29803
   402
  hence "f ?x < f x / 2" by auto
hoelzl@29803
   403
  hence "f ?x < 0" using `f x < 0` by auto
hoelzl@29803
   404
  thus False using `0 \<le> f ?x` by auto
hoelzl@29803
   405
qed
huffman@31338
   406
paulson@14477
   407
huffman@20755
   408
subsection {* Uniform Continuity *}
huffman@20755
   409
paulson@14477
   410
lemma isUCont_isCont: "isUCont f ==> isCont f x"
huffman@23012
   411
by (simp add: isUCont_def isCont_def LIM_def, force)
paulson@14477
   412
huffman@23118
   413
lemma isUCont_Cauchy:
huffman@23118
   414
  "\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
huffman@23118
   415
unfolding isUCont_def
huffman@31338
   416
apply (rule metric_CauchyI)
huffman@23118
   417
apply (drule_tac x=e in spec, safe)
huffman@31338
   418
apply (drule_tac e=s in metric_CauchyD, safe)
huffman@23118
   419
apply (rule_tac x=M in exI, simp)
huffman@23118
   420
done
huffman@23118
   421
huffman@23118
   422
lemma (in bounded_linear) isUCont: "isUCont f"
huffman@31338
   423
unfolding isUCont_def dist_norm
huffman@23118
   424
proof (intro allI impI)
huffman@23118
   425
  fix r::real assume r: "0 < r"
huffman@23118
   426
  obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
huffman@23118
   427
    using pos_bounded by fast
huffman@23118
   428
  show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
huffman@23118
   429
  proof (rule exI, safe)
huffman@23118
   430
    from r K show "0 < r / K" by (rule divide_pos_pos)
huffman@23118
   431
  next
huffman@23118
   432
    fix x y :: 'a
huffman@23118
   433
    assume xy: "norm (x - y) < r / K"
huffman@23118
   434
    have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
huffman@23118
   435
    also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le)
huffman@23118
   436
    also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq)
huffman@23118
   437
    finally show "norm (f x - f y) < r" .
huffman@23118
   438
  qed
huffman@23118
   439
qed
huffman@23118
   440
huffman@23118
   441
lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
huffman@23118
   442
by (rule isUCont [THEN isUCont_Cauchy])
huffman@23118
   443
paulson@14477
   444
huffman@21165
   445
subsection {* Relation of LIM and LIMSEQ *}
kleing@19023
   446
kleing@19023
   447
lemma LIMSEQ_SEQ_conv1:
huffman@44254
   448
  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
huffman@44254
   449
  assumes f: "f -- a --> l"
huffman@44254
   450
  shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
huffman@44254
   451
  using tendsto_compose_eventually [OF f, where F=sequentially] by simp
huffman@31338
   452
huffman@44254
   453
lemma LIMSEQ_SEQ_conv2_lemma:
huffman@44254
   454
  fixes a :: "'a::metric_space"
huffman@44254
   455
  assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> eventually (\<lambda>x. P (S x)) sequentially"
huffman@44254
   456
  shows "eventually P (at a)"
kleing@19023
   457
proof (rule ccontr)
huffman@44254
   458
  let ?I = "\<lambda>n. inverse (real (Suc n))"
huffman@44254
   459
  let ?F = "\<lambda>n::nat. SOME x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
huffman@44254
   460
  assume "\<not> eventually P (at a)"
huffman@44254
   461
  hence P: "\<forall>d>0. \<exists>x. x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
huffman@44254
   462
    unfolding eventually_at by simp
huffman@44254
   463
  hence "\<And>n. \<exists>x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
huffman@44254
   464
  hence F: "\<And>n. ?F n \<noteq> a \<and> dist (?F n) a < ?I n \<and> \<not> P (?F n)"
huffman@21165
   465
    by (rule someI_ex)
huffman@21165
   466
  hence F1: "\<And>n. ?F n \<noteq> a"
huffman@44254
   467
    and F2: "\<And>n. dist (?F n) a < ?I n"
huffman@44254
   468
    and F3: "\<And>n. \<not> P (?F n)"
huffman@21165
   469
    by fast+
kleing@19023
   470
  have "?F ----> a"
huffman@44254
   471
    using LIMSEQ_inverse_real_of_nat
huffman@44254
   472
    by (rule metric_tendsto_imp_tendsto,
huffman@44254
   473
      simp add: dist_norm F2 [THEN less_imp_le])
kleing@19023
   474
  moreover have "\<forall>n. ?F n \<noteq> a"
huffman@21165
   475
    by (rule allI) (rule F1)
huffman@44254
   476
  ultimately have "eventually (\<lambda>n. P (?F n)) sequentially"
huffman@44254
   477
    using assms by simp
huffman@44254
   478
  thus "False" by (simp add: F3)
kleing@19023
   479
qed
kleing@19023
   480
huffman@44254
   481
lemma LIMSEQ_SEQ_conv2:
huffman@44254
   482
  fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
huffman@44254
   483
  assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
huffman@44254
   484
  shows "f -- a --> l"
huffman@44254
   485
  using assms unfolding tendsto_def [where l=l]
huffman@44254
   486
  by (simp add: LIMSEQ_SEQ_conv2_lemma)
huffman@44254
   487
kleing@19023
   488
lemma LIMSEQ_SEQ_conv:
huffman@44254
   489
  "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
huffman@44254
   490
   (X -- a --> (L::'b::topological_space))"
huffman@44253
   491
  using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
kleing@19023
   492
huffman@44314
   493
subsection {* Legacy theorem names *}
huffman@44314
   494
huffman@44314
   495
lemmas LIM_ident [simp] = tendsto_ident_at
huffman@44314
   496
lemmas LIM_const [simp] = tendsto_const [where F="at x", standard]
huffman@44314
   497
lemmas LIM_add = tendsto_add [where F="at x", standard]
huffman@44314
   498
lemmas LIM_add_zero = tendsto_add_zero [where F="at x", standard]
huffman@44314
   499
lemmas LIM_minus = tendsto_minus [where F="at x", standard]
huffman@44314
   500
lemmas LIM_diff = tendsto_diff [where F="at x", standard]
huffman@44314
   501
lemmas LIM_norm = tendsto_norm [where F="at x", standard]
huffman@44314
   502
lemmas LIM_norm_zero = tendsto_norm_zero [where F="at x", standard]
huffman@44314
   503
lemmas LIM_norm_zero_cancel = tendsto_norm_zero_cancel [where F="at x", standard]
huffman@44314
   504
lemmas LIM_norm_zero_iff = tendsto_norm_zero_iff [where F="at x", standard]
huffman@44314
   505
lemmas LIM_rabs = tendsto_rabs [where F="at x", standard]
huffman@44314
   506
lemmas LIM_rabs_zero = tendsto_rabs_zero [where F="at x", standard]
huffman@44314
   507
lemmas LIM_rabs_zero_cancel = tendsto_rabs_zero_cancel [where F="at x", standard]
huffman@44314
   508
lemmas LIM_rabs_zero_iff = tendsto_rabs_zero_iff [where F="at x", standard]
huffman@44314
   509
lemmas LIM_compose = tendsto_compose [where F="at x", standard]
huffman@44314
   510
lemmas LIM_mult = tendsto_mult [where F="at x", standard]
huffman@44314
   511
lemmas LIM_scaleR = tendsto_scaleR [where F="at x", standard]
huffman@44314
   512
lemmas LIM_of_real = tendsto_of_real [where F="at x", standard]
huffman@44314
   513
lemmas LIM_power = tendsto_power [where F="at x", standard]
huffman@44314
   514
lemmas LIM_inverse = tendsto_inverse [where F="at x", standard]
huffman@44314
   515
lemmas LIM_sgn = tendsto_sgn [where F="at x", standard]
huffman@44314
   516
lemmas isCont_LIM_compose = isCont_tendsto_compose [where F="at x", standard]
huffman@44314
   517
paulson@10751
   518
end