author  hoelzl 
Tue, 05 Nov 2013 09:44:59 +0100  
changeset 54260  6a967667fd45 
parent 54258  adfc759263ab 
child 55522  23d2cbac6dce 
permissions  rwrr 
41983  1 
(* Title: HOL/Multivariate_Analysis/Extended_Real_Limits.thy 
2 
Author: Johannes Hölzl, TU München 

3 
Author: Robert Himmelmann, TU München 

4 
Author: Armin Heller, TU München 

5 
Author: Bogdan Grechuk, University of Edinburgh 

6 
*) 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

7 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

8 
header {* Limits on the Extended real number line *} 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

9 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

10 
theory Extended_Real_Limits 
43920  11 
imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

12 
begin 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

13 

51351  14 
lemma convergent_limsup_cl: 
53788  15 
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}" 
51351  16 
shows "convergent X \<Longrightarrow> limsup X = lim X" 
17 
by (auto simp: convergent_def limI lim_imp_Limsup) 

18 

19 
lemma lim_increasing_cl: 

20 
assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m" 

53788  21 
obtains l where "f > (l::'a::{complete_linorder,linorder_topology})" 
51351  22 
proof 
23 
show "f > (SUP n. f n)" 

24 
using assms 

25 
by (intro increasing_tendsto) 

26 
(auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans) 

27 
qed 

28 

29 
lemma lim_decreasing_cl: 

30 
assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m" 

53788  31 
obtains l where "f > (l::'a::{complete_linorder,linorder_topology})" 
51351  32 
proof 
33 
show "f > (INF n. f n)" 

34 
using assms 

35 
by (intro decreasing_tendsto) 

36 
(auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans) 

37 
qed 

38 

39 
lemma compact_complete_linorder: 

53788  40 
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}" 
51351  41 
shows "\<exists>l r. subseq r \<and> (X \<circ> r) > l" 
42 
proof  

43 
obtain r where "subseq r" and mono: "monoseq (X \<circ> r)" 

53788  44 
using seq_monosub[of X] 
45 
unfolding comp_def 

46 
by auto 

51351  47 
then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)" 
48 
by (auto simp add: monoseq_def) 

53788  49 
then obtain l where "(X \<circ> r) > l" 
50 
using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"] 

51 
by auto 

52 
then show ?thesis 

53 
using `subseq r` by auto 

51351  54 
qed 
55 

53788  56 
lemma compact_UNIV: 
57 
"compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)" 

51351  58 
using compact_complete_linorder 
59 
by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def) 

60 

61 
lemma compact_eq_closed: 

53788  62 
fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" 
51351  63 
shows "compact S \<longleftrightarrow> closed S" 
53788  64 
using closed_inter_compact[of S, OF _ compact_UNIV] compact_imp_closed 
65 
by auto 

51351  66 

67 
lemma closed_contains_Sup_cl: 

53788  68 
fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" 
69 
assumes "closed S" 

70 
and "S \<noteq> {}" 

71 
shows "Sup S \<in> S" 

51351  72 
proof  
73 
from compact_eq_closed[of S] compact_attains_sup[of S] assms 

53788  74 
obtain s where S: "s \<in> S" "\<forall>t\<in>S. t \<le> s" 
75 
by auto 

53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
51641
diff
changeset

76 
then have "Sup S = s" 
51351  77 
by (auto intro!: Sup_eqI) 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
51641
diff
changeset

78 
with S show ?thesis 
51351  79 
by simp 
80 
qed 

81 

82 
lemma closed_contains_Inf_cl: 

53788  83 
fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" 
84 
assumes "closed S" 

85 
and "S \<noteq> {}" 

86 
shows "Inf S \<in> S" 

51351  87 
proof  
88 
from compact_eq_closed[of S] compact_attains_inf[of S] assms 

53788  89 
obtain s where S: "s \<in> S" "\<forall>t\<in>S. s \<le> t" 
90 
by auto 

53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
51641
diff
changeset

91 
then have "Inf S = s" 
51351  92 
by (auto intro!: Inf_eqI) 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
51641
diff
changeset

93 
with S show ?thesis 
51351  94 
by simp 
95 
qed 

96 

53788  97 
lemma ereal_dense3: 
98 
fixes x y :: ereal 

99 
shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y" 

51351  100 
proof (cases x y rule: ereal2_cases, simp_all) 
53788  101 
fix r q :: real 
102 
assume "r < q" 

103 
from Rats_dense_in_real[OF this] show "\<exists>x. r < real_of_rat x \<and> real_of_rat x < q" 

51351  104 
by (fastforce simp: Rats_def) 
105 
next 

53788  106 
fix r :: real 
107 
show "\<exists>x. r < real_of_rat x" "\<exists>x. real_of_rat x < r" 

51351  108 
using gt_ex[of r] lt_ex[of r] Rats_dense_in_real 
109 
by (auto simp: Rats_def) 

110 
qed 

111 

112 
instance ereal :: second_countable_topology 

113 
proof (default, intro exI conjI) 

114 
let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)" 

53788  115 
show "countable ?B" 
116 
by (auto intro: countable_rat) 

51351  117 
show "open = generate_topology ?B" 
118 
proof (intro ext iffI) 

53788  119 
fix S :: "ereal set" 
120 
assume "open S" 

51351  121 
then show "generate_topology ?B S" 
122 
unfolding open_generated_order 

123 
proof induct 

124 
case (Basis b) 

53788  125 
then obtain e where "b = {..<e} \<or> b = {e<..}" 
126 
by auto 

51351  127 
moreover have "{..<e} = \<Union>{{..<x}x. x \<in> \<rat> \<and> x < e}" "{e<..} = \<Union>{{x<..}x. x \<in> \<rat> \<and> e < x}" 
128 
by (auto dest: ereal_dense3 

129 
simp del: ex_simps 

130 
simp add: ex_simps[symmetric] conj_commute Rats_def image_iff) 

131 
ultimately show ?case 

132 
by (auto intro: generate_topology.intros) 

133 
qed (auto intro: generate_topology.intros) 

134 
next 

53788  135 
fix S 
136 
assume "generate_topology ?B S" 

137 
then show "open S" 

138 
by induct auto 

51351  139 
qed 
140 
qed 

141 

