author  huffman 
Tue, 04 May 2010 13:08:56 0700  
changeset 36662  621122eeb138 
parent 36661  0a5b7b818d65 
child 36665  5d37a96de20c 
permissions  rwrr 
10751  1 
(* Title : Lim.thy 
2 
Author : Jacques D. Fleuriot 

3 
Copyright : 1998 University of Cambridge 

14477  4 
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 
10751  5 
*) 
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  8 

15131  9 
theory Lim 
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
28952
diff
changeset

10 
imports SEQ 
15131  11 
begin 
14477  12 

22641
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
22637
diff
changeset

13 
text{*Standard Definitions*} 
10751  14 

36661
0a5b7b818d65
make (f  a > x) an abbreviation for (f > x) (at a)
huffman
parents:
32650
diff
changeset

15 
abbreviation 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

16 
LIM :: "['a::topological_space \<Rightarrow> 'b::topological_space, 'a, 'b] \<Rightarrow> bool" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset

17 
("((_)/  (_)/ > (_))" [60, 0, 60] 60) where 
36661
0a5b7b818d65
make (f  a > x) an abbreviation for (f > x) (at a)
huffman
parents:
32650
diff
changeset

18 
"f  a > L \<equiv> (f > L) (at a)" 
10751  19 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset

20 
definition 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

21 
isCont :: "['a::topological_space \<Rightarrow> 'b::topological_space, 'a] \<Rightarrow> bool" where 
19765  22 
"isCont f a = (f  a > (f a))" 
10751  23 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset

24 
definition 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

25 
isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

26 
[code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)" 
10751  27 

31392  28 
subsection {* Limits of Functions *} 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31338
diff
changeset

29 

36661
0a5b7b818d65
make (f  a > x) an abbreviation for (f > x) (at a)
huffman
parents:
32650
diff
changeset

30 
lemma LIM_def: "f  a > L = 
0a5b7b818d65
make (f  a > x) an abbreviation for (f > x) (at a)
huffman
parents:
32650
diff
changeset

31 
(\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s 
0a5b7b818d65
make (f  a > x) an abbreviation for (f > x) (at a)
huffman
parents:
32650
diff
changeset

32 
> dist (f x) L < r)" 
0a5b7b818d65
make (f  a > x) an abbreviation for (f > x) (at a)
huffman
parents:
32650
diff
changeset

33 
unfolding tendsto_iff eventually_at .. 
10751  34 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

35 
lemma metric_LIM_I: 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

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) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

37 
\<Longrightarrow> f  a > L" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

38 
by (simp add: LIM_def) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

39 

d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

40 
lemma metric_LIM_D: 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

41 
"\<lbrakk>f  a > L; 0 < r\<rbrakk> 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

42 
\<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

43 
by (simp add: LIM_def) 
14477  44 

45 
lemma LIM_eq: 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

46 
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

47 
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

48 
(\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (xa) < s > norm (f x  L) < r)" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

49 
by (simp add: LIM_def dist_norm) 
14477  50 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

51 
lemma LIM_I: 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

52 
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

53 
shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (xa) < s > norm (f x  L) < r) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

54 
==> f  a > L" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

55 
by (simp add: LIM_eq) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

56 

14477  57 
lemma LIM_D: 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

58 
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

59 
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

60 
==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (xa) < s > norm (f x  L) < r" 
14477  61 
by (simp add: LIM_eq) 
62 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

63 
lemma LIM_offset: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

64 
fixes a :: "'a::real_normed_vector" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

65 
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

66 
apply (rule topological_tendstoI) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

67 
apply (drule (2) topological_tendstoD) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

68 
apply (simp only: eventually_at dist_norm) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

69 
apply (clarify, rule_tac x=d in exI, safe) 
20756  70 
apply (drule_tac x="x + k" in spec) 
29667  71 
apply (simp add: algebra_simps) 
20756  72 
done 
73 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

74 
lemma LIM_offset_zero: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

75 
fixes a :: "'a::real_normed_vector" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

76 
shows "f  a > L \<Longrightarrow> (\<lambda>h. f (a + h))  0 > L" 
21239  77 
by (drule_tac k="a" in LIM_offset, simp add: add_commute) 
78 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

79 
lemma LIM_offset_zero_cancel: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

80 
fixes a :: "'a::real_normed_vector" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

81 
shows "(\<lambda>h. f (a + h))  0 > L \<Longrightarrow> f  a > L" 
21239  82 
by (drule_tac k=" a" in LIM_offset, simp) 
83 

