author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45051  c478d1876371 
child 47761  dfe747e72fa8 
permissions  rwrr 
41983  1 
(* Title: HOL/Multivariate_Analysis/Extended_Real_Limits.thy 
2 
Author: Johannes Hölzl, TU München 

3 
Author: Robert Himmelmann, TU München 

4 
Author: Armin Heller, TU München 

5 
Author: Bogdan Grechuk, University of Edinburgh 

6 
*) 

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

7 

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

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

9 

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

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

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

13 

43920  14 
lemma continuous_on_ereal[intro, simp]: "continuous_on A ereal" 
15 
unfolding continuous_on_topological open_ereal_def by auto 

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

16 

43920  17 
lemma continuous_at_ereal[intro, simp]: "continuous (at x) ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

18 
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

19 

43920  20 
lemma continuous_within_ereal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

21 
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

22 

43920  23 
lemma ereal_open_uminus: 
24 
fixes S :: "ereal set" 

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

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

26 
shows "open (uminus ` S)" 
43920  27 
unfolding open_ereal_def 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

28 
proof (intro conjI impI) 
43920  29 
obtain x y where S: "open (ereal ` S)" 
30 
"\<infinity> \<in> S \<Longrightarrow> {ereal x<..} \<subseteq> S" "\<infinity> \<in> S \<Longrightarrow> {..< ereal y} \<subseteq> S" 

31 
using `open S` unfolding open_ereal_def by auto 

32 
have "ereal ` uminus ` S = uminus ` (ereal ` S)" 

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

33 
proof safe 
43920  34 
fix x y assume "ereal x =  y" "y \<in> S" 
35 
then show "x \<in> uminus ` ereal ` S" by (cases y) auto 

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

36 
next 
43920  37 
fix x assume "ereal x \<in> S" 
38 
then show " x \<in> ereal ` uminus ` S" 

39 
by (auto intro: image_eqI[of _ _ "ereal x"]) 

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

40 
qed 
43920  41 
then show "open (ereal ` uminus ` S)" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

42 
using S by (auto intro: open_negations) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

43 
{ assume "\<infinity> \<in> uminus ` S" 
43920  44 
then have "\<infinity> \<in> S" by (metis image_iff ereal_uminus_uminus) 
45 
then have "uminus ` {..<ereal y} \<subseteq> uminus ` S" using S by (intro image_mono) auto 

46 
then show "\<exists>x. {ereal x<..} \<subseteq> uminus ` S" using ereal_uminus_lessThan by auto } 

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

47 
{ assume "\<infinity> \<in> uminus ` S" 
43920  48 
then have "\<infinity> : S" by (metis image_iff ereal_uminus_uminus) 
49 
then have "uminus ` {ereal x<..} <= uminus ` S" using S by (intro image_mono) auto 

50 
then show "\<exists>y. {..<ereal y} <= uminus ` S" using ereal_uminus_greaterThan by auto } 

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

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

52 

43920  53 
lemma ereal_uminus_complement: 
54 
fixes S :: "ereal set" 

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

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

56 
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

57 

43920  58 
lemma ereal_closed_uminus: 
59 
fixes S :: "ereal set" 

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

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

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

62 
using assms unfolding closed_def 
43920  63 
using ereal_open_uminus[of " S"] ereal_uminus_complement by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

64 

44571  65 
instance ereal :: perfect_space 
66 
proof (default, rule) 

67 
fix a :: ereal assume a: "open {a}" 

41980
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 
43920  71 
then obtain y where "{..<ereal y} <= {a}" using a open_MInfty2[of "{a}"] by auto 
72 
hence "ereal(y  1):{a}" apply (subst subsetD[of "{..<ereal y}"]) by auto 

41980
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 
43920  76 
then obtain y where "{ereal y<..} <= {a}" using a open_PInfty2[of "{a}"] by auto 
77 
hence "ereal(y+1):{a}" apply (subst subsetD[of "{ereal y<..}"]) by auto 

41980
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 
43920  81 
from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this 
41980
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" 
43920  83 
using fin ereal_between ereal_dense[of a "a+e"] by auto 
84 
then have "b: {ae <..< a+e}" using fin ereal_between[of a e] e by auto 

41980
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 

43920  89 
lemma ereal_closed_contains_Inf: 
90 
fixes S :: "ereal set" 

41980
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 
43920  98 
then obtain y where "{..<ereal y} <= (S)" using a open_MInfty2[of " S"] by auto 
99 
hence "ereal y <= Inf S" by (metis Compl_anti_mono Compl_lessThan atLeast_iff 

41980
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)) 
44918  104 
then show False using `Inf S ~: S` by (simp add: top_ereal_def) 
41980
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 
43920  107 
from ereal_open_cont_interval[OF a this] guess e . note e = this 
41980
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) 
43920  109 
hence *: "x>Inf Se" using e by (metis fin ereal_between(1) order_less_le_trans) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