43920  142 
lemma continuous_on_ereal[intro, simp]: "continuous_on A ereal" 
53788  143 
unfolding continuous_on_topological open_ereal_def 
144 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

145 

43920  146 
lemma continuous_at_ereal[intro, simp]: "continuous (at x) ereal" 
53788  147 
using continuous_on_eq_continuous_at[of UNIV] 
148 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

149 

43920  150 
lemma continuous_within_ereal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) ereal" 
53788  151 
using continuous_on_eq_continuous_within[of A] 
152 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

153 

43920  154 
lemma ereal_open_uminus: 
155 
fixes S :: "ereal set" 

53788  156 
assumes "open S" 
157 
shows "open (uminus ` S)" 

51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset

158 
using `open S`[unfolded open_generated_order] 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset

159 
proof induct 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset

160 
have "range uminus = (UNIV :: ereal set)" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset

161 
by (auto simp: image_iff ereal_uminus_eq_reorder) 
53788  162 
then show "open (range uminus :: ereal set)" 
163 
by simp 

51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset

164 
qed (auto simp add: image_Union image_Int) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

165 

43920  166 
lemma ereal_uminus_complement: 
167 
fixes S :: "ereal set" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

168 
shows "uminus ` ( S) =  uminus ` S" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

169 
by (auto intro!: bij_image_Compl_eq surjI[of _ uminus] simp: bij_betw_def) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

170 

43920  171 
lemma ereal_closed_uminus: 
172 
fixes S :: "ereal set" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

173 
assumes "closed S" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

174 
shows "closed (uminus ` S)" 
53788  175 
using assms 
176 
unfolding closed_def ereal_uminus_complement[symmetric] 

177 
by (rule ereal_open_uminus) 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

178 

43920  179 
lemma ereal_open_closed_aux: 
180 
fixes S :: "ereal set" 

53788  181 
assumes "open S" 
182 
and "closed S" 

183 
and S: "(\<infinity>) \<notin> S" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

184 
shows "S = {}" 
49664  185 
proof (rule ccontr) 
53788  186 
assume "\<not> ?thesis" 
187 
then have *: "Inf S \<in> S" 

188 
by (metis assms(2) closed_contains_Inf_cl) 

189 
{ 

190 
assume "Inf S = \<infinity>" 

191 
then have False 

192 
using * assms(3) by auto 

193 
} 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

194 
moreover 
53788  195 
{ 
196 
assume "Inf S = \<infinity>" 

197 
then have "S = {\<infinity>}" 

198 
by (metis Inf_eq_PInfty `S \<noteq> {}`) 

199 
then have False 

200 
by (metis assms(1) not_open_singleton) 

201 
} 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

202 
moreover 
53788  203 
{ 
204 
assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" 

205 
from ereal_open_cont_interval[OF assms(1) * fin] 

206 
obtain e where e: "e > 0" "{Inf S  e<..<Inf S + e} \<subseteq> S" . 

207 
then obtain b where b: "Inf S  e < b" "b < Inf S" 

208 
using fin ereal_between[of "Inf S" e] dense[of "Inf S  e"] 

44918  209 
by auto 
53788  210 
then have "b: {Inf S  e <..< Inf S + e}" 
211 
using e fin ereal_between[of "Inf S" e] 

212 
by auto 

213 
then have "b \<in> S" 

214 
using e by auto 

215 
then have False 

216 
using b by (metis complete_lattice_class.Inf_lower leD) 

217 
} 

218 
ultimately show False 

219 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

220 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

221 

43920  222 
lemma ereal_open_closed: 
223 
fixes S :: "ereal set" 

53788  224 
shows "open S \<and> closed S \<longleftrightarrow> S = {} \<or> S = UNIV" 
49664  225 
proof  
53788  226 
{ 
227 
assume lhs: "open S \<and> closed S" 

228 
{ 

229 
assume "\<infinity> \<notin> S" 

230 
then have "S = {}" 

231 
using lhs ereal_open_closed_aux by auto 

232 
} 

49664  233 
moreover 
53788  234 
{ 
235 
assume "\<infinity> \<in> S" 

236 
then have " S = {}" 

237 
using lhs ereal_open_closed_aux[of "S"] by auto 

238 
} 

239 
ultimately have "S = {} \<or> S = UNIV" 

240 
by auto 

241 
} 

242 
then show ?thesis 

243 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

244 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

245 

43920  246 
lemma ereal_open_affinity_pos: 
43923  247 
fixes S :: "ereal set" 
53788  248 
assumes "open S" 
249 
and m: "m \<noteq> \<infinity>" "0 < m" 

250 
and t: "\<bar>t\<bar> \<noteq> \<infinity>" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

251 
shows "open ((\<lambda>x. m * x + t) ` S)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

252 
proof  
53788  253 
obtain r where r[simp]: "m = ereal r" 
254 
using m by (cases m) auto 

255 
obtain p where p[simp]: "t = ereal p" 

256 
using t by auto 

257 
have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> \<infinity>" "m \<noteq> 0" 

258 
using m by auto 

259 
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

260 
let ?f = "(\<lambda>x. m * x + t)" 
49664  261 
show ?thesis 
262 
unfolding open_ereal_def 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

263 
proof (intro conjI impI exI subsetI) 
43920  264 
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

265 
proof safe 
49664  266 
fix x y 
267 
assume "ereal y = m * x + t" "x \<in> S" 

43920  268 
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

269 
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

270 
qed force 
43920  271 
then show "open (ereal ` ?f ` S)" 
53788  272 
using open_affinity[OF T(1) `r \<noteq> 0`] 
273 
by (auto simp: ac_simps) 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

274 
next 
49664  275 
assume "\<infinity> \<in> ?f`S" 
53788  276 
with `0 < r` have "\<infinity> \<in> S" 
277 
by auto 

49664  278 
fix x 
279 
assume "x \<in> {ereal (r * l + p)<..}" 

53788  280 
then have [simp]: "ereal (r * l + p) < x" 
281 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

282 
show "x \<in> ?f`S" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

283 
proof (rule image_eqI) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

284 
show "x = m * ((x  t) / m) + t" 
53788  285 
using m t 
286 
by (cases rule: ereal3_cases[of m x t]) auto 

287 
have "ereal l < (x  t) / m" 

288 
using m t 