15228  84 
lemma LIM_const [simp]: "(%x. k)  x > k" 
36661
0a5b7b818d65
make (f  a > x) an abbreviation for (f > x) (at a)
huffman
parents:
32650
diff
changeset

85 
by (rule tendsto_const) 
14477  86 

32650  87 
lemma LIM_cong_limit: "\<lbrakk> f  x > L ; K = L \<rbrakk> \<Longrightarrow> f  x > K" by simp 
88 

14477  89 
lemma LIM_add: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

90 
fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" 
14477  91 
assumes f: "f  a > L" and g: "g  a > M" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

92 
shows "(\<lambda>x. f x + g x)  a > (L + M)" 
36661
0a5b7b818d65
make (f  a > x) an abbreviation for (f > x) (at a)
huffman
parents:
32650
diff
changeset

93 
using assms by (rule tendsto_add) 
14477  94 

21257  95 
lemma LIM_add_zero: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

96 
fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

97 
shows "\<lbrakk>f  a > 0; g  a > 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x)  a > 0" 
21257  98 
by (drule (1) LIM_add, simp) 
99 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

100 
lemma LIM_minus: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

101 
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

102 
shows "f  a > L \<Longrightarrow> (\<lambda>x.  f x)  a >  L" 
36661
0a5b7b818d65
make (f  a > x) an abbreviation for (f > x) (at a)
huffman
parents:
32650
diff
changeset

103 
by (rule tendsto_minus) 
14477  104 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

105 
(* TODO: delete *) 
14477  106 
lemma LIM_add_minus: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

107 
fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

108 
shows "[ f  x > l; g  x > m ] ==> (%x. f(x) + g(x))  x > (l + m)" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

109 
by (intro LIM_add LIM_minus) 
14477  110 

111 
lemma LIM_diff: 

36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

112 
fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

113 
shows "\<lbrakk>f  x > l; g  x > m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x  g x)  x > l  m" 
36661
0a5b7b818d65
make (f  a > x) an abbreviation for (f > x) (at a)
huffman
parents:
32650
diff
changeset

114 
by (rule tendsto_diff) 
14477  115 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

116 
lemma LIM_zero: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

117 
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

118 
shows "f  a > l \<Longrightarrow> (\<lambda>x. f x  l)  a > 0" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

119 
unfolding tendsto_iff dist_norm by simp 
21239  120 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

121 
lemma LIM_zero_cancel: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
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 "(\<lambda>x. f x  l)  a > 0 \<Longrightarrow> f  a > l" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

124 
unfolding tendsto_iff dist_norm by simp 
21239  125 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

126 
lemma LIM_zero_iff: 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

127 
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

128 
shows "(\<lambda>x. f x  l)  a > 0 = f  a > l" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

129 
unfolding tendsto_iff dist_norm by simp 
21399  130 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

131 
lemma metric_LIM_imp_LIM: 
21257  132 
assumes f: "f  a > l" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

133 
assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l" 
21257  134 
shows "g  a > m" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

135 
apply (rule tendstoI, drule tendstoD [OF f]) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

136 
apply (simp add: eventually_at_topological, safe) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

137 
apply (rule_tac x="S" in exI, safe) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

138 
apply (drule_tac x="x" in bspec, safe) 
21257  139 
apply (erule (1) order_le_less_trans [OF le]) 
140 
done 

141 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

142 
lemma LIM_imp_LIM: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

143 
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

144 
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

145 
assumes f: "f  a > l" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

146 
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

147 
shows "g  a > m" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

148 
apply (rule metric_LIM_imp_LIM [OF f]) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

149 
apply (simp add: dist_norm le) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

150 
done 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

151 

d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

152 
lemma LIM_norm: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

153 
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

154 
shows "f  a > l \<Longrightarrow> (\<lambda>x. norm (f x))  a > norm l" 
36661
0a5b7b818d65
make (f  a > x) an abbreviation for (f > x) (at a)
huffman
parents:
32650
diff
changeset

155 
by (rule tendsto_norm) 
21257  156 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

157 
lemma LIM_norm_zero: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

158 
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

159 
shows "f  a > 0 \<Longrightarrow> (\<lambda>x. norm (f x))  a > 0" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

160 
by (rule tendsto_norm_zero) 
21257  161 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

162 
lemma LIM_norm_zero_cancel: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

163 
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

