author  wenzelm 
Tue, 06 Oct 2015 17:46:07 +0200  
changeset 61342  b98cd131e2b5 
parent 61306  9dd394c866fc 
child 61426  d53db136e8fd 
permissions  rwrr 
52265  1 
(* Title: HOL/Topological_Spaces.thy 
51471  2 
Author: Brian Huffman 
3 
Author: Johannes Hölzl 

4 
*) 

5 

60758  6 
section \<open>Topological Spaces\<close> 
51471  7 

8 
theory Topological_Spaces 

51773  9 
imports Main Conditionally_Complete_Lattices 
51471  10 
begin 
11 

57953  12 
named_theorems continuous_intros "structural introduction rules for continuity" 
13 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

14 

60758  15 
subsection \<open>Topological space\<close> 
51471  16 

17 
class "open" = 

18 
fixes "open" :: "'a set \<Rightarrow> bool" 

19 

20 
class topological_space = "open" + 

21 
assumes open_UNIV [simp, intro]: "open UNIV" 

22 
assumes open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)" 

60585  23 
assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union>K)" 
51471  24 
begin 
25 

26 
definition 

27 
closed :: "'a set \<Rightarrow> bool" where 

28 
"closed S \<longleftrightarrow> open ( S)" 

29 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

30 
lemma open_empty [continuous_intros, intro, simp]: "open {}" 
51471  31 
using open_Union [of "{}"] by simp 
32 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

33 
lemma open_Un [continuous_intros, intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)" 
51471  34 
using open_Union [of "{S, T}"] by simp 
35 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

36 
lemma open_UN [continuous_intros, intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)" 
56166  37 
using open_Union [of "B ` A"] by simp 
51471  38 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

39 
lemma open_Inter [continuous_intros, intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)" 
51471  40 
by (induct set: finite) auto 
41 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

42 
lemma open_INT [continuous_intros, intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)" 
56166  43 
using open_Inter [of "B ` A"] by simp 
51471  44 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

45 
lemma openI: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

46 
assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

47 
shows "open S" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

48 
proof  
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

49 
have "open (\<Union>{T. open T \<and> T \<subseteq> S})" by auto 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

50 
moreover have "\<Union>{T. open T \<and> T \<subseteq> S} = S" by (auto dest!: assms) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

51 
ultimately show "open S" by simp 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

52 
qed 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

53 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

54 
lemma closed_empty [continuous_intros, intro, simp]: "closed {}" 
51471  55 
unfolding closed_def by simp 
56 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

57 
lemma closed_Un [continuous_intros, intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)" 
51471  58 
unfolding closed_def by auto 
59 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

60 
lemma closed_UNIV [continuous_intros, intro, simp]: "closed UNIV" 
51471  61 
unfolding closed_def by simp 
62 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

63 
lemma closed_Int [continuous_intros, intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<inter> T)" 
51471  64 
unfolding closed_def by auto 
65 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

66 
lemma closed_INT [continuous_intros, intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)" 
51471  67 
unfolding closed_def by auto 
68 

60585  69 
lemma closed_Inter [continuous_intros, intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter>K)" 
51471  70 
unfolding closed_def uminus_Inf by auto 
71 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

72 
lemma closed_Union [continuous_intros, intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)" 
51471  73 
by (induct set: finite) auto 
74 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

75 
lemma closed_UN [continuous_intros, intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)" 
56166  76 
using closed_Union [of "B ` A"] by simp 
51471  77 

78 
lemma open_closed: "open S \<longleftrightarrow> closed ( S)" 

79 
unfolding closed_def by simp 

80 

81 
lemma closed_open: "closed S \<longleftrightarrow> open ( S)" 

82 
unfolding closed_def by simp 

83 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

84 
lemma open_Diff [continuous_intros, intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S  T)" 
51471  85 
unfolding closed_open Diff_eq by (rule open_Int) 
86 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

87 
lemma closed_Diff [continuous_intros, intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed (S  T)" 
51471  88 
unfolding open_closed Diff_eq by (rule closed_Int) 
89 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

90 
lemma open_Compl [continuous_intros, intro]: "closed S \<Longrightarrow> open ( S)" 
51471  91 
unfolding closed_open . 
92 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

93 
lemma closed_Compl [continuous_intros, intro]: "open S \<Longrightarrow> closed ( S)" 
51471  94 
unfolding open_closed . 
95 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

96 
lemma open_Collect_neg: "closed {x. P x} \<Longrightarrow> open {x. \<not> P x}" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

97 
unfolding Collect_neg_eq by (rule open_Compl) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

98 

87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

99 
lemma open_Collect_conj: assumes "open {x. P x}" "open {x. Q x}" shows "open {x. P x \<and> Q x}" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

100 
using open_Int[OF assms] by (simp add: Int_def) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

101 

87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

102 
lemma open_Collect_disj: assumes "open {x. P x}" "open {x. Q x}" shows "open {x. P x \<or> Q x}" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

103 
using open_Un[OF assms] by (simp add: Un_def) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

104 

87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

105 
lemma open_Collect_ex: "(\<And>i. open {x. P i x}) \<Longrightarrow> open {x. \<exists>i. P i x}" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

106 
using open_UN[of UNIV "\<lambda>i. {x. P i x}"] unfolding Collect_ex_eq by simp 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

107 

87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

108 
lemma open_Collect_imp: "closed {x. P x} \<Longrightarrow> open {x. Q x} \<Longrightarrow> open {x. P x \<longrightarrow> Q x}" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

109 
unfolding imp_conv_disj by (intro open_Collect_disj open_Collect_neg) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

110 

87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

111 
lemma open_Collect_const: "open {x. P}" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

112 
by (cases P) auto 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

113 

87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

114 
lemma closed_Collect_neg: "open {x. P x} \<Longrightarrow> closed {x. \<not> P x}" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

115 
unfolding Collect_neg_eq by (rule closed_Compl) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

116 

87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

117 
lemma closed_Collect_conj: assumes "closed {x. P x}" "closed {x. Q x}" shows "closed {x. P x \<and> Q x}" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

118 
using closed_Int[OF assms] by (simp add: Int_def) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

119 

87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

120 
lemma closed_Collect_disj: assumes "closed {x. P x}" "closed {x. Q x}" shows "closed {x. P x \<or> Q x}" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

121 
using closed_Un[OF assms] by (simp add: Un_def) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

122 

87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

123 
lemma closed_Collect_all: "(\<And>i. closed {x. P i x}) \<Longrightarrow> closed {x. \<forall>i. P i x}" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

124 
using closed_INT[of UNIV "\<lambda>i. {x. P i x}"] unfolding Collect_all_eq by simp 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

125 

87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

126 
lemma closed_Collect_imp: "open {x. P x} \<Longrightarrow> closed {x. Q x} \<Longrightarrow> closed {x. P x \<longrightarrow> Q x}" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

127 
unfolding imp_conv_disj by (intro closed_Collect_disj closed_Collect_neg) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

128 

87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

129 
lemma closed_Collect_const: "closed {x. P}" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

130 
by (cases P) auto 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

131 

51471  132 
end 
133 

60758  134 
subsection\<open>Hausdorff and other separation properties\<close> 
51471  135 

136 
class t0_space = topological_space + 

137 
assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)" 

138 

139 
class t1_space = topological_space + 

140 
assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> x \<in> U \<and> y \<notin> U" 

141 

142 
instance t1_space \<subseteq> t0_space 

143 
proof qed (fast dest: t1_space) 

144 

145 
lemma separation_t1: 

146 
fixes x y :: "'a::t1_space" 

147 
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)" 

148 
using t1_space[of x y] by blast 

149 

150 
lemma closed_singleton: 

151 
fixes a :: "'a::t1_space" 

152 
shows "closed {a}" 

153 
proof  

154 
let ?T = "\<Union>{S. open S \<and> a \<notin> S}" 

155 
have "open ?T" by (simp add: open_Union) 

156 
also have "?T =  {a}" 

157 
by (simp add: set_eq_iff separation_t1, auto) 

158 
finally show "closed {a}" unfolding closed_def . 

159 
qed 

160 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

161 
lemma closed_insert [continuous_intros, simp]: 
51471  162 
fixes a :: "'a::t1_space" 
163 
assumes "closed S" shows "closed (insert a S)" 

164 
proof  

165 
from closed_singleton assms 

166 
have "closed ({a} \<union> S)" by (rule closed_Un) 

167 
thus "closed (insert a S)" by simp 

168 
qed 

169 

170 
lemma finite_imp_closed: 

171 
fixes S :: "'a::t1_space set" 

172 
shows "finite S \<Longrightarrow> closed S" 

173 
by (induct set: finite, simp_all) 

174 

60758  175 
text \<open>T2 spaces are also known as Hausdorff spaces.\<close> 
51471  176 

177 
class t2_space = topological_space + 

178 
assumes hausdorff: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" 

179 

180 
instance t2_space \<subseteq> t1_space 

181 
proof qed (fast dest: hausdorff) 

182 

183 
lemma separation_t2: 

184 
fixes x y :: "'a::t2_space" 

185 
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})" 