289 
by (simp add: ereal_less_divide_pos ereal_less_minus) 

290 
then show "(x  t) / m \<in> S" 

291 
using T(2)[OF `\<infinity> \<in> S`] by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

292 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

293 
next 
53788  294 
assume "\<infinity> \<in> ?f ` S" 
295 
with `0 < r` have "\<infinity> \<in> S" 

296 
by auto 

43920  297 
fix x assume "x \<in> {..<ereal (r * u + p)}" 
53788  298 
then have [simp]: "x < ereal (r * u + p)" 
299 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

300 
show "x \<in> ?f`S" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

301 
proof (rule image_eqI) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

302 
show "x = m * ((x  t) / m) + t" 
53788  303 
using m t 
304 
by (cases rule: ereal3_cases[of m x t]) auto 

43920  305 
have "(x  t)/m < ereal u" 
53788  306 
using m t 
307 
by (simp add: ereal_divide_less_pos ereal_minus_less) 

308 
then show "(x  t)/m \<in> S" 

309 
using T(3)[OF `\<infinity> \<in> S`] 

310 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

311 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

312 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

313 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

314 

43920  315 
lemma ereal_open_affinity: 
43923  316 
fixes S :: "ereal set" 
49664  317 
assumes "open S" 
318 
and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0" 

319 
and t: "\<bar>t\<bar> \<noteq> \<infinity>" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

320 
shows "open ((\<lambda>x. m * x + t) ` S)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

321 
proof cases 
49664  322 
assume "0 < m" 
323 
then show ?thesis 

53788  324 
using ereal_open_affinity_pos[OF `open S` _ _ t, of m] m 
325 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

326 
next 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

327 
assume "\<not> 0 < m" then 
53788  328 
have "0 < m" 
329 
using `m \<noteq> 0` 

330 
by (cases m) auto 

331 
then have m: "m \<noteq> \<infinity>" "0 < m" 

332 
using `\<bar>m\<bar> \<noteq> \<infinity>` 

43920  333 
by (auto simp: ereal_uminus_eq_reorder) 
53788  334 
from ereal_open_affinity_pos[OF ereal_open_uminus[OF `open S`] m t] show ?thesis 
335 
unfolding image_image by simp 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

336 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

337 

43920  338 
lemma ereal_lim_mult: 
339 
fixes X :: "'a \<Rightarrow> ereal" 

49664  340 
assumes lim: "(X > L) net" 
341 
and a: "\<bar>a\<bar> \<noteq> \<infinity>" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

342 
shows "((\<lambda>i. a * X i) > a * L) net" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

343 
proof cases 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

344 
assume "a \<noteq> 0" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

345 
show ?thesis 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

346 
proof (rule topological_tendstoI) 
49664  347 
fix S 
53788  348 
assume "open S" and "a * L \<in> S" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

349 
have "a * L / a = L" 
53788  350 
using `a \<noteq> 0` a 
351 
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

352 
then have L: "L \<in> ((\<lambda>x. x / a) ` S)" 
53788  353 
using `a * L \<in> S` 
354 
by (force simp: image_iff) 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

355 
moreover have "open ((\<lambda>x. x / a) ` S)" 
43920  356 
using ereal_open_affinity[OF `open S`, of "inverse a" 0] `a \<noteq> 0` a 
357 
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

358 
note * = lim[THEN topological_tendstoD, OF this L] 
53788  359 
{ 
360 
fix x 

49664  361 
from a `a \<noteq> 0` have "a * (x / a) = x" 
53788  362 
by (cases rule: ereal2_cases[of a x]) auto 
363 
} 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

364 
note this[simp] 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

365 
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

366 
by (rule eventually_mono[OF _ *]) auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

367 
qed 
44918  368 
qed auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

369 

43920  370 
lemma ereal_lim_uminus: 
49664  371 
fixes X :: "'a \<Rightarrow> ereal" 
53788  372 
shows "((\<lambda>i.  X i) >  L) net \<longleftrightarrow> (X > L) net" 
43920  373 
using ereal_lim_mult[of X L net "ereal (1)"] 
49664  374 
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

375 
by (auto simp add: algebra_simps) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

376 

53788  377 
lemma ereal_open_atLeast: 
378 
fixes x :: ereal 

379 
shows "open {x..} \<longleftrightarrow> x = \<infinity>" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

380 
proof 
53788  381 
assume "x = \<infinity>" 
382 
then have "{x..} = UNIV" 

383 
by auto 

384 
then show "open {x..}" 

385 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

386 
next 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

387 
assume "open {x..}" 
53788  388 
then have "open {x..} \<and> closed {x..}" 
389 
by auto 

390 
then have "{x..} = UNIV" 

391 
unfolding ereal_open_closed by auto 

392 
then show "x = \<infinity>" 

393 
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

394 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

395 

53788  396 
lemma open_uminus_iff: 
397 
fixes S :: "ereal set" 

398 
shows "open (uminus ` S) \<longleftrightarrow> open S" 

399 
using ereal_open_uminus[of S] ereal_open_uminus[of "uminus ` S"] 

400 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

401 

43920  402 
lemma ereal_Liminf_uminus: 
53788  403 
fixes f :: "'a \<Rightarrow> ereal" 
404 
shows "Liminf net (\<lambda>x.  (f x)) =  Limsup net f" 

43920  405 
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

406 

43920  407 
lemma ereal_Lim_uminus: 
49664  408 
fixes f :: "'a \<Rightarrow> ereal" 
409 
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

410 
using 
43920  411 
ereal_lim_mult[of f f0 net " 1"] 
412 
ereal_lim_mult[of "\<lambda>x.  (f x)" "f0" net " 1"] 

413 
by (auto simp: ereal_uminus_reorder) 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

414 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

415 
lemma Liminf_PInfty: 
43920  416 
fixes f :: "'a \<Rightarrow> ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

417 
assumes "\<not> trivial_limit net" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

418 
shows "(f > \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>" 
53788  419 
unfolding tendsto_iff_Liminf_eq_Limsup[OF assms] 
420 
using Liminf_le_Limsup[OF assms, of f] 

421 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

422 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

423 
lemma Limsup_MInfty: 
43920  424 
fixes f :: "'a \<Rightarrow> ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

425 
assumes "\<not> trivial_limit net" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

