author  huffman 
Wed, 31 Aug 2011 07:51:55 0700  
changeset 44627  134c06282ae6 
parent 44571  bd91b77c4cd6 
child 45031  9583f2b56f85 
permissions  rwrr 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

1 
(* Title : Limits.thy 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

2 
Author : Brian Huffman 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

4 

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

5 
header {* Filters and Limits *} 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

6 

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

7 
theory Limits 
36822  8 
imports RealVector 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

10 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

11 
subsection {* Filters *} 
31392  12 

13 
text {* 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

14 
This definition also allows nonproper filters. 
31392  15 
*} 
16 

36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset

17 
locale is_filter = 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

18 
fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool" 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

19 
assumes True: "F (\<lambda>x. True)" 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

20 
assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)" 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

21 
assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)" 
36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset

22 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

23 
typedef (open) 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}" 
31392  24 
proof 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

25 
show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro) 
31392  26 
qed 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

27 

44195  28 
lemma is_filter_Rep_filter: "is_filter (Rep_filter F)" 
29 
using Rep_filter [of F] by simp 

31392  30 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

31 
lemma Abs_filter_inverse': 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

32 
assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F" 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

33 
using assms by (simp add: Abs_filter_inverse) 
31392  34 

35 

36 
subsection {* Eventually *} 

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

37 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

38 
definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool" 
44195  39 
where "eventually P F \<longleftrightarrow> Rep_filter F P" 
36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset

40 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

41 
lemma eventually_Abs_filter: 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

42 
assumes "is_filter F" shows "eventually P (Abs_filter F) = F P" 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

43 
unfolding eventually_def using assms by (simp add: Abs_filter_inverse) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

44 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

45 
lemma filter_eq_iff: 
44195  46 
shows "F = F' \<longleftrightarrow> (\<forall>P. eventually P F = eventually P F')" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

47 
unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def .. 
36360
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

48 

44195  49 
lemma eventually_True [simp]: "eventually (\<lambda>x. True) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

50 
unfolding eventually_def 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

51 
by (rule is_filter.True [OF is_filter_Rep_filter]) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

52 

44195  53 
lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P F" 
36630  54 
proof  
55 
assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext) 

44195  56 
thus "eventually P F" by simp 
36630  57 
qed 
58 

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

59 
lemma eventually_mono: 
44195  60 
"(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

61 
unfolding eventually_def 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

62 
by (rule is_filter.mono [OF is_filter_Rep_filter]) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

63 

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

64 
lemma eventually_conj: 
44195  65 
assumes P: "eventually (\<lambda>x. P x) F" 
66 
assumes Q: "eventually (\<lambda>x. Q x) F" 

67 
shows "eventually (\<lambda>x. P x \<and> Q x) F" 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

68 
using assms unfolding eventually_def 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

69 
by (rule is_filter.conj [OF is_filter_Rep_filter]) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

70 

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

71 
lemma eventually_mp: 
44195  72 
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" 
73 
assumes "eventually (\<lambda>x. P x) F" 

74 
shows "eventually (\<lambda>x. Q x) F" 

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

75 
proof (rule eventually_mono) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

76 
show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp 
44195  77 
show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

78 
using assms by (rule eventually_conj) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

80 

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

81 
lemma eventually_rev_mp: 
44195  82 
assumes "eventually (\<lambda>x. P x) F" 
83 
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" 

84 
shows "eventually (\<lambda>x. Q x) F" 

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

85 
using assms(2) assms(1) by (rule eventually_mp) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

86 

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

87 
lemma eventually_conj_iff: 
44195  88 
"eventually (\<lambda>x. P x \<and> Q x) F \<longleftrightarrow> eventually P F \<and> eventually Q F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

89 
by (auto intro: eventually_conj elim: eventually_rev_mp) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

90 

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

91 
lemma eventually_elim1: 
44195  92 
assumes "eventually (\<lambda>i. P i) F" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

93 
assumes "\<And>i. P i \<Longrightarrow> Q i" 
44195  94 
shows "eventually (\<lambda>i. Q i) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

95 
using assms by (auto elim!: eventually_rev_mp) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

96 

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

97 
lemma eventually_elim2: 
44195  98 
assumes "eventually (\<lambda>i. P i) F" 
99 
assumes "eventually (\<lambda>i. Q i) F" 

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

100 
assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i" 
44195  101 
shows "eventually (\<lambda>i. R i) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

102 
using assms by (auto elim!: eventually_rev_mp) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

103 

36360
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

104 
subsection {* Finerthan relation *} 
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

105 

44195  106 
text {* @{term "F \<le> F'"} means that filter @{term F} is finer than 
107 
filter @{term F'}. *} 

36360
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

108 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

109 
instantiation filter :: (type) complete_lattice 
36360
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

110 
begin 
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

111 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

112 
definition le_filter_def: 
44195  113 
"F \<le> F' \<longleftrightarrow> (\<forall>P. eventually P F' \<longrightarrow> eventually P F)" 
36360
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

114 

9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

115 
definition 
44195  116 
"(F :: 'a filter) < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F" 
36360
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

117 

9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

118 
definition 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

119 
"top = Abs_filter (\<lambda>P. \<forall>x. P x)" 
36630  120 

121 
definition 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

122 
"bot = Abs_filter (\<lambda>P. True)" 
36360
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

123 

36630  124 
definition 
44195  125 
"sup F F' = Abs_filter (\<lambda>P. eventually P F \<and> eventually P F')" 
36630  126 

127 
definition 

44195  128 
"inf F F' = Abs_filter 
129 
(\<lambda>P. \<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))" 

36630  130 

131 
definition 

44195  132 
"Sup S = Abs_filter (\<lambda>P. \<forall>F\<in>S. eventually P F)" 
36630  133 

134 
definition 

44195  135 
"Inf S = Sup {F::'a filter. \<forall>F'\<in>S. F \<le> F'}" 
36630  136 

137 
lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)" 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

138 
unfolding top_filter_def 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

139 
by (rule eventually_Abs_filter, rule is_filter.intro, auto) 
36630  140 