186 
using hausdorff[of x y] by blast 

187 

188 
lemma separation_t0: 

189 
fixes x y :: "'a::t0_space" 

190 
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))" 

191 
using t0_space[of x y] by blast 

192 

60758  193 
text \<open>A perfect space is a topological space with no isolated points.\<close> 
51471  194 

195 
class perfect_space = topological_space + 

196 
assumes not_open_singleton: "\<not> open {x}" 

197 

198 

60758  199 
subsection \<open>Generators for toplogies\<close> 
51471  200 

201 
inductive generate_topology for S where 

202 
UNIV: "generate_topology S UNIV" 

203 
 Int: "generate_topology S a \<Longrightarrow> generate_topology S b \<Longrightarrow> generate_topology S (a \<inter> b)" 

204 
 UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology S k) \<Longrightarrow> generate_topology S (\<Union>K)" 

205 
 Basis: "s \<in> S \<Longrightarrow> generate_topology S s" 

206 

207 
hide_fact (open) UNIV Int UN Basis 

208 

209 
lemma generate_topology_Union: 

210 
"(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)" 

56166  211 
using generate_topology.UN [of "K ` I"] by auto 
51471  212 

213 
lemma topological_space_generate_topology: 

214 
"class.topological_space (generate_topology S)" 

61169  215 
by standard (auto intro: generate_topology.intros) 
51471  216 

60758  217 
subsection \<open>Order topologies\<close> 
51471  218 

219 
class order_topology = order + "open" + 

220 
assumes open_generated_order: "open = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))" 

221 
begin 

222 

223 
subclass topological_space 

224 
unfolding open_generated_order 

225 
by (rule topological_space_generate_topology) 

226 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

227 
lemma open_greaterThan [continuous_intros, simp]: "open {a <..}" 
51471  228 
unfolding open_generated_order by (auto intro: generate_topology.Basis) 
229 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

230 
lemma open_lessThan [continuous_intros, simp]: "open {..< a}" 
51471  231 
unfolding open_generated_order by (auto intro: generate_topology.Basis) 
232 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

233 
lemma open_greaterThanLessThan [continuous_intros, simp]: "open {a <..< b}" 
51471  234 
unfolding greaterThanLessThan_eq by (simp add: open_Int) 
235 

236 
end 

237 

238 
class linorder_topology = linorder + order_topology 

239 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

240 
lemma closed_atMost [continuous_intros, simp]: "closed {.. a::'a::linorder_topology}" 
51471  241 
by (simp add: closed_open) 
242 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

243 
lemma closed_atLeast [continuous_intros, simp]: "closed {a::'a::linorder_topology ..}" 
51471  244 
by (simp add: closed_open) 
245 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56329
diff
changeset

246 
lemma closed_atLeastAtMost [continuous_intros, simp]: "closed {a::'a::linorder_topology .. b}" 
51471  247 
proof  
248 
have "{a .. b} = {a ..} \<inter> {.. b}" 

249 
by auto 

250 
then show ?thesis 

251 
by (simp add: closed_Int) 

252 
qed 

253 

254 
lemma (in linorder) less_separate: 

255 
assumes "x < y" 

256 
shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}" 

53381  257 
proof (cases "\<exists>z. x < z \<and> z < y") 
258 
case True 

259 
then obtain z where "x < z \<and> z < y" .. 

51471  260 
then have "x \<in> {..< z} \<and> y \<in> {z <..} \<and> {z <..} \<inter> {..< z} = {}" 
261 
by auto 

262 
then show ?thesis by blast 

263 
next 

53381  264 
case False 
60758  265 
with \<open>x < y\<close> have "x \<in> {..< y} \<and> y \<in> {x <..} \<and> {x <..} \<inter> {..< y} = {}" 
51471  266 
by auto 
267 
then show ?thesis by blast 

268 
qed 

269 

270 
instance linorder_topology \<subseteq> t2_space 

271 
proof 

272 
fix x y :: 'a 

273 
from less_separate[of x y] less_separate[of y x] 

274 
show "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" 

275 
by (elim neqE) (metis open_lessThan open_greaterThan Int_commute)+ 

276 
qed 

277 

51480
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

278 
lemma (in linorder_topology) open_right: 
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

279 
assumes "open S" "x \<in> S" and gt_ex: "x < y" shows "\<exists>b>x. {x ..< b} \<subseteq> S" 
51471  280 
using assms unfolding open_generated_order 
281 
proof induction 

282 
case (Int A B) 

283 
then obtain a b where "a > x" "{x ..< a} \<subseteq> A" "b > x" "{x ..< b} \<subseteq> B" by auto 

284 
then show ?case by (auto intro!: exI[of _ "min a b"]) 

285 
next 

51480
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

286 
case (Basis S) then show ?case by (fastforce intro: exI[of _ y] gt_ex) 
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

287 
qed blast+ 
51471  288 

51480
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

289 
lemma (in linorder_topology) open_left: 
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

290 
assumes "open S" "x \<in> S" and lt_ex: "y < x" shows "\<exists>b<x. {b <.. x} \<subseteq> S" 
51471  291 
using assms unfolding open_generated_order 
292 
proof induction 

293 
case (Int A B) 

294 
then obtain a b where "a < x" "{a <.. x} \<subseteq> A" "b < x" "{b <.. x} \<subseteq> B" by auto 

295 
then show ?case by (auto intro!: exI[of _ "max a b"]) 

296 
next 

51480
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

297 
case (Basis S) then show ?case by (fastforce intro: exI[of _ y] lt_ex) 
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

298 
qed blast+ 
51471  299 

60758  300 
subsubsection \<open>Boolean is an order topology\<close> 
59106  301 

60758  302 
text \<open>It also is a discrete topology, but don't have a type class for it (yet).\<close> 
59106  303 

304 
instantiation bool :: order_topology 

305 
begin 

306 

307 
definition open_bool :: "bool set \<Rightarrow> bool" where 

308 
"open_bool = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))" 

309 

310 
instance 

311 
proof qed (rule open_bool_def) 

312 

313 
end 

314 

315 
lemma open_bool[simp, intro!]: "open (A::bool set)" 

316 
proof  

317 
have *: "{False <..} = {True}" "{..< True} = {False}" 

318 
by auto 

319 
have "A = UNIV \<or> A = {} \<or> A = {False <..} \<or> A = {..< True}" 

320 
using subset_UNIV[of A] unfolding UNIV_bool * by auto 

321 
then show "open A" 

322 
by auto 

323 
qed 

324 

60758  325 
subsubsection \<open>Topological filters\<close> 
51471  326 

327 
definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter" 

57276  328 
where "nhds a = (INF S:{S. open S \<and> a \<in> S}. principal S)" 
51471  329 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

330 
definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter" ("at (_) within (_)" [1000, 60] 60) 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

331 
where "at a within s = inf (nhds a) (principal (s  {a}))" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

332 

cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

333 
abbreviation (in topological_space) at :: "'a \<Rightarrow> 'a filter" ("at") where 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

334 
"at x \<equiv> at x within (CONST UNIV)" 
51471  335 

51473  336 
abbreviation (in order_topology) at_right :: "'a \<Rightarrow> 'a filter" where 
51471  337 
"at_right x \<equiv> at x within {x <..}" 
338 

51473  339 
abbreviation (in order_topology) at_left :: "'a \<Rightarrow> 'a filter" where 
51471  340 
"at_left x \<equiv> at x within {..< x}" 
341 

57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

342 
lemma (in topological_space) nhds_generated_topology: 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

343 
"open = generate_topology T \<Longrightarrow> nhds x = (INF S:{S\<in>T. x \<in> S}. principal S)" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

344 
unfolding nhds_def 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

345 
proof (safe intro!: antisym INF_greatest) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

346 
fix S assume "generate_topology T S" "x \<in> S" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

347 
then show "(INF S:{S \<in> T. x \<in> S}. principal S) \<le> principal S" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

348 
by induction 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

349 
(auto intro: INF_lower order_trans simp add: inf_principal[symmetric] simp del: inf_principal) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

350 
qed (auto intro!: INF_lower intro: generate_topology.intros) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

351 

51473  352 
lemma (in topological_space) eventually_nhds: 
51471  353 
"eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))" 
57276  354 
unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal) 
51471  355 

356 
lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot" 

357 
unfolding trivial_limit_def eventually_nhds by simp 

358 

60182
e1ea5a6379c9
generalized tends over powr; added DERIV rule for powr
hoelzl
parents:
60172
diff
changeset

359 
lemma (in t1_space) t1_space_nhds: 
e1ea5a6379c9
generalized tends over powr; added DERIV rule for powr
hoelzl
parents:
60172
diff
changeset

360 
"x \<noteq> y \<Longrightarrow> (\<forall>\<^sub>F x in nhds x. x \<noteq> y)" 
e1ea5a6379c9
generalized tends over powr; added DERIV rule for powr
hoelzl
parents:
60172
diff
changeset

361 
by (drule t1_space) (auto simp: eventually_nhds) 
e1ea5a6379c9
generalized tends over powr; added DERIV rule for powr
hoelzl
parents:
60172
diff
changeset

