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