author  huffman 
Thu, 11 Jun 2009 11:51:12 0700  
changeset 31565  da5a5589418e 
parent 31492  5400beeddb55 
child 31588  2651f172c38b 
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 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

8 
imports RealVector RComplete 
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 

31392  11 
subsection {* Nets *} 
12 

13 
text {* 

14 
A net is now defined as a filter base. 

15 
The definition also allows nonproper filter bases. 

16 
*} 

17 

18 
typedef (open) 'a net = 

19 
"{net :: 'a set set. (\<exists>A. A \<in> net) 

20 
\<and> (\<forall>A\<in>net. \<forall>B\<in>net. \<exists>C\<in>net. C \<subseteq> A \<and> C \<subseteq> B)}" 

21 
proof 

22 
show "UNIV \<in> ?net" by auto 

23 
qed 

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

24 

31392  25 
lemma Rep_net_nonempty: "\<exists>A. A \<in> Rep_net net" 
26 
using Rep_net [of net] by simp 

27 

28 
lemma Rep_net_directed: 

29 
"A \<in> Rep_net net \<Longrightarrow> B \<in> Rep_net net \<Longrightarrow> \<exists>C\<in>Rep_net net. C \<subseteq> A \<and> C \<subseteq> B" 

30 
using Rep_net [of net] by simp 

31 

32 
lemma Abs_net_inverse': 

33 
assumes "\<exists>A. A \<in> net" 

34 
assumes "\<And>A B. A \<in> net \<Longrightarrow> B \<in> net \<Longrightarrow> \<exists>C\<in>net. C \<subseteq> A \<and> C \<subseteq> B" 

35 
shows "Rep_net (Abs_net net) = net" 

36 
using assms by (simp add: Abs_net_inverse) 

37 

38 
lemma image_nonempty: "\<exists>x. x \<in> A \<Longrightarrow> \<exists>x. x \<in> f ` A" 

39 
by auto 

40 

41 

42 
subsection {* Eventually *} 

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

43 

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

44 
definition 
31392  45 
eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where 
46 
[code del]: "eventually P net \<longleftrightarrow> (\<exists>A\<in>Rep_net net. \<forall>x\<in>A. P x)" 

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

47 

31392  48 
lemma eventually_True [simp]: "eventually (\<lambda>x. True) net" 
49 
unfolding eventually_def using Rep_net_nonempty [of net] by fast 

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

50 

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

51 
lemma eventually_mono: 
31392  52 
"(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P net \<Longrightarrow> eventually Q net" 
53 
unfolding eventually_def by blast 

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

54 

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

55 
lemma eventually_conj: 
31392  56 
assumes P: "eventually (\<lambda>x. P x) net" 
57 
assumes Q: "eventually (\<lambda>x. Q x) net" 

58 
shows "eventually (\<lambda>x. P x \<and> Q x) net" 

59 
proof  

60 
obtain A where A: "A \<in> Rep_net net" "\<forall>x\<in>A. P x" 

61 
using P unfolding eventually_def by fast 

62 
obtain B where B: "B \<in> Rep_net net" "\<forall>x\<in>B. Q x" 

63 
using Q unfolding eventually_def by fast 

64 
obtain C where C: "C \<in> Rep_net net" "C \<subseteq> A" "C \<subseteq> B" 

65 
using Rep_net_directed [OF A(1) B(1)] by fast 

66 
then have "\<forall>x\<in>C. P x \<and> Q x" "C \<in> Rep_net net" 

67 
using A(2) B(2) by auto 

68 
then show ?thesis unfolding eventually_def .. 

69 
qed 

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: 
31392  72 
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) net" 
73 
assumes "eventually (\<lambda>x. P x) net" 

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

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 
31392  77 
show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) net" 
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: 
31392  82 
assumes "eventually (\<lambda>x. P x) net" 
83 
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) net" 

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

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: 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

88 
"eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

89 
by (auto intro: eventually_conj elim: eventually_rev_mp) 
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: 
31392  92 
assumes "eventually (\<lambda>i. P i) net" 
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" 
31392  94 
shows "eventually (\<lambda>i. Q i) net" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