36629
de62713aec6e
swap ordering on nets, so x <= y means 'x is finer than y'
huffman
parents:
36360
diff
changeset

141 
lemma eventually_bot [simp]: "eventually P bot" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

142 
unfolding bot_filter_def 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

143 
by (subst eventually_Abs_filter, rule is_filter.intro, auto) 
36360
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

144 

36630  145 
lemma eventually_sup: 
44195  146 
"eventually P (sup F F') \<longleftrightarrow> eventually P F \<and> eventually P F'" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

147 
unfolding sup_filter_def 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

148 
by (rule eventually_Abs_filter, rule is_filter.intro) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

149 
(auto elim!: eventually_rev_mp) 
36630  150 

151 
lemma eventually_inf: 

44195  152 
"eventually P (inf F F') \<longleftrightarrow> 
153 
(\<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))" 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

154 
unfolding inf_filter_def 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

155 
apply (rule eventually_Abs_filter, rule is_filter.intro) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

156 
apply (fast intro: eventually_True) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

157 
apply clarify 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

158 
apply (intro exI conjI) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

159 
apply (erule (1) eventually_conj) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

160 
apply (erule (1) eventually_conj) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

161 
apply simp 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

162 
apply auto 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

163 
done 
36630  164 

165 
lemma eventually_Sup: 

44195  166 
"eventually P (Sup S) \<longleftrightarrow> (\<forall>F\<in>S. eventually P F)" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

167 
unfolding Sup_filter_def 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

168 
apply (rule eventually_Abs_filter, rule is_filter.intro) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

169 
apply (auto intro: eventually_conj elim!: eventually_rev_mp) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

170 
done 
36630  171 

36360
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

172 
instance proof 
44195  173 
fix F F' F'' :: "'a filter" and S :: "'a filter set" 
174 
{ show "F < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F" 

175 
by (rule less_filter_def) } 

176 
{ show "F \<le> F" 

177 
unfolding le_filter_def by simp } 

178 
{ assume "F \<le> F'" and "F' \<le> F''" thus "F \<le> F''" 

179 
unfolding le_filter_def by simp } 

180 
{ assume "F \<le> F'" and "F' \<le> F" thus "F = F'" 

181 
unfolding le_filter_def filter_eq_iff by fast } 

182 
{ show "F \<le> top" 

183 
unfolding le_filter_def eventually_top by (simp add: always_eventually) } 

184 
{ show "bot \<le> F" 

185 
unfolding le_filter_def by simp } 

186 
{ show "F \<le> sup F F'" and "F' \<le> sup F F'" 

187 
unfolding le_filter_def eventually_sup by simp_all } 

188 
{ assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''" 

189 
unfolding le_filter_def eventually_sup by simp } 

190 
{ show "inf F F' \<le> F" and "inf F F' \<le> F'" 

191 
unfolding le_filter_def eventually_inf by (auto intro: eventually_True) } 

192 
{ assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''" 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

193 
unfolding le_filter_def eventually_inf 
44195  194 
by (auto elim!: eventually_mono intro: eventually_conj) } 
195 
{ assume "F \<in> S" thus "F \<le> Sup S" 

196 
unfolding le_filter_def eventually_Sup by simp } 

197 
{ assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'" 

198 
unfolding le_filter_def eventually_Sup by simp } 

199 
{ assume "F'' \<in> S" thus "Inf S \<le> F''" 

200 
unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp } 

201 
{ assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S" 

202 
unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp } 

36360
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

203 
qed 
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

204 

9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

205 
end 
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

206 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

207 
lemma filter_leD: 
44195  208 
"F \<le> F' \<Longrightarrow> eventually P F' \<Longrightarrow> eventually P F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

209 
unfolding le_filter_def by simp 
36360
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

210 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

211 
lemma filter_leI: 
44195  212 
"(\<And>P. eventually P F' \<Longrightarrow> eventually P F) \<Longrightarrow> F \<le> F'" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

213 
unfolding le_filter_def by simp 
36360
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

214 

9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

215 
lemma eventually_False: 
44195  216 
"eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

217 
unfolding filter_eq_iff by (auto elim: eventually_rev_mp) 
36360
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

218 

44342
8321948340ea
redefine constant 'trivial_limit' as an abbreviation
huffman
parents:
44282
diff
changeset

219 
abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool" 
8321948340ea
redefine constant 'trivial_limit' as an abbreviation
huffman
parents:
44282
diff
changeset

220 
where "trivial_limit F \<equiv> F = bot" 
8321948340ea
redefine constant 'trivial_limit' as an abbreviation
huffman
parents:
44282
diff
changeset

221 

8321948340ea
redefine constant 'trivial_limit' as an abbreviation
huffman
parents:
44282
diff
changeset

222 
lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F" 
8321948340ea
redefine constant 'trivial_limit' as an abbreviation
huffman
parents:
44282
diff
changeset

223 
by (rule eventually_False [symmetric]) 
8321948340ea
redefine constant 'trivial_limit' as an abbreviation
huffman
parents:
44282
diff
changeset

224 

8321948340ea
redefine constant 'trivial_limit' as an abbreviation
huffman
parents:
44282
diff
changeset

225 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

226 
subsection {* Map function for filters *} 
36654  227 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

228 
definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter" 
44195  229 
where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)" 
36654  230 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

231 
lemma eventually_filtermap: 
44195  232 
"eventually P (filtermap f F) = eventually (\<lambda>x. P (f x)) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

233 
unfolding filtermap_def 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

234 
apply (rule eventually_Abs_filter) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

235 
apply (rule is_filter.intro) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

236 
apply (auto elim!: eventually_rev_mp) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

237 
done 
36654  238 

44195  239 
lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

240 
by (simp add: filter_eq_iff eventually_filtermap) 
36654  241 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

242 
lemma filtermap_filtermap: 
44195  243 
"filtermap f (filtermap g F) = filtermap (\<lambda>x. f (g x)) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

244 
by (simp add: filter_eq_iff eventually_filtermap) 
36654  245 