426 
shows "(f > \<infinity>) net \<longleftrightarrow> Limsup net f = \<infinity>" 
53788  427 
unfolding tendsto_iff_Liminf_eq_Limsup[OF assms] 
428 
using Liminf_le_Limsup[OF assms, of f] 

429 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

430 

50104  431 
lemma convergent_ereal: 
53788  432 
fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder,linorder_topology}" 
50104  433 
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

434 
using tendsto_iff_Liminf_eq_Limsup[of sequentially] 
50104  435 
by (auto simp: convergent_def) 
436 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

437 
lemma liminf_PInfty: 
51351  438 
fixes X :: "nat \<Rightarrow> ereal" 
439 
shows "X > \<infinity> \<longleftrightarrow> liminf X = \<infinity>" 

49664  440 
by (metis Liminf_PInfty trivial_limit_sequentially) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

441 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

442 
lemma limsup_MInfty: 
51351  443 
fixes X :: "nat \<Rightarrow> ereal" 
444 
shows "X > \<infinity> \<longleftrightarrow> limsup X = \<infinity>" 

49664  445 
by (metis Limsup_MInfty trivial_limit_sequentially) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

446 

43920  447 
lemma ereal_lim_mono: 
53788  448 
fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology" 
449 
assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n" 

450 
and "X > x" 

451 
and "Y > y" 

452 
shows "x \<le> y" 

51000  453 
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

454 

43920  455 
lemma incseq_le_ereal: 
51351  456 
fixes X :: "nat \<Rightarrow> 'a::linorder_topology" 
53788  457 
assumes inc: "incseq X" 
458 
and lim: "X > L" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

459 
shows "X N \<le> L" 
53788  460 
using inc 
461 
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

462 

49664  463 
lemma decseq_ge_ereal: 
464 
assumes dec: "decseq X" 

51351  465 
and lim: "X > (L::'a::linorder_topology)" 
53788  466 
shows "X N \<ge> L" 
49664  467 
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

468 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

469 
lemma bounded_abs: 
53788  470 
fixes a :: real 
471 
assumes "a \<le> x" 

472 
and "x \<le> b" 

473 
shows "abs x \<le> max (abs a) (abs b)" 

49664  474 
by (metis abs_less_iff assms leI le_max_iff_disj 
475 
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

476 

43920  477 
lemma ereal_Sup_lim: 
53788  478 
fixes a :: "'a::{complete_linorder,linorder_topology}" 
479 
assumes "\<And>n. b n \<in> s" 

480 
and "b > a" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

481 
shows "a \<le> Sup s" 
49664  482 
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

483 

43920  484 
lemma ereal_Inf_lim: 
53788  485 
fixes a :: "'a::{complete_linorder,linorder_topology}" 
486 
assumes "\<And>n. b n \<in> s" 

487 
and "b > a" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

488 
shows "Inf s \<le> a" 
49664  489 
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

490 

43920  491 
lemma SUP_Lim_ereal: 
53788  492 
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}" 
493 
assumes inc: "incseq X" 

494 
and l: "X > l" 

495 
shows "(SUP n. X n) = l" 

496 
using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l] 

497 
by simp 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

498 

51351  499 
lemma INF_Lim_ereal: 
53788  500 
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}" 
501 
assumes dec: "decseq X" 

502 
and l: "X > l" 

503 
shows "(INF n. X n) = l" 

504 
using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l] 

505 
by simp 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

506 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

507 
lemma SUP_eq_LIMSEQ: 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

508 
assumes "mono f" 
43920  509 
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

510 
proof 
43920  511 
have inc: "incseq (\<lambda>i. ereal (f i))" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

512 
using `mono f` unfolding mono_def incseq_def by auto 
53788  513 
{ 
514 
assume "f > x" 

515 
then have "(\<lambda>i. ereal (f i)) > ereal x" 

516 
by auto 

517 
from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" . 

518 
next 

519 
assume "(SUP n. ereal (f n)) = ereal x" 

520 
with LIMSEQ_SUP[OF inc] show "f > x" by auto 

521 
} 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

522 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

523 

43920  524 
lemma liminf_ereal_cminus: 
49664  525 
fixes f :: "nat \<Rightarrow> ereal" 
526 
assumes "c \<noteq> \<infinity>" 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

527 
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

528 
proof (cases c) 
49664  529 
case PInf 
53788  530 
then show ?thesis 
531 
by (simp add: Liminf_const) 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

532 
next 
49664  533 
case (real r) 
534 
then show ?thesis 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

535 
unfolding liminf_SUPR_INFI limsup_INFI_SUPR 
43920  536 
apply (subst INFI_ereal_cminus) 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

537 
apply auto 
43920  538 
apply (subst SUPR_ereal_cminus) 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

539 
apply auto 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

540 
done 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

541 
qed (insert `c \<noteq> \<infinity>`, simp) 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

542 

49664  543 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

544 
subsubsection {* Continuity *} 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

545 

43920  546 
lemma continuous_at_of_ereal: 
547 
fixes x0 :: ereal 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

548 
assumes "\<bar>x0\<bar> \<noteq> \<infinity>" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

549 
shows "continuous (at x0) real" 
49664  550 
proof  
53788  551 
{ 
552 
fix T 

553 
assume T: "open T" "real x0 \<in> T" 

554 
def S \<equiv> "ereal ` T" 

555 
then have "ereal (real x0) \<in> S" 

556 
using T by auto 

557 
then have "x0 \<in> S" 

558 
using assms ereal_real by auto 

559 
moreover have "open S" 

560 
using open_ereal S_def T by auto 

561 
moreover have "\<forall>y\<in>S. real y \<in> T" 

562 
using S_def T by auto 

563 
ultimately have "\<exists>S. x0 \<in> S \<and> open S \<and> (\<forall>y\<in>S. real y \<in> T)" 

564 
by auto 

49664  565 
} 
53788  566 
then show ?thesis 
567 
unfolding continuous_at_open by blast 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

568 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

569 

43920  570 
lemma continuous_at_iff_ereal: 
53788  571 
fixes f :: "'a::t2_space \<Rightarrow> real" 
572 
shows "continuous (at x0) f \<longleftrightarrow> continuous (at x0) (ereal \<circ> f)" 