95 
using assms by (auto elim!: eventually_rev_mp) 
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: 
31392  98 
assumes "eventually (\<lambda>i. P i) net" 
99 
assumes "eventually (\<lambda>i. Q i) net" 

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" 
31392  101 
shows "eventually (\<lambda>i. R i) net" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

103 

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

104 

31392  105 
subsection {* Standard Nets *} 
106 

107 
definition 

108 
sequentially :: "nat net" where 

109 
[code del]: "sequentially = Abs_net (range (\<lambda>n. {n..}))" 

110 

111 
definition 

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

112 
within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

113 
[code del]: "net within S = Abs_net ((\<lambda>A. A \<inter> S) ` Rep_net net)" 
31392  114 

115 
definition 

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

116 
at :: "'a::topological_space \<Rightarrow> 'a net" where 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset

117 
[code del]: "at a = Abs_net ((\<lambda>S. S  {a}) ` {S. open S \<and> a \<in> S})" 
31392  118 

119 
lemma Rep_net_sequentially: 

120 
"Rep_net sequentially = range (\<lambda>n. {n..})" 

121 
unfolding sequentially_def 

122 
apply (rule Abs_net_inverse') 

123 
apply (rule image_nonempty, simp) 

124 
apply (clarsimp, rename_tac m n) 

125 
apply (rule_tac x="max m n" in exI, auto) 

126 
done 

127 

128 
lemma Rep_net_within: 

129 
"Rep_net (net within S) = (\<lambda>A. A \<inter> S) ` Rep_net net" 

130 
unfolding within_def 

131 
apply (rule Abs_net_inverse') 

132 
apply (rule image_nonempty, rule Rep_net_nonempty) 

133 
apply (clarsimp, rename_tac A B) 

134 
apply (drule (1) Rep_net_directed) 

135 
apply (clarify, rule_tac x=C in bexI, auto) 

136 
done 

137 

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

138 
lemma Rep_net_at: 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset

139 
"Rep_net (at a) = ((\<lambda>S. S  {a}) ` {S. open S \<and> a \<in> S})" 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

140 
unfolding at_def 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

141 
apply (rule Abs_net_inverse') 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

142 
apply (rule image_nonempty) 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset

143 
apply (rule_tac x="UNIV" in exI, simp) 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

144 
apply (clarsimp, rename_tac S T) 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset

145 
apply (rule_tac x="S \<inter> T" in exI, auto simp add: open_Int) 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

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

147 

31392  148 
lemma eventually_sequentially: 
149 
"eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)" 

150 
unfolding eventually_def Rep_net_sequentially by auto 

151 

152 
lemma eventually_within: 

153 
"eventually P (net within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net" 

154 
unfolding eventually_def Rep_net_within by auto 

155 

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

156 
lemma eventually_at_topological: 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset

157 
"eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))" 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

158 
unfolding eventually_def Rep_net_at by auto 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

159 

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

160 
lemma eventually_at: 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

161 
fixes a :: "'a::metric_space" 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset

162 
shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)" 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset

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

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

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

166 
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

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

168 
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

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

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

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

172 

31392  173 

31355  174 
subsection {* Boundedness *} 
175 

176 
definition 

31392  177 
Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

178 
[code del]: "Bfun f net = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) net)" 
31355  179 

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

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

181 
assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) net" shows "Bfun f net" 
31355  182 
unfolding Bfun_def 
183 
proof (intro exI conjI allI) 

184 
show "0 < max K 1" by simp 

185 
next 

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

186 
show "eventually (\<lambda>x. norm (f x) \<le> max K 1) net" 
31355  187 
using K by (rule eventually_elim1, simp) 
188 
qed 

189 

190 
lemma BfunE: 

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

191 
assumes "Bfun f net" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

192 
obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) net" 
31355  193 
using assms unfolding Bfun_def by fast 
194 

195 

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

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

197 

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

198 
definition 
31392  199 
Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

200 
[code del]: "Zfun f net = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) net)" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

201 

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

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

203 
"(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) net) \<Longrightarrow> Zfun f net" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

205 

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

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

207 
"\<lbrakk>Zfun f net; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) net" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

209 

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

211 
"eventually (\<lambda>x. f x = g x) net \<Longrightarrow> Zfun g net \<Longrightarrow> Zfun f net" 
31355  212 
unfolding Zfun_def by (auto elim!: eventually_rev_mp) 
213 

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