362 

57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

363 
lemma at_within_eq: "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s  {x}))" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

364 
unfolding nhds_def at_within_def by (subst INF_inf_const2[symmetric]) (auto simp add: Diff_Int_distrib) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

365 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

366 
lemma eventually_at_filter: 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

367 
"eventually P (at a within s) \<longleftrightarrow> eventually (\<lambda>x. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x) (nhds a)" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

368 
unfolding at_within_def eventually_inf_principal by (simp add: imp_conjL[symmetric] conj_commute) 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

369 

cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

370 
lemma at_le: "s \<subseteq> t \<Longrightarrow> at x within s \<le> at x within t" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

371 
unfolding at_within_def by (intro inf_mono) auto 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

372 

51471  373 
lemma eventually_at_topological: 
51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

374 
"eventually P (at a within s) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x))" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

375 
unfolding eventually_nhds eventually_at_filter by simp 
51471  376 

51481
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

377 
lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a" 
51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

378 
unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I) 
51481
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

379 

61234  380 
lemma at_within_open_NO_MATCH: 
381 
"a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a" 

382 
by (simp only: at_within_open) 

383 

61245  384 
lemma at_within_nhd: 
385 
assumes "x \<in> S" "open S" "T \<inter> S  {x} = U \<inter> S  {x}" 

386 
shows "at x within T = at x within U" 

387 
unfolding filter_eq_iff eventually_at_filter 

388 
proof (intro allI eventually_subst) 

389 
have "eventually (\<lambda>x. x \<in> S) (nhds x)" 

390 
using \<open>x \<in> S\<close> \<open>open S\<close> by (auto simp: eventually_nhds) 

391 
then show "\<forall>\<^sub>F n in nhds x. (n \<noteq> x \<longrightarrow> n \<in> T \<longrightarrow> P n) = (n \<noteq> x \<longrightarrow> n \<in> U \<longrightarrow> P n)" for P 

392 
by eventually_elim (insert \<open>T \<inter> S  {x} = U \<inter> S  {x}\<close>, blast) 

393 
qed 

394 

53859  395 
lemma at_within_empty [simp]: "at a within {} = bot" 
396 
unfolding at_within_def by simp 

397 

53860  398 
lemma at_within_union: "at x within (S \<union> T) = sup (at x within S) (at x within T)" 
399 
unfolding filter_eq_iff eventually_sup eventually_at_filter 

400 
by (auto elim!: eventually_rev_mp) 

401 

51471  402 
lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}" 
403 
unfolding trivial_limit_def eventually_at_topological 

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

405 

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

407 
by (simp add: at_eq_bot_iff not_open_singleton) 

408 

57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

409 
lemma (in order_topology) nhds_order: "nhds x = 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

410 
inf (INF a:{x <..}. principal {..< a}) (INF a:{..< x}. principal {a <..})" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

411 
proof  
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

412 
have 1: "{S \<in> range lessThan \<union> range greaterThan. x \<in> S} = 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

413 
(\<lambda>a. {..< a}) ` {x <..} \<union> (\<lambda>a. {a <..}) ` {..< x}" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

414 
by auto 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

415 
show ?thesis 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

416 
unfolding nhds_generated_topology[OF open_generated_order] INF_union 1 INF_image comp_def .. 
51471  417 
qed 
418 

57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

419 
lemma (in linorder_topology) at_within_order: "UNIV \<noteq> {x} \<Longrightarrow> 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

420 
at x within s = inf (INF a:{x <..}. principal ({..< a} \<inter> s  {x})) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

421 
(INF a:{..< x}. principal ({a <..} \<inter> s  {x}))" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

422 
proof (cases "{x <..} = {}" "{..< x} = {}" rule: case_split[case_product case_split]) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

423 
assume "UNIV \<noteq> {x}" "{x<..} = {}" "{..< x} = {}" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

424 
moreover have "UNIV = {..< x} \<union> {x} \<union> {x <..}" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

425 
by auto 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

426 
ultimately show ?thesis 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

427 
by auto 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

428 
qed (auto simp: at_within_def nhds_order Int_Diff inf_principal[symmetric] INF_inf_const2 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

429 
inf_sup_aci[where 'a="'a filter"] 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

430 
simp del: inf_principal) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

431 

159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

432 
lemma (in linorder_topology) at_left_eq: 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

433 
"y < x \<Longrightarrow> at_left x = (INF a:{..< x}. principal {a <..< x})" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

434 
by (subst at_within_order) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

435 
(auto simp: greaterThan_Int_greaterThan greaterThanLessThan_eq[symmetric] min.absorb2 INF_constant 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

436 
intro!: INF_lower2 inf_absorb2) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

437 

159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

438 
lemma (in linorder_topology) eventually_at_left: 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

439 
"y < x \<Longrightarrow> eventually P (at_left x) \<longleftrightarrow> (\<exists>b<x. \<forall>y>b. y < x \<longrightarrow> P y)" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

440 
unfolding at_left_eq by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

441 

159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

442 
lemma (in linorder_topology) at_right_eq: 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

443 
"x < y \<Longrightarrow> at_right x = (INF a:{x <..}. principal {x <..< a})" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

444 
by (subst at_within_order) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

445 
(auto simp: lessThan_Int_lessThan greaterThanLessThan_eq[symmetric] max.absorb2 INF_constant Int_commute 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

446 
intro!: INF_lower2 inf_absorb1) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

447 

159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

448 
lemma (in linorder_topology) eventually_at_right: 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

449 
"x < y \<Longrightarrow> eventually P (at_right x) \<longleftrightarrow> (\<exists>b>x. \<forall>y>x. y < b \<longrightarrow> P y)" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

450 
unfolding at_right_eq by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def) 
51471  451 

57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

452 
lemma trivial_limit_at_right_top: "at_right (top::_::{order_top, linorder_topology}) = bot" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

453 
unfolding filter_eq_iff eventually_at_topological by auto 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

454 

0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

455 
lemma trivial_limit_at_left_bot: "at_left (bot::_::{order_bot, linorder_topology}) = bot" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

456 
unfolding filter_eq_iff eventually_at_topological by auto 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

457 

51471  458 
lemma trivial_limit_at_left_real [simp]: 
57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

459 
"\<not> trivial_limit (at_left (x::'a::{no_bot, dense_order, linorder_topology}))" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

460 
using lt_ex[of x] 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

461 
by safe (auto simp add: trivial_limit_def eventually_at_left dest: dense) 
51471  462 

463 
lemma trivial_limit_at_right_real [simp]: 

57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

464 
"\<not> trivial_limit (at_right (x::'a::{no_top, dense_order, linorder_topology}))" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

465 
using gt_ex[of x] 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

466 
by safe (auto simp add: trivial_limit_def eventually_at_right dest: dense) 
51471  467 

468 
lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)" 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

469 
by (auto simp: eventually_at_filter filter_eq_iff eventually_sup 
51471  470 
elim: eventually_elim2 eventually_elim1) 
471 

472 
lemma eventually_at_split: 

473 
"eventually P (at (x::'a::linorder_topology)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)" 

474 
by (subst at_eq_sup_left_right) (simp add: eventually_sup) 

475 

60758  476 
subsubsection \<open>Tendsto\<close> 
51471  477 

478 
abbreviation (in topological_space) 

479 
tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr ">" 55) where 

480 
"(f > l) F \<equiv> filterlim f (nhds l) F" 

481 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

482 
definition (in t2_space) Lim :: "'f filter \<Rightarrow> ('f \<Rightarrow> 'a) \<Rightarrow> 'a" where 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

483 
"Lim A f = (THE l. (f > l) A)" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

484 

51471  485 
lemma tendsto_eq_rhs: "(f > x) F \<Longrightarrow> x = y \<Longrightarrow> (f > y) F" 
486 
by simp 

487 

57953  488 
named_theorems tendsto_intros "introduction rules for tendsto" 
60758  489 
setup \<open> 
51471  490 
Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros}, 
57953  491 
fn context => 
492 
Named_Theorems.get (Context.proof_of context) @{named_theorems tendsto_intros} 

493 
> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm]))) 

60758  494 
\<close> 
51471  495 

51473  496 
lemma (in topological_space) tendsto_def: 
497 
"(f > l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)" 

57276  498 
unfolding nhds_def filterlim_INF filterlim_principal by auto 
51471  499 

500 
lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f > l) F' \<Longrightarrow> (f > l) F" 

501 
unfolding tendsto_def le_filter_def by fast 

502 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

503 
lemma tendsto_within_subset: "(f > l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f > l) (at x within T)" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

504 
by (blast intro: tendsto_mono at_le) 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

505 

cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

506 
lemma filterlim_at: 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

507 
"(LIM x F. f x :> at b within s) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> s \<and> f x \<noteq> b) F \<and> (f > b) F)" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

508 
by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute) 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

509 

51473  510 
lemma (in topological_space) topological_tendstoI: 
51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

511 
"(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) \<Longrightarrow> (f > l) F" 
51471  512 
unfolding tendsto_def by auto 
513 