44195  246 
lemma filtermap_mono: "F \<le> F' \<Longrightarrow> filtermap f F \<le> filtermap f F'" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

247 
unfolding le_filter_def eventually_filtermap by simp 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

248 

730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

249 
lemma filtermap_bot [simp]: "filtermap f bot = bot" 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

250 
by (simp add: filter_eq_iff eventually_filtermap) 
36654  251 

252 

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

253 
subsection {* Sequentially *} 
31392  254 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

255 
definition sequentially :: "nat filter" 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

256 
where "sequentially = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)" 
31392  257 

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

258 
lemma eventually_sequentially: 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

259 
"eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

260 
unfolding sequentially_def 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

261 
proof (rule eventually_Abs_filter, rule is_filter.intro) 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

262 
fix P Q :: "nat \<Rightarrow> bool" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

263 
assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n" 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

264 
then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

265 
then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

266 
then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" .. 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

267 
qed auto 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

268 

44342
8321948340ea
redefine constant 'trivial_limit' as an abbreviation
huffman
parents:
44282
diff
changeset

269 
lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

270 
unfolding filter_eq_iff eventually_sequentially by auto 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

271 

44342
8321948340ea
redefine constant 'trivial_limit' as an abbreviation
huffman
parents:
44282
diff
changeset

272 
lemmas trivial_limit_sequentially = sequentially_bot 
8321948340ea
redefine constant 'trivial_limit' as an abbreviation
huffman
parents:
44282
diff
changeset

273 

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

274 
lemma eventually_False_sequentially [simp]: 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

275 
"\<not> eventually (\<lambda>n. False) sequentially" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

276 
by (simp add: eventually_False) 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

277 

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

278 
lemma le_sequentially: 
44195  279 
"F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

280 
unfolding le_filter_def eventually_sequentially 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

281 
by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp) 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

282 

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

283 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

284 
subsection {* Standard filters *} 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

285 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

286 
definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70) 
44195  287 
where "F within S = Abs_filter (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F)" 
31392  288 

44206
5e4a1664106e
localeize some constant definitions, so complete_space can inherit from metric_space
huffman
parents:
44205
diff
changeset

289 
definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

290 
where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))" 
36654  291 

44206
5e4a1664106e
localeize some constant definitions, so complete_space can inherit from metric_space
huffman
parents:
44205
diff
changeset

292 
definition (in topological_space) at :: "'a \<Rightarrow> 'a filter" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

293 
where "at a = nhds a within  {a}" 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

294 

31392  295 
lemma eventually_within: 
44195  296 
"eventually P (F within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

297 
unfolding within_def 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

298 
by (rule eventually_Abs_filter, rule is_filter.intro) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

299 
(auto elim!: eventually_rev_mp) 
31392  300 

44195  301 
lemma within_UNIV: "F within UNIV = F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

302 
unfolding filter_eq_iff eventually_within by simp 
36360
9d8f7efd9289
define finerthan ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset

303 

36654  304 
lemma eventually_nhds: 
305 
"eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))" 

306 
unfolding nhds_def 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

307 
proof (rule eventually_Abs_filter, rule is_filter.intro) 
36654  308 
have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. True)" by simp 
309 
thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. True)" by  rule 

36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset

310 
next 
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset

311 
fix P Q 
36654  312 
assume "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)" 
313 
and "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)" 

36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset

314 
then obtain S T where 
36654  315 
"open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)" 
316 
"open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)" by auto 

317 
hence "open (S \<inter> T) \<and> a \<in> S \<inter> T \<and> (\<forall>x\<in>(S \<inter> T). P x \<and> Q x)" 

36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset

318 
by (simp add: open_Int) 
36654  319 
thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x \<and> Q x)" by  rule 
36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset

320 
qed auto 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

321 

36656
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset

322 
lemma eventually_nhds_metric: 
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset

323 
"eventually P (nhds a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. dist x a < d \<longrightarrow> P x)" 
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset

324 
unfolding eventually_nhds open_dist 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

325 
apply safe 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

326 
apply fast 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset

327 
apply (rule_tac x="{x. dist x a < d}" in exI, simp) 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

328 
apply clarsimp 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

329 
apply (rule_tac x="d  dist x a" in exI, clarsimp) 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

330 
apply (simp only: less_diff_eq) 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

331 
apply (erule le_less_trans [OF dist_triangle]) 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

332 
done 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

333 

44571  334 
lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot" 
335 
unfolding trivial_limit_def eventually_nhds by simp 

336 

36656
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset

337 
lemma eventually_at_topological: 
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset

338 
"eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))" 
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset

339 
unfolding at_def eventually_within eventually_nhds by simp 
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset

340 

fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset

341 
lemma eventually_at: 
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset

342 
fixes a :: "'a::metric_space" 
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset

343 
shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)" 
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset

344 
unfolding at_def eventually_within eventually_nhds_metric by auto 
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset

345 

44571  346 
lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}" 
347 
unfolding trivial_limit_def eventually_at_topological 

348 
by (safe, case_tac "S = {a}", simp, fast, fast) 

349 

350 
lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot" 

351 
by (simp add: at_eq_bot_iff not_open_singleton) 

352 

31392  353 

31355  354 
subsection {* Boundedness *} 
355 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

356 
definition Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" 
44195  357 
where "Bfun f F = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) F)" 
31355  358 

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

359 
lemma BfunI: 
44195  360 
assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) F" shows "Bfun f F" 
31355  361 
unfolding Bfun_def 
362 
proof (intro exI conjI allI) 

363 
show "0 < max K 1" by simp 

364 
next 

44195  365 
show "eventually (\<lambda>x. norm (f x) \<le> max K 1) F" 
31355  366 
using K by (rule eventually_elim1, simp) 
367 
qed 

368 

369 
lemma BfunE: 

44195  370 
assumes "Bfun f F" 
371 
obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) F" 

31355  372 
using assms unfolding Bfun_def by fast 
373 

374 

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

375 
subsection {* Convergence to Zero *} 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

376 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