214 
lemma Zfun_zero: "Zfun (\<lambda>x. 0) net" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

216 

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

217 
lemma Zfun_norm_iff: "Zfun (\<lambda>x. norm (f x)) net = Zfun (\<lambda>x. f x) net" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

219 

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

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

221 
assumes f: "Zfun f net" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

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

223 
shows "Zfun (\<lambda>x. g x) net" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

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

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

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

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

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

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

231 
then have "eventually (\<lambda>x. norm (f x) < r / K) net" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

232 
using ZfunD [OF f] by fast 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

233 
with g show "eventually (\<lambda>x. norm (g x) < r) net" 
31355  234 
proof (rule eventually_elim2) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

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

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

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

238 
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

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

240 
thus "norm (g x) < r" 
31355  241 
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

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

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

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

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

246 
hence K: "K \<le> 0" by (simp only: not_less) 
31355  247 
show ?thesis 
248 
proof (rule ZfunI) 

249 
fix r :: real 

250 
assume "0 < r" 

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

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

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

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

255 
also have "\<dots> \<le> norm (f x) * 0" 
31355  256 
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

257 
finally show "norm (g x) < r" 
31355  258 
using `0 < r` by simp 
259 
qed 

260 
qed 

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

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

262 

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

263 
lemma Zfun_le: "\<lbrakk>Zfun g net; \<forall>x. norm (f x) \<le> norm (g x)\<rbrakk> \<Longrightarrow> Zfun f net" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

265 

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

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

267 
assumes f: "Zfun f net" and g: "Zfun g net" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

268 
shows "Zfun (\<lambda>x. f x + g x) net" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

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

271 
hence r: "0 < r / 2" by simp 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

272 
have "eventually (\<lambda>x. norm (f x) < r/2) net" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

273 
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

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

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

276 
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

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

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

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

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

281 
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

282 
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

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

284 
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

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

286 
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

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

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

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

290 

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

291 
lemma Zfun_minus: "Zfun f net \<Longrightarrow> Zfun (\<lambda>x.  f x) net" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

293 

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

294 
lemma Zfun_diff: "\<lbrakk>Zfun f net; Zfun g net\<rbrakk> \<Longrightarrow> Zfun (\<lambda>x. f x  g x) net" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

296 

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

297 
lemma (in bounded_linear) Zfun: 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

298 
assumes g: "Zfun g net" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

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

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

301 
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

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

303 
then have "eventually (\<lambda>x. norm (f (g x)) \<le> norm (g x) * K) net" 
31355  304 
by simp 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

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

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

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

308 

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

309 
lemma (in bounded_bilinear) Zfun: 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

310 
assumes f: "Zfun f net" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

311 
assumes g: "Zfun g net" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

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

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

314 
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

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

316 
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

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

318 
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

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

320 
have "eventually (\<lambda>x. norm (f x) < r) net" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

321 
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

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

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

324 
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

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

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

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

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

329 
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

330 
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

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

332 
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

333 
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

334 
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

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

336 
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

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

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

339 

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

340 
lemma (in bounded_bilinear) Zfun_left: 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

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

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

343 

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

344 
lemma (in bounded_bilinear) Zfun_right: 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

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

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

347 

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

348 
lemmas Zfun_mult = mult.Zfun 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

349 
lemmas Zfun_mult_right = mult.Zfun_right 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

350 
lemmas Zfun_mult_left = mult.Zfun_left 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

351 

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

352 

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

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

354 

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

355 
definition 
31488  356 
tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool" 
357 
(infixr ">" 55) 

358 
where [code del]: 

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

359 
"(f > l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

360 

31565  361 
ML{* 
362 
structure TendstoIntros = 

363 
NamedThmsFun(val name = "tendsto_intros" 

364 
val description = "introduction rules for tendsto"); 

365 
*} 

366 

367 
setup TendstoIntros.setup 

368 

31488  369 
lemma topological_tendstoI: 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset

370 
"(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

371 
\<Longrightarrow> (f > l) net" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

373 

31488  374 
lemma topological_tendstoD: 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset

375 
"(f > l) net \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net" 
31488  376 
unfolding tendsto_def by auto 
377 

378 
lemma tendstoI: 

379 
assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net" 

380 
shows "(f > l) net" 