110 
{ assume "x<Inf S+e" hence "x:{Inf Se <..< 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 

43920  118 
lemma ereal_closed_contains_Sup: 
119 
fixes S :: "ereal set" 

41980
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 
43920  123 
have "closed (uminus ` S)" by (metis assms(1) ereal_closed_uminus) 
124 
hence "Inf (uminus ` S) : uminus ` S" using assms ereal_closed_contains_Inf[of "uminus ` S"] by auto 

125 
hence " Sup S : uminus ` S" using ereal_Sup_uminus_image_eq[of "uminus ` S"] by (auto simp: image_image) 

126 
thus ?thesis by (metis imageI ereal_uminus_uminus ereal_minus_minus_image) 

41980
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 

43920  129 
lemma ereal_open_closed_aux: 
130 
fixes S :: "ereal set" 

41980
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 ~= {}" 
43920  136 
hence *: "(Inf S):S" by (metis assms(2) ereal_closed_contains_Inf) 
41980
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 ~= {}`) 
44571  140 
hence False by (metis assms(1) not_open_singleton) } 
41980
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>" 
43920  143 
from ereal_open_cont_interval[OF assms(1) * fin] guess e . note e = this 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

144 
then obtain b where b_def: "Inf Se<b & b<Inf S" 
43920  145 
using fin ereal_between[of "Inf S" e] ereal_dense[of "Inf Se"] by auto 
44918  146 
hence "b: {Inf Se <..< Inf S+e}" using e fin ereal_between[of "Inf S" e] 
147 
by auto 

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

148 
hence "b:S" using e by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

149 
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

150 
} ultimately show False by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

152 

43920  153 
lemma ereal_open_closed: 
154 
fixes S :: "ereal set" 

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

155 
shows "(open S & closed S) <> (S = {}  S = UNIV)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

157 
{ assume lhs: "open S & closed S" 
43920  158 
{ assume "(\<infinity>) ~: S" hence "S={}" using lhs ereal_open_closed_aux by auto } 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

159 
moreover 
43920  160 
{ assume "(\<infinity>) : S" hence "( S)={}" using lhs ereal_open_closed_aux[of "S"] by auto } 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

161 
ultimately have "S = {}  S = UNIV" by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

162 
} thus ?thesis by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

164 

43920  165 
lemma ereal_open_affinity_pos: 
43923  166 
fixes S :: "ereal set" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

167 
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

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

169 
proof  
43920  170 
obtain r where r[simp]: "m = ereal r" using m by (cases m) auto 
171 
obtain p where p[simp]: "t = ereal p" using t by auto 

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

172 
have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> \<infinity>" "m \<noteq> 0" using m by auto 
43920  173 
from `open S`[THEN ereal_openE] guess l u . note T = this 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

174 
let ?f = "(\<lambda>x. m * x + t)" 
43920  175 
show ?thesis unfolding open_ereal_def 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

176 
proof (intro conjI impI exI subsetI) 
43920  177 
have "ereal ` ?f ` S = (\<lambda>x. r * x + p) ` (ereal ` S)" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

178 
proof safe 
43920  179 
fix x y assume "ereal y = m * x + t" "x \<in> S" 
180 
then show "y \<in> (\<lambda>x. r * x + p) ` ereal ` S" 

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

181 
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

182 
qed force 
43920  183 
then show "open (ereal ` ?f ` S)" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

184 
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

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

186 
assume "\<infinity> \<in> ?f`S" with `0 < r` have "\<infinity> \<in> S" by auto 
43920  187 
fix x assume "x \<in> {ereal (r * l + p)<..}" 
188 
then have [simp]: "ereal (r * l + p) < x" by auto 

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

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

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

191 
show "x = m * ((x  t) / m) + t" 
43920  192 
using m t by (cases rule: ereal3_cases[of m x t]) auto 
193 
have "ereal l < (x  t)/m" 

194 
using m t by (simp add: ereal_less_divide_pos ereal_less_minus) 

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

195 
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

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

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

198 
assume "\<infinity> \<in> ?f`S" with `0 < r` have "\<infinity> \<in> S" by auto 
43920  199 
fix x assume "x \<in> {..<ereal (r * u + p)}" 
200 
then have [simp]: "x < ereal (r * u + p)" by auto 

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

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

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

203 
show "x = m * ((x  t) / m) + t" 
43920  204 
using m t by (cases rule: ereal3_cases[of m x t]) auto 
205 
have "(x  t)/m < ereal u" 

206 
using m t by (simp add: ereal_divide_less_pos ereal_minus_less) 

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

207 
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

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

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

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

211 

43920  212 
lemma ereal_open_affinity: 
43923  213 
fixes S :: "ereal set" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

214 
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

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

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

217 
assume "0 < m" then show ?thesis 
43920  218 
using ereal_open_affinity_pos[OF `open S` _ _ t, of m] m by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

220 
assume "\<not> 0 < m" then 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

221 
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

222 
then have m: "m \<noteq> \<infinity>" "0 < m" using `\<bar>m\<bar> \<noteq> \<infinity>` 
43920  223 
by (auto simp: ereal_uminus_eq_reorder) 
224 
from ereal_open_affinity_pos[OF ereal_open_uminus[OF `open S`] m t] 

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

225 
show ?thesis unfolding image_image by simp 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

227 

43920  228 
lemma ereal_lim_mult: 
229 
fixes X :: "'a \<Rightarrow> ereal" 

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

230 
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

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

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

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

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

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

236 
fix S assume "open S" "a * L \<in> S" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

237 
have "a * L / a = L" 
43920  238 
using `a \<noteq> 0` a by (cases rule: ereal2_cases[of a L]) auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

239 
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

240 
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

241 
moreover have "open ((\<lambda>x. x / a) ` S)" 
43920  242 
using ereal_open_affinity[OF `open S`, of "inverse a" 0] `a \<noteq> 0` a 
243 
by (auto simp: ereal_divide_eq ereal_inverse_eq_0 divide_ereal_def ac_simps) 

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

244 
note * = lim[THEN topological_tendstoD, OF this L] 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

245 
{ fix x from a `a \<noteq> 0` have "a * (x / a) = x" 
43920  246 
by (cases rule: ereal2_cases[of a x]) auto } 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

248 
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

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

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

252 

43920  253 
lemma ereal_lim_uminus: 
254 
fixes X :: "'a \<Rightarrow> ereal" shows "((\<lambda>i.  X i) > L) net \<longleftrightarrow> (X > L) net" 

255 
using ereal_lim_mult[of X L net "ereal (1)"] 

256 
ereal_lim_mult[of "(\<lambda>i.  X i)" "L" net "ereal (1)"] 

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

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

258 

43920  259 
lemma Lim_bounded2_ereal: 
260 
assumes lim:"f > (l :: ereal)" 

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

261 
and ge: "ALL n>=N. f n >= C" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

262 
shows "l>=C" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

264 
def g == "(%i. (f i))" 
43920  265 
{ fix n assume "n>=N" hence "g n <= C" using assms ereal_minus_le_minus g_def by auto } 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

266 
hence "ALL n>=N. g n <= C" by auto 
43920  267 
moreover have limg: "g > (l)" using g_def ereal_lim_uminus lim by auto 
268 
ultimately have "l <= C" using Lim_bounded_ereal[of g "l" _ "C"] by auto 

269 
from this show ?thesis using ereal_minus_le_minus by auto 

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

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

271 

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

272 

43923  273 
lemma ereal_open_atLeast: fixes x :: ereal shows "open {x..} \<longleftrightarrow> x = \<infinity>" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

275 
assume "x = \<infinity>" then have "{x..} = UNIV" by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

276 
then show "open {x..}" by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

278 
assume "open {x..}" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

279 
then have "open {x..} \<and> closed {x..}" by auto 
43920  280 
then have "{x..} = UNIV" unfolding ereal_open_closed by auto 
281 
then show "x = \<infinity>" by (simp add: bot_ereal_def atLeast_eq_UNIV_iff) 

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

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

283 

43920  284 
lemma ereal_open_mono_set: 
285 
fixes S :: "ereal set" 

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

286 
defines "a \<equiv> Inf S" 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

287 
shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {a <..})" 
43920  288 
by (metis Inf_UNIV a_def atLeast_eq_UNIV_iff ereal_open_atLeast 
289 
ereal_open_closed mono_set_iff open_ereal_greaterThan) 

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

290 

43920  291 
lemma ereal_closed_mono_set: 
292 
fixes S :: "ereal set" 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

293 
shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})" 
43920  294 
by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast 
295 
ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan) 

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

