author | hoelzl |
Mon, 14 Mar 2011 14:37:49 +0100 | |
changeset 41981 | cdf7693bbe08 |
parent 41980 | 28b51effc5ed |
child 41983 | 2dc6e382a58b |
permissions | -rw-r--r-- |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1 |
(* Title: src/HOL/Multivariate_Analysis/Extended_Reals.thy |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
2 |
Author: Johannes Hölzl; TU München |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
3 |
Author: Robert Himmelmann; TU München |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
4 |
Author: Armin Heller; TU München |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
5 |
Author: Bogdan Grechuk; University of Edinburgh *) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
6 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
7 |
header {* Limits on the Extended real number line *} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
8 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
9 |
theory Extended_Real_Limits |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
10 |
imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Reals" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
11 |
begin |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
12 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
13 |
lemma continuous_on_extreal[intro, simp]: "continuous_on A extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
14 |
unfolding continuous_on_topological open_extreal_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
15 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
16 |
lemma continuous_at_extreal[intro, simp]: "continuous (at x) extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
17 |
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
|
18 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
19 |
lemma continuous_within_extreal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
20 |
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
|
21 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
22 |
lemma extreal_open_uminus: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
23 |
fixes S :: "extreal set" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
24 |
assumes "open S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
25 |
shows "open (uminus ` S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
26 |
unfolding open_extreal_def |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
27 |
proof (intro conjI impI) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
28 |
obtain x y where S: "open (extreal -` S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
29 |
"\<infinity> \<in> S \<Longrightarrow> {extreal x<..} \<subseteq> S" "-\<infinity> \<in> S \<Longrightarrow> {..< extreal y} \<subseteq> S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
30 |
using `open S` unfolding open_extreal_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
31 |
have "extreal -` uminus ` S = uminus ` (extreal -` S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
32 |
proof safe |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
33 |
fix x y assume "extreal x = - y" "y \<in> S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
34 |
then show "x \<in> uminus ` extreal -` S" by (cases y) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
35 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
36 |
fix x assume "extreal x \<in> S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
37 |
then show "- x \<in> extreal -` uminus ` S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
38 |
by (auto intro: image_eqI[of _ _ "extreal x"]) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
39 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
40 |
then show "open (extreal -` uminus ` S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
41 |
using S by (auto intro: open_negations) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
42 |
{ assume "\<infinity> \<in> uminus ` S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
43 |
then have "-\<infinity> \<in> S" by (metis image_iff extreal_uminus_uminus) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
44 |
then have "uminus ` {..<extreal y} \<subseteq> uminus ` S" using S by (intro image_mono) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
45 |
then show "\<exists>x. {extreal x<..} \<subseteq> uminus ` S" using extreal_uminus_lessThan by auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
46 |
{ assume "-\<infinity> \<in> uminus ` S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
47 |
then have "\<infinity> : S" by (metis image_iff extreal_uminus_uminus) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
48 |
then have "uminus ` {extreal x<..} <= uminus ` S" using S by (intro image_mono) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
49 |
then show "\<exists>y. {..<extreal y} <= uminus ` S" using extreal_uminus_greaterThan by auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
50 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
51 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
52 |
lemma extreal_uminus_complement: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
53 |
fixes S :: "extreal set" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
54 |
shows "uminus ` (- S) = - uminus ` S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
55 |
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
|
56 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
57 |
lemma extreal_closed_uminus: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
58 |
fixes S :: "extreal set" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
59 |
assumes "closed S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
60 |
shows "closed (uminus ` S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
61 |
using assms unfolding closed_def |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
62 |
using extreal_open_uminus[of "- S"] extreal_uminus_complement by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
63 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
64 |
lemma not_open_extreal_singleton: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
65 |
"\<not> (open {a :: extreal})" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
66 |
proof(rule ccontr) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
67 |
assume "\<not> \<not> open {a}" hence a: "open {a}" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
68 |
show False |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
69 |
proof (cases a) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
70 |
case MInf |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
71 |
then obtain y where "{..<extreal y} <= {a}" using a open_MInfty2[of "{a}"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
72 |
hence "extreal(y - 1):{a}" apply (subst subsetD[of "{..<extreal y}"]) by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
73 |
then show False using `a=(-\<infinity>)` by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
74 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
75 |
case PInf |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
76 |
then obtain y where "{extreal y<..} <= {a}" using a open_PInfty2[of "{a}"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
77 |
hence "extreal(y+1):{a}" apply (subst subsetD[of "{extreal y<..}"]) by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
78 |
then show False using `a=\<infinity>` by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
79 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
80 |
case (real r) then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
81 |
from extreal_open_cont_interval[OF a singletonI this] guess e . note e = this |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
82 |
then obtain b where b_def: "a<b & b<a+e" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
83 |
using fin extreal_between extreal_dense[of a "a+e"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
84 |
then have "b: {a-e <..< a+e}" using fin extreal_between[of a e] e by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
85 |
then show False using b_def e by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
86 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
87 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
88 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
89 |
lemma extreal_closed_contains_Inf: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
90 |
fixes S :: "extreal set" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
91 |
assumes "closed S" "S ~= {}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
92 |
shows "Inf S : S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
93 |
proof(rule ccontr) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
94 |
assume "Inf S \<notin> S" hence a: "open (-S)" "Inf S:(- S)" using assms by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
95 |
show False |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
96 |
proof (cases "Inf S") |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
97 |
case MInf hence "(-\<infinity>) : - S" using a by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
98 |
then obtain y where "{..<extreal y} <= (-S)" using a open_MInfty2[of "- S"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
99 |
hence "extreal y <= Inf S" by (metis Compl_anti_mono Compl_lessThan atLeast_iff |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
100 |
complete_lattice_class.Inf_greatest double_complement set_rev_mp) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
101 |
then show False using MInf by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
102 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
103 |
case PInf then have "S={\<infinity>}" by (metis Inf_eq_PInfty assms(2)) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
104 |
then show False by (metis `Inf S ~: S` insert_code mem_def PInf) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
105 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
106 |
case (real r) then have fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
107 |
from extreal_open_cont_interval[OF a this] guess e . note e = this |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
108 |
{ fix x assume "x:S" hence "x>=Inf S" by (rule complete_lattice_class.Inf_lower) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
109 |
hence *: "x>Inf S-e" using e by (metis fin extreal_between(1) order_less_le_trans) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
110 |
{ assume "x<Inf S+e" hence "x:{Inf S-e <..< Inf S+e}" using * by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
111 |
hence False using e `x:S` by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
112 |
} hence "x>=Inf S+e" by (metis linorder_le_less_linear) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
113 |
} hence "Inf S + e <= Inf S" by (metis le_Inf_iff) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
114 |
then show False using real e by (cases e) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
115 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
116 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
117 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
118 |
lemma extreal_closed_contains_Sup: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
119 |
fixes S :: "extreal set" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
120 |
assumes "closed S" "S ~= {}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
121 |
shows "Sup S : S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
122 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
123 |
have "closed (uminus ` S)" by (metis assms(1) extreal_closed_uminus) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
124 |
hence "Inf (uminus ` S) : uminus ` S" using assms extreal_closed_contains_Inf[of "uminus ` S"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
125 |
hence "- Sup S : uminus ` S" using extreal_Sup_uminus_image_eq[of "uminus ` S"] by (auto simp: image_image) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
126 |
thus ?thesis by (metis imageI extreal_uminus_uminus extreal_minus_minus_image) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
127 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
128 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
129 |
lemma extreal_open_closed_aux: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
130 |
fixes S :: "extreal set" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
131 |
assumes "open S" "closed S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
132 |
assumes S: "(-\<infinity>) ~: S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
133 |
shows "S = {}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
134 |
proof(rule ccontr) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
135 |
assume "S ~= {}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
136 |
hence *: "(Inf S):S" by (metis assms(2) extreal_closed_contains_Inf) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
137 |
{ assume "Inf S=(-\<infinity>)" hence False using * assms(3) by auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
138 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
139 |
{ assume "Inf S=\<infinity>" hence "S={\<infinity>}" by (metis Inf_eq_PInfty `S ~= {}`) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
140 |
hence False by (metis assms(1) not_open_extreal_singleton) } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
141 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
142 |
{ assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
143 |
from extreal_open_cont_interval[OF assms(1) * fin] guess e . note e = this |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
144 |
then obtain b where b_def: "Inf S-e<b & b<Inf S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
145 |
using fin extreal_between[of "Inf S" e] extreal_dense[of "Inf S-e"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
146 |
hence "b: {Inf S-e <..< Inf S+e}" using e fin extreal_between[of "Inf S" e] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
147 |
hence "b:S" using e by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
148 |
hence False using b_def by (metis complete_lattice_class.Inf_lower leD) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
149 |
} ultimately show False by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
150 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
151 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
152 |
lemma extreal_open_closed: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
153 |
fixes S :: "extreal set" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
154 |
shows "(open S & closed S) <-> (S = {} | S = UNIV)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
155 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
156 |
{ assume lhs: "open S & closed S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
157 |
{ assume "(-\<infinity>) ~: S" hence "S={}" using lhs extreal_open_closed_aux by auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
158 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
159 |
{ assume "(-\<infinity>) : S" hence "(- S)={}" using lhs extreal_open_closed_aux[of "-S"] by auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
160 |
ultimately have "S = {} | S = UNIV" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
161 |
} thus ?thesis by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
162 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
163 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
164 |
lemma extreal_open_affinity_pos: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
165 |
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
|
166 |
shows "open ((\<lambda>x. m * x + t) ` S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
167 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
168 |
obtain r where r[simp]: "m = extreal r" using m by (cases m) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
169 |
obtain p where p[simp]: "t = extreal p" using t by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
170 |
have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0" using m by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
171 |
from `open S`[THEN extreal_openE] guess l u . note T = this |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
172 |
let ?f = "(\<lambda>x. m * x + t)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
173 |
show ?thesis unfolding open_extreal_def |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
174 |
proof (intro conjI impI exI subsetI) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
175 |
have "extreal -` ?f ` S = (\<lambda>x. r * x + p) ` (extreal -` S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
176 |
proof safe |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
177 |
fix x y assume "extreal y = m * x + t" "x \<in> S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
178 |
then show "y \<in> (\<lambda>x. r * x + p) ` extreal -` S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
179 |
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
|
180 |
qed force |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
181 |
then show "open (extreal -` ?f ` S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
182 |
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
|
183 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
184 |
assume "\<infinity> \<in> ?f`S" with `0 < r` have "\<infinity> \<in> S" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
185 |
fix x assume "x \<in> {extreal (r * l + p)<..}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
186 |
then have [simp]: "extreal (r * l + p) < x" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
187 |
show "x \<in> ?f`S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
188 |
proof (rule image_eqI) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
189 |
show "x = m * ((x - t) / m) + t" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
190 |
using m t by (cases rule: extreal3_cases[of m x t]) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
191 |
have "extreal l < (x - t)/m" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
192 |
using m t by (simp add: extreal_less_divide_pos extreal_less_minus) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
193 |
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
|
194 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
195 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
196 |
assume "-\<infinity> \<in> ?f`S" with `0 < r` have "-\<infinity> \<in> S" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
197 |
fix x assume "x \<in> {..<extreal (r * u + p)}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
198 |
then have [simp]: "x < extreal (r * u + p)" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
199 |
show "x \<in> ?f`S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
200 |
proof (rule image_eqI) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
201 |
show "x = m * ((x - t) / m) + t" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
202 |
using m t by (cases rule: extreal3_cases[of m x t]) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
203 |
have "(x - t)/m < extreal u" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
204 |
using m t by (simp add: extreal_divide_less_pos extreal_minus_less) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
205 |
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
|
206 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
207 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
208 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
209 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
210 |
lemma extreal_open_affinity: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
211 |
assumes "open S" and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0" and t: "\<bar>t\<bar> \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
212 |
shows "open ((\<lambda>x. m * x + t) ` S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
213 |
proof cases |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
214 |
assume "0 < m" then show ?thesis |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
215 |
using extreal_open_affinity_pos[OF `open S` _ _ t, of m] m by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
216 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
217 |
assume "\<not> 0 < m" then |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
218 |
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
|
219 |
then have m: "-m \<noteq> \<infinity>" "0 < -m" using `\<bar>m\<bar> \<noteq> \<infinity>` |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
220 |
by (auto simp: extreal_uminus_eq_reorder) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
221 |
from extreal_open_affinity_pos[OF extreal_open_uminus[OF `open S`] m t] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
222 |
show ?thesis unfolding image_image by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
223 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
224 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
225 |
lemma extreal_lim_mult: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
226 |
fixes X :: "'a \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
227 |
assumes lim: "(X ---> L) net" and a: "\<bar>a\<bar> \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
228 |
shows "((\<lambda>i. a * X i) ---> a * L) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
229 |
proof cases |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
230 |
assume "a \<noteq> 0" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
231 |
show ?thesis |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
232 |
proof (rule topological_tendstoI) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
233 |
fix S assume "open S" "a * L \<in> S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
234 |
have "a * L / a = L" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
235 |
using `a \<noteq> 0` a by (cases rule: extreal2_cases[of a L]) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
236 |
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
|
237 |
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
|
238 |
moreover have "open ((\<lambda>x. x / a) ` S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
239 |
using extreal_open_affinity[OF `open S`, of "inverse a" 0] `a \<noteq> 0` a |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
240 |
by (auto simp: extreal_divide_eq extreal_inverse_eq_0 divide_extreal_def ac_simps) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
241 |
note * = lim[THEN topological_tendstoD, OF this L] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
242 |
{ fix x from a `a \<noteq> 0` have "a * (x / a) = x" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
243 |
by (cases rule: extreal2_cases[of a x]) auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
244 |
note this[simp] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
245 |
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
|
246 |
by (rule eventually_mono[OF _ *]) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
247 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
248 |
qed auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
249 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
250 |
lemma extreal_lim_uminus: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
251 |
fixes X :: "'a \<Rightarrow> extreal" shows "((\<lambda>i. - X i) ---> -L) net \<longleftrightarrow> (X ---> L) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
252 |
using extreal_lim_mult[of X L net "extreal (-1)"] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
253 |
extreal_lim_mult[of "(\<lambda>i. - X i)" "-L" net "extreal (-1)"] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
254 |
by (auto simp add: algebra_simps) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
255 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
256 |
lemma Lim_bounded2_extreal: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
257 |
assumes lim:"f ----> (l :: extreal)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
258 |
and ge: "ALL n>=N. f n >= C" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
259 |
shows "l>=C" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
260 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
261 |
def g == "(%i. -(f i))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
262 |
{ fix n assume "n>=N" hence "g n <= -C" using assms extreal_minus_le_minus g_def by auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
263 |
hence "ALL n>=N. g n <= -C" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
264 |
moreover have limg: "g ----> (-l)" using g_def extreal_lim_uminus lim by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
265 |
ultimately have "-l <= -C" using Lim_bounded_extreal[of g "-l" _ "-C"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
266 |
from this show ?thesis using extreal_minus_le_minus by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
267 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
268 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
269 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
270 |
lemma extreal_open_atLeast: "open {x..} \<longleftrightarrow> x = -\<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
271 |
proof |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
272 |
assume "x = -\<infinity>" then have "{x..} = UNIV" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
273 |
then show "open {x..}" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
274 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
275 |
assume "open {x..}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
276 |
then have "open {x..} \<and> closed {x..}" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
277 |
then have "{x..} = UNIV" unfolding extreal_open_closed by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
278 |
then show "x = -\<infinity>" by (simp add: bot_extreal_def atLeast_eq_UNIV_iff) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
279 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
280 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
281 |
lemma extreal_open_mono_set: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
282 |
fixes S :: "extreal set" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
283 |
defines "a \<equiv> Inf S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
284 |
shows "(open S \<and> mono S) \<longleftrightarrow> (S = UNIV \<or> S = {a <..})" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
285 |
by (metis Inf_UNIV a_def atLeast_eq_UNIV_iff extreal_open_atLeast |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
286 |
extreal_open_closed mono_set_iff open_extreal_greaterThan) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
287 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
288 |
lemma extreal_closed_mono_set: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
289 |
fixes S :: "extreal set" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
290 |
shows "(closed S \<and> mono S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
291 |
by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_extreal_atLeast |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
292 |
extreal_open_closed mono_empty mono_set_iff open_extreal_greaterThan) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
293 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
294 |
lemma extreal_Liminf_Sup_monoset: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
295 |
fixes f :: "'a => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
296 |
shows "Liminf net f = Sup {l. \<forall>S. open S \<longrightarrow> mono S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
297 |
unfolding Liminf_Sup |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
298 |
proof (intro arg_cong[where f="\<lambda>P. Sup (Collect P)"] ext iffI allI impI) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
299 |
fix l S assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono S" "l \<in> S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
300 |
then have "S = UNIV \<or> S = {Inf S <..}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
301 |
using extreal_open_mono_set[of S] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
302 |
then show "eventually (\<lambda>x. f x \<in> S) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
303 |
proof |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
304 |
assume S: "S = {Inf S<..}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
305 |
then have "Inf S < l" using `l \<in> S` by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
306 |
then have "eventually (\<lambda>x. Inf S < f x) net" using ev by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
307 |
then show "eventually (\<lambda>x. f x \<in> S) net" by (subst S) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
308 |
qed auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
309 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
310 |
fix l y assume S: "\<forall>S. open S \<longrightarrow> mono S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net" "y < l" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
311 |
have "eventually (\<lambda>x. f x \<in> {y <..}) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
312 |
using `y < l` by (intro S[rule_format]) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
313 |
then show "eventually (\<lambda>x. y < f x) net" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
314 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
315 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
316 |
lemma extreal_Limsup_Inf_monoset: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
317 |
fixes f :: "'a => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
318 |
shows "Limsup net f = Inf {l. \<forall>S. open S \<longrightarrow> mono (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
319 |
unfolding Limsup_Inf |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
320 |
proof (intro arg_cong[where f="\<lambda>P. Inf (Collect P)"] ext iffI allI impI) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
321 |
fix l S assume ev: "\<forall>y>l. eventually (\<lambda>x. f x < y) net" and "open S" "mono (uminus`S)" "l \<in> S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
322 |
then have "open (uminus`S) \<and> mono (uminus`S)" by (simp add: extreal_open_uminus) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
323 |
then have "S = UNIV \<or> S = {..< Sup S}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
324 |
unfolding extreal_open_mono_set extreal_Inf_uminus_image_eq extreal_image_uminus_shift by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
325 |
then show "eventually (\<lambda>x. f x \<in> S) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
326 |
proof |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
327 |
assume S: "S = {..< Sup S}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
328 |
then have "l < Sup S" using `l \<in> S` by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
329 |
then have "eventually (\<lambda>x. f x < Sup S) net" using ev by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
330 |
then show "eventually (\<lambda>x. f x \<in> S) net" by (subst S) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
331 |
qed auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
332 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
333 |
fix l y assume S: "\<forall>S. open S \<longrightarrow> mono (uminus`S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net" "l < y" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
334 |
have "eventually (\<lambda>x. f x \<in> {..< y}) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
335 |
using `l < y` by (intro S[rule_format]) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
336 |
then show "eventually (\<lambda>x. f x < y) net" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
337 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
338 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
339 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
340 |
lemma open_uminus_iff: "open (uminus ` S) \<longleftrightarrow> open (S::extreal set)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
341 |
using extreal_open_uminus[of S] extreal_open_uminus[of "uminus`S"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
342 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
343 |
lemma extreal_Limsup_uminus: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
344 |
fixes f :: "'a => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
345 |
shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
346 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
347 |
{ fix P l have "(\<exists>x. (l::extreal) = -x \<and> P x) \<longleftrightarrow> P (-l)" by (auto intro!: exI[of _ "-l"]) } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
348 |
note Ex_cancel = this |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
349 |
{ fix P :: "extreal set \<Rightarrow> bool" have "(\<forall>S. P S) \<longleftrightarrow> (\<forall>S. P (uminus`S))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
350 |
apply auto by (erule_tac x="uminus`S" in allE) (auto simp: image_image) } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
351 |
note add_uminus_image = this |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
352 |
{ fix x S have "(x::extreal) \<in> uminus`S \<longleftrightarrow> -x\<in>S" by (auto intro!: image_eqI[of _ _ "-x"]) } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
353 |
note remove_uminus_image = this |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
354 |
show ?thesis |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
355 |
unfolding extreal_Limsup_Inf_monoset extreal_Liminf_Sup_monoset |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
356 |
unfolding extreal_Inf_uminus_image_eq[symmetric] image_Collect Ex_cancel |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
357 |
by (subst add_uminus_image) (simp add: open_uminus_iff remove_uminus_image) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
358 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
359 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
360 |
lemma extreal_Liminf_uminus: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
361 |
fixes f :: "'a => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
362 |
shows "Liminf net (\<lambda>x. - (f x)) = -(Limsup net f)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
363 |
using extreal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
364 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
365 |
lemma extreal_Lim_uminus: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
366 |
fixes f :: "'a \<Rightarrow> extreal" shows "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x) ---> - f0) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
367 |
using |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
368 |
extreal_lim_mult[of f f0 net "- 1"] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
369 |
extreal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
370 |
by (auto simp: extreal_uminus_reorder) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
371 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
372 |
lemma lim_imp_Limsup: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
373 |
fixes f :: "'a => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
374 |
assumes "\<not> trivial_limit net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
375 |
assumes lim: "(f ---> f0) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
376 |
shows "Limsup net f = f0" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
377 |
using extreal_Lim_uminus[of f f0] lim_imp_Liminf[of net "(%x. -(f x))" "-f0"] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
378 |
extreal_Liminf_uminus[of net f] assms by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
379 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
380 |
lemma Liminf_PInfty: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
381 |
fixes f :: "'a \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
382 |
assumes "\<not> trivial_limit net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
383 |
shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
384 |
proof (intro lim_imp_Liminf iffI assms) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
385 |
assume rhs: "Liminf net f = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
386 |
{ fix S assume "open S & \<infinity> : S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
387 |
then obtain m where "{extreal m<..} <= S" using open_PInfty2 by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
388 |
moreover have "eventually (\<lambda>x. f x \<in> {extreal m<..}) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
389 |
using rhs unfolding Liminf_Sup top_extreal_def[symmetric] Sup_eq_top_iff |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
390 |
by (auto elim!: allE[where x="extreal m"] simp: top_extreal_def) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
391 |
ultimately have "eventually (%x. f x : S) net" apply (subst eventually_mono) by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
392 |
} then show "(f ---> \<infinity>) net" unfolding tendsto_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
393 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
394 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
395 |
lemma Limsup_MInfty: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
396 |
fixes f :: "'a \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
397 |
assumes "\<not> trivial_limit net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
398 |
shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
399 |
using assms extreal_Lim_uminus[of f "-\<infinity>"] Liminf_PInfty[of _ "\<lambda>x. - (f x)"] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
400 |
extreal_Liminf_uminus[of _ f] by (auto simp: extreal_uminus_eq_reorder) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
401 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
402 |
lemma extreal_Liminf_eq_Limsup: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
403 |
fixes f :: "'a \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
404 |
assumes ntriv: "\<not> trivial_limit net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
405 |
assumes lim: "Liminf net f = f0" "Limsup net f = f0" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
406 |
shows "(f ---> f0) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
407 |
proof (cases f0) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
408 |
case PInf then show ?thesis using Liminf_PInfty[OF ntriv] lim by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
409 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
410 |
case MInf then show ?thesis using Limsup_MInfty[OF ntriv] lim by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
411 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
412 |
case (real r) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
413 |
show "(f ---> f0) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
414 |
proof (rule topological_tendstoI) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
415 |
fix S assume "open S""f0 \<in> S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
416 |
then obtain a b where "a < Liminf net f" "Limsup net f < b" "{a<..<b} \<subseteq> S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
417 |
using extreal_open_cont_interval2[of S f0] real lim by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
418 |
then have "eventually (\<lambda>x. f x \<in> {a<..<b}) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
419 |
unfolding Liminf_Sup Limsup_Inf less_Sup_iff Inf_less_iff |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
420 |
by (auto intro!: eventually_conj simp add: greaterThanLessThan_iff) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
421 |
with `{a<..<b} \<subseteq> S` show "eventually (%x. f x : S) net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
422 |
by (rule_tac eventually_mono) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
423 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
424 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
425 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
426 |
lemma extreal_Liminf_eq_Limsup_iff: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
427 |
fixes f :: "'a \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
428 |
assumes "\<not> trivial_limit net" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
429 |
shows "(f ---> f0) net \<longleftrightarrow> Liminf net f = f0 \<and> Limsup net f = f0" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
430 |
by (metis assms extreal_Liminf_eq_Limsup lim_imp_Liminf lim_imp_Limsup) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
431 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
432 |
lemma limsup_INFI_SUPR: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
433 |
fixes f :: "nat \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
434 |
shows "limsup f = (INF n. SUP m:{n..}. f m)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
435 |
using extreal_Limsup_uminus[of sequentially "\<lambda>x. - f x"] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
436 |
by (simp add: liminf_SUPR_INFI extreal_INFI_uminus extreal_SUPR_uminus) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
437 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
438 |
lemma liminf_PInfty: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
439 |
fixes X :: "nat => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
440 |
shows "X ----> \<infinity> <-> liminf X = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
441 |
by (metis Liminf_PInfty trivial_limit_sequentially) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
442 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
443 |
lemma limsup_MInfty: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
444 |
fixes X :: "nat => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
445 |
shows "X ----> (-\<infinity>) <-> limsup X = (-\<infinity>)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
446 |
by (metis Limsup_MInfty trivial_limit_sequentially) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
447 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
448 |
lemma extreal_lim_mono: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
449 |
fixes X Y :: "nat => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
450 |
assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
451 |
assumes "X ----> x" "Y ----> y" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
452 |
shows "x <= y" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
453 |
by (metis extreal_Liminf_eq_Limsup_iff[OF trivial_limit_sequentially] assms liminf_mono) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
454 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
455 |
lemma incseq_le_extreal: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
456 |
fixes X :: "nat \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
457 |
assumes inc: "incseq X" and lim: "X ----> L" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
458 |
shows "X N \<le> L" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
459 |
using inc |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
460 |
by (intro extreal_lim_mono[of N, OF _ Lim_const lim]) (simp add: incseq_def) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
461 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
462 |
lemma decseq_ge_extreal: assumes dec: "decseq X" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
463 |
and lim: "X ----> (L::extreal)" shows "X N >= L" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
464 |
using dec |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
465 |
by (intro extreal_lim_mono[of N, OF _ lim Lim_const]) (simp add: decseq_def) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
466 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
467 |
lemma liminf_bounded_open: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
468 |
fixes x :: "nat \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
469 |
shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
470 |
(is "_ \<longleftrightarrow> ?P x0") |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
471 |
proof |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
472 |
assume "?P x0" then show "x0 \<le> liminf x" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
473 |
unfolding extreal_Liminf_Sup_monoset eventually_sequentially |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
474 |
by (intro complete_lattice_class.Sup_upper) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
475 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
476 |
assume "x0 \<le> liminf x" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
477 |
{ fix S :: "extreal set" assume om: "open S & mono S & x0:S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
478 |
{ assume "S = UNIV" hence "EX N. (ALL n>=N. x n : S)" by auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
479 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
480 |
{ assume "~(S=UNIV)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
481 |
then obtain B where B_def: "S = {B<..}" using om extreal_open_mono_set by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
482 |
hence "B<x0" using om by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
483 |
hence "EX N. ALL n>=N. x n : S" unfolding B_def using `x0 \<le> liminf x` liminf_bounded_iff by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
484 |
} ultimately have "EX N. (ALL n>=N. x n : S)" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
485 |
} then show "?P x0" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
486 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
487 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
488 |
lemma limsup_subseq_mono: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
489 |
fixes X :: "nat \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
490 |
assumes "subseq r" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
491 |
shows "limsup (X \<circ> r) \<le> limsup X" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
492 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
493 |
have "(\<lambda>n. - X n) \<circ> r = (\<lambda>n. - (X \<circ> r) n)" by (simp add: fun_eq_iff) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
494 |
then have "- limsup X \<le> - limsup (X \<circ> r)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
495 |
using liminf_subseq_mono[of r "(%n. - X n)"] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
496 |
extreal_Liminf_uminus[of sequentially X] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
497 |
extreal_Liminf_uminus[of sequentially "X o r"] assms by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
498 |
then show ?thesis by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
499 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
500 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
501 |
lemma bounded_abs: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
502 |
assumes "(a::real)<=x" "x<=b" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
503 |
shows "abs x <= max (abs a) (abs b)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
504 |
by (metis abs_less_iff assms leI le_max_iff_disj less_eq_real_def less_le_not_le less_minus_iff minus_minus) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
505 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
506 |
lemma bounded_increasing_convergent2: fixes f::"nat => real" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
507 |
assumes "ALL n. f n <= B" "ALL n m. n>=m --> f n >= f m" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
508 |
shows "EX l. (f ---> l) sequentially" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
509 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
510 |
def N == "max (abs (f 0)) (abs B)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
511 |
{ fix n have "abs (f n) <= N" unfolding N_def apply (subst bounded_abs) using assms by auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
512 |
hence "bounded {f n| n::nat. True}" unfolding bounded_real by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
513 |
from this show ?thesis apply(rule Topology_Euclidean_Space.bounded_increasing_convergent) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
514 |
using assms by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
515 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
516 |
lemma lim_extreal_increasing: assumes "\<And>n m. n >= m \<Longrightarrow> f n >= f m" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
517 |
obtains l where "f ----> (l::extreal)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
518 |
proof(cases "f = (\<lambda>x. - \<infinity>)") |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
519 |
case True then show thesis using Lim_const[of "- \<infinity>" sequentially] by (intro that[of "-\<infinity>"]) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
520 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
521 |
case False |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
522 |
from this obtain N where N_def: "f N > (-\<infinity>)" by (auto simp: fun_eq_iff) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
523 |
have "ALL n>=N. f n >= f N" using assms by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
524 |
hence minf: "ALL n>=N. f n > (-\<infinity>)" using N_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
525 |
def Y == "(%n. (if n>=N then f n else f N))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
526 |
hence incy: "!!n m. n>=m ==> Y n >= Y m" using assms by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
527 |
from minf have minfy: "ALL n. Y n ~= (-\<infinity>)" using Y_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
528 |
show thesis |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
529 |
proof(cases "EX B. ALL n. f n < extreal B") |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
530 |
case False thus thesis apply- apply(rule that[of \<infinity>]) unfolding Lim_PInfty not_ex not_all |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
531 |
apply safe apply(erule_tac x=B in allE,safe) apply(rule_tac x=x in exI,safe) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
532 |
apply(rule order_trans[OF _ assms[rule_format]]) by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
533 |
next case True then guess B .. |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
534 |
hence "ALL n. Y n < extreal B" using Y_def by auto note B = this[rule_format] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
535 |
{ fix n have "Y n < \<infinity>" using B[of n] apply (subst less_le_trans) by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
536 |
hence "Y n ~= \<infinity> & Y n ~= (-\<infinity>)" using minfy by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
537 |
} hence *: "ALL n. \<bar>Y n\<bar> \<noteq> \<infinity>" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
538 |
{ fix n have "real (Y n) < B" proof- case goal1 thus ?case |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
539 |
using B[of n] apply-apply(subst(asm) extreal_real'[THEN sym]) defer defer |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
540 |
unfolding extreal_less using * by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
541 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
542 |
} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
543 |
hence B': "ALL n. (real (Y n) <= B)" using less_imp_le by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
544 |
have "EX l. (%n. real (Y n)) ----> l" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
545 |
apply(rule bounded_increasing_convergent2) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
546 |
proof safe show "!!n. real (Y n) <= B" using B' by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
547 |
fix n m::nat assume "n<=m" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
548 |
hence "extreal (real (Y n)) <= extreal (real (Y m))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
549 |
using incy[rule_format,of n m] apply(subst extreal_real)+ |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
550 |
using *[rule_format, of n] *[rule_format, of m] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
551 |
thus "real (Y n) <= real (Y m)" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
552 |
qed then guess l .. note l=this |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
553 |
have "Y ----> extreal l" using l apply-apply(subst(asm) lim_extreal[THEN sym]) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
554 |
unfolding extreal_real using * by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
555 |
thus thesis apply-apply(rule that[of "extreal l"]) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
556 |
apply (subst tail_same_limit[of Y _ N]) using Y_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
557 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
558 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
559 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
560 |
lemma lim_extreal_decreasing: assumes "\<And>n m. n >= m \<Longrightarrow> f n <= f m" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
561 |
obtains l where "f ----> (l::extreal)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
562 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
563 |
from lim_extreal_increasing[of "\<lambda>x. - f x"] assms |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
564 |
obtain l where "(\<lambda>x. - f x) ----> l" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
565 |
from extreal_lim_mult[OF this, of "- 1"] show thesis |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
566 |
by (intro that[of "-l"]) (simp add: extreal_uminus_eq_reorder) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
567 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
568 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
569 |
lemma compact_extreal: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
570 |
fixes X :: "nat \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
571 |
shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
572 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
573 |
obtain r where "subseq r" and mono: "monoseq (X \<circ> r)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
574 |
using seq_monosub[of X] unfolding comp_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
575 |
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)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
576 |
by (auto simp add: monoseq_def) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
577 |
then obtain l where "(X\<circ>r) ----> l" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
578 |
using lim_extreal_increasing[of "X \<circ> r"] lim_extreal_decreasing[of "X \<circ> r"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
579 |
then show ?thesis using `subseq r` by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
580 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
581 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
582 |
lemma extreal_Sup_lim: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
583 |
assumes "\<And>n. b n \<in> s" "b ----> (a::extreal)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
584 |
shows "a \<le> Sup s" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
585 |
by (metis Lim_bounded_extreal assms complete_lattice_class.Sup_upper) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
586 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
587 |
lemma extreal_Inf_lim: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
588 |
assumes "\<And>n. b n \<in> s" "b ----> (a::extreal)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
589 |
shows "Inf s \<le> a" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
590 |
by (metis Lim_bounded2_extreal assms complete_lattice_class.Inf_lower) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
591 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
592 |
lemma SUP_Lim_extreal: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
593 |
fixes X :: "nat \<Rightarrow> extreal" assumes "incseq X" "X ----> l" shows "(SUP n. X n) = l" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
594 |
proof (rule extreal_SUPI) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
595 |
fix n from assms show "X n \<le> l" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
596 |
by (intro incseq_le_extreal) (simp add: incseq_def) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
597 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
598 |
fix y assume "\<And>n. n \<in> UNIV \<Longrightarrow> X n \<le> y" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
599 |
with extreal_Sup_lim[OF _ `X ----> l`, of "{..y}"] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
600 |
show "l \<le> y" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
601 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
602 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
603 |
lemma LIMSEQ_extreal_SUPR: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
604 |
fixes X :: "nat \<Rightarrow> extreal" assumes "incseq X" shows "X ----> (SUP n. X n)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
605 |
proof (rule lim_extreal_increasing) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
606 |
fix n m :: nat assume "m \<le> n" then show "X m \<le> X n" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
607 |
using `incseq X` by (simp add: incseq_def) |
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 |
fix l assume "X ----> l" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
610 |
with SUP_Lim_extreal[of X, OF assms this] show ?thesis by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
611 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
612 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
613 |
lemma INF_Lim_extreal: "decseq X \<Longrightarrow> X ----> l \<Longrightarrow> (INF n. X n) = (l::extreal)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
614 |
using SUP_Lim_extreal[of "\<lambda>i. - X i" "- l"] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
615 |
by (simp add: extreal_SUPR_uminus extreal_lim_uminus) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
616 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
617 |
lemma LIMSEQ_extreal_INFI: "decseq X \<Longrightarrow> X ----> (INF n. X n :: extreal)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
618 |
using LIMSEQ_extreal_SUPR[of "\<lambda>i. - X i"] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
619 |
by (simp add: extreal_SUPR_uminus extreal_lim_uminus) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
620 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
621 |
lemma SUP_eq_LIMSEQ: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
622 |
assumes "mono f" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
623 |
shows "(SUP n. extreal (f n)) = extreal x \<longleftrightarrow> f ----> x" |
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 |
have inc: "incseq (\<lambda>i. extreal (f i))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
626 |
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
|
627 |
{ assume "f ----> x" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
628 |
then have "(\<lambda>i. extreal (f i)) ----> extreal x" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
629 |
from SUP_Lim_extreal[OF inc this] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
630 |
show "(SUP n. extreal (f n)) = extreal x" . } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
631 |
{ assume "(SUP n. extreal (f n)) = extreal x" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
632 |
with LIMSEQ_extreal_SUPR[OF inc] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
633 |
show "f ----> x" by auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
634 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
635 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
636 |
lemma Liminf_within: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
637 |
fixes f :: "'a::metric_space => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
638 |
shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
639 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
640 |
let ?l="(SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
641 |
{ fix T assume T_def: "open T & mono T & ?l:T" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
642 |
have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
643 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
644 |
{ assume "T=UNIV" hence ?thesis by (simp add: gt_ex) } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
645 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
646 |
{ assume "~(T=UNIV)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
647 |
then obtain B where "T={B<..}" using T_def extreal_open_mono_set[of T] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
648 |
hence "B<?l" using T_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
649 |
then obtain d where d_def: "0<d & B<(INF y:(S Int ball x d - {x}). f y)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
650 |
unfolding less_SUP_iff by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
651 |
{ fix y assume "y:S & 0 < dist y x & dist y x < d" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
652 |
hence "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
653 |
hence "f y:T" using d_def INF_leI[of y "S Int ball x d - {x}" f] `T={B<..}` by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
654 |
} hence ?thesis apply(rule_tac x="d" in exI) using d_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
655 |
} ultimately show ?thesis by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
656 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
657 |
} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
658 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
659 |
{ fix z |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
660 |
assume a: "ALL T. open T --> mono T --> z : T --> |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
661 |
(EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
662 |
{ fix B assume "B<z" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
663 |
then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> B < f y)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
664 |
using a[rule_format, of "{B<..}"] mono_greaterThan by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
665 |
{ fix y assume "y:(S Int ball x d - {x})" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
666 |
hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
667 |
by (metis dist_eq_0_iff real_less_def zero_le_dist) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
668 |
hence "B <= f y" using d_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
669 |
} hence "B <= INFI (S Int ball x d - {x}) f" apply (subst le_INFI) by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
670 |
also have "...<=?l" apply (subst le_SUPI) using d_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
671 |
finally have "B<=?l" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
672 |
} hence "z <= ?l" using extreal_le_extreal[of z "?l"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
673 |
} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
674 |
ultimately show ?thesis unfolding extreal_Liminf_Sup_monoset eventually_within |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
675 |
apply (subst extreal_SupI[of _ "(SUP e:{0<..}. INFI (S Int ball x e - {x}) f)"]) by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
676 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
677 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
678 |
lemma Limsup_within: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
679 |
fixes f :: "'a::metric_space => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
680 |
shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
681 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
682 |
let ?l="(INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
683 |
{ fix T assume T_def: "open T & mono (uminus ` T) & ?l:T" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
684 |
have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
685 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
686 |
{ assume "T=UNIV" hence ?thesis by (simp add: gt_ex) } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
687 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
688 |
{ assume "~(T=UNIV)" hence "~(uminus ` T = UNIV)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
689 |
by (metis Int_UNIV_right Int_absorb1 image_mono extreal_minus_minus_image subset_UNIV) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
690 |
hence "uminus ` T = {Inf (uminus ` T)<..}" using T_def extreal_open_mono_set[of "uminus ` T"] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
691 |
extreal_open_uminus[of T] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
692 |
then obtain B where "T={..<B}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
693 |
unfolding extreal_Inf_uminus_image_eq extreal_uminus_lessThan[symmetric] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
694 |
unfolding inj_image_eq_iff[OF extreal_inj_on_uminus] by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
695 |
hence "?l<B" using T_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
696 |
then obtain d where d_def: "0<d & (SUP y:(S Int ball x d - {x}). f y)<B" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
697 |
unfolding INF_less_iff by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
698 |
{ fix y assume "y:S & 0 < dist y x & dist y x < d" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
699 |
hence "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
700 |
hence "f y:T" using d_def le_SUPI[of y "S Int ball x d - {x}" f] `T={..<B}` by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
701 |
} hence ?thesis apply(rule_tac x="d" in exI) using d_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
702 |
} ultimately show ?thesis by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
703 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
704 |
} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
705 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
706 |
{ fix z |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
707 |
assume a: "ALL T. open T --> mono (uminus ` T) --> z : T --> |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
708 |
(EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
709 |
{ fix B assume "z<B" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
710 |
then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> f y<B)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
711 |
using a[rule_format, of "{..<B}"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
712 |
{ fix y assume "y:(S Int ball x d - {x})" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
713 |
hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
714 |
by (metis dist_eq_0_iff real_less_def zero_le_dist) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
715 |
hence "f y <= B" using d_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
716 |
} hence "SUPR (S Int ball x d - {x}) f <= B" apply (subst SUP_leI) by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
717 |
moreover have "?l<=SUPR (S Int ball x d - {x}) f" apply (subst INF_leI) using d_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
718 |
ultimately have "?l<=B" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
719 |
} hence "?l <= z" using extreal_ge_extreal[of z "?l"] by auto |
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 |
ultimately show ?thesis unfolding extreal_Limsup_Inf_monoset eventually_within |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
722 |
apply (subst extreal_InfI) by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
723 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
724 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
725 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
726 |
lemma Liminf_within_UNIV: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
727 |
fixes f :: "'a::metric_space => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
728 |
shows "Liminf (at x) f = Liminf (at x within UNIV) f" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
729 |
by (metis within_UNIV) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
730 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
731 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
732 |
lemma Liminf_at: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
733 |
fixes f :: "'a::metric_space => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
734 |
shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
735 |
using Liminf_within[of x UNIV f] Liminf_within_UNIV[of x f] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
736 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
737 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
738 |
lemma Limsup_within_UNIV: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
739 |
fixes f :: "'a::metric_space => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
740 |
shows "Limsup (at x) f = Limsup (at x within UNIV) f" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
741 |
by (metis within_UNIV) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
742 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
743 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
744 |
lemma Limsup_at: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
745 |
fixes f :: "'a::metric_space => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
746 |
shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
747 |
using Limsup_within[of x UNIV f] Limsup_within_UNIV[of x f] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
748 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
749 |
lemma Lim_within_constant: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
750 |
fixes f :: "'a::metric_space => 'b::topological_space" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
751 |
assumes "ALL y:S. f y = C" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
752 |
shows "(f ---> C) (at x within S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
753 |
unfolding tendsto_def eventually_within |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
754 |
by (metis assms(1) linorder_le_less_linear n_not_Suc_n real_of_nat_le_zero_cancel_iff) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
755 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
756 |
lemma Liminf_within_constant: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
757 |
fixes f :: "'a::metric_space => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
758 |
assumes "ALL y:S. f y = C" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
759 |
assumes "~trivial_limit (at x within S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
760 |
shows "Liminf (at x within S) f = C" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
761 |
by (metis Lim_within_constant assms lim_imp_Liminf) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
762 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
763 |
lemma Limsup_within_constant: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
764 |
fixes f :: "'a::metric_space => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
765 |
assumes "ALL y:S. f y = C" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
766 |
assumes "~trivial_limit (at x within S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
767 |
shows "Limsup (at x within S) f = C" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
768 |
by (metis Lim_within_constant assms lim_imp_Limsup) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
769 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
770 |
lemma islimpt_punctured: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
771 |
"x islimpt S = x islimpt (S-{x})" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
772 |
unfolding islimpt_def by blast |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
773 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
774 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
775 |
lemma islimpt_in_closure: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
776 |
"(x islimpt S) = (x:closure(S-{x}))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
777 |
unfolding closure_def using islimpt_punctured by blast |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
778 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
779 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
780 |
lemma not_trivial_limit_within: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
781 |
"~trivial_limit (at x within S) = (x:closure(S-{x}))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
782 |
using islimpt_in_closure by (metis trivial_limit_within) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
783 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
784 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
785 |
lemma not_trivial_limit_within_ball: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
786 |
"(~trivial_limit (at x within S)) = (ALL e>0. S Int ball x e - {x} ~= {})" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
787 |
(is "?lhs = ?rhs") |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
788 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
789 |
{ assume "?lhs" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
790 |
{ fix e :: real assume "e>0" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
791 |
then obtain y where "y:(S-{x}) & dist y x < e" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
792 |
using `?lhs` not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
793 |
hence "y : (S Int ball x e - {x})" unfolding ball_def by (simp add: dist_commute) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
794 |
hence "S Int ball x e - {x} ~= {}" by blast |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
795 |
} hence "?rhs" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
796 |
} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
797 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
798 |
{ assume "?rhs" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
799 |
{ fix e :: real assume "e>0" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
800 |
then obtain y where "y : (S Int ball x e - {x})" using `?rhs` by blast |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
801 |
hence "y:(S-{x}) & dist y x < e" unfolding ball_def by (simp add: dist_commute) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
802 |
hence "EX y:(S-{x}). dist y x < e" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
803 |
} hence "?lhs" using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
804 |
} ultimately show ?thesis by auto |
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 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
807 |
subsubsection {* Continuity *} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
808 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
809 |
lemma continuous_imp_tendsto: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
810 |
assumes "continuous (at x0) f" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
811 |
assumes "x ----> x0" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
812 |
shows "(f o x) ----> (f x0)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
813 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
814 |
{ fix S assume "open S & (f x0):S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
815 |
from this obtain T where T_def: "open T & x0 : T & (ALL x:T. f x : S)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
816 |
using assms continuous_at_open by metis |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
817 |
hence "(EX N. ALL n>=N. x n : T)" using assms tendsto_explicit T_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
818 |
hence "(EX N. ALL n>=N. f(x n) : S)" using T_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
819 |
} from this show ?thesis using tendsto_explicit[of "f o x" "f x0"] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
820 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
821 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
822 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
823 |
lemma continuous_at_sequentially2: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
824 |
fixes f :: "'a::metric_space => 'b:: topological_space" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
825 |
shows "continuous (at x0) f <-> (ALL x. (x ----> x0) --> (f o x) ----> (f x0))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
826 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
827 |
{ assume "~(continuous (at x0) f)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
828 |
from this obtain T where T_def: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
829 |
"open T & f x0 : T & (ALL S. (open S & x0 : S) --> (EX x':S. f x' ~: T))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
830 |
using continuous_at_open[of x0 f] by metis |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
831 |
def X == "{x'. f x' ~: T}" hence "x0 islimpt X" unfolding islimpt_def using T_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
832 |
from this obtain x where x_def: "(ALL n. x n : X) & x ----> x0" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
833 |
using islimpt_sequential[of x0 X] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
834 |
hence "~(f o x) ----> (f x0)" unfolding tendsto_explicit using X_def T_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
835 |
hence "EX x. x ----> x0 & (~(f o x) ----> (f x0))" using x_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
836 |
} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
837 |
from this show ?thesis using continuous_imp_tendsto by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
838 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
839 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
840 |
lemma continuous_at_of_extreal: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
841 |
fixes x0 :: extreal |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
842 |
assumes "\<bar>x0\<bar> \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
843 |
shows "continuous (at x0) real" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
844 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
845 |
{ fix T assume T_def: "open T & real x0 : T" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
846 |
def S == "extreal ` T" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
847 |
hence "extreal (real x0) : S" using T_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
848 |
hence "x0 : S" using assms extreal_real by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
849 |
moreover have "open S" using open_extreal S_def T_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
850 |
moreover have "ALL y:S. real y : T" using S_def T_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
851 |
ultimately have "EX S. x0 : S & open S & (ALL y:S. real y : T)" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
852 |
} from this show ?thesis unfolding continuous_at_open by blast |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
853 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
854 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
855 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
856 |
lemma continuous_at_iff_extreal: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
857 |
fixes f :: "'a::t2_space => real" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
858 |
shows "continuous (at x0) f <-> continuous (at x0) (extreal o f)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
859 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
860 |
{ assume "continuous (at x0) f" hence "continuous (at x0) (extreal o f)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
861 |
using continuous_at_extreal continuous_at_compose[of x0 f extreal] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
862 |
} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
863 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
864 |
{ assume "continuous (at x0) (extreal o f)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
865 |
hence "continuous (at x0) (real o (extreal o f))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
866 |
using continuous_at_of_extreal by (intro continuous_at_compose[of x0 "extreal o f"]) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
867 |
moreover have "real o (extreal o f) = f" using real_extreal_id by (simp add: o_assoc) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
868 |
ultimately have "continuous (at x0) f" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
869 |
} ultimately show ?thesis by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
870 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
871 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
872 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
873 |
lemma continuous_on_iff_extreal: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
874 |
fixes f :: "'a::t2_space => real" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
875 |
fixes A assumes "open A" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
876 |
shows "continuous_on A f <-> continuous_on A (extreal o f)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
877 |
using continuous_at_iff_extreal assms by (auto simp add: continuous_on_eq_continuous_at) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
878 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
879 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
880 |
lemma continuous_on_real: "continuous_on (UNIV-{\<infinity>,(-\<infinity>)}) real" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
881 |
using continuous_at_of_extreal continuous_on_eq_continuous_at open_image_extreal by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
882 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
883 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
884 |
lemma continuous_on_iff_real: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
885 |
fixes f :: "'a::t2_space => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
886 |
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
|
887 |
shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
888 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
889 |
have "f ` A <= UNIV-{\<infinity>,(-\<infinity>)}" using assms by force |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
890 |
hence *: "continuous_on (f ` A) real" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
891 |
using continuous_on_real by (simp add: continuous_on_subset) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
892 |
have **: "continuous_on ((real o f) ` A) extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
893 |
using continuous_on_extreal continuous_on_subset[of "UNIV" "extreal" "(real o f) ` A"] by blast |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
894 |
{ assume "continuous_on A f" hence "continuous_on A (real o f)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
895 |
apply (subst continuous_on_compose) using * by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
896 |
} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
897 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
898 |
{ assume "continuous_on A (real o f)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
899 |
hence "continuous_on A (extreal o (real o f))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
900 |
apply (subst continuous_on_compose) using ** by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
901 |
hence "continuous_on A f" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
902 |
apply (subst continuous_on_eq[of A "extreal o (real o f)" f]) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
903 |
using assms extreal_real by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
904 |
} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
905 |
ultimately show ?thesis by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
906 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
907 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
908 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
909 |
lemma continuous_at_const: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
910 |
fixes f :: "'a::t2_space => extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
911 |
assumes "ALL x. (f x = C)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
912 |
shows "ALL x. continuous (at x) f" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
913 |
unfolding continuous_at_open using assms t1_space by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
914 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
915 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
916 |
lemma closure_contains_Inf: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
917 |
fixes S :: "real set" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
918 |
assumes "S ~= {}" "EX B. ALL x:S. B<=x" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
919 |
shows "Inf S : closure S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
920 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
921 |
have *: "ALL x:S. Inf S <= x" using Inf_lower_EX[of _ S] assms by metis |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
922 |
{ fix e assume "e>(0 :: real)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
923 |
from this obtain x where x_def: "x:S & x < Inf S + e" using Inf_close `S ~= {}` by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
924 |
moreover hence "x > Inf S - e" using * by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
925 |
ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
926 |
hence "EX x:S. abs (x - Inf S) < e" using x_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
927 |
} from this show ?thesis apply (subst closure_approachable) unfolding dist_norm by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
928 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
929 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
930 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
931 |
lemma closed_contains_Inf: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
932 |
fixes S :: "real set" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
933 |
assumes "S ~= {}" "EX B. ALL x:S. B<=x" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
934 |
assumes "closed S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
935 |
shows "Inf S : S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
936 |
by (metis closure_contains_Inf closure_closed assms) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
937 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
938 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
939 |
lemma mono_closed_real: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
940 |
fixes S :: "real set" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
941 |
assumes mono: "ALL y z. y:S & y<=z --> z:S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
942 |
assumes "closed S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
943 |
shows "S = {} | S = UNIV | (EX a. S = {a ..})" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
944 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
945 |
{ assume "S ~= {}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
946 |
{ assume ex: "EX B. ALL x:S. B<=x" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
947 |
hence *: "ALL x:S. Inf S <= x" using Inf_lower_EX[of _ S] ex by metis |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
948 |
hence "Inf S : S" apply (subst closed_contains_Inf) using ex `S ~= {}` `closed S` by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
949 |
hence "ALL x. (Inf S <= x <-> x:S)" using mono[rule_format, of "Inf S"] * by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
950 |
hence "S = {Inf S ..}" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
951 |
hence "EX a. S = {a ..}" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
952 |
} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
953 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
954 |
{ assume "~(EX B. ALL x:S. B<=x)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
955 |
hence nex: "ALL B. EX x:S. x<B" by (simp add: not_le) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
956 |
{ fix y obtain x where "x:S & x < y" using nex by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
957 |
hence "y:S" using mono[rule_format, of x y] by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
958 |
} hence "S = UNIV" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
959 |
} ultimately have "S = UNIV | (EX a. S = {a ..})" by blast |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
960 |
} from this show ?thesis by blast |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
961 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
962 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
963 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
964 |
lemma mono_closed_extreal: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
965 |
fixes S :: "real set" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
966 |
assumes mono: "ALL y z. y:S & y<=z --> z:S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
967 |
assumes "closed S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
968 |
shows "EX a. S = {x. a <= extreal x}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
969 |
proof- |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
970 |
{ assume "S = {}" hence ?thesis apply(rule_tac x=PInfty in exI) by auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
971 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
972 |
{ assume "S = UNIV" hence ?thesis apply(rule_tac x="-\<infinity>" in exI) by auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
973 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
974 |
{ assume "EX a. S = {a ..}" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
975 |
from this obtain a where "S={a ..}" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
976 |
hence ?thesis apply(rule_tac x="extreal a" in exI) by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
977 |
} ultimately show ?thesis using mono_closed_real[of S] assms by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
978 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
979 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
980 |
subsection {* Sums *} |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
981 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
982 |
lemma setsum_extreal[simp]: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
983 |
"(\<Sum>x\<in>A. extreal (f x)) = extreal (\<Sum>x\<in>A. f x)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
984 |
proof cases |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
985 |
assume "finite A" then show ?thesis by induct auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
986 |
qed simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
987 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
988 |
lemma setsum_Pinfty: "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> (finite P \<and> (\<exists>i\<in>P. f i = \<infinity>))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
989 |
proof safe |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
990 |
assume *: "setsum f P = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
991 |
show "finite P" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
992 |
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
|
993 |
show "\<exists>i\<in>P. f i = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
994 |
proof (rule ccontr) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
995 |
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
|
996 |
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
|
997 |
by induct auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
998 |
with * show False by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
999 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1000 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1001 |
fix i assume "finite P" "i \<in> P" "f i = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1002 |
thus "setsum f P = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1003 |
proof induct |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1004 |
case (insert x A) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1005 |
show ?case using insert by (cases "x = i") auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1006 |
qed simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1007 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1008 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1009 |
lemma setsum_Inf: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1010 |
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
|
1011 |
proof |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1012 |
assume *: "\<bar>setsum f A\<bar> = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1013 |
have "finite A" by (rule ccontr) (insert *, auto) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1014 |
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
|
1015 |
proof (rule ccontr) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1016 |
assume "\<not> ?thesis" then have "\<forall>i\<in>A. \<exists>r. f i = extreal r" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1017 |
from bchoice[OF this] guess r .. |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1018 |
with * show False by (auto simp: setsum_extreal) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1019 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1020 |
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
|
1021 |
next |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1022 |
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
|
1023 |
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
|
1024 |
then show "\<bar>setsum f A\<bar> = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1025 |
proof induct |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1026 |
case (insert j A) then show ?case |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1027 |
by (cases rule: extreal3_cases[of "f i" "f j" "setsum f A"]) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1028 |
qed simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1029 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1030 |
|
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41980
diff
changeset
|
1031 |
lemma setsum_real_of_extreal: |
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1032 |
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
|
1033 |
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
|
1034 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1035 |
have "\<forall>x\<in>S. \<exists>r. f x = extreal r" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1036 |
proof |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1037 |
fix x assume "x \<in> S" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1038 |
from assms[OF this] show "\<exists>r. f x = extreal r" by (cases "f x") auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1039 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1040 |
from bchoice[OF this] guess r .. |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1041 |
then show ?thesis by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1042 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1043 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1044 |
lemma setsum_extreal_0: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1045 |
fixes f :: "'a \<Rightarrow> extreal" assumes "finite A" "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1046 |
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
|
1047 |
proof |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1048 |
assume *: "(\<Sum>x\<in>A. f x) = 0" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1049 |
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
|
1050 |
then have "\<forall>i\<in>A. \<bar>f i\<bar> \<noteq> \<infinity>" using assms by (force simp: setsum_Pinfty) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1051 |
then have "\<forall>i\<in>A. \<exists>r. f i = extreal r" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1052 |
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
|
1053 |
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
|
1054 |
qed (rule setsum_0') |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1055 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1056 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1057 |
lemma setsum_extreal_right_distrib: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1058 |
fixes f :: "'a \<Rightarrow> extreal" assumes "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1059 |
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
|
1060 |
proof cases |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1061 |
assume "finite A" then show ?thesis using assms |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1062 |
by induct (auto simp: extreal_right_distrib setsum_nonneg) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1063 |
qed simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1064 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1065 |
lemma sums_extreal_positive: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1066 |
fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>i. 0 \<le> f i" shows "f sums (SUP n. \<Sum>i<n. f i)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1067 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1068 |
have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1069 |
using extreal_add_mono[OF _ assms] by (auto intro!: incseq_SucI) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1070 |
from LIMSEQ_extreal_SUPR[OF this] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1071 |
show ?thesis unfolding sums_def by (simp add: atLeast0LessThan) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1072 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1073 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1074 |
lemma summable_extreal_pos: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1075 |
fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>i. 0 \<le> f i" shows "summable f" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1076 |
using sums_extreal_positive[of f, OF assms] unfolding summable_def by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1077 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1078 |
lemma suminf_extreal_eq_SUPR: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1079 |
fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>i. 0 \<le> f i" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1080 |
shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1081 |
using sums_extreal_positive[of f, OF assms, THEN sums_unique] by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1082 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1083 |
lemma sums_extreal: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1084 |
"(\<lambda>x. extreal (f x)) sums extreal x \<longleftrightarrow> f sums x" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1085 |
unfolding sums_def by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1086 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1087 |
lemma suminf_bound: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1088 |
fixes f :: "nat \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1089 |
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
|
1090 |
shows "suminf f \<le> x" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1091 |
proof (rule Lim_bounded_extreal) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1092 |
have "summable f" using pos[THEN summable_extreal_pos] . |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1093 |
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
|
1094 |
by (auto dest!: summable_sums simp: sums_def atLeast0LessThan) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1095 |
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
|
1096 |
using assms by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1097 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1098 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1099 |
lemma suminf_bound_add: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1100 |
fixes f :: "nat \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1101 |
assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x" and pos: "\<And>n. 0 \<le> f n" and "y \<noteq> -\<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1102 |
shows "suminf f + y \<le> x" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1103 |
proof (cases y) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1104 |
case (real r) then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1105 |
using assms by (simp add: extreal_le_minus) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1106 |
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
|
1107 |
then show "(\<Sum> n. f n) + y \<le> x" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1108 |
using assms real by (simp add: extreal_le_minus) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1109 |
qed (insert assms, auto) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1110 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1111 |
lemma sums_finite: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1112 |
assumes "\<forall>N\<ge>n. f N = 0" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1113 |
shows "f sums (\<Sum>N<n. f N)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1114 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1115 |
{ fix i have "(\<Sum>N<i + n. f N) = (\<Sum>N<n. f N)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1116 |
by (induct i) (insert assms, auto) } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1117 |
note this[simp] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1118 |
show ?thesis unfolding sums_def |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1119 |
by (rule LIMSEQ_offset[of _ n]) (auto simp add: atLeast0LessThan) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1120 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1121 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1122 |
lemma suminf_finite: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1123 |
fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,t2_space}" assumes "\<forall>N\<ge>n. f N = 0" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1124 |
shows "suminf f = (\<Sum>N<n. f N)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1125 |
using sums_finite[OF assms, THEN sums_unique] by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1126 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1127 |
lemma suminf_extreal_0[simp]: "(\<Sum>i. 0) = (0::'a::{comm_monoid_add,t2_space})" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1128 |
using suminf_finite[of 0 "\<lambda>x. 0"] by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1129 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1130 |
lemma suminf_upper: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1131 |
fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>n. 0 \<le> f n" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1132 |
shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1133 |
unfolding suminf_extreal_eq_SUPR[OF assms] SUPR_def |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1134 |
by (auto intro: complete_lattice_class.Sup_upper image_eqI) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1135 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1136 |
lemma suminf_0_le: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1137 |
fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>n. 0 \<le> f n" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1138 |
shows "0 \<le> (\<Sum>n. f n)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1139 |
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
|
1140 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1141 |
lemma suminf_le_pos: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1142 |
fixes f g :: "nat \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1143 |
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
|
1144 |
shows "suminf f \<le> suminf g" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1145 |
proof (safe intro!: suminf_bound) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1146 |
fix n { fix N have "0 \<le> g N" using assms(2,1)[of N] by auto } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1147 |
have "setsum f {..<n} \<le> setsum g {..<n}" using assms by (auto intro: setsum_mono) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1148 |
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
|
1149 |
finally show "setsum f {..<n} \<le> suminf g" . |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1150 |
qed (rule assms(2)) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1151 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1152 |
lemma suminf_half_series_extreal: "(\<Sum>n. (1/2 :: extreal)^Suc n) = 1" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1153 |
using sums_extreal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1154 |
by (simp add: one_extreal_def) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1155 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1156 |
lemma suminf_add_extreal: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1157 |
fixes f g :: "nat \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1158 |
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
|
1159 |
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
|
1160 |
apply (subst (1 2 3) suminf_extreal_eq_SUPR) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1161 |
unfolding setsum_addf |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1162 |
by (intro assms extreal_add_nonneg_nonneg SUPR_extreal_add_pos incseq_setsumI setsum_nonneg ballI)+ |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1163 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1164 |
lemma suminf_cmult_extreal: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1165 |
fixes f g :: "nat \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1166 |
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
|
1167 |
shows "(\<Sum>i. a * f i) = a * suminf f" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1168 |
by (auto simp: setsum_extreal_right_distrib[symmetric] assms |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1169 |
extreal_zero_le_0_iff setsum_nonneg suminf_extreal_eq_SUPR |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1170 |
intro!: SUPR_extreal_cmult ) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1171 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1172 |
lemma suminf_PInfty: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1173 |
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
|
1174 |
shows "f i \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1175 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1176 |
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
|
1177 |
have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1178 |
then show ?thesis |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1179 |
unfolding setsum_Pinfty by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1180 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1181 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1182 |
lemma suminf_PInfty_fun: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1183 |
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
|
1184 |
shows "\<exists>f'. f = (\<lambda>x. extreal (f' x))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1185 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1186 |
have "\<forall>i. \<exists>r. f i = extreal r" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1187 |
proof |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1188 |
fix i show "\<exists>r. f i = extreal r" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1189 |
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
|
1190 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1191 |
from choice[OF this] show ?thesis by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1192 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1193 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1194 |
lemma summable_extreal: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1195 |
assumes "\<And>i. 0 \<le> f i" "(\<Sum>i. extreal (f i)) \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1196 |
shows "summable f" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1197 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1198 |
have "0 \<le> (\<Sum>i. extreal (f i))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1199 |
using assms by (intro suminf_0_le) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1200 |
with assms obtain r where r: "(\<Sum>i. extreal (f i)) = extreal r" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1201 |
by (cases "\<Sum>i. extreal (f i)") auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1202 |
from summable_extreal_pos[of "\<lambda>x. extreal (f x)"] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1203 |
have "summable (\<lambda>x. extreal (f x))" using assms by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1204 |
from summable_sums[OF this] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1205 |
have "(\<lambda>x. extreal (f x)) sums (\<Sum>x. extreal (f x))" by auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1206 |
then show "summable f" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1207 |
unfolding r sums_extreal summable_def .. |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1208 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1209 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1210 |
lemma suminf_extreal: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1211 |
assumes "\<And>i. 0 \<le> f i" "(\<Sum>i. extreal (f i)) \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1212 |
shows "(\<Sum>i. extreal (f i)) = extreal (suminf f)" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1213 |
proof (rule sums_unique[symmetric]) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1214 |
from summable_extreal[OF assms] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1215 |
show "(\<lambda>x. extreal (f x)) sums (extreal (suminf f))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1216 |
unfolding sums_extreal using assms by (intro summable_sums summable_extreal) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1217 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1218 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1219 |
lemma suminf_extreal_minus: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1220 |
fixes f g :: "nat \<Rightarrow> extreal" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1221 |
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
|
1222 |
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
|
1223 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1224 |
{ 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
|
1225 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1226 |
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
|
1227 |
from suminf_PInfty_fun[OF `\<And>i. 0 \<le> g i` fin(2)] guess g' .. note this[simp] |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1228 |
{ fix i have "0 \<le> f i - g i" using ord[of i] by (auto simp: extreal_le_minus_iff) } |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1229 |
moreover |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1230 |
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
|
1231 |
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
|
1232 |
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
|
1233 |
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
|
1234 |
apply simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1235 |
by (subst (1 2 3) suminf_extreal) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1236 |
(auto intro!: suminf_diff[symmetric] summable_extreal) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1237 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1238 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1239 |
lemma suminf_extreal_PInf[simp]: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1240 |
"(\<Sum>x. \<infinity>) = \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1241 |
proof - |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1242 |
have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>)" by (rule suminf_upper) auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1243 |
then show ?thesis by simp |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1244 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1245 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1246 |
lemma summable_real_of_extreal: |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1247 |
assumes f: "\<And>i. 0 \<le> f i" and fin: "(\<Sum>i. f i) \<noteq> \<infinity>" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1248 |
shows "summable (\<lambda>i. real (f i))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1249 |
proof (rule summable_def[THEN iffD2]) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1250 |
have "0 \<le> (\<Sum>i. f i)" using assms by (auto intro: suminf_0_le) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1251 |
with fin obtain r where r: "extreal r = (\<Sum>i. f i)" by (cases "(\<Sum>i. f i)") auto |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1252 |
{ 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
|
1253 |
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
|
1254 |
note fin = this |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1255 |
have "(\<lambda>i. extreal (real (f i))) sums (\<Sum>i. extreal (real (f i)))" |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1256 |
using f by (auto intro!: summable_extreal_pos summable_sums simp: extreal_le_real_iff zero_extreal_def) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1257 |
also have "\<dots> = extreal r" using fin r by (auto simp: extreal_real) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1258 |
finally show "\<exists>r. (\<lambda>i. real (f i)) sums r" by (auto simp: sums_extreal) |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1259 |
qed |
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1260 |
|
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset
|
1261 |
end |