164 
shows "(\<lambda>x. norm (f x))  a > 0 \<Longrightarrow> f  a > 0" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

165 
by (rule tendsto_norm_zero_cancel) 
21257  166 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

167 
lemma LIM_norm_zero_iff: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

168 
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

169 
shows "(\<lambda>x. norm (f x))  a > 0 = f  a > 0" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

170 
by (rule tendsto_norm_zero_iff) 
21399  171 

22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

172 
lemma LIM_rabs: "f  a > (l::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>)  a > \<bar>l\<bar>" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

173 
by (fold real_norm_def, rule LIM_norm) 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

174 

2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

175 
lemma LIM_rabs_zero: "f  a > (0::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>)  a > 0" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

176 
by (fold real_norm_def, rule LIM_norm_zero) 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

177 

2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

178 
lemma LIM_rabs_zero_cancel: "(\<lambda>x. \<bar>f x\<bar>)  a > (0::real) \<Longrightarrow> f  a > 0" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

179 
by (fold real_norm_def, rule LIM_norm_zero_cancel) 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

180 

2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

181 
lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>)  a > (0::real) = f  a > 0" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

182 
by (fold real_norm_def, rule LIM_norm_zero_iff) 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

183 

36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

184 
lemma at_neq_bot: 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

185 
fixes a :: "'a::real_normed_algebra_1" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

186 
shows "at a \<noteq> bot"  {* TODO: find a more appropriate class *} 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

187 
unfolding eventually_False [symmetric] 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

188 
unfolding eventually_at dist_norm 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

189 
by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

190 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

191 
lemma LIM_const_not_eq: 
23076
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset

192 
fixes a :: "'a::real_normed_algebra_1" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

193 
fixes k L :: "'b::metric_space" 
23076
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset

194 
shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k)  a > L" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

195 
by (simp add: tendsto_const_iff at_neq_bot) 
14477  196 

21786  197 
lemmas LIM_not_zero = LIM_const_not_eq [where L = 0] 
198 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

199 
lemma LIM_const_eq: 
23076
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset

200 
fixes a :: "'a::real_normed_algebra_1" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

201 
fixes k L :: "'b::metric_space" 
23076
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset

202 
shows "(\<lambda>x. k)  a > L \<Longrightarrow> k = L" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

203 
by (simp add: tendsto_const_iff at_neq_bot) 
14477  204 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

205 
lemma LIM_unique: 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

206 
fixes a :: "'a::real_normed_algebra_1"  {* TODO: find a more appropriate class *} 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

207 
fixes L M :: "'b::metric_space" 
23076
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset

208 
shows "\<lbrakk>f  a > L; f  a > M\<rbrakk> \<Longrightarrow> L = M" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

209 
by (drule (1) tendsto_dist, simp add: tendsto_const_iff at_neq_bot) 
14477  210 

23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23040
diff
changeset

211 
lemma LIM_ident [simp]: "(\<lambda>x. x)  a > a" 
36661
0a5b7b818d65
make (f  a > x) an abbreviation for (f > x) (at a)
huffman
parents:
32650
diff
changeset

212 
by (rule tendsto_ident_at) 
14477  213 

214 
text{*Limits are equal for functions equal except at limit point*} 

215 
lemma LIM_equal: 

216 
"[ \<forall>x. x \<noteq> a > (f x = g x) ] ==> (f  a > l) = (g  a > l)" 

36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

217 
unfolding tendsto_def eventually_at_topological by simp 
14477  218 

20796  219 
lemma LIM_cong: 
220 
"\<lbrakk>a = b; \<And>x. x \<noteq> b \<Longrightarrow> f x = g x; l = m\<rbrakk> 

21399  221 
\<Longrightarrow> ((\<lambda>x. f x)  a > l) = ((\<lambda>x. g x)  b > m)" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

222 
by (simp add: LIM_equal) 
20796  223 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

224 
lemma metric_LIM_equal2: 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

225 
assumes 1: "0 < R" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

226 
assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x" 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

227 
shows "g  a > l \<Longrightarrow> f  a > l" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

228 
apply (rule topological_tendstoI) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

229 
apply (drule (2) topological_tendstoD) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

230 
apply (simp add: eventually_at, safe) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

231 
apply (rule_tac x="min d R" in exI, safe) 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

232 
apply (simp add: 1) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

233 
apply (simp add: 2) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

234 
done 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

235 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

236 
lemma LIM_equal2: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