296 

43920  297 
lemma ereal_Liminf_Sup_monoset: 
298 
fixes f :: "'a => ereal" 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

299 
shows "Liminf net f = Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

301 
proof (intro arg_cong[where f="\<lambda>P. Sup (Collect P)"] ext iffI allI impI) 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

302 
fix l S assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono_set S" "l \<in> S" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

303 
then have "S = UNIV \<or> S = {Inf S <..}" 
43920  304 
using ereal_open_mono_set[of S] by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

305 
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

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

307 
assume S: "S = {Inf S<..}" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

308 
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

309 
then have "eventually (\<lambda>x. Inf S < f x) net" using ev by auto 
44918  310 
then show "eventually (\<lambda>x. f x \<in> S) net" by (subst S) auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

312 
next 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

313 
fix l y assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net" "y < l" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

314 
have "eventually (\<lambda>x. f x \<in> {y <..}) net" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

315 
using `y < l` by (intro S[rule_format]) auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

316 
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

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

318 

43920  319 
lemma ereal_Limsup_Inf_monoset: 
320 
fixes f :: "'a => ereal" 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

321 
shows "Limsup net f = Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

323 
proof (intro arg_cong[where f="\<lambda>P. Inf (Collect P)"] ext iffI allI impI) 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

324 
fix l S assume ev: "\<forall>y>l. eventually (\<lambda>x. f x < y) net" and "open S" "mono_set (uminus`S)" "l \<in> S" 
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

325 
then have "open (uminus`S) \<and> mono_set (uminus`S)" by (simp add: ereal_open_uminus) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

326 
then have "S = UNIV \<or> S = {..< Sup S}" 
43920  327 
unfolding ereal_open_mono_set ereal_Inf_uminus_image_eq ereal_image_uminus_shift by simp 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

328 
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

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

330 
assume S: "S = {..< Sup S}" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

331 
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

332 
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

333 
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

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

335 
next 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

336 
fix l y assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus`S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net" "l < y" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

337 
have "eventually (\<lambda>x. f x \<in> {..< y}) net" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

338 
using `l < y` by (intro S[rule_format]) auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

339 
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

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

341 

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

342 

43920  343 
lemma open_uminus_iff: "open (uminus ` S) \<longleftrightarrow> open (S::ereal set)" 
344 
using ereal_open_uminus[of S] ereal_open_uminus[of "uminus`S"] by auto 

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

345 

43920  346 
lemma ereal_Limsup_uminus: 
347 
fixes f :: "'a => ereal" 

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

348 
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

349 
proof  
43920  350 
{ fix P l have "(\<exists>x. (l::ereal) = x \<and> P x) \<longleftrightarrow> P (l)" by (auto intro!: exI[of _ "l"]) } 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