49664  573 
proof  
53788  574 
{ 
575 
assume "continuous (at x0) f" 

576 
then have "continuous (at x0) (ereal \<circ> f)" 

577 
using continuous_at_ereal continuous_at_compose[of x0 f ereal] 

578 
by auto 

49664  579 
} 
580 
moreover 

53788  581 
{ 
582 
assume "continuous (at x0) (ereal \<circ> f)" 

583 
then have "continuous (at x0) (real \<circ> (ereal \<circ> f))" 

584 
using continuous_at_of_ereal 

585 
by (intro continuous_at_compose[of x0 "ereal \<circ> f"]) auto 

586 
moreover have "real \<circ> (ereal \<circ> f) = f" 

587 
using real_ereal_id by (simp add: o_assoc) 

588 
ultimately have "continuous (at x0) f" 

589 
by auto 

590 
} 

591 
ultimately show ?thesis 

592 
by auto 

41980
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 

43920  596 
lemma continuous_on_iff_ereal: 
49664  597 
fixes f :: "'a::t2_space => real" 
53788  598 
assumes "open A" 
599 
shows "continuous_on A f \<longleftrightarrow> continuous_on A (ereal \<circ> f)" 

600 
using continuous_at_iff_ereal assms 

601 
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

602 

53788  603 
lemma continuous_on_real: "continuous_on (UNIV  {\<infinity>, \<infinity>::ereal}) real" 
604 
using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal 

605 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

606 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

607 
lemma continuous_on_iff_real: 
53788  608 
fixes f :: "'a::t2_space \<Rightarrow> ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

609 
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

610 
shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)" 
49664  611 
proof  
53788  612 
have "f ` A \<subseteq> UNIV  {\<infinity>, \<infinity>}" 
613 
using assms by force 

49664  614 
then have *: "continuous_on (f ` A) real" 
615 
using continuous_on_real by (simp add: continuous_on_subset) 

53788  616 
have **: "continuous_on ((real \<circ> f) ` A) ereal" 
617 
using continuous_on_ereal continuous_on_subset[of "UNIV" "ereal" "(real \<circ> f) ` A"] 

618 
by blast 

619 
{ 

620 
assume "continuous_on A f" 

621 
then have "continuous_on A (real \<circ> f)" 

49664  622 
apply (subst continuous_on_compose) 
53788  623 
using * 
624 
apply auto 

49664  625 
done 
626 
} 

627 
moreover 

53788  628 
{ 
629 
assume "continuous_on A (real \<circ> f)" 

630 
then have "continuous_on A (ereal \<circ> (real \<circ> f))" 

49664  631 
apply (subst continuous_on_compose) 
53788  632 
using ** 
633 
apply auto 

49664  634 
done 
635 
then have "continuous_on A f" 

53788  636 
apply (subst continuous_on_eq[of A "ereal \<circ> (real \<circ> f)" f]) 
637 
using assms ereal_real 

638 
apply auto 

49664  639 
done 
640 
} 

53788  641 
ultimately show ?thesis 
642 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

643 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

644 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

645 
lemma continuous_at_const: 
53788  646 
fixes f :: "'a::t2_space \<Rightarrow> ereal" 
647 
assumes "\<forall>x. f x = C" 

648 
shows "\<forall>x. continuous (at x) f" 

649 
unfolding continuous_at_open 

650 
using assms t1_space 

651 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

652 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

653 
lemma mono_closed_real: 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

654 
fixes S :: "real set" 
53788  655 
assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S" 
49664  656 
and "closed S" 
53788  657 
shows "S = {} \<or> S = UNIV \<or> (\<exists>a. S = {a..})" 
49664  658 
proof  
53788  659 
{ 
660 
assume "S \<noteq> {}" 

661 
{ assume ex: "\<exists>B. \<forall>x\<in>S. B \<le> x" 

662 
then have *: "\<forall>x\<in>S. Inf S \<le> x" 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

663 
using cInf_lower[of _ S] ex by (metis bdd_below_def) 
53788  664 
then have "Inf S \<in> S" 
665 
apply (subst closed_contains_Inf) 

666 
using ex `S \<noteq> {}` `closed S` 

667 
apply auto 

668 
done 

669 
then have "\<forall>x. Inf S \<le> x \<longleftrightarrow> x \<in> S" 

670 
using mono[rule_format, of "Inf S"] * 

671 
by auto 

672 
then have "S = {Inf S ..}" 

673 
by auto 

674 
then have "\<exists>a. S = {a ..}" 

675 
by auto 

49664  676 
} 
677 
moreover 

53788  678 
{ 
679 
assume "\<not> (\<exists>B. \<forall>x\<in>S. B \<le> x)" 

680 
then have nex: "\<forall>B. \<exists>x\<in>S. x < B" 

681 
by (simp add: not_le) 

682 
{ 

683 
fix y 

684 
obtain x where "x\<in>S" and "x < y" 

685 
using nex by auto 

686 
then have "y \<in> S" 

687 
using mono[rule_format, of x y] by auto 

688 
} 

689 
then have "S = UNIV" 

690 
by auto 

49664  691 
} 
53788  692 
ultimately have "S = UNIV \<or> (\<exists>a. S = {a ..})" 
693 
by blast 

694 
} 

695 
then show ?thesis 

696 
by blast 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

697 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

698 

43920  699 
lemma mono_closed_ereal: 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

700 
fixes S :: "real set" 
53788  701 
assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S" 
49664  702 
and "closed S" 
53788  703 
shows "\<exists>a. S = {x. a \<le> ereal x}" 
49664  704 
proof  
53788  705 
{ 
706 
assume "S = {}" 

707 
then have ?thesis 

708 
apply (rule_tac x=PInfty in exI) 

709 
apply auto 

710 
done 

711 
} 

49664  712 
moreover 
53788  713 
{ 
714 
assume "S = UNIV" 

715 
then have ?thesis 

716 
apply (rule_tac x="\<infinity>" in exI) 

717 
apply auto 

718 
done 

719 
} 

49664  720 
moreover 
53788  721 
{ 
722 
assume "\<exists>a. S = {a ..}" 

723 
then obtain a where "S = {a ..}" 

724 
by auto 

725 
then have ?thesis 

726 
apply (rule_tac x="ereal a" in exI) 

727 
apply auto 

728 
done 

49664  729 
} 
53788  730 
ultimately show ?thesis 
731 
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

