author  huffman 
Sat, 20 Aug 2011 06:34:51 0700  
changeset 44342  8321948340ea 
parent 44282  f0de18b62d63 
child 44568  e6f291cb5810 
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 

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

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

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

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

337 

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

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

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

340 
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

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

342 

31392  343 

31355  344 
subsection {* Boundedness *} 
345 

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

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

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

349 
lemma BfunI: 
44195  350 
assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) F" shows "Bfun f F" 
31355  351 
unfolding Bfun_def 
352 
proof (intro exI conjI allI) 

353 
show "0 < max K 1" by simp 

354 
next 

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

358 

359 
lemma BfunE: 

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

31355  362 
using assms unfolding Bfun_def by fast 
363 

364 

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

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

366 

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

367 
definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" 
44195  368 
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

369 

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

370 
lemma ZfunI: 
44195  371 
"(\<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

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

373 

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

374 
lemma ZfunD: 
44195  375 
"\<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

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

377 

31355  378 
lemma Zfun_ssubst: 
44195  379 
"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

380 
unfolding Zfun_def by (auto elim!: eventually_rev_mp) 
31355  381 

44195  382 
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

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

384 

44195  385 
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

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 

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

388 
lemma Zfun_imp_Zfun: 
44195  389 
assumes f: "Zfun f F" 
390 
assumes g: "eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F" 

391 
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

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

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

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

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

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

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

398 
using K by (rule divide_pos_pos) 
44195  399 
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

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

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

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

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

406 
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

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

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

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

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

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

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

414 
hence K: "K \<le> 0" by (simp only: not_less) 
31355  415 
show ?thesis 
416 
proof (rule ZfunI) 

417 
fix r :: real 

418 
assume "0 < r" 

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

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

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

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

425 
finally show "norm (g x) < r" 
31355  426 
using `0 < r` by simp 
427 
qed 

428 
qed 

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

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

430 

44195  431 
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

432 
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

433 

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

434 
lemma Zfun_add: 
44195  435 
assumes f: "Zfun f F" and g: "Zfun g F" 
436 
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

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

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

439 
hence r: "0 < r / 2" by simp 
44195  440 
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

441 
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

442 
moreover 
44195  443 
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

444 
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

445 
ultimately 
44195  446 
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

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

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

449 
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

450 
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

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

452 
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

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

454 
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

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

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

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

458 

44195  459 
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

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

461 

44195  462 
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

463 
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

464 

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

465 
lemma (in bounded_linear) Zfun: 
44195  466 
assumes g: "Zfun g F" 
467 
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

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

469 
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

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

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

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

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

476 

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

477 
lemma (in bounded_bilinear) Zfun: 
44195  478 
assumes f: "Zfun f F" 
479 
assumes g: "Zfun g F" 

480 
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

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

482 
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

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

484 
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

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

486 
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

487 
by (rule positive_imp_inverse_positive) 
44195  488 
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

489 
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

490 
moreover 
44195  491 
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

492 
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

493 
ultimately 
44195  494 
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

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

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

497 
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

498 
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

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

500 
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

501 
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

502 
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

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

504 
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

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

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

507 

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

508 
lemma (in bounded_bilinear) Zfun_left: 
44195  509 
"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

510 
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

511 

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

512 
lemma (in bounded_bilinear) Zfun_right: 
44195  513 
"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

514 
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

515 

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

516 
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

517 
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

518 
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

519 

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

520 

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

522 

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

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

524 
tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr ">" 55) where 
44195  525 
"(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

526 

31902  527 
ML {* 
528 
structure Tendsto_Intros = Named_Thms 

529 
( 

530 
val name = "tendsto_intros" 

531 
val description = "introduction rules for tendsto" 

532 
) 

31565  533 
*} 
534 

31902  535 
setup Tendsto_Intros.setup 
31565  536 

44195  537 
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

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

539 

31488  540 
lemma topological_tendstoI: 
44195  541 
"(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) 
542 
\<Longrightarrow> (f > l) F" 

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

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

544 

31488  545 
lemma topological_tendstoD: 
44195  546 
"(f > l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F" 
31488  547 
unfolding tendsto_def by auto 
548 

549 
lemma tendstoI: 

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

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

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

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

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

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

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

