src/HOL/Lim.thy
author hoelzl
Fri, 22 Mar 2013 10:41:43 +0100
changeset 51473 1210309fddab
parent 51472 adb441e4b9e9
child 51478 270b21f3ae0a
permissions -rw-r--r--
move first_countable_topology to the HOL image
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     1
(*  Title       : Lim.thy
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     2
    Author      : Jacques D. Fleuriot
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     3
    Copyright   : 1998  University of Cambridge
14477
cc61fd03e589 conversion of Hyperreal/Lim to new-style
paulson
parents: 14387
diff changeset
     4
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     5
*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     6
21165
8fb49f668511 moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents: 21141
diff changeset
     7
header{* Limits and Continuity *}
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     8
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15086
diff changeset
     9
theory Lim
29197
6d4cb27ed19c adapted HOL source structure to distribution layout
haftmann
parents: 28952
diff changeset
    10
imports SEQ
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15086
diff changeset
    11
begin
14477
cc61fd03e589 conversion of Hyperreal/Lim to new-style
paulson
parents: 14387
diff changeset
    12
31392
69570155ddf8 replace filters with filter bases
huffman
parents: 31355
diff changeset
    13
subsection {* Limits of Functions *}
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents: 31338
diff changeset
    14
14477
cc61fd03e589 conversion of Hyperreal/Lim to new-style
paulson
parents: 14387
diff changeset
    15
lemma LIM_eq:
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    16
  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    17
  shows "f -- a --> L =
20561
6a6d8004322f generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents: 20552
diff changeset
    18
     (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    19
by (simp add: LIM_def dist_norm)
14477
cc61fd03e589 conversion of Hyperreal/Lim to new-style
paulson
parents: 14387
diff changeset
    20
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20432
diff changeset
    21
lemma LIM_I:
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    22
  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    23
  shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20432
diff changeset
    24
      ==> f -- a --> L"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20432
diff changeset
    25
by (simp add: LIM_eq)
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20432
diff changeset
    26
14477
cc61fd03e589 conversion of Hyperreal/Lim to new-style
paulson
parents: 14387
diff changeset
    27
lemma LIM_D:
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    28
  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    29
  shows "[| f -- a --> L; 0<r |]
20561
6a6d8004322f generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents: 20552
diff changeset
    30
      ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
14477
cc61fd03e589 conversion of Hyperreal/Lim to new-style
paulson
parents: 14387
diff changeset
    31
by (simp add: LIM_eq)
cc61fd03e589 conversion of Hyperreal/Lim to new-style
paulson
parents: 14387
diff changeset
    32
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    33
lemma LIM_offset:
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    34
  fixes a :: "'a::real_normed_vector"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    35
  shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    36
apply (rule topological_tendstoI)
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    37
apply (drule (2) topological_tendstoD)
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    38
apply (simp only: eventually_at dist_norm)
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    39
apply (clarify, rule_tac x=d in exI, safe)
20756
fec7f5834ffe more reorganizing sections
huffman
parents: 20755
diff changeset
    40
apply (drule_tac x="x + k" in spec)
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29197
diff changeset
    41
apply (simp add: algebra_simps)
20756
fec7f5834ffe more reorganizing sections
huffman
parents: 20755
diff changeset
    42
done
fec7f5834ffe more reorganizing sections
huffman
parents: 20755
diff changeset
    43
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    44
lemma LIM_offset_zero:
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    45
  fixes a :: "'a::real_normed_vector"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    46
  shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
21239
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
    47
by (drule_tac k="a" in LIM_offset, simp add: add_commute)
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
    48
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    49
lemma LIM_offset_zero_cancel:
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    50
  fixes a :: "'a::real_normed_vector"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    51
  shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
21239
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
    52
by (drule_tac k="- a" in LIM_offset, simp)
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
    53
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    54
lemma LIM_zero:
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    55
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
44570
b93d1b3ee300 generalize LIM_zero lemmas to arbitrary filters
huffman
parents: 44568
diff changeset
    56
  shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    57
unfolding tendsto_iff dist_norm by simp
21239
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
    58
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    59
lemma LIM_zero_cancel:
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    60
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
44570
b93d1b3ee300 generalize LIM_zero lemmas to arbitrary filters
huffman
parents: 44568
diff changeset
    61
  shows "((\<lambda>x. f x - l) ---> 0) F \<Longrightarrow> (f ---> l) F"
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    62
unfolding tendsto_iff dist_norm by simp
21239
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
    63
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    64
lemma LIM_zero_iff:
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    65
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
44570
b93d1b3ee300 generalize LIM_zero lemmas to arbitrary filters
huffman
parents: 44568
diff changeset
    66
  shows "((\<lambda>x. f x - l) ---> 0) F = (f ---> l) F"
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    67
unfolding tendsto_iff dist_norm by simp
21399
700ae58d2273 add lemmas LIM_zero_iff, LIM_norm_zero_iff
huffman
parents: 21282
diff changeset
    68
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    69
lemma LIM_imp_LIM:
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    70
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    71
  fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    72
  assumes f: "f -- a --> l"
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    73
  assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    74
  shows "g -- a --> m"
44251
d101ed3177b6 add lemma metric_tendsto_imp_tendsto
huffman
parents: 44233
diff changeset
    75
  by (rule metric_LIM_imp_LIM [OF f],
d101ed3177b6 add lemma metric_tendsto_imp_tendsto
huffman
parents: 44233
diff changeset
    76
    simp add: dist_norm le)
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    77
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    78
lemma LIM_equal2:
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    79
  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    80
  assumes 1: "0 < R"
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    81
  assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    82
  shows "g -- a --> l \<Longrightarrow> f -- a --> l"
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    83
by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    84
23040
d329182b5966 add lemmas LIM_compose2, isCont_LIM_compose2
huffman
parents: 23012
diff changeset
    85
lemma LIM_compose2:
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    86
  fixes a :: "'a::real_normed_vector"
23040
d329182b5966 add lemmas LIM_compose2, isCont_LIM_compose2
huffman
parents: 23012
diff changeset
    87
  assumes f: "f -- a --> b"
d329182b5966 add lemmas LIM_compose2, isCont_LIM_compose2
huffman
parents: 23012
diff changeset
    88
  assumes g: "g -- b --> c"
d329182b5966 add lemmas LIM_compose2, isCont_LIM_compose2
huffman
parents: 23012
diff changeset
    89
  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
d329182b5966 add lemmas LIM_compose2, isCont_LIM_compose2
huffman
parents: 23012
diff changeset
    90
  shows "(\<lambda>x. g (f x)) -- a --> c"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
    91
by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
23040
d329182b5966 add lemmas LIM_compose2, isCont_LIM_compose2
huffman
parents: 23012
diff changeset
    92
21282
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
    93
lemma real_LIM_sandwich_zero:
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36661
diff changeset
    94
  fixes f g :: "'a::topological_space \<Rightarrow> real"
21282
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
    95
  assumes f: "f -- a --> 0"
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
    96
  assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
    97
  assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
    98
  shows "g -- a --> 0"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents: 50331
diff changeset
    99
proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *)
21282
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
   100
  fix x assume x: "x \<noteq> a"
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
   101
  have "norm (g x - 0) = g x" by (simp add: 1 x)
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
   102
  also have "g x \<le> f x" by (rule 2 [OF x])
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
   103
  also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
   104
  also have "\<bar>f x\<bar> = norm (f x - 0)" by simp
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
   105
  finally show "norm (g x - 0) \<le> norm (f x - 0)" .
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
   106
qed
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
   107
14477
cc61fd03e589 conversion of Hyperreal/Lim to new-style
paulson
parents: 14387
diff changeset
   108
20755
956a0377a408 reorganize sections
huffman
parents: 20754
diff changeset
   109
subsection {* Continuity *}
14477
cc61fd03e589 conversion of Hyperreal/Lim to new-style
paulson
parents: 14387
diff changeset
   110
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
   111
lemma LIM_isCont_iff:
36665
5d37a96de20c generalize more lemmas about limits
huffman
parents: 36662
diff changeset
   112
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
   113
  shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
21239
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
   114
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
   115
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
   116
lemma isCont_iff:
36665
5d37a96de20c generalize more lemmas about limits
huffman
parents: 36662
diff changeset
   117
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
   118
  shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
21239
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
   119
by (simp add: isCont_def LIM_isCont_iff)
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
   120
44233
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   121
lemma isCont_norm [simp]:
36665
5d37a96de20c generalize more lemmas about limits
huffman
parents: 36662
diff changeset
   122
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
   123
  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
44314
dbad46932536 Lim.thy: legacy theorems
huffman
parents: 44312
diff changeset
   124
  unfolding isCont_def by (rule tendsto_norm)
21786
66da6af2b0c9 cleaned up; generalized some proofs
huffman
parents: 21733
diff changeset
   125
44233
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   126
lemma isCont_rabs [simp]:
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   127
  fixes f :: "'a::topological_space \<Rightarrow> real"
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   128
  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
44314
dbad46932536 Lim.thy: legacy theorems
huffman
parents: 44312
diff changeset
   129
  unfolding isCont_def by (rule tendsto_rabs)
22627
2b093ba973bc new LIM/isCont lemmas for abs, of_real, and power
huffman
parents: 22613
diff changeset
   130
44233
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   131
lemma isCont_add [simp]:
36665
5d37a96de20c generalize more lemmas about limits
huffman
parents: 36662
diff changeset
   132
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
   133
  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
44314
dbad46932536 Lim.thy: legacy theorems
huffman
parents: 44312
diff changeset
   134
  unfolding isCont_def by (rule tendsto_add)
21239
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
   135
44233
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   136
lemma isCont_minus [simp]:
36665
5d37a96de20c generalize more lemmas about limits
huffman
parents: 36662
diff changeset
   137
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
   138
  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
44314
dbad46932536 Lim.thy: legacy theorems
huffman
parents: 44312
diff changeset
   139
  unfolding isCont_def by (rule tendsto_minus)
21239
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
   140
44233
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   141
lemma isCont_diff [simp]:
36665
5d37a96de20c generalize more lemmas about limits
huffman
parents: 36662
diff changeset
   142
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
   143
  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
44314
dbad46932536 Lim.thy: legacy theorems
huffman
parents: 44312
diff changeset
   144
  unfolding isCont_def by (rule tendsto_diff)
21239
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
   145
44233
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   146
lemma isCont_mult [simp]:
36665
5d37a96de20c generalize more lemmas about limits
huffman
parents: 36662
diff changeset
   147
  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
21786
66da6af2b0c9 cleaned up; generalized some proofs
huffman
parents: 21733
diff changeset
   148
  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
44314
dbad46932536 Lim.thy: legacy theorems
huffman
parents: 44312
diff changeset
   149
  unfolding isCont_def by (rule tendsto_mult)
21239
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
   150
44233
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   151
lemma isCont_inverse [simp]:
36665
5d37a96de20c generalize more lemmas about limits
huffman
parents: 36662
diff changeset
   152
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
21786
66da6af2b0c9 cleaned up; generalized some proofs
huffman
parents: 21733
diff changeset
   153
  shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
44314
dbad46932536 Lim.thy: legacy theorems
huffman
parents: 44312
diff changeset
   154
  unfolding isCont_def by (rule tendsto_inverse)
21239
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
   155
44233
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   156
lemma isCont_divide [simp]:
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   157
  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   158
  shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a"
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   159
  unfolding isCont_def by (rule tendsto_divide)
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   160
23040
d329182b5966 add lemmas LIM_compose2, isCont_LIM_compose2
huffman
parents: 23012
diff changeset
   161
lemma isCont_LIM_compose2:
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
   162
  fixes a :: "'a::real_normed_vector"
23040
d329182b5966 add lemmas LIM_compose2, isCont_LIM_compose2
huffman
parents: 23012
diff changeset
   163
  assumes f [unfolded isCont_def]: "isCont f a"
d329182b5966 add lemmas LIM_compose2, isCont_LIM_compose2
huffman
parents: 23012
diff changeset
   164
  assumes g: "g -- f a --> l"
d329182b5966 add lemmas LIM_compose2, isCont_LIM_compose2
huffman
parents: 23012
diff changeset
   165
  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
d329182b5966 add lemmas LIM_compose2, isCont_LIM_compose2
huffman
parents: 23012
diff changeset
   166
  shows "(\<lambda>x. g (f x)) -- a --> l"
d329182b5966 add lemmas LIM_compose2, isCont_LIM_compose2
huffman
parents: 23012
diff changeset
   167
by (rule LIM_compose2 [OF f g inj])
d329182b5966 add lemmas LIM_compose2, isCont_LIM_compose2
huffman
parents: 23012
diff changeset
   168
44233
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   169
lemma (in bounded_linear) isCont:
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   170
  "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
44314
dbad46932536 Lim.thy: legacy theorems
huffman
parents: 44312
diff changeset
   171
  unfolding isCont_def by (rule tendsto)
21282
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
   172
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
   173
lemma (in bounded_bilinear) isCont:
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
   174
  "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
44314
dbad46932536 Lim.thy: legacy theorems
huffman
parents: 44312
diff changeset
   175
  unfolding isCont_def by (rule tendsto)
21282
dd647b4d7952 added bounded_linear and bounded_bilinear locales
huffman
parents: 21257
diff changeset
   176
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44254
diff changeset
   177
lemmas isCont_scaleR [simp] =
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44254
diff changeset
   178
  bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
21239
d4fbe2c87ef1 LIM_compose -> isCont_LIM_compose;
huffman
parents: 21165
diff changeset
   179
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44254
diff changeset
   180
lemmas isCont_of_real [simp] =
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44254
diff changeset
   181
  bounded_linear.isCont [OF bounded_linear_of_real]
22627
2b093ba973bc new LIM/isCont lemmas for abs, of_real, and power
huffman
parents: 22613
diff changeset
   182
44233
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   183
lemma isCont_power [simp]:
36665
5d37a96de20c generalize more lemmas about limits
huffman
parents: 36662
diff changeset
   184
  fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
22627
2b093ba973bc new LIM/isCont lemmas for abs, of_real, and power
huffman
parents: 22613
diff changeset
   185
  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
44314
dbad46932536 Lim.thy: legacy theorems
huffman
parents: 44312
diff changeset
   186
  unfolding isCont_def by (rule tendsto_power)
22627
2b093ba973bc new LIM/isCont lemmas for abs, of_real, and power
huffman
parents: 22613
diff changeset
   187
44233
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   188
lemma isCont_sgn [simp]:
36665
5d37a96de20c generalize more lemmas about limits
huffman
parents: 36662
diff changeset
   189
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
   190
  shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
44314
dbad46932536 Lim.thy: legacy theorems
huffman
parents: 44312
diff changeset
   191
  unfolding isCont_def by (rule tendsto_sgn)
29885
379e43e513c2 add lemmas about sgn
huffman
parents: 29803
diff changeset
   192
44233
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   193
lemma isCont_setsum [simp]:
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   194
  fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   195
  fixes A :: "'a set"
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   196
  shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   197
  unfolding isCont_def by (simp add: tendsto_setsum)
15228
4d332d10fa3d revised simprules for division
paulson
parents: 15195
diff changeset
   198
44233
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   199
lemmas isCont_intros =
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   200
  isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   201
  isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
aa74ce315bae add simp rules for isCont
huffman
parents: 44218
diff changeset
   202
  isCont_of_real isCont_power isCont_sgn isCont_setsum
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29667
diff changeset
   203
20755
956a0377a408 reorganize sections
huffman
parents: 20754
diff changeset
   204
subsection {* Uniform Continuity *}
956a0377a408 reorganize sections
huffman
parents: 20754
diff changeset
   205
23118
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   206
lemma (in bounded_linear) isUCont: "isUCont f"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
   207
unfolding isUCont_def dist_norm
23118
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   208
proof (intro allI impI)
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   209
  fix r::real assume r: "0 < r"
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   210
  obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   211
    using pos_bounded by fast
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   212
  show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   213
  proof (rule exI, safe)
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   214
    from r K show "0 < r / K" by (rule divide_pos_pos)
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   215
  next
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   216
    fix x y :: 'a
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   217
    assume xy: "norm (x - y) < r / K"
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   218
    have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   219
    also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le)
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   220
    also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq)
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   221
    finally show "norm (f x - f y) < r" .
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   222
  qed
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   223
qed
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   224
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   225
lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   226
by (rule isUCont [THEN isUCont_Cauchy])
ce3cf072ae14 add isUCont lemmas
huffman
parents: 23076
diff changeset
   227
14477
cc61fd03e589 conversion of Hyperreal/Lim to new-style
paulson
parents: 14387
diff changeset
   228
50331
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 45031
diff changeset
   229
lemma LIM_less_bound: 
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 45031
diff changeset
   230
  fixes f :: "real \<Rightarrow> real"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 45031
diff changeset
   231
  assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 45031
diff changeset
   232
  shows "0 \<le> f x"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 45031
diff changeset
   233
proof (rule tendsto_le_const)
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 45031
diff changeset
   234
  show "(f ---> f x) (at_left x)"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 45031
diff changeset
   235
    using `isCont f x` by (simp add: filterlim_at_split isCont_def)
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 45031
diff changeset
   236
  show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 45031
diff changeset
   237
    using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 45031
diff changeset
   238
qed simp
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 45031
diff changeset
   239
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   240
end