author | haftmann |
Wed, 19 Mar 2014 18:47:22 +0100 | |
changeset 56218 | 1c3f1f2431f9 |
parent 56212 | 3253aaf73a01 |
child 57025 | e7fd64f82876 |
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 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
8 |
header {* Limits on the Extended real number line *} |
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 |
43920 | 11 |
imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
12 |
begin |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
13 |
|
51351 | 14 |
lemma convergent_limsup_cl: |
53788 | 15 |
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}" |
51351 | 16 |
shows "convergent X \<Longrightarrow> limsup X = lim X" |
17 |
by (auto simp: convergent_def limI lim_imp_Limsup) |
|
18 |
||
19 |
lemma lim_increasing_cl: |
|
20 |
assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m" |
|
53788 | 21 |
obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})" |
51351 | 22 |
proof |
23 |
show "f ----> (SUP n. f n)" |
|
24 |
using assms |
|
25 |
by (intro increasing_tendsto) |
|
26 |
(auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans) |
|
27 |
qed |
|
28 |
||
29 |
lemma lim_decreasing_cl: |
|
30 |
assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m" |
|
53788 | 31 |
obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})" |
51351 | 32 |
proof |
33 |
show "f ----> (INF n. f n)" |
|
34 |
using assms |
|
35 |
by (intro decreasing_tendsto) |
|
36 |
(auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans) |
|
37 |
qed |
|
38 |
||
39 |
lemma compact_complete_linorder: |
|
53788 | 40 |
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}" |
51351 | 41 |
shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l" |
42 |
proof - |
|
43 |
obtain r where "subseq r" and mono: "monoseq (X \<circ> r)" |
|
53788 | 44 |
using seq_monosub[of X] |
45 |
unfolding comp_def |
|
46 |
by auto |
|
51351 | 47 |
then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)" |
48 |
by (auto simp add: monoseq_def) |
|
53788 | 49 |
then obtain l where "(X \<circ> r) ----> l" |
50 |
using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"] |
|
51 |
by auto |
|
52 |
then show ?thesis |
|
53 |
using `subseq r` by auto |
|
51351 | 54 |
qed |
55 |
||
53788 | 56 |
lemma compact_UNIV: |
57 |
"compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)" |
|
51351 | 58 |
using compact_complete_linorder |
59 |
by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def) |
|
60 |
||
61 |
lemma compact_eq_closed: |
|
53788 | 62 |
fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" |
51351 | 63 |
shows "compact S \<longleftrightarrow> closed S" |
53788 | 64 |
using closed_inter_compact[of S, OF _ compact_UNIV] compact_imp_closed |
65 |
by auto |
|
51351 | 66 |
|
67 |
lemma closed_contains_Sup_cl: |
|
53788 | 68 |
fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" |
69 |
assumes "closed S" |
|
70 |
and "S \<noteq> {}" |
|
71 |
shows "Sup S \<in> S" |
|
51351 | 72 |
proof - |
73 |
from compact_eq_closed[of S] compact_attains_sup[of S] assms |
|
53788 | 74 |
obtain s where S: "s \<in> S" "\<forall>t\<in>S. t \<le> s" |
75 |
by auto |
|
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
51641
diff
changeset
|
76 |
then have "Sup S = s" |
51351 | 77 |
by (auto intro!: Sup_eqI) |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
51641
diff
changeset
|
78 |
with S show ?thesis |
51351 | 79 |
by simp |
80 |
qed |
|
81 |
||
82 |
lemma closed_contains_Inf_cl: |
|
53788 | 83 |
fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" |
84 |
assumes "closed S" |
|
85 |
and "S \<noteq> {}" |
|
86 |
shows "Inf S \<in> S" |
|
51351 | 87 |
proof - |
88 |
from compact_eq_closed[of S] compact_attains_inf[of S] assms |
|
53788 | 89 |
obtain s where S: "s \<in> S" "\<forall>t\<in>S. s \<le> t" |
90 |
by auto |
|
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
51641
diff
changeset
|
91 |
then have "Inf S = s" |
51351 | 92 |
by (auto intro!: Inf_eqI) |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
51641
diff
changeset
|
93 |
with S show ?thesis |
51351 | 94 |
by simp |
95 |
qed |
|
96 |
||
53788 | 97 |
lemma ereal_dense3: |
98 |
fixes x y :: ereal |
|
99 |
shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y" |
|
51351 | 100 |
proof (cases x y rule: ereal2_cases, simp_all) |
53788 | 101 |
fix r q :: real |
102 |
assume "r < q" |
|
103 |
from Rats_dense_in_real[OF this] show "\<exists>x. r < real_of_rat x \<and> real_of_rat x < q" |
|
51351 | 104 |
by (fastforce simp: Rats_def) |
105 |
next |
|
53788 | 106 |
fix r :: real |
107 |
show "\<exists>x. r < real_of_rat x" "\<exists>x. real_of_rat x < r" |
|
51351 | 108 |
using gt_ex[of r] lt_ex[of r] Rats_dense_in_real |
109 |
by (auto simp: Rats_def) |
|
110 |
qed |
|
111 |
||
112 |
instance ereal :: second_countable_topology |
|
113 |
proof (default, intro exI conjI) |
|
114 |
let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)" |
|
53788 | 115 |
show "countable ?B" |
116 |
by (auto intro: countable_rat) |
|
51351 | 117 |
show "open = generate_topology ?B" |
118 |
proof (intro ext iffI) |
|
53788 | 119 |
fix S :: "ereal set" |
120 |
assume "open S" |
|
51351 | 121 |
then show "generate_topology ?B S" |
122 |
unfolding open_generated_order |
|
123 |
proof induct |
|
124 |
case (Basis b) |
|
53788 | 125 |
then obtain e where "b = {..<e} \<or> b = {e<..}" |
126 |
by auto |
|
51351 | 127 |
moreover have "{..<e} = \<Union>{{..<x}|x. x \<in> \<rat> \<and> x < e}" "{e<..} = \<Union>{{x<..}|x. x \<in> \<rat> \<and> e < x}" |
128 |
by (auto dest: ereal_dense3 |
|
129 |
simp del: ex_simps |
|
130 |
simp add: ex_simps[symmetric] conj_commute Rats_def image_iff) |
|
131 |
ultimately show ?case |
|
132 |
by (auto intro: generate_topology.intros) |
|
133 |
qed (auto intro: generate_topology.intros) |
|
134 |
next |
|
53788 | 135 |
fix S |
136 |
assume "generate_topology ?B S" |
|
137 |
then show "open S" |
|
138 |
by induct auto |
|
51351 | 139 |
qed |
140 |
qed |
|
141 |
||
43920 | 142 |
lemma continuous_on_ereal[intro, simp]: "continuous_on A ereal" |
53788 | 143 |
unfolding continuous_on_topological open_ereal_def |
144 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
145 |
|
43920 | 146 |
lemma continuous_at_ereal[intro, simp]: "continuous (at x) ereal" |
53788 | 147 |
using continuous_on_eq_continuous_at[of UNIV] |
148 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
149 |
|
43920 | 150 |
lemma continuous_within_ereal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) ereal" |
53788 | 151 |
using continuous_on_eq_continuous_within[of A] |
152 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
153 |
|
43920 | 154 |
lemma ereal_open_uminus: |
155 |
fixes S :: "ereal set" |
|
53788 | 156 |
assumes "open S" |
157 |
shows "open (uminus ` S)" |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
158 |
using `open S`[unfolded open_generated_order] |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
159 |
proof induct |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
160 |
have "range uminus = (UNIV :: ereal set)" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
161 |
by (auto simp: image_iff ereal_uminus_eq_reorder) |
53788 | 162 |
then show "open (range uminus :: ereal set)" |
163 |
by simp |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
164 |
qed (auto simp add: image_Union image_Int) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
165 |
|
43920 | 166 |
lemma ereal_uminus_complement: |
167 |
fixes S :: "ereal set" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
168 |
shows "uminus ` (- S) = - uminus ` S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
169 |
by (auto intro!: bij_image_Compl_eq surjI[of _ uminus] simp: bij_betw_def) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
170 |
|
43920 | 171 |
lemma ereal_closed_uminus: |
172 |
fixes S :: "ereal set" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
173 |
assumes "closed S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
174 |
shows "closed (uminus ` S)" |
53788 | 175 |
using assms |
176 |
unfolding closed_def ereal_uminus_complement[symmetric] |
|
177 |
by (rule ereal_open_uminus) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
178 |
|
43920 | 179 |
lemma ereal_open_closed_aux: |
180 |
fixes S :: "ereal set" |
|
53788 | 181 |
assumes "open S" |
182 |
and "closed S" |
|
183 |
and S: "(-\<infinity>) \<notin> S" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
184 |
shows "S = {}" |
49664 | 185 |
proof (rule ccontr) |
53788 | 186 |
assume "\<not> ?thesis" |
187 |
then have *: "Inf S \<in> S" |
|
188 |
by (metis assms(2) closed_contains_Inf_cl) |
|
189 |
{ |
|
190 |
assume "Inf S = -\<infinity>" |
|
191 |
then have False |
|
192 |
using * assms(3) by auto |
|
193 |
} |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
194 |
moreover |
53788 | 195 |
{ |
196 |
assume "Inf S = \<infinity>" |
|
197 |
then have "S = {\<infinity>}" |
|
198 |
by (metis Inf_eq_PInfty `S \<noteq> {}`) |
|
199 |
then have False |
|
200 |
by (metis assms(1) not_open_singleton) |
|
201 |
} |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
202 |
moreover |
53788 | 203 |
{ |
204 |
assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" |
|
205 |
from ereal_open_cont_interval[OF assms(1) * fin] |
|
206 |
obtain e where e: "e > 0" "{Inf S - e<..<Inf S + e} \<subseteq> S" . |
|
207 |
then obtain b where b: "Inf S - e < b" "b < Inf S" |
|
208 |
using fin ereal_between[of "Inf S" e] dense[of "Inf S - e"] |
|
44918 | 209 |
by auto |
53788 | 210 |
then have "b: {Inf S - e <..< Inf S + e}" |
211 |
using e fin ereal_between[of "Inf S" e] |
|
212 |
by auto |
|
213 |
then have "b \<in> S" |
|
214 |
using e by auto |
|
215 |
then have False |
|
216 |
using b by (metis complete_lattice_class.Inf_lower leD) |
|
217 |
} |
|
218 |
ultimately show False |
|
219 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
220 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
221 |
|
43920 | 222 |
lemma ereal_open_closed: |
223 |
fixes S :: "ereal set" |
|
53788 | 224 |
shows "open S \<and> closed S \<longleftrightarrow> S = {} \<or> S = UNIV" |
49664 | 225 |
proof - |
53788 | 226 |
{ |
227 |
assume lhs: "open S \<and> closed S" |
|
228 |
{ |
|
229 |
assume "-\<infinity> \<notin> S" |
|
230 |
then have "S = {}" |
|
231 |
using lhs ereal_open_closed_aux by auto |
|
232 |
} |
|
49664 | 233 |
moreover |
53788 | 234 |
{ |
235 |
assume "-\<infinity> \<in> S" |
|
236 |
then have "- S = {}" |
|
237 |
using lhs ereal_open_closed_aux[of "-S"] by auto |
|
238 |
} |
|
239 |
ultimately have "S = {} \<or> S = UNIV" |
|
240 |
by auto |
|
241 |
} |
|
242 |
then show ?thesis |
|
243 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
244 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
245 |
|
43920 | 246 |
lemma ereal_open_affinity_pos: |
43923 | 247 |
fixes S :: "ereal set" |
53788 | 248 |
assumes "open S" |
249 |
and m: "m \<noteq> \<infinity>" "0 < m" |
|
250 |
and t: "\<bar>t\<bar> \<noteq> \<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
251 |
shows "open ((\<lambda>x. m * x + t) ` S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
252 |
proof - |
53788 | 253 |
obtain r where r[simp]: "m = ereal r" |
254 |
using m by (cases m) auto |
|
255 |
obtain p where p[simp]: "t = ereal p" |
|
256 |
using t by auto |
|
257 |
have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0" |
|
258 |
using m by auto |
|
55522 | 259 |
from `open S` [THEN ereal_openE] |
260 |
obtain l u where T: |
|
261 |
"open (ereal -` S)" |
|
262 |
"\<infinity> \<in> S \<Longrightarrow> {ereal l<..} \<subseteq> S" |
|
263 |
"- \<infinity> \<in> S \<Longrightarrow> {..<ereal u} \<subseteq> S" |
|
264 |
by blast |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
265 |
let ?f = "(\<lambda>x. m * x + t)" |
49664 | 266 |
show ?thesis |
267 |
unfolding open_ereal_def |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
268 |
proof (intro conjI impI exI subsetI) |
43920 | 269 |
have "ereal -` ?f ` S = (\<lambda>x. r * x + p) ` (ereal -` S)" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
270 |
proof safe |
49664 | 271 |
fix x y |
272 |
assume "ereal y = m * x + t" "x \<in> S" |
|
43920 | 273 |
then show "y \<in> (\<lambda>x. r * x + p) ` ereal -` S" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
274 |
using `r \<noteq> 0` by (cases x) (auto intro!: image_eqI[of _ _ "real x"] split: split_if_asm) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
275 |
qed force |
43920 | 276 |
then show "open (ereal -` ?f ` S)" |
53788 | 277 |
using open_affinity[OF T(1) `r \<noteq> 0`] |
278 |
by (auto simp: ac_simps) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
279 |
next |
49664 | 280 |
assume "\<infinity> \<in> ?f`S" |
53788 | 281 |
with `0 < r` have "\<infinity> \<in> S" |
282 |
by auto |
|
49664 | 283 |
fix x |
284 |
assume "x \<in> {ereal (r * l + p)<..}" |
|
53788 | 285 |
then have [simp]: "ereal (r * l + p) < x" |
286 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
287 |
show "x \<in> ?f`S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
288 |
proof (rule image_eqI) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
289 |
show "x = m * ((x - t) / m) + t" |
53788 | 290 |
using m t |
291 |
by (cases rule: ereal3_cases[of m x t]) auto |
|
292 |
have "ereal l < (x - t) / m" |
|
293 |
using m t |
|
294 |
by (simp add: ereal_less_divide_pos ereal_less_minus) |
|
295 |
then show "(x - t) / m \<in> S" |
|
296 |
using T(2)[OF `\<infinity> \<in> S`] by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
297 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
298 |
next |
53788 | 299 |
assume "-\<infinity> \<in> ?f ` S" |
300 |
with `0 < r` have "-\<infinity> \<in> S" |
|
301 |
by auto |
|
43920 | 302 |
fix x assume "x \<in> {..<ereal (r * u + p)}" |
53788 | 303 |
then have [simp]: "x < ereal (r * u + p)" |
304 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
305 |
show "x \<in> ?f`S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
306 |
proof (rule image_eqI) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
307 |
show "x = m * ((x - t) / m) + t" |
53788 | 308 |
using m t |
309 |
by (cases rule: ereal3_cases[of m x t]) auto |
|
43920 | 310 |
have "(x - t)/m < ereal u" |
53788 | 311 |
using m t |
312 |
by (simp add: ereal_divide_less_pos ereal_minus_less) |
|
313 |
then show "(x - t)/m \<in> S" |
|
314 |
using T(3)[OF `-\<infinity> \<in> S`] |
|
315 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
316 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
317 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
318 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
319 |
|
43920 | 320 |
lemma ereal_open_affinity: |
43923 | 321 |
fixes S :: "ereal set" |
49664 | 322 |
assumes "open S" |
323 |
and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0" |
|
324 |
and t: "\<bar>t\<bar> \<noteq> \<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
325 |
shows "open ((\<lambda>x. m * x + t) ` S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
326 |
proof cases |
49664 | 327 |
assume "0 < m" |
328 |
then show ?thesis |
|
53788 | 329 |
using ereal_open_affinity_pos[OF `open S` _ _ t, of m] m |
330 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
331 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
332 |
assume "\<not> 0 < m" then |
53788 | 333 |
have "0 < -m" |
334 |
using `m \<noteq> 0` |
|
335 |
by (cases m) auto |
|
336 |
then have m: "-m \<noteq> \<infinity>" "0 < -m" |
|
337 |
using `\<bar>m\<bar> \<noteq> \<infinity>` |
|
43920 | 338 |
by (auto simp: ereal_uminus_eq_reorder) |
53788 | 339 |
from ereal_open_affinity_pos[OF ereal_open_uminus[OF `open S`] m t] show ?thesis |
340 |
unfolding image_image by simp |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
341 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
342 |
|
43920 | 343 |
lemma ereal_lim_mult: |
344 |
fixes X :: "'a \<Rightarrow> ereal" |
|
49664 | 345 |
assumes lim: "(X ---> L) net" |
346 |
and a: "\<bar>a\<bar> \<noteq> \<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
347 |
shows "((\<lambda>i. a * X i) ---> a * L) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
348 |
proof cases |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
349 |
assume "a \<noteq> 0" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
350 |
show ?thesis |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
351 |
proof (rule topological_tendstoI) |
49664 | 352 |
fix S |
53788 | 353 |
assume "open S" and "a * L \<in> S" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
354 |
have "a * L / a = L" |
53788 | 355 |
using `a \<noteq> 0` a |
356 |
by (cases rule: ereal2_cases[of a L]) auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
357 |
then have L: "L \<in> ((\<lambda>x. x / a) ` S)" |
53788 | 358 |
using `a * L \<in> S` |
359 |
by (force simp: image_iff) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
360 |
moreover have "open ((\<lambda>x. x / a) ` S)" |
43920 | 361 |
using ereal_open_affinity[OF `open S`, of "inverse a" 0] `a \<noteq> 0` a |
362 |
by (auto simp: ereal_divide_eq ereal_inverse_eq_0 divide_ereal_def ac_simps) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
363 |
note * = lim[THEN topological_tendstoD, OF this L] |
53788 | 364 |
{ |
365 |
fix x |
|
49664 | 366 |
from a `a \<noteq> 0` have "a * (x / a) = x" |
53788 | 367 |
by (cases rule: ereal2_cases[of a x]) auto |
368 |
} |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
369 |
note this[simp] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
370 |
show "eventually (\<lambda>x. a * X x \<in> S) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
371 |
by (rule eventually_mono[OF _ *]) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
372 |
qed |
44918 | 373 |
qed auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
374 |
|
43920 | 375 |
lemma ereal_lim_uminus: |
49664 | 376 |
fixes X :: "'a \<Rightarrow> ereal" |
53788 | 377 |
shows "((\<lambda>i. - X i) ---> - L) net \<longleftrightarrow> (X ---> L) net" |
43920 | 378 |
using ereal_lim_mult[of X L net "ereal (-1)"] |
49664 | 379 |
ereal_lim_mult[of "(\<lambda>i. - X i)" "-L" net "ereal (-1)"] |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
380 |
by (auto simp add: algebra_simps) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
381 |
|
53788 | 382 |
lemma ereal_open_atLeast: |
383 |
fixes x :: ereal |
|
384 |
shows "open {x..} \<longleftrightarrow> x = -\<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
385 |
proof |
53788 | 386 |
assume "x = -\<infinity>" |
387 |
then have "{x..} = UNIV" |
|
388 |
by auto |
|
389 |
then show "open {x..}" |
|
390 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
391 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
392 |
assume "open {x..}" |
53788 | 393 |
then have "open {x..} \<and> closed {x..}" |
394 |
by auto |
|
395 |
then have "{x..} = UNIV" |
|
396 |
unfolding ereal_open_closed by auto |
|
397 |
then show "x = -\<infinity>" |
|
398 |
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
|
399 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
400 |
|
53788 | 401 |
lemma open_uminus_iff: |
402 |
fixes S :: "ereal set" |
|
403 |
shows "open (uminus ` S) \<longleftrightarrow> open S" |
|
404 |
using ereal_open_uminus[of S] ereal_open_uminus[of "uminus ` S"] |
|
405 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
406 |
|
43920 | 407 |
lemma ereal_Liminf_uminus: |
53788 | 408 |
fixes f :: "'a \<Rightarrow> ereal" |
409 |
shows "Liminf net (\<lambda>x. - (f x)) = - Limsup net f" |
|
43920 | 410 |
using ereal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
411 |
|
43920 | 412 |
lemma ereal_Lim_uminus: |
49664 | 413 |
fixes f :: "'a \<Rightarrow> ereal" |
414 |
shows "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x) ---> - f0) net" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
415 |
using |
43920 | 416 |
ereal_lim_mult[of f f0 net "- 1"] |
417 |
ereal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"] |
|
418 |
by (auto simp: ereal_uminus_reorder) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
419 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
420 |
lemma Liminf_PInfty: |
43920 | 421 |
fixes f :: "'a \<Rightarrow> ereal" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
422 |
assumes "\<not> trivial_limit net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
423 |
shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>" |
53788 | 424 |
unfolding tendsto_iff_Liminf_eq_Limsup[OF assms] |
425 |
using Liminf_le_Limsup[OF assms, of f] |
|
426 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
427 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
428 |
lemma Limsup_MInfty: |
43920 | 429 |
fixes f :: "'a \<Rightarrow> ereal" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
430 |
assumes "\<not> trivial_limit net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
431 |
shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>" |
53788 | 432 |
unfolding tendsto_iff_Liminf_eq_Limsup[OF assms] |
433 |
using Liminf_le_Limsup[OF assms, of f] |
|
434 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
435 |
|
50104 | 436 |
lemma convergent_ereal: |
53788 | 437 |
fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder,linorder_topology}" |
50104 | 438 |
shows "convergent X \<longleftrightarrow> limsup X = liminf X" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
439 |
using tendsto_iff_Liminf_eq_Limsup[of sequentially] |
50104 | 440 |
by (auto simp: convergent_def) |
441 |
||
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
442 |
lemma liminf_PInfty: |
51351 | 443 |
fixes X :: "nat \<Rightarrow> ereal" |
444 |
shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>" |
|
49664 | 445 |
by (metis Liminf_PInfty trivial_limit_sequentially) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
446 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
447 |
lemma limsup_MInfty: |
51351 | 448 |
fixes X :: "nat \<Rightarrow> ereal" |
449 |
shows "X ----> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>" |
|
49664 | 450 |
by (metis Limsup_MInfty trivial_limit_sequentially) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
451 |
|
43920 | 452 |
lemma ereal_lim_mono: |
53788 | 453 |
fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology" |
454 |
assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n" |
|
455 |
and "X ----> x" |
|
456 |
and "Y ----> y" |
|
457 |
shows "x \<le> y" |
|
51000 | 458 |
using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
459 |
|
43920 | 460 |
lemma incseq_le_ereal: |
51351 | 461 |
fixes X :: "nat \<Rightarrow> 'a::linorder_topology" |
53788 | 462 |
assumes inc: "incseq X" |
463 |
and lim: "X ----> L" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
464 |
shows "X N \<le> L" |
53788 | 465 |
using inc |
466 |
by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
467 |
|
49664 | 468 |
lemma decseq_ge_ereal: |
469 |
assumes dec: "decseq X" |
|
51351 | 470 |
and lim: "X ----> (L::'a::linorder_topology)" |
53788 | 471 |
shows "X N \<ge> L" |
49664 | 472 |
using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
473 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
474 |
lemma bounded_abs: |
53788 | 475 |
fixes a :: real |
476 |
assumes "a \<le> x" |
|
477 |
and "x \<le> b" |
|
478 |
shows "abs x \<le> max (abs a) (abs b)" |
|
49664 | 479 |
by (metis abs_less_iff assms leI le_max_iff_disj |
480 |
less_eq_real_def less_le_not_le less_minus_iff minus_minus) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
481 |
|
43920 | 482 |
lemma ereal_Sup_lim: |
53788 | 483 |
fixes a :: "'a::{complete_linorder,linorder_topology}" |
484 |
assumes "\<And>n. b n \<in> s" |
|
485 |
and "b ----> a" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
486 |
shows "a \<le> Sup s" |
49664 | 487 |
by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
488 |
|
43920 | 489 |
lemma ereal_Inf_lim: |
53788 | 490 |
fixes a :: "'a::{complete_linorder,linorder_topology}" |
491 |
assumes "\<And>n. b n \<in> s" |
|
492 |
and "b ----> a" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
493 |
shows "Inf s \<le> a" |
49664 | 494 |
by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
495 |
|
43920 | 496 |
lemma SUP_Lim_ereal: |
53788 | 497 |
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}" |
498 |
assumes inc: "incseq X" |
|
499 |
and l: "X ----> l" |
|
500 |
shows "(SUP n. X n) = l" |
|
501 |
using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l] |
|
502 |
by simp |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
503 |
|
51351 | 504 |
lemma INF_Lim_ereal: |
53788 | 505 |
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}" |
506 |
assumes dec: "decseq X" |
|
507 |
and l: "X ----> l" |
|
508 |
shows "(INF n. X n) = l" |
|
509 |
using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l] |
|
510 |
by simp |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
511 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
512 |
lemma SUP_eq_LIMSEQ: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
513 |
assumes "mono f" |
43920 | 514 |
shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f ----> x" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
515 |
proof |
43920 | 516 |
have inc: "incseq (\<lambda>i. ereal (f i))" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
517 |
using `mono f` unfolding mono_def incseq_def by auto |
53788 | 518 |
{ |
519 |
assume "f ----> x" |
|
520 |
then have "(\<lambda>i. ereal (f i)) ----> ereal x" |
|
521 |
by auto |
|
522 |
from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" . |
|
523 |
next |
|
524 |
assume "(SUP n. ereal (f n)) = ereal x" |
|
525 |
with LIMSEQ_SUP[OF inc] show "f ----> x" by auto |
|
526 |
} |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
527 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
528 |
|
43920 | 529 |
lemma liminf_ereal_cminus: |
49664 | 530 |
fixes f :: "nat \<Rightarrow> ereal" |
531 |
assumes "c \<noteq> -\<infinity>" |
|
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
532 |
shows "liminf (\<lambda>x. c - f x) = c - limsup f" |
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
533 |
proof (cases c) |
49664 | 534 |
case PInf |
53788 | 535 |
then show ?thesis |
536 |
by (simp add: Liminf_const) |
|
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
537 |
next |
49664 | 538 |
case (real r) |
539 |
then show ?thesis |
|
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56166
diff
changeset
|
540 |
unfolding liminf_SUP_INF limsup_INF_SUP |
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56166
diff
changeset
|
541 |
apply (subst INF_ereal_cminus) |
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
542 |
apply auto |
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56166
diff
changeset
|
543 |
apply (subst SUP_ereal_cminus) |
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
544 |
apply auto |
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
545 |
done |
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
546 |
qed (insert `c \<noteq> -\<infinity>`, simp) |
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
547 |
|
49664 | 548 |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
549 |
subsubsection {* Continuity *} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
550 |
|
43920 | 551 |
lemma continuous_at_of_ereal: |
552 |
fixes x0 :: ereal |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
553 |
assumes "\<bar>x0\<bar> \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
554 |
shows "continuous (at x0) real" |
49664 | 555 |
proof - |
53788 | 556 |
{ |
557 |
fix T |
|
558 |
assume T: "open T" "real x0 \<in> T" |
|
559 |
def S \<equiv> "ereal ` T" |
|
560 |
then have "ereal (real x0) \<in> S" |
|
561 |
using T by auto |
|
562 |
then have "x0 \<in> S" |
|
563 |
using assms ereal_real by auto |
|
564 |
moreover have "open S" |
|
565 |
using open_ereal S_def T by auto |
|
566 |
moreover have "\<forall>y\<in>S. real y \<in> T" |
|
567 |
using S_def T by auto |
|
568 |
ultimately have "\<exists>S. x0 \<in> S \<and> open S \<and> (\<forall>y\<in>S. real y \<in> T)" |
|
569 |
by auto |
|
49664 | 570 |
} |
53788 | 571 |
then show ?thesis |
572 |
unfolding continuous_at_open by blast |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
573 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
574 |
|
43920 | 575 |
lemma continuous_at_iff_ereal: |
53788 | 576 |
fixes f :: "'a::t2_space \<Rightarrow> real" |
577 |
shows "continuous (at x0) f \<longleftrightarrow> continuous (at x0) (ereal \<circ> f)" |
|
49664 | 578 |
proof - |
53788 | 579 |
{ |
580 |
assume "continuous (at x0) f" |
|
581 |
then have "continuous (at x0) (ereal \<circ> f)" |
|
582 |
using continuous_at_ereal continuous_at_compose[of x0 f ereal] |
|
583 |
by auto |
|
49664 | 584 |
} |
585 |
moreover |
|
53788 | 586 |
{ |
587 |
assume "continuous (at x0) (ereal \<circ> f)" |
|
588 |
then have "continuous (at x0) (real \<circ> (ereal \<circ> f))" |
|
589 |
using continuous_at_of_ereal |
|
590 |
by (intro continuous_at_compose[of x0 "ereal \<circ> f"]) auto |
|
591 |
moreover have "real \<circ> (ereal \<circ> f) = f" |
|
592 |
using real_ereal_id by (simp add: o_assoc) |
|
593 |
ultimately have "continuous (at x0) f" |
|
594 |
by auto |
|
595 |
} |
|
596 |
ultimately show ?thesis |
|
597 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
598 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
599 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
600 |
|
43920 | 601 |
lemma continuous_on_iff_ereal: |
49664 | 602 |
fixes f :: "'a::t2_space => real" |
53788 | 603 |
assumes "open A" |
604 |
shows "continuous_on A f \<longleftrightarrow> continuous_on A (ereal \<circ> f)" |
|
605 |
using continuous_at_iff_ereal assms |
|
606 |
by (auto simp add: continuous_on_eq_continuous_at cong del: continuous_on_cong) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
607 |
|
53788 | 608 |
lemma continuous_on_real: "continuous_on (UNIV - {\<infinity>, -\<infinity>::ereal}) real" |
609 |
using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal |
|
610 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
611 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
612 |
lemma continuous_on_iff_real: |
53788 | 613 |
fixes f :: "'a::t2_space \<Rightarrow> ereal" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
614 |
assumes "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
615 |
shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)" |
49664 | 616 |
proof - |
53788 | 617 |
have "f ` A \<subseteq> UNIV - {\<infinity>, -\<infinity>}" |
618 |
using assms by force |
|
49664 | 619 |
then have *: "continuous_on (f ` A) real" |
620 |
using continuous_on_real by (simp add: continuous_on_subset) |
|
53788 | 621 |
have **: "continuous_on ((real \<circ> f) ` A) ereal" |
622 |
using continuous_on_ereal continuous_on_subset[of "UNIV" "ereal" "(real \<circ> f) ` A"] |
|
623 |
by blast |
|
624 |
{ |
|
625 |
assume "continuous_on A f" |
|
626 |
then have "continuous_on A (real \<circ> f)" |
|
49664 | 627 |
apply (subst continuous_on_compose) |
53788 | 628 |
using * |
629 |
apply auto |
|
49664 | 630 |
done |
631 |
} |
|
632 |
moreover |
|
53788 | 633 |
{ |
634 |
assume "continuous_on A (real \<circ> f)" |
|
635 |
then have "continuous_on A (ereal \<circ> (real \<circ> f))" |
|
49664 | 636 |
apply (subst continuous_on_compose) |
53788 | 637 |
using ** |
638 |
apply auto |
|
49664 | 639 |
done |
640 |
then have "continuous_on A f" |
|
53788 | 641 |
apply (subst continuous_on_eq[of A "ereal \<circ> (real \<circ> f)" f]) |
642 |
using assms ereal_real |
|
643 |
apply auto |
|
49664 | 644 |
done |
645 |
} |
|
53788 | 646 |
ultimately show ?thesis |
647 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
648 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
649 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
650 |
lemma continuous_at_const: |
53788 | 651 |
fixes f :: "'a::t2_space \<Rightarrow> ereal" |
652 |
assumes "\<forall>x. f x = C" |
|
653 |
shows "\<forall>x. continuous (at x) f" |
|
654 |
unfolding continuous_at_open |
|
655 |
using assms t1_space |
|
656 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
657 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
658 |
lemma mono_closed_real: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
659 |
fixes S :: "real set" |
53788 | 660 |
assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S" |
49664 | 661 |
and "closed S" |
53788 | 662 |
shows "S = {} \<or> S = UNIV \<or> (\<exists>a. S = {a..})" |
49664 | 663 |
proof - |
53788 | 664 |
{ |
665 |
assume "S \<noteq> {}" |
|
666 |
{ assume ex: "\<exists>B. \<forall>x\<in>S. B \<le> x" |
|
667 |
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
|
668 |
using cInf_lower[of _ S] ex by (metis bdd_below_def) |
53788 | 669 |
then have "Inf S \<in> S" |
670 |
apply (subst closed_contains_Inf) |
|
671 |
using ex `S \<noteq> {}` `closed S` |
|
672 |
apply auto |
|
673 |
done |
|
674 |
then have "\<forall>x. Inf S \<le> x \<longleftrightarrow> x \<in> S" |
|
675 |
using mono[rule_format, of "Inf S"] * |
|
676 |
by auto |
|
677 |
then have "S = {Inf S ..}" |
|
678 |
by auto |
|
679 |
then have "\<exists>a. S = {a ..}" |
|
680 |
by auto |
|
49664 | 681 |
} |
682 |
moreover |
|
53788 | 683 |
{ |
684 |
assume "\<not> (\<exists>B. \<forall>x\<in>S. B \<le> x)" |
|
685 |
then have nex: "\<forall>B. \<exists>x\<in>S. x < B" |
|
686 |
by (simp add: not_le) |
|
687 |
{ |
|
688 |
fix y |
|
689 |
obtain x where "x\<in>S" and "x < y" |
|
690 |
using nex by auto |
|
691 |
then have "y \<in> S" |
|
692 |
using mono[rule_format, of x y] by auto |
|
693 |
} |
|
694 |
then have "S = UNIV" |
|
695 |
by auto |
|
49664 | 696 |
} |
53788 | 697 |
ultimately have "S = UNIV \<or> (\<exists>a. S = {a ..})" |
698 |
by blast |
|
699 |
} |
|
700 |
then show ?thesis |
|
701 |
by blast |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
702 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
703 |
|
43920 | 704 |
lemma mono_closed_ereal: |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
705 |
fixes S :: "real set" |
53788 | 706 |
assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S" |
49664 | 707 |
and "closed S" |
53788 | 708 |
shows "\<exists>a. S = {x. a \<le> ereal x}" |
49664 | 709 |
proof - |
53788 | 710 |
{ |
711 |
assume "S = {}" |
|
712 |
then have ?thesis |
|
713 |
apply (rule_tac x=PInfty in exI) |
|
714 |
apply auto |
|
715 |
done |
|
716 |
} |
|
49664 | 717 |
moreover |
53788 | 718 |
{ |
719 |
assume "S = UNIV" |
|
720 |
then have ?thesis |
|
721 |
apply (rule_tac x="-\<infinity>" in exI) |
|
722 |
apply auto |
|
723 |
done |
|
724 |
} |
|
49664 | 725 |
moreover |
53788 | 726 |
{ |
727 |
assume "\<exists>a. S = {a ..}" |
|
728 |
then obtain a where "S = {a ..}" |
|
729 |
by auto |
|
730 |
then have ?thesis |
|
731 |
apply (rule_tac x="ereal a" in exI) |
|
732 |
apply auto |
|
733 |
done |
|
49664 | 734 |
} |
53788 | 735 |
ultimately show ?thesis |
736 |
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
|
737 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
738 |
|
53788 | 739 |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
740 |
subsection {* Sums *} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
741 |
|
49664 | 742 |
lemma setsum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)" |
53788 | 743 |
proof (cases "finite A") |
744 |
case True |
|
49664 | 745 |
then show ?thesis by induct auto |
53788 | 746 |
next |
747 |
case False |
|
748 |
then show ?thesis by simp |
|
749 |
qed |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
750 |
|
43923 | 751 |
lemma setsum_Pinfty: |
752 |
fixes f :: "'a \<Rightarrow> ereal" |
|
53788 | 753 |
shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
754 |
proof safe |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
755 |
assume *: "setsum f P = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
756 |
show "finite P" |
53788 | 757 |
proof (rule ccontr) |
758 |
assume "infinite P" |
|
759 |
with * show False |
|
760 |
by auto |
|
761 |
qed |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
762 |
show "\<exists>i\<in>P. f i = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
763 |
proof (rule ccontr) |
53788 | 764 |
assume "\<not> ?thesis" |
765 |
then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>" |
|
766 |
by auto |
|
767 |
with `finite P` have "setsum f P \<noteq> \<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
768 |
by induct auto |
53788 | 769 |
with * show False |
770 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
771 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
772 |
next |
53788 | 773 |
fix i |
774 |
assume "finite P" and "i \<in> P" and "f i = \<infinity>" |
|
49664 | 775 |
then show "setsum f P = \<infinity>" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
776 |
proof induct |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
777 |
case (insert x A) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
778 |
show ?case using insert by (cases "x = i") auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
779 |
qed simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
780 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
781 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
782 |
lemma setsum_Inf: |
43923 | 783 |
fixes f :: "'a \<Rightarrow> ereal" |
53788 | 784 |
shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
785 |
proof |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
786 |
assume *: "\<bar>setsum f A\<bar> = \<infinity>" |
53788 | 787 |
have "finite A" |
788 |
by (rule ccontr) (insert *, auto) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
789 |
moreover have "\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
790 |
proof (rule ccontr) |
53788 | 791 |
assume "\<not> ?thesis" |
792 |
then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" |
|
793 |
by auto |
|
794 |
from bchoice[OF this] obtain r where "\<forall>x\<in>A. f x = ereal (r x)" .. |
|
795 |
with * show False |
|
796 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
797 |
qed |
53788 | 798 |
ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" |
799 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
800 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
801 |
assume "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" |
53788 | 802 |
then obtain i where "finite A" "i \<in> A" and "\<bar>f i\<bar> = \<infinity>" |
803 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
804 |
then show "\<bar>setsum f A\<bar> = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
805 |
proof induct |
53788 | 806 |
case (insert j A) |
807 |
then show ?case |
|
43920 | 808 |
by (cases rule: ereal3_cases[of "f i" "f j" "setsum f A"]) auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
809 |
qed simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
810 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
811 |
|
43920 | 812 |
lemma setsum_real_of_ereal: |
43923 | 813 |
fixes f :: "'i \<Rightarrow> ereal" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
814 |
assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
815 |
shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
816 |
proof - |
43920 | 817 |
have "\<forall>x\<in>S. \<exists>r. f x = ereal r" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
818 |
proof |
53788 | 819 |
fix x |
820 |
assume "x \<in> S" |
|
821 |
from assms[OF this] show "\<exists>r. f x = ereal r" |
|
822 |
by (cases "f x") auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
823 |
qed |
53788 | 824 |
from bchoice[OF this] obtain r where "\<forall>x\<in>S. f x = ereal (r x)" .. |
825 |
then show ?thesis |
|
826 |
by simp |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
827 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
828 |
|
43920 | 829 |
lemma setsum_ereal_0: |
53788 | 830 |
fixes f :: "'a \<Rightarrow> ereal" |
831 |
assumes "finite A" |
|
832 |
and "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
833 |
shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
834 |
proof |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
835 |
assume *: "(\<Sum>x\<in>A. f x) = 0" |
53788 | 836 |
then have "(\<Sum>x\<in>A. f x) \<noteq> \<infinity>" |
837 |
by auto |
|
838 |
then have "\<forall>i\<in>A. \<bar>f i\<bar> \<noteq> \<infinity>" |
|
839 |
using assms by (force simp: setsum_Pinfty) |
|
840 |
then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" |
|
841 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
842 |
from bchoice[OF this] * assms show "\<forall>i\<in>A. f i = 0" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
843 |
using setsum_nonneg_eq_0_iff[of A "\<lambda>i. real (f i)"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
844 |
qed (rule setsum_0') |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
845 |
|
43920 | 846 |
lemma setsum_ereal_right_distrib: |
49664 | 847 |
fixes f :: "'a \<Rightarrow> ereal" |
848 |
assumes "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
849 |
shows "r * setsum f A = (\<Sum>n\<in>A. r * f n)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
850 |
proof cases |
49664 | 851 |
assume "finite A" |
852 |
then show ?thesis using assms |
|
43920 | 853 |
by induct (auto simp: ereal_right_distrib setsum_nonneg) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
854 |
qed simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
855 |
|
43920 | 856 |
lemma sums_ereal_positive: |
49664 | 857 |
fixes f :: "nat \<Rightarrow> ereal" |
858 |
assumes "\<And>i. 0 \<le> f i" |
|
859 |
shows "f sums (SUP n. \<Sum>i<n. f i)" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
860 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
861 |
have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)" |
53788 | 862 |
using ereal_add_mono[OF _ assms] |
863 |
by (auto intro!: incseq_SucI) |
|
51000 | 864 |
from LIMSEQ_SUP[OF this] |
53788 | 865 |
show ?thesis unfolding sums_def |
866 |
by (simp add: atLeast0LessThan) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
867 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
868 |
|
43920 | 869 |
lemma summable_ereal_pos: |
49664 | 870 |
fixes f :: "nat \<Rightarrow> ereal" |
871 |
assumes "\<And>i. 0 \<le> f i" |
|
872 |
shows "summable f" |
|
53788 | 873 |
using sums_ereal_positive[of f, OF assms] |
874 |
unfolding summable_def |
|
875 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
876 |
|
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56166
diff
changeset
|
877 |
lemma suminf_ereal_eq_SUP: |
49664 | 878 |
fixes f :: "nat \<Rightarrow> ereal" |
879 |
assumes "\<And>i. 0 \<le> f i" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
880 |
shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)" |
53788 | 881 |
using sums_ereal_positive[of f, OF assms, THEN sums_unique] |
882 |
by simp |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
883 |
|
49664 | 884 |
lemma sums_ereal: "(\<lambda>x. ereal (f x)) sums ereal x \<longleftrightarrow> f sums x" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
885 |
unfolding sums_def by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
886 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
887 |
lemma suminf_bound: |
43920 | 888 |
fixes f :: "nat \<Rightarrow> ereal" |
53788 | 889 |
assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x" |
890 |
and pos: "\<And>n. 0 \<le> f n" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
891 |
shows "suminf f \<le> x" |
43920 | 892 |
proof (rule Lim_bounded_ereal) |
893 |
have "summable f" using pos[THEN summable_ereal_pos] . |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
894 |
then show "(\<lambda>N. \<Sum>n<N. f n) ----> suminf f" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
895 |
by (auto dest!: summable_sums simp: sums_def atLeast0LessThan) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
896 |
show "\<forall>n\<ge>0. setsum f {..<n} \<le> x" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
897 |
using assms by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
898 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
899 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
900 |
lemma suminf_bound_add: |
43920 | 901 |
fixes f :: "nat \<Rightarrow> ereal" |
49664 | 902 |
assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x" |
903 |
and pos: "\<And>n. 0 \<le> f n" |
|
904 |
and "y \<noteq> -\<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
905 |
shows "suminf f + y \<le> x" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
906 |
proof (cases y) |
49664 | 907 |
case (real r) |
908 |
then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y" |
|
43920 | 909 |
using assms by (simp add: ereal_le_minus) |
53788 | 910 |
then have "(\<Sum> n. f n) \<le> x - y" |
911 |
using pos by (rule suminf_bound) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
912 |
then show "(\<Sum> n. f n) + y \<le> x" |
43920 | 913 |
using assms real by (simp add: ereal_le_minus) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
914 |
qed (insert assms, auto) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
915 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
916 |
lemma suminf_upper: |
49664 | 917 |
fixes f :: "nat \<Rightarrow> ereal" |
918 |
assumes "\<And>n. 0 \<le> f n" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
919 |
shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)" |
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56166
diff
changeset
|
920 |
unfolding suminf_ereal_eq_SUP [OF assms] |
56166 | 921 |
by (auto intro: complete_lattice_class.SUP_upper) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
922 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
923 |
lemma suminf_0_le: |
49664 | 924 |
fixes f :: "nat \<Rightarrow> ereal" |
925 |
assumes "\<And>n. 0 \<le> f n" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
926 |
shows "0 \<le> (\<Sum>n. f n)" |
53788 | 927 |
using suminf_upper[of f 0, OF assms] |
928 |
by simp |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
929 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
930 |
lemma suminf_le_pos: |
43920 | 931 |
fixes f g :: "nat \<Rightarrow> ereal" |
53788 | 932 |
assumes "\<And>N. f N \<le> g N" |
933 |
and "\<And>N. 0 \<le> f N" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
934 |
shows "suminf f \<le> suminf g" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
935 |
proof (safe intro!: suminf_bound) |
49664 | 936 |
fix n |
53788 | 937 |
{ |
938 |
fix N |
|
939 |
have "0 \<le> g N" |
|
940 |
using assms(2,1)[of N] by auto |
|
941 |
} |
|
49664 | 942 |
have "setsum f {..<n} \<le> setsum g {..<n}" |
943 |
using assms by (auto intro: setsum_mono) |
|
53788 | 944 |
also have "\<dots> \<le> suminf g" |
945 |
using `\<And>N. 0 \<le> g N` |
|
946 |
by (rule suminf_upper) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
947 |
finally show "setsum f {..<n} \<le> suminf g" . |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
948 |
qed (rule assms(2)) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
949 |
|
53788 | 950 |
lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal) ^ Suc n) = 1" |
43920 | 951 |
using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric] |
952 |
by (simp add: one_ereal_def) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
953 |
|
43920 | 954 |
lemma suminf_add_ereal: |
955 |
fixes f g :: "nat \<Rightarrow> ereal" |
|
53788 | 956 |
assumes "\<And>i. 0 \<le> f i" |
957 |
and "\<And>i. 0 \<le> g i" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
958 |
shows "(\<Sum>i. f i + g i) = suminf f + suminf g" |
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56166
diff
changeset
|
959 |
apply (subst (1 2 3) suminf_ereal_eq_SUP) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
960 |
unfolding setsum_addf |
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56166
diff
changeset
|
961 |
apply (intro assms ereal_add_nonneg_nonneg SUP_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+ |
49664 | 962 |
done |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
963 |
|
43920 | 964 |
lemma suminf_cmult_ereal: |
965 |
fixes f g :: "nat \<Rightarrow> ereal" |
|
53788 | 966 |
assumes "\<And>i. 0 \<le> f i" |
967 |
and "0 \<le> a" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
968 |
shows "(\<Sum>i. a * f i) = a * suminf f" |
43920 | 969 |
by (auto simp: setsum_ereal_right_distrib[symmetric] assms |
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56166
diff
changeset
|
970 |
ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUP |
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56166
diff
changeset
|
971 |
intro!: SUP_ereal_cmult) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
972 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
973 |
lemma suminf_PInfty: |
43923 | 974 |
fixes f :: "nat \<Rightarrow> ereal" |
53788 | 975 |
assumes "\<And>i. 0 \<le> f i" |
976 |
and "suminf f \<noteq> \<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
977 |
shows "f i \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
978 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
979 |
from suminf_upper[of f "Suc i", OF assms(1)] assms(2) |
53788 | 980 |
have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>" |
981 |
by auto |
|
982 |
then show ?thesis |
|
983 |
unfolding setsum_Pinfty by simp |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
984 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
985 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
986 |
lemma suminf_PInfty_fun: |
53788 | 987 |
assumes "\<And>i. 0 \<le> f i" |
988 |
and "suminf f \<noteq> \<infinity>" |
|
43920 | 989 |
shows "\<exists>f'. f = (\<lambda>x. ereal (f' x))" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
990 |
proof - |
43920 | 991 |
have "\<forall>i. \<exists>r. f i = ereal r" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
992 |
proof |
53788 | 993 |
fix i |
994 |
show "\<exists>r. f i = ereal r" |
|
995 |
using suminf_PInfty[OF assms] assms(1)[of i] |
|
996 |
by (cases "f i") auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
997 |
qed |
53788 | 998 |
from choice[OF this] show ?thesis |
999 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1000 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1001 |
|
43920 | 1002 |
lemma summable_ereal: |
53788 | 1003 |
assumes "\<And>i. 0 \<le> f i" |
1004 |
and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1005 |
shows "summable f" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1006 |
proof - |
43920 | 1007 |
have "0 \<le> (\<Sum>i. ereal (f i))" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1008 |
using assms by (intro suminf_0_le) auto |
43920 | 1009 |
with assms obtain r where r: "(\<Sum>i. ereal (f i)) = ereal r" |
1010 |
by (cases "\<Sum>i. ereal (f i)") auto |
|
1011 |
from summable_ereal_pos[of "\<lambda>x. ereal (f x)"] |
|
53788 | 1012 |
have "summable (\<lambda>x. ereal (f x))" |
1013 |
using assms by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1014 |
from summable_sums[OF this] |
53788 | 1015 |
have "(\<lambda>x. ereal (f x)) sums (\<Sum>x. ereal (f x))" |
1016 |
by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1017 |
then show "summable f" |
43920 | 1018 |
unfolding r sums_ereal summable_def .. |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1019 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1020 |
|
43920 | 1021 |
lemma suminf_ereal: |
53788 | 1022 |
assumes "\<And>i. 0 \<le> f i" |
1023 |
and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>" |
|
43920 | 1024 |
shows "(\<Sum>i. ereal (f i)) = ereal (suminf f)" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1025 |
proof (rule sums_unique[symmetric]) |
43920 | 1026 |
from summable_ereal[OF assms] |
1027 |
show "(\<lambda>x. ereal (f x)) sums (ereal (suminf f))" |
|
53788 | 1028 |
unfolding sums_ereal |
1029 |
using assms |
|
1030 |
by (intro summable_sums summable_ereal) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1031 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1032 |
|
43920 | 1033 |
lemma suminf_ereal_minus: |
1034 |
fixes f g :: "nat \<Rightarrow> ereal" |
|
53788 | 1035 |
assumes ord: "\<And>i. g i \<le> f i" "\<And>i. 0 \<le> g i" |
1036 |
and fin: "suminf f \<noteq> \<infinity>" "suminf g \<noteq> \<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1037 |
shows "(\<Sum>i. f i - g i) = suminf f - suminf g" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1038 |
proof - |
53788 | 1039 |
{ |
1040 |
fix i |
|
1041 |
have "0 \<le> f i" |
|
1042 |
using ord[of i] by auto |
|
1043 |
} |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1044 |
moreover |
53788 | 1045 |
from suminf_PInfty_fun[OF `\<And>i. 0 \<le> f i` fin(1)] obtain f' where [simp]: "f = (\<lambda>x. ereal (f' x))" .. |
1046 |
from suminf_PInfty_fun[OF `\<And>i. 0 \<le> g i` fin(2)] obtain g' where [simp]: "g = (\<lambda>x. ereal (g' x))" .. |
|
1047 |
{ |
|
1048 |
fix i |
|
1049 |
have "0 \<le> f i - g i" |
|
1050 |
using ord[of i] by (auto simp: ereal_le_minus_iff) |
|
1051 |
} |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1052 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1053 |
have "suminf (\<lambda>i. f i - g i) \<le> suminf f" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1054 |
using assms by (auto intro!: suminf_le_pos simp: field_simps) |
53788 | 1055 |
then have "suminf (\<lambda>i. f i - g i) \<noteq> \<infinity>" |
1056 |
using fin by auto |
|
1057 |
ultimately show ?thesis |
|
1058 |
using assms `\<And>i. 0 \<le> f i` |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1059 |
apply simp |
49664 | 1060 |
apply (subst (1 2 3) suminf_ereal) |
1061 |
apply (auto intro!: suminf_diff[symmetric] summable_ereal) |
|
1062 |
done |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1063 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1064 |
|
49664 | 1065 |
lemma suminf_ereal_PInf [simp]: "(\<Sum>x. \<infinity>::ereal) = \<infinity>" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1066 |
proof - |
53788 | 1067 |
have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)" |
1068 |
by (rule suminf_upper) auto |
|
1069 |
then show ?thesis |
|
1070 |
by simp |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1071 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1072 |
|
43920 | 1073 |
lemma summable_real_of_ereal: |
43923 | 1074 |
fixes f :: "nat \<Rightarrow> ereal" |
49664 | 1075 |
assumes f: "\<And>i. 0 \<le> f i" |
1076 |
and fin: "(\<Sum>i. f i) \<noteq> \<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1077 |
shows "summable (\<lambda>i. real (f i))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1078 |
proof (rule summable_def[THEN iffD2]) |
53788 | 1079 |
have "0 \<le> (\<Sum>i. f i)" |
1080 |
using assms by (auto intro: suminf_0_le) |
|
1081 |
with fin obtain r where r: "ereal r = (\<Sum>i. f i)" |
|
1082 |
by (cases "(\<Sum>i. f i)") auto |
|
1083 |
{ |
|
1084 |
fix i |
|
1085 |
have "f i \<noteq> \<infinity>" |
|
1086 |
using f by (intro suminf_PInfty[OF _ fin]) auto |
|
1087 |
then have "\<bar>f i\<bar> \<noteq> \<infinity>" |
|
1088 |
using f[of i] by auto |
|
1089 |
} |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1090 |
note fin = this |
43920 | 1091 |
have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))" |
53788 | 1092 |
using f |
1093 |
by (auto intro!: summable_ereal_pos summable_sums simp: ereal_le_real_iff zero_ereal_def) |
|
1094 |
also have "\<dots> = ereal r" |
|
1095 |
using fin r by (auto simp: ereal_real) |
|
1096 |
finally show "\<exists>r. (\<lambda>i. real (f i)) sums r" |
|
1097 |
by (auto simp: sums_ereal) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1098 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1099 |
|
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
1100 |
lemma suminf_SUP_eq: |
43920 | 1101 |
fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ereal" |
53788 | 1102 |
assumes "\<And>i. incseq (\<lambda>n. f n i)" |
1103 |
and "\<And>n i. 0 \<le> f n i" |
|
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
1104 |
shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)" |
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
1105 |
proof - |
53788 | 1106 |
{ |
1107 |
fix n :: nat |
|
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
1108 |
have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)" |
53788 | 1109 |
using assms |
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56166
diff
changeset
|
1110 |
by (auto intro!: SUP_ereal_setsum [symmetric]) |
53788 | 1111 |
} |
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
1112 |
note * = this |
53788 | 1113 |
show ?thesis |
1114 |
using assms |
|
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56166
diff
changeset
|
1115 |
apply (subst (1 2) suminf_ereal_eq_SUP) |
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
1116 |
unfolding * |
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44918
diff
changeset
|
1117 |
apply (auto intro!: SUP_upper2) |
49664 | 1118 |
apply (subst SUP_commute) |
1119 |
apply rule |
|
1120 |
done |
|
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
1121 |
qed |
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
1122 |
|
47761 | 1123 |
lemma suminf_setsum_ereal: |
1124 |
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal" |
|
1125 |
assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a" |
|
1126 |
shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)" |
|
53788 | 1127 |
proof (cases "finite A") |
1128 |
case True |
|
1129 |
then show ?thesis |
|
1130 |
using nonneg |
|
47761 | 1131 |
by induct (simp_all add: suminf_add_ereal setsum_nonneg) |
53788 | 1132 |
next |
1133 |
case False |
|
1134 |
then show ?thesis by simp |
|
1135 |
qed |
|
47761 | 1136 |
|
50104 | 1137 |
lemma suminf_ereal_eq_0: |
1138 |
fixes f :: "nat \<Rightarrow> ereal" |
|
1139 |
assumes nneg: "\<And>i. 0 \<le> f i" |
|
1140 |
shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)" |
|
1141 |
proof |
|
1142 |
assume "(\<Sum>i. f i) = 0" |
|
53788 | 1143 |
{ |
1144 |
fix i |
|
1145 |
assume "f i \<noteq> 0" |
|
1146 |
with nneg have "0 < f i" |
|
1147 |
by (auto simp: less_le) |
|
50104 | 1148 |
also have "f i = (\<Sum>j. if j = i then f i else 0)" |
1149 |
by (subst suminf_finite[where N="{i}"]) auto |
|
1150 |
also have "\<dots> \<le> (\<Sum>i. f i)" |
|
53788 | 1151 |
using nneg |
1152 |
by (auto intro!: suminf_le_pos) |
|
1153 |
finally have False |
|
1154 |
using `(\<Sum>i. f i) = 0` by auto |
|
1155 |
} |
|
1156 |
then show "\<forall>i. f i = 0" |
|
1157 |
by auto |
|
50104 | 1158 |
qed simp |
1159 |
||
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1160 |
lemma Liminf_within: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1161 |
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
|
1162 |
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
|
1163 |
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
|
1164 |
proof (rule SUP_eq, simp_all add: Ball_def Bex_def, safe) |
53788 | 1165 |
fix P d |
1166 |
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
|
1167 |
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
|
1168 |
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
|
1169 |
then show "\<exists>r>0. INFIMUM (Collect P) f \<le> INFIMUM (S \<inter> ball x r - {x}) f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1170 |
by (intro exI[of _ d] INF_mono conjI `0 < d`) auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1171 |
next |
53788 | 1172 |
fix d :: real |
1173 |
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
|
1174 |
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
|
1175 |
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
|
1176 |
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
|
1177 |
(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
|
1178 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1179 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1180 |
lemma Limsup_within: |
53788 | 1181 |
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
|
1182 |
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
|
1183 |
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
|
1184 |
proof (rule INF_eq, simp_all add: Ball_def Bex_def, safe) |
53788 | 1185 |
fix P d |
1186 |
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
|
1187 |
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
|
1188 |
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
|
1189 |
then show "\<exists>r>0. SUPREMUM (S \<inter> ball x r - {x}) f \<le> SUPREMUM (Collect P) f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1190 |
by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1191 |
next |
53788 | 1192 |
fix d :: real |
1193 |
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
|
1194 |
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
|
1195 |
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
|
1196 |
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
|
1197 |
(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
|
1198 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1199 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1200 |
lemma Liminf_at: |
54257
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53788
diff
changeset
|
1201 |
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
|
1202 |
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
|
1203 |
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
|
1204 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1205 |
lemma Limsup_at: |
54257
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53788
diff
changeset
|
1206 |
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
|
1207 |
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
|
1208 |
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
|
1209 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1210 |
lemma min_Liminf_at: |
53788 | 1211 |
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
|
1212 |
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
|
1213 |
unfolding inf_min[symmetric] Liminf_at |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1214 |
apply (subst inf_commute) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1215 |
apply (subst SUP_inf) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1216 |
apply (intro SUP_cong[OF refl]) |
54260
6a967667fd45
use INF and SUP on conditionally complete lattices in multivariate analysis
hoelzl
parents:
54258
diff
changeset
|
1217 |
apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union) |
56166 | 1218 |
apply (drule sym) |
1219 |
apply auto |
|
1220 |
by (metis INF_absorb centre_in_ball) |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1221 |
|
53788 | 1222 |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1223 |
subsection {* monoset *} |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1224 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1225 |
definition (in order) mono_set: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1226 |
"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
|
1227 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1228 |
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
|
1229 |
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
|
1230 |
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
|
1231 |
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
|
1232 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1233 |
lemma (in complete_linorder) mono_set_iff: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1234 |
fixes S :: "'a set" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1235 |
defines "a \<equiv> Inf S" |
53788 | 1236 |
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
|
1237 |
proof |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1238 |
assume "mono_set S" |
53788 | 1239 |
then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" |
1240 |
by (auto simp: mono_set) |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1241 |
show ?c |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1242 |
proof cases |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1243 |
assume "a \<in> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1244 |
show ?c |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1245 |
using mono[OF _ `a \<in> S`] |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1246 |
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
|
1247 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1248 |
assume "a \<notin> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1249 |
have "S = {a <..}" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1250 |
proof safe |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1251 |
fix x assume "x \<in> S" |
53788 | 1252 |
then have "a \<le> x" |
1253 |
unfolding a_def by (rule Inf_lower) |
|
1254 |
then show "a < x" |
|
1255 |
using `x \<in> S` `a \<notin> S` by (cases "a = x") auto |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1256 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1257 |
fix x assume "a < x" |
53788 | 1258 |
then obtain y where "y < x" "y \<in> S" |
1259 |
unfolding a_def Inf_less_iff .. |
|
1260 |
with mono[of y x] show "x \<in> S" |
|
1261 |
by auto |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1262 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1263 |
then show ?c .. |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1264 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1265 |
qed auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1266 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1267 |
lemma ereal_open_mono_set: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1268 |
fixes S :: "ereal set" |
53788 | 1269 |
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
|
1270 |
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
|
1271 |
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
|
1272 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1273 |
lemma ereal_closed_mono_set: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1274 |
fixes S :: "ereal set" |
53788 | 1275 |
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
|
1276 |
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
|
1277 |
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
|
1278 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1279 |
lemma ereal_Liminf_Sup_monoset: |
53788 | 1280 |
fixes f :: "'a \<Rightarrow> ereal" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1281 |
shows "Liminf net f = |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1282 |
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
|
1283 |
(is "_ = Sup ?A") |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1284 |
proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least) |
53788 | 1285 |
fix P |
1286 |
assume P: "eventually P net" |
|
1287 |
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
|
1288 |
assume S: "mono_set S" "INFIMUM (Collect P) f \<in> S" |
53788 | 1289 |
{ |
1290 |
fix x |
|
1291 |
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
|
1292 |
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
|
1293 |
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
|
1294 |
with S have "f x \<in> S" |
53788 | 1295 |
by (simp add: mono_set) |
1296 |
} |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1297 |
with P show "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
|
1298 |
by (auto elim: eventually_elim1) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1299 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1300 |
fix y l |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1301 |
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
|
1302 |
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
|
1303 |
show "l \<le> y" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1304 |
proof (rule dense_le) |
53788 | 1305 |
fix B |
1306 |
assume "B < l" |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1307 |
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
|
1308 |
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
|
1309 |
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
|
1310 |
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
|
1311 |
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
|
1312 |
by (intro INF_greatest) auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1313 |
ultimately show "B \<le> y" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1314 |
by simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1315 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1316 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1317 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1318 |
lemma ereal_Limsup_Inf_monoset: |
53788 | 1319 |
fixes f :: "'a \<Rightarrow> ereal" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1320 |
shows "Limsup net f = |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1321 |
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
|
1322 |
(is "_ = Inf ?A") |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1323 |
proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest) |
53788 | 1324 |
fix P |
1325 |
assume P: "eventually P net" |
|
1326 |
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
|
1327 |
assume S: "mono_set (uminus`S)" "SUPREMUM (Collect P) f \<in> S" |
53788 | 1328 |
{ |
1329 |
fix x |
|
1330 |
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
|
1331 |
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
|
1332 |
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
|
1333 |
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
|
1334 |
have "f x \<in> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1335 |
by (simp add: inj_image_mem_iff) } |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1336 |
with P show "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
|
1337 |
by (auto elim: eventually_elim1) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1338 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1339 |
fix y l |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1340 |
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
|
1341 |
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
|
1342 |
show "y \<le> l" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1343 |
proof (rule dense_ge) |
53788 | 1344 |
fix B |
1345 |
assume "l < B" |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1346 |
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
|
1347 |
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
|
1348 |
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
|
1349 |
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
|
1350 |
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
|
1351 |
by (intro SUP_least) auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1352 |
ultimately show "y \<le> B" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1353 |
by simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1354 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1355 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1356 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1357 |
lemma liminf_bounded_open: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1358 |
fixes x :: "nat \<Rightarrow> ereal" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1359 |
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
|
1360 |
(is "_ \<longleftrightarrow> ?P x0") |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1361 |
proof |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1362 |
assume "?P x0" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1363 |
then show "x0 \<le> liminf x" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1364 |
unfolding ereal_Liminf_Sup_monoset eventually_sequentially |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1365 |
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
|
1366 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1367 |
assume "x0 \<le> liminf x" |
53788 | 1368 |
{ |
1369 |
fix S :: "ereal set" |
|
1370 |
assume om: "open S" "mono_set S" "x0 \<in> S" |
|
1371 |
{ |
|
1372 |
assume "S = UNIV" |
|
1373 |
then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S" |
|
1374 |
by auto |
|
1375 |
} |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1376 |
moreover |
53788 | 1377 |
{ |
1378 |
assume "S \<noteq> UNIV" |
|
1379 |
then obtain B where B: "S = {B<..}" |
|
1380 |
using om ereal_open_mono_set by auto |
|
1381 |
then have "B < x0" |
|
1382 |
using om by auto |
|
1383 |
then have "\<exists>N. \<forall>n\<ge>N. x n \<in> S" |
|
1384 |
unfolding B |
|
1385 |
using `x0 \<le> liminf x` liminf_bounded_iff |
|
1386 |
by auto |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1387 |
} |
53788 | 1388 |
ultimately have "\<exists>N. \<forall>n\<ge>N. x n \<in> S" |
1389 |
by auto |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1390 |
} |
53788 | 1391 |
then show "?P x0" |
1392 |
by auto |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1393 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1394 |
|
44125 | 1395 |
end |