377 
definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" 
44195  378 
where "Zfun f F = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) F)" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

379 

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

380 
lemma ZfunI: 
44195  381 
"(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) F) \<Longrightarrow> Zfun f F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

382 
unfolding Zfun_def by simp 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

383 

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

384 
lemma ZfunD: 
44195  385 
"\<lbrakk>Zfun f F; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

386 
unfolding Zfun_def by simp 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

387 

31355  388 
lemma Zfun_ssubst: 
44195  389 
"eventually (\<lambda>x. f x = g x) F \<Longrightarrow> Zfun g F \<Longrightarrow> Zfun f F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

390 
unfolding Zfun_def by (auto elim!: eventually_rev_mp) 
31355  391 

44195  392 
lemma Zfun_zero: "Zfun (\<lambda>x. 0) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

393 
unfolding Zfun_def by simp 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

394 

44195  395 
lemma Zfun_norm_iff: "Zfun (\<lambda>x. norm (f x)) F = Zfun (\<lambda>x. f x) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

396 
unfolding Zfun_def by simp 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

397 

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

398 
lemma Zfun_imp_Zfun: 
44195  399 
assumes f: "Zfun f F" 
400 
assumes g: "eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F" 

401 
shows "Zfun (\<lambda>x. g x) F" 

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

402 
proof (cases) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

403 
assume K: "0 < K" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

404 
show ?thesis 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

405 
proof (rule ZfunI) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

406 
fix r::real assume "0 < r" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

407 
hence "0 < r / K" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

408 
using K by (rule divide_pos_pos) 
44195  409 
then have "eventually (\<lambda>x. norm (f x) < r / K) F" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

410 
using ZfunD [OF f] by fast 
44195  411 
with g show "eventually (\<lambda>x. norm (g x) < r) F" 
31355  412 
proof (rule eventually_elim2) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

413 
fix x 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

414 
assume *: "norm (g x) \<le> norm (f x) * K" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

415 
assume "norm (f x) < r / K" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

416 
hence "norm (f x) * K < r" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

417 
by (simp add: pos_less_divide_eq K) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

418 
thus "norm (g x) < r" 
31355  419 
by (simp add: order_le_less_trans [OF *]) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

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

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

423 
assume "\<not> 0 < K" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

424 
hence K: "K \<le> 0" by (simp only: not_less) 
31355  425 
show ?thesis 
426 
proof (rule ZfunI) 

427 
fix r :: real 

428 
assume "0 < r" 

44195  429 
from g show "eventually (\<lambda>x. norm (g x) < r) F" 
31355  430 
proof (rule eventually_elim1) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

431 
fix x 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

432 
assume "norm (g x) \<le> norm (f x) * K" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

433 
also have "\<dots> \<le> norm (f x) * 0" 
31355  434 
using K norm_ge_zero by (rule mult_left_mono) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

435 
finally show "norm (g x) < r" 
31355  436 
using `0 < r` by simp 
437 
qed 

438 
qed 

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

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

440 

44195  441 
lemma Zfun_le: "\<lbrakk>Zfun g F; \<forall>x. norm (f x) \<le> norm (g x)\<rbrakk> \<Longrightarrow> Zfun f F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

442 
by (erule_tac K="1" in Zfun_imp_Zfun, simp) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

443 

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

444 
lemma Zfun_add: 
44195  445 
assumes f: "Zfun f F" and g: "Zfun g F" 
446 
shows "Zfun (\<lambda>x. f x + g x) F" 

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

447 
proof (rule ZfunI) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

448 
fix r::real assume "0 < r" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

449 
hence r: "0 < r / 2" by simp 
44195  450 
have "eventually (\<lambda>x. norm (f x) < r/2) F" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

451 
using f r by (rule ZfunD) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

452 
moreover 
44195  453 
have "eventually (\<lambda>x. norm (g x) < r/2) F" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

454 
using g r by (rule ZfunD) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

455 
ultimately 
44195  456 
show "eventually (\<lambda>x. norm (f x + g x) < r) F" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

457 
proof (rule eventually_elim2) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

458 
fix x 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

459 
assume *: "norm (f x) < r/2" "norm (g x) < r/2" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

460 
have "norm (f x + g x) \<le> norm (f x) + norm (g x)" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

461 
by (rule norm_triangle_ineq) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

462 
also have "\<dots> < r/2 + r/2" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

463 
using * by (rule add_strict_mono) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

464 
finally show "norm (f x + g x) < r" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

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

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

468 

44195  469 
lemma Zfun_minus: "Zfun f F \<Longrightarrow> Zfun (\<lambda>x.  f x) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

470 
unfolding Zfun_def by simp 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

471 

44195  472 
lemma Zfun_diff: "\<lbrakk>Zfun f F; Zfun g F\<rbrakk> \<Longrightarrow> Zfun (\<lambda>x. f x  g x) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

473 
by (simp only: diff_minus Zfun_add Zfun_minus) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

474 

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

475 
lemma (in bounded_linear) Zfun: 
44195  476 
assumes g: "Zfun g F" 
477 
shows "Zfun (\<lambda>x. f (g x)) F" 

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

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

479 
obtain K where "\<And>x. norm (f x) \<le> norm x * K" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

480 
using bounded by fast 
44195  481 
then have "eventually (\<lambda>x. norm (f (g x)) \<le> norm (g x) * K) F" 
31355  482 
by simp 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

483 
with g show ?thesis 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

484 
by (rule Zfun_imp_Zfun) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

486 

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

487 
lemma (in bounded_bilinear) Zfun: 
44195  488 
assumes f: "Zfun f F" 
489 
assumes g: "Zfun g F" 

490 
shows "Zfun (\<lambda>x. f x ** g x) F" 

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

491 
proof (rule ZfunI) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

492 
fix r::real assume r: "0 < r" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

493 
obtain K where K: "0 < K" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

494 
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

495 
using pos_bounded by fast 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

496 
from K have K': "0 < inverse K" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

497 
by (rule positive_imp_inverse_positive) 
44195  498 
have "eventually (\<lambda>x. norm (f x) < r) F" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