237 
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

238 
assumes 1: "0 < R" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

239 
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

240 
shows "g  a > l \<Longrightarrow> f  a > l" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

241 
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

242 

36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

243 
text{*Two uses in Transcendental.ML*} (* BH: no longer true; delete? *) 
14477  244 
lemma LIM_trans: 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

245 
fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

246 
shows "[ (%x. f(x) + g(x))  a > 0; g  a > l ] ==> f  a > l" 
14477  247 
apply (drule LIM_add, assumption) 
248 
apply (auto simp add: add_assoc) 

249 
done 

250 

21239  251 
lemma LIM_compose: 
252 
assumes g: "g  l > g l" 

253 
assumes f: "f  a > l" 

254 
shows "(\<lambda>x. g (f x))  a > g l" 

36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

255 
proof (rule topological_tendstoI) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

256 
fix C assume C: "open C" "g l \<in> C" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

257 
obtain B where B: "open B" "l \<in> B" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

258 
and gC: "\<And>y. y \<in> B \<Longrightarrow> y \<noteq> l \<Longrightarrow> g y \<in> C" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

259 
using topological_tendstoD [OF g C] 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

260 
unfolding eventually_at_topological by fast 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

261 
obtain A where A: "open A" "a \<in> A" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

262 
and fB: "\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x \<in> B" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

263 
using topological_tendstoD [OF f B] 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

264 
unfolding eventually_at_topological by fast 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

265 
show "eventually (\<lambda>x. g (f x) \<in> C) (at a)" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

266 
unfolding eventually_at_topological 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

267 
proof (intro exI conjI ballI impI) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

268 
show "open A" and "a \<in> A" using A . 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

269 
next 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

270 
fix x assume "x \<in> A" and "x \<noteq> a" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

271 
then show "g (f x) \<in> C" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

272 
by (cases "f x = l", simp add: C, simp add: gC fB) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

273 
qed 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

274 
qed 
21239  275 

36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

276 
lemma LIM_compose_eventually: 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

277 
assumes f: "f  a > b" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

278 
assumes g: "g  b > c" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

279 
assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

280 
shows "(\<lambda>x. g (f x))  a > c" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

281 
proof (rule topological_tendstoI) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

282 
fix C assume C: "open C" "c \<in> C" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

283 
obtain B where B: "open B" "b \<in> B" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

284 
and gC: "\<And>y. y \<in> B \<Longrightarrow> y \<noteq> b \<Longrightarrow> g y \<in> C" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

285 
using topological_tendstoD [OF g C] 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

286 
unfolding eventually_at_topological by fast 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

287 
obtain A where A: "open A" "a \<in> A" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

288 
and fB: "\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x \<in> B" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

289 
using topological_tendstoD [OF f B] 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

290 
unfolding eventually_at_topological by fast 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

291 
have "eventually (\<lambda>x. f x \<noteq> b \<longrightarrow> g (f x) \<in> C) (at a)" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

292 
unfolding eventually_at_topological 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

293 
proof (intro exI conjI ballI impI) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

294 
show "open A" and "a \<in> A" using A . 
21239  295 
next 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

296 
fix x assume "x \<in> A" and "x \<noteq> a" and "f x \<noteq> b" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

297 
then show "g (f x) \<in> C" by (simp add: gC fB) 
21239  298 
qed 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

299 
with inj show "eventually (\<lambda>x. g (f x) \<in> C) (at a)" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

300 
by (rule eventually_rev_mp) 
21239  301 
qed 
302 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

303 
lemma metric_LIM_compose2: 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

304 
assumes f: "f  a > b" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

305 
assumes g: "g  b > c" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

306 
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

307 
shows "(\<lambda>x. g (f x))  a > c" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

308 
using f g inj [folded eventually_at] 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

309 
by (rule LIM_compose_eventually) 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

310 

23040  311 
lemma LIM_compose2: 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

312 
fixes a :: "'a::real_normed_vector" 
23040  313 
assumes f: "f  a > b" 
314 
assumes g: "g  b > c" 

315 
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x  a) < d \<longrightarrow> f x \<noteq> b" 

316 
shows "(\<lambda>x. g (f x))  a > c" 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

317 
by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]]) 
23040  318 

21239  319 
lemma LIM_o: "\<lbrakk>g  l > g l; f  a > l\<rbrakk> \<Longrightarrow> (g \<circ> f)  a > g l" 
320 
unfolding o_def by (rule LIM_compose) 

