src/HOL/Library/Euclidean_Space.thy
 changeset 33269 3b7e2dbbd684 parent 32960 69916a850301
```     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Fri Oct 23 14:33:07 2009 +0200
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Tue Oct 27 12:59:57 2009 +0000
1.3 @@ -2297,242 +2297,9 @@
1.4    ultimately show ?thesis by metis
1.5  qed
1.6
1.7 -(* Supremum and infimum of real sets *)
1.8 -
1.9 -
1.10 -definition rsup:: "real set \<Rightarrow> real" where
1.11 -  "rsup S = (SOME a. isLub UNIV S a)"
1.12 -
1.13 -lemma rsup_alt: "rsup S = (SOME a. (\<forall>x \<in> S. x \<le> a) \<and> (\<forall>b. (\<forall>x \<in> S. x \<le> b) \<longrightarrow> a \<le> b))"  by (auto simp  add: isLub_def rsup_def leastP_def isUb_def setle_def setge_def)
1.14 -
1.15 -lemma rsup: assumes Se: "S \<noteq> {}" and b: "\<exists>b. S *<= b"
1.16 -  shows "isLub UNIV S (rsup S)"
1.17 -using Se b
1.18 -unfolding rsup_def
1.19 -apply clarify
1.20 -apply (rule someI_ex)
1.21 -apply (rule reals_complete)
1.22 -by (auto simp add: isUb_def setle_def)
1.23 -
1.24 -lemma rsup_le: assumes Se: "S \<noteq> {}" and Sb: "S *<= b" shows "rsup S \<le> b"
1.25 -proof-
1.26 -  from Sb have bu: "isUb UNIV S b" by (simp add: isUb_def setle_def)
1.27 -  from rsup[OF Se] Sb have "isLub UNIV S (rsup S)"  by blast
1.28 -  then show ?thesis using bu by (auto simp add: isLub_def leastP_def setle_def setge_def)
1.29 -qed
1.30 -
1.31 -lemma rsup_finite_Max: assumes fS: "finite S" and Se: "S \<noteq> {}"
1.32 -  shows "rsup S = Max S"
1.33 -using fS Se
1.34 -proof-
1.35 -  let ?m = "Max S"
1.36 -  from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis
1.37 -  with rsup[OF Se] have lub: "isLub UNIV S (rsup S)" by (metis setle_def)
1.38 -  from Max_in[OF fS Se] lub have mrS: "?m \<le> rsup S"
1.39 -    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
1.40 -  moreover
1.41 -  have "rsup S \<le> ?m" using Sm lub
1.42 -    by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
1.43 -  ultimately  show ?thesis by arith
1.44 -qed
1.45 -
1.46 -lemma rsup_finite_in: assumes fS: "finite S" and Se: "S \<noteq> {}"
1.47 -  shows "rsup S \<in> S"
1.48 -  using rsup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis
1.49 -
1.50 -lemma rsup_finite_Ub: assumes fS: "finite S" and Se: "S \<noteq> {}"
1.51 -  shows "isUb S S (rsup S)"
1.52 -  using rsup_finite_Max[OF fS Se] rsup_finite_in[OF fS Se] Max_ge[OF fS]
1.53 -  unfolding isUb_def setle_def by metis
1.54 -
1.55 -lemma rsup_finite_ge_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
1.56 -  shows "a \<le> rsup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
1.57 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
1.58 -
1.59 -lemma rsup_finite_le_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
1.60 -  shows "a \<ge> rsup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
1.61 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
1.62 -
1.63 -lemma rsup_finite_gt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
1.64 -  shows "a < rsup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
1.65 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
1.66 -
1.67 -lemma rsup_finite_lt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
1.68 -  shows "a > rsup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
1.69 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
1.70 -
1.71 -lemma rsup_unique: assumes b: "S *<= b" and S: "\<forall>b' < b. \<exists>x \<in> S. b' < x"
1.72 -  shows "rsup S = b"
1.73 -using b S
1.74 -unfolding setle_def rsup_alt
1.75 -apply -
1.76 -apply (rule some_equality)
1.77 -apply (metis  linorder_not_le order_eq_iff[symmetric])+
1.78 -done
1.79 -
1.80 -lemma rsup_le_subset: "S\<noteq>{} \<Longrightarrow> S \<subseteq> T \<Longrightarrow> (\<exists>b. T *<= b) \<Longrightarrow> rsup S \<le> rsup T"
1.81 -  apply (rule rsup_le)
1.82 -  apply simp
1.83 -  using rsup[of T] by (auto simp add: isLub_def leastP_def setge_def setle_def isUb_def)
1.84 -
1.85 -lemma isUb_def': "isUb R S = (\<lambda>x. S *<= x \<and> x \<in> R)"
1.86 -  apply (rule ext)
1.87 -  by (metis isUb_def)
1.88 -
1.89 -lemma UNIV_trivial: "UNIV x" using UNIV_I[of x] by (metis mem_def)
1.90 -lemma rsup_bounds: assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
1.91 -  shows "a \<le> rsup S \<and> rsup S \<le> b"
1.92 -proof-
1.93 -  from rsup[OF Se] u have lub: "isLub UNIV S (rsup S)" by blast
1.94 -  hence b: "rsup S \<le> b" using u by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def')
1.95 -  from Se obtain y where y: "y \<in> S" by blast
1.96 -  from lub l have "a \<le> rsup S" apply (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def')
1.97 -    apply (erule ballE[where x=y])
1.98 -    apply (erule ballE[where x=y])
1.99 -    apply arith
1.100 -    using y apply auto
1.101 -    done
1.102 -  with b show ?thesis by blast
1.103 -qed
1.104 -
1.105 -lemma rsup_abs_le: "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>rsup S\<bar> \<le> a"
1.106 -  unfolding abs_le_interval_iff  using rsup_bounds[of S "-a" a]
1.107 -  by (auto simp add: setge_def setle_def)
1.108 -
1.109 -lemma rsup_asclose: assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>rsup S - l\<bar> \<le> e"
1.110 -proof-
1.111 -  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
1.112 -  show ?thesis using S b rsup_bounds[of S "l - e" "l+e"] unfolding th
1.113 -    by  (auto simp add: setge_def setle_def)
1.114 -qed
1.115 -
1.116 -definition rinf:: "real set \<Rightarrow> real" where
1.117 -  "rinf S = (SOME a. isGlb UNIV S a)"
1.118 -
1.119 -lemma rinf_alt: "rinf S = (SOME a. (\<forall>x \<in> S. x \<ge> a) \<and> (\<forall>b. (\<forall>x \<in> S. x \<ge> b) \<longrightarrow> a \<ge> b))"  by (auto simp  add: isGlb_def rinf_def greatestP_def isLb_def setle_def setge_def)
1.120 -
1.121 -lemma reals_complete_Glb: assumes Se: "\<exists>x. x \<in> S" and lb: "\<exists> y. isLb UNIV S y"
1.122 -  shows "\<exists>(t::real). isGlb UNIV S t"
1.123 -proof-
1.124 -  let ?M = "uminus ` S"
1.125 -  from lb have th: "\<exists>y. isUb UNIV ?M y" apply (auto simp add: isUb_def isLb_def setle_def setge_def)
1.126 -    by (rule_tac x="-y" in exI, auto)
1.127 -  from Se have Me: "\<exists>x. x \<in> ?M" by blast
1.128 -  from reals_complete[OF Me th] obtain t where t: "isLub UNIV ?M t" by blast
1.129 -  have "isGlb UNIV S (- t)" using t
1.130 -    apply (auto simp add: isLub_def isGlb_def leastP_def greatestP_def setle_def setge_def isUb_def isLb_def)
1.131 -    apply (erule_tac x="-y" in allE)
1.132 -    apply auto
1.133 -    done
1.134 -  then show ?thesis by metis
1.135 -qed
1.136 -
1.137 -lemma rinf: assumes Se: "S \<noteq> {}" and b: "\<exists>b. b <=* S"
1.138 -  shows "isGlb UNIV S (rinf S)"
1.139 -using Se b
1.140 -unfolding rinf_def
1.141 -apply clarify
1.142 -apply (rule someI_ex)
1.143 -apply (rule reals_complete_Glb)
1.144 -apply (auto simp add: isLb_def setle_def setge_def)
1.145 -done
1.146 -
1.147 -lemma rinf_ge: assumes Se: "S \<noteq> {}" and Sb: "b <=* S" shows "rinf S \<ge> b"
1.148 -proof-
1.149 -  from Sb have bu: "isLb UNIV S b" by (simp add: isLb_def setge_def)
1.150 -  from rinf[OF Se] Sb have "isGlb UNIV S (rinf S)"  by blast
1.151 -  then show ?thesis using bu by (auto simp add: isGlb_def greatestP_def setle_def setge_def)
1.152 -qed
1.153 -
1.154 -lemma rinf_finite_Min: assumes fS: "finite S" and Se: "S \<noteq> {}"
1.155 -  shows "rinf S = Min S"
1.156 -using fS Se
1.157 -proof-
1.158 -  let ?m = "Min S"
1.159 -  from Min_le[OF fS] have Sm: "\<forall> x\<in> S. x \<ge> ?m" by metis
1.160 -  with rinf[OF Se] have glb: "isGlb UNIV S (rinf S)" by (metis setge_def)
1.161 -  from Min_in[OF fS Se] glb have mrS: "?m \<ge> rinf S"
1.162 -    by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def)
1.163 -  moreover
1.164 -  have "rinf S \<ge> ?m" using Sm glb
1.165 -    by (auto simp add: isGlb_def greatestP_def isLb_def setle_def setge_def)
1.166 -  ultimately  show ?thesis by arith
1.167 -qed
1.168 -
1.169 -lemma rinf_finite_in: assumes fS: "finite S" and Se: "S \<noteq> {}"
1.170 -  shows "rinf S \<in> S"
1.171 -  using rinf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis
1.172 -
1.173 -lemma rinf_finite_Lb: assumes fS: "finite S" and Se: "S \<noteq> {}"
1.174 -  shows "isLb S S (rinf S)"
1.175 -  using rinf_finite_Min[OF fS Se] rinf_finite_in[OF fS Se] Min_le[OF fS]
1.176 -  unfolding isLb_def setge_def by metis
1.177 -
1.178 -lemma rinf_finite_ge_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
1.179 -  shows "a \<le> rinf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
1.180 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
1.181 -
1.182 -lemma rinf_finite_le_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
1.183 -  shows "a \<ge> rinf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
1.184 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
1.185 -
1.186 -lemma rinf_finite_gt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
1.187 -  shows "a < rinf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
1.188 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
1.189 -
1.190 -lemma rinf_finite_lt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
1.191 -  shows "a > rinf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
1.192 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
1.193 -
1.194 -lemma rinf_unique: assumes b: "b <=* S" and S: "\<forall>b' > b. \<exists>x \<in> S. b' > x"
1.195 -  shows "rinf S = b"
1.196 -using b S
1.197 -unfolding setge_def rinf_alt
1.198 -apply -
1.199 -apply (rule some_equality)
1.200 -apply (metis  linorder_not_le order_eq_iff[symmetric])+
1.201 -done
1.202 -
1.203 -lemma rinf_ge_subset: "S\<noteq>{} \<Longrightarrow> S \<subseteq> T \<Longrightarrow> (\<exists>b. b <=* T) \<Longrightarrow> rinf S >= rinf T"
1.204 -  apply (rule rinf_ge)
1.205 -  apply simp
1.206 -  using rinf[of T] by (auto simp add: isGlb_def greatestP_def setge_def setle_def isLb_def)
1.207 -
1.208 -lemma isLb_def': "isLb R S = (\<lambda>x. x <=* S \<and> x \<in> R)"
1.209 -  apply (rule ext)
1.210 -  by (metis isLb_def)
1.211 -
1.212 -lemma rinf_bounds: assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
1.213 -  shows "a \<le> rinf S \<and> rinf S \<le> b"
1.214 -proof-
1.215 -  from rinf[OF Se] l have lub: "isGlb UNIV S (rinf S)" by blast
1.216 -  hence b: "a \<le> rinf S" using l by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def')
1.217 -  from Se obtain y where y: "y \<in> S" by blast
1.218 -  from lub u have "b \<ge> rinf S" apply (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def')
1.219 -    apply (erule ballE[where x=y])
1.220 -    apply (erule ballE[where x=y])
1.221 -    apply arith
1.222 -    using y apply auto
1.223 -    done
1.224 -  with b show ?thesis by blast
1.225 -qed
1.226 -
1.227 -lemma rinf_abs_ge: "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>rinf S\<bar> \<le> a"
1.228 -  unfolding abs_le_interval_iff  using rinf_bounds[of S "-a" a]
1.229 -  by (auto simp add: setge_def setle_def)
1.230 -
1.231 -lemma rinf_asclose: assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>rinf S - l\<bar> \<le> e"
1.232 -proof-
1.233 -  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
1.234 -  show ?thesis using S b rinf_bounds[of S "l - e" "l+e"] unfolding th
1.235 -    by  (auto simp add: setge_def setle_def)
1.236 -qed
1.237 -
1.238 -
1.239 -
1.240  subsection{* Operator norm. *}
1.241
1.242 -definition "onorm f = rsup {norm (f x)| x. norm x = 1}"
1.243 +definition "onorm f = Sup {norm (f x)| x. norm x = 1}"
1.244
1.245  lemma norm_bound_generalize:
1.246    fixes f:: "real ^'n::finite \<Rightarrow> real^'m::finite"
1.247 @@ -2578,7 +2345,7 @@
1.248      have Se: "?S \<noteq> {}" using  norm_basis by auto
1.249      from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
1.250        unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def)
1.251 -    {from rsup[OF Se b, unfolded onorm_def[symmetric]]
1.252 +    {from Sup[OF Se b, unfolded onorm_def[symmetric]]
1.253        show "norm (f x) <= onorm f * norm x"
1.254          apply -
1.255          apply (rule spec[where x = x])
1.256 @@ -2586,7 +2353,7 @@
1.257          by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
1.258      {
1.259        show "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
1.260 -        using rsup[OF Se b, unfolded onorm_def[symmetric]]
1.261 +        using Sup[OF Se b, unfolded onorm_def[symmetric]]
1.262          unfolding norm_bound_generalize[OF lf, symmetric]
1.263          by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
1.264    }
1.265 @@ -2612,7 +2379,7 @@
1.266      by(auto intro: vector_choose_size set_ext)
1.267    show ?thesis
1.268      unfolding onorm_def th
1.269 -    apply (rule rsup_unique) by (simp_all  add: setle_def)
1.270 +    apply (rule Sup_unique) by (simp_all  add: setle_def)
1.271  qed
1.272
1.273  lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n::finite \<Rightarrow> real ^'m::finite)"
1.274 @@ -3055,31 +2822,6 @@
1.275  qed
1.276
1.277  (* ------------------------------------------------------------------------- *)
1.278 -(* Relate max and min to sup and inf.                                        *)
1.279 -(* ------------------------------------------------------------------------- *)
1.280 -
1.281 -lemma real_max_rsup: "max x y = rsup {x,y}"
1.282 -proof-
1.283 -  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
1.284 -  from rsup_finite_le_iff[OF f, of "max x y"] have "rsup {x,y} \<le> max x y" by simp
1.285 -  moreover
1.286 -  have "max x y \<le> rsup {x,y}" using rsup_finite_ge_iff[OF f, of "max x y"]
1.287 -    by (simp add: linorder_linear)
1.288 -  ultimately show ?thesis by arith
1.289 -qed
1.290 -
1.291 -lemma real_min_rinf: "min x y = rinf {x,y}"
1.292 -proof-
1.293 -  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
1.294 -  from rinf_finite_le_iff[OF f, of "min x y"] have "rinf {x,y} \<le> min x y"
1.295 -    by (simp add: linorder_linear)
1.296 -  moreover
1.297 -  have "min x y \<le> rinf {x,y}" using rinf_finite_ge_iff[OF f, of "min x y"]
1.298 -    by simp
1.299 -  ultimately show ?thesis by arith
1.300 -qed
1.301 -
1.302 -(* ------------------------------------------------------------------------- *)
1.303  (* Geometric progression.                                                    *)
1.304  (* ------------------------------------------------------------------------- *)
1.305
1.306 @@ -5048,7 +4790,7 @@
1.307
1.308  (* Infinity norm.                                                            *)
1.309
1.310 -definition "infnorm (x::real^'n::finite) = rsup {abs(x\$i) |i. i\<in> (UNIV :: 'n set)}"
1.311 +definition "infnorm (x::real^'n::finite) = Sup {abs(x\$i) |i. i\<in> (UNIV :: 'n set)}"
1.312
1.313  lemma numseg_dimindex_nonempty: "\<exists>i. i \<in> (UNIV :: 'n set)"
1.314    by auto
1.315 @@ -5065,7 +4807,7 @@
1.316
1.317  lemma infnorm_pos_le: "0 \<le> infnorm (x::real^'n::finite)"
1.318    unfolding infnorm_def
1.319 -  unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
1.320 +  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
1.321    unfolding infnorm_set_image
1.322    by auto
1.323
1.324 @@ -5076,13 +4818,13 @@
1.325    have th2: "\<And>x (y::real). abs(x + y) - abs(x) <= abs(y)" by arith
1.326    show ?thesis
1.327    unfolding infnorm_def
1.328 -  unfolding rsup_finite_le_iff[ OF infnorm_set_lemma]
1.329 +  unfolding Sup_finite_le_iff[ OF infnorm_set_lemma]
1.330    apply (subst diff_le_eq[symmetric])
1.331 -  unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
1.332 +  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
1.333    unfolding infnorm_set_image bex_simps
1.334    apply (subst th)
1.335    unfolding th1
1.336 -  unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
1.337 +  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
1.338
1.339    unfolding infnorm_set_image ball_simps bex_simps
1.340    apply simp
1.341 @@ -5094,7 +4836,7 @@
1.342  proof-
1.343    have "infnorm x <= 0 \<longleftrightarrow> x = 0"
1.344      unfolding infnorm_def
1.345 -    unfolding rsup_finite_le_iff[OF infnorm_set_lemma]
1.346 +    unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
1.347      unfolding infnorm_set_image ball_simps
1.348      by vector
1.349    then show ?thesis using infnorm_pos_le[of x] by simp
1.350 @@ -5105,7 +4847,7 @@
1.351
1.352  lemma infnorm_neg: "infnorm (- x) = infnorm x"
1.353    unfolding infnorm_def
1.354 -  apply (rule cong[of "rsup" "rsup"])
1.355 +  apply (rule cong[of "Sup" "Sup"])
1.356    apply blast
1.357    apply (rule set_ext)
1.358    apply auto
1.359 @@ -5140,14 +4882,15 @@
1.360      apply (rule finite_imageI) unfolding Collect_def mem_def by simp
1.361    have S0: "?S \<noteq> {}" by blast
1.362    have th1: "\<And>S f. f ` S = { f i| i. i \<in> S}" by blast
1.363 -  from rsup_finite_in[OF fS S0] rsup_finite_Ub[OF fS S0]
1.364 -  show ?thesis unfolding infnorm_def isUb_def setle_def
1.365 -    unfolding infnorm_set_image ball_simps by auto
1.366 +  from Sup_finite_in[OF fS S0]
1.367 +  show ?thesis unfolding infnorm_def infnorm_set_image
1.368 +    by (metis Sup_finite_ge_iff finite finite_imageI UNIV_not_empty image_is_empty
1.369 +              rangeI real_le_refl)
1.370  qed
1.371
1.372  lemma infnorm_mul_lemma: "infnorm(a *s x) <= \<bar>a\<bar> * infnorm x"
1.373    apply (subst infnorm_def)
1.374 -  unfolding rsup_finite_le_iff[OF infnorm_set_lemma]
1.375 +  unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
1.376    unfolding infnorm_set_image ball_simps
1.378    apply (rule allI)
1.379 @@ -5180,7 +4923,7 @@
1.380  (* Prove that it differs only up to a bound from Euclidean norm.             *)
1.381
1.382  lemma infnorm_le_norm: "infnorm x \<le> norm x"
1.383 -  unfolding infnorm_def rsup_finite_le_iff[OF infnorm_set_lemma]
1.384 +  unfolding infnorm_def Sup_finite_le_iff[OF infnorm_set_lemma]
1.385    unfolding infnorm_set_image  ball_simps
1.386    by (metis component_le_norm)
1.387  lemma card_enum: "card {1 .. n} = n" by auto
1.388 @@ -5200,7 +4943,7 @@
1.389      apply (rule setsum_bounded)
1.390      apply (rule power_mono)
1.391      unfolding abs_of_nonneg[OF infnorm_pos_le]
1.392 -    unfolding infnorm_def  rsup_finite_ge_iff[OF infnorm_set_lemma]
1.393 +    unfolding infnorm_def  Sup_finite_ge_iff[OF infnorm_set_lemma]
1.394      unfolding infnorm_set_image bex_simps
1.395      apply blast
1.396      by (rule abs_ge_zero)
```