author  hoelzl 
Wed, 23 Sep 2009 13:17:17 +0200  
changeset 32650  34bfa2492298 
parent 32642  026e7c6a6d08 
child 36661  0a5b7b818d65 
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 

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

16 
LIM :: "['a::metric_space \<Rightarrow> 'b::metric_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 
28562  18 
[code del]: "f  a > L = 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

19 
(\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

20 
> dist (f x) L < r)" 
10751  21 

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

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

23 
isCont :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a] \<Rightarrow> bool" where 
19765  24 
"isCont f a = (f  a > (f a))" 
10751  25 

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

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

27 
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

28 
[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  29 

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

31 

31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31392
diff
changeset

32 
lemma LIM_conv_tendsto: "(f  a > L) \<longleftrightarrow> (f > L) (at a)" 
31488  33 
unfolding LIM_def 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: 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

64 
fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space" 
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" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

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

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

68 
apply (drule_tac x="r" in spec, safe) 
20756  69 
apply (rule_tac x="s" in exI, safe) 
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: 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

75 
fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space" 
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: 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

80 
fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space" 
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" 
14477  85 
by (simp add: LIM_def) 
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: 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

90 
fixes f g :: "'a::metric_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)" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31338
diff
changeset

93 
using assms unfolding LIM_conv_tendsto by (rule tendsto_add) 
14477  94 

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

96 
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

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 

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

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

101 
fixes a b :: "'a::ab_group_add" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

102 
shows "( a)  ( b) =  (a  b)" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

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

104 

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

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

106 
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

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

108 
unfolding LIM_conv_tendsto by (rule tendsto_minus) 
14477  109 

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

110 
(* TODO: delete *) 
14477  111 
lemma LIM_add_minus: 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

112 
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

113 
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

114 
by (intro LIM_add LIM_minus) 
14477  115 

116 
lemma LIM_diff: 

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

117 
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

118 
shows "\<lbrakk>f  x > l; g  x > m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x  g x)  x > l  m" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31338
diff
changeset

119 
unfolding LIM_conv_tendsto by (rule tendsto_diff) 
14477  120 

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

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

122 
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

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

124 
by (simp add: LIM_def dist_norm) 
21239  125 

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

126 
lemma LIM_zero_cancel: 
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 \<Longrightarrow> f  a > l" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

129 
by (simp add: LIM_def dist_norm) 
21239  130 

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

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

132 
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

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

134 
by (simp add: LIM_def dist_norm) 
21399  135 

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

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

138 
assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l" 
21257  139 
shows "g  a > m" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

140 
apply (rule metric_LIM_I, drule metric_LIM_D [OF f], safe) 
21257  141 
apply (rule_tac x="s" in exI, safe) 
142 
apply (drule_tac x="x" in spec, safe) 

143 
apply (erule (1) order_le_less_trans [OF le]) 

144 
done 

145 

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

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

147 
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

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

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

150 
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

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

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

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

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

155 

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

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

157 
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

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

159 
unfolding LIM_conv_tendsto by (rule tendsto_norm) 
21257  160 

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

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

162 
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

163 
shows "f  a > 0 \<Longrightarrow> (\<lambda>x. norm (f x))  a > 0" 
21257  164 
by (drule LIM_norm, simp) 
165 

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

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

167 
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

168 
shows "(\<lambda>x. norm (f x))  a > 0 \<Longrightarrow> f  a > 0" 
21257  169 
by (erule LIM_imp_LIM, simp) 
170 

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

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

172 
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

173 
shows "(\<lambda>x. norm (f x))  a > 0 = f  a > 0" 
21399  174 
by (rule iffI [OF LIM_norm_zero_cancel LIM_norm_zero]) 
175 

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

176 
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

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

178 

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

179 
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

180 
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

181 

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

182 
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

183 
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

184 

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

185 
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

186 
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

187 

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

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

189 
fixes a :: "'a::real_normed_algebra_1" 
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset

190 
shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k)  a > L" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

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

192 
apply (rule_tac x="dist k L" in exI, simp add: zero_less_dist_iff, safe) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

193 
apply (rule_tac x="a + of_real (s/2)" in exI, simp add: dist_norm) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

194 
done 
14477  195 

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

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

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

199 
fixes a :: "'a::real_normed_algebra_1" 
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset

200 
shows "(\<lambda>x. k)  a > L \<Longrightarrow> k = L" 
14477  201 
apply (rule ccontr) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

202 
apply (blast dest: LIM_const_not_eq) 
14477  203 
done 
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 *} 
23076
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset

207 
shows "\<lbrakk>f  a > L; f  a > M\<rbrakk> \<Longrightarrow> L = M" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

208 
apply (rule ccontr) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

209 
apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

210 
apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

211 
apply (clarify, rename_tac r s) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

212 
apply (subgoal_tac "min r s \<noteq> 0") 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

213 
apply (subgoal_tac "dist L M < dist L M / 2 + dist L M / 2", simp) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