321 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

322 
lemma real_LIM_sandwich_zero: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

323 
fixes f g :: "'a::topological_space \<Rightarrow> real" 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

324 
assumes f: "f  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

325 
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

326 
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

327 
shows "g  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

328 
proof (rule LIM_imp_LIM [OF f]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

329 
fix x assume x: "x \<noteq> a" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

330 
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

331 
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

332 
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

333 
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

334 
finally show "norm (g x  0) \<le> norm (f x  0)" . 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

335 
qed 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

336 

22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21810
diff
changeset

337 
text {* Bounded Linear Operators *} 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

338 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

339 
lemma (in bounded_linear) LIM: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

340 
"g  a > l \<Longrightarrow> (\<lambda>x. f (g x))  a > f l" 
36661
0a5b7b818d65
make (f  a > x) an abbreviation for (f > x) (at a)
huffman
parents:
32650
diff
changeset

341 
by (rule tendsto) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31338
diff
changeset

342 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31338
diff
changeset

343 
lemma (in bounded_linear) cont: "f  a > f a" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31338
diff
changeset

344 
by (rule LIM [OF LIM_ident]) 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

345 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

346 
lemma (in bounded_linear) LIM_zero: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

347 
"g  a > 0 \<Longrightarrow> (\<lambda>x. f (g x))  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

348 
by (drule LIM, simp only: zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

349 

22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21810
diff
changeset

350 
text {* Bounded Bilinear Operators *} 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

351 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31338
diff
changeset

352 
lemma (in bounded_bilinear) LIM: 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31338
diff
changeset

353 
"\<lbrakk>f  a > L; g  a > M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x)  a > L ** M" 
36661
0a5b7b818d65
make (f  a > x) an abbreviation for (f > x) (at a)
huffman
parents:
32650
diff
changeset

354 
by (rule tendsto) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31338
diff
changeset

355 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

356 
lemma (in bounded_bilinear) LIM_prod_zero: 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

357 
fixes a :: "'d::metric_space" 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

358 
assumes f: "f  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

359 
assumes g: "g  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

360 
shows "(\<lambda>x. f x ** g x)  a > 0" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31338
diff
changeset

361 
using LIM [OF f g] by (simp add: zero_left) 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

362 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

363 
lemma (in bounded_bilinear) LIM_left_zero: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

364 
"f  a > 0 \<Longrightarrow> (\<lambda>x. f x ** c)  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

365 
by (rule bounded_linear.LIM_zero [OF bounded_linear_left]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

366 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

367 
lemma (in bounded_bilinear) LIM_right_zero: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

368 
"f  a > 0 \<Longrightarrow> (\<lambda>x. c ** f x)  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

369 
by (rule bounded_linear.LIM_zero [OF bounded_linear_right]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

370 

23127  371 
lemmas LIM_mult = mult.LIM 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

372 

23127  373 
lemmas LIM_mult_zero = mult.LIM_prod_zero 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

374 

23127  375 
lemmas LIM_mult_left_zero = mult.LIM_left_zero 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

376 

23127  377 
lemmas LIM_mult_right_zero = mult.LIM_right_zero 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

378 

23127  379 
lemmas LIM_scaleR = scaleR.LIM 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

380 

23127  381 
lemmas LIM_of_real = of_real.LIM 
22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

382 

2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

383 
lemma LIM_power: 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

384 
fixes f :: "'a::metric_space \<Rightarrow> 'b::{power,real_normed_algebra}" 
22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

385 
assumes f: "f  a > l" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

386 
shows "(\<lambda>x. f x ^ n)  a > l ^ n" 
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
29885
diff
changeset

387 
by (induct n, simp, simp add: LIM_mult f) 
22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

388 

22641
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
22637
diff
changeset

389 
subsubsection {* Derived theorems about @{term LIM} *} 
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
22637
diff
changeset

390 

31355  391 
lemma LIM_inverse: 
392 
fixes L :: "'a::real_normed_div_algebra" 

393 
shows "\<lbrakk>f  a > L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x))  a > inverse L" 

394 
by (rule tendsto_inverse) 

22637  395 

396 
lemma LIM_inverse_fun: 

397 
assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)" 

398 
shows "inverse  a > inverse a" 

31355  399 
by (rule LIM_inverse [OF LIM_ident a]) 
22637  400 

29885  401 
lemma LIM_sgn: 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

402 
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

403 
shows "\<lbrakk>f  a > l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x))  a > sgn l" 
29885  404 
unfolding sgn_div_norm 
405 
by (simp add: LIM_scaleR LIM_inverse LIM_norm) 

406 

14477  407 

20755  408 
subsection {* Continuity *} 
14477  409 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

410 
lemma LIM_isCont_iff: 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

411 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

412 
shows "(f  a > f a) = ((\<lambda>h. f (a + h))  0 > f a)" 
21239  413 
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) 
414 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

415 
lemma isCont_iff: 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

416 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

417 
shows "isCont f x = (\<lambda>h. f (x + h))  0 > f x" 
21239  418 
by (simp add: isCont_def LIM_isCont_iff) 
419 

23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23040
diff
changeset

420 
lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a" 
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23040
diff
changeset

421 
unfolding isCont_def by (rule LIM_ident) 
21239  422 

21786  423 
lemma isCont_const [simp]: "isCont (\<lambda>x. k) a" 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

424 
unfolding isCont_def by (rule LIM_const) 
21239  425 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

426 
lemma isCont_norm: 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

427 
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

428 
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a" 
21786  429 
unfolding isCont_def by (rule LIM_norm) 
430 

22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

431 
lemma isCont_rabs: "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x :: real\<bar>) a" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

432 
unfolding isCont_def by (rule LIM_rabs) 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

433 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

434 
lemma isCont_add: 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

435 
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

436 
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a" 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

437 
unfolding isCont_def by (rule LIM_add) 
21239  438 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

439 
lemma isCont_minus: 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

440 
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

441 
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x.  f x) a" 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

442 
unfolding isCont_def by (rule LIM_minus) 
21239  443 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

444 
lemma isCont_diff: 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

445 
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

446 
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x  g x) a" 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