51473  514 
lemma (in topological_space) topological_tendstoD: 
51471  515 
"(f > l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F" 
516 
unfolding tendsto_def by auto 

517 

57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

518 
lemma (in order_topology) order_tendsto_iff: 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

519 
"(f > x) F \<longleftrightarrow> (\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

520 
unfolding nhds_order filterlim_inf filterlim_INF filterlim_principal by auto 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

521 

159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

522 
lemma (in order_topology) order_tendstoI: 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

523 
"(\<And>a. a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F) \<Longrightarrow> (\<And>a. y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F) \<Longrightarrow> 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

524 
(f > y) F" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

525 
unfolding order_tendsto_iff by auto 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

526 

159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

527 
lemma (in order_topology) order_tendstoD: 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

528 
assumes "(f > y) F" 
51471  529 
shows "a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F" 
530 
and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F" 

57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

531 
using assms unfolding order_tendsto_iff by auto 
51471  532 

533 
lemma tendsto_bot [simp]: "(f > a) bot" 

534 
unfolding tendsto_def by simp 

535 

57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

536 
lemma (in linorder_topology) tendsto_max: 
56949  537 
assumes X: "(X > x) net" 
538 
assumes Y: "(Y > y) net" 

539 
shows "((\<lambda>x. max (X x) (Y x)) > max x y) net" 

540 
proof (rule order_tendstoI) 

541 
fix a assume "a < max x y" 

542 
then show "eventually (\<lambda>x. a < max (X x) (Y x)) net" 

543 
using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a] 

544 
by (auto simp: less_max_iff_disj elim: eventually_elim1) 

545 
next 

546 
fix a assume "max x y < a" 

547 
then show "eventually (\<lambda>x. max (X x) (Y x) < a) net" 

548 
using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a] 

549 
by (auto simp: eventually_conj_iff) 

550 
qed 

551 

57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

552 
lemma (in linorder_topology) tendsto_min: 
56949  553 
assumes X: "(X > x) net" 
554 
assumes Y: "(Y > y) net" 

555 
shows "((\<lambda>x. min (X x) (Y x)) > min x y) net" 

556 
proof (rule order_tendstoI) 

557 
fix a assume "a < min x y" 

558 
then show "eventually (\<lambda>x. a < min (X x) (Y x)) net" 

559 
using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a] 

560 
by (auto simp: eventually_conj_iff) 

561 
next 

562 
fix a assume "min x y < a" 

563 
then show "eventually (\<lambda>x. min (X x) (Y x) < a) net" 

564 
using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a] 

565 
by (auto simp: min_less_iff_disj elim: eventually_elim1) 

566 
qed 

567 

58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57953
diff
changeset

568 
lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) > a) (at a within s)" 
51471  569 
unfolding tendsto_def eventually_at_topological by auto 
570 

58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57953
diff
changeset

571 
lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) > k) F" 
51471  572 
by (simp add: tendsto_def) 
573 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

574 
lemma (in t2_space) tendsto_unique: 
57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

575 
assumes "F \<noteq> bot" and "(f > a) F" and "(f > b) F" 
51471  576 
shows "a = b" 
577 
proof (rule ccontr) 

578 
assume "a \<noteq> b" 

579 
obtain U V where "open U" "open V" "a \<in> U" "b \<in> V" "U \<inter> V = {}" 

60758  580 
using hausdorff [OF \<open>a \<noteq> b\<close>] by fast 
51471  581 
have "eventually (\<lambda>x. f x \<in> U) F" 
60758  582 
using \<open>(f > a) F\<close> \<open>open U\<close> \<open>a \<in> U\<close> by (rule topological_tendstoD) 
51471  583 
moreover 
584 
have "eventually (\<lambda>x. f x \<in> V) F" 

60758  585 
using \<open>(f > b) F\<close> \<open>open V\<close> \<open>b \<in> V\<close> by (rule topological_tendstoD) 
51471  586 
ultimately 
587 
have "eventually (\<lambda>x. False) F" 

588 
proof eventually_elim 

589 
case (elim x) 

590 
hence "f x \<in> U \<inter> V" by simp 

60758  591 
with \<open>U \<inter> V = {}\<close> show ?case by simp 
51471  592 
qed 
60758  593 
with \<open>\<not> trivial_limit F\<close> show "False" 
51471  594 
by (simp add: trivial_limit_def) 
595 
qed 

596 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

597 
lemma (in t2_space) tendsto_const_iff: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

598 
assumes "\<not> trivial_limit F" shows "((\<lambda>x. a :: 'a) > b) F \<longleftrightarrow> a = b" 
58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57953
diff
changeset

599 
by (auto intro!: tendsto_unique [OF assms tendsto_const]) 
51471  600 

601 
lemma increasing_tendsto: 

602 
fixes f :: "_ \<Rightarrow> 'a::order_topology" 

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

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

605 
shows "(f > l) F" 

606 
using assms by (intro order_tendstoI) (auto elim!: eventually_elim1) 

607 

608 
lemma decreasing_tendsto: 

609 
fixes f :: "_ \<Rightarrow> 'a::order_topology" 

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

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

612 
shows "(f > l) F" 

613 
using assms by (intro order_tendstoI) (auto elim!: eventually_elim1) 

614 

615 
lemma tendsto_sandwich: 

616 
fixes f g h :: "'a \<Rightarrow> 'b::order_topology" 

617 
assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net" 

618 
assumes lim: "(f > c) net" "(h > c) net" 

619 
shows "(g > c) net" 

620 
proof (rule order_tendstoI) 

621 
fix a show "a < c \<Longrightarrow> eventually (\<lambda>x. a < g x) net" 

622 
using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2) 

623 
next 

624 
fix a show "c < a \<Longrightarrow> eventually (\<lambda>x. g x < a) net" 

625 
using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2) 

626 
qed 

627 

628 
lemma tendsto_le: 

629 
fixes f g :: "'a \<Rightarrow> 'b::linorder_topology" 

630 
assumes F: "\<not> trivial_limit F" 

631 
assumes x: "(f > x) F" and y: "(g > y) F" 

632 
assumes ev: "eventually (\<lambda>x. g x \<le> f x) F" 

633 
shows "y \<le> x" 

634 
proof (rule ccontr) 

635 
assume "\<not> y \<le> x" 

636 
with less_separate[of x y] obtain a b where xy: "x < a" "b < y" "{..<a} \<inter> {b<..} = {}" 

637 
by (auto simp: not_le) 

638 
then have "eventually (\<lambda>x. f x < a) F" "eventually (\<lambda>x. b < g x) F" 

639 
using x y by (auto intro: order_tendstoD) 

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

641 
by eventually_elim (insert xy, fastforce) 

642 
with F show False 

643 
by (simp add: eventually_False) 

644 
qed 

645 

646 
lemma tendsto_le_const: 

647 
fixes f :: "'a \<Rightarrow> 'b::linorder_topology" 

648 
assumes F: "\<not> trivial_limit F" 

56289  649 
assumes x: "(f > x) F" and a: "eventually (\<lambda>i. a \<le> f i) F" 
51471  650 
shows "a \<le> x" 
651 
using F x tendsto_const a by (rule tendsto_le) 

652 

56289  653 
lemma tendsto_ge_const: 
654 
fixes f :: "'a \<Rightarrow> 'b::linorder_topology" 

655 
assumes F: "\<not> trivial_limit F" 

656 
assumes x: "(f > x) F" and a: "eventually (\<lambda>i. a \<ge> f i) F" 

657 
shows "a \<ge> x" 

658 
by (rule tendsto_le [OF F tendsto_const x a]) 

659 

60758  660 
subsubsection \<open>Rules about @{const Lim}\<close> 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

661 

57276  662 
lemma tendsto_Lim: 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

663 
"\<not>(trivial_limit net) \<Longrightarrow> (f > l) net \<Longrightarrow> Lim net f = l" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

664 
unfolding Lim_def using tendsto_unique[of net f] by auto 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

665 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

666 
lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x" 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

667 
by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

668 

51471  669 
lemma filterlim_at_bot_at_right: 
57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

670 
fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder" 
51471  671 
assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y" 
672 
assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)" 

673 
assumes Q: "eventually Q (at_right a)" and bound: "\<And>b. Q b \<Longrightarrow> a < b" 

674 
assumes P: "eventually P at_bot" 

675 
shows "filterlim f at_bot (at_right a)" 

676 
proof  

677 
from P obtain x where x: "\<And>y. y \<le> x \<Longrightarrow> P y" 

678 
unfolding eventually_at_bot_linorder by auto 

679 
show ?thesis 

680 
proof (intro filterlim_at_bot_le[THEN iffD2] allI impI) 

681 
fix z assume "z \<le> x" 

682 
with x have "P z" by auto 

683 
have "eventually (\<lambda>x. x \<le> g z) (at_right a)" 

60758  684 
using bound[OF bij(2)[OF \<open>P z\<close>]] 
685 
unfolding eventually_at_right[OF bound[OF bij(2)[OF \<open>P z\<close>]]] by (auto intro!: exI[of _ "g z"]) 