499 
using f r by (rule ZfunD) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

500 
moreover 
44195  501 
have "eventually (\<lambda>x. norm (g x) < inverse K) F" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

502 
using g K' by (rule ZfunD) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

503 
ultimately 
44195  504 
show "eventually (\<lambda>x. norm (f x ** g x) < r) F" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

505 
proof (rule eventually_elim2) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

506 
fix x 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

507 
assume *: "norm (f x) < r" "norm (g x) < inverse K" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

508 
have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

509 
by (rule norm_le) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

510 
also have "norm (f x) * norm (g x) * K < r * inverse K * K" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

511 
by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero * K) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

512 
also from K have "r * inverse K * K = r" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

513 
by simp 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

514 
finally show "norm (f x ** g x) < r" . 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

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

517 

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

518 
lemma (in bounded_bilinear) Zfun_left: 
44195  519 
"Zfun f F \<Longrightarrow> Zfun (\<lambda>x. f x ** a) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

520 
by (rule bounded_linear_left [THEN bounded_linear.Zfun]) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

521 

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

522 
lemma (in bounded_bilinear) Zfun_right: 
44195  523 
"Zfun f F \<Longrightarrow> Zfun (\<lambda>x. a ** f x) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

524 
by (rule bounded_linear_right [THEN bounded_linear.Zfun]) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

525 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

526 
lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult] 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

527 
lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult] 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

528 
lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult] 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

529 

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

530 

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

532 

44206
5e4a1664106e
localeize some constant definitions, so complete_space can inherit from metric_space
huffman
parents:
44205
diff
changeset

533 
definition (in topological_space) 
5e4a1664106e
localeize some constant definitions, so complete_space can inherit from metric_space
huffman
parents:
44205
diff
changeset

534 
tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr ">" 55) where 
44195  535 
"(f > l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

536 

31902  537 
ML {* 
538 
structure Tendsto_Intros = Named_Thms 

539 
( 

540 
val name = "tendsto_intros" 

541 
val description = "introduction rules for tendsto" 

542 
) 

31565  543 
*} 
544 

31902  545 
setup Tendsto_Intros.setup 
31565  546 

44195  547 
lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f > l) F' \<Longrightarrow> (f > l) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

548 
unfolding tendsto_def le_filter_def by fast 
36656
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset

549 

31488  550 
lemma topological_tendstoI: 
44195  551 
"(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) 
552 
\<Longrightarrow> (f > l) F" 

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

553 
unfolding tendsto_def by auto 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

554 

31488  555 
lemma topological_tendstoD: 
44195  556 
"(f > l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F" 
31488  557 
unfolding tendsto_def by auto 
558 

559 
lemma tendstoI: 

44195  560 
assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F" 
561 
shows "(f > l) F" 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

562 
apply (rule topological_tendstoI) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

563 
apply (simp add: open_dist) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

564 
apply (drule (1) bspec, clarify) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

565 
apply (drule assms) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

566 
apply (erule eventually_elim1, simp) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

567 
done 
31488  568 

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

569 
lemma tendstoD: 
44195  570 
"(f > l) F \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

571 
apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

572 
apply (clarsimp simp add: open_dist) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

573 
apply (rule_tac x="e  dist x l" in exI, clarsimp) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

574 
apply (simp only: less_diff_eq) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

575 
apply (erule le_less_trans [OF dist_triangle]) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

576 
apply simp 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

577 
apply simp 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

578 
done 
31488  579 

580 
lemma tendsto_iff: 

44195  581 
"(f > l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

582 
using tendstoI tendstoD by fast 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

583 

44195  584 
lemma tendsto_Zfun_iff: "(f > a) F = Zfun (\<lambda>x. f x  a) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

585 
by (simp only: tendsto_iff Zfun_def dist_norm) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

586 

31565  587 
lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) > a) (at a)" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

588 
unfolding tendsto_def eventually_at_topological by auto 
31565  589 

590 
lemma tendsto_ident_at_within [tendsto_intros]: 

36655  591 
"((\<lambda>x. x) > a) (at a within S)" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

592 
unfolding tendsto_def eventually_within eventually_at_topological by auto 
31565  593 

44195  594 
lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) > k) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

595 
by (simp add: tendsto_def) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

596 

44205
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

597 
lemma tendsto_unique: 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

598 
fixes f :: "'a \<Rightarrow> 'b::t2_space" 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

599 
assumes "\<not> trivial_limit F" and "(f > a) F" and "(f > b) F" 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

600 
shows "a = b" 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

601 
proof (rule ccontr) 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

602 
assume "a \<noteq> b" 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

603 
obtain U V where "open U" "open V" "a \<in> U" "b \<in> V" "U \<inter> V = {}" 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

604 
using hausdorff [OF `a \<noteq> b`] by fast 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

605 
have "eventually (\<lambda>x. f x \<in> U) F" 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

606 
using `(f > a) F` `open U` `a \<in> U` by (rule topological_tendstoD) 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

607 
moreover 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

608 
have "eventually (\<lambda>x. f x \<in> V) F" 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

609 
using `(f > b) F` `open V` `b \<in> V` by (rule topological_tendstoD) 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

610 
ultimately 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

611 
have "eventually (\<lambda>x. False) F" 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

612 
proof (rule eventually_elim2) 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

613 
fix x 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

614 
assume "f x \<in> U" "f x \<in> V" 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

615 
hence "f x \<in> U \<inter> V" by simp 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

616 
with `U \<inter> V = {}` show "False" by simp 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

617 
qed 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

618 
with `\<not> trivial_limit F` show "False" 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

619 
by (simp add: trivial_limit_def) 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

620 
qed 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

621 

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

622 
lemma tendsto_const_iff: 
44205
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

623 
fixes a b :: "'a::t2_space" 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

624 
assumes "\<not> trivial_limit F" shows "((\<lambda>x. a) > b) F \<longleftrightarrow> a = b" 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

625 
by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const]) 
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

626 

44218  627 
lemma tendsto_compose: 
628 
assumes g: "(g > g l) (at l)" 

