author | hoelzl |
Tue, 26 Mar 2013 12:21:00 +0100 | |
changeset 51530 | 609914f0934a |
parent 51481 | ef949192e5d6 |
child 51641 | cd05e9fcc63d |
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: |
15 |
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}" |
|
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" |
|
21 |
obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})" |
|
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" |
|
31 |
obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})" |
|
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: |
|
40 |
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}" |
|
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)" |
|
44 |
using seq_monosub[of X] unfolding comp_def by auto |
|
45 |
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)" |
|
46 |
by (auto simp add: monoseq_def) |
|
47 |
then obtain l where "(X\<circ>r) ----> l" |
|
48 |
using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"] by auto |
|
49 |
then show ?thesis using `subseq r` by auto |
|
50 |
qed |
|
51 |
||
52 |
lemma compact_UNIV: "compact (UNIV :: 'a::{complete_linorder, linorder_topology, second_countable_topology} set)" |
|
53 |
using compact_complete_linorder |
|
54 |
by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def) |
|
55 |
||
56 |
lemma compact_eq_closed: |
|
57 |
fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set" |
|
58 |
shows "compact S \<longleftrightarrow> closed S" |
|
59 |
using closed_inter_compact[of S, OF _ compact_UNIV] compact_imp_closed by auto |
|
60 |
||
61 |
lemma closed_contains_Sup_cl: |
|
62 |
fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set" |
|
63 |
assumes "closed S" "S \<noteq> {}" shows "Sup S \<in> S" |
|
64 |
proof - |
|
65 |
from compact_eq_closed[of S] compact_attains_sup[of S] assms |
|
66 |
obtain s where "s \<in> S" "\<forall>t\<in>S. t \<le> s" by auto |
|
67 |
moreover then have "Sup S = s" |
|
68 |
by (auto intro!: Sup_eqI) |
|
69 |
ultimately show ?thesis |
|
70 |
by simp |
|
71 |
qed |
|
72 |
||
73 |
lemma closed_contains_Inf_cl: |
|
74 |
fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set" |
|
75 |
assumes "closed S" "S \<noteq> {}" shows "Inf S \<in> S" |
|
76 |
proof - |
|
77 |
from compact_eq_closed[of S] compact_attains_inf[of S] assms |
|
78 |
obtain s where "s \<in> S" "\<forall>t\<in>S. s \<le> t" by auto |
|
79 |
moreover then have "Inf S = s" |
|
80 |
by (auto intro!: Inf_eqI) |
|
81 |
ultimately show ?thesis |
|
82 |
by simp |
|
83 |
qed |
|
84 |
||
85 |
lemma ereal_dense3: |
|
86 |
fixes x y :: ereal shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y" |
|
87 |
proof (cases x y rule: ereal2_cases, simp_all) |
|
88 |
fix r q :: real assume "r < q" |
|
89 |
from Rats_dense_in_real[OF this] |
|
90 |
show "\<exists>x. r < real_of_rat x \<and> real_of_rat x < q" |
|
91 |
by (fastforce simp: Rats_def) |
|
92 |
next |
|
93 |
fix r :: real show "\<exists>x. r < real_of_rat x" "\<exists>x. real_of_rat x < r" |
|
94 |
using gt_ex[of r] lt_ex[of r] Rats_dense_in_real |
|
95 |
by (auto simp: Rats_def) |
|
96 |
qed |
|
97 |
||
98 |
instance ereal :: second_countable_topology |
|
99 |
proof (default, intro exI conjI) |
|
100 |
let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)" |
|
101 |
show "countable ?B" by (auto intro: countable_rat) |
|
102 |
show "open = generate_topology ?B" |
|
103 |
proof (intro ext iffI) |
|
104 |
fix S :: "ereal set" assume "open S" |
|
105 |
then show "generate_topology ?B S" |
|
106 |
unfolding open_generated_order |
|
107 |
proof induct |
|
108 |
case (Basis b) |
|
109 |
then obtain e where "b = {..< e} \<or> b = {e <..}" by auto |
|
110 |
moreover have "{..<e} = \<Union>{{..<x}|x. x \<in> \<rat> \<and> x < e}" "{e<..} = \<Union>{{x<..}|x. x \<in> \<rat> \<and> e < x}" |
|
111 |
by (auto dest: ereal_dense3 |
|
112 |
simp del: ex_simps |
|
113 |
simp add: ex_simps[symmetric] conj_commute Rats_def image_iff) |
|
114 |
ultimately show ?case |
|
115 |
by (auto intro: generate_topology.intros) |
|
116 |
qed (auto intro: generate_topology.intros) |
|
117 |
next |
|
118 |
fix S assume "generate_topology ?B S" then show "open S" by induct auto |
|
119 |
qed |
|
120 |
qed |
|
121 |
||
43920 | 122 |
lemma continuous_on_ereal[intro, simp]: "continuous_on A ereal" |
123 |
unfolding continuous_on_topological open_ereal_def by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
124 |
|
43920 | 125 |
lemma continuous_at_ereal[intro, simp]: "continuous (at x) ereal" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
126 |
using continuous_on_eq_continuous_at[of UNIV] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
127 |
|
43920 | 128 |
lemma continuous_within_ereal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) ereal" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
129 |
using continuous_on_eq_continuous_within[of A] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
130 |
|
43920 | 131 |
lemma ereal_open_uminus: |
132 |
fixes S :: "ereal set" |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
133 |
assumes "open S" shows "open (uminus ` S)" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
134 |
using `open S`[unfolded open_generated_order] |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
135 |
proof induct |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
136 |
have "range uminus = (UNIV :: ereal set)" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
137 |
by (auto simp: image_iff ereal_uminus_eq_reorder) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
138 |
then show "open (range uminus :: ereal set)" by simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
139 |
qed (auto simp add: image_Union image_Int) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
140 |
|
43920 | 141 |
lemma ereal_uminus_complement: |
142 |
fixes S :: "ereal set" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
143 |
shows "uminus ` (- S) = - uminus ` S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
144 |
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
|
145 |
|
43920 | 146 |
lemma ereal_closed_uminus: |
147 |
fixes S :: "ereal set" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
148 |
assumes "closed S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
149 |
shows "closed (uminus ` S)" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
150 |
using assms unfolding closed_def ereal_uminus_complement[symmetric] by (rule ereal_open_uminus) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
151 |
|
43920 | 152 |
lemma ereal_open_closed_aux: |
153 |
fixes S :: "ereal set" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
154 |
assumes "open S" "closed S" |
49664 | 155 |
and S: "(-\<infinity>) ~: S" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
156 |
shows "S = {}" |
49664 | 157 |
proof (rule ccontr) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
158 |
assume "S ~= {}" |
51351 | 159 |
then have *: "(Inf S):S" by (metis assms(2) closed_contains_Inf_cl) |
49664 | 160 |
{ assume "Inf S=(-\<infinity>)" |
161 |
then have False using * assms(3) by auto } |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
162 |
moreover |
49664 | 163 |
{ assume "Inf S=\<infinity>" |
164 |
then have "S={\<infinity>}" by (metis Inf_eq_PInfty `S ~= {}`) |
|
165 |
then have False by (metis assms(1) not_open_singleton) } |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
166 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
167 |
{ assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" |
43920 | 168 |
from ereal_open_cont_interval[OF assms(1) * fin] guess e . note e = this |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
169 |
then obtain b where b_def: "Inf S-e<b & b<Inf S" |
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51000
diff
changeset
|
170 |
using fin ereal_between[of "Inf S" e] dense[of "Inf S-e"] by auto |
49664 | 171 |
then have "b: {Inf S-e <..< Inf S+e}" using e fin ereal_between[of "Inf S" e] |
44918 | 172 |
by auto |
49664 | 173 |
then have "b:S" using e by auto |
174 |
then have False using b_def by (metis complete_lattice_class.Inf_lower leD) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
175 |
} ultimately show False by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
176 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
177 |
|
43920 | 178 |
lemma ereal_open_closed: |
179 |
fixes S :: "ereal set" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
180 |
shows "(open S & closed S) <-> (S = {} | S = UNIV)" |
49664 | 181 |
proof - |
182 |
{ assume lhs: "open S & closed S" |
|
183 |
{ assume "(-\<infinity>) ~: S" |
|
184 |
then have "S={}" using lhs ereal_open_closed_aux by auto } |
|
185 |
moreover |
|
186 |
{ assume "(-\<infinity>) : S" |
|
187 |
then have "(- S)={}" using lhs ereal_open_closed_aux[of "-S"] by auto } |
|
188 |
ultimately have "S = {} | S = UNIV" by auto |
|
189 |
} then show ?thesis by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
190 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
191 |
|
43920 | 192 |
lemma ereal_open_affinity_pos: |
43923 | 193 |
fixes S :: "ereal set" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
194 |
assumes "open S" and m: "m \<noteq> \<infinity>" "0 < m" and t: "\<bar>t\<bar> \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
195 |
shows "open ((\<lambda>x. m * x + t) ` S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
196 |
proof - |
43920 | 197 |
obtain r where r[simp]: "m = ereal r" using m by (cases m) auto |
198 |
obtain p where p[simp]: "t = ereal p" using t by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
199 |
have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0" using m by auto |
43920 | 200 |
from `open S`[THEN ereal_openE] guess l u . note T = this |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
201 |
let ?f = "(\<lambda>x. m * x + t)" |
49664 | 202 |
show ?thesis |
203 |
unfolding open_ereal_def |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
204 |
proof (intro conjI impI exI subsetI) |
43920 | 205 |
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
|
206 |
proof safe |
49664 | 207 |
fix x y |
208 |
assume "ereal y = m * x + t" "x \<in> S" |
|
43920 | 209 |
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
|
210 |
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
|
211 |
qed force |
43920 | 212 |
then show "open (ereal -` ?f ` S)" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
213 |
using open_affinity[OF T(1) `r \<noteq> 0`] by (auto simp: ac_simps) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
214 |
next |
49664 | 215 |
assume "\<infinity> \<in> ?f`S" |
216 |
with `0 < r` have "\<infinity> \<in> S" by auto |
|
217 |
fix x |
|
218 |
assume "x \<in> {ereal (r * l + p)<..}" |
|
43920 | 219 |
then have [simp]: "ereal (r * l + p) < x" by auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
220 |
show "x \<in> ?f`S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
221 |
proof (rule image_eqI) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
222 |
show "x = m * ((x - t) / m) + t" |
43920 | 223 |
using m t by (cases rule: ereal3_cases[of m x t]) auto |
224 |
have "ereal l < (x - t)/m" |
|
225 |
using m t by (simp add: ereal_less_divide_pos ereal_less_minus) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
226 |
then show "(x - t)/m \<in> S" using T(2)[OF `\<infinity> \<in> S`] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
227 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
228 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
229 |
assume "-\<infinity> \<in> ?f`S" with `0 < r` have "-\<infinity> \<in> S" by auto |
43920 | 230 |
fix x assume "x \<in> {..<ereal (r * u + p)}" |
231 |
then have [simp]: "x < ereal (r * u + p)" by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
232 |
show "x \<in> ?f`S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
233 |
proof (rule image_eqI) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
234 |
show "x = m * ((x - t) / m) + t" |
43920 | 235 |
using m t by (cases rule: ereal3_cases[of m x t]) auto |
236 |
have "(x - t)/m < ereal u" |
|
237 |
using m t by (simp add: ereal_divide_less_pos ereal_minus_less) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
238 |
then show "(x - t)/m \<in> S" using T(3)[OF `-\<infinity> \<in> S`] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
239 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
240 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
241 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
242 |
|
43920 | 243 |
lemma ereal_open_affinity: |
43923 | 244 |
fixes S :: "ereal set" |
49664 | 245 |
assumes "open S" |
246 |
and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0" |
|
247 |
and t: "\<bar>t\<bar> \<noteq> \<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
248 |
shows "open ((\<lambda>x. m * x + t) ` S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
249 |
proof cases |
49664 | 250 |
assume "0 < m" |
251 |
then show ?thesis |
|
43920 | 252 |
using ereal_open_affinity_pos[OF `open S` _ _ t, of m] m by auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
253 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
254 |
assume "\<not> 0 < m" then |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
255 |
have "0 < -m" using `m \<noteq> 0` by (cases m) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
256 |
then have m: "-m \<noteq> \<infinity>" "0 < -m" using `\<bar>m\<bar> \<noteq> \<infinity>` |
43920 | 257 |
by (auto simp: ereal_uminus_eq_reorder) |
258 |
from ereal_open_affinity_pos[OF ereal_open_uminus[OF `open S`] m t] |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
259 |
show ?thesis unfolding image_image by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
260 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
261 |
|
43920 | 262 |
lemma ereal_lim_mult: |
263 |
fixes X :: "'a \<Rightarrow> ereal" |
|
49664 | 264 |
assumes lim: "(X ---> L) net" |
265 |
and a: "\<bar>a\<bar> \<noteq> \<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
266 |
shows "((\<lambda>i. a * X i) ---> a * L) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
267 |
proof cases |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
268 |
assume "a \<noteq> 0" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
269 |
show ?thesis |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
270 |
proof (rule topological_tendstoI) |
49664 | 271 |
fix S |
272 |
assume "open S" "a * L \<in> S" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
273 |
have "a * L / a = L" |
43920 | 274 |
using `a \<noteq> 0` a 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
|
275 |
then have L: "L \<in> ((\<lambda>x. x / a) ` S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
276 |
using `a * L \<in> S` by (force simp: image_iff) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
277 |
moreover have "open ((\<lambda>x. x / a) ` S)" |
43920 | 278 |
using ereal_open_affinity[OF `open S`, of "inverse a" 0] `a \<noteq> 0` a |
279 |
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
|
280 |
note * = lim[THEN topological_tendstoD, OF this L] |
49664 | 281 |
{ fix x |
282 |
from a `a \<noteq> 0` have "a * (x / a) = x" |
|
43920 | 283 |
by (cases rule: ereal2_cases[of a x]) auto } |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
284 |
note this[simp] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
285 |
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
|
286 |
by (rule eventually_mono[OF _ *]) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
287 |
qed |
44918 | 288 |
qed auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
289 |
|
43920 | 290 |
lemma ereal_lim_uminus: |
49664 | 291 |
fixes X :: "'a \<Rightarrow> ereal" |
292 |
shows "((\<lambda>i. - X i) ---> -L) net \<longleftrightarrow> (X ---> L) net" |
|
43920 | 293 |
using ereal_lim_mult[of X L net "ereal (-1)"] |
49664 | 294 |
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
|
295 |
by (auto simp add: algebra_simps) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
296 |
|
43923 | 297 |
lemma ereal_open_atLeast: fixes x :: ereal shows "open {x..} \<longleftrightarrow> x = -\<infinity>" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
298 |
proof |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
299 |
assume "x = -\<infinity>" then have "{x..} = UNIV" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
300 |
then show "open {x..}" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
301 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
302 |
assume "open {x..}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
303 |
then have "open {x..} \<and> closed {x..}" by auto |
43920 | 304 |
then have "{x..} = UNIV" unfolding ereal_open_closed by auto |
305 |
then show "x = -\<infinity>" 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
|
306 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
307 |
|
43920 | 308 |
lemma open_uminus_iff: "open (uminus ` S) \<longleftrightarrow> open (S::ereal set)" |
309 |
using ereal_open_uminus[of S] ereal_open_uminus[of "uminus`S"] by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
310 |
|
43920 | 311 |
lemma ereal_Liminf_uminus: |
312 |
fixes f :: "'a => ereal" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
313 |
shows "Liminf net (\<lambda>x. - (f x)) = -(Limsup net f)" |
43920 | 314 |
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
|
315 |
|
43920 | 316 |
lemma ereal_Lim_uminus: |
49664 | 317 |
fixes f :: "'a \<Rightarrow> ereal" |
318 |
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
|
319 |
using |
43920 | 320 |
ereal_lim_mult[of f f0 net "- 1"] |
321 |
ereal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"] |
|
322 |
by (auto simp: ereal_uminus_reorder) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
323 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
324 |
lemma Liminf_PInfty: |
43920 | 325 |
fixes f :: "'a \<Rightarrow> ereal" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
326 |
assumes "\<not> trivial_limit net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
327 |
shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>" |
51351 | 328 |
unfolding tendsto_iff_Liminf_eq_Limsup[OF assms] using Liminf_le_Limsup[OF assms, of f] by auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
329 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
330 |
lemma Limsup_MInfty: |
43920 | 331 |
fixes f :: "'a \<Rightarrow> ereal" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
332 |
assumes "\<not> trivial_limit net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
333 |
shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>" |
51351 | 334 |
unfolding tendsto_iff_Liminf_eq_Limsup[OF assms] using Liminf_le_Limsup[OF assms, of f] by auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
335 |
|
50104 | 336 |
lemma convergent_ereal: |
51351 | 337 |
fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}" |
50104 | 338 |
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
|
339 |
using tendsto_iff_Liminf_eq_Limsup[of sequentially] |
50104 | 340 |
by (auto simp: convergent_def) |
341 |
||
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
342 |
lemma liminf_PInfty: |
51351 | 343 |
fixes X :: "nat \<Rightarrow> ereal" |
344 |
shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>" |
|
49664 | 345 |
by (metis Liminf_PInfty trivial_limit_sequentially) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
346 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
347 |
lemma limsup_MInfty: |
51351 | 348 |
fixes X :: "nat \<Rightarrow> ereal" |
349 |
shows "X ----> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>" |
|
49664 | 350 |
by (metis Limsup_MInfty trivial_limit_sequentially) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
351 |
|
43920 | 352 |
lemma ereal_lim_mono: |
51351 | 353 |
fixes X Y :: "nat => 'a::linorder_topology" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
354 |
assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n" |
49664 | 355 |
and "X ----> x" "Y ----> y" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
356 |
shows "x <= y" |
51000 | 357 |
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
|
358 |
|
43920 | 359 |
lemma incseq_le_ereal: |
51351 | 360 |
fixes X :: "nat \<Rightarrow> 'a::linorder_topology" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
361 |
assumes inc: "incseq X" and lim: "X ----> L" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
362 |
shows "X N \<le> L" |
49664 | 363 |
using inc 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
|
364 |
|
49664 | 365 |
lemma decseq_ge_ereal: |
366 |
assumes dec: "decseq X" |
|
51351 | 367 |
and lim: "X ----> (L::'a::linorder_topology)" |
49664 | 368 |
shows "X N >= L" |
369 |
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
|
370 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
371 |
lemma bounded_abs: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
372 |
assumes "(a::real)<=x" "x<=b" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
373 |
shows "abs x <= max (abs a) (abs b)" |
49664 | 374 |
by (metis abs_less_iff assms leI le_max_iff_disj |
375 |
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
|
376 |
|
43920 | 377 |
lemma ereal_Sup_lim: |
51351 | 378 |
assumes "\<And>n. b n \<in> s" "b ----> (a::'a::{complete_linorder, linorder_topology})" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
379 |
shows "a \<le> Sup s" |
49664 | 380 |
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
|
381 |
|
43920 | 382 |
lemma ereal_Inf_lim: |
51351 | 383 |
assumes "\<And>n. b n \<in> s" "b ----> (a::'a::{complete_linorder, linorder_topology})" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
384 |
shows "Inf s \<le> a" |
49664 | 385 |
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
|
386 |
|
43920 | 387 |
lemma SUP_Lim_ereal: |
51000 | 388 |
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}" |
51351 | 389 |
assumes inc: "incseq X" and l: "X ----> l" shows "(SUP n. X n) = l" |
51000 | 390 |
using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l] by simp |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
391 |
|
51351 | 392 |
lemma INF_Lim_ereal: |
393 |
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}" |
|
394 |
assumes dec: "decseq X" and l: "X ----> l" shows "(INF n. X n) = l" |
|
395 |
using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l] by simp |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
396 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
397 |
lemma SUP_eq_LIMSEQ: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
398 |
assumes "mono f" |
43920 | 399 |
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
|
400 |
proof |
43920 | 401 |
have inc: "incseq (\<lambda>i. ereal (f i))" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
402 |
using `mono f` unfolding mono_def incseq_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
403 |
{ assume "f ----> x" |
49664 | 404 |
then have "(\<lambda>i. ereal (f i)) ----> ereal x" by auto |
405 |
from SUP_Lim_ereal[OF inc this] |
|
406 |
show "(SUP n. ereal (f n)) = ereal x" . } |
|
43920 | 407 |
{ assume "(SUP n. ereal (f n)) = ereal x" |
51000 | 408 |
with LIMSEQ_SUP[OF inc] |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
409 |
show "f ----> x" by auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
410 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
411 |
|
43920 | 412 |
lemma liminf_ereal_cminus: |
49664 | 413 |
fixes f :: "nat \<Rightarrow> ereal" |
414 |
assumes "c \<noteq> -\<infinity>" |
|
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
415 |
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
|
416 |
proof (cases c) |
49664 | 417 |
case PInf |
418 |
then show ?thesis by (simp add: Liminf_const) |
|
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
419 |
next |
49664 | 420 |
case (real r) |
421 |
then show ?thesis |
|
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
422 |
unfolding liminf_SUPR_INFI limsup_INFI_SUPR |
43920 | 423 |
apply (subst INFI_ereal_cminus) |
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
424 |
apply auto |
43920 | 425 |
apply (subst SUPR_ereal_cminus) |
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
426 |
apply auto |
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
427 |
done |
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
428 |
qed (insert `c \<noteq> -\<infinity>`, simp) |
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
429 |
|
49664 | 430 |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
431 |
subsubsection {* Continuity *} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
432 |
|
43920 | 433 |
lemma continuous_at_of_ereal: |
434 |
fixes x0 :: ereal |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
435 |
assumes "\<bar>x0\<bar> \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
436 |
shows "continuous (at x0) real" |
49664 | 437 |
proof - |
438 |
{ fix T |
|
439 |
assume T_def: "open T & real x0 : T" |
|
440 |
def S == "ereal ` T" |
|
441 |
then have "ereal (real x0) : S" using T_def by auto |
|
442 |
then have "x0 : S" using assms ereal_real by auto |
|
443 |
moreover have "open S" using open_ereal S_def T_def by auto |
|
444 |
moreover have "ALL y:S. real y : T" using S_def T_def by auto |
|
445 |
ultimately have "EX S. x0 : S & open S & (ALL y:S. real y : T)" by auto |
|
446 |
} |
|
447 |
then show ?thesis unfolding continuous_at_open by blast |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
448 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
449 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
450 |
|
43920 | 451 |
lemma continuous_at_iff_ereal: |
49664 | 452 |
fixes f :: "'a::t2_space => real" |
453 |
shows "continuous (at x0) f <-> continuous (at x0) (ereal o f)" |
|
454 |
proof - |
|
455 |
{ assume "continuous (at x0) f" |
|
456 |
then have "continuous (at x0) (ereal o f)" |
|
457 |
using continuous_at_ereal continuous_at_compose[of x0 f ereal] by auto |
|
458 |
} |
|
459 |
moreover |
|
460 |
{ assume "continuous (at x0) (ereal o f)" |
|
461 |
then have "continuous (at x0) (real o (ereal o f))" |
|
462 |
using continuous_at_of_ereal by (intro continuous_at_compose[of x0 "ereal o f"]) auto |
|
463 |
moreover have "real o (ereal o f) = f" using real_ereal_id by (simp add: o_assoc) |
|
464 |
ultimately have "continuous (at x0) f" by auto |
|
465 |
} ultimately show ?thesis by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
466 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
467 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
468 |
|
43920 | 469 |
lemma continuous_on_iff_ereal: |
49664 | 470 |
fixes f :: "'a::t2_space => real" |
471 |
fixes A assumes "open A" |
|
472 |
shows "continuous_on A f <-> continuous_on A (ereal o f)" |
|
51481
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51475
diff
changeset
|
473 |
using continuous_at_iff_ereal assms 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
|
474 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
475 |
|
43923 | 476 |
lemma continuous_on_real: "continuous_on (UNIV-{\<infinity>,(-\<infinity>::ereal)}) real" |
49664 | 477 |
using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal by auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
478 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
479 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
480 |
lemma continuous_on_iff_real: |
43920 | 481 |
fixes f :: "'a::t2_space => ereal" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
482 |
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
|
483 |
shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)" |
49664 | 484 |
proof - |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
485 |
have "f ` A <= UNIV-{\<infinity>,(-\<infinity>)}" using assms by force |
49664 | 486 |
then have *: "continuous_on (f ` A) real" |
487 |
using continuous_on_real by (simp add: continuous_on_subset) |
|
488 |
have **: "continuous_on ((real o f) ` A) ereal" |
|
489 |
using continuous_on_ereal continuous_on_subset[of "UNIV" "ereal" "(real o f) ` A"] by blast |
|
490 |
{ assume "continuous_on A f" |
|
491 |
then have "continuous_on A (real o f)" |
|
492 |
apply (subst continuous_on_compose) |
|
493 |
using * apply auto |
|
494 |
done |
|
495 |
} |
|
496 |
moreover |
|
497 |
{ assume "continuous_on A (real o f)" |
|
498 |
then have "continuous_on A (ereal o (real o f))" |
|
499 |
apply (subst continuous_on_compose) |
|
500 |
using ** apply auto |
|
501 |
done |
|
502 |
then have "continuous_on A f" |
|
503 |
apply (subst continuous_on_eq[of A "ereal o (real o f)" f]) |
|
504 |
using assms ereal_real apply auto |
|
505 |
done |
|
506 |
} |
|
507 |
ultimately show ?thesis by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
508 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
509 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
510 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
511 |
lemma continuous_at_const: |
43920 | 512 |
fixes f :: "'a::t2_space => ereal" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
513 |
assumes "ALL x. (f x = C)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
514 |
shows "ALL x. continuous (at x) f" |
49664 | 515 |
unfolding continuous_at_open using assms t1_space by auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
516 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
517 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
518 |
lemma mono_closed_real: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
519 |
fixes S :: "real set" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
520 |
assumes mono: "ALL y z. y:S & y<=z --> z:S" |
49664 | 521 |
and "closed S" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
522 |
shows "S = {} | S = UNIV | (EX a. S = {a ..})" |
49664 | 523 |
proof - |
524 |
{ assume "S ~= {}" |
|
525 |
{ assume ex: "EX B. ALL x:S. B<=x" |
|
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51351
diff
changeset
|
526 |
then have *: "ALL x:S. Inf S <= x" using cInf_lower_EX[of _ S] ex by metis |
49664 | 527 |
then have "Inf S : S" apply (subst closed_contains_Inf) using ex `S ~= {}` `closed S` by auto |
528 |
then have "ALL x. (Inf S <= x <-> x:S)" using mono[rule_format, of "Inf S"] * by auto |
|
529 |
then have "S = {Inf S ..}" by auto |
|
530 |
then have "EX a. S = {a ..}" by auto |
|
531 |
} |
|
532 |
moreover |
|
533 |
{ assume "~(EX B. ALL x:S. B<=x)" |
|
534 |
then have nex: "ALL B. EX x:S. x<B" by (simp add: not_le) |
|
535 |
{ fix y |
|
536 |
obtain x where "x:S & x < y" using nex by auto |
|
537 |
then have "y:S" using mono[rule_format, of x y] by auto |
|
538 |
} then have "S = UNIV" by auto |
|
539 |
} |
|
540 |
ultimately have "S = UNIV | (EX a. S = {a ..})" by blast |
|
541 |
} then show ?thesis by blast |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
542 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
543 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
544 |
|
43920 | 545 |
lemma mono_closed_ereal: |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
546 |
fixes S :: "real set" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
547 |
assumes mono: "ALL y z. y:S & y<=z --> z:S" |
49664 | 548 |
and "closed S" |
43920 | 549 |
shows "EX a. S = {x. a <= ereal x}" |
49664 | 550 |
proof - |
551 |
{ assume "S = {}" |
|
552 |
then have ?thesis apply(rule_tac x=PInfty in exI) by auto } |
|
553 |
moreover |
|
554 |
{ assume "S = UNIV" |
|
555 |
then have ?thesis apply(rule_tac x="-\<infinity>" in exI) by auto } |
|
556 |
moreover |
|
557 |
{ assume "EX a. S = {a ..}" |
|
558 |
then obtain a where "S={a ..}" by auto |
|
559 |
then have ?thesis apply(rule_tac x="ereal a" in exI) by auto |
|
560 |
} |
|
561 |
ultimately show ?thesis 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
|
562 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
563 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
564 |
subsection {* Sums *} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
565 |
|
49664 | 566 |
lemma setsum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
567 |
proof cases |
49664 | 568 |
assume "finite A" |
569 |
then show ?thesis by induct auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
570 |
qed simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
571 |
|
43923 | 572 |
lemma setsum_Pinfty: |
573 |
fixes f :: "'a \<Rightarrow> ereal" |
|
574 |
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
|
575 |
proof safe |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
576 |
assume *: "setsum f P = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
577 |
show "finite P" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
578 |
proof (rule ccontr) assume "infinite P" with * show False by auto qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
579 |
show "\<exists>i\<in>P. f i = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
580 |
proof (rule ccontr) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
581 |
assume "\<not> ?thesis" then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
582 |
from `finite P` this have "setsum f P \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
583 |
by induct auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
584 |
with * show False by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
585 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
586 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
587 |
fix i assume "finite P" "i \<in> P" "f i = \<infinity>" |
49664 | 588 |
then show "setsum f P = \<infinity>" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
589 |
proof induct |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
590 |
case (insert x A) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
591 |
show ?case using insert by (cases "x = i") auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
592 |
qed simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
593 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
594 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
595 |
lemma setsum_Inf: |
43923 | 596 |
fixes f :: "'a \<Rightarrow> ereal" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
597 |
shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
598 |
proof |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
599 |
assume *: "\<bar>setsum f A\<bar> = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
600 |
have "finite A" by (rule ccontr) (insert *, auto) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
601 |
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
|
602 |
proof (rule ccontr) |
43920 | 603 |
assume "\<not> ?thesis" then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" by auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
604 |
from bchoice[OF this] guess r .. |
44142 | 605 |
with * show False by auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
606 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
607 |
ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
608 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
609 |
assume "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
610 |
then obtain i where "finite A" "i \<in> A" "\<bar>f i\<bar> = \<infinity>" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
611 |
then show "\<bar>setsum f A\<bar> = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
612 |
proof induct |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
613 |
case (insert j A) then show ?case |
43920 | 614 |
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
|
615 |
qed simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
616 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
617 |
|
43920 | 618 |
lemma setsum_real_of_ereal: |
43923 | 619 |
fixes f :: "'i \<Rightarrow> ereal" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
620 |
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
|
621 |
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
|
622 |
proof - |
43920 | 623 |
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
|
624 |
proof |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
625 |
fix x assume "x \<in> S" |
43920 | 626 |
from assms[OF this] show "\<exists>r. f x = ereal r" by (cases "f x") auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
627 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
628 |
from bchoice[OF this] guess r .. |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
629 |
then show ?thesis by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
630 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
631 |
|
43920 | 632 |
lemma setsum_ereal_0: |
633 |
fixes f :: "'a \<Rightarrow> ereal" assumes "finite A" "\<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
|
634 |
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
|
635 |
proof |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
636 |
assume *: "(\<Sum>x\<in>A. f x) = 0" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
637 |
then have "(\<Sum>x\<in>A. f x) \<noteq> \<infinity>" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
638 |
then have "\<forall>i\<in>A. \<bar>f i\<bar> \<noteq> \<infinity>" using assms by (force simp: setsum_Pinfty) |
43920 | 639 |
then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" by auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
640 |
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
|
641 |
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
|
642 |
qed (rule setsum_0') |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
643 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
644 |
|
43920 | 645 |
lemma setsum_ereal_right_distrib: |
49664 | 646 |
fixes f :: "'a \<Rightarrow> ereal" |
647 |
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
|
648 |
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
|
649 |
proof cases |
49664 | 650 |
assume "finite A" |
651 |
then show ?thesis using assms |
|
43920 | 652 |
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
|
653 |
qed simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
654 |
|
43920 | 655 |
lemma sums_ereal_positive: |
49664 | 656 |
fixes f :: "nat \<Rightarrow> ereal" |
657 |
assumes "\<And>i. 0 \<le> f i" |
|
658 |
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
|
659 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
660 |
have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)" |
43920 | 661 |
using ereal_add_mono[OF _ assms] by (auto intro!: incseq_SucI) |
51000 | 662 |
from LIMSEQ_SUP[OF this] |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
663 |
show ?thesis unfolding sums_def by (simp add: atLeast0LessThan) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
664 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
665 |
|
43920 | 666 |
lemma summable_ereal_pos: |
49664 | 667 |
fixes f :: "nat \<Rightarrow> ereal" |
668 |
assumes "\<And>i. 0 \<le> f i" |
|
669 |
shows "summable f" |
|
43920 | 670 |
using sums_ereal_positive[of f, OF assms] unfolding summable_def by auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
671 |
|
43920 | 672 |
lemma suminf_ereal_eq_SUPR: |
49664 | 673 |
fixes f :: "nat \<Rightarrow> ereal" |
674 |
assumes "\<And>i. 0 \<le> f i" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
675 |
shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)" |
43920 | 676 |
using sums_ereal_positive[of f, OF assms, THEN sums_unique] by simp |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
677 |
|
49664 | 678 |
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
|
679 |
unfolding sums_def by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
680 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
681 |
lemma suminf_bound: |
43920 | 682 |
fixes f :: "nat \<Rightarrow> ereal" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
683 |
assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x" and pos: "\<And>n. 0 \<le> f n" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
684 |
shows "suminf f \<le> x" |
43920 | 685 |
proof (rule Lim_bounded_ereal) |
686 |
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
|
687 |
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
|
688 |
by (auto dest!: summable_sums simp: sums_def atLeast0LessThan) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
689 |
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
|
690 |
using assms by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
691 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
692 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
693 |
lemma suminf_bound_add: |
43920 | 694 |
fixes f :: "nat \<Rightarrow> ereal" |
49664 | 695 |
assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x" |
696 |
and pos: "\<And>n. 0 \<le> f n" |
|
697 |
and "y \<noteq> -\<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
698 |
shows "suminf f + y \<le> x" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
699 |
proof (cases y) |
49664 | 700 |
case (real r) |
701 |
then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y" |
|
43920 | 702 |
using assms by (simp add: ereal_le_minus) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
703 |
then have "(\<Sum> n. f n) \<le> x - y" using pos by (rule suminf_bound) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
704 |
then show "(\<Sum> n. f n) + y \<le> x" |
43920 | 705 |
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
|
706 |
qed (insert assms, auto) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
707 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
708 |
lemma suminf_upper: |
49664 | 709 |
fixes f :: "nat \<Rightarrow> ereal" |
710 |
assumes "\<And>n. 0 \<le> f n" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
711 |
shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)" |
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44918
diff
changeset
|
712 |
unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def |
45031 | 713 |
by (auto intro: complete_lattice_class.Sup_upper) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
714 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
715 |
lemma suminf_0_le: |
49664 | 716 |
fixes f :: "nat \<Rightarrow> ereal" |
717 |
assumes "\<And>n. 0 \<le> f n" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
718 |
shows "0 \<le> (\<Sum>n. f n)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
719 |
using suminf_upper[of f 0, OF assms] by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
720 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
721 |
lemma suminf_le_pos: |
43920 | 722 |
fixes f g :: "nat \<Rightarrow> ereal" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
723 |
assumes "\<And>N. f N \<le> g N" "\<And>N. 0 \<le> f N" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
724 |
shows "suminf f \<le> suminf g" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
725 |
proof (safe intro!: suminf_bound) |
49664 | 726 |
fix n |
727 |
{ fix N have "0 \<le> g N" using assms(2,1)[of N] by auto } |
|
728 |
have "setsum f {..<n} \<le> setsum g {..<n}" |
|
729 |
using assms by (auto intro: setsum_mono) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
730 |
also have "... \<le> suminf g" using `\<And>N. 0 \<le> g N` by (rule suminf_upper) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
731 |
finally show "setsum f {..<n} \<le> suminf g" . |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
732 |
qed (rule assms(2)) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
733 |
|
43920 | 734 |
lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal)^Suc n) = 1" |
735 |
using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric] |
|
736 |
by (simp add: one_ereal_def) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
737 |
|
43920 | 738 |
lemma suminf_add_ereal: |
739 |
fixes f g :: "nat \<Rightarrow> ereal" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
740 |
assumes "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
741 |
shows "(\<Sum>i. f i + g i) = suminf f + suminf g" |
43920 | 742 |
apply (subst (1 2 3) suminf_ereal_eq_SUPR) |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
743 |
unfolding setsum_addf |
49664 | 744 |
apply (intro assms ereal_add_nonneg_nonneg SUPR_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+ |
745 |
done |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
746 |
|
43920 | 747 |
lemma suminf_cmult_ereal: |
748 |
fixes f g :: "nat \<Rightarrow> ereal" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
749 |
assumes "\<And>i. 0 \<le> f i" "0 \<le> a" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
750 |
shows "(\<Sum>i. a * f i) = a * suminf f" |
43920 | 751 |
by (auto simp: setsum_ereal_right_distrib[symmetric] assms |
752 |
ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUPR |
|
753 |
intro!: SUPR_ereal_cmult ) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
754 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
755 |
lemma suminf_PInfty: |
43923 | 756 |
fixes f :: "nat \<Rightarrow> ereal" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
757 |
assumes "\<And>i. 0 \<le> f i" "suminf f \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
758 |
shows "f i \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
759 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
760 |
from suminf_upper[of f "Suc i", OF assms(1)] assms(2) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
761 |
have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>" by auto |
49664 | 762 |
then show ?thesis unfolding setsum_Pinfty by simp |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
763 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
764 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
765 |
lemma suminf_PInfty_fun: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
766 |
assumes "\<And>i. 0 \<le> f i" "suminf f \<noteq> \<infinity>" |
43920 | 767 |
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
|
768 |
proof - |
43920 | 769 |
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
|
770 |
proof |
43920 | 771 |
fix i show "\<exists>r. f i = ereal r" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
772 |
using suminf_PInfty[OF assms] assms(1)[of i] by (cases "f i") auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
773 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
774 |
from choice[OF this] show ?thesis by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
775 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
776 |
|
43920 | 777 |
lemma summable_ereal: |
778 |
assumes "\<And>i. 0 \<le> f i" "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
779 |
shows "summable f" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
780 |
proof - |
43920 | 781 |
have "0 \<le> (\<Sum>i. ereal (f i))" |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
782 |
using assms by (intro suminf_0_le) auto |
43920 | 783 |
with assms obtain r where r: "(\<Sum>i. ereal (f i)) = ereal r" |
784 |
by (cases "\<Sum>i. ereal (f i)") auto |
|
785 |
from summable_ereal_pos[of "\<lambda>x. ereal (f x)"] |
|
786 |
have "summable (\<lambda>x. ereal (f x))" using assms by auto |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
787 |
from summable_sums[OF this] |
43920 | 788 |
have "(\<lambda>x. ereal (f x)) sums (\<Sum>x. ereal (f x))" by auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
789 |
then show "summable f" |
43920 | 790 |
unfolding r sums_ereal summable_def .. |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
791 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
792 |
|
43920 | 793 |
lemma suminf_ereal: |
794 |
assumes "\<And>i. 0 \<le> f i" "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>" |
|
795 |
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
|
796 |
proof (rule sums_unique[symmetric]) |
43920 | 797 |
from summable_ereal[OF assms] |
798 |
show "(\<lambda>x. ereal (f x)) sums (ereal (suminf f))" |
|
799 |
unfolding sums_ereal using assms by (intro summable_sums summable_ereal) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
800 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
801 |
|
43920 | 802 |
lemma suminf_ereal_minus: |
803 |
fixes f g :: "nat \<Rightarrow> ereal" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
804 |
assumes ord: "\<And>i. g i \<le> f i" "\<And>i. 0 \<le> g i" and fin: "suminf f \<noteq> \<infinity>" "suminf g \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
805 |
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
|
806 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
807 |
{ fix i have "0 \<le> f i" using ord[of i] by auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
808 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
809 |
from suminf_PInfty_fun[OF `\<And>i. 0 \<le> f i` fin(1)] guess f' .. note this[simp] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
810 |
from suminf_PInfty_fun[OF `\<And>i. 0 \<le> g i` fin(2)] guess g' .. note this[simp] |
43920 | 811 |
{ fix i have "0 \<le> f i - g i" using ord[of i] by (auto simp: ereal_le_minus_iff) } |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
812 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
813 |
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
|
814 |
using assms by (auto intro!: suminf_le_pos simp: field_simps) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
815 |
then have "suminf (\<lambda>i. f i - g i) \<noteq> \<infinity>" using fin by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
816 |
ultimately show ?thesis using assms `\<And>i. 0 \<le> f i` |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
817 |
apply simp |
49664 | 818 |
apply (subst (1 2 3) suminf_ereal) |
819 |
apply (auto intro!: suminf_diff[symmetric] summable_ereal) |
|
820 |
done |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
821 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
822 |
|
49664 | 823 |
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
|
824 |
proof - |
43923 | 825 |
have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)" by (rule suminf_upper) auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
826 |
then show ?thesis by simp |
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 summable_real_of_ereal: |
43923 | 830 |
fixes f :: "nat \<Rightarrow> ereal" |
49664 | 831 |
assumes f: "\<And>i. 0 \<le> f i" |
832 |
and fin: "(\<Sum>i. f i) \<noteq> \<infinity>" |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
833 |
shows "summable (\<lambda>i. real (f i))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
834 |
proof (rule summable_def[THEN iffD2]) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
835 |
have "0 \<le> (\<Sum>i. f i)" using assms by (auto intro: suminf_0_le) |
43920 | 836 |
with fin obtain r where r: "ereal r = (\<Sum>i. f i)" by (cases "(\<Sum>i. f i)") auto |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
837 |
{ fix i have "f i \<noteq> \<infinity>" using f by (intro suminf_PInfty[OF _ fin]) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
838 |
then have "\<bar>f i\<bar> \<noteq> \<infinity>" using f[of i] by auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
839 |
note fin = this |
43920 | 840 |
have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))" |
841 |
using f by (auto intro!: summable_ereal_pos summable_sums simp: ereal_le_real_iff zero_ereal_def) |
|
842 |
also have "\<dots> = ereal r" using fin r by (auto simp: ereal_real) |
|
843 |
finally show "\<exists>r. (\<lambda>i. real (f i)) sums r" by (auto simp: sums_ereal) |
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
844 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
845 |
|
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
846 |
lemma suminf_SUP_eq: |
43920 | 847 |
fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ereal" |
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
848 |
assumes "\<And>i. incseq (\<lambda>n. f n i)" "\<And>n i. 0 \<le> f n i" |
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
849 |
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
|
850 |
proof - |
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
851 |
{ fix n :: nat |
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
852 |
have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)" |
43920 | 853 |
using assms by (auto intro!: SUPR_ereal_setsum[symmetric]) } |
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
854 |
note * = this |
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
855 |
show ?thesis using assms |
43920 | 856 |
apply (subst (1 2) suminf_ereal_eq_SUPR) |
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
857 |
unfolding * |
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44918
diff
changeset
|
858 |
apply (auto intro!: SUP_upper2) |
49664 | 859 |
apply (subst SUP_commute) |
860 |
apply rule |
|
861 |
done |
|
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
862 |
qed |
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset
|
863 |
|
47761 | 864 |
lemma suminf_setsum_ereal: |
865 |
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal" |
|
866 |
assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a" |
|
867 |
shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)" |
|
868 |
proof cases |
|
49664 | 869 |
assume "finite A" |
870 |
then show ?thesis using nonneg |
|
47761 | 871 |
by induct (simp_all add: suminf_add_ereal setsum_nonneg) |
872 |
qed simp |
|
873 |
||
50104 | 874 |
lemma suminf_ereal_eq_0: |
875 |
fixes f :: "nat \<Rightarrow> ereal" |
|
876 |
assumes nneg: "\<And>i. 0 \<le> f i" |
|
877 |
shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)" |
|
878 |
proof |
|
879 |
assume "(\<Sum>i. f i) = 0" |
|
880 |
{ fix i assume "f i \<noteq> 0" |
|
881 |
with nneg have "0 < f i" by (auto simp: less_le) |
|
882 |
also have "f i = (\<Sum>j. if j = i then f i else 0)" |
|
883 |
by (subst suminf_finite[where N="{i}"]) auto |
|
884 |
also have "\<dots> \<le> (\<Sum>i. f i)" |
|
885 |
using nneg by (auto intro!: suminf_le_pos) |
|
886 |
finally have False using `(\<Sum>i. f i) = 0` by auto } |
|
887 |
then show "\<forall>i. f i = 0" by auto |
|
888 |
qed simp |
|
889 |
||
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
890 |
lemma Liminf_within: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
891 |
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
|
892 |
shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)" |
51530
609914f0934a
rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
hoelzl
parents:
51481
diff
changeset
|
893 |
unfolding Liminf_def eventually_within_less |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
894 |
proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
895 |
fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
896 |
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
|
897 |
by (auto simp: zero_less_dist_iff dist_commute) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
898 |
then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
899 |
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
|
900 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
901 |
fix d :: real assume "0 < d" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
902 |
then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and> |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
903 |
INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
904 |
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
|
905 |
(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
|
906 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
907 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
908 |
lemma Limsup_within: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
909 |
fixes f :: "'a::metric_space => 'b::complete_lattice" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
910 |
shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)" |
51530
609914f0934a
rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
hoelzl
parents:
51481
diff
changeset
|
911 |
unfolding Limsup_def eventually_within_less |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
912 |
proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
913 |
fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
914 |
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
|
915 |
by (auto simp: zero_less_dist_iff dist_commute) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
916 |
then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
917 |
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
|
918 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
919 |
fix d :: real assume "0 < d" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
920 |
then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and> |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
921 |
SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
922 |
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
|
923 |
(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
|
924 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
925 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
926 |
lemma Liminf_at: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
927 |
fixes f :: "'a::metric_space => _" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
928 |
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
|
929 |
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
|
930 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
931 |
lemma Limsup_at: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
932 |
fixes f :: "'a::metric_space => _" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
933 |
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
|
934 |
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
|
935 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
936 |
lemma min_Liminf_at: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
937 |
fixes f :: "'a::metric_space => 'b::complete_linorder" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
938 |
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
|
939 |
unfolding inf_min[symmetric] Liminf_at |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
940 |
apply (subst inf_commute) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
941 |
apply (subst SUP_inf) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
942 |
apply (intro SUP_cong[OF refl]) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
943 |
apply (cut_tac A="ball x b - {x}" and B="{x}" and M=f in INF_union) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
944 |
apply (simp add: INF_def del: inf_ereal_def) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
945 |
done |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
946 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
947 |
subsection {* monoset *} |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
948 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
949 |
definition (in order) mono_set: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
950 |
"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
|
951 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
952 |
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
|
953 |
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
|
954 |
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
|
955 |
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
|
956 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
957 |
lemma (in complete_linorder) mono_set_iff: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
958 |
fixes S :: "'a set" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
959 |
defines "a \<equiv> Inf S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
960 |
shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c") |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
961 |
proof |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
962 |
assume "mono_set S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
963 |
then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
964 |
show ?c |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
965 |
proof cases |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
966 |
assume "a \<in> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
967 |
show ?c |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
968 |
using mono[OF _ `a \<in> S`] |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
969 |
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
|
970 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
971 |
assume "a \<notin> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
972 |
have "S = {a <..}" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
973 |
proof safe |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
974 |
fix x assume "x \<in> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
975 |
then have "a \<le> x" unfolding a_def by (rule Inf_lower) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
976 |
then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
977 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
978 |
fix x assume "a < x" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
979 |
then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff .. |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
980 |
with mono[of y x] show "x \<in> S" by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
981 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
982 |
then show ?c .. |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
983 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
984 |
qed auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
985 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
986 |
lemma ereal_open_mono_set: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
987 |
fixes S :: "ereal set" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
988 |
shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {Inf S <..})" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
989 |
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
|
990 |
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
|
991 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
992 |
lemma ereal_closed_mono_set: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
993 |
fixes S :: "ereal set" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
994 |
shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
995 |
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
|
996 |
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
|
997 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
998 |
lemma ereal_Liminf_Sup_monoset: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
999 |
fixes f :: "'a => ereal" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1000 |
shows "Liminf net f = |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1001 |
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
|
1002 |
(is "_ = Sup ?A") |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1003 |
proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1004 |
fix P assume P: "eventually P net" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1005 |
fix S assume S: "mono_set S" "INFI (Collect P) f \<in> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1006 |
{ fix x assume "P x" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1007 |
then have "INFI (Collect P) f \<le> f x" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1008 |
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
|
1009 |
with S have "f x \<in> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1010 |
by (simp add: mono_set) } |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1011 |
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
|
1012 |
by (auto elim: eventually_elim1) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1013 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1014 |
fix y l |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1015 |
assume S: "\<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
|
1016 |
assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1017 |
show "l \<le> y" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1018 |
proof (rule dense_le) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1019 |
fix B assume "B < l" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1020 |
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
|
1021 |
by (intro S[rule_format]) auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1022 |
then have "INFI {x. B < f x} f \<le> y" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1023 |
using P by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1024 |
moreover have "B \<le> INFI {x. B < f x} f" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1025 |
by (intro INF_greatest) auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1026 |
ultimately show "B \<le> y" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1027 |
by simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1028 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1029 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1030 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1031 |
lemma ereal_Limsup_Inf_monoset: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1032 |
fixes f :: "'a => ereal" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1033 |
shows "Limsup net f = |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1034 |
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
|
1035 |
(is "_ = Inf ?A") |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1036 |
proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1037 |
fix P assume P: "eventually P net" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1038 |
fix S assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1039 |
{ fix x assume "P x" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1040 |
then have "f x \<le> SUPR (Collect P) f" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1041 |
by (intro complete_lattice_class.SUP_upper) simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1042 |
with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1043 |
have "f x \<in> S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1044 |
by (simp add: inj_image_mem_iff) } |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1045 |
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
|
1046 |
by (auto elim: eventually_elim1) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1047 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1048 |
fix y l |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1049 |
assume S: "\<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
|
1050 |
assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1051 |
show "y \<le> l" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1052 |
proof (rule dense_ge) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1053 |
fix B assume "l < B" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1054 |
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
|
1055 |
by (intro S[rule_format]) auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1056 |
then have "y \<le> SUPR {x. f x < B} f" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1057 |
using P by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1058 |
moreover have "SUPR {x. f x < B} f \<le> B" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1059 |
by (intro SUP_least) auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1060 |
ultimately show "y \<le> B" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1061 |
by simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1062 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1063 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1064 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1065 |
lemma liminf_bounded_open: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1066 |
fixes x :: "nat \<Rightarrow> ereal" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1067 |
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
|
1068 |
(is "_ \<longleftrightarrow> ?P x0") |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1069 |
proof |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1070 |
assume "?P x0" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1071 |
then show "x0 \<le> liminf x" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1072 |
unfolding ereal_Liminf_Sup_monoset eventually_sequentially |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1073 |
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
|
1074 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1075 |
assume "x0 \<le> liminf x" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1076 |
{ fix S :: "ereal set" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1077 |
assume om: "open S & mono_set S & x0:S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1078 |
{ assume "S = UNIV" then have "EX N. (ALL n>=N. x n : S)" by auto } |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1079 |
moreover |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1080 |
{ assume "~(S=UNIV)" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1081 |
then obtain B where B_def: "S = {B<..}" using om ereal_open_mono_set by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1082 |
then have "B<x0" using om by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1083 |
then have "EX N. ALL n>=N. x n : S" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1084 |
unfolding B_def using `x0 \<le> liminf x` liminf_bounded_iff by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1085 |
} |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1086 |
ultimately have "EX N. (ALL n>=N. x n : S)" by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1087 |
} |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1088 |
then show "?P x0" by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1089 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset
|
1090 |
|
44125 | 1091 |
end |