51471  686 
with Q show "eventually (\<lambda>x. f x \<le> z) (at_right a)" 
60758  687 
by eventually_elim (metis bij \<open>P z\<close> mono) 
51471  688 
qed 
689 
qed 

690 

691 
lemma filterlim_at_top_at_left: 

57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

692 
fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder" 
51471  693 
assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y" 
694 
assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)" 

695 
assumes Q: "eventually Q (at_left a)" and bound: "\<And>b. Q b \<Longrightarrow> b < a" 

696 
assumes P: "eventually P at_top" 

697 
shows "filterlim f at_top (at_left a)" 

698 
proof  

699 
from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y" 

700 
unfolding eventually_at_top_linorder by auto 

701 
show ?thesis 

702 
proof (intro filterlim_at_top_ge[THEN iffD2] allI impI) 

703 
fix z assume "x \<le> z" 

704 
with x have "P z" by auto 

705 
have "eventually (\<lambda>x. g z \<le> x) (at_left a)" 

60758  706 
using bound[OF bij(2)[OF \<open>P z\<close>]] 
707 
unfolding eventually_at_left[OF bound[OF bij(2)[OF \<open>P z\<close>]]] by (auto intro!: exI[of _ "g z"]) 

51471  708 
with Q show "eventually (\<lambda>x. z \<le> f x) (at_left a)" 
60758  709 
by eventually_elim (metis bij \<open>P z\<close> mono) 
51471  710 
qed 
711 
qed 

712 

713 
lemma filterlim_split_at: 

714 
"filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::'a::linorder_topology))" 

715 
by (subst at_eq_sup_left_right) (rule filterlim_sup) 

716 

717 
lemma filterlim_at_split: 

718 
"filterlim f F (at (x::'a::linorder_topology)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)" 

719 
by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup) 

720 

57025  721 
lemma eventually_nhds_top: 
722 
fixes P :: "'a :: {order_top, linorder_topology} \<Rightarrow> bool" 

723 
assumes "(b::'a) < top" 

724 
shows "eventually P (nhds top) \<longleftrightarrow> (\<exists>b<top. (\<forall>z. b < z \<longrightarrow> P z))" 

725 
unfolding eventually_nhds 

726 
proof safe 

727 
fix S :: "'a set" assume "open S" "top \<in> S" 

60758  728 
note open_left[OF this \<open>b < top\<close>] 
57025  729 
moreover assume "\<forall>s\<in>S. P s" 
730 
ultimately show "\<exists>b<top. \<forall>z>b. P z" 

731 
by (auto simp: subset_eq Ball_def) 

732 
next 

733 
fix b assume "b < top" "\<forall>z>b. P z" 

734 
then show "\<exists>S. open S \<and> top \<in> S \<and> (\<forall>xa\<in>S. P xa)" 

735 
by (intro exI[of _ "{b <..}"]) auto 

736 
qed 

51471  737 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

738 
lemma tendsto_at_within_iff_tendsto_nhds: 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

739 
"(g > g l) (at l within S) \<longleftrightarrow> (g > g l) (inf (nhds l) (principal S))" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

740 
unfolding tendsto_def eventually_at_filter eventually_inf_principal 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

741 
by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

742 

60758  743 
subsection \<open>Limits on sequences\<close> 
51471  744 

745 
abbreviation (in topological_space) 

746 
LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool" 

747 
("((_)/ > (_))" [60, 60] 60) where 

748 
"X > L \<equiv> (X > L) sequentially" 

749 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

750 
abbreviation (in t2_space) lim :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

751 
"lim X \<equiv> Lim sequentially X" 
51471  752 

753 
definition (in topological_space) convergent :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where 

754 
"convergent X = (\<exists>L. X > L)" 

755 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

756 
lemma lim_def: "lim X = (THE L. X > L)" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

757 
unfolding Lim_def .. 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

758 

60758  759 
subsubsection \<open>Monotone sequences and subsequences\<close> 
51471  760 

761 
definition 

762 
monoseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where 

60758  763 
\<open>Definition of monotonicity. 
51471  764 
The use of disjunction here complicates proofs considerably. 
765 
One alternative is to add a Boolean argument to indicate the direction. 

60758  766 
Another is to develop the notions of increasing and decreasing first.\<close> 
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55945
diff
changeset

767 
"monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) \<or> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))" 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55945
diff
changeset

768 

f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55945
diff
changeset

769 
abbreviation incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55945
diff
changeset

770 
"incseq X \<equiv> mono X" 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55945
diff
changeset

771 

f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55945
diff
changeset

772 
lemma incseq_def: "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<ge> X m)" 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55945
diff
changeset

773 
unfolding mono_def .. 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55945
diff
changeset

774 

f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55945
diff
changeset

775 
abbreviation decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55945
diff
changeset

776 
"decseq X \<equiv> antimono X" 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55945
diff
changeset

777 

f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55945
diff
changeset

778 
lemma decseq_def: "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)" 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55945
diff
changeset

779 
unfolding antimono_def .. 
51471  780 

781 
definition 

782 
subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where 

60758  783 
\<open>Definition of subsequence\<close> 
51471  784 
"subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)" 
785 

786 
lemma incseq_SucI: 

787 
"(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X" 

788 
using lift_Suc_mono_le[of X] 

789 
by (auto simp: incseq_def) 

790 

791 
lemma incseqD: "\<And>i j. incseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f i \<le> f j" 

792 
by (auto simp: incseq_def) 

793 

794 
lemma incseq_SucD: "incseq A \<Longrightarrow> A i \<le> A (Suc i)" 

795 
using incseqD[of A i "Suc i"] by auto 

796 

797 
lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))" 

798 
by (auto intro: incseq_SucI dest: incseq_SucD) 

799 

800 
lemma incseq_const[simp, intro]: "incseq (\<lambda>x. k)" 

801 
unfolding incseq_def by auto 

802 

803 
lemma decseq_SucI: 

804 
"(\<And>n. X (Suc n) \<le> X n) \<Longrightarrow> decseq X" 

805 
using order.lift_Suc_mono_le[OF dual_order, of X] 

806 
by (auto simp: decseq_def) 

807 

808 
lemma decseqD: "\<And>i j. decseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f j \<le> f i" 

809 
by (auto simp: decseq_def) 

810 

811 
lemma decseq_SucD: "decseq A \<Longrightarrow> A (Suc i) \<le> A i" 

812 
using decseqD[of A i "Suc i"] by auto 

813 

814 
lemma decseq_Suc_iff: "decseq f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)" 

815 
by (auto intro: decseq_SucI dest: decseq_SucD) 

816 

817 
lemma decseq_const[simp, intro]: "decseq (\<lambda>x. k)" 

818 
unfolding decseq_def by auto 

819 

820 
lemma monoseq_iff: "monoseq X \<longleftrightarrow> incseq X \<or> decseq X" 

821 
unfolding monoseq_def incseq_def decseq_def .. 

822 

823 
lemma monoseq_Suc: 

824 
"monoseq X \<longleftrightarrow> (\<forall>n. X n \<le> X (Suc n)) \<or> (\<forall>n. X (Suc n) \<le> X n)" 

825 
unfolding monoseq_iff incseq_Suc_iff decseq_Suc_iff .. 

826 

827 
lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X" 

828 
by (simp add: monoseq_def) 

829 

830 
lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X" 

831 
by (simp add: monoseq_def) 

832 

833 
lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X" 

834 
by (simp add: monoseq_Suc) 

835 

836 
lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X" 

837 
by (simp add: monoseq_Suc) 

838 

839 
lemma monoseq_minus: 

840 
fixes a :: "nat \<Rightarrow> 'a::ordered_ab_group_add" 

841 
assumes "monoseq a" 

842 
shows "monoseq (\<lambda> n.  a n)" 

843 
proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n") 

844 
case True 

845 
hence "\<forall> m. \<forall> n \<ge> m.  a n \<le>  a m" by auto 

846 
thus ?thesis by (rule monoI2) 

847 
next 

848 
case False 

60758  849 
hence "\<forall> m. \<forall> n \<ge> m.  a m \<le>  a n" using \<open>monoseq a\<close>[unfolded monoseq_def] by auto 
51471  850 
thus ?thesis by (rule monoI1) 
851 
qed 

852 

60758  853 
text\<open>Subsequence (alternative definition, (e.g. Hoskins)\<close> 
51471  854 

855 
lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))" 

856 
apply (simp add: subseq_def) 

857 
apply (auto dest!: less_imp_Suc_add) 

858 
apply (induct_tac k) 

859 
apply (auto intro: less_trans) 

860 
done 

861 

60758  862 
text\<open>for any sequence, there is a monotonic subsequence\<close> 
51471  863 
lemma seq_monosub: 
864 
fixes s :: "nat => 'a::linorder" 

57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

865 
shows "\<exists>f. subseq f \<and> monoseq (\<lambda>n. (s (f n)))" 
51471  866 
proof cases 
57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

867 
assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. s m \<le> s p" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

868 
then have "\<exists>f. \<forall>n. (\<forall>m\<ge>f n. s m \<le> s (f n)) \<and> f n < f (Suc n)" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