629 
assumes f: "(f > l) F" 

630 
shows "((\<lambda>x. g (f x)) > g l) F" 

631 
proof (rule topological_tendstoI) 

632 
fix B assume B: "open B" "g l \<in> B" 

633 
obtain A where A: "open A" "l \<in> A" 

634 
and gB: "\<forall>y. y \<in> A \<longrightarrow> g y \<in> B" 

635 
using topological_tendstoD [OF g B] B(2) 

636 
unfolding eventually_at_topological by fast 

637 
hence "\<forall>x. f x \<in> A \<longrightarrow> g (f x) \<in> B" by simp 

638 
from this topological_tendstoD [OF f A] 

639 
show "eventually (\<lambda>x. g (f x) \<in> B) F" 

640 
by (rule eventually_mono) 

641 
qed 

642 

44253
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

643 
lemma tendsto_compose_eventually: 
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

644 
assumes g: "(g > m) (at l)" 
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

645 
assumes f: "(f > l) F" 
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

646 
assumes inj: "eventually (\<lambda>x. f x \<noteq> l) F" 
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

647 
shows "((\<lambda>x. g (f x)) > m) F" 
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

648 
proof (rule topological_tendstoI) 
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

649 
fix B assume B: "open B" "m \<in> B" 
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

650 
obtain A where A: "open A" "l \<in> A" 
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

651 
and gB: "\<And>y. y \<in> A \<Longrightarrow> y \<noteq> l \<Longrightarrow> g y \<in> B" 
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

652 
using topological_tendstoD [OF g B] 
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

653 
unfolding eventually_at_topological by fast 
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

654 
show "eventually (\<lambda>x. g (f x) \<in> B) F" 
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

655 
using topological_tendstoD [OF f A] inj 
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

656 
by (rule eventually_elim2) (simp add: gB) 
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

657 
qed 
c073a0bd8458
add lemma tendsto_compose_eventually; use it to shorten some proofs
huffman
parents:
44251
diff
changeset

658 

44251  659 
lemma metric_tendsto_imp_tendsto: 
660 
assumes f: "(f > a) F" 

661 
assumes le: "eventually (\<lambda>x. dist (g x) b \<le> dist (f x) a) F" 

662 
shows "(g > b) F" 

663 
proof (rule tendstoI) 

664 
fix e :: real assume "0 < e" 

665 
with f have "eventually (\<lambda>x. dist (f x) a < e) F" by (rule tendstoD) 

666 
with le show "eventually (\<lambda>x. dist (g x) b < e) F" 

667 
using le_less_trans by (rule eventually_elim2) 

668 
qed 

669 

44205
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

670 
subsubsection {* Distance and norms *} 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

671 

31565  672 
lemma tendsto_dist [tendsto_intros]: 
44195  673 
assumes f: "(f > l) F" and g: "(g > m) F" 
674 
shows "((\<lambda>x. dist (f x) (g x)) > dist l m) F" 

31565  675 
proof (rule tendstoI) 
676 
fix e :: real assume "0 < e" 

677 
hence e2: "0 < e/2" by simp 

678 
from tendstoD [OF f e2] tendstoD [OF g e2] 

44195  679 
show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) F" 
31565  680 
proof (rule eventually_elim2) 
681 
fix x assume "dist (f x) l < e/2" "dist (g x) m < e/2" 

682 
then show "dist (dist (f x) (g x)) (dist l m) < e" 

683 
unfolding dist_real_def 

684 
using dist_triangle2 [of "f x" "g x" "l"] 

685 
using dist_triangle2 [of "g x" "l" "m"] 

686 
using dist_triangle3 [of "l" "m" "f x"] 

687 
using dist_triangle [of "f x" "m" "g x"] 

688 
by arith 

689 
qed 

690 
qed 

691 

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

692 
lemma norm_conv_dist: "norm x = dist x 0" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

693 
unfolding dist_norm by simp 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

694 

31565  695 
lemma tendsto_norm [tendsto_intros]: 
44195  696 
"(f > a) F \<Longrightarrow> ((\<lambda>x. norm (f x)) > norm a) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

697 
unfolding norm_conv_dist by (intro tendsto_intros) 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

698 

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

699 
lemma tendsto_norm_zero: 
44195  700 
"(f > 0) F \<Longrightarrow> ((\<lambda>x. norm (f x)) > 0) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

701 
by (drule tendsto_norm, simp) 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

702 

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

703 
lemma tendsto_norm_zero_cancel: 
44195  704 
"((\<lambda>x. norm (f x)) > 0) F \<Longrightarrow> (f > 0) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

705 
unfolding tendsto_iff dist_norm by simp 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

706 

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

707 
lemma tendsto_norm_zero_iff: 
44195  708 
"((\<lambda>x. norm (f x)) > 0) F \<longleftrightarrow> (f > 0) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

709 
unfolding tendsto_iff dist_norm by simp 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

710 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

711 
lemma tendsto_rabs [tendsto_intros]: 
44195  712 
"(f > (l::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) > \<bar>l\<bar>) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

713 
by (fold real_norm_def, rule tendsto_norm) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

714 

0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

715 
lemma tendsto_rabs_zero: 
44195  716 
"(f > (0::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) > 0) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

717 
by (fold real_norm_def, rule tendsto_norm_zero) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

718 

0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

719 
lemma tendsto_rabs_zero_cancel: 
44195  720 
"((\<lambda>x. \<bar>f x\<bar>) > (0::real)) F \<Longrightarrow> (f > 0) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

721 
by (fold real_norm_def, rule tendsto_norm_zero_cancel) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

722 

0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

723 
lemma tendsto_rabs_zero_iff: 
44195  724 
"((\<lambda>x. \<bar>f x\<bar>) > (0::real)) F \<longleftrightarrow> (f > 0) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

725 
by (fold real_norm_def, rule tendsto_norm_zero_iff) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

726 

0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

727 
subsubsection {* Addition and subtraction *} 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

728 

31565  729 
lemma tendsto_add [tendsto_intros]: 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