447 
unfolding isCont_def by (rule LIM_diff) 
21239  448 

449 
lemma isCont_mult: 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

450 
fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_algebra" 
21786  451 
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a" 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

452 
unfolding isCont_def by (rule LIM_mult) 
21239  453 

454 
lemma isCont_inverse: 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

455 
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_div_algebra" 
21786  456 
shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a" 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

457 
unfolding isCont_def by (rule LIM_inverse) 
21239  458 

459 
lemma isCont_LIM_compose: 

460 
"\<lbrakk>isCont g l; f  a > l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x))  a > g l" 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

461 
unfolding isCont_def by (rule LIM_compose) 
21239  462 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

463 
lemma metric_isCont_LIM_compose2: 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

464 
assumes f [unfolded isCont_def]: "isCont f a" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

465 
assumes g: "g  f a > l" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

466 
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

467 
shows "(\<lambda>x. g (f x))  a > l" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

468 
by (rule metric_LIM_compose2 [OF f g inj]) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

469 

23040  470 
lemma isCont_LIM_compose2: 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

471 
fixes a :: "'a::real_normed_vector" 
23040  472 
assumes f [unfolded isCont_def]: "isCont f a" 
473 
assumes g: "g  f a > l" 

474 
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x  a) < d \<longrightarrow> f x \<noteq> f a" 

475 
shows "(\<lambda>x. g (f x))  a > l" 

476 
by (rule LIM_compose2 [OF f g inj]) 

477 

21239  478 
lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a" 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

479 
unfolding isCont_def by (rule LIM_compose) 
21239  480 

481 
lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a" 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

482 
unfolding o_def by (rule isCont_o2) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

483 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

484 
lemma (in bounded_linear) isCont: "isCont f a" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

485 
unfolding isCont_def by (rule cont) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

486 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

487 
lemma (in bounded_bilinear) isCont: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

488 
"\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

489 
unfolding isCont_def by (rule LIM) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

490 

23127  491 
lemmas isCont_scaleR = scaleR.isCont 
21239  492 

22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

493 
lemma isCont_of_real: 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

494 
"isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a" 
22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

495 
unfolding isCont_def by (rule LIM_of_real) 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

496 

2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

497 
lemma isCont_power: 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

498 
fixes f :: "'a::metric_space \<Rightarrow> 'b::{power,real_normed_algebra}" 
22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

499 
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

500 
unfolding isCont_def by (rule LIM_power) 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

501 

29885  502 
lemma isCont_sgn: 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

503 
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

504 
shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a" 
29885  505 
unfolding isCont_def by (rule LIM_sgn) 
506 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

507 
lemma isCont_abs [simp]: "isCont abs (a::real)" 
23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23040
diff
changeset

