author  hoelzl 
Thu, 31 Jan 2013 11:31:27 +0100  
changeset 50999  3de230ed0547 
parent 50880  b22ecedde1c7 
child 51022  78de6c7e8a58 
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 

49834  23 
typedef '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 

50880  71 
lemma eventually_Ball_finite: 
72 
assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net" 

73 
shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net" 

74 
using assms by (induct set: finite, simp, simp add: eventually_conj) 

75 

76 
lemma eventually_all_finite: 

77 
fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool" 

78 
assumes "\<And>y. eventually (\<lambda>x. P x y) net" 

79 
shows "eventually (\<lambda>x. \<forall>y. P x y) net" 

80 
using eventually_Ball_finite [of UNIV P] assms by simp 

81 

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

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

85 
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

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

87 
show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp 
44195  88 
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

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

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

91 

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

92 
lemma eventually_rev_mp: 
44195  93 
assumes "eventually (\<lambda>x. P x) F" 
94 
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" 

95 
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

96 
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

97 

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

98 
lemma eventually_conj_iff: 
44195  99 
"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

100 
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

101 

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

102 
lemma eventually_elim1: 
44195  103 
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

104 
assumes "\<And>i. P i \<Longrightarrow> Q i" 
44195  105 
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

106 
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

107 

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

108 
lemma eventually_elim2: 
44195  109 
assumes "eventually (\<lambda>i. P i) F" 
110 
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

111 
assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i" 
44195  112 
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

113 
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

114 

45892  115 
lemma eventually_subst: 
116 
assumes "eventually (\<lambda>n. P n = Q n) F" 

117 
shows "eventually P F = eventually Q F" (is "?L = ?R") 

118 
proof  

119 
from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" 

120 
and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F" 

121 
by (auto elim: eventually_elim1) 

122 
then show ?thesis by (auto elim: eventually_elim2) 

123 
qed 

124 

46886  125 
ML {* 
47432  126 
fun eventually_elim_tac ctxt thms thm = 
127 
let 

46886  128 
val thy = Proof_Context.theory_of ctxt 
129 
val mp_thms = thms RL [@{thm eventually_rev_mp}] 

130 
val raw_elim_thm = 

131 
(@{thm allI} RS @{thm always_eventually}) 

132 
> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms 

133 
> fold (fn _ => fn thm => @{thm impI} RS thm) thms 

134 
val cases_prop = prop_of (raw_elim_thm RS thm) 

135 
val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])]) 

136 
in 

137 
CASES cases (rtac raw_elim_thm 1) thm 

138 
end 

139 
*} 

140 

47432  141 
method_setup eventually_elim = {* 
142 
Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt)) 

143 
*} "elimination of eventually quantifiers" 

45892  144 

145 

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

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

147 

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

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

150 

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

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

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

153 

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

154 
definition le_filter_def: 
44195  155 
"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

156 

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

157 
definition 
44195  158 
"(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

159 

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

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

161 
"top = Abs_filter (\<lambda>P. \<forall>x. P x)" 
36630  162 

163 
definition 

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

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

165 

36630  166 
definition 
44195  167 
"sup F F' = Abs_filter (\<lambda>P. eventually P F \<and> eventually P F')" 
36630  168 

169 
definition 

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

36630  172 

173 
definition 

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

176 
definition 

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

179 
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

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

181 
by (rule eventually_Abs_filter, rule is_filter.intro, auto) 
36630  182 

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

183 
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

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

185 
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

186 

36630  187 
lemma eventually_sup: 
44195  188 
"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

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

190 
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

191 
(auto elim!: eventually_rev_mp) 
36630  192 

193 
lemma eventually_inf: 

44195  194 
"eventually P (inf F F') \<longleftrightarrow> 
195 
(\<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

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

197 
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

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

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

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

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

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

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

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

205 
done 
36630  206 

207 
lemma eventually_Sup: 

44195  208 
"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

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

210 
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

211 
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

212 
done 
36630  213 

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

214 
instance proof 
44195  215 
fix F F' F'' :: "'a filter" and S :: "'a filter set" 
216 
{ show "F < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F" 

217 
by (rule less_filter_def) } 

218 
{ show "F \<le> F" 

219 
unfolding le_filter_def by simp } 

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

221 
unfolding le_filter_def by simp } 

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

223 
unfolding le_filter_def filter_eq_iff by fast } 

224 
{ show "F \<le> top" 

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

226 
{ show "bot \<le> F" 

227 
unfolding le_filter_def by simp } 

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

229 
unfolding le_filter_def eventually_sup by simp_all } 

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

231 
unfolding le_filter_def eventually_sup by simp } 

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

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

234 
{ 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

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

238 
unfolding le_filter_def eventually_Sup by simp } 

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

240 
unfolding le_filter_def eventually_Sup by simp } 

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

242 
unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp } 

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

244 
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

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

246 

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

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