351 
note Ex_cancel = this 
43920  352 
{ fix P :: "ereal set \<Rightarrow> bool" have "(\<forall>S. P S) \<longleftrightarrow> (\<forall>S. P (uminus`S))" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

353 
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

354 
note add_uminus_image = this 
43920  355 
{ fix x S have "(x::ereal) \<in> uminus`S \<longleftrightarrow> x\<in>S" by (auto intro!: image_eqI[of _ _ "x"]) } 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

356 
note remove_uminus_image = this 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

357 
show ?thesis 
43920  358 
unfolding ereal_Limsup_Inf_monoset ereal_Liminf_Sup_monoset 
359 
unfolding ereal_Inf_uminus_image_eq[symmetric] image_Collect Ex_cancel 

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

360 
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

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

362 

43920  363 
lemma ereal_Liminf_uminus: 
364 
fixes f :: "'a => ereal" 

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

365 
shows "Liminf net (\<lambda>x.  (f x)) = (Limsup net f)" 
43920  366 
using ereal_Limsup_uminus[of _ "(\<lambda>x.  (f x))"] by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

367 

43920  368 
lemma ereal_Lim_uminus: 
369 
fixes f :: "'a \<Rightarrow> ereal" shows "(f > f0) net \<longleftrightarrow> ((\<lambda>x.  f x) >  f0) net" 

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

370 
using 
43920  371 
ereal_lim_mult[of f f0 net " 1"] 
372 
ereal_lim_mult[of "\<lambda>x.  (f x)" "f0" net " 1"] 

373 
by (auto simp: ereal_uminus_reorder) 

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

374 

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

375 
lemma lim_imp_Limsup: 
43920  376 
fixes f :: "'a => ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

378 
assumes lim: "(f > f0) net" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

379 
shows "Limsup net f = f0" 
43920  380 
using ereal_Lim_uminus[of f f0] lim_imp_Liminf[of net "(%x. (f x))" "f0"] 
381 
ereal_Liminf_uminus[of net f] assms by simp 

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

382 

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

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

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

386 
shows "(f > \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

387 
proof (intro lim_imp_Liminf iffI assms) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

388 
assume rhs: "Liminf net f = \<infinity>" 
43923  389 
{ fix S :: "ereal set" assume "open S & \<infinity> : S" 
43920  390 
then obtain m where "{ereal m<..} <= S" using open_PInfty2 by auto 
391 
moreover have "eventually (\<lambda>x. f x \<in> {ereal m<..}) net" 

392 
using rhs unfolding Liminf_Sup top_ereal_def[symmetric] Sup_eq_top_iff 

393 
by (auto elim!: allE[where x="ereal m"] simp: top_ereal_def) 

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

394 
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

395 
} 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

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

397 

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

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

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

401 
shows "(f > \<infinity>) net \<longleftrightarrow> Limsup net f = \<infinity>" 
43920  402 
using assms ereal_Lim_uminus[of f "\<infinity>"] Liminf_PInfty[of _ "\<lambda>x.  (f x)"] 
403 
ereal_Liminf_uminus[of _ f] by (auto simp: ereal_uminus_eq_reorder) 

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

404 

43920  405 
lemma ereal_Liminf_eq_Limsup: 
406 
fixes f :: "'a \<Rightarrow> ereal" 

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

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

408 
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

409 
shows "(f > f0) net" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

410 
proof (cases f0) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

411 
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

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

413 
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

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

415 
case (real r) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

416 
show "(f > f0) net" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

418 
fix S assume "open S""f0 \<in> S" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

419 
then obtain a b where "a < Liminf net f" "Limsup net f < b" "{a<..<b} \<subseteq> S" 
43920  420 
using ereal_open_cont_interval2[of S f0] real lim by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

421 
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

422 
unfolding Liminf_Sup Limsup_Inf less_Sup_iff Inf_less_iff 
44142  423 
by (auto intro!: eventually_conj) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

424 
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

425 
by (rule_tac eventually_mono) auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

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

428 

43920  429 
lemma ereal_Liminf_eq_Limsup_iff: 
430 
fixes f :: "'a \<Rightarrow> ereal" 

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

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

432 
shows "(f > f0) net \<longleftrightarrow> Liminf net f = f0 \<and> Limsup net f = f0" 
43920  433 
by (metis assms ereal_Liminf_eq_Limsup lim_imp_Liminf lim_imp_Limsup) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

434 

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

435 
lemma limsup_INFI_SUPR: 
43920  436 
fixes f :: "nat \<Rightarrow> ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

437 
shows "limsup f = (INF n. SUP m:{n..}. f m)" 
43920  438 
using ereal_Limsup_uminus[of sequentially "\<lambda>x.  f x"] 
439 
by (simp add: liminf_SUPR_INFI ereal_INFI_uminus ereal_SUPR_uminus) 

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

440 

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

441 
lemma liminf_PInfty: 
43920  442 
fixes X :: "nat => ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

443 
shows "X > \<infinity> <> liminf X = \<infinity>" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

445 

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

446 
lemma limsup_MInfty: 
43920  447 
fixes X :: "nat => ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

448 
shows "X > (\<infinity>) <> limsup X = (\<infinity>)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

450 

43920  451 
lemma ereal_lim_mono: 
452 
fixes X Y :: "nat => ereal" 

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

453 
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

454 
assumes "X > x" "Y > y" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

455 
shows "x <= y" 
43920  456 
by (metis ereal_Liminf_eq_Limsup_iff[OF trivial_limit_sequentially] assms liminf_mono) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

457 

43920  458 
lemma incseq_le_ereal: 
459 
fixes X :: "nat \<Rightarrow> ereal" 

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

460 
assumes inc: "incseq X" and lim: "X > L" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

461 
shows "X N \<le> L" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

462 
using inc 
44125  463 
by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

464 

43920  465 
lemma decseq_ge_ereal: assumes dec: "decseq X" 
466 
and lim: "X > (L::ereal)" shows "X N >= L" 

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

467 
using dec 
44125  468 
by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

469 

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

470 
lemma liminf_bounded_open: 
43920  471 
fixes x :: "nat \<Rightarrow> ereal" 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

472 
shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

473 
(is "_ \<longleftrightarrow> ?P x0") 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

475 
assume "?P x0" then show "x0 \<le> liminf x" 
43920  476 
unfolding ereal_Liminf_Sup_monoset eventually_sequentially 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

477 
by (intro complete_lattice_class.Sup_upper) auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

479 
assume "x0 \<le> liminf x" 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

480 
{ fix S :: "ereal set" assume om: "open S & mono_set S & x0:S" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

481 
{ 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

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

483 
{ assume "~(S=UNIV)" 
43920  484 
then obtain B where B_def: "S = {B<..}" using om ereal_open_mono_set by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

485 
hence "B<x0" using om by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

486 
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

487 
} 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

488 
} then show "?P x0" by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

490 

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

491 
lemma limsup_subseq_mono: 
43920  492 
fixes X :: "nat \<Rightarrow> ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

493 
assumes "subseq r" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

494 
shows "limsup (X \<circ> r) \<le> limsup X" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

496 
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

497 
then have " limsup X \<le>  limsup (X \<circ> r)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

498 
using liminf_subseq_mono[of r "(%n.  X n)"] 
43920  499 
ereal_Liminf_uminus[of sequentially X] 
500 
ereal_Liminf_uminus[of sequentially "X o r"] assms by auto 

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

501 
then show ?thesis by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

503 

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

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

505 
assumes "(a::real)<=x" "x<=b" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

506 
shows "abs x <= max (abs a) (abs b)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

507 
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

508 

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

509 
lemma bounded_increasing_convergent2: fixes f::"nat => real" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

510 
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

511 
shows "EX l. (f > l) sequentially" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

513 
def N == "max (abs (f 0)) (abs B)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

514 
{ 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

515 
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

516 
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

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

518 
qed 
43920  519 
lemma lim_ereal_increasing: assumes "\<And>n m. n >= m \<Longrightarrow> f n >= f m" 
520 
obtains l where "f > (l::ereal)" 

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

521 
proof(cases "f = (\<lambda>x.  \<infinity>)") 
44125  522 
case True then show thesis using tendsto_const[of " \<infinity>" sequentially] by (intro that[of "\<infinity>"]) auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

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

525 
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

526 
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

527 
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

528 
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

529 
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

530 
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

531 
show thesis 
43920  532 
proof(cases "EX B. ALL n. f n < ereal B") 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

533 
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

534 
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

535 
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

536 
next case True then guess B .. 
43920  537 
hence "ALL n. Y n < ereal B" using Y_def by auto note B = this[rule_format] 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

538 
{ 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

539 
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

540 
} 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

541 
{ fix n have "real (Y n) < B" proof case goal1 thus ?case 
43920  542 
using B[of n] applyapply(subst(asm) ereal_real'[THEN sym]) defer defer 
543 
unfolding ereal_less using * by auto 

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

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

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

546 
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

547 
have "EX l. (%n. real (Y n)) > l" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

548 
apply(rule bounded_increasing_convergent2) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

549 
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

550 
fix n m::nat assume "n<=m" 
43920  551 
hence "ereal (real (Y n)) <= ereal (real (Y m))" 
552 
using incy[rule_format,of n m] apply(subst ereal_real)+ 

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

553 
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

554 
thus "real (Y n) <= real (Y m)" by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

555 
qed then guess l .. note l=this 
43920  556 
have "Y > ereal l" using l applyapply(subst(asm) lim_ereal[THEN sym]) 
557 
unfolding ereal_real using * by auto 

558 
thus thesis applyapply(rule that[of "ereal l"]) 

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

559 
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

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

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

562 

43920  563 
lemma lim_ereal_decreasing: assumes "\<And>n m. n >= m \<Longrightarrow> f n <= f m" 
564 
obtains l where "f > (l::ereal)" 

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

565 
proof  
43920  566 
from lim_ereal_increasing[of "\<lambda>x.  f x"] assms 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

567 
obtain l where "(\<lambda>x.  f x) > l" by auto 
43920  568 
from ereal_lim_mult[OF this, of " 1"] show thesis 
569 
by (intro that[of "l"]) (simp add: ereal_uminus_eq_reorder) 

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

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

571 

43920  572 
lemma compact_ereal: 
573 
fixes X :: "nat \<Rightarrow> ereal" 

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

574 
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

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

576 
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

577 
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

578 
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

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

580 
then obtain l where "(X\<circ>r) > l" 
43920  581 
using lim_ereal_increasing[of "X \<circ> r"] lim_ereal_decreasing[of "X \<circ> r"] by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

582 
then show ?thesis using `subseq r` by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

584 

43920  585 
lemma ereal_Sup_lim: 
586 
assumes "\<And>n. b n \<in> s" "b > (a::ereal)" 

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

587 
shows "a \<le> Sup s" 
43920  588 
by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

589 

43920  590 
lemma ereal_Inf_lim: 
591 
assumes "\<And>n. b n \<in> s" "b > (a::ereal)" 

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

592 
shows "Inf s \<le> a" 
43920  593 
by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

594 

43920  595 
lemma SUP_Lim_ereal: 
596 
fixes X :: "nat \<Rightarrow> ereal" assumes "incseq X" "X > l" shows "(SUP n. X n) = l" 

597 
proof (rule ereal_SUPI) 

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

598 
fix n from assms show "X n \<le> l" 
43920  599 
by (intro incseq_le_ereal) (simp add: incseq_def) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

601 
fix y assume "\<And>n. n \<in> UNIV \<Longrightarrow> X n \<le> y" 
43920  602 
with ereal_Sup_lim[OF _ `X > l`, of "{..y}"] 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

603 
show "l \<le> y" by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

605 

43920  606 
lemma LIMSEQ_ereal_SUPR: 
607 
fixes X :: "nat \<Rightarrow> ereal" assumes "incseq X" shows "X > (SUP n. X n)" 

608 
proof (rule lim_ereal_increasing) 

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

609 
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

610 
using `incseq X` by (simp add: incseq_def) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

612 
fix l assume "X > l" 
43920  613 
with SUP_Lim_ereal[of X, OF assms this] show ?thesis by simp 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

615 

43920  616 
lemma INF_Lim_ereal: "decseq X \<Longrightarrow> X > l \<Longrightarrow> (INF n. X n) = (l::ereal)" 
617 
using SUP_Lim_ereal[of "\<lambda>i.  X i" " l"] 

618 
by (simp add: ereal_SUPR_uminus ereal_lim_uminus) 

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

619 

43920  620 
lemma LIMSEQ_ereal_INFI: "decseq X \<Longrightarrow> X > (INF n. X n :: ereal)" 
621 
using LIMSEQ_ereal_SUPR[of "\<lambda>i.  X i"] 

622 
by (simp add: ereal_SUPR_uminus ereal_lim_uminus) 

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

623 

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

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

625 
assumes "mono f" 
43920  626 
shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f > x" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

629 
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

630 
{ assume "f > x" 
43920  631 
then have "(\<lambda>i. ereal (f i)) > ereal x" by auto 
632 
from SUP_Lim_ereal[OF inc this] 

633 
show "(SUP n. ereal (f n)) = ereal x" . } 

634 
{ assume "(SUP n. ereal (f n)) = ereal x" 

635 
with LIMSEQ_ereal_SUPR[OF inc] 

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

636 
show "f > x" by auto } 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

638 

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

639 
lemma Liminf_within: 
43920  640 
fixes f :: "'a::metric_space => ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

641 
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

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

643 
let ?l="(SUP e:{0<..}. INF y:(S Int ball x e  {x}). f y)" 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

644 
{ fix T assume T_def: "open T & mono_set T & ?l:T" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

645 
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

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

647 
{ 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

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

649 
{ assume "~(T=UNIV)" 
43920  650 
then obtain B where "T={B<..}" using T_def ereal_open_mono_set[of T] by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

651 
hence "B<?l" using T_def by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

652 
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

653 
unfolding less_SUP_iff by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

654 
{ 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

655 
hence "y:(S Int ball x d  {x})" unfolding ball_def by (auto simp add: dist_commute) 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44918
diff
changeset

656 
hence "f y:T" using d_def INF_lower[of y "S Int ball x d  {x}" f] `T={B<..}` by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

657 
} 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

658 
} ultimately show ?thesis by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

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

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

662 
{ fix z 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

663 
assume a: "ALL T. open T > mono_set T > z : T > 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

665 
{ fix B assume "B<z" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

666 
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

667 
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

668 
{ 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

669 
hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute) 
45051
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45032
diff
changeset

670 
by (metis dist_eq_0_iff less_le zero_le_dist) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

671 
hence "B <= f y" using d_def by auto 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44918
diff
changeset

672 
} hence "B <= INFI (S Int ball x d  {x}) f" apply (subst INF_greatest) by auto 
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44918
diff
changeset

673 
also have "...<=?l" apply (subst SUP_upper) using d_def by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

674 
finally have "B<=?l" by auto 
43920  675 
} hence "z <= ?l" using ereal_le_ereal[of z "?l"] by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

676 
} 
43920  677 
ultimately show ?thesis unfolding ereal_Liminf_Sup_monoset eventually_within 
678 
apply (subst ereal_SupI[of _ "(SUP e:{0<..}. INFI (S Int ball x e  {x}) f)"]) by auto 

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

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

680 

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

681 
lemma Limsup_within: 
43920  682 
fixes f :: "'a::metric_space => ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

683 
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

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

685 
let ?l="(INF e:{0<..}. SUP y:(S Int ball x e  {x}). f y)" 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

686 
{ fix T assume T_def: "open T & mono_set (uminus ` T) & ?l:T" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

687 
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

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

689 
{ 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

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

691 
{ assume "~(T=UNIV)" hence "~(uminus ` T = UNIV)" 
43920  692 
by (metis Int_UNIV_right Int_absorb1 image_mono ereal_minus_minus_image subset_UNIV) 
693 
hence "uminus ` T = {Inf (uminus ` T)<..}" using T_def ereal_open_mono_set[of "uminus ` T"] 

694 
ereal_open_uminus[of T] by auto 

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

695 
then obtain B where "T={..<B}" 
43920  696 
unfolding ereal_Inf_uminus_image_eq ereal_uminus_lessThan[symmetric] 
697 
unfolding inj_image_eq_iff[OF ereal_inj_on_uminus] by simp 

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

698 
hence "?l<B" using T_def by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

699 
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

700 
unfolding INF_less_iff by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

701 
{ 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

702 
hence "y:(S Int ball x d  {x})" unfolding ball_def by (auto simp add: dist_commute) 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44918
diff
changeset

703 
hence "f y:T" using d_def SUP_upper[of y "S Int ball x d  {x}" f] `T={..<B}` by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

704 
} 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

705 
} ultimately show ?thesis by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

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

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

709 
{ fix z 
44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
44167
diff
changeset

710 
assume a: "ALL T. open T > mono_set (uminus ` T) > z : T > 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

712 
{ fix B assume "z<B" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

713 
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

714 
using a[rule_format, of "{..<B}"] by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

715 
{ 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

716 
hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute) 
45051
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45032
diff
changeset

717 
by (metis dist_eq_0_iff less_le zero_le_dist) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

718 
hence "f y <= B" using d_def by auto 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44918
diff
changeset

719 
} hence "SUPR (S Int ball x d  {x}) f <= B" apply (subst SUP_least) by auto 
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44918
diff
changeset

720 
moreover have "?l<=SUPR (S Int ball x d  {x}) f" apply (subst INF_lower) using d_def by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

721 
ultimately have "?l<=B" by auto 
43920  722 
} hence "?l <= z" using ereal_ge_ereal[of z "?l"] by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

723 
} 
43920  724 
ultimately show ?thesis unfolding ereal_Limsup_Inf_monoset eventually_within 
725 
apply (subst ereal_InfI) by auto 

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

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

727 

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

728 

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

729 
lemma Liminf_within_UNIV: 
43920  730 
fixes f :: "'a::metric_space => ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

731 
shows "Liminf (at x) f = Liminf (at x within UNIV) f" 
45031  732 
by simp (* TODO: delete *) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

733 

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

734 

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

735 
lemma Liminf_at: 
43920  736 
fixes f :: "'a::metric_space => ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

737 
shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e  {x}). f y)" 
45031  738 
using Liminf_within[of x UNIV f] by simp 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

739 

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

740 

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

741 
lemma Limsup_within_UNIV: 
43920  742 
fixes f :: "'a::metric_space => ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

743 
shows "Limsup (at x) f = Limsup (at x within UNIV) f" 
45031  744 
by simp (* TODO: delete *) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

745 

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

746 

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

747 
lemma Limsup_at: 
43920  748 
fixes f :: "'a::metric_space => ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

749 
shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e  {x}). f y)" 
45031  750 
using Limsup_within[of x UNIV f] by simp 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

751 

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

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

753 
assumes "ALL y:S. f y = C" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

754 
shows "(f > C) (at x within S)" 
45032  755 
unfolding tendsto_def Limits.eventually_within eventually_at_topological 
756 
using assms by simp (metis open_UNIV UNIV_I) 

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

757 

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

758 
lemma Liminf_within_constant: 
45032  759 
fixes f :: "'a::topological_space \<Rightarrow> ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

760 
assumes "ALL y:S. f y = C" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

761 
assumes "~trivial_limit (at x within S)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

762 
shows "Liminf (at x within S) f = C" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

763 
by (metis Lim_within_constant assms lim_imp_Liminf) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

764 

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

765 
lemma Limsup_within_constant: 
45032  766 
fixes f :: "'a::topological_space \<Rightarrow> ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

767 
assumes "ALL y:S. f y = C" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

768 
assumes "~trivial_limit (at x within S)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

769 
shows "Limsup (at x within S) f = C" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

770 
by (metis Lim_within_constant assms lim_imp_Limsup) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

771 

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

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

773 
"x islimpt S = x islimpt (S{x})" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

774 
unfolding islimpt_def by blast 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

775 

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

776 

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

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

778 
"(x islimpt S) = (x:closure(S{x}))" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

779 
unfolding closure_def using islimpt_punctured by blast 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

780 

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

781 

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

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

783 
"~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

784 
using islimpt_in_closure by (metis trivial_limit_within) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

785 

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

786 

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

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

788 
"(~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

789 
(is "?lhs = ?rhs") 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

791 
{ assume "?lhs" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

792 
{ fix e :: real assume "e>0" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

793 
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

794 
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

795 
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

796 
hence "S Int ball x e  {x} ~= {}" by blast 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

797 
} hence "?rhs" by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

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

800 
{ assume "?rhs" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

801 
{ fix e :: real assume "e>0" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

802 
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

803 
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

804 
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

805 
} 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

806 
} ultimately show ?thesis by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

808 

43920  809 
lemma liminf_ereal_cminus: 
810 
fixes f :: "nat \<Rightarrow> ereal" assumes "c \<noteq> \<infinity>" 

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

811 
shows "liminf (\<lambda>x. c  f x) = c  limsup f" 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

812 
proof (cases c) 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

813 
case PInf then show ?thesis by (simp add: Liminf_const) 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

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

815 
case (real r) then show ?thesis 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
41983
diff
changeset

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

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

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

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

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

823 

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

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

825 

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

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

827 
assumes "continuous (at x0) f" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

828 
assumes "x > x0" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

829 
shows "(f o x) > (f x0)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

831 
{ fix S assume "open S & (f x0):S" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

832 
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

833 
using assms continuous_at_open by metis 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

834 
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

835 
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

836 
} 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

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

838 

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_sequentially2: 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

841 
fixes f :: "'a::metric_space => 'b:: topological_space" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

842 
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

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

844 
{ assume "~(continuous (at x0) f)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

845 
from this obtain T where T_def: 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

846 
"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

847 
using continuous_at_open[of x0 f] by metis 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

848 
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

849 
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

850 
using islimpt_sequential[of x0 X] by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

851 
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

852 
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

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

854 
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

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

856 

43920  857 
lemma continuous_at_of_ereal: 
858 
fixes x0 :: ereal 

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

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

860 
shows "continuous (at x0) real" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

862 
{ fix T assume T_def: "open T & real x0 : T" 
43920  863 
def S == "ereal ` T" 
864 
hence "ereal (real x0) : S" using T_def by auto 

865 
hence "x0 : S" using assms ereal_real by auto 

866 
moreover have "open S" using open_ereal S_def T_def by auto 

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

867 
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

868 
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

869 
} 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

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 

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

874 
fixes f :: "'a::t2_space => real" 
43920  875 
shows "continuous (at x0) f <> continuous (at x0) (ereal o f)" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

876 
proof 
43920  877 
{ assume "continuous (at x0) f" hence "continuous (at x0) (ereal o f)" 
878 
using continuous_at_ereal continuous_at_compose[of x0 f ereal] by auto 

41980
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 
moreover 
43920  881 
{ assume "continuous (at x0) (ereal o f)" 
882 
hence "continuous (at x0) (real o (ereal o f))" 

883 
using continuous_at_of_ereal by (intro continuous_at_compose[of x0 "ereal o f"]) auto 

884 
moreover have "real o (ereal o f) = f" using real_ereal_id by (simp add: o_assoc) 

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

885 
ultimately have "continuous (at x0) f" by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

886 
} ultimately show ?thesis by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

888 

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

889 

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

891 
fixes f :: "'a::t2_space => real" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

892 
fixes A assumes "open A" 
43920  893 
shows "continuous_on A f <> continuous_on A (ereal o f)" 
894 
using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at) 

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

895 

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

896 

43923  897 
lemma continuous_on_real: "continuous_on (UNIV{\<infinity>,(\<infinity>::ereal)}) real" 
43920  898 
using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

899 

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

900 

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

901 
lemma continuous_on_iff_real: 
43920  902 
fixes f :: "'a::t2_space => ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

903 
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

904 
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

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

906 
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

907 
hence *: "continuous_on (f ` A) real" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

908 
using continuous_on_real by (simp add: continuous_on_subset) 
43920  909 
have **: "continuous_on ((real o f) ` A) ereal" 
910 
using continuous_on_ereal continuous_on_subset[of "UNIV" "ereal" "(real o f) ` A"] by blast 

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

911 
{ 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

912 
apply (subst continuous_on_compose) using * by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

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

915 
{ assume "continuous_on A (real o f)" 
43920  916 
hence "continuous_on A (ereal o (real o f))" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

917 
apply (subst continuous_on_compose) using ** by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

918 
hence "continuous_on A f" 
43920  919 
apply (subst continuous_on_eq[of A "ereal o (real o f)" f]) 
920 
using assms ereal_real by auto 

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

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

922 
ultimately show ?thesis by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

924 

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

925 

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

926 
lemma continuous_at_const: 
43920  927 
fixes f :: "'a::t2_space => ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

928 
assumes "ALL x. (f x = C)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

929 
shows "ALL x. continuous (at x) f" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

930 
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

931 

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

932 

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

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

934 
fixes S :: "real set" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

935 
assumes "S ~= {}" "EX B. ALL x:S. B<=x" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

936 
shows "Inf S : closure S" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

938 
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

939 
{ fix e assume "e>(0 :: real)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

940 
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

941 
moreover hence "x > Inf S  e" using * by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

942 
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

943 
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

944 
} 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

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

946 

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

947 

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

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

949 
fixes S :: "real set" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

950 
assumes "S ~= {}" "EX B. ALL x:S. B<=x" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

952 
shows "Inf S : S" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

953 
by (metis closure_contains_Inf closure_closed assms) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

954 

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

955 

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

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

957 
fixes S :: "real set" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

958 
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

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

960 
shows "S = {}  S = UNIV  (EX a. S = {a ..})" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

962 
{ assume "S ~= {}" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

963 
{ assume ex: "EX B. ALL x:S. B<=x" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

964 
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

965 
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

966 
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

967 
hence "S = {Inf S ..}" by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

968 
hence "EX a. S = {a ..}" by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

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

971 
{ assume "~(EX B. ALL x:S. B<=x)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

972 
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

973 
{ 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

974 
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

975 
} hence "S = UNIV" by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

976 
} 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

977 
} from this show ?thesis by blast 
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 

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

982 
fixes S :: "real set" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

983 
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

984 
assumes "closed S" 
43920  985 
shows "EX a. S = {x. a <= ereal x}" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

987 
{ 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

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

989 
{ 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

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

991 
{ assume "EX a. S = {a ..}" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

992 
from this obtain a where "S={a ..}" by auto 
43920  993 
hence ?thesis apply(rule_tac x="ereal a" in exI) by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

994 
} 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

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

996 

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

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

998 

43920  999 
lemma setsum_ereal[simp]: 
1000 
"(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)" 

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

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

1002 
assume "finite A" then show ?thesis by induct auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

1004 

43923  1005 
lemma setsum_Pinfty: 
1006 
fixes f :: "'a \<Rightarrow> ereal" 

1007 
shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> (finite P \<and> (\<exists>i\<in>P. f i = \<infinity>))" 

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

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

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

1010 
show "finite P" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1011 
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

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

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

1014 
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

1015 
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

1016 
by induct auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1017 
with * show False by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

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

1020 
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

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

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

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

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

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

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

1027 

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

1028 
lemma setsum_Inf: 
43923  1029 
fixes f :: "'a \<Rightarrow> ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1030 
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

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

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

1033 
have "finite A" by (rule ccontr) (insert *, auto) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1034 
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

1035 
proof (rule ccontr) 
43920  1036 
assume "\<not> ?thesis" then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1037 
from bchoice[OF this] guess r .. 
44142  1038 
with * show False by auto 
41980
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 
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

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

1042 
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

1043 
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

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

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

1046 
case (insert j A) then show ?case 
43920  1047 
by (cases rule: ereal3_cases[of "f i" "f j" "setsum f A"]) auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

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

1050 

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

1053 
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

1054 
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

1055 
proof  
43920  1056 
have "\<forall>x\<in>S. \<exists>r. f x = ereal r" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

1058 
fix x assume "x \<in> S" 
43920  1059 
from assms[OF this] show "\<exists>r. f x = ereal r" by (cases "f x") auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

1061 
from bchoice[OF this] guess r .. 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1062 
then show ?thesis by simp 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

1064 

43920  1065 
lemma setsum_ereal_0: 
1066 
fixes f :: "'a \<Rightarrow> ereal" assumes "finite A" "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i" 

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

1067 
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

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

1069 
assume *: "(\<Sum>x\<in>A. f x) = 0" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1070 
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

1071 
then have "\<forall>i\<in>A. \<bar>f i\<bar> \<noteq> \<infinity>" using assms by (force simp: setsum_Pinfty) 
43920  1072 
then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" by auto 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1073 
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

1074 
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

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

1076 

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

1077 

43920  1078 
lemma setsum_ereal_right_distrib: 
1079 
fixes f :: "'a \<Rightarrow> ereal" assumes "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i" 

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

1080 
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

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

1082 
assume "finite A" then show ?thesis using assms 
43920  1083 
by induct (auto simp: ereal_right_distrib setsum_nonneg) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

1085 

43920  1086 
lemma sums_ereal_positive: 
1087 
fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>i. 0 \<le> f i" shows "f sums (SUP n. \<Sum>i<n. f i)" 

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

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

1089 
have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)" 
43920  1090 
using ereal_add_mono[OF _ assms] by (auto intro!: incseq_SucI) 
1091 
from LIMSEQ_ereal_SUPR[OF this] 

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

1092 
show ?thesis unfolding sums_def by (simp add: atLeast0LessThan) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

1094 

43920  1095 
lemma summable_ereal_pos: 
1096 
fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>i. 0 \<le> f i" shows "summable f" 

1097 
using sums_ereal_positive[of f, OF assms] unfolding summable_def by auto 

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

1098 

43920  1099 
lemma suminf_ereal_eq_SUPR: 
1100 
fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>i. 0 \<le> f i" 

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

1101 
shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)" 
43920  1102 
using sums_ereal_positive[of f, OF assms, THEN sums_unique] by simp 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1103 

43920  1104 
lemma sums_ereal: 
1105 
"(\<lambda>x. ereal (f x)) sums ereal x \<longleftrightarrow> f sums x" 

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

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

1107 

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

1108 
lemma suminf_bound: 
43920  1109 
fixes f :: "nat \<Rightarrow> ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1110 
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

1111 
shows "suminf f \<le> x" 
43920  1112 
proof (rule Lim_bounded_ereal) 
1113 
have "summable f" using pos[THEN summable_ereal_pos] . 

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

1114 
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

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

1116 
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

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

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

1119 

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

1120 
lemma suminf_bound_add: 
43920  1121 
fixes f :: "nat \<Rightarrow> ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1122 
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

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

1124 
proof (cases y) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1125 
case (real r) then have "\<forall>N. (\<Sum>n<N. f n) \<le> x  y" 
43920  1126 
using assms by (simp add: ereal_le_minus) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1127 
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

1128 
then show "(\<Sum> n. f n) + y \<le> x" 
43920  1129 
using assms real by (simp add: ereal_le_minus) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

1131 

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

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

1133 
assumes "\<forall>N\<ge>n. f N = 0" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1134 
shows "f sums (\<Sum>N<n. f N)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

1136 
{ 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

1137 
by (induct i) (insert assms, auto) } 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

1139 
show ?thesis unfolding sums_def 
44125  1140 
by (rule LIMSEQ_offset[of _ n]) (auto simp add: atLeast0LessThan intro: tendsto_const) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

1142 

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

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

1144 
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

1145 
shows "suminf f = (\<Sum>N<n. f N)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1146 
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

1147 

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

1148 
lemma suminf_upper: 
43920  1149 
fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>n. 0 \<le> f n" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1150 
shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)" 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44918
diff
changeset

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

1153 

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

1154 
lemma suminf_0_le: 
43920  1155 
fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>n. 0 \<le> f n" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1156 
shows "0 \<le> (\<Sum>n. f n)" 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1157 
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

1158 

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

1159 
lemma suminf_le_pos: 
43920  1160 
fixes f g :: "nat \<Rightarrow> ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1161 
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

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

1163 
proof (safe intro!: suminf_bound) 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1164 
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

1165 
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

1166 
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

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

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

1169 

43920  1170 
lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal)^Suc n) = 1" 
1171 
using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric] 

1172 
by (simp add: one_ereal_def) 

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

1173 

43920  1174 
lemma suminf_add_ereal: 
1175 
fixes f g :: "nat \<Rightarrow> ereal" 

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

1176 
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

1177 
shows "(\<Sum>i. f i + g i) = suminf f + suminf g" 
43920  1178 
apply (subst (1 2 3) suminf_ereal_eq_SUPR) 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1179 
unfolding setsum_addf 
43920  1180 
by (intro assms ereal_add_nonneg_nonneg SUPR_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+ 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1181 

43920  1182 
lemma suminf_cmult_ereal: 
1183 
fixes f g :: "nat \<Rightarrow> ereal" 

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

1184 
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

1185 
shows "(\<Sum>i. a * f i) = a * suminf f" 
43920  1186 
by (auto simp: setsum_ereal_right_distrib[symmetric] assms 
1187 
ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUPR 

1188 
intro!: SUPR_ereal_cmult ) 

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

1189 

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

1190 
lemma suminf_PInfty: 
43923  1191 
fixes f :: "nat \<Rightarrow> ereal" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1192 
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

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

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

1195 
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

1196 
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

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

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

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

1200 

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

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

1202 
assumes "\<And>i. 0 \<le> f i" "suminf f \<noteq> \<infinity>" 
43920  1203 
shows "\<exists>f'. f = (\<lambda>x. ereal (f' x))" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1204 
proof  
43920  1205 
have "\<forall>i. \<exists>r. f i = ereal r" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1206 
proof 
43920  1207 
fix i show "\<exists>r. f i = ereal r" 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

1208 
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

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

1210 
from choice[OF this] show ?thesis by auto 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff
changeset

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

1212 

43920  1213 
lemma summable_ereal: 
1214 
assumes "\<And>i. 0 \<le> f i" "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>" 