214 
apply (subgoal_tac "dist L M \<le> dist (f (a + of_real (min r s / 2))) L + 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

215 
dist (f (a + of_real (min r s / 2))) M") 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

216 
apply (erule le_less_trans, rule add_strict_mono) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

217 
apply (drule spec, erule mp, simp add: dist_norm) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

218 
apply (drule spec, erule mp, simp add: dist_norm) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

219 
apply (subst dist_commute, rule dist_triangle) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

220 
apply simp 
14477  221 
done 
222 

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

223 
lemma LIM_ident [simp]: "(\<lambda>x. x)  a > a" 
14477  224 
by (auto simp add: LIM_def) 
225 

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

227 
lemma LIM_equal: 

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

229 
by (simp add: LIM_def) 

230 

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

21399  233 
\<Longrightarrow> ((\<lambda>x. f x)  a > l) = ((\<lambda>x. g x)  b > m)" 
20796  234 
by (simp add: LIM_def) 
235 

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

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

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

238 
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

239 
shows "g  a > l \<Longrightarrow> f  a > l" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

240 
apply (unfold LIM_def, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

241 
apply (drule_tac x="r" in spec, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

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

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

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

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

246 

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

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

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

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

250 
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

251 
shows "g  a > l \<Longrightarrow> f  a > l" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

252 
apply (unfold LIM_def dist_norm, safe) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

253 
apply (drule_tac x="r" in spec, safe) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

254 
apply (rule_tac x="min s R" in exI, safe) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

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

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

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

258 

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

259 
text{*Two uses in Transcendental.ML*} 
14477  260 
lemma LIM_trans: 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

261 
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

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

265 
done 

266 

21239  267 
lemma LIM_compose: 
268 
assumes g: "g  l > g l" 

269 
assumes f: "f  a > l" 

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

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

271 
proof (rule metric_LIM_I) 
21239  272 
fix r::real assume r: "0 < r" 
273 
obtain s where s: "0 < s" 

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

274 
and less_r: "\<And>y. \<lbrakk>y \<noteq> l; dist y l < s\<rbrakk> \<Longrightarrow> dist (g y) (g l) < r" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

275 
using metric_LIM_D [OF g r] by fast 
21239  276 
obtain t where t: "0 < t" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

277 
and less_s: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> dist (f x) l < s" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

278 
using metric_LIM_D [OF f s] by fast 
21239  279 

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

280 
show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> dist x a < t \<longrightarrow> dist (g (f x)) (g l) < r" 
21239  281 
proof (rule exI, safe) 
282 
show "0 < t" using t . 

283 
next 

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

284 
fix x assume "x \<noteq> a" and "dist x a < t" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

285 
hence "dist (f x) l < s" by (rule less_s) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

286 
thus "dist (g (f x)) (g l) < r" 
21239  287 
using r less_r by (case_tac "f x = l", simp_all) 
288 
qed 

289 
qed 

290 

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

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

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

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

294 
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

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

296 
proof (rule metric_LIM_I) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

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

298 
assume r: "0 < r" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

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

300 
and less_r: "\<And>y. \<lbrakk>y \<noteq> b; dist y b < s\<rbrakk> \<Longrightarrow> dist (g y) c < r" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

301 
using metric_LIM_D [OF g r] by fast 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

302 
obtain t where t: "0 < t" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

303 
and less_s: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> dist (f x) b < s" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

304 
using metric_LIM_D [OF f s] by fast 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

305 
obtain d where d: "0 < d" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

306 
and neq_b: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < d\<rbrakk> \<Longrightarrow> f x \<noteq> b" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

307 
using inj by fast 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

308 

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

309 
show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> dist x a < t \<longrightarrow> dist (g (f x)) c < r" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

310 
proof (safe intro!: exI) 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

311 
show "0 < min d t" using d t by simp 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

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

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

314 
assume "x \<noteq> a" and "dist x a < min d t" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

315 
hence "f x \<noteq> b" and "dist (f x) b < s" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

316 
using neq_b less_s by simp_all 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

317 
thus "dist (g (f x)) c < r" 
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31336
diff
changeset

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

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

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

321 

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

323 
fixes a :: "'a::real_normed_vector" 
23040  324 
assumes f: "f  a > b" 
325 
assumes g: "g  b > c" 

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

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

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

328 
by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]]) 
23040  329 

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

332 

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

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

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

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

336 
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

337 
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

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

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

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

341 
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

342 
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

343 
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

344 
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

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

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

347 

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

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

349 

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

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

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

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

353 

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

354 
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

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

356 

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

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

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

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

360 

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

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

362 

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

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

364 
"\<lbrakk>f  a > L; g  a > M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x)  a > L ** M" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31338
diff
changeset

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

366 

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

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

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

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

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

371 
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

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

373 

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

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

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

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

377 

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

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

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

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

381 

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

383 

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

385 

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

387 

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

389 

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

391 

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

393 

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

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

395 
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

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

397 
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

398 
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

399 

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

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

401 

31355  402 
lemma LIM_inverse: 
403 
fixes L :: "'a::real_normed_div_algebra" 

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

405 
unfolding LIM_conv_tendsto 