381 
apply (rule topological_tendstoI) 

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

382 
apply (simp add: open_dist) 
31488  383 
apply (drule (1) bspec, clarify) 
384 
apply (drule assms) 

385 
apply (erule eventually_elim1, simp) 

386 
done 

387 

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

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

389 
"(f > l) net \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net" 
31488  390 
apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD) 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset

391 
apply (clarsimp simp add: open_dist) 
31488  392 
apply (rule_tac x="e  dist x l" in exI, clarsimp) 
393 
apply (simp only: less_diff_eq) 

394 
apply (erule le_less_trans [OF dist_triangle]) 

395 
apply simp 

396 
apply simp 

397 
done 

398 

399 
lemma tendsto_iff: 

400 
"(f > l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)" 

401 
using tendstoI tendstoD by fast 

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

402 

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

403 
lemma tendsto_Zfun_iff: "(f > a) net = Zfun (\<lambda>x. f x  a) net" 
31488  404 
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

405 

31565  406 
lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) > a) (at a)" 
407 
unfolding tendsto_def eventually_at_topological by auto 

408 

409 
lemma tendsto_ident_at_within [tendsto_intros]: 

410 
"a \<in> S \<Longrightarrow> ((\<lambda>x. x) > a) (at a within S)" 

411 
unfolding tendsto_def eventually_within eventually_at_topological by auto 

412 

413 
lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) > k) net" 

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

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

415 

31565  416 
lemma tendsto_dist [tendsto_intros]: 
417 
assumes f: "(f > l) net" and g: "(g > m) net" 

418 
shows "((\<lambda>x. dist (f x) (g x)) > dist l m) net" 

419 
proof (rule tendstoI) 

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

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

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

423 
show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) net" 

424 
proof (rule eventually_elim2) 

425 
fix x assume "dist (f x) l < e/2" "dist (g x) m < e/2" 

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

427 
unfolding dist_real_def 

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

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

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

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

432 
by arith 

433 
qed 

434 
qed 

435 

436 
lemma tendsto_norm [tendsto_intros]: 

437 
"(f > a) net \<Longrightarrow> ((\<lambda>x. norm (f x)) > norm a) net" 

31488  438 
apply (simp add: tendsto_iff dist_norm, safe) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

439 
apply (drule_tac x="e" in spec, safe) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

440 
apply (erule eventually_elim1) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

441 
apply (erule order_le_less_trans [OF norm_triangle_ineq3]) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

442 
done 
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 add_diff_add: 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

445 
fixes a b c d :: "'a::ab_group_add" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

446 
shows "(a + c)  (b + d) = (a  b) + (c  d)" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

448 

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

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

450 
fixes a b :: "'a::ab_group_add" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

451 
shows "( a)  ( b) =  (a  b)" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

453 

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

455 
fixes a b :: "'a::real_normed_vector" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

456 
shows "\<lbrakk>(f > a) net; (g > b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) > a + b) net" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

458 

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

460 
fixes a :: "'a::real_normed_vector" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

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

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

463 

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

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

465 
fixes a :: "'a::real_normed_vector" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

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

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

468 

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

470 
fixes a b :: "'a::real_normed_vector" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

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

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

473 

31565  474 
lemma (in bounded_linear) tendsto [tendsto_intros]: 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

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

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

477 

31565  478 
lemma (in bounded_bilinear) tendsto [tendsto_intros]: 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

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

480 
by (simp only: tendsto_Zfun_iff prod_diff_prod 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

482 

31355  483 

484 
subsection {* Continuity of Inverse *} 

485 

486 
lemma (in bounded_bilinear) Zfun_prod_Bfun: 

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

487 
assumes f: "Zfun f net" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

488 
assumes g: "Bfun g net" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

489 
shows "Zfun (\<lambda>x. f x ** g x) net" 
31355  490 
proof  
491 
obtain K where K: "0 \<le> K" 

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

493 
using nonneg_bounded by fast 

494 
obtain B where B: "0 < B" 

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

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

496 
using g by (rule BfunE) 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

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

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

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

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

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

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

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

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

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

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

511 
by (rule Zfun_imp_Zfun) 
31355  512 
qed 
513 

514 
lemma (in bounded_bilinear) flip: 

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

516 
apply default 

517 
apply (rule add_right) 

518 
apply (rule add_left) 

519 
apply (rule scaleR_right) 

520 
apply (rule scaleR_left) 

521 
apply (subst mult_commute) 

522 
using bounded by fast 

523 

524 
lemma (in bounded_bilinear) Bfun_prod_Zfun: 

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

525 
assumes f: "Bfun f net" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

526 
assumes g: "Zfun g net" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

527 
shows "Zfun (\<lambda>x. f x ** g x) net" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

528 
using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) 
31355  529 