869 
by (intro dependent_nat_choice) (auto simp: conj_commute) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

870 
then obtain f where "subseq f" and mono: "\<And>n m. f n \<le> m \<Longrightarrow> s m \<le> s (f n)" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

871 
by (auto simp: subseq_Suc_iff) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

872 
moreover 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

873 
then have "incseq f" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

874 
unfolding subseq_Suc_iff incseq_Suc_iff by (auto intro: less_imp_le) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

875 
then have "monoseq (\<lambda>n. s (f n))" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

876 
by (auto simp add: incseq_def intro!: mono monoI2) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

877 
ultimately show ?thesis 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

878 
by auto 
51471  879 
next 
880 
assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))" 

881 
then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less) 

57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

882 
have "\<exists>f. \<forall>n. N < f n \<and> f n < f (Suc n) \<and> s (f n) \<le> s (f (Suc n))" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

883 
proof (intro dependent_nat_choice) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

884 
fix x assume "N < x" with N[of x] show "\<exists>y>N. x < y \<and> s x \<le> s y" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

885 
by (auto intro: less_trans) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

886 
qed auto 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

887 
then show ?thesis 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

888 
by (auto simp: monoseq_iff incseq_Suc_iff subseq_Suc_iff) 
51471  889 
qed 
890 

891 
lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n" 

892 
proof(induct n) 

893 
case 0 thus ?case by simp 

894 
next 

895 
case (Suc n) 

896 
from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps 

897 
have "n < f (Suc n)" by arith 

898 
thus ?case by arith 

899 
qed 

900 

901 
lemma eventually_subseq: 

902 
"subseq r \<Longrightarrow> eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially" 

903 
unfolding eventually_sequentially by (metis seq_suble le_trans) 

904 

51473  905 
lemma not_eventually_sequentiallyD: 
906 
assumes P: "\<not> eventually P sequentially" 

907 
shows "\<exists>r. subseq r \<and> (\<forall>n. \<not> P (r n))" 

908 
proof  

909 
from P have "\<forall>n. \<exists>m\<ge>n. \<not> P m" 

910 
unfolding eventually_sequentially by (simp add: not_less) 

911 
then obtain r where "\<And>n. r n \<ge> n" "\<And>n. \<not> P (r n)" 

912 
by (auto simp: choice_iff) 

913 
then show ?thesis 

914 
by (auto intro!: exI[of _ "\<lambda>n. r (((Suc \<circ> r) ^^ Suc n) 0)"] 

915 
simp: less_eq_Suc_le subseq_Suc_iff) 

916 
qed 

917 

51471  918 
lemma filterlim_subseq: "subseq f \<Longrightarrow> filterlim f sequentially sequentially" 
919 
unfolding filterlim_iff by (metis eventually_subseq) 

920 

921 
lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)" 

922 
unfolding subseq_def by simp 

923 

924 
lemma subseq_mono: assumes "subseq r" "m < n" shows "r m < r n" 

925 
using assms by (auto simp: subseq_def) 

926 

927 
lemma incseq_imp_monoseq: "incseq X \<Longrightarrow> monoseq X" 

928 
by (simp add: incseq_def monoseq_def) 

929 

930 
lemma decseq_imp_monoseq: "decseq X \<Longrightarrow> monoseq X" 

931 
by (simp add: decseq_def monoseq_def) 

932 

933 
lemma decseq_eq_incseq: 

934 
fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n.  X n)" 

935 
by (simp add: decseq_def incseq_def) 

936 

937 
lemma INT_decseq_offset: 

938 
assumes "decseq F" 

939 
shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)" 

940 
proof safe 

941 
fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)" 

942 
show "x \<in> F i" 

943 
proof cases 

944 
from x have "x \<in> F n" by auto 

60758  945 
also assume "i \<le> n" with \<open>decseq F\<close> have "F n \<subseteq> F i" 
51471  946 
unfolding decseq_def by simp 
947 
finally show ?thesis . 

948 
qed (insert x, simp) 

949 
qed auto 

950 

951 
lemma LIMSEQ_const_iff: 

952 
fixes k l :: "'a::t2_space" 

953 
shows "(\<lambda>n. k) > l \<longleftrightarrow> k = l" 

954 
using trivial_limit_sequentially by (rule tendsto_const_iff) 

955 

956 
lemma LIMSEQ_SUP: 

957 
"incseq X \<Longrightarrow> X > (SUP i. X i :: 'a :: {complete_linorder, linorder_topology})" 

958 
by (intro increasing_tendsto) 

959 
(auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans) 

960 

961 
lemma LIMSEQ_INF: 

962 
"decseq X \<Longrightarrow> X > (INF i. X i :: 'a :: {complete_linorder, linorder_topology})" 

963 
by (intro decreasing_tendsto) 

964 
(auto simp: INF_lower INF_less_iff decseq_def eventually_sequentially intro: le_less_trans) 

965 

966 
lemma LIMSEQ_ignore_initial_segment: 

967 
"f > a \<Longrightarrow> (\<lambda>n. f (n + k)) > a" 

51474
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

968 
unfolding tendsto_def 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

969 
by (subst eventually_sequentially_seg[where k=k]) 
51471  970 

971 
lemma LIMSEQ_offset: 

972 
"(\<lambda>n. f (n + k)) > a \<Longrightarrow> f > a" 

51474
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

973 
unfolding tendsto_def 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51473
diff
changeset

974 
by (subst (asm) eventually_sequentially_seg[where k=k]) 
51471  975 

976 
lemma LIMSEQ_Suc: "f > l \<Longrightarrow> (\<lambda>n. f (Suc n)) > l" 

977 
by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp) 

978 

979 
lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) > l \<Longrightarrow> f > l" 

980 
by (rule_tac k="Suc 0" in LIMSEQ_offset, simp) 

981 

982 
lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) > l = f > l" 

983 
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc) 

984 

985 
lemma LIMSEQ_unique: 

986 
fixes a b :: "'a::t2_space" 

987 
shows "\<lbrakk>X > a; X > b\<rbrakk> \<Longrightarrow> a = b" 

988 
using trivial_limit_sequentially by (rule tendsto_unique) 

989 

990 
lemma LIMSEQ_le_const: 

991 
"\<lbrakk>X > (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x" 

992 
using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially) 

993 

994 
lemma LIMSEQ_le: 

995 
"\<lbrakk>X > x; Y > y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::'a::linorder_topology)" 

996 
using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially) 

997 

998 
lemma LIMSEQ_le_const2: 

999 
"\<lbrakk>X > (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a" 

58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57953
diff
changeset

1000 
by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) auto 
51471  1001 

1002 
lemma convergentD: "convergent X ==> \<exists>L. (X > L)" 

1003 
by (simp add: convergent_def) 

1004 

1005 
lemma convergentI: "(X > L) ==> convergent X" 

1006 
by (auto simp add: convergent_def) 

1007 

1008 
lemma convergent_LIMSEQ_iff: "convergent X = (X > lim X)" 

1009 
by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def) 

1010 

1011 
lemma convergent_const: "convergent (\<lambda>n. c)" 

1012 
by (rule convergentI, rule tendsto_const) 

1013 

1014 
lemma monoseq_le: 

1015 
"monoseq a \<Longrightarrow> a > (x::'a::linorder_topology) \<Longrightarrow> 

1016 
((\<forall> n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)) \<or> ((\<forall> n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m))" 

1017 
by (metis LIMSEQ_le_const LIMSEQ_le_const2 decseq_def incseq_def monoseq_iff) 

1018 

1019 
lemma LIMSEQ_subseq_LIMSEQ: 

1020 
"\<lbrakk> X > L; subseq f \<rbrakk> \<Longrightarrow> (X o f) > L" 

1021 
unfolding comp_def by (rule filterlim_compose[of X, OF _ filterlim_subseq]) 

1022 

1023 
lemma convergent_subseq_convergent: 

1024 
"\<lbrakk>convergent X; subseq f\<rbrakk> \<Longrightarrow> convergent (X o f)" 

1025 
unfolding convergent_def by (auto intro: LIMSEQ_subseq_LIMSEQ) 

1026 

1027 
lemma limI: "X > L ==> lim X = L" 

57276  1028 
by (rule tendsto_Lim) (rule trivial_limit_sequentially) 
51471  1029 

1030 
lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::'a::linorder_topology)) \<Longrightarrow> lim f \<le> x" 

1031 
using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff) 

1032 

60758  1033 
subsubsection\<open>Increasing and Decreasing Series\<close> 
51471  1034 

1035 
lemma incseq_le: "incseq X \<Longrightarrow> X > L \<Longrightarrow> X n \<le> (L::'a::linorder_topology)" 

1036 
by (metis incseq_def LIMSEQ_le_const) 

1037 

1038 
lemma decseq_le: "decseq X \<Longrightarrow> X > L \<Longrightarrow> (L::'a::linorder_topology) \<le> X n" 

1039 
by (metis decseq_def LIMSEQ_le_const2) 

1040 

60758  1041 
subsection \<open>First countable topologies\<close> 
51473  1042 

1043 
class first_countable_topology = topological_space + 