248 

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

249 
lemma filter_leD: 
44195  250 
"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

251 
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

252 

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

253 
lemma filter_leI: 
44195  254 
"(\<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

255 
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

256 

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

257 
lemma eventually_False: 
44195  258 
"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

259 
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

260 

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

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

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

263 

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

264 
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

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

266 

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

267 

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

268 
subsection {* Map function for filters *} 
36654  269 

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

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

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

273 
lemma eventually_filtermap: 
44195  274 
"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

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

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

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

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

279 
done 
36654  280 

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

282 
by (simp add: filter_eq_iff eventually_filtermap) 
36654  283 

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

284 
lemma filtermap_filtermap: 
44195  285 
"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

286 
by (simp add: filter_eq_iff eventually_filtermap) 
36654  287 

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

289 
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

290 

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

291 
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

292 
by (simp add: filter_eq_iff eventually_filtermap) 
36654  293 

50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

294 
lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)" 
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

295 
by (auto simp: filter_eq_iff eventually_filtermap eventually_sup) 
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

296 

50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

297 
subsection {* Order filters *} 
31392  298 

50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

299 
definition at_top :: "('a::order) filter" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

300 
where "at_top = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)" 
31392  301 

50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

302 
lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)" 
50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

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

304 
proof (rule eventually_Abs_filter, rule is_filter.intro) 
50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

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

306 
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

307 
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

308 
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

309 
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

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

311 

50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

312 
lemma eventually_ge_at_top: 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

313 
"eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

314 
unfolding eventually_at_top_linorder by auto 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

315 

50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

316 
lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::dense_linorder. \<forall>n>N. P n)" 
50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

317 
unfolding eventually_at_top_linorder 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

318 
proof safe 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

319 
fix N assume "\<forall>n\<ge>N. P n" then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N]) 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

320 
next 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

321 
fix N assume "\<forall>n>N. P n" 
50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

322 
moreover from gt_ex[of N] guess y .. 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

323 
ultimately show "\<exists>N. \<forall>n\<ge>N. P n" by (auto intro!: exI[of _ y]) 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

324 
qed 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

325 

50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

326 
lemma eventually_gt_at_top: 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

327 
"eventually (\<lambda>x. (c::_::dense_linorder) < x) at_top" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

328 
unfolding eventually_at_top_dense by auto 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

329 

50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

330 
definition at_bot :: "('a::order) filter" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

331 
where "at_bot = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<le>k. P n)" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

332 

491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

333 
lemma eventually_at_bot_linorder: 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

334 
fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

335 
unfolding at_bot_def 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

336 
proof (rule eventually_Abs_filter, rule is_filter.intro) 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

337 
fix P Q :: "'a \<Rightarrow> bool" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

338 
assume "\<exists>i. \<forall>n\<le>i. P n" and "\<exists>j. \<forall>n\<le>j. Q n" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

339 
then obtain i j where "\<forall>n\<le>i. P n" and "\<forall>n\<le>j. Q n" by auto 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

340 
then have "\<forall>n\<le>min i j. P n \<and> Q n" by simp 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

341 
then show "\<exists>k. \<forall>n\<le>k. P n \<and> Q n" .. 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

342 
qed auto 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

343 

50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

344 
lemma eventually_le_at_bot: 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

345 
"eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

346 
unfolding eventually_at_bot_linorder by auto 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

347 

50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

348 
lemma eventually_at_bot_dense: 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

349 
fixes P :: "'a::dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

350 
unfolding eventually_at_bot_linorder 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

351 
proof safe 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

352 
fix N assume "\<forall>n\<le>N. P n" then show "\<exists>N. \<forall>n<N. P n" by (auto intro!: exI[of _ N]) 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

353 
next 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

354 
fix N assume "\<forall>n<N. P n" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

355 
moreover from lt_ex[of N] guess y .. 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

356 
ultimately show "\<exists>N. \<forall>n\<le>N. P n" by (auto intro!: exI[of _ y]) 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

357 
qed 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

358 

50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

359 
lemma eventually_gt_at_bot: 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

360 
"eventually (\<lambda>x. x < (c::_::dense_linorder)) at_bot" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

361 
unfolding eventually_at_bot_dense by auto 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

362 

50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

363 
subsection {* Sequentially *} 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

364 

491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

365 
abbreviation sequentially :: "nat filter" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

366 
where "sequentially == at_top" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

367 

491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

368 
lemma sequentially_def: "sequentially = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

369 
unfolding at_top_def by simp 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

370 

491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

371 
lemma eventually_sequentially: 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

372 
"eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

373 
by (rule eventually_at_top_linorder) 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

374 

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

375 
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

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

377 

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

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

379 

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

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

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

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

383 

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

384 
lemma le_sequentially: 
44195  385 
"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

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

387 
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

388 

45892  389 
lemma eventually_sequentiallyI: 
390 
assumes "\<And>x. c \<le> x \<Longrightarrow> P x" 