732 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

733 

53788  734 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

735 
subsection {* Sums *} 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

736 

49664  737 
lemma setsum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)" 
53788  738 
proof (cases "finite A") 
739 
case True 

49664  740 
then show ?thesis by induct auto 
53788  741 
next 
742 
case False 

743 
then show ?thesis by simp 

744 
qed 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

745 

43923  746 
lemma setsum_Pinfty: 
747 
fixes f :: "'a \<Rightarrow> ereal" 

53788  748 
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

749 
proof safe 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

750 
assume *: "setsum f P = \<infinity>" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

751 
show "finite P" 
53788  752 
proof (rule ccontr) 
753 
assume "infinite P" 

754 
with * show False 

755 
by auto 

756 
qed 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

757 
show "\<exists>i\<in>P. f i = \<infinity>" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

758 
proof (rule ccontr) 
53788  759 
assume "\<not> ?thesis" 
760 
then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>" 

761 
by auto 

762 
with `finite P` have "setsum f P \<noteq> \<infinity>" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

763 
by induct auto 
53788  764 
with * show False 
765 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

766 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

767 
next 
53788  768 
fix i 
769 
assume "finite P" and "i \<in> P" and "f i = \<infinity>" 

49664  770 
then show "setsum f P = \<infinity>" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

771 
proof induct 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

772 
case (insert x A) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

773 
show ?case using insert by (cases "x = i") auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

774 
qed simp 
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 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

777 
lemma setsum_Inf: 
43923  778 
fixes f :: "'a \<Rightarrow> ereal" 
53788  779 
shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

780 
proof 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

781 
assume *: "\<bar>setsum f A\<bar> = \<infinity>" 
53788  782 
have "finite A" 
783 
by (rule ccontr) (insert *, auto) 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

784 
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

785 
proof (rule ccontr) 
53788  786 
assume "\<not> ?thesis" 
787 
then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" 

788 
by auto 

789 
from bchoice[OF this] obtain r where "\<forall>x\<in>A. f x = ereal (r x)" .. 

790 
with * show False 

791 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

792 
qed 
53788  793 
ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" 
794 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

795 
next 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

796 
assume "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" 
53788  797 
then obtain i where "finite A" "i \<in> A" and "\<bar>f i\<bar> = \<infinity>" 
798 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

799 
then show "\<bar>setsum f A\<bar> = \<infinity>" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

800 
proof induct 
53788  801 
case (insert j A) 
802 
then show ?case 

43920  803 
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

804 
qed simp 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

805 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

806 

43920  807 
lemma setsum_real_of_ereal: 
43923  808 
fixes f :: "'i \<Rightarrow> ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

809 
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

810 
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

811 
proof  
43920  812 
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

813 
proof 
53788  814 
fix x 
815 
assume "x \<in> S" 

816 
from assms[OF this] show "\<exists>r. f x = ereal r" 

817 
by (cases "f x") auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

818 
qed 
53788  819 
from bchoice[OF this] obtain r where "\<forall>x\<in>S. f x = ereal (r x)" .. 
820 
then show ?thesis 

821 
by simp 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

822 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

823 

43920  824 
lemma setsum_ereal_0: 
53788  825 
fixes f :: "'a \<Rightarrow> ereal" 
826 
assumes "finite A" 

827 
and "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

828 
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

829 
proof 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

830 
assume *: "(\<Sum>x\<in>A. f x) = 0" 
53788  831 
then have "(\<Sum>x\<in>A. f x) \<noteq> \<infinity>" 
832 
by auto 

833 
then have "\<forall>i\<in>A. \<bar>f i\<bar> \<noteq> \<infinity>" 

834 
using assms by (force simp: setsum_Pinfty) 

835 
then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" 

836 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

837 
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

838 
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

839 
qed (rule setsum_0') 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

840 

43920  841 
lemma setsum_ereal_right_distrib: 
49664  842 
fixes f :: "'a \<Rightarrow> ereal" 
843 
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

844 
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

845 
proof cases 
49664  846 
assume "finite A" 
847 
then show ?thesis using assms 

43920  848 
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

849 
qed simp 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

850 

43920  851 
lemma sums_ereal_positive: 
49664  852 
fixes f :: "nat \<Rightarrow> ereal" 
853 
assumes "\<And>i. 0 \<le> f i" 

854 
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

855 
proof  
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

856 
have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)" 
53788  857 
using ereal_add_mono[OF _ assms] 
858 
by (auto intro!: incseq_SucI) 

51000  859 
from LIMSEQ_SUP[OF this] 
53788  860 
show ?thesis unfolding sums_def 
861 
by (simp add: atLeast0LessThan) 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

862 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

863 

43920  864 
lemma summable_ereal_pos: 
49664  865 
fixes f :: "nat \<Rightarrow> ereal" 
866 
assumes "\<And>i. 0 \<le> f i" 

867 
shows "summable f" 

53788  868 
using sums_ereal_positive[of f, OF assms] 
869 
unfolding summable_def 

870 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

871 

43920  872 
lemma suminf_ereal_eq_SUPR: 
49664  873 
fixes f :: "nat \<Rightarrow> ereal" 
874 
assumes "\<And>i. 0 \<le> f i" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

875 
shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)" 
53788  876 
using sums_ereal_positive[of f, OF assms, THEN sums_unique] 
877 
by simp 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

878 

49664  879 
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

880 
unfolding sums_def by simp 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

881 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

882 
lemma suminf_bound: 
43920  883 
fixes f :: "nat \<Rightarrow> ereal" 
53788  884 
assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x" 
885 
and pos: "\<And>n. 0 \<le> f n" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

886 
shows "suminf f \<le> x" 
43920  887 
proof (rule Lim_bounded_ereal) 
888 
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

889 
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

890 
by (auto dest!: summable_sums simp: sums_def atLeast0LessThan) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

891 
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

892 
using assms by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

893 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

894 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

895 
lemma suminf_bound_add: 
43920  896 
fixes f :: "nat \<Rightarrow> ereal" 
49664  897 
assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x" 
898 
and pos: "\<And>n. 0 \<le> f n" 

899 
and "y \<noteq> \<infinity>" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

900 
shows "suminf f + y \<le> x" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