406 
by (rule tendsto_inverse) 

22637  407 

408 
lemma LIM_inverse_fun: 

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

410 
shows "inverse  a > inverse a" 

31355  411 
by (rule LIM_inverse [OF LIM_ident a]) 
22637  412 

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

414 
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

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

418 

14477  419 

20755  420 
subsection {* Continuity *} 
14477  421 

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

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

423 
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

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

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

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

428 
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

429 
shows "isCont f x = (\<lambda>h. f (x + h))  0 > f x" 
21239  430 
by (simp add: isCont_def LIM_isCont_iff) 
431 

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

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

433 
unfolding isCont_def by (rule LIM_ident) 
21239  434 

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

436 
unfolding isCont_def by (rule LIM_const) 
21239  437 

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

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

439 
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

440 
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a" 
21786  441 
unfolding isCont_def by (rule LIM_norm) 
442 

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

443 
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

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

445 

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

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

447 
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

448 
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

449 
unfolding isCont_def by (rule LIM_add) 
21239  450 

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

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

452 
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

453 
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

454 
unfolding isCont_def by (rule LIM_minus) 
21239  455 

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

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

457 
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

458 
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

459 
unfolding isCont_def by (rule LIM_diff) 
21239  460 

461 
lemma isCont_mult: 

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

462 
fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_algebra" 
21786  463 
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

464 
unfolding isCont_def by (rule LIM_mult) 
21239  465 

466 
lemma isCont_inverse: 

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

467 
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_div_algebra" 
21786  468 
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

469 
unfolding isCont_def by (rule LIM_inverse) 
21239  470 

471 
lemma isCont_LIM_compose: 

472 
"\<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

473 
unfolding isCont_def by (rule LIM_compose) 
21239  474 

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

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

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

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

478 
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

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

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

481 

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

483 
fixes a :: "'a::real_normed_vector" 
23040  484 
assumes f [unfolded isCont_def]: "isCont f a" 
485 
assumes g: "g  f a > l" 

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

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

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

489 

21239  490 
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

491 
unfolding isCont_def by (rule LIM_compose) 
21239  492 

493 
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

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

495 

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

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

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

498 

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

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

500 
"\<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

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

502 

23127  503 
lemmas isCont_scaleR = scaleR.isCont 
21239  504 

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

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

506 
"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

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

508 

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

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

510 
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

511 
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

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

513 

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

515 
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

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

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

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

520 
by (rule isCont_rabs [OF isCont_ident]) 
15228  521 

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

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

523 
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

524 
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

525 
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

526 
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

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

528 
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

529 
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

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

531 

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

532 
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

533 
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

534 
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

535 
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

536 
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

537 
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

538 
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

539 
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

540 

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

541 
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

542 
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

543 
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

544 
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

545 
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

546 
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

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

548 
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

549 
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

550 
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

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

552 
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

553 
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

554 
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

555 
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

556 
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

557 
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

558 
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

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

560 

14477  561 

20755  562 
subsection {* Uniform Continuity *} 
563 

14477  564 
lemma isUCont_isCont: "isUCont f ==> isCont f x" 
23012  565 
by (simp add: isUCont_def isCont_def LIM_def, force) 
14477  566 

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

569 
unfolding isUCont_def 

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

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

572 
apply (drule_tac e=s in metric_CauchyD, safe) 
23118  573 
apply (rule_tac x=M in exI, simp) 
574 
done 

575 

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

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

577 
unfolding isUCont_def dist_norm 
23118  578 
proof (intro allI impI) 
579 
fix r::real assume r: "0 < r" 

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

581 
using pos_bounded by fast 

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

583 
proof (rule exI, safe) 

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

585 
next 

586 
fix x y :: 'a 

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

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

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

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

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

592 
qed 

593 
qed 

594 

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

596 
by (rule isUCont [THEN isUCont_Cauchy]) 

597 

14477  598 

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

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

600 

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

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

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

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

604 
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

605 
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

606 
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

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

608 
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

609 
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

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

611 
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

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

613 
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

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

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

616 
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

617 
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

618 
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

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

620 

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

621 

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

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

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

624 
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

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

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

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

628 
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

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

630 
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

631 
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

632 
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

633 

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

634 
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

635 
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

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

637 
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

638 
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

639 
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

640 
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

641 
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

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

643 

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

644 
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

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

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

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

648 
(* choose no such that inverse (real (Suc n)) < e *) 
23441  649 
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

650 
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

651 
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

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

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

654 
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

655 
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

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

657 
also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))" 
23441  658 
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

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

660 
"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

661 
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

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

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

664 

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

665 
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

666 
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

667 

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

668 
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

669 
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

670 

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

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

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

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

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

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

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

677 
(* 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

678 
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

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

680 
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

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

682 
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

683 
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

684 
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

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

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

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

688 

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

689 
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

690 
"(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > (a::real) \<longrightarrow> (\<lambda>n. X (S n)) > L) = 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

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

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

693 
assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" 
23441  694 
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

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

696 
assume "(X  a > L)" 
23441  697 
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

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

699 

10751  700 
end 