391 
shows "eventually P sequentially" 

392 
using assms by (auto simp: eventually_sequentially) 

393 

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

394 

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

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

396 

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

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

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

400 
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

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

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

403 
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

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

405 

50326  406 
abbreviation at_right :: "'a\<Colon>{topological_space, order} \<Rightarrow> 'a filter" where 
407 
"at_right x \<equiv> at x within {x <..}" 

408 

409 
abbreviation at_left :: "'a\<Colon>{topological_space, order} \<Rightarrow> 'a filter" where 

410 
"at_left x \<equiv> at x within {..< x}" 

411 

50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

412 
definition at_infinity :: "'a::real_normed_vector filter" where 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

413 
"at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

414 

31392  415 
lemma eventually_within: 
44195  416 
"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

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

418 
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

419 
(auto elim!: eventually_rev_mp) 
31392  420 

45031  421 
lemma within_UNIV [simp]: "F within UNIV = F" 
422 
unfolding filter_eq_iff eventually_within by simp 

423 

424 
lemma within_empty [simp]: "F within {} = bot" 

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

425 
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

426 

50347  427 
lemma within_within_eq: "(F within S) within T = F within (S \<inter> T)" 
428 
by (auto simp: filter_eq_iff eventually_within elim: eventually_elim1) 

429 

430 
lemma at_within_eq: "at x within T = nhds x within (T  {x})" 

431 
unfolding at_def within_within_eq by (simp add: ac_simps Diff_eq) 

432 

50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

433 
lemma within_le: "F within S \<le> F" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

434 
unfolding le_filter_def eventually_within by (auto elim: eventually_elim1) 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

435 

50323  436 
lemma le_withinI: "F \<le> F' \<Longrightarrow> eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S" 
437 
unfolding le_filter_def eventually_within by (auto elim: eventually_elim2) 

438 

439 
lemma le_within_iff: "eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S \<longleftrightarrow> F \<le> F'" 

440 
by (blast intro: within_le le_withinI order_trans) 

441 

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

444 
unfolding nhds_def 

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

445 
proof (rule eventually_Abs_filter, rule is_filter.intro) 
36654  446 
have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. True)" by simp 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

447 
thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. True)" .. 
36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset

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

449 
fix P Q 
36654  450 
assume "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)" 
451 
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

452 
then obtain S T where 
36654  453 
"open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)" 
454 
"open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)" by auto 

455 
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

456 
by (simp add: open_Int) 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

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

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

459 

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

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

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

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

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

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

465 
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

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

467 
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

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

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

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

471 

50999  472 
lemma eventually_nhds_order: 
473 
"eventually P (nhds (a::'a::linorder_topology)) \<longleftrightarrow> 

474 
(\<exists>S. open_interval S \<and> a \<in> S \<and> (\<forall>z\<in>S. P z))" 

475 
(is "_ \<longleftrightarrow> ?rhs") 

476 
unfolding eventually_nhds by (auto dest!: open_orderD dest: open_interval_imp_open) 

477 

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

480 

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

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

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

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

484 

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

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

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

487 
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

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

489 

50327  490 
lemma eventually_within_less: (* COPY FROM Topo/eventually_within *) 
491 
"eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)" 

492 
unfolding eventually_within eventually_at dist_nz by auto 

493 

494 
lemma eventually_within_le: (* COPY FROM Topo/eventually_within_le *) 

495 
"eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)" 

496 
unfolding eventually_within_less by auto (metis dense order_le_less_trans) 

497 

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

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

501 

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

503 
by (simp add: at_eq_bot_iff not_open_singleton) 

504 

50331  505 
lemma trivial_limit_at_left_real [simp]: (* maybe generalize type *) 
506 
"\<not> trivial_limit (at_left (x::real))" 

507 
unfolding trivial_limit_def eventually_within_le 

508 
apply clarsimp 

509 
apply (rule_tac x="x  d/2" in bexI) 

510 
apply (auto simp: dist_real_def) 

511 
done 

512 

513 
lemma trivial_limit_at_right_real [simp]: (* maybe generalize type *) 

514 
"\<not> trivial_limit (at_right (x::real))" 

515 
unfolding trivial_limit_def eventually_within_le 

516 
apply clarsimp 

517 
apply (rule_tac x="x + d/2" in bexI) 

518 
apply (auto simp: dist_real_def) 

519 
done 

520 

50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

521 
lemma eventually_at_infinity: 
50325  522 
"eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)" 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

523 
unfolding at_infinity_def 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

524 
proof (rule eventually_Abs_filter, rule is_filter.intro) 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

525 
fix P Q :: "'a \<Rightarrow> bool" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

526 
assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<exists>s. \<forall>x. s \<le> norm x \<longrightarrow> Q x" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

527 
then obtain r s where 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