901 
proof (cases y) 
49664  902 
case (real r) 
903 
then have "\<forall>N. (\<Sum>n<N. f n) \<le> x  y" 

43920  904 
using assms by (simp add: ereal_le_minus) 
53788  905 
then have "(\<Sum> n. f n) \<le> x  y" 
906 
using pos by (rule suminf_bound) 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

907 
then show "(\<Sum> n. f n) + y \<le> x" 
43920  908 
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

909 
qed (insert assms, auto) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

910 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

911 
lemma suminf_upper: 
49664  912 
fixes f :: "nat \<Rightarrow> ereal" 
913 
assumes "\<And>n. 0 \<le> f n" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

914 
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

915 
unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def 
45031  916 
by (auto intro: complete_lattice_class.Sup_upper) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

917 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

918 
lemma suminf_0_le: 
49664  919 
fixes f :: "nat \<Rightarrow> ereal" 
920 
assumes "\<And>n. 0 \<le> f n" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

921 
shows "0 \<le> (\<Sum>n. f n)" 
53788  922 
using suminf_upper[of f 0, OF assms] 
923 
by simp 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

924 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

925 
lemma suminf_le_pos: 
43920  926 
fixes f g :: "nat \<Rightarrow> ereal" 
53788  927 
assumes "\<And>N. f N \<le> g N" 
928 
and "\<And>N. 0 \<le> f N" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

929 
shows "suminf f \<le> suminf g" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

930 
proof (safe intro!: suminf_bound) 
49664  931 
fix n 
53788  932 
{ 
933 
fix N 

934 
have "0 \<le> g N" 

935 
using assms(2,1)[of N] by auto 

936 
} 

49664  937 
have "setsum f {..<n} \<le> setsum g {..<n}" 
938 
using assms by (auto intro: setsum_mono) 

53788  939 
also have "\<dots> \<le> suminf g" 
940 
using `\<And>N. 0 \<le> g N` 

941 
by (rule suminf_upper) 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

942 
finally show "setsum f {..<n} \<le> suminf g" . 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

943 
qed (rule assms(2)) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

944 

53788  945 
lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal) ^ Suc n) = 1" 
43920  946 
using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric] 
947 
by (simp add: one_ereal_def) 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

948 

43920  949 
lemma suminf_add_ereal: 
950 
fixes f g :: "nat \<Rightarrow> ereal" 

53788  951 
assumes "\<And>i. 0 \<le> f i" 
952 
and "\<And>i. 0 \<le> g i" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

953 
shows "(\<Sum>i. f i + g i) = suminf f + suminf g" 
43920  954 
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

955 
unfolding setsum_addf 
49664  956 
apply (intro assms ereal_add_nonneg_nonneg SUPR_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+ 
957 
done 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

958 

43920  959 
lemma suminf_cmult_ereal: 
960 
fixes f g :: "nat \<Rightarrow> ereal" 

53788  961 
assumes "\<And>i. 0 \<le> f i" 
962 
and "0 \<le> a" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

963 
shows "(\<Sum>i. a * f i) = a * suminf f" 
43920  964 
by (auto simp: setsum_ereal_right_distrib[symmetric] assms 
53788  965 
ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUPR 
966 
intro!: SUPR_ereal_cmult ) 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

967 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

968 
lemma suminf_PInfty: 
43923  969 
fixes f :: "nat \<Rightarrow> ereal" 
53788  970 
assumes "\<And>i. 0 \<le> f i" 
971 
and "suminf f \<noteq> \<infinity>" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

972 
shows "f i \<noteq> \<infinity>" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

973 
proof  
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

974 
from suminf_upper[of f "Suc i", OF assms(1)] assms(2) 
53788  975 
have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>" 
976 
by auto 

977 
then show ?thesis 

978 
unfolding setsum_Pinfty by simp 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

979 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

980 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

981 
lemma suminf_PInfty_fun: 
53788  982 
assumes "\<And>i. 0 \<le> f i" 
983 
and "suminf f \<noteq> \<infinity>" 

43920  984 
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

985 
proof  
43920  986 
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

987 
proof 
53788  988 
fix i 
989 
show "\<exists>r. f i = ereal r" 

990 
using suminf_PInfty[OF assms] assms(1)[of i] 

991 
by (cases "f i") auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

992 
qed 
53788  993 
from choice[OF this] show ?thesis 
994 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

995 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

996 

43920  997 
lemma summable_ereal: 
53788  998 
assumes "\<And>i. 0 \<le> f i" 
999 
and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1000 
shows "summable f" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1001 
proof  
43920  1002 
have "0 \<le> (\<Sum>i. ereal (f i))" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1003 
using assms by (intro suminf_0_le) auto 
43920  1004 
with assms obtain r where r: "(\<Sum>i. ereal (f i)) = ereal r" 
1005 
by (cases "\<Sum>i. ereal (f i)") auto 

1006 
from summable_ereal_pos[of "\<lambda>x. ereal (f x)"] 

53788  1007 
have "summable (\<lambda>x. ereal (f x))" 
1008 
using assms by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1009 
from summable_sums[OF this] 
53788  1010 
have "(\<lambda>x. ereal (f x)) sums (\<Sum>x. ereal (f x))" 
1011 
by auto 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1012 
then show "summable f" 
43920  1013 
unfolding r sums_ereal summable_def .. 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1014 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1015 

43920  1016 
lemma suminf_ereal: 
53788  1017 
assumes "\<And>i. 0 \<le> f i" 
1018 
and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>" 

43920  1019 
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

1020 
proof (rule sums_unique[symmetric]) 
43920  1021 
from summable_ereal[OF assms] 
1022 
show "(\<lambda>x. ereal (f x)) sums (ereal (suminf f))" 

53788  1023 
unfolding sums_ereal 
1024 
using assms 

1025 
by (intro summable_sums summable_ereal) 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1026 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1027 

43920  1028 
lemma suminf_ereal_minus: 
1029 
fixes f g :: "nat \<Rightarrow> ereal" 

53788  1030 
assumes ord: "\<And>i. g i \<le> f i" "\<And>i. 0 \<le> g i" 
1031 
and fin: "suminf f \<noteq> \<infinity>" "suminf g \<noteq> \<infinity>" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1032 
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

1033 
proof  
53788  1034 
{ 
1035 
fix i 

1036 
have "0 \<le> f i" 

1037 
using ord[of i] by auto 

1038 
} 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1039 
moreover 
53788  1040 
from suminf_PInfty_fun[OF `\<And>i. 0 \<le> f i` fin(1)] obtain f' where [simp]: "f = (\<lambda>x. ereal (f' x))" .. 
1041 
from suminf_PInfty_fun[OF `\<And>i. 0 \<le> g i` fin(2)] obtain g' where [simp]: "g = (\<lambda>x. ereal (g' x))" .. 