530 
lemma inverse_diff_inverse: 

531 
"\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk> 

532 
\<Longrightarrow> inverse a  inverse b =  (inverse a * (a  b) * inverse b)" 

533 
by (simp add: algebra_simps) 

534 

535 
lemma Bfun_inverse_lemma: 

536 
fixes x :: "'a::real_normed_div_algebra" 

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

538 
apply (subst nonzero_norm_inverse, clarsimp) 

539 
apply (erule (1) le_imp_inverse_le) 

540 
done 

541 

542 
lemma Bfun_inverse: 

543 
fixes a :: "'a::real_normed_div_algebra" 

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

544 
assumes f: "(f > a) net" 
31355  545 
assumes a: "a \<noteq> 0" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

546 
shows "Bfun (\<lambda>x. inverse (f x)) net" 
31355  547 
proof  
548 
from a have "0 < norm a" by simp 

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

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

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

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

552 
using tendstoD [OF f r1] by fast 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

553 
hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a  r)) net" 
31355  554 
proof (rule eventually_elim1) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

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

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

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

559 
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

560 
hence "norm (inverse (f x)) = inverse (norm (f x))" 
31355  561 
by (rule nonzero_norm_inverse) 
562 
also have "\<dots> \<le> inverse (norm a  r)" 

563 
proof (rule le_imp_inverse_le) 

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

565 
next 

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

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

568 
also have "\<dots> = norm (f x  a)" 
31355  569 
by (rule norm_minus_commute) 
570 
also have "\<dots> < r" using 1 . 

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

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

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

576 
qed 

577 

578 
lemma tendsto_inverse_lemma: 

579 
fixes a :: "'a::real_normed_div_algebra" 

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

580 
shows "\<lbrakk>(f > a) net; a \<noteq> 0; eventually (\<lambda>x. f x \<noteq> 0) net\<rbrakk> 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

581 
\<Longrightarrow> ((\<lambda>x. inverse (f x)) > inverse a) net" 
31355  582 
apply (subst tendsto_Zfun_iff) 
583 
apply (rule Zfun_ssubst) 

584 
apply (erule eventually_elim1) 

585 
apply (erule (1) inverse_diff_inverse) 

586 
apply (rule Zfun_minus) 

587 
apply (rule Zfun_mult_left) 

588 
apply (rule mult.Bfun_prod_Zfun) 

589 
apply (erule (1) Bfun_inverse) 

590 
apply (simp add: tendsto_Zfun_iff) 

591 
done 

592 

31565  593 
lemma tendsto_inverse [tendsto_intros]: 
31355  594 
fixes a :: "'a::real_normed_div_algebra" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

595 
assumes f: "(f > a) net" 
31355  596 
assumes a: "a \<noteq> 0" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

597 
shows "((\<lambda>x. inverse (f x)) > inverse a) net" 
31355  598 
proof  
599 
from a have "0 < norm a" by simp 

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

600 
with f have "eventually (\<lambda>x. dist (f x) a < norm a) net" 
31355  601 
by (rule tendstoD) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

602 
then have "eventually (\<lambda>x. f x \<noteq> 0) net" 
31355  603 
unfolding dist_norm by (auto elim!: eventually_elim1) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

604 
with f a show ?thesis 
31355  605 
by (rule tendsto_inverse_lemma) 
606 
qed 

607 

31565  608 
lemma tendsto_divide [tendsto_intros]: 
31355  609 
fixes a b :: "'a::real_normed_field" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

610 
shows "\<lbrakk>(f > a) net; (g > b) net; b \<noteq> 0\<rbrakk> 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

611 
\<Longrightarrow> ((\<lambda>x. f x / g x) > a / b) net" 
31355  612 
by (simp add: mult.tendsto tendsto_inverse divide_inverse) 
613 

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

614 
end 