1044 
assumes first_countable_basis: 

1045 
"\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" 

1046 

1047 
lemma (in first_countable_topology) countable_basis_at_decseq: 

1048 
obtains A :: "nat \<Rightarrow> 'a set" where 

1049 
"\<And>i. open (A i)" "\<And>i. x \<in> (A i)" 

1050 
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially" 

1051 
proof atomize_elim 

1052 
from first_countable_basis[of x] obtain A :: "nat \<Rightarrow> 'a set" where 

1053 
nhds: "\<And>i. open (A i)" "\<And>i. x \<in> A i" 

1054 
and incl: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>i. A i \<subseteq> S" by auto 

1055 
def F \<equiv> "\<lambda>n. \<Inter>i\<le>n. A i" 

1056 
show "\<exists>A. (\<forall>i. open (A i)) \<and> (\<forall>i. x \<in> A i) \<and> 

1057 
(\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially)" 

1058 
proof (safe intro!: exI[of _ F]) 

1059 
fix i 

51480
3793c3a11378
move connected to HOL image; used to show intermediate value theorem
hoelzl
parents:
51479
diff
changeset

1060 
show "open (F i)" using nhds(1) by (auto simp: F_def) 
51473  1061 
show "x \<in> F i" using nhds(2) by (auto simp: F_def) 
1062 
next 

1063 
fix S assume "open S" "x \<in> S" 

1064 
from incl[OF this] obtain i where "F i \<subseteq> S" unfolding F_def by auto 

1065 
moreover have "\<And>j. i \<le> j \<Longrightarrow> F j \<subseteq> F i" 

1066 
by (auto simp: F_def) 

1067 
ultimately show "eventually (\<lambda>i. F i \<subseteq> S) sequentially" 

1068 
by (auto simp: eventually_sequentially) 

1069 
qed 

1070 
qed 

1071 

57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1072 
lemma (in first_countable_topology) nhds_countable: 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1073 
obtains X :: "nat \<Rightarrow> 'a set" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1074 
where "decseq X" "\<And>n. open (X n)" "\<And>n. x \<in> X n" "nhds x = (INF n. principal (X n))" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1075 
proof  
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1076 
from first_countable_basis obtain A :: "nat \<Rightarrow> 'a set" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1077 
where A: "\<And>n. x \<in> A n" "\<And>n. open (A n)" "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>i. A i \<subseteq> S" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1078 
by metis 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1079 
show thesis 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1080 
proof 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1081 
show "decseq (\<lambda>n. \<Inter>i\<le>n. A i)" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1082 
by (auto simp: decseq_def) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1083 
show "\<And>n. x \<in> (\<Inter>i\<le>n. A i)" "\<And>n. open (\<Inter>i\<le>n. A i)" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1084 
using A by auto 
60585  1085 
show "nhds x = (INF n. principal (\<Inter>i\<le>n. A i))" 
57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1086 
using A unfolding nhds_def 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1087 
apply (intro INF_eq) 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1088 
apply simp_all 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1089 
apply force 
60585  1090 
apply (intro exI[of _ "\<Inter>i\<le>n. A i" for n] conjI open_INT) 
57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1091 
apply auto 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1092 
done 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1093 
qed 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1094 
qed 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

1095 

51473  1096 
lemma (in first_countable_topology) countable_basis: 
1097 
obtains A :: "nat \<Rightarrow> 'a set" where 

1098 
"\<And>i. open (A i)" "\<And>i. x \<in> A i" 

1099 
"\<And>F. (\<forall>n. F n \<in> A n) \<Longrightarrow> F > x" 

1100 
proof atomize_elim 

53381  1101 
obtain A :: "nat \<Rightarrow> 'a set" where A: 
1102 
"\<And>i. open (A i)" 

1103 
"\<And>i. x \<in> A i" 

1104 
"\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially" 

1105 
by (rule countable_basis_at_decseq) blast 

1106 
{ 

1107 
fix F S assume "\<forall>n. F n \<in> A n" "open S" "x \<in> S" 

51473  1108 
with A(3)[of S] have "eventually (\<lambda>n. F n \<in> S) sequentially" 
53381  1109 
by (auto elim: eventually_elim1 simp: subset_eq) 
1110 
} 

51473  1111 
with A show "\<exists>A. (\<forall>i. open (A i)) \<and> (\<forall>i. x \<in> A i) \<and> (\<forall>F. (\<forall>n. F n \<in> A n) \<longrightarrow> F > x)" 
1112 
by (intro exI[of _ A]) (auto simp: tendsto_def) 

1113 
qed 

1114 

1115 
lemma (in first_countable_topology) sequentially_imp_eventually_nhds_within: 

1116 
assumes "\<forall>f. (\<forall>n. f n \<in> s) \<and> f > a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially" 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

1117 
shows "eventually P (inf (nhds a) (principal s))" 
51473  1118 
proof (rule ccontr) 
53381  1119 
obtain A :: "nat \<Rightarrow> 'a set" where A: 
1120 
"\<And>i. open (A i)" 

1121 
"\<And>i. a \<in> A i" 

1122 
"\<And>F. \<forall>n. F n \<in> A n \<Longrightarrow> F > a" 

1123 
by (rule countable_basis) blast 

1124 
assume "\<not> ?thesis" 

51473  1125 
with A have P: "\<exists>F. \<forall>n. F n \<in> s \<and> F n \<in> A n \<and> \<not> P (F n)" 
51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

1126 
unfolding eventually_inf_principal eventually_nhds by (intro choice) fastforce 
53381  1127 
then obtain F where F0: "\<forall>n. F n \<in> s" and F2: "\<forall>n. F n \<in> A n" and F3: "\<forall>n. \<not> P (F n)" 
1128 
by blast 

51473  1129 
with A have "F > a" by auto 
1130 
hence "eventually (\<lambda>n. P (F n)) sequentially" 

1131 
using assms F0 by simp 

1132 
thus "False" by (simp add: F3) 

1133 
qed 

1134 

1135 
lemma (in first_countable_topology) eventually_nhds_within_iff_sequentially: 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

1136 
"eventually P (inf (nhds a) (principal s)) \<longleftrightarrow> 
51473  1137 
(\<forall>f. (\<forall>n. f n \<in> s) \<and> f > a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)" 
1138 
proof (safe intro!: sequentially_imp_eventually_nhds_within) 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

1139 
assume "eventually P (inf (nhds a) (principal s))" 
51473  1140 
then obtain S where "open S" "a \<in> S" "\<forall>x\<in>S. x \<in> s \<longrightarrow> P x" 
51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

1141 
by (auto simp: eventually_inf_principal eventually_nhds) 
51473  1142 
moreover fix f assume "\<forall>n. f n \<in> s" "f > a" 
1143 
ultimately show "eventually (\<lambda>n. P (f n)) sequentially" 

1144 
by (auto dest!: topological_tendstoD elim: eventually_elim1) 

1145 
qed 

1146 

1147 
lemma (in first_countable_topology) eventually_nhds_iff_sequentially: 

1148 
"eventually P (nhds a) \<longleftrightarrow> (\<forall>f. f > a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)" 

1149 
using eventually_nhds_within_iff_sequentially[of P a UNIV] by simp 

1150 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1151 
lemma tendsto_at_iff_sequentially: 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1152 
fixes f :: "'a :: first_countable_topology \<Rightarrow> _" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1153 
shows "(f > a) (at x within s) \<longleftrightarrow> (\<forall>X. (\<forall>i. X i \<in> s  {x}) \<longrightarrow> X > x \<longrightarrow> ((f \<circ> X) > a))" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1154 
unfolding filterlim_def[of _ "nhds a"] le_filter_def eventually_filtermap at_within_def eventually_nhds_within_iff_sequentially comp_def 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1155 
by metis 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1156 

60758  1157 
subsection \<open>Function limit at a point\<close> 
51471  1158 

1159 
abbreviation 

1160 
LIM :: "('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" 

1161 
("((_)/  (_)/ > (_))" [60, 0, 60] 60) where 

1162 
"f  a > L \<equiv> (f > L) (at a)" 

1163 

51481
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

1164 
lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f > l) (at a within S) \<longleftrightarrow> (f  a > l)" 
51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

1165 
unfolding tendsto_def by (simp add: at_within_open[where S=S]) 
51481
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51480
diff
changeset

1166 

51471  1167 
lemma LIM_const_not_eq[tendsto_intros]: 
1168 
fixes a :: "'a::perfect_space" 

1169 
fixes k L :: "'b::t2_space" 

1170 
shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k)  a > L" 

1171 
by (simp add: tendsto_const_iff) 

1172 

1173 
lemmas LIM_not_zero = LIM_const_not_eq [where L = 0] 

1174 

1175 
lemma LIM_const_eq: 

1176 
fixes a :: "'a::perfect_space" 

1177 
fixes k L :: "'b::t2_space" 

1178 
shows "(\<lambda>x. k)  a > L \<Longrightarrow> k = L" 

1179 
by (simp add: tendsto_const_iff) 

1180 

1181 
lemma LIM_unique: 

1182 
fixes a :: "'a::perfect_space" and L M :: "'b::t2_space" 