557 
done 
31488  558 

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

559 
lemma tendstoD: 
44195  560 
"(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

561 
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

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

563 
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

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

565 
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

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

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

568 
done 
31488  569 

570 
lemma tendsto_iff: 

44195  571 
"(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

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

573 

44195  574 
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

575 
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

576 

31565  577 
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

578 
unfolding tendsto_def eventually_at_topological by auto 
31565  579 

580 
lemma tendsto_ident_at_within [tendsto_intros]: 

36655  581 
"((\<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

582 
unfolding tendsto_def eventually_within eventually_at_topological by auto 
31565  583 

44195  584 
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

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

586 

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

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

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

589 
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

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

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

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

593 
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

594 
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

595 
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

596 
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

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

598 
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

599 
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

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

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

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

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

604 
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

605 
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

606 
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

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

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

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

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

611 

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

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

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

614 
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

615 
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

616 

44218  617 
lemma tendsto_compose: 
618 
assumes g: "(g > g l) (at l)" 

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

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

621 
proof (rule topological_tendstoI) 

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

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

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

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

626 
unfolding eventually_at_topological by fast 

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

628 
from this topological_tendstoD [OF f A] 

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

630 
by (rule eventually_mono) 

631 
qed 

632 

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

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

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

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

636 
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

637 
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

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

639 
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

640 
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

641 
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

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

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

644 
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

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

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

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

648 

44251  649 
lemma metric_tendsto_imp_tendsto: 
650 
assumes f: "(f > a) F" 

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

652 
shows "(g > b) F" 

653 
proof (rule tendstoI) 

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

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

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

657 
using le_less_trans by (rule eventually_elim2) 

658 
qed 

659 

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

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

661 

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

31565  665 
proof (rule tendstoI) 
666 
fix e :: real assume "0 < e" 

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

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

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

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

673 
unfolding dist_real_def 

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

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

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

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

678 
by arith 

679 
qed 

680 
qed 

681 

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

682 
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

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

684 

31565  685 
lemma tendsto_norm [tendsto_intros]: 
44195  686 
"(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

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

688 

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

689 
lemma tendsto_norm_zero: 
44195  690 
"(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

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

692 

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

693 
lemma tendsto_norm_zero_cancel: 
44195  694 
"((\<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

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

696 

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

697 
lemma tendsto_norm_zero_iff: 
44195  698 
"((\<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

699 
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

700 

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

701 
lemma tendsto_rabs [tendsto_intros]: 
44195  702 
"(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

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

704 

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

705 
lemma tendsto_rabs_zero: 
44195  706 
"(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

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

708 

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

709 
lemma tendsto_rabs_zero_cancel: 
44195  710 
"((\<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

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

712 

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

713 
lemma tendsto_rabs_zero_iff: 
44195  714 
"((\<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

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

716 

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

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

718 

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

720 
fixes a b :: "'a::real_normed_vector" 
44195  721 
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

722 
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

723 

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

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

725 
fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector" 
44195  726 
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

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

728 

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

730 
fixes a :: "'a::real_normed_vector" 
44195  731 
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

732 
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

733 

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

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

735 
fixes a :: "'a::real_normed_vector" 
44195  736 
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

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

738 

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

740 
fixes a b :: "'a::real_normed_vector" 
44195  741 
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

742 
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

743 

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

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

31588  748 
proof (cases "finite S") 
749 
assume "finite S" thus ?thesis using assms 

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

750 
by (induct, simp add: tendsto_const, simp add: tendsto_add) 
31588  751 
next 
752 
assume "\<not> finite S" thus ?thesis 

753 
by (simp add: tendsto_const) 

754 
qed 

755 

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

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

757 

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

758 
lemma (in bounded_linear) tendsto: 
44195  759 
"(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

760 
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

761 

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

762 
lemma (in bounded_linear) tendsto_zero: 
44195  763 
"(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

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

765 

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

766 
lemma (in bounded_bilinear) tendsto: 
44195  767 
"\<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

768 
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

769 
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

770 

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

771 
lemma (in bounded_bilinear) tendsto_zero: 
44195  772 
assumes f: "(f > 0) F" 
773 
assumes g: "(g > 0) F" 

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

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