1042 
{ 

1043 
fix i 

1044 
have "0 \<le> f i  g i" 

1045 
using ord[of i] by (auto simp: ereal_le_minus_iff) 

1046 
} 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1047 
moreover 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1048 
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

1049 
using assms by (auto intro!: suminf_le_pos simp: field_simps) 
53788  1050 
then have "suminf (\<lambda>i. f i  g i) \<noteq> \<infinity>" 
1051 
using fin by auto 

1052 
ultimately show ?thesis 

1053 
using assms `\<And>i. 0 \<le> f i` 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1054 
apply simp 
49664  1055 
apply (subst (1 2 3) suminf_ereal) 
1056 
apply (auto intro!: suminf_diff[symmetric] summable_ereal) 

1057 
done 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1058 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1059 

49664  1060 
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

1061 
proof  
53788  1062 
have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)" 
1063 
by (rule suminf_upper) auto 

1064 
then show ?thesis 

1065 
by simp 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1066 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1067 

43920  1068 
lemma summable_real_of_ereal: 
43923  1069 
fixes f :: "nat \<Rightarrow> ereal" 
49664  1070 
assumes f: "\<And>i. 0 \<le> f i" 
1071 
and fin: "(\<Sum>i. f i) \<noteq> \<infinity>" 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1072 
shows "summable (\<lambda>i. real (f i))" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1073 
proof (rule summable_def[THEN iffD2]) 
53788  1074 
have "0 \<le> (\<Sum>i. f i)" 
1075 
using assms by (auto intro: suminf_0_le) 

1076 
with fin obtain r where r: "ereal r = (\<Sum>i. f i)" 

1077 
by (cases "(\<Sum>i. f i)") auto 

1078 
{ 

1079 
fix i 

1080 
have "f i \<noteq> \<infinity>" 

1081 
using f by (intro suminf_PInfty[OF _ fin]) auto 

1082 
then have "\<bar>f i\<bar> \<noteq> \<infinity>" 

1083 
using f[of i] by auto 

1084 
} 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1085 
note fin = this 
43920  1086 
have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))" 
53788  1087 
using f 
1088 
by (auto intro!: summable_ereal_pos summable_sums simp: ereal_le_real_iff zero_ereal_def) 

1089 
also have "\<dots> = ereal r" 

1090 
using fin r by (auto simp: ereal_real) 

1091 
finally show "\<exists>r. (\<lambda>i. real (f i)) sums r" 

1092 
by (auto simp: sums_ereal) 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1093 
qed 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1094 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

1095 
lemma suminf_SUP_eq: 
43920  1096 
fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ereal" 
53788  1097 
assumes "\<And>i. incseq (\<lambda>n. f n i)" 
1098 
and "\<And>n i. 0 \<le> f n i" 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

1099 
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

1100 
proof  
53788  1101 
{ 
1102 
fix n :: nat 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

1103 
have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)" 
53788  1104 
using assms 
1105 
by (auto intro!: SUPR_ereal_setsum[symmetric]) 

1106 
} 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

1107 
note * = this 
53788  1108 
show ?thesis 
1109 
using assms 

43920  1110 
apply (subst (1 2) suminf_ereal_eq_SUPR) 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

1111 
unfolding * 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44918
diff
changeset

1112 
apply (auto intro!: SUP_upper2) 
49664  1113 
apply (subst SUP_commute) 
1114 
apply rule 

1115 
done 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

1116 
qed 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

1117 

47761  1118 
lemma suminf_setsum_ereal: 
1119 
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal" 

1120 
assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a" 

1121 
shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)" 

53788  1122 
proof (cases "finite A") 
1123 
case True 

1124 
then show ?thesis 

1125 
using nonneg 

47761  1126 
by induct (simp_all add: suminf_add_ereal setsum_nonneg) 
53788  1127 
next 
1128 
case False 

1129 
then show ?thesis by simp 

1130 
qed 

47761  1131 

50104  1132 
lemma suminf_ereal_eq_0: 
1133 
fixes f :: "nat \<Rightarrow> ereal" 

1134 
assumes nneg: "\<And>i. 0 \<le> f i" 

1135 
shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)" 

1136 
proof 

1137 
assume "(\<Sum>i. f i) = 0" 

53788  1138 
{ 
1139 
fix i 

1140 
assume "f i \<noteq> 0" 

1141 
with nneg have "0 < f i" 

1142 
by (auto simp: less_le) 

50104  1143 
also have "f i = (\<Sum>j. if j = i then f i else 0)" 
1144 
by (subst suminf_finite[where N="{i}"]) auto 

1145 
also have "\<dots> \<le> (\<Sum>i. f i)" 

53788  1146 
using nneg 
1147 
by (auto intro!: suminf_le_pos) 

1148 
finally have False 

1149 
using `(\<Sum>i. f i) = 0` by auto 

1150 
} 

1151 
then show "\<forall>i. f i = 0" 

1152 
by auto 

50104  1153 
qed simp 
1154 

51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset

1155 
lemma Liminf_within: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset

1156 
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

1157 
shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e  {x}). f y)" 
51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51530
diff
changeset

1158 
unfolding Liminf_def eventually_at 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset

1159 
proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe) 
53788  1160 
fix P d 
1161 
assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y" 

51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset

1162 
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

1163 
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

1164 
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

1165 
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

1166 
next 
53788  1167 
fix d :: real 
1168 
assume "0 < d" 

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

1169 
then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and> 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset

1170 
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

1171 
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

1172 
(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

1173 
qed 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset

1174 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset

1175 
lemma Limsup_within: 
53788  1176 
fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice" 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset

1177 
shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e  {x}). f y)" 
51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51530
diff
changeset

1178 
unfolding Limsup_def eventually_at 
51340 