author | hoelzl |
Thu, 20 Oct 2016 18:41:59 +0200 | |
changeset 64320 | ba194424b895 |
parent 63627 | 6ddb43c6b711 |
child 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
63627 | 1 |
(* Title: HOL/Analysis/Extended_Real_Limits.thy |
41983 | 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 |
||
64320
ba194424b895
HOL-Probability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63627
diff
changeset
|
59 |
instance enat :: second_countable_topology |
ba194424b895
HOL-Probability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63627
diff
changeset
|
60 |
proof |
ba194424b895
HOL-Probability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63627
diff
changeset
|
61 |
show "\<exists>B::enat set set. countable B \<and> open = generate_topology B" |
ba194424b895
HOL-Probability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63627
diff
changeset
|
62 |
proof (intro exI conjI) |
ba194424b895
HOL-Probability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63627
diff
changeset
|
63 |
show "countable (range lessThan \<union> range greaterThan::enat set set)" |
ba194424b895
HOL-Probability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63627
diff
changeset
|
64 |
by auto |
ba194424b895
HOL-Probability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63627
diff
changeset
|
65 |
qed (simp add: open_enat_def) |
ba194424b895
HOL-Probability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63627
diff
changeset
|
66 |
qed |
ba194424b895
HOL-Probability: move stopping time from AFP/Markov_Models
hoelzl
parents:
63627
diff
changeset
|
67 |
|
51351 | 68 |
instance ereal :: second_countable_topology |
61169 | 69 |
proof (standard, intro exI conjI) |
51351 | 70 |
let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)" |
53788 | 71 |
show "countable ?B" |
72 |
by (auto intro: countable_rat) |
|
51351 | 73 |
show "open = generate_topology ?B" |
74 |
proof (intro ext iffI) |
|
53788 | 75 |
fix S :: "ereal set" |
76 |
assume "open S" |
|
51351 | 77 |
then show "generate_topology ?B S" |
78 |
unfolding open_generated_order |
|
79 |
proof induct |
|
80 |
case (Basis b) |
|
53788 | 81 |
then obtain e where "b = {..<e} \<or> b = {e<..}" |
82 |
by auto |
|
51351 | 83 |
moreover have "{..<e} = \<Union>{{..<x}|x. x \<in> \<rat> \<and> x < e}" "{e<..} = \<Union>{{x<..}|x. x \<in> \<rat> \<and> e < x}" |
84 |
by (auto dest: ereal_dense3 |
|
85 |
simp del: ex_simps |
|
86 |
simp add: ex_simps[symmetric] conj_commute Rats_def image_iff) |
|
87 |
ultimately show ?case |
|
88 |
by (auto intro: generate_topology.intros) |
|
89 |
qed (auto intro: generate_topology.intros) |
|
90 |
next |
|
53788 | 91 |
fix S |
92 |
assume "generate_topology ?B S" |
|
93 |
then show "open S" |
|
94 |
by induct auto |
|
51351 | 95 |
qed |
96 |
qed |
|
97 |
||
62375 | 98 |
text \<open>This is a copy from \<open>ereal :: second_countable_topology\<close>. Maybe find a common super class of |
99 |
topological spaces where the rational numbers are densely embedded ?\<close> |
|
100 |
instance ennreal :: second_countable_topology |
|
101 |
proof (standard, intro exI conjI) |
|
102 |
let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ennreal set set)" |
|
103 |
show "countable ?B" |
|
104 |
by (auto intro: countable_rat) |
|
105 |
show "open = generate_topology ?B" |
|
106 |
proof (intro ext iffI) |
|
107 |
fix S :: "ennreal set" |
|
108 |
assume "open S" |
|
109 |
then show "generate_topology ?B S" |
|
110 |
unfolding open_generated_order |
|
111 |
proof induct |
|
112 |
case (Basis b) |
|
113 |
then obtain e where "b = {..<e} \<or> b = {e<..}" |
|
114 |
by auto |
|
115 |
moreover have "{..<e} = \<Union>{{..<x}|x. x \<in> \<rat> \<and> x < e}" "{e<..} = \<Union>{{x<..}|x. x \<in> \<rat> \<and> e < x}" |
|
116 |
by (auto dest: ennreal_rat_dense |
|
117 |
simp del: ex_simps |
|
118 |
simp add: ex_simps[symmetric] conj_commute Rats_def image_iff) |
|
119 |
ultimately show ?case |
|
120 |
by (auto intro: generate_topology.intros) |
|
121 |
qed (auto intro: generate_topology.intros) |
|
122 |
next |
|
123 |
fix S |
|
124 |
assume "generate_topology ?B S" |
|
125 |
then show "open S" |
|
126 |
by induct auto |
|
127 |
qed |
|
128 |
qed |
|
129 |
||
43920 | 130 |
lemma ereal_open_closed_aux: |
131 |
fixes S :: "ereal set" |
|
53788 | 132 |
assumes "open S" |
133 |
and "closed S" |
|
134 |
and S: "(-\<infinity>) \<notin> S" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
135 |
shows "S = {}" |
49664 | 136 |
proof (rule ccontr) |
53788 | 137 |
assume "\<not> ?thesis" |
138 |
then have *: "Inf S \<in> S" |
|
62375 | 139 |
|
53788 | 140 |
by (metis assms(2) closed_contains_Inf_cl) |
141 |
{ |
|
142 |
assume "Inf S = -\<infinity>" |
|
143 |
then have False |
|
144 |
using * assms(3) by auto |
|
145 |
} |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
146 |
moreover |
53788 | 147 |
{ |
148 |
assume "Inf S = \<infinity>" |
|
149 |
then have "S = {\<infinity>}" |
|
60420 | 150 |
by (metis Inf_eq_PInfty \<open>S \<noteq> {}\<close>) |
53788 | 151 |
then have False |
152 |
by (metis assms(1) not_open_singleton) |
|
153 |
} |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
154 |
moreover |
53788 | 155 |
{ |
156 |
assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" |
|
157 |
from ereal_open_cont_interval[OF assms(1) * fin] |
|
158 |
obtain e where e: "e > 0" "{Inf S - e<..<Inf S + e} \<subseteq> S" . |
|
159 |
then obtain b where b: "Inf S - e < b" "b < Inf S" |
|
160 |
using fin ereal_between[of "Inf S" e] dense[of "Inf S - e"] |
|
44918 | 161 |
by auto |
53788 | 162 |
then have "b: {Inf S - e <..< Inf S + e}" |
163 |
using e fin ereal_between[of "Inf S" e] |
|
164 |
by auto |
|
165 |
then have "b \<in> S" |
|
166 |
using e by auto |
|
167 |
then have False |
|
168 |
using b by (metis complete_lattice_class.Inf_lower leD) |
|
169 |
} |
|
170 |
ultimately show False |
|
171 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
172 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
173 |
|
43920 | 174 |
lemma ereal_open_closed: |
175 |
fixes S :: "ereal set" |
|
53788 | 176 |
shows "open S \<and> closed S \<longleftrightarrow> S = {} \<or> S = UNIV" |
49664 | 177 |
proof - |
53788 | 178 |
{ |
179 |
assume lhs: "open S \<and> closed S" |
|
180 |
{ |
|
181 |
assume "-\<infinity> \<notin> S" |
|
182 |
then have "S = {}" |
|
183 |
using lhs ereal_open_closed_aux by auto |
|
184 |
} |
|
49664 | 185 |
moreover |
53788 | 186 |
{ |
187 |
assume "-\<infinity> \<in> S" |
|
188 |
then have "- S = {}" |
|
189 |
using lhs ereal_open_closed_aux[of "-S"] by auto |
|
190 |
} |
|
191 |
ultimately have "S = {} \<or> S = UNIV" |
|
192 |
by auto |
|
193 |
} |
|
194 |
then show ?thesis |
|
195 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
196 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
197 |
|
53788 | 198 |
lemma ereal_open_atLeast: |
199 |
fixes x :: ereal |
|
200 |
shows "open {x..} \<longleftrightarrow> x = -\<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
201 |
proof |
53788 | 202 |
assume "x = -\<infinity>" |
203 |
then have "{x..} = UNIV" |
|
204 |
by auto |
|
205 |
then show "open {x..}" |
|
206 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
207 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
208 |
assume "open {x..}" |
53788 | 209 |
then have "open {x..} \<and> closed {x..}" |
210 |
by auto |
|
211 |
then have "{x..} = UNIV" |
|
212 |
unfolding ereal_open_closed by auto |
|
213 |
then show "x = -\<infinity>" |
|
214 |
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
|
215 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
216 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
217 |
lemma mono_closed_real: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
218 |
fixes S :: "real set" |
53788 | 219 |
assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S" |
49664 | 220 |
and "closed S" |
53788 | 221 |
shows "S = {} \<or> S = UNIV \<or> (\<exists>a. S = {a..})" |
49664 | 222 |
proof - |
53788 | 223 |
{ |
224 |
assume "S \<noteq> {}" |
|
225 |
{ assume ex: "\<exists>B. \<forall>x\<in>S. B \<le> x" |
|
226 |
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
|
227 |
using cInf_lower[of _ S] ex by (metis bdd_below_def) |
53788 | 228 |
then have "Inf S \<in> S" |
229 |
apply (subst closed_contains_Inf) |
|
60420 | 230 |
using ex \<open>S \<noteq> {}\<close> \<open>closed S\<close> |
53788 | 231 |
apply auto |
232 |
done |
|
233 |
then have "\<forall>x. Inf S \<le> x \<longleftrightarrow> x \<in> S" |
|
234 |
using mono[rule_format, of "Inf S"] * |
|
235 |
by auto |
|
236 |
then have "S = {Inf S ..}" |
|
237 |
by auto |
|
238 |
then have "\<exists>a. S = {a ..}" |
|
239 |
by auto |
|
49664 | 240 |
} |
241 |
moreover |
|
53788 | 242 |
{ |
243 |
assume "\<not> (\<exists>B. \<forall>x\<in>S. B \<le> x)" |
|
244 |
then have nex: "\<forall>B. \<exists>x\<in>S. x < B" |
|
245 |
by (simp add: not_le) |
|
246 |
{ |
|
247 |
fix y |
|
248 |
obtain x where "x\<in>S" and "x < y" |
|
249 |
using nex by auto |
|
250 |
then have "y \<in> S" |
|
251 |
using mono[rule_format, of x y] by auto |
|
252 |
} |
|
253 |
then have "S = UNIV" |
|
254 |
by auto |
|
49664 | 255 |
} |
53788 | 256 |
ultimately have "S = UNIV \<or> (\<exists>a. S = {a ..})" |
257 |
by blast |
|
258 |
} |
|
259 |
then show ?thesis |
|
260 |
by blast |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
261 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
262 |
|
43920 | 263 |
lemma mono_closed_ereal: |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
264 |
fixes S :: "real set" |
53788 | 265 |
assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S" |
49664 | 266 |
and "closed S" |
53788 | 267 |
shows "\<exists>a. S = {x. a \<le> ereal x}" |
49664 | 268 |
proof - |
53788 | 269 |
{ |
270 |
assume "S = {}" |
|
271 |
then have ?thesis |
|
272 |
apply (rule_tac x=PInfty in exI) |
|
273 |
apply auto |
|
274 |
done |
|
275 |
} |
|
49664 | 276 |
moreover |
53788 | 277 |
{ |
278 |
assume "S = UNIV" |
|
279 |
then have ?thesis |
|
280 |
apply (rule_tac x="-\<infinity>" in exI) |
|
281 |
apply auto |
|
282 |
done |
|
283 |
} |
|
49664 | 284 |
moreover |
53788 | 285 |
{ |
286 |
assume "\<exists>a. S = {a ..}" |
|
287 |
then obtain a where "S = {a ..}" |
|
288 |
by auto |
|
289 |
then have ?thesis |
|
290 |
apply (rule_tac x="ereal a" in exI) |
|
291 |
apply auto |
|
292 |
done |
|
49664 | 293 |
} |
53788 | 294 |
ultimately show ?thesis |
295 |
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
|
296 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
297 |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
298 |
lemma Liminf_within: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
299 |
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
|
300 |
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
|
301 |
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
|
302 |
proof (rule SUP_eq, simp_all add: Ball_def Bex_def, safe) |
53788 | 303 |
fix P d |
304 |
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
|
305 |
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
|
306 |
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
|
307 |
then show "\<exists>r>0. INFIMUM (Collect P) f \<le> INFIMUM (S \<inter> ball x r - {x}) f" |
60420 | 308 |
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
|
309 |
next |
53788 | 310 |
fix d :: real |
311 |
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
|
312 |
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
|
313 |
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
|
314 |
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
|
315 |
(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
|
316 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
317 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
318 |
lemma Limsup_within: |
53788 | 319 |
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
|
320 |
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
|
321 |
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
|
322 |
proof (rule INF_eq, simp_all add: Ball_def Bex_def, safe) |
53788 | 323 |
fix P d |
324 |
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
|
325 |
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
|
326 |
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
|
327 |
then show "\<exists>r>0. SUPREMUM (S \<inter> ball x r - {x}) f \<le> SUPREMUM (Collect P) f" |
60420 | 328 |
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
|
329 |
next |
53788 | 330 |
fix d :: real |
331 |
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
|
332 |
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
|
333 |
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
|
334 |
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
|
335 |
(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
|
336 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
337 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
338 |
lemma Liminf_at: |
54257
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53788
diff
changeset
|
339 |
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
|
340 |
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
|
341 |
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
|
342 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
343 |
lemma Limsup_at: |
54257
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53788
diff
changeset
|
344 |
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
|
345 |
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
|
346 |
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
|
347 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
348 |
lemma min_Liminf_at: |
53788 | 349 |
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
|
350 |
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
|
351 |
unfolding inf_min[symmetric] Liminf_at |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
352 |
apply (subst inf_commute) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
353 |
apply (subst SUP_inf) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
354 |
apply (intro SUP_cong[OF refl]) |
54260
6a967667fd45
use INF and SUP on conditionally complete lattices in multivariate analysis
hoelzl
parents:
54258
diff
changeset
|
355 |
apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union) |
56166 | 356 |
apply (drule sym) |
357 |
apply auto |
|
57865 | 358 |
apply (metis INF_absorb centre_in_ball) |
359 |
done |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
360 |
|
60420 | 361 |
subsection \<open>monoset\<close> |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
362 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
363 |
definition (in order) mono_set: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
364 |
"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
|
365 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
366 |
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
|
367 |
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
|
368 |
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
|
369 |
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
|
370 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
371 |
lemma (in complete_linorder) mono_set_iff: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
372 |
fixes S :: "'a set" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
373 |
defines "a \<equiv> Inf S" |
53788 | 374 |
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
|
375 |
proof |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
376 |
assume "mono_set S" |
53788 | 377 |
then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" |
378 |
by (auto simp: mono_set) |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
379 |
show ?c |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
380 |
proof cases |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
381 |
assume "a \<in> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
382 |
show ?c |
60420 | 383 |
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
|
384 |
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
|
385 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
386 |
assume "a \<notin> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
387 |
have "S = {a <..}" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
388 |
proof safe |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
389 |
fix x assume "x \<in> S" |
53788 | 390 |
then have "a \<le> x" |
391 |
unfolding a_def by (rule Inf_lower) |
|
392 |
then show "a < x" |
|
60420 | 393 |
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
|
394 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
395 |
fix x assume "a < x" |
53788 | 396 |
then obtain y where "y < x" "y \<in> S" |
397 |
unfolding a_def Inf_less_iff .. |
|
398 |
with mono[of y x] show "x \<in> S" |
|
399 |
by auto |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
400 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
401 |
then show ?c .. |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
402 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
403 |
qed auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
404 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
405 |
lemma ereal_open_mono_set: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
406 |
fixes S :: "ereal set" |
53788 | 407 |
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
|
408 |
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
|
409 |
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
|
410 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
411 |
lemma ereal_closed_mono_set: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
412 |
fixes S :: "ereal set" |
53788 | 413 |
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
|
414 |
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
|
415 |
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
|
416 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
417 |
lemma ereal_Liminf_Sup_monoset: |
53788 | 418 |
fixes f :: "'a \<Rightarrow> ereal" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
419 |
shows "Liminf net f = |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
420 |
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
|
421 |
(is "_ = Sup ?A") |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
422 |
proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least) |
53788 | 423 |
fix P |
424 |
assume P: "eventually P net" |
|
425 |
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
|
426 |
assume S: "mono_set S" "INFIMUM (Collect P) f \<in> S" |
53788 | 427 |
{ |
428 |
fix x |
|
429 |
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
|
430 |
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
|
431 |
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
|
432 |
with S have "f x \<in> S" |
53788 | 433 |
by (simp add: mono_set) |
434 |
} |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
435 |
with P show "eventually (\<lambda>x. f x \<in> S) net" |
61810 | 436 |
by (auto elim: eventually_mono) |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
437 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
438 |
fix y l |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
439 |
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
|
440 |
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
|
441 |
show "l \<le> y" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
442 |
proof (rule dense_le) |
53788 | 443 |
fix B |
444 |
assume "B < l" |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
445 |
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
|
446 |
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
|
447 |
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
|
448 |
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
|
449 |
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
|
450 |
by (intro INF_greatest) auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
451 |
ultimately show "B \<le> y" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
452 |
by simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
453 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
454 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
455 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
456 |
lemma ereal_Limsup_Inf_monoset: |
53788 | 457 |
fixes f :: "'a \<Rightarrow> ereal" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
458 |
shows "Limsup net f = |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
459 |
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
|
460 |
(is "_ = Inf ?A") |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
461 |
proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest) |
53788 | 462 |
fix P |
463 |
assume P: "eventually P net" |
|
464 |
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
|
465 |
assume S: "mono_set (uminus`S)" "SUPREMUM (Collect P) f \<in> S" |
53788 | 466 |
{ |
467 |
fix x |
|
468 |
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
|
469 |
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
|
470 |
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
|
471 |
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
|
472 |
have "f x \<in> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
473 |
by (simp add: inj_image_mem_iff) } |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
474 |
with P show "eventually (\<lambda>x. f x \<in> S) net" |
61810 | 475 |
by (auto elim: eventually_mono) |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
476 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
477 |
fix y l |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
478 |
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
|
479 |
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
|
480 |
show "y \<le> l" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
481 |
proof (rule dense_ge) |
53788 | 482 |
fix B |
483 |
assume "l < B" |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
484 |
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
|
485 |
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
|
486 |
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
|
487 |
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
|
488 |
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
|
489 |
by (intro SUP_least) auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
490 |
ultimately show "y \<le> B" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
491 |
by simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
492 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
493 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
494 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
495 |
lemma liminf_bounded_open: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
496 |
fixes x :: "nat \<Rightarrow> ereal" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
497 |
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
|
498 |
(is "_ \<longleftrightarrow> ?P x0") |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
499 |
proof |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
500 |
assume "?P x0" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
501 |
then show "x0 \<le> liminf x" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
502 |
unfolding ereal_Liminf_Sup_monoset eventually_sequentially |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
503 |
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
|
504 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
505 |
assume "x0 \<le> liminf x" |
53788 | 506 |
{ |
507 |
fix S :: "ereal set" |
|
508 |
assume om: "open S" "mono_set S" "x0 \<in> S" |
|
509 |
{ |
|
510 |
assume "S = UNIV" |
|
511 |
then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S" |
|
512 |
by auto |
|
513 |
} |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
514 |
moreover |
53788 | 515 |
{ |
516 |
assume "S \<noteq> UNIV" |
|
517 |
then obtain B where B: "S = {B<..}" |
|
518 |
using om ereal_open_mono_set by auto |
|
519 |
then have "B < x0" |
|
520 |
using om by auto |
|
521 |
then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S" |
|
522 |
unfolding B |
|
60420 | 523 |
using \<open>x0 \<le> liminf x\<close> liminf_bounded_iff |
53788 | 524 |
by auto |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
525 |
} |
53788 | 526 |
ultimately have "\<exists>N. \<forall>n\<ge>N. x n \<in> S" |
527 |
by auto |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
528 |
} |
53788 | 529 |
then show "?P x0" |
530 |
by auto |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
531 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
532 |
|
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
533 |
subsection "Relate extended reals and the indicator function" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
534 |
|
59000 | 535 |
lemma ereal_indicator_le_0: "(indicator S x::ereal) \<le> 0 \<longleftrightarrow> x \<notin> S" |
536 |
by (auto split: split_indicator simp: one_ereal_def) |
|
537 |
||
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
538 |
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
|
539 |
by (auto simp: indicator_def one_ereal_def) |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
540 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
541 |
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
|
542 |
by (simp split: split_indicator) |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
543 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
544 |
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
|
545 |
by (simp split: split_indicator) |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
546 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
547 |
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
|
548 |
unfolding indicator_def by auto |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
549 |
|
59425 | 550 |
lemma indicator_inter_arith_ereal: "indicator A x * indicator B x = (indicator (A \<inter> B) x :: ereal)" |
551 |
by (simp split: split_indicator) |
|
552 |
||
44125 | 553 |
end |