775 
using tendsto [OF f g] by (simp add: zero_left) 
31355  776 

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

777 
lemma (in bounded_bilinear) tendsto_left_zero: 
44195  778 
"(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

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

780 

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

781 
lemma (in bounded_bilinear) tendsto_right_zero: 
44195  782 
"(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

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

784 

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

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

786 
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

787 

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

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

789 
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

790 

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

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

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

793 

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

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

795 
fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}" 
44195  796 
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

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

798 

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

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

800 
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}" 
44195  801 
assumes "\<And>i. i \<in> S \<Longrightarrow> (f i > L i) F" 
802 
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

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

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

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

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

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

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

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

810 

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

811 
subsubsection {* Inverse and division *} 
31355  812 

813 
lemma (in bounded_bilinear) Zfun_prod_Bfun: 

44195  814 
assumes f: "Zfun f F" 
815 
assumes g: "Bfun g F" 

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

31355  817 
proof  
818 
obtain K where K: "0 \<le> K" 

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

820 
using nonneg_bounded by fast 

821 
obtain B where B: "0 < B" 

44195  822 
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

823 
using g by (rule BfunE) 
44195  824 
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

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

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

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

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

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

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

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

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

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

838 
by (rule Zfun_imp_Zfun) 
31355  839 
qed 
840 

841 
lemma (in bounded_bilinear) flip: 

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

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

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

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

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

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

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

849 
using bounded by fast 
31355  850 

851 
lemma (in bounded_bilinear) Bfun_prod_Zfun: 

44195  852 
assumes f: "Bfun f F" 
853 
assumes g: "Zfun g F" 

854 
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

855 
using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) 
31355  856 

857 
lemma Bfun_inverse_lemma: 

858 
fixes x :: "'a::real_normed_div_algebra" 

859 
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

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

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

862 
done 
31355  863 

864 
lemma Bfun_inverse: 

865 
fixes a :: "'a::real_normed_div_algebra" 

44195  866 
assumes f: "(f > a) F" 
31355  867 
assumes a: "a \<noteq> 0" 
44195  868 
shows "Bfun (\<lambda>x. inverse (f x)) F" 
31355  869 
proof  
870 
from a have "0 < norm a" by simp 

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

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

44195  873 
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

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

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

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

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

881 
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

882 
hence "norm (inverse (f x)) = inverse (norm (f x))" 
31355  883 
by (rule nonzero_norm_inverse) 
884 
also have "\<dots> \<le> inverse (norm a  r)" 

885 
proof (rule le_imp_inverse_le) 

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

887 
next 

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

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

890 
also have "\<dots> = norm (f x  a)" 
31355  891 
by (rule norm_minus_commute) 
892 
also have "\<dots> < r" using 1 . 

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

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

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

898 
qed 

899 

900 
lemma tendsto_inverse_lemma: 

901 
fixes a :: "'a::real_normed_div_algebra" 

44195  902 
shows "\<lbrakk>(f > a) F; a \<noteq> 0; eventually (\<lambda>x. f x \<noteq> 0) F\<rbrakk> 
903 
\<Longrightarrow> ((\<lambda>x. inverse (f x)) > inverse a) F" 

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

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

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

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

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

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

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

910 
apply (rule bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult]) 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

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

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

913 
done 
31355  914 

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

44195  922 
with f have "eventually (\<lambda>x. dist (f x) a < norm a) F" 
31355  923 
by (rule tendstoD) 
44195  924 
then have "eventually (\<lambda>x. f x \<noteq> 0) F" 
31355  925 
unfolding dist_norm by (auto elim!: eventually_elim1) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

926 
with f a show ?thesis 
31355  927 
by (rule tendsto_inverse_lemma) 
928 
qed 

929 

31565  930 
lemma tendsto_divide [tendsto_intros]: 
31355  931 
fixes a b :: "'a::real_normed_field" 
44195  932 
shows "\<lbrakk>(f > a) F; (g > b) F; b \<noteq> 0\<rbrakk> 
933 
\<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

934 
by (simp add: tendsto_mult tendsto_inverse divide_inverse) 
31355  935 

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

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

937 
fixes l :: "'a::real_normed_vector" 
44195  938 
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

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

940 

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

941 
end 