730 
fixes a b :: "'a::real_normed_vector" 
44195  731 
shows "\<lbrakk>(f > a) F; (g > b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) > a + b) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

732 
by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

733 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

734 
lemma tendsto_add_zero: 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

735 
fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector" 
44195  736 
shows "\<lbrakk>(f > 0) F; (g > 0) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) > 0) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

737 
by (drule (1) tendsto_add, simp) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

738 

31565  739 
lemma tendsto_minus [tendsto_intros]: 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

740 
fixes a :: "'a::real_normed_vector" 
44195  741 
shows "(f > a) F \<Longrightarrow> ((\<lambda>x.  f x) >  a) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

742 
by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

743 

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

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

745 
fixes a :: "'a::real_normed_vector" 
44195  746 
shows "((\<lambda>x.  f x) >  a) F \<Longrightarrow> (f > a) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

747 
by (drule tendsto_minus, simp) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

748 

31565  749 
lemma tendsto_diff [tendsto_intros]: 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

750 
fixes a b :: "'a::real_normed_vector" 
44195  751 
shows "\<lbrakk>(f > a) F; (g > b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x  g x) > a  b) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

752 
by (simp add: diff_minus tendsto_add tendsto_minus) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

753 

31588  754 
lemma tendsto_setsum [tendsto_intros]: 
755 
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector" 

44195  756 
assumes "\<And>i. i \<in> S \<Longrightarrow> (f i > a i) F" 
757 
shows "((\<lambda>x. \<Sum>i\<in>S. f i x) > (\<Sum>i\<in>S. a i)) F" 

31588  758 
proof (cases "finite S") 
759 
assume "finite S" thus ?thesis using assms 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

760 
by (induct, simp add: tendsto_const, simp add: tendsto_add) 
31588  761 
next 
762 
assume "\<not> finite S" thus ?thesis 

763 
by (simp add: tendsto_const) 

764 
qed 

765 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

766 
subsubsection {* Linear operators and multiplication *} 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

767 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

768 
lemma (in bounded_linear) tendsto: 
44195  769 
"(g > a) F \<Longrightarrow> ((\<lambda>x. f (g x)) > f a) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

770 
by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

771 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

772 
lemma (in bounded_linear) tendsto_zero: 
44195  773 
"(g > 0) F \<Longrightarrow> ((\<lambda>x. f (g x)) > 0) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

774 
by (drule tendsto, simp only: zero) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

775 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

776 
lemma (in bounded_bilinear) tendsto: 
44195  777 
"\<lbrakk>(f > a) F; (g > b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) > a ** b) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

778 
by (simp only: tendsto_Zfun_iff prod_diff_prod 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

779 
Zfun_add Zfun Zfun_left Zfun_right) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

780 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

781 
lemma (in bounded_bilinear) tendsto_zero: 
44195  782 
assumes f: "(f > 0) F" 
783 
assumes g: "(g > 0) F" 

784 
shows "((\<lambda>x. f x ** g x) > 0) F" 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

785 
using tendsto [OF f g] by (simp add: zero_left) 
31355  786 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

787 
lemma (in bounded_bilinear) tendsto_left_zero: 
44195  788 
"(f > 0) F \<Longrightarrow> ((\<lambda>x. f x ** c) > 0) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

789 
by (rule bounded_linear.tendsto_zero [OF bounded_linear_left]) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

790 

0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

791 
lemma (in bounded_bilinear) tendsto_right_zero: 
44195  792 
"(f > 0) F \<Longrightarrow> ((\<lambda>x. c ** f x) > 0) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

793 
by (rule bounded_linear.tendsto_zero [OF bounded_linear_right]) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

794 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

795 
lemmas tendsto_of_real [tendsto_intros] = 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

796 
bounded_linear.tendsto [OF bounded_linear_of_real] 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

797 

f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

798 
lemmas tendsto_scaleR [tendsto_intros] = 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

799 
bounded_bilinear.tendsto [OF bounded_bilinear_scaleR] 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

800 

f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

801 
lemmas tendsto_mult [tendsto_intros] = 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

802 
bounded_bilinear.tendsto [OF bounded_bilinear_mult] 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

803 

44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

804 
lemmas tendsto_mult_zero = 
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

805 
bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult] 
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

806 

e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

807 
lemmas tendsto_mult_left_zero = 
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

808 
bounded_bilinear.tendsto_left_zero [OF bounded_bilinear_mult] 
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

809 

e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

810 
lemmas tendsto_mult_right_zero = 
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

811 
bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult] 
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

812 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

813 
lemma tendsto_power [tendsto_intros]: 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

814 
fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}" 
44195  815 
shows "(f > a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) > a ^ n) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

816 
by (induct n) (simp_all add: tendsto_const tendsto_mult) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

817 

0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

818 
lemma tendsto_setprod [tendsto_intros]: 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

819 
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}" 
44195  820 
assumes "\<And>i. i \<in> S \<Longrightarrow> (f i > L i) F" 
821 
shows "((\<lambda>x. \<Prod>i\<in>S. f i x) > (\<Prod>i\<in>S. L i)) F" 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

822 
proof (cases "finite S") 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

823 
assume "finite S" thus ?thesis using assms 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

824 
by (induct, simp add: tendsto_const, simp add: tendsto_mult) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

825 
next 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

826 
assume "\<not> finite S" thus ?thesis 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

827 
by (simp add: tendsto_const) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

828 
qed 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

829 

0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

830 
subsubsection {* Inverse and division *} 
31355  831 

832 
lemma (in bounded_bilinear) Zfun_prod_Bfun: 

44195  833 
assumes f: "Zfun f F" 
834 
assumes g: "Bfun g F" 

835 
shows "Zfun (\<lambda>x. f x ** g x) F" 

31355  836 
proof  
837 
obtain K where K: "0 \<le> K" 

838 
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" 

839 
using nonneg_bounded by fast 

840 
obtain B where B: "0 < B" 

44195  841 
and norm_g: "eventually (\<lambda>x. norm (g x) \<le> B) F" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