1183 
shows "f  a > L \<Longrightarrow> f  a > M \<Longrightarrow> L = M" 

1184 
using at_neq_bot by (rule tendsto_unique) 

1185 

60758  1186 
text \<open>Limits are equal for functions equal except at limit point\<close> 
51471  1187 

1188 
lemma LIM_equal: "\<forall>x. x \<noteq> a > (f x = g x) \<Longrightarrow> (f  a > l) \<longleftrightarrow> (g  a > l)" 

1189 
unfolding tendsto_def eventually_at_topological by simp 

1190 

1191 
lemma LIM_cong: "a = b \<Longrightarrow> (\<And>x. x \<noteq> b \<Longrightarrow> f x = g x) \<Longrightarrow> l = m \<Longrightarrow> (f  a > l) \<longleftrightarrow> (g  b > m)" 

1192 
by (simp add: LIM_equal) 

1193 

1194 
lemma LIM_cong_limit: "f  x > L \<Longrightarrow> K = L \<Longrightarrow> f  x > K" 

1195 
by simp 

1196 

1197 
lemma tendsto_at_iff_tendsto_nhds: 

1198 
"g  l > g l \<longleftrightarrow> (g > g l) (nhds l)" 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

1199 
unfolding tendsto_def eventually_at_filter 
51471  1200 
by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1) 
1201 

1202 
lemma tendsto_compose: 

1203 
"g  l > g l \<Longrightarrow> (f > l) F \<Longrightarrow> ((\<lambda>x. g (f x)) > g l) F" 

1204 
unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g]) 

1205 

1206 
lemma LIM_o: "\<lbrakk>g  l > g l; f  a > l\<rbrakk> \<Longrightarrow> (g \<circ> f)  a > g l" 

1207 
unfolding o_def by (rule tendsto_compose) 

1208 

1209 
lemma tendsto_compose_eventually: 

1210 
"g  l > m \<Longrightarrow> (f > l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) > m) F" 

1211 
by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at) 

1212 

1213 
lemma LIM_compose_eventually: 

1214 
assumes f: "f  a > b" 

1215 
assumes g: "g  b > c" 

1216 
assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)" 

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

1218 
using g f inj by (rule tendsto_compose_eventually) 

1219 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1220 
lemma tendsto_compose_filtermap: "((g \<circ> f) > T) F \<longleftrightarrow> (g > T) (filtermap f F)" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1221 
by (simp add: filterlim_def filtermap_filtermap comp_def) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1222 

60758  1223 
subsubsection \<open>Relation of LIM and LIMSEQ\<close> 
51473  1224 

1225 
lemma (in first_countable_topology) sequentially_imp_eventually_within: 

1226 
"(\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f > a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially) \<Longrightarrow> 

1227 
eventually P (at a within s)" 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51518
diff
changeset

1228 
unfolding at_within_def 
51473  1229 
by (intro sequentially_imp_eventually_nhds_within) auto 
1230 

1231 
lemma (in first_countable_topology) sequentially_imp_eventually_at: 

1232 
"(\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f > a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially) \<Longrightarrow> eventually P (at a)" 

1233 
using assms sequentially_imp_eventually_within [where s=UNIV] by simp 

1234 

1235 
lemma LIMSEQ_SEQ_conv1: 

1236 
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" 

1237 
assumes f: "f  a > l" 

1238 
shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. f (S n)) > l" 

1239 
using tendsto_compose_eventually [OF f, where F=sequentially] by simp 

1240 

1241 
lemma LIMSEQ_SEQ_conv2: 

1242 
fixes f :: "'a::first_countable_topology \<Rightarrow> 'b::topological_space" 

1243 
assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. f (S n)) > l" 

1244 
shows "f  a > l" 

1245 
using assms unfolding tendsto_def [where l=l] by (simp add: sequentially_imp_eventually_at) 

1246 

1247 
lemma LIMSEQ_SEQ_conv: 

1248 
"(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > (a::'a::first_countable_topology) \<longrightarrow> (\<lambda>n. X (S n)) > L) = 

1249 
(X  a > (L::'b::topological_space))" 

1250 
using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 .. 

1251 

57025  1252 
lemma sequentially_imp_eventually_at_left: 
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60150
diff
changeset

1253 
fixes a :: "'a :: {linorder_topology, first_countable_topology}" 
57025  1254 
assumes b[simp]: "b < a" 
1255 
assumes *: "\<And>f. (\<And>n. b < f n) \<Longrightarrow> (\<And>n. f n < a) \<Longrightarrow> incseq f \<Longrightarrow> f > a \<Longrightarrow> eventually (\<lambda>n. P (f n)) sequentially" 

1256 
shows "eventually P (at_left a)" 

1257 
proof (safe intro!: sequentially_imp_eventually_within) 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1258 
fix X assume X: "\<forall>n. X n \<in> {..< a} \<and> X n \<noteq> a" "X > a" 
57025  1259 
show "eventually (\<lambda>n. P (X n)) sequentially" 
1260 
proof (rule ccontr) 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1261 
assume neg: "\<not> eventually (\<lambda>n. P (X n)) sequentially" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1262 
have "\<exists>s. \<forall>n. (\<not> P (X (s n)) \<and> b < X (s n)) \<and> (X (s n) \<le> X (s (Suc n)) \<and> Suc (s n) \<le> s (Suc n))" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1263 
proof (rule dependent_nat_choice) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1264 
have "\<not> eventually (\<lambda>n. b < X n \<longrightarrow> P (X n)) sequentially" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1265 
by (intro not_eventually_impI neg order_tendstoD(1) [OF X(2) b]) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1266 
then show "\<exists>x. \<not> P (X x) \<and> b < X x" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1267 
by (auto dest!: not_eventuallyD) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1268 
next 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1269 
fix x n 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1270 
have "\<not> eventually (\<lambda>n. Suc x \<le> n \<longrightarrow> b < X n \<longrightarrow> X x < X n \<longrightarrow> P (X n)) sequentially" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1271 
using X by (intro not_eventually_impI order_tendstoD(1)[OF X(2)] eventually_ge_at_top neg) auto 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1272 
then show "\<exists>n. (\<not> P (X n) \<and> b < X n) \<and> (X x \<le> X n \<and> Suc x \<le> n)" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1273 
by (auto dest!: not_eventuallyD) 
57025  1274 
qed 
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1275 
then guess s .. 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1276 
then have "\<And>n. b < X (s n)" "\<And>n. X (s n) < a" "incseq (\<lambda>n. X (s n))" "(\<lambda>n. X (s n)) > a" "\<And>n. \<not> P (X (s n))" 
60758  1277 
using X by (auto simp: subseq_Suc_iff Suc_le_eq incseq_Suc_iff intro!: LIMSEQ_subseq_LIMSEQ[OF \<open>X > a\<close>, unfolded comp_def]) 
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1278 
from *[OF this(1,2,3,4)] this(5) show False by auto 
57025  1279 
qed 
1280 
qed 

1281 

1282 
lemma tendsto_at_left_sequentially: 

60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60150
diff
changeset

1283 
fixes a :: "_ :: {linorder_topology, first_countable_topology}" 
57025  1284 
assumes "b < a" 
1285 
assumes *: "\<And>S. (\<And>n. S n < a) \<Longrightarrow> (\<And>n. b < S n) \<Longrightarrow> incseq S \<Longrightarrow> S > a \<Longrightarrow> (\<lambda>n. X (S n)) > L" 

1286 
shows "(X > L) (at_left a)" 

1287 
using assms unfolding tendsto_def [where l=L] 

1288 
by (simp add: sequentially_imp_eventually_at_left) 

1289 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1290 
lemma sequentially_imp_eventually_at_right: 
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60150
diff
changeset

1291 
fixes a :: "'a :: {linorder_topology, first_countable_topology}" 
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1292 
assumes b[simp]: "a < b" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1293 
assumes *: "\<And>f. (\<And>n. a < f n) \<Longrightarrow> (\<And>n. f n < b) \<Longrightarrow> decseq f \<Longrightarrow> f > a \<Longrightarrow> eventually (\<lambda>n. P (f n)) sequentially" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1294 
shows "eventually P (at_right a)" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1295 
proof (safe intro!: sequentially_imp_eventually_within) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1296 
fix X assume X: "\<forall>n. X n \<in> {a <..} \<and> X n \<noteq> a" "X > a" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1297 
show "eventually (\<lambda>n. P (X n)) sequentially" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1298 
proof (rule ccontr) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1299 
assume neg: "\<not> eventually (\<lambda>n. P (X n)) sequentially" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1300 
have "\<exists>s. \<forall>n. (\<not> P (X (s n)) \<and> X (s n) < b) \<and> (X (s (Suc n)) \<le> X (s n) \<and> Suc (s n) \<le> s (Suc n))" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1301 
proof (rule dependent_nat_choice) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1302 
have "\<not> eventually (\<lambda>n. X n < b \<longrightarrow> P (X n)) sequentially" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57276
diff
changeset

1303 
by (intro not_eventually_impI neg order_tendstoD(2) [OF X(2) b]) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval 