author | paulson <lp15@cam.ac.uk> |
Mon, 04 Apr 2016 16:52:56 +0100 | |
changeset 62843 | 313d3b697c9a |
parent 62375 | 670063003ad3 |
permissions | -rw-r--r-- |
41983 | 1 |
(* Title: HOL/Multivariate_Analysis/Extended_Real_Limits.thy |
2 |
Author: Johannes Hölzl, TU München |
|
3 |
Author: Robert Himmelmann, TU München |
|
4 |
Author: Armin Heller, TU München |
|
5 |
Author: Bogdan Grechuk, University of Edinburgh |
|
6 |
*) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
7 |
|
60420 | 8 |
section \<open>Limits on the Extended real number line\<close> |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
9 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
10 |
theory Extended_Real_Limits |
61560 | 11 |
imports |
12 |
Topology_Euclidean_Space |
|
13 |
"~~/src/HOL/Library/Extended_Real" |
|
62375 | 14 |
"~~/src/HOL/Library/Extended_Nonnegative_Real" |
61560 | 15 |
"~~/src/HOL/Library/Indicator_Function" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
16 |
begin |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
17 |
|
53788 | 18 |
lemma compact_UNIV: |
19 |
"compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)" |
|
51351 | 20 |
using compact_complete_linorder |
21 |
by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def) |
|
22 |
||
23 |
lemma compact_eq_closed: |
|
53788 | 24 |
fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" |
51351 | 25 |
shows "compact S \<longleftrightarrow> closed S" |
62843
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62375
diff
changeset
|
26 |
using closed_Int_compact[of S, OF _ compact_UNIV] compact_imp_closed |
53788 | 27 |
by auto |
51351 | 28 |
|
29 |
lemma closed_contains_Sup_cl: |
|
53788 | 30 |
fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" |
31 |
assumes "closed S" |
|
32 |
and "S \<noteq> {}" |
|
33 |
shows "Sup S \<in> S" |
|
51351 | 34 |
proof - |
35 |
from compact_eq_closed[of S] compact_attains_sup[of S] assms |
|
53788 | 36 |
obtain s where S: "s \<in> S" "\<forall>t\<in>S. t \<le> s" |
37 |
by auto |
|
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
51641
diff
changeset
|
38 |
then have "Sup S = s" |
51351 | 39 |
by (auto intro!: Sup_eqI) |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
51641
diff
changeset
|
40 |
with S show ?thesis |
51351 | 41 |
by simp |
42 |
qed |
|
43 |
||
44 |
lemma closed_contains_Inf_cl: |
|
53788 | 45 |
fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" |
46 |
assumes "closed S" |
|
47 |
and "S \<noteq> {}" |
|
48 |
shows "Inf S \<in> S" |
|
51351 | 49 |
proof - |
50 |
from compact_eq_closed[of S] compact_attains_inf[of S] assms |
|
53788 | 51 |
obtain s where S: "s \<in> S" "\<forall>t\<in>S. s \<le> t" |
52 |
by auto |
|
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
51641
diff
changeset
|
53 |
then have "Inf S = s" |
51351 | 54 |
by (auto intro!: Inf_eqI) |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
51641
diff
changeset
|
55 |
with S show ?thesis |
51351 | 56 |
by simp |
57 |
qed |
|
58 |
||
59 |
instance ereal :: second_countable_topology |
|
61169 | 60 |
proof (standard, intro exI conjI) |
51351 | 61 |
let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)" |
53788 | 62 |
show "countable ?B" |
63 |
by (auto intro: countable_rat) |
|
51351 | 64 |
show "open = generate_topology ?B" |
65 |
proof (intro ext iffI) |
|
53788 | 66 |
fix S :: "ereal set" |
67 |
assume "open S" |
|
51351 | 68 |
then show "generate_topology ?B S" |
69 |
unfolding open_generated_order |
|
70 |
proof induct |
|
71 |
case (Basis b) |
|
53788 | 72 |
then obtain e where "b = {..<e} \<or> b = {e<..}" |
73 |
by auto |
|
51351 | 74 |
moreover have "{..<e} = \<Union>{{..<x}|x. x \<in> \<rat> \<and> x < e}" "{e<..} = \<Union>{{x<..}|x. x \<in> \<rat> \<and> e < x}" |
75 |
by (auto dest: ereal_dense3 |
|
76 |
simp del: ex_simps |
|
77 |
simp add: ex_simps[symmetric] conj_commute Rats_def image_iff) |
|
78 |
ultimately show ?case |
|
79 |
by (auto intro: generate_topology.intros) |
|
80 |
qed (auto intro: generate_topology.intros) |
|
81 |
next |
|
53788 | 82 |
fix S |
83 |
assume "generate_topology ?B S" |
|
84 |
then show "open S" |
|
85 |
by induct auto |
|
51351 | 86 |
qed |
87 |
qed |
|
88 |
||
62375 | 89 |
text \<open>This is a copy from \<open>ereal :: second_countable_topology\<close>. Maybe find a common super class of |
90 |
topological spaces where the rational numbers are densely embedded ?\<close> |
|
91 |
instance ennreal :: second_countable_topology |
|
92 |
proof (standard, intro exI conjI) |
|
93 |
let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ennreal set set)" |
|
94 |
show "countable ?B" |
|
95 |
by (auto intro: countable_rat) |
|
96 |
show "open = generate_topology ?B" |
|
97 |
proof (intro ext iffI) |
|
98 |
fix S :: "ennreal set" |
|
99 |
assume "open S" |
|
100 |
then show "generate_topology ?B S" |
|
101 |
unfolding open_generated_order |
|
102 |
proof induct |
|
103 |
case (Basis b) |
|
104 |
then obtain e where "b = {..<e} \<or> b = {e<..}" |
|
105 |
by auto |
|
106 |
moreover have "{..<e} = \<Union>{{..<x}|x. x \<in> \<rat> \<and> x < e}" "{e<..} = \<Union>{{x<..}|x. x \<in> \<rat> \<and> e < x}" |
|
107 |
by (auto dest: ennreal_rat_dense |
|
108 |
simp del: ex_simps |
|
109 |
simp add: ex_simps[symmetric] conj_commute Rats_def image_iff) |
|
110 |
ultimately show ?case |
|
111 |
by (auto intro: generate_topology.intros) |
|
112 |
qed (auto intro: generate_topology.intros) |
|
113 |
next |
|
114 |
fix S |
|
115 |
assume "generate_topology ?B S" |
|
116 |
then show "open S" |
|
117 |
by induct auto |
|
118 |
qed |
|
119 |
qed |
|
120 |
||
43920 | 121 |
lemma ereal_open_closed_aux: |
122 |
fixes S :: "ereal set" |
|
53788 | 123 |
assumes "open S" |
124 |
and "closed S" |
|
125 |
and S: "(-\<infinity>) \<notin> S" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
126 |
shows "S = {}" |
49664 | 127 |
proof (rule ccontr) |
53788 | 128 |
assume "\<not> ?thesis" |
129 |
then have *: "Inf S \<in> S" |
|
62375 | 130 |
|
53788 | 131 |
by (metis assms(2) closed_contains_Inf_cl) |
132 |
{ |
|
133 |
assume "Inf S = -\<infinity>" |
|
134 |
then have False |
|
135 |
using * assms(3) by auto |
|
136 |
} |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
137 |
moreover |
53788 | 138 |
{ |
139 |
assume "Inf S = \<infinity>" |
|
140 |
then have "S = {\<infinity>}" |
|
60420 | 141 |
by (metis Inf_eq_PInfty \<open>S \<noteq> {}\<close>) |
53788 | 142 |
then have False |
143 |
by (metis assms(1) not_open_singleton) |
|
144 |
} |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
145 |
moreover |
53788 | 146 |
{ |
147 |
assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" |
|
148 |
from ereal_open_cont_interval[OF assms(1) * fin] |
|
149 |
obtain e where e: "e > 0" "{Inf S - e<..<Inf S + e} \<subseteq> S" . |
|
150 |
then obtain b where b: "Inf S - e < b" "b < Inf S" |
|
151 |
using fin ereal_between[of "Inf S" e] dense[of "Inf S - e"] |
|
44918 | 152 |
by auto |
53788 | 153 |
then have "b: {Inf S - e <..< Inf S + e}" |
154 |
using e fin ereal_between[of "Inf S" e] |
|
155 |
by auto |
|
156 |
then have "b \<in> S" |
|
157 |
using e by auto |
|
158 |
then have False |
|
159 |
using b by (metis complete_lattice_class.Inf_lower leD) |
|
160 |
} |
|
161 |
ultimately show False |
|
162 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
163 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
164 |
|
43920 | 165 |
lemma ereal_open_closed: |
166 |
fixes S :: "ereal set" |
|
53788 | 167 |
shows "open S \<and> closed S \<longleftrightarrow> S = {} \<or> S = UNIV" |
49664 | 168 |
proof - |
53788 | 169 |
{ |
170 |
assume lhs: "open S \<and> closed S" |
|
171 |
{ |
|
172 |
assume "-\<infinity> \<notin> S" |
|
173 |
then have "S = {}" |
|
174 |
using lhs ereal_open_closed_aux by auto |
|
175 |
} |
|
49664 | 176 |
moreover |
53788 | 177 |
{ |
178 |
assume "-\<infinity> \<in> S" |
|
179 |
then have "- S = {}" |
|
180 |
using lhs ereal_open_closed_aux[of "-S"] by auto |
|
181 |
} |
|
182 |
ultimately have "S = {} \<or> S = UNIV" |
|
183 |
by auto |
|
184 |
} |
|
185 |
then show ?thesis |
|
186 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
187 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
188 |
|
53788 | 189 |
lemma ereal_open_atLeast: |
190 |
fixes x :: ereal |
|
191 |
shows "open {x..} \<longleftrightarrow> x = -\<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
192 |
proof |
53788 | 193 |
assume "x = -\<infinity>" |
194 |
then have "{x..} = UNIV" |
|
195 |
by auto |
|
196 |
then show "open {x..}" |
|
197 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
198 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
199 |
assume "open {x..}" |
53788 | 200 |
then have "open {x..} \<and> closed {x..}" |
201 |
by auto |
|
202 |
then have "{x..} = UNIV" |
|
203 |
unfolding ereal_open_closed by auto |
|
204 |
then show "x = -\<infinity>" |
|
205 |
by (simp add: bot_ereal_def atLeast_eq_UNIV_iff) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
206 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
207 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
208 |
lemma mono_closed_real: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
209 |
fixes S :: "real set" |
53788 | 210 |
assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S" |
49664 | 211 |
and "closed S" |
53788 | 212 |
shows "S = {} \<or> S = UNIV \<or> (\<exists>a. S = {a..})" |
49664 | 213 |
proof - |
53788 | 214 |
{ |
215 |
assume "S \<noteq> {}" |
|
216 |
{ assume ex: "\<exists>B. \<forall>x\<in>S. B \<le> x" |
|
217 |
then have *: "\<forall>x\<in>S. Inf S \<le> x" |
|
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset
|
218 |
using cInf_lower[of _ S] ex by (metis bdd_below_def) |
53788 | 219 |
then have "Inf S \<in> S" |
220 |
apply (subst closed_contains_Inf) |
|
60420 | 221 |
using ex \<open>S \<noteq> {}\<close> \<open>closed S\<close> |
53788 | 222 |
apply auto |
223 |
done |
|
224 |
then have "\<forall>x. Inf S \<le> x \<longleftrightarrow> x \<in> S" |
|
225 |
using mono[rule_format, of "Inf S"] * |
|
226 |
by auto |
|
227 |
then have "S = {Inf S ..}" |
|
228 |
by auto |
|
229 |
then have "\<exists>a. S = {a ..}" |
|
230 |
by auto |
|
49664 | 231 |
} |
232 |
moreover |
|
53788 | 233 |
{ |
234 |
assume "\<not> (\<exists>B. \<forall>x\<in>S. B \<le> x)" |
|
235 |
then have nex: "\<forall>B. \<exists>x\<in>S. x < B" |
|
236 |
by (simp add: not_le) |
|
237 |
{ |
|
238 |
fix y |
|
239 |
obtain x where "x\<in>S" and "x < y" |
|
240 |
using nex by auto |
|
241 |
then have "y \<in> S" |
|
242 |
using mono[rule_format, of x y] by auto |
|
243 |
} |
|
244 |
then have "S = UNIV" |
|
245 |
by auto |
|
49664 | 246 |
} |
53788 | 247 |
ultimately have "S = UNIV \<or> (\<exists>a. S = {a ..})" |
248 |
by blast |
|
249 |
} |
|
250 |
then show ?thesis |
|
251 |
by blast |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
252 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
253 |
|
43920 | 254 |
lemma mono_closed_ereal: |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
255 |
fixes S :: "real set" |
53788 | 256 |
assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S" |
49664 | 257 |
and "closed S" |
53788 | 258 |
shows "\<exists>a. S = {x. a \<le> ereal x}" |
49664 | 259 |
proof - |
53788 | 260 |
{ |
261 |
assume "S = {}" |
|
262 |
then have ?thesis |
|
263 |
apply (rule_tac x=PInfty in exI) |
|
264 |
apply auto |
|
265 |
done |
|
266 |
} |
|
49664 | 267 |
moreover |
53788 | 268 |
{ |
269 |
assume "S = UNIV" |
|
270 |
then have ?thesis |
|
271 |
apply (rule_tac x="-\<infinity>" in exI) |
|
272 |
apply auto |
|
273 |
done |
|
274 |
} |
|
49664 | 275 |
moreover |
53788 | 276 |
{ |
277 |
assume "\<exists>a. S = {a ..}" |
|
278 |
then obtain a where "S = {a ..}" |
|
279 |
by auto |
|
280 |
then have ?thesis |
|
281 |
apply (rule_tac x="ereal a" in exI) |
|
282 |
apply auto |
|
283 |
done |
|
49664 | 284 |
} |
53788 | 285 |
ultimately show ?thesis |
286 |
using mono_closed_real[of S] assms by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
287 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
288 |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
289 |
lemma Liminf_within: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
290 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
291 |
shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)" |
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51530
diff
changeset
|
292 |
unfolding Liminf_def eventually_at |
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56166
diff
changeset
|
293 |
proof (rule SUP_eq, simp_all add: Ball_def Bex_def, safe) |
53788 | 294 |
fix P d |
295 |
assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y" |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
296 |
then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
297 |
by (auto simp: zero_less_dist_iff dist_commute) |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
298 |
then show "\<exists>r>0. INFIMUM (Collect P) f \<le> INFIMUM (S \<inter> ball x r - {x}) f" |
60420 | 299 |
by (intro exI[of _ d] INF_mono conjI \<open>0 < d\<close>) auto |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
300 |
next |
53788 | 301 |
fix d :: real |
302 |
assume "0 < d" |
|
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51530
diff
changeset
|
303 |
then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and> |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
304 |
INFIMUM (S \<inter> ball x d - {x}) f \<le> INFIMUM (Collect P) f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
305 |
by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"]) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
306 |
(auto intro!: INF_mono exI[of _ d] simp: dist_commute) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
307 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
308 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
309 |
lemma Limsup_within: |
53788 | 310 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
311 |
shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)" |
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51530
diff
changeset
|
312 |
unfolding Limsup_def eventually_at |
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56166
diff
changeset
|
313 |
proof (rule INF_eq, simp_all add: Ball_def Bex_def, safe) |
53788 | 314 |
fix P d |
315 |
assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y" |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
316 |
then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
317 |
by (auto simp: zero_less_dist_iff dist_commute) |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
318 |
then show "\<exists>r>0. SUPREMUM (S \<inter> ball x r - {x}) f \<le> SUPREMUM (Collect P) f" |
60420 | 319 |
by (intro exI[of _ d] SUP_mono conjI \<open>0 < d\<close>) auto |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
320 |
next |
53788 | 321 |
fix d :: real |
322 |
assume "0 < d" |
|
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51530
diff
changeset
|
323 |
then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and> |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
324 |
SUPREMUM (Collect P) f \<le> SUPREMUM (S \<inter> ball x d - {x}) f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
325 |
by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"]) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
326 |
(auto intro!: SUP_mono exI[of _ d] simp: dist_commute) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
327 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
328 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
329 |
lemma Liminf_at: |
54257
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53788
diff
changeset
|
330 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
331 |
shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
332 |
using Liminf_within[of x UNIV f] by simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
333 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
334 |
lemma Limsup_at: |
54257
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53788
diff
changeset
|
335 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
336 |
shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
337 |
using Limsup_within[of x UNIV f] by simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
338 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
339 |
lemma min_Liminf_at: |
53788 | 340 |
fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_linorder" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
341 |
shows "min (f x) (Liminf (at x) f) = (SUP e:{0<..}. INF y:ball x e. f y)" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
342 |
unfolding inf_min[symmetric] Liminf_at |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
343 |
apply (subst inf_commute) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
344 |
apply (subst SUP_inf) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
345 |
apply (intro SUP_cong[OF refl]) |
54260
6a967667fd45
use INF and SUP on conditionally complete lattices in multivariate analysis
hoelzl
parents:
54258
diff
changeset
|
346 |
apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union) |
56166 | 347 |
apply (drule sym) |
348 |
apply auto |
|
57865 | 349 |
apply (metis INF_absorb centre_in_ball) |
350 |
done |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
351 |
|
60420 | 352 |
subsection \<open>monoset\<close> |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
353 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
354 |
definition (in order) mono_set: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
355 |
"mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
356 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
357 |
lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
358 |
lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
359 |
lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
360 |
lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
361 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
362 |
lemma (in complete_linorder) mono_set_iff: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
363 |
fixes S :: "'a set" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
364 |
defines "a \<equiv> Inf S" |
53788 | 365 |
shows "mono_set S \<longleftrightarrow> S = {a <..} \<or> S = {a..}" (is "_ = ?c") |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
366 |
proof |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
367 |
assume "mono_set S" |
53788 | 368 |
then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" |
369 |
by (auto simp: mono_set) |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
370 |
show ?c |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
371 |
proof cases |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
372 |
assume "a \<in> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
373 |
show ?c |
60420 | 374 |
using mono[OF _ \<open>a \<in> S\<close>] |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
375 |
by (auto intro: Inf_lower simp: a_def) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
376 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
377 |
assume "a \<notin> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
378 |
have "S = {a <..}" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
379 |
proof safe |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
380 |
fix x assume "x \<in> S" |
53788 | 381 |
then have "a \<le> x" |
382 |
unfolding a_def by (rule Inf_lower) |
|
383 |
then show "a < x" |
|
60420 | 384 |
using \<open>x \<in> S\<close> \<open>a \<notin> S\<close> by (cases "a = x") auto |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
385 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
386 |
fix x assume "a < x" |
53788 | 387 |
then obtain y where "y < x" "y \<in> S" |
388 |
unfolding a_def Inf_less_iff .. |
|
389 |
with mono[of y x] show "x \<in> S" |
|
390 |
by auto |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
391 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
392 |
then show ?c .. |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
393 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
394 |
qed auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
395 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
396 |
lemma ereal_open_mono_set: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
397 |
fixes S :: "ereal set" |
53788 | 398 |
shows "open S \<and> mono_set S \<longleftrightarrow> S = UNIV \<or> S = {Inf S <..}" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
399 |
by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
400 |
ereal_open_closed mono_set_iff open_ereal_greaterThan) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
401 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
402 |
lemma ereal_closed_mono_set: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
403 |
fixes S :: "ereal set" |
53788 | 404 |
shows "closed S \<and> mono_set S \<longleftrightarrow> S = {} \<or> S = {Inf S ..}" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
405 |
by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
406 |
ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
407 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
408 |
lemma ereal_Liminf_Sup_monoset: |
53788 | 409 |
fixes f :: "'a \<Rightarrow> ereal" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
410 |
shows "Liminf net f = |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
411 |
Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
412 |
(is "_ = Sup ?A") |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
413 |
proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least) |
53788 | 414 |
fix P |
415 |
assume P: "eventually P net" |
|
416 |
fix S |
|
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
417 |
assume S: "mono_set S" "INFIMUM (Collect P) f \<in> S" |
53788 | 418 |
{ |
419 |
fix x |
|
420 |
assume "P x" |
|
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
421 |
then have "INFIMUM (Collect P) f \<le> f x" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
422 |
by (intro complete_lattice_class.INF_lower) simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
423 |
with S have "f x \<in> S" |
53788 | 424 |
by (simp add: mono_set) |
425 |
} |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
426 |
with P show "eventually (\<lambda>x. f x \<in> S) net" |
61810 | 427 |
by (auto elim: eventually_mono) |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
428 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
429 |
fix y l |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
430 |
assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net" |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
431 |
assume P: "\<forall>P. eventually P net \<longrightarrow> INFIMUM (Collect P) f \<le> y" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
432 |
show "l \<le> y" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
433 |
proof (rule dense_le) |
53788 | 434 |
fix B |
435 |
assume "B < l" |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
436 |
then have "eventually (\<lambda>x. f x \<in> {B <..}) net" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
437 |
by (intro S[rule_format]) auto |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
438 |
then have "INFIMUM {x. B < f x} f \<le> y" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
439 |
using P by auto |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
440 |
moreover have "B \<le> INFIMUM {x. B < f x} f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
441 |
by (intro INF_greatest) auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
442 |
ultimately show "B \<le> y" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
443 |
by simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
444 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
445 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
446 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
447 |
lemma ereal_Limsup_Inf_monoset: |
53788 | 448 |
fixes f :: "'a \<Rightarrow> ereal" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
449 |
shows "Limsup net f = |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
450 |
Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
451 |
(is "_ = Inf ?A") |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
452 |
proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest) |
53788 | 453 |
fix P |
454 |
assume P: "eventually P net" |
|
455 |
fix S |
|
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
456 |
assume S: "mono_set (uminus`S)" "SUPREMUM (Collect P) f \<in> S" |
53788 | 457 |
{ |
458 |
fix x |
|
459 |
assume "P x" |
|
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
460 |
then have "f x \<le> SUPREMUM (Collect P) f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
461 |
by (intro complete_lattice_class.SUP_upper) simp |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
462 |
with S(1)[unfolded mono_set, rule_format, of "- SUPREMUM (Collect P) f" "- f x"] S(2) |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
463 |
have "f x \<in> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
464 |
by (simp add: inj_image_mem_iff) } |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
465 |
with P show "eventually (\<lambda>x. f x \<in> S) net" |
61810 | 466 |
by (auto elim: eventually_mono) |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
467 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
468 |
fix y l |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
469 |
assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net" |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
470 |
assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPREMUM (Collect P) f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
471 |
show "y \<le> l" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
472 |
proof (rule dense_ge) |
53788 | 473 |
fix B |
474 |
assume "l < B" |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
475 |
then have "eventually (\<lambda>x. f x \<in> {..< B}) net" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
476 |
by (intro S[rule_format]) auto |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
477 |
then have "y \<le> SUPREMUM {x. f x < B} f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
478 |
using P by auto |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
479 |
moreover have "SUPREMUM {x. f x < B} f \<le> B" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
480 |
by (intro SUP_least) auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
481 |
ultimately show "y \<le> B" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
482 |
by simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
483 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
484 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
485 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
486 |
lemma liminf_bounded_open: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
487 |
fixes x :: "nat \<Rightarrow> ereal" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
488 |
shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
489 |
(is "_ \<longleftrightarrow> ?P x0") |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
490 |
proof |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
491 |
assume "?P x0" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
492 |
then show "x0 \<le> liminf x" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
493 |
unfolding ereal_Liminf_Sup_monoset eventually_sequentially |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
494 |
by (intro complete_lattice_class.Sup_upper) auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
495 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
496 |
assume "x0 \<le> liminf x" |
53788 | 497 |
{ |
498 |
fix S :: "ereal set" |
|
499 |
assume om: "open S" "mono_set S" "x0 \<in> S" |
|
500 |
{ |
|
501 |
assume "S = UNIV" |
|
502 |
then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S" |
|
503 |
by auto |
|
504 |
} |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
505 |
moreover |
53788 | 506 |
{ |
507 |
assume "S \<noteq> UNIV" |
|
508 |
then obtain B where B: "S = {B<..}" |
|
509 |
using om ereal_open_mono_set by auto |
|
510 |
then have "B < x0" |
|
511 |
using om by auto |
|
512 |
then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S" |
|
513 |
unfolding B |
|
60420 | 514 |
using \<open>x0 \<le> liminf x\<close> liminf_bounded_iff |
53788 | 515 |
by auto |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
516 |
} |
53788 | 517 |
ultimately have "\<exists>N. \<forall>n\<ge>N. x n \<in> S" |
518 |
by auto |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
519 |
} |
53788 | 520 |
then show "?P x0" |
521 |
by auto |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
522 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
523 |
|
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
524 |
subsection "Relate extended reals and the indicator function" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
525 |
|
59000 | 526 |
lemma ereal_indicator_le_0: "(indicator S x::ereal) \<le> 0 \<longleftrightarrow> x \<notin> S" |
527 |
by (auto split: split_indicator simp: one_ereal_def) |
|
528 |
||
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
529 |
lemma ereal_indicator: "ereal (indicator A x) = indicator A x" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
530 |
by (auto simp: indicator_def one_ereal_def) |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
531 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
532 |
lemma ereal_mult_indicator: "ereal (x * indicator A y) = ereal x * indicator A y" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
533 |
by (simp split: split_indicator) |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
534 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
535 |
lemma ereal_indicator_mult: "ereal (indicator A y * x) = indicator A y * ereal x" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
536 |
by (simp split: split_indicator) |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
537 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
538 |
lemma ereal_indicator_nonneg[simp, intro]: "0 \<le> (indicator A x ::ereal)" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
539 |
unfolding indicator_def by auto |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
540 |
|
59425 | 541 |
lemma indicator_inter_arith_ereal: "indicator A x * indicator B x = (indicator (A \<inter> B) x :: ereal)" |
542 |
by (simp split: split_indicator) |
|
543 |
||
44125 | 544 |
end |