528 
"\<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<forall>x. s \<le> norm x \<longrightarrow> Q x" by auto 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

529 
then have "\<forall>x. max r s \<le> norm x \<longrightarrow> P x \<and> Q x" by simp 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

530 
then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" .. 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

531 
qed auto 
31392  532 

50325  533 
lemma at_infinity_eq_at_top_bot: 
534 
"(at_infinity \<Colon> real filter) = sup at_top at_bot" 

535 
unfolding sup_filter_def at_infinity_def eventually_at_top_linorder eventually_at_bot_linorder 

536 
proof (intro arg_cong[where f=Abs_filter] ext iffI) 

537 
fix P :: "real \<Rightarrow> bool" assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" 

538 
then guess r .. 

539 
then have "(\<forall>x\<ge>r. P x) \<and> (\<forall>x\<le>r. P x)" by auto 

540 
then show "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)" by auto 

541 
next 

542 
fix P :: "real \<Rightarrow> bool" assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)" 

543 
then obtain p q where "\<forall>x\<ge>p. P x" "\<forall>x\<le>q. P x" by auto 

544 
then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" 

545 
by (intro exI[of _ "max p (q)"]) 

546 
(auto simp: abs_real_def) 

547 
qed 

548 

549 
lemma at_top_le_at_infinity: 

550 
"at_top \<le> (at_infinity :: real filter)" 

551 
unfolding at_infinity_eq_at_top_bot by simp 

552 

553 
lemma at_bot_le_at_infinity: 

554 
"at_bot \<le> (at_infinity :: real filter)" 

555 
unfolding at_infinity_eq_at_top_bot by simp 

556 

31355  557 
subsection {* Boundedness *} 
558 

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

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

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

562 
lemma BfunI: 
44195  563 
assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) F" shows "Bfun f F" 
31355  564 
unfolding Bfun_def 
565 
proof (intro exI conjI allI) 

566 
show "0 < max K 1" by simp 

567 
next 

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

571 

572 
lemma BfunE: 

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

31355  575 
using assms unfolding Bfun_def by fast 
576 

577 

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

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

579 

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

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

582 

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

583 
lemma ZfunI: 
44195  584 
"(\<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

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

586 

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

587 
lemma ZfunD: 
44195  588 
"\<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

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

590 

31355  591 
lemma Zfun_ssubst: 
44195  592 
"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

593 
unfolding Zfun_def by (auto elim!: eventually_rev_mp) 
31355  594 

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

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

597 

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

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

600 

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

601 
lemma Zfun_imp_Zfun: 
44195  602 
assumes f: "Zfun f F" 
603 
assumes g: "eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F" 

604 
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

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

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

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

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

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

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

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

613 
using ZfunD [OF f] by fast 
44195  614 
with g show "eventually (\<lambda>x. norm (g x) < r) F" 
46887  615 
proof eventually_elim 
616 
case (elim x) 

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

617 
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

618 
by (simp add: pos_less_divide_eq K) 
46887  619 
thus ?case 
620 
by (simp add: order_le_less_trans [OF elim(1)]) 

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

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

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

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

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

625 
hence K: "K \<le> 0" by (simp only: not_less) 
31355  626 
show ?thesis 
627 
proof (rule ZfunI) 

628 
fix r :: real 

629 
assume "0 < r" 

44195  630 
from g show "eventually (\<lambda>x. norm (g x) < r) F" 
46887  631 
proof eventually_elim 
632 
case (elim x) 

633 
also have "norm (f x) * K \<le> norm (f x) * 0" 

31355  634 
using K norm_ge_zero by (rule mult_left_mono) 
46887  635 
finally show ?case 
31355  636 
using `0 < r` by simp 
637 
qed 

638 
qed 

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

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

640 

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

642 
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

643 

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

644 
lemma Zfun_add: 
44195  645 
assumes f: "Zfun f F" and g: "Zfun g F" 
646 
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

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

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

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

651 
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

652 
moreover 
44195  653 
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

654 
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

655 
ultimately 
44195  656 
show "eventually (\<lambda>x. norm (f x + g x) < r) F" 
46887  657 
proof eventually_elim 
658 
case (elim x) 

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

659 
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

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

661 
also have "\<dots> < r/2 + r/2" 
46887  662 
using elim by (rule add_strict_mono) 
663 
finally show ?case 

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

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

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

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

667 

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

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

670 

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

672 
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

673 

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

674 
lemma (in bounded_linear) Zfun: 
44195  675 
assumes g: "Zfun g F" 
676 
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

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

678 
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

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

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

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

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

685 

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

686 
lemma (in bounded_bilinear) Zfun: 
44195  687 
assumes f: "Zfun f F" 
688 
assumes g: "Zfun g F" 

689 
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

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

691 
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

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

693 
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

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

695 
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

696 
by (rule positive_imp_inverse_positive) 
44195  697 
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

698 
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

699 
moreover 
44195  700 
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