508 
by (rule isCont_rabs [OF isCont_ident]) 
15228  509 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

510 
lemma isCont_setsum: 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

511 
fixes f :: "'a \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::real_normed_vector" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

512 
fixes A :: "'a set" assumes "finite A" 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

513 
shows "\<forall> i \<in> A. isCont (f i) x \<Longrightarrow> isCont (\<lambda> x. \<Sum> i \<in> A. f i x) x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

514 
using `finite A` 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

515 
proof induct 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

516 
case (insert a F) show "isCont (\<lambda> x. \<Sum> i \<in> (insert a F). f i x) x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

517 
unfolding setsum_insert[OF `finite F` `a \<notin> F`] by (rule isCont_add, auto simp add: insert) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

518 
qed auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

519 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

520 
lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

521 
and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

522 
shows "0 \<le> f x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

523 
proof (rule ccontr) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

524 
assume "\<not> 0 \<le> f x" hence "f x < 0" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

525 
hence "0 <  f x / 2" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

526 
from isCont[unfolded isCont_def, THEN LIM_D, OF this] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

527 
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 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

528 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

529 
let ?x = "x  min (s / 2) ((x  b) / 2)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

530 
have "?x < x" and "\<bar> ?x  x \<bar> < s" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

531 
using `b < x` and `0 < s` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

532 
have "b < ?x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

533 
proof (cases "s < x  b") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

534 
case True thus ?thesis using `0 < s` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

535 
next 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

536 
case False hence "s / 2 \<ge> (x  b) / 2" by auto 
32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32436
diff
changeset

537 
hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2) 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

538 
thus ?thesis using `b < x` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

539 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

540 
hence "0 \<le> f ?x" using all_le `?x < x` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

541 
moreover have "\<bar>f ?x  f x\<bar> <  f x / 2" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

542 
using s_D[OF _ `\<bar> ?x  x \<bar> < s`] `?x < x` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

543 
hence "f ?x  f x <  f x / 2" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

544 
hence "f ?x < f x / 2" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

545 
hence "f ?x < 0" using `f x < 0` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

546 
thus False using `0 \<le> f ?x` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

547 
qed 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

548 

14477  549 

20755  550 
subsection {* Uniform Continuity *} 
551 

14477  552 
lemma isUCont_isCont: "isUCont f ==> isCont f x" 
23012  553 
by (simp add: isUCont_def isCont_def LIM_def, force) 
14477  554 

23118  555 
lemma isUCont_Cauchy: 
556 
"\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))" 

557 
unfolding isUCont_def 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

558 
apply (rule metric_CauchyI) 
23118  559 
apply (drule_tac x=e in spec, safe) 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

560 
apply (drule_tac e=s in metric_CauchyD, safe) 
23118  561 
apply (rule_tac x=M in exI, simp) 
562 
done 

563 

564 
lemma (in bounded_linear) isUCont: "isUCont f" 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

565 
unfolding isUCont_def dist_norm 
23118  566 
proof (intro allI impI) 
567 
fix r::real assume r: "0 < r" 

568 
obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K" 

569 
using pos_bounded by fast 

570 
show "\<exists>s>0. \<forall>x y. norm (x  y) < s \<longrightarrow> norm (f x  f y) < r" 

571 
proof (rule exI, safe) 

572 
from r K show "0 < r / K" by (rule divide_pos_pos) 

573 
next 

574 
fix x y :: 'a 

575 
assume xy: "norm (x  y) < r / K" 

576 
have "norm (f x  f y) = norm (f (x  y))" by (simp only: diff) 

577 
also have "\<dots> \<le> norm (x  y) * K" by (rule norm_le) 

578 
also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq) 

579 
finally show "norm (f x  f y) < r" . 

580 
qed 

581 
qed 

582 

583 
lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))" 

584 
by (rule isUCont [THEN isUCont_Cauchy]) 

585 

14477  586 

21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

587 
subsection {* Relation of LIM and LIMSEQ *} 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

588 

5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

589 
lemma LIMSEQ_SEQ_conv1: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

590 
fixes a :: "'a::metric_space" and L :: "'b::metric_space" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

591 
assumes X: "X  a > L" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

592 
shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

593 
proof (safe intro!: metric_LIMSEQ_I) 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

594 
fix S :: "nat \<Rightarrow> 'a" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

595 
fix r :: real 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

596 
assume rgz: "0 < r" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