842 
using g by (rule BfunE) 
44195  843 
have "eventually (\<lambda>x. norm (f x ** g x) \<le> norm (f x) * (B * K)) F" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

844 
using norm_g proof (rule eventually_elim1) 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

845 
fix x 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

846 
assume *: "norm (g x) \<le> B" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

847 
have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" 
31355  848 
by (rule norm_le) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

849 
also have "\<dots> \<le> norm (f x) * B * K" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

850 
by (intro mult_mono' order_refl norm_g norm_ge_zero 
31355  851 
mult_nonneg_nonneg K *) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

852 
also have "\<dots> = norm (f x) * (B * K)" 
31355  853 
by (rule mult_assoc) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

854 
finally show "norm (f x ** g x) \<le> norm (f x) * (B * K)" . 
31355  855 
qed 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

856 
with f show ?thesis 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

857 
by (rule Zfun_imp_Zfun) 
31355  858 
qed 
859 

860 
lemma (in bounded_bilinear) flip: 

861 
"bounded_bilinear (\<lambda>x y. y ** x)" 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

862 
apply default 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

863 
apply (rule add_right) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

864 
apply (rule add_left) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

865 
apply (rule scaleR_right) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

866 
apply (rule scaleR_left) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

867 
apply (subst mult_commute) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

868 
using bounded by fast 
31355  869 

870 
lemma (in bounded_bilinear) Bfun_prod_Zfun: 

44195  871 
assumes f: "Bfun f F" 
872 
assumes g: "Zfun g F" 

873 
shows "Zfun (\<lambda>x. f x ** g x) F" 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

874 
using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) 
31355  875 

876 
lemma Bfun_inverse_lemma: 

877 
fixes x :: "'a::real_normed_div_algebra" 

878 
shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r" 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

879 
apply (subst nonzero_norm_inverse, clarsimp) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

880 
apply (erule (1) le_imp_inverse_le) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

881 
done 
31355  882 

883 
lemma Bfun_inverse: 

884 
fixes a :: "'a::real_normed_div_algebra" 

44195  885 
assumes f: "(f > a) F" 
31355  886 
assumes a: "a \<noteq> 0" 
44195  887 
shows "Bfun (\<lambda>x. inverse (f x)) F" 
31355  888 
proof  
889 
from a have "0 < norm a" by simp 

890 
hence "\<exists>r>0. r < norm a" by (rule dense) 

891 
then obtain r where r1: "0 < r" and r2: "r < norm a" by fast 

44195  892 
have "eventually (\<lambda>x. dist (f x) a < r) F" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

893 
using tendstoD [OF f r1] by fast 
44195  894 
hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a  r)) F" 
31355  895 
proof (rule eventually_elim1) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

896 
fix x 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

897 
assume "dist (f x) a < r" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

898 
hence 1: "norm (f x  a) < r" 
31355  899 
by (simp add: dist_norm) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

900 
hence 2: "f x \<noteq> 0" using r2 by auto 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

901 
hence "norm (inverse (f x)) = inverse (norm (f x))" 
31355  902 
by (rule nonzero_norm_inverse) 
903 
also have "\<dots> \<le> inverse (norm a  r)" 

904 
proof (rule le_imp_inverse_le) 

905 
show "0 < norm a  r" using r2 by simp 

906 
next 

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

907 
have "norm a  norm (f x) \<le> norm (a  f x)" 
31355  908 
by (rule norm_triangle_ineq2) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

909 
also have "\<dots> = norm (f x  a)" 
31355  910 
by (rule norm_minus_commute) 
911 
also have "\<dots> < r" using 1 . 

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

912 
finally show "norm a  r \<le> norm (f x)" by simp 
31355  913 
qed 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

914 
finally show "norm (inverse (f x)) \<le> inverse (norm a  r)" . 
31355  915 
qed 
916 
thus ?thesis by (rule BfunI) 

917 
qed 

918 

31565  919 
lemma tendsto_inverse [tendsto_intros]: 
31355  920 
fixes a :: "'a::real_normed_div_algebra" 
44195  921 
assumes f: "(f > a) F" 
31355  922 
assumes a: "a \<noteq> 0" 
44195  923 
shows "((\<lambda>x. inverse (f x)) > inverse a) F" 
31355  924 
proof  
925 
from a have "0 < norm a" by simp 

44195  926 
with f have "eventually (\<lambda>x. dist (f x) a < norm a) F" 
31355  927 
by (rule tendstoD) 
44195  928 
then have "eventually (\<lambda>x. f x \<noteq> 0) F" 
31355  929 
unfolding dist_norm by (auto elim!: eventually_elim1) 
44627  930 
with a have "eventually (\<lambda>x. inverse (f x)  inverse a = 
931 
 (inverse (f x) * (f x  a) * inverse a)) F" 

932 
by (auto elim!: eventually_elim1 simp: inverse_diff_inverse) 

933 
moreover have "Zfun (\<lambda>x.  (inverse (f x) * (f x  a) * inverse a)) F" 

934 
by (intro Zfun_minus Zfun_mult_left 

935 
bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult] 

936 
Bfun_inverse [OF f a] f [unfolded tendsto_Zfun_iff]) 

937 
ultimately show ?thesis 

938 
unfolding tendsto_Zfun_iff by (rule Zfun_ssubst) 

31355  939 
qed 
940 

31565  941 
lemma tendsto_divide [tendsto_intros]: 
31355  942 
fixes a b :: "'a::real_normed_field" 
44195  943 
shows "\<lbrakk>(f > a) F; (g > b) F; b \<noteq> 0\<rbrakk> 
944 
\<Longrightarrow> ((\<lambda>x. f x / g x) > a / b) F" 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

945 
by (simp add: tendsto_mult tendsto_inverse divide_inverse) 
31355  946 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

947 
lemma tendsto_sgn [tendsto_intros]: 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

948 
fixes l :: "'a::real_normed_vector" 
44195  949 
shows "\<lbrakk>(f > l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) > sgn l) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

950 
unfolding sgn_div_norm by (simp add: tendsto_intros) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

951 

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

952 
end 