701 
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

702 
ultimately 
44195  703 
show "eventually (\<lambda>x. norm (f x ** g x) < r) F" 
46887  704 
proof eventually_elim 
705 
case (elim x) 

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

706 
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

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

708 
also have "norm (f x) * norm (g x) * K < r * inverse K * K" 
46887  709 
by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero elim K) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

710 
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

711 
by simp 
46887  712 
finally show ?case . 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

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

715 

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

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

718 
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

719 

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

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

722 
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

723 

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

724 
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

725 
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

726 
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

727 

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

728 

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

730 

50322
b06b95a5fda2
rename filter_lim to filterlim to be consistent with filtermap
hoelzl
parents:
50247
diff
changeset

731 
definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where 
b06b95a5fda2
rename filter_lim to filterlim to be consistent with filtermap
hoelzl
parents:
50247
diff
changeset

732 
"filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2" 
50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

733 

491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

734 
syntax 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

735 
"_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10) 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

736 

491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

737 
translations 
50322
b06b95a5fda2
rename filter_lim to filterlim to be consistent with filtermap
hoelzl
parents:
50247
diff
changeset

738 
"LIM x F1. f :> F2" == "CONST filterlim (%x. f) F2 F1" 
50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

739 

50325  740 
lemma filterlim_iff: 
741 
"(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)" 

742 
unfolding filterlim_def le_filter_def eventually_filtermap .. 

50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

743 

50327  744 
lemma filterlim_compose: 
50323  745 
"filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1" 
746 
unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans) 

747 

50327  748 
lemma filterlim_mono: 
50323  749 
"filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'" 
750 
unfolding filterlim_def by (metis filtermap_mono order_trans) 

751 

50419  752 
lemma filterlim_ident: "LIM x F. x :> F" 
753 
by (simp add: filterlim_def filtermap_ident) 

754 

50327  755 
lemma filterlim_cong: 
756 
"F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'" 

757 
by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2) 

758 

50325  759 
lemma filterlim_within: 
760 
"(LIM x F1. f x :> F2 within S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F1 \<and> (LIM x F1. f x :> F2))" 

761 
unfolding filterlim_def 

762 
proof safe 

763 
assume "filtermap f F1 \<le> F2 within S" then show "eventually (\<lambda>x. f x \<in> S) F1" 

764 
by (auto simp: le_filter_def eventually_filtermap eventually_within elim!: allE[of _ "\<lambda>x. x \<in> S"]) 

765 
qed (auto intro: within_le order_trans simp: le_within_iff eventually_filtermap) 

766 

50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

767 
lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2" 
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

768 
unfolding filterlim_def filtermap_filtermap .. 
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

769 

d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

770 
lemma filterlim_sup: 
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

771 
"filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)" 
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

772 
unfolding filterlim_def filtermap_sup by auto 
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

773 

50331  774 
lemma filterlim_Suc: "filterlim Suc sequentially sequentially" 
775 
by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq) 

776 

50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

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

778 
tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr ">" 55) where 
50322
b06b95a5fda2
rename filter_lim to filterlim to be consistent with filtermap
hoelzl
parents:
50247
diff
changeset

779 
"(f > l) F \<equiv> filterlim f (nhds l) F" 
45892  780 

31902  781 
ML {* 
782 
structure Tendsto_Intros = Named_Thms 

783 
( 

45294  784 
val name = @{binding tendsto_intros} 
31902  785 
val description = "introduction rules for tendsto" 
786 
) 

31565  787 
*} 
788 

31902  789 
setup Tendsto_Intros.setup 
31565  790 

50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

791 
lemma tendsto_def: "(f > l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)" 
50322
b06b95a5fda2
rename filter_lim to filterlim to be consistent with filtermap
hoelzl
parents:
50247
diff
changeset

792 
unfolding filterlim_def 
50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

793 
proof safe 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

794 
fix S assume "open S" "l \<in> S" "filtermap f F \<le> nhds l" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

795 
then show "eventually (\<lambda>x. f x \<in> S) F" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

796 
unfolding eventually_nhds eventually_filtermap le_filter_def 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

797 
by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp) 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

798 
qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def) 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

799 

50325  800 
lemma filterlim_at: 
801 
"(LIM x F. f x :> at b) \<longleftrightarrow> (eventually (\<lambda>x. f x \<noteq> b) F \<and> (f > b) F)" 

802 
by (simp add: at_def filterlim_within) 

803 

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

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

806 

31488  807 
lemma topological_tendstoI: 
44195  808 
"(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) 
809 
\<Longrightarrow> (f > l) F" 

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

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

811 

31488  812 
lemma topological_tendstoD: 
44195  813 
"(f > l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F" 
31488  814 
unfolding tendsto_def by auto 
815 

816 
lemma tendstoI: 

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

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

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

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

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

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

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

824 
done 
31488  825 

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

826 
lemma tendstoD: 
44195  827 
"(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

828 
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

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

830 
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

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

832 
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

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

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

835 
done 
31488  836 

837 
lemma tendsto_iff: 

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

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

840 

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

842 
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

843 

45031  844 
lemma tendsto_bot [simp]: "(f > a) bot" 
845 
unfolding tendsto_def by simp 

846 

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

848 
unfolding tendsto_def eventually_at_topological by auto 
31565  849 

850 
lemma tendsto_ident_at_within [tendsto_intros]: 

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

852 
unfolding tendsto_def eventually_within eventually_at_topological by auto 
31565  853 

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

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

856 

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

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

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

859 
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

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

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

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

863 
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

864 
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

865 
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

866 
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

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

868 
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

869 
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

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

871 
have "eventually (\<lambda>x. False) F" 
46887  872 
proof eventually_elim 
873 
case (elim x) 

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

874 
hence "f x \<in> U \<inter> V" by simp 
46887  875 
with `U \<inter> V = {}` show ?case by simp 
44205
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

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

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

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

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

880 

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

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

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

883 
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

884 
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

885 

50323  886 
lemma tendsto_at_iff_tendsto_nhds: 
887 
"(g > g l) (at l) \<longleftrightarrow> (g > g l) (nhds l)" 

888 
unfolding tendsto_def at_def eventually_within 

889 
by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1) 

890 

44218  891 
lemma tendsto_compose: 
50323  892 
"(g > g l) (at l) \<Longrightarrow> (f > l) F \<Longrightarrow> ((\<lambda>x. g (f x)) > g l) F" 
893 
unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g]) 

44218  894 

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

895 
lemma tendsto_compose_eventually: 
50325  896 
"(g > m) (at l) \<Longrightarrow> (f > l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) > m) F" 
897 
by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at) 

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

898 

44251  899 
lemma metric_tendsto_imp_tendsto: 
900 
assumes f: "(f > a) F" 

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

902 
shows "(g > b) F" 

903 
proof (rule tendstoI) 

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

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

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

907 
using le_less_trans by (rule eventually_elim2) 

908 
qed 

909 

50999  910 
lemma increasing_tendsto: 
911 
fixes f :: "_ \<Rightarrow> 'a::linorder_topology" 

912 
assumes bdd: "eventually (\<lambda>n. f n \<le> l) F" 

913 
and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F" 

914 
shows "(f > l) F" 

915 
proof (rule topological_tendstoI) 

916 
fix S assume "open S" "l \<in> S" 

917 
then show "eventually (\<lambda>x. f x \<in> S) F" 

918 
proof (induct rule: open_order_induct) 

919 
case (greaterThanLessThan a b) with en bdd show ?case 

920 
by (auto elim!: eventually_elim2) 

921 
qed (insert en bdd, auto elim!: eventually_elim1) 

922 
qed 

923 

924 
lemma decreasing_tendsto: 

925 
fixes f :: "_ \<Rightarrow> 'a::linorder_topology" 

926 
assumes bdd: "eventually (\<lambda>n. l \<le> f n) F" 

927 
and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F" 

928 
shows "(f > l) F" 

929 
proof (rule topological_tendstoI) 

930 
fix S assume "open S" "l \<in> S" 

931 
then show "eventually (\<lambda>x. f x \<in> S) F" 

932 
proof (induct rule: open_order_induct) 

933 
case (greaterThanLessThan a b) 

934 
with en have "eventually (\<lambda>n. f n < b) F" by auto 

935 
with bdd show ?case 

936 
by eventually_elim (insert greaterThanLessThan, auto) 

937 
qed (insert en bdd, auto elim!: eventually_elim1) 

938 
qed 

939 

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

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

941 

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

31565  945 
proof (rule tendstoI) 
946 
fix e :: real assume "0 < e" 

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

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

44195  949 
show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) F" 
46887  950 
proof (eventually_elim) 
951 
case (elim x) 

31565  952 
then show "dist (dist (f x) (g x)) (dist l m) < e" 
953 
unfolding dist_real_def 

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

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

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

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

958 
by arith 

959 
qed 

960 
qed 

961 

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

962 
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

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

964 

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

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

968 

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

969 
lemma tendsto_norm_zero: 
44195  970 
"(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

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

972 

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

973 
lemma tendsto_norm_zero_cancel: 
44195  974 
"((\<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

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

976 

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

977 
lemma tendsto_norm_zero_iff: 
44195  978 
"((\<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

979 
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

980 

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

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

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

984 

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

985 
lemma tendsto_rabs_zero: 
44195  986 
"(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

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

988 

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

989 
lemma tendsto_rabs_zero_cancel: 
44195  990 
"((\<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

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

992 

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

993 
lemma tendsto_rabs_zero_iff: 
44195  994 
"((\<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

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

996 

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

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

998 

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

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

1002 
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

1003 

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

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

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

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

1008 

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

1010 
fixes a :: "'a::real_normed_vector" 
44195  1011 
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

1012 
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

1013 

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

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

1015 
fixes a :: "'a::real_normed_vector" 
44195  1016 
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

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

1018 

50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

1019 
lemma tendsto_minus_cancel_left: 
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

1020 
"(f >  (y::_::real_normed_vector)) F \<longleftrightarrow> ((\<lambda>x.  f x) > y) F" 
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

1021 
using tendsto_minus_cancel[of f " y" F] tendsto_minus[of f " y" F] 
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

1022 
by auto 
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

1023 

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

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

1027 
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

1028 

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

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

31588  1033 
proof (cases "finite S") 
1034 
assume "finite S" thus ?thesis using assms 

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

1035 
by (induct, simp add: tendsto_const, simp add: tendsto_add) 
31588  1036 
next 
1037 
assume "\<not> finite S" thus ?thesis 

1038 
by (simp add: tendsto_const) 

1039 
qed 

1040 

50999  1041 
lemma tendsto_sandwich: 
1042 
fixes f g h :: "'a \<Rightarrow> 'b::linorder_topology" 

45892  1043 
assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net" 
1044 
assumes lim: "(f > c) net" "(h > c) net" 

1045 
shows "(g > c) net" 

50999  1046 
proof (rule topological_tendstoI) 
1047 
fix S assume "open S" "c \<in> S" 

1048 
from open_orderD[OF this] obtain T where "open_interval T" "c \<in> T" "T \<subseteq> S" by auto 

1049 
with lim[THEN topological_tendstoD, of T] 

1050 
have "eventually (\<lambda>x. f x \<in> T) net" "eventually (\<lambda>x. h x \<in> T) net" 

1051 
by (auto dest: open_interval_imp_open) 

1052 
with ev have "eventually (\<lambda>x. g x \<in> T) net" 

1053 
by eventually_elim (insert `open_interval T`, auto dest: open_intervalD) 

1054 
with `T \<subseteq> S` show "eventually (\<lambda>x. g x \<in> S) net" 

1055 
by (auto elim: eventually_elim1) 

45892  1056 
qed 
1057 

50999  1058 
lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real] 
1059 

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

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

1061 

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

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

1064 
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

1065 

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

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

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

1069 

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

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

1072 
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

1073 
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

1074 

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

1075 
lemma (in bounded_bilinear) tendsto_zero: 
44195  1076 
assumes f: "(f > 0) F" 
1077 
assumes g: "(g > 0) F" 

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

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

1079 
using tendsto [OF f g] by (simp add: zero_left) 
31355  1080 

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

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

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

1084 

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

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

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

1088 

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

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

1090 
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

1091 

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

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

1093 
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

1094 

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

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

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

1097 

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

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

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

1100 

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

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

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

1103 

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

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

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

1106 

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

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

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

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

1111 

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

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

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

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

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

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

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

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

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

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

1123 

50999  1124 
lemma tendsto_le: 
1125 
fixes f g :: "'a \<Rightarrow> 'b::linorder_topology" 

50331  1126 
assumes F: "\<not> trivial_limit F" 
50999  1127 
assumes x: "(f > x) F" and y: "(g > y) F" 
1128 
assumes ev: "eventually (\<lambda>x. g x \<le> f x) F" 

1129 
shows "y \<le> x" 

50331  1130 
proof (rule ccontr) 
50999  1131 
assume "\<not> y \<le> x" 
1132 
then have "x < y" by simp 

1133 
from less_separate[OF this] obtain a b where xy: "x \<in> {..<a}" "y \<in> {b <..}" "{..<a} \<inter> {b<..} = {}" 

1134 
by auto 

1135 
then have less: "\<And>x y. x < a \<Longrightarrow> b < y \<Longrightarrow> x < y" 

1136 
by auto 

1137 
from x[THEN topological_tendstoD, of "{..<a}"] y[THEN topological_tendstoD, of "{b <..}"] xy 

1138 
have "eventually (\<lambda>x. f x \<in> {..<a}) F" "eventually (\<lambda>x. g x \<in> {b <..}) F" by auto 

1139 
with ev have "eventually (\<lambda>x. False) F" 

1140 
by eventually_elim (auto dest!: less) 

50331  1141 
with F show False 
1142 
by (simp add: eventually_False) 

1143 
qed 

1144 

50999  1145 
lemma tendsto_le_const: 
1146 
fixes f :: "'a \<Rightarrow> 'b::linorder_topology" 

50331  1147 
assumes F: "\<not> trivial_limit F" 
50999  1148 
assumes x: "(f > x) F" and a: "eventually (\<lambda>x. a \<le> f x) F" 
1149 
shows "a \<le> x" 

1150 
using F x tendsto_const a by (rule tendsto_le) 

50331  1151 

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

1152 
subsubsection {* Inverse and division *} 
31355  1153 

1154 
lemma (in bounded_bilinear) Zfun_prod_Bfun: 

44195  1155 
assumes f: "Zfun f F" 
1156 
assumes g: "Bfun g F" 

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

31355  1158 
proof  
1159 
obtain K where K: "0 \<le> K" 

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

1161 
using nonneg_bounded by fast 

1162 
obtain B where B: "0 < B" 

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

1164 
using g by (rule BfunE) 
44195  1165 
have "eventually (\<lambda>x. norm (f x ** g x) \<le> norm (f x) * (B * K)) F" 
46887  1166 
using norm_g proof eventually_elim 
1167 
case (elim x) 

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

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

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

1171 
by (intro mult_mono' order_refl norm_g norm_ge_zero 
46887  1172 
mult_nonneg_nonneg K elim) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

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

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

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

1178 
by (rule Zfun_imp_Zfun) 
31355  1179 
qed 
1180 

1181 
lemma (in bounded_bilinear) flip: 

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

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

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

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

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

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

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

1189 
using bounded by fast 
31355  1190 

1191 
lemma (in bounded_bilinear) Bfun_prod_Zfun: 

44195  1192 
assumes f: "Bfun f F" 
1193 
assumes g: "Zfun g F" 

1194 
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

1195 
using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) 
31355  1196 

1197 
lemma Bfun_inverse_lemma: 

1198 
fixes x :: "'a::real_normed_div_algebra" 

1199 
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

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

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

1202 
done 
31355  1203 

1204 
lemma Bfun_inverse: 

1205 
fixes a :: "'a::real_normed_div_algebra" 

44195  1206 
assumes f: "(f > a) F" 
31355  1207 
assumes a: "a \<noteq> 0" 
44195  1208 
shows "Bfun (\<lambda>x. inverse (f x)) F" 
31355  1209 
proof  
1210 
from a have "0 < norm a" by simp 

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

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

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

1214 
using tendstoD [OF f r1] by fast 
44195  1215 
hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a  r)) F" 
46887  1216 
proof eventually_elim 
1217 
case (elim x) 

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

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

1220 
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

1221 
hence "norm (inverse (f x)) = inverse (norm (f x))" 
31355  1222 
by (rule nonzero_norm_inverse) 
1223 
also have "\<dots> \<le> inverse (norm a  r)" 

1224 
proof (rule le_imp_inverse_le) 

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

1226 
next 

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

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

1229 
also have "\<dots> = norm (f x  a)" 
31355  1230 
by (rule norm_minus_commute) 
1231 
also have "\<dots> < r" using 1 . 

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

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

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

1237 
qed 

1238 

31565  1239 
lemma tendsto_inverse [tendsto_intros]: 
31355  1240 
fixes a :: "'a::real_normed_div_algebra" 
44195  1241 
assumes f: "(f > a) F" 
31355  1242 
assumes a: "a \<noteq> 0" 
44195  1243 
shows "((\<lambda>x. inverse (f x)) > inverse a) F" 
31355  1244 
proof  
1245 
from a have "0 < norm a" by simp 

44195  1246 
with f have "eventually (\<lambda>x. dist (f x) a < norm a) F" 
31355  1247 
by (rule tendstoD) 
44195  1248 
then have "eventually (\<lambda>x. f x \<noteq> 0) F" 
31355  1249 
unfolding dist_norm by (auto elim!: eventually_elim1) 
44627  1250 
with a have "eventually (\<lambda>x. inverse (f x)  inverse a = 
1251 
 (inverse (f x) * (f x  a) * inverse a)) F" 

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

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

1254 
by (intro Zfun_minus Zfun_mult_left 

1255 
bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult] 

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

1257 
ultimately show ?thesis 

1258 
unfolding tendsto_Zfun_iff by (rule Zfun_ssubst) 

31355  1259 
qed 
1260 

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

1265 
by (simp add: tendsto_mult tendsto_inverse divide_inverse) 
31355  1266 

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

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

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

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

1271 

50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

1272 
subsection {* Limits to @{const at_top} and @{const at_bot} *} 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

1273 

50322
b06b95a5fda2
rename filter_lim to filterlim to be consistent with filtermap
hoelzl
parents:
50247
diff
changeset

1274 
lemma filterlim_at_top: 
50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

1275 
fixes f :: "'a \<Rightarrow> ('b::linorder)" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

1276 
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

1277 
by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1) 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

1278 

a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

1279 
lemma filterlim_at_top_dense: 
50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

1280 
fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" 
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

1281 
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)" 
50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

1282 
by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

1283 
filterlim_at_top[of f F] filterlim_iff[of f at_top F]) 
50247
491c5c81c2e8
introduce filter_lim as a generatlization of tendsto
hoelzl
parents:
49834
diff
changeset

1284 

50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

1285 
lemma filterlim_at_top_ge: 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

1286 
fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl</ 