597 
assume as: "\<forall>n. S n \<noteq> a" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

598 
assume S: "S > a" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

599 
from metric_LIM_D [OF X rgz] obtain s 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

600 
where sgz: "0 < s" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

601 
and aux: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < s\<rbrakk> \<Longrightarrow> dist (X x) L < r" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

602 
by fast 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

603 
from metric_LIMSEQ_D [OF S sgz] 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

604 
obtain no where "\<forall>n\<ge>no. dist (S n) a < s" by blast 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

605 
hence "\<forall>n\<ge>no. dist (X (S n)) L < r" by (simp add: aux as) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

606 
thus "\<exists>no. \<forall>n\<ge>no. dist (X (S n)) L < r" .. 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

607 
qed 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

608 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

609 

19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

610 
lemma LIMSEQ_SEQ_conv2: 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

611 
fixes a :: real and L :: "'a::metric_space" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

612 
assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

613 
shows "X  a > L" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

614 
proof (rule ccontr) 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

615 
assume "\<not> (X  a > L)" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

616 
hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x  a) < s > dist (X x) L < r)" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

617 
unfolding LIM_def dist_norm . 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

618 
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 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

619 
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) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

620 
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 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

621 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

622 
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" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

623 
have "\<And>n. \<exists>x. x\<noteq>a \<and> \<bar>x  a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

624 
using rdef by simp 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

625 
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" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

626 
by (rule someI_ex) 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

627 
hence F1: "\<And>n. ?F n \<noteq> a" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

628 
and F2: "\<And>n. \<bar>?F n  a\<bar> < inverse (real (Suc n))" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

629 
and F3: "\<And>n. dist (X (?F n)) L \<ge> r" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

630 
by fast+ 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

631 

19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

632 
have "?F > a" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

633 
proof (rule LIMSEQ_I, unfold real_norm_def) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

634 
fix e::real 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

635 
assume "0 < e" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

636 
(* choose no such that inverse (real (Suc n)) < e *) 
23441  637 
then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

638 
then obtain m where nodef: "inverse (real (Suc m)) < e" by auto 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

639 
show "\<exists>no. \<forall>n. no \<le> n > \<bar>?F n  a\<bar> < e" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

640 
proof (intro exI allI impI) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

641 
fix n 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

642 
assume mlen: "m \<le> n" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

643 
have "\<bar>?F n  a\<bar> < inverse (real (Suc n))" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

644 
by (rule F2) 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

645 
also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))" 
23441  646 
using mlen by auto 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

647 
also from nodef have 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

648 
"inverse (real (Suc m)) < e" . 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

649 
finally show "\<bar>?F n  a\<bar> < e" . 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

650 
qed 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

651 
qed 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

652 

5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

653 
moreover have "\<forall>n. ?F n \<noteq> a" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

654 
by (rule allI) (rule F1) 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

655 

19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

656 
moreover from prems have "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" by simp 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

657 
ultimately have "(\<lambda>n. X (?F n)) > L" by simp 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

658 

5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

659 
moreover have "\<not> ((\<lambda>n. X (?F n)) > L)" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

660 
proof  
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

661 
{ 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

662 
fix no::nat 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

663 
obtain n where "n = no + 1" by simp 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

664 
then have nolen: "no \<le> n" by simp 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

665 
(* We prove this by showing that for any m there is an n\<ge>m such that X (?F n)  L \<ge> r *) 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

666 
have "dist (X (?F n)) L \<ge> r" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

667 
by (rule F3) 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

668 
with nolen have "\<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r" by fast 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

669 
} 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

670 
then have "(\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r)" by simp 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

671 
with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> e)" by auto 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

672 
thus ?thesis by (unfold LIMSEQ_def, auto simp add: not_less) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

673 
qed 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

674 
ultimately show False by simp 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

675 
qed 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

676 

5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

677 
lemma LIMSEQ_SEQ_conv: 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

678 
"(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > (a::real) \<longrightarrow> (\<lambda>n. X (S n)) > L) = 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36661
diff
changeset

679 
(X  a > (L::'a::metric_space))" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

680 
proof 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

681 
assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" 
23441  682 
thus "X  a > L" by (rule LIMSEQ_SEQ_conv2) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

683 
next 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

684 
assume "(X  a > L)" 
23441  685 
thus "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" by (rule LIMSEQ_SEQ_conv1) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

686 
qed 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

687 

10751  688 
end 