1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Sep 22 20:37:47 2012 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Sep 22 20:38:42 2012 +0200
1.3 @@ -36,16 +36,16 @@
1.4 lemma mem_convex_alt:
1.5 assumes "convex S" "x : S" "y : S" "u>=0" "v>=0" "u+v>0"
1.6 shows "((u/(u+v)) *\<^sub>R x + (v/(u+v)) *\<^sub>R y) : S"
1.7 - apply (subst mem_convex_2)
1.8 + apply (subst mem_convex_2)
1.9 using assms apply (auto simp add: algebra_simps zero_le_divide_iff)
1.10 using add_divide_distrib[of u v "u+v"] apply auto
1.11 done
1.12
1.13 -lemma inj_on_image_mem_iff: "inj_on f B ==> (A <= B) ==> (f a : f`A) ==> (a : B) ==> (a : A)"
1.14 +lemma inj_on_image_mem_iff: "inj_on f B ==> (A <= B) ==> (f a : f`A) ==> (a : B) ==> (a : A)"
1.15 by (blast dest: inj_onD)
1.16
1.17 lemma independent_injective_on_span_image:
1.18 - assumes iS: "independent S"
1.19 + assumes iS: "independent S"
1.20 and lf: "linear f" and fi: "inj_on f (span S)"
1.21 shows "independent (f ` S)"
1.22 proof -
1.23 @@ -65,10 +65,10 @@
1.24
1.25 lemma dim_image_eq:
1.26 fixes f :: "'n::euclidean_space => 'm::euclidean_space"
1.27 - assumes lf: "linear f" and fi: "inj_on f (span S)"
1.28 + assumes lf: "linear f" and fi: "inj_on f (span S)"
1.29 shows "dim (f ` S) = dim (S:: ('n::euclidean_space) set)"
1.30 proof -
1.31 - obtain B where B_def: "B<=S & independent B & S <= span B & card B = dim S"
1.32 + obtain B where B_def: "B<=S & independent B & S <= span B & card B = dim S"
1.33 using basis_exists[of S] by auto
1.34 then have "span S = span B"
1.35 using span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto
1.36 @@ -90,20 +90,20 @@
1.37 also have "... <-> (!x : S. !y : S. f x - f y = 0 --> x - y = 0)" by simp
1.38 also have "... <-> (!x : S. !y : S. f (x - y) = 0 --> x - y = 0)"
1.39 by (simp add: linear_sub[OF lf])
1.40 - also have "... <-> (! x : S. f x = 0 --> x = 0)"
1.41 + also have "... <-> (! x : S. f x = 0 --> x = 0)"
1.42 using `subspace S` subspace_def[of S] subspace_sub[of S] by auto
1.43 finally show ?thesis .
1.44 qed
1.45
1.46 lemma subspace_Inter: "(!s : f. subspace s) ==> subspace (Inter f)"
1.47 - unfolding subspace_def by auto
1.48 + unfolding subspace_def by auto
1.49
1.50 lemma span_eq[simp]: "(span s = s) <-> subspace s"
1.51 unfolding span_def by (rule hull_eq, rule subspace_Inter)
1.52
1.53 lemma basis_inj_on: "d \<subseteq> {..<DIM('n)} \<Longrightarrow> inj_on (basis :: nat => 'n::euclidean_space) d"
1.54 by (auto simp add: inj_on_def euclidean_eq[where 'a='n])
1.55 -
1.56 +
1.57 lemma finite_substdbasis: "finite {basis i ::'n::euclidean_space |i. i : (d:: nat set)}" (is "finite ?S")
1.58 proof -
1.59 have eq: "?S = basis ` d" by blast
1.60 @@ -152,7 +152,7 @@
1.61 done
1.62 qed
1.63
1.64 -lemma dim_cball:
1.65 +lemma dim_cball:
1.66 assumes "0<e"
1.67 shows "dim (cball (0 :: 'n::euclidean_space) e) = DIM('n)"
1.68 proof -
1.69 @@ -163,7 +163,7 @@
1.70 moreover hence "x = (norm x/e) *\<^sub>R y" by auto
1.71 ultimately have "x : span (cball 0 e)"
1.72 using span_mul[of y "cball 0 e" "norm x/e"] span_inc[of "cball 0 e"] by auto
1.73 - } then have "span (cball 0 e) = (UNIV :: ('n::euclidean_space) set)" by auto
1.74 + } then have "span (cball 0 e) = (UNIV :: ('n::euclidean_space) set)" by auto
1.75 then show ?thesis
1.76 using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp add: dim_UNIV)
1.77 qed
1.78 @@ -171,13 +171,13 @@
1.79 lemma indep_card_eq_dim_span:
1.80 fixes B :: "('n::euclidean_space) set"
1.81 assumes "independent B"
1.82 - shows "finite B & card B = dim (span B)"
1.83 + shows "finite B & card B = dim (span B)"
1.84 using assms basis_card_eq_dim[of B "span B"] span_inc by auto
1.85
1.86 lemma setsum_not_0: "setsum f A ~= 0 ==> EX a:A. f a ~= 0"
1.87 by (rule ccontr) auto
1.88
1.89 -lemma translate_inj_on:
1.90 +lemma translate_inj_on:
1.91 fixes A :: "('a::ab_group_add) set"
1.92 shows "inj_on (%x. a+x) A"
1.93 unfolding inj_on_def by auto
1.94 @@ -206,7 +206,7 @@
1.95 done
1.96
1.97 lemma translation_inverse_subset:
1.98 - assumes "((%x. -a+x) ` V) <= (S :: 'n::ab_group_add set)"
1.99 + assumes "((%x. -a+x) ` V) <= (S :: 'n::ab_group_add set)"
1.100 shows "V <= ((%x. a+x) ` S)"
1.101 proof -
1.102 { fix x
1.103 @@ -394,7 +394,7 @@
1.104 unfolding affine_def by auto
1.105
1.106 lemma affine_Inter: "(\<forall>s\<in>f. affine s) \<Longrightarrow> affine (\<Inter> f)"
1.107 - unfolding affine_def by auto
1.108 + unfolding affine_def by auto
1.109
1.110 lemma affine_Int: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"
1.111 unfolding affine_def by auto
1.112 @@ -416,7 +416,7 @@
1.113 unfolding affine_def
1.114 apply rule
1.115 apply(rule, rule, rule)
1.116 - apply(erule conjE)+
1.117 + apply(erule conjE)+
1.118 defer
1.119 apply (rule, rule, rule, rule, rule)
1.120 proof -
1.121 @@ -480,9 +480,9 @@
1.122 case True
1.123 then have "s - {x} \<noteq> {}" "card (s - {x}) = n"
1.124 unfolding c and as(1)[symmetric]
1.125 - proof (rule_tac ccontr)
1.126 + proof (rule_tac ccontr)
1.127 assume "\<not> s - {x} \<noteq> {}"
1.128 - then have "card (s - {x}) = 0" unfolding card_0_eq[OF *(2)] by simp
1.129 + then have "card (s - {x}) = 0" unfolding card_0_eq[OF *(2)] by simp
1.130 then show False using True by auto
1.131 qed auto
1.132 then show ?thesis
1.133 @@ -640,12 +640,12 @@
1.134 then show ?thesis
1.135 apply (rule_tac x="\<lambda>x. (if x=a then v else 0) + u x" in exI)
1.136 unfolding setsum_clauses(2)[OF `?as`] apply simp
1.137 - unfolding scaleR_left_distrib and setsum_addf
1.138 + unfolding scaleR_left_distrib and setsum_addf
1.139 unfolding vu and * and scaleR_zero_left
1.140 apply (auto simp add: setsum_delta[OF `?as`])
1.141 done
1.142 next
1.143 - case False
1.144 + case False
1.145 then have **:
1.146 "\<And>x. x \<in> s \<Longrightarrow> u x = (if x = a then v else u x)"
1.147 "\<And>x. x \<in> s \<Longrightarrow> u x *\<^sub>R x = (if x = a then v *\<^sub>R x else u x *\<^sub>R x)" by auto
1.148 @@ -666,7 +666,7 @@
1.149 shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs")
1.150 proof -
1.151 have *:
1.152 - "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)"
1.153 + "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)"
1.154 "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
1.155 have "?lhs = {y. \<exists>u. setsum u {a, b} = 1 \<and> (\<Sum>v\<in>{a, b}. u v *\<^sub>R v) = y}"
1.156 using affine_hull_finite[of "{a,b}"] by auto
1.157 @@ -681,7 +681,7 @@
1.158 shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" (is "?lhs = ?rhs")
1.159 proof -
1.160 have *:
1.161 - "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)"
1.162 + "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)"
1.163 "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
1.164 show ?thesis
1.165 apply (simp add: affine_hull_finite affine_hull_finite_step)
1.166 @@ -708,7 +708,7 @@
1.167 using hull_mono[of "{x, y, z}" "S"] assms by auto
1.168 moreover
1.169 have "affine hull S = S" using assms affine_hull_eq[of S] by auto
1.170 - ultimately show ?thesis by auto
1.171 + ultimately show ?thesis by auto
1.172 qed
1.173
1.174 lemma mem_affine_3_minus:
1.175 @@ -750,7 +750,7 @@
1.176 unfolding subset_eq Ball_def
1.177 unfolding affine_hull_explicit and mem_Collect_eq
1.178 proof (rule, rule, erule exE, erule conjE)
1.179 - fix y v
1.180 + fix y v
1.181 assume "y = a + v" "v \<in> span {x - a |x. x \<in> s}"
1.182 then obtain t u where obt:"finite t" "t \<subseteq> {x - a |x. x \<in> s}" "a + (\<Sum>v\<in>t. u v *\<^sub>R v) = y"
1.183 unfolding span_explicit by auto
1.184 @@ -780,7 +780,7 @@
1.185
1.186 lemma affine_parallel_expl_aux:
1.187 fixes S T :: "'a::real_vector set"
1.188 - assumes "!x. (x : S <-> (a+x) : T)"
1.189 + assumes "!x. (x : S <-> (a+x) : T)"
1.190 shows "T = ((%x. a + x) ` S)"
1.191 proof -
1.192 { fix x
1.193 @@ -788,7 +788,7 @@
1.194 then have "(-a)+x : S" using assms by auto
1.195 then have "x : ((%x. a + x) ` S)"
1.196 using imageI[of "-a+x" S "(%x. a+x)"] by auto }
1.197 - moreover have "T >= ((%x. a + x) ` S)" using assms by auto
1.198 + moreover have "T >= ((%x. a + x) ` S)" using assms by auto
1.199 ultimately show ?thesis by auto
1.200 qed
1.201
1.202 @@ -811,11 +811,11 @@
1.203
1.204 lemma affine_parallel_assoc:
1.205 assumes "affine_parallel A B" "affine_parallel B C"
1.206 - shows "affine_parallel A C"
1.207 + shows "affine_parallel A C"
1.208 proof -
1.209 from assms obtain ab where "B=((%x. ab + x) ` A)"
1.210 - unfolding affine_parallel_def by auto
1.211 - moreover
1.212 + unfolding affine_parallel_def by auto
1.213 + moreover
1.214 from assms obtain bc where "C=((%x. bc + x) ` B)"
1.215 unfolding affine_parallel_def by auto
1.216 ultimately show ?thesis
1.217 @@ -856,7 +856,7 @@
1.218 shows "affine T"
1.219 proof -
1.220 from assms obtain a where "T=((%x. a + x) ` S)"
1.221 - unfolding affine_parallel_def by auto
1.222 + unfolding affine_parallel_def by auto
1.223 then show ?thesis using affine_translation assms by auto
1.224 qed
1.225
1.226 @@ -871,7 +871,7 @@
1.227 have h0: "subspace S ==> (affine S & 0 : S)"
1.228 using subspace_imp_affine[of S] subspace_0 by auto
1.229 { assume assm: "affine S & 0 : S"
1.230 - { fix c :: real
1.231 + { fix c :: real
1.232 fix x assume x_def: "x : S"
1.233 have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto
1.234 moreover
1.235 @@ -894,7 +894,7 @@
1.236 ultimately
1.237 have "(x+y) : S" using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto
1.238 }
1.239 - then have "!x : S. !y : S. (x+y) : S" by auto
1.240 + then have "!x : S. !y : S. (x+y) : S" by auto
1.241 then have "subspace S" using h1 assm unfolding subspace_def by auto
1.242 }
1.243 then show ?thesis using h0 by metis
1.244 @@ -905,25 +905,25 @@
1.245 shows "subspace ((%x. (-a)+x) ` S)"
1.246 proof -
1.247 have "affine ((%x. (-a)+x) ` S)"
1.248 - using affine_translation assms by auto
1.249 + using affine_translation assms by auto
1.250 moreover have "0 : ((%x. (-a)+x) ` S)"
1.251 using assms exI[of "(%x. x:S & -a+x=0)" a] by auto
1.252 - ultimately show ?thesis using subspace_affine by auto
1.253 + ultimately show ?thesis using subspace_affine by auto
1.254 qed
1.255
1.256 lemma parallel_subspace_explicit:
1.257 assumes "affine S" "a : S"
1.258 - assumes "L == {y. ? x : S. (-a)+x=y}"
1.259 - shows "subspace L & affine_parallel S L"
1.260 + assumes "L == {y. ? x : S. (-a)+x=y}"
1.261 + shows "subspace L & affine_parallel S L"
1.262 proof -
1.263 have par: "affine_parallel S L"
1.264 unfolding affine_parallel_def using assms by auto
1.265 - then have "affine L" using assms parallel_is_affine by auto
1.266 + then have "affine L" using assms parallel_is_affine by auto
1.267 moreover have "0 : L"
1.268 using assms apply auto
1.269 using exI[of "(%x. x:S & -a+x=0)" a] apply auto
1.270 done
1.271 - ultimately show ?thesis using subspace_affine par by auto
1.272 + ultimately show ?thesis using subspace_affine par by auto
1.273 qed
1.274
1.275 lemma parallel_subspace_aux:
1.276 @@ -949,10 +949,10 @@
1.277
1.278 lemma affine_parallel_subspace:
1.279 assumes "affine S" "S ~= {}"
1.280 - shows "?!L. subspace L & affine_parallel S L"
1.281 + shows "?!L. subspace L & affine_parallel S L"
1.282 proof -
1.283 have ex: "? L. subspace L & affine_parallel S L"
1.284 - using assms parallel_subspace_explicit by auto
1.285 + using assms parallel_subspace_explicit by auto
1.286 { fix L1 L2
1.287 assume ass: "subspace L1 & affine_parallel S L1" "subspace L2 & affine_parallel S L2"
1.288 then have "affine_parallel L1 L2"
1.289 @@ -1084,7 +1084,7 @@
1.290 { fix x
1.291 assume "x : S"
1.292 then have "1 *\<^sub>R x : ?rhs"
1.293 - apply auto
1.294 + apply auto
1.295 apply (rule_tac x="1" in exI)
1.296 apply auto
1.297 done
1.298 @@ -1253,7 +1253,7 @@
1.299 fixes s :: "'a::real_normed_vector set"
1.300 assumes "convex s" shows "connected s"
1.301 proof-
1.302 - { fix e1 e2 assume as:"open e1" "open e2" "e1 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2"
1.303 + { fix e1 e2 assume as:"open e1" "open e2" "e1 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2"
1.304 assume "e1 \<inter> s \<noteq> {}" "e2 \<inter> s \<noteq> {}"
1.305 then obtain x1 x2 where x1:"x1\<in>e1" "x1\<in>s" and x2:"x2\<in>e2" "x2\<in>s" by auto
1.306 hence n:"norm (x1 - x2) > 0" unfolding zero_less_norm_iff using as(3) by auto
1.307 @@ -1277,7 +1277,7 @@
1.308 using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2
1.309 using as(3) by auto
1.310 then obtain x where "x\<ge>0" "x\<le>1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2" by auto
1.311 - hence False using as(4)
1.312 + hence False using as(4)
1.313 using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]]
1.314 using x1(2) x2(2) by auto }
1.315 thus ?thesis unfolding connected_def by auto
1.316 @@ -1322,7 +1322,7 @@
1.317
1.318 lemma convex_ball:
1.319 fixes x :: "'a::real_normed_vector"
1.320 - shows "convex (ball x e)"
1.321 + shows "convex (ball x e)"
1.322 proof(auto simp add: convex_def)
1.323 fix y z assume yz:"dist x y < e" "dist x z < e"
1.324 fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
1.325 @@ -1339,7 +1339,7 @@
1.326 fix u v ::real assume uv:" 0 \<le> u" "0 \<le> v" "u + v = 1"
1.327 have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz
1.328 using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto
1.329 - thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" using convex_bound_le[OF yz uv] by auto
1.330 + thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" using convex_bound_le[OF yz uv] by auto
1.331 qed
1.332
1.333 lemma connected_ball:
1.334 @@ -1379,15 +1379,15 @@
1.335 lemma convex_hull_linear_image:
1.336 assumes "bounded_linear f"
1.337 shows "f ` (convex hull s) = convex hull (f ` s)"
1.338 - apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3
1.339 + apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3
1.340 apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption
1.341 apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption
1.342 proof-
1.343 interpret f: bounded_linear f by fact
1.344 - show "convex {x. f x \<in> convex hull f ` s}"
1.345 + show "convex {x. f x \<in> convex hull f ` s}"
1.346 unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next
1.347 interpret f: bounded_linear f by fact
1.348 - show "convex {x. x \<in> f ` (convex hull s)}" using convex_convex_hull[unfolded convex_def, of s]
1.349 + show "convex {x. x \<in> f ` (convex hull s)}" using convex_convex_hull[unfolded convex_def, of s]
1.350 unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
1.351 qed auto
1.352
1.353 @@ -1411,7 +1411,7 @@
1.354 b \<in> (convex hull s) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull")
1.355 apply(rule,rule hull_minimal,rule) unfolding insert_iff prefer 3 apply rule proof-
1.356 fix x assume x:"x = a \<or> x \<in> s"
1.357 - thus "x\<in>?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer
1.358 + thus "x\<in>?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer
1.359 apply(rule_tac x=0 in exI) using assms hull_subset[of s convex] by auto
1.360 next
1.361 fix x assume "x\<in>?hull"
1.362 @@ -1435,11 +1435,11 @@
1.363 thus ?thesis unfolding obt1(5) obt2(5) * using assms hull_subset[of s convex] by(auto simp add: ** scaleR_right_distrib)
1.364 next
1.365 have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
1.366 - also have "\<dots> = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
1.367 + also have "\<dots> = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
1.368 also have "\<dots> = u * v1 + v * v2" by simp finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
1.369 case False have "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2" apply -
1.370 apply(rule add_nonneg_nonneg) prefer 4 apply(rule add_nonneg_nonneg) apply(rule_tac [!] mult_nonneg_nonneg)
1.371 - using as(1,2) obt1(1,2) obt2(1,2) by auto
1.372 + using as(1,2) obt1(1,2) obt2(1,2) by auto
1.373 thus ?thesis unfolding obt1(5) obt2(5) unfolding * and ** using False
1.374 apply(rule_tac x="((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI) defer
1.375 apply(rule convex_convex_hull[of s, unfolded convex_def, rule_format]) using obt1(4) obt2(4)
1.376 @@ -1451,7 +1451,7 @@
1.377 have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono)
1.378 apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto
1.379 also have "\<dots> \<le> 1" unfolding right_distrib[symmetric] and as(3) using u1 u2 by auto
1.380 - finally
1.381 + finally
1.382 show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI)
1.383 apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def
1.384 using as(1,2) obt1(1,2) obt2(1,2) * by(auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps)
1.385 @@ -1484,7 +1484,7 @@
1.386 have *:"\<And>P (x1::'a) x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)"
1.387 "{1..k1 + k2} \<inter> {1..k1} = {1..k1}" "{1..k1 + k2} \<inter> - {1..k1} = (\<lambda>i. i + k1) ` {1..k2}"
1.388 prefer 3 apply(rule,rule) unfolding image_iff apply(rule_tac x="x - k1" in bexI) by(auto simp add: not_le)
1.389 - have inj:"inj_on (\<lambda>i. i + k1) {1..k2}" unfolding inj_on_def by auto
1.390 + have inj:"inj_on (\<lambda>i. i + k1) {1..k2}" unfolding inj_on_def by auto
1.391 show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" apply(rule)
1.392 apply(rule_tac x="k1 + k2" in exI, rule_tac x="\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)" in exI)
1.393 apply(rule_tac x="\<lambda>i. if i \<in> {1..k1} then x1 i else x2 (i - k1)" in exI) apply(rule,rule) defer apply(rule)
1.394 @@ -1507,9 +1507,9 @@
1.395 shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>
1.396 setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set")
1.397 proof(rule hull_unique, auto simp add: convex_def[of ?set])
1.398 - fix x assume "x\<in>s" thus " \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = x"
1.399 + fix x assume "x\<in>s" thus " \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = x"
1.400 apply(rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI) apply auto
1.401 - unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto
1.402 + unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto
1.403 next
1.404 fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
1.405 fix ux assume ux:"\<forall>x\<in>s. 0 \<le> ux x" "setsum ux s = (1::real)"
1.406 @@ -1522,9 +1522,9 @@
1.407 moreover have "(\<Sum>x\<in>s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
1.408 unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[symmetric] and scaleR_right.setsum [symmetric] by auto
1.409 ultimately show "\<exists>uc. (\<forall>x\<in>s. 0 \<le> uc x) \<and> setsum uc s = 1 \<and> (\<Sum>x\<in>s. uc x *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
1.410 - apply(rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI) by auto
1.411 + apply(rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI) by auto
1.412 next
1.413 - fix t assume t:"s \<subseteq> t" "convex t"
1.414 + fix t assume t:"s \<subseteq> t" "convex t"
1.415 fix u assume u:"\<forall>x\<in>s. 0 \<le> u x" "setsum u s = (1::real)"
1.416 thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> t" using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]]
1.417 using assms and t(1) by auto
1.418 @@ -1554,9 +1554,9 @@
1.419 { fix j assume "j\<in>{1..k}"
1.420 hence "y j \<in> p" "0 \<le> setsum u {i. Suc 0 \<le> i \<and> i \<le> k \<and> y i = y j}"
1.421 using obt(1)[THEN bspec[where x=j]] and obt(2) apply simp
1.422 - apply(rule setsum_nonneg) using obt(1) by auto }
1.423 + apply(rule setsum_nonneg) using obt(1) by auto }
1.424 moreover
1.425 - have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v}) = 1"
1.426 + have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v}) = 1"
1.427 unfolding setsum_image_gen[OF fin, symmetric] using obt(2) by auto
1.428 moreover have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v} *\<^sub>R v) = x"
1.429 using setsum_image_gen[OF fin, of "\<lambda>i. u i *\<^sub>R y i" y, symmetric]
1.430 @@ -1570,7 +1570,7 @@
1.431 then obtain s u where obt:"finite s" "s \<subseteq> p" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto
1.432
1.433 obtain f where f:"inj_on f {1..card s}" "f ` {1..card s} = s" using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto
1.434 -
1.435 +
1.436 { fix i::nat assume "i\<in>{1..card s}"
1.437 hence "f i \<in> s" apply(subst f(2)[symmetric]) by auto
1.438 hence "0 \<le> u (f i)" "f i \<in> p" using obt(2,3) by auto }
1.439 @@ -1584,10 +1584,10 @@
1.440 by (auto simp add: setsum_constant_scaleR) }
1.441
1.442 hence "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *\<^sub>R f i) = y"
1.443 - unfolding setsum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f]
1.444 + unfolding setsum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f]
1.445 unfolding f using setsum_cong2[of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"]
1.446 using setsum_cong2 [of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto
1.447 -
1.448 +
1.449 ultimately have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> setsum u {1..k} = 1 \<and> (\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y"
1.450 apply(rule_tac x="card s" in exI) apply(rule_tac x="u \<circ> f" in exI) apply(rule_tac x=f in exI) by fastforce
1.451 hence "y \<in> ?lhs" unfolding convex_hull_indexed by auto }
1.452 @@ -1672,22 +1672,22 @@
1.453
1.454 lemma affine_dependent_imp_dependent:
1.455 shows "affine_dependent s \<Longrightarrow> dependent s"
1.456 - unfolding affine_dependent_def dependent_def
1.457 + unfolding affine_dependent_def dependent_def
1.458 using affine_hull_subset_span by auto
1.459
1.460 lemma dependent_imp_affine_dependent:
1.461 assumes "dependent {x - a| x . x \<in> s}" "a \<notin> s"
1.462 shows "affine_dependent (insert a s)"
1.463 proof-
1.464 - from assms(1)[unfolded dependent_explicit] obtain S u v
1.465 + from assms(1)[unfolded dependent_explicit] obtain S u v
1.466 where obt:"finite S" "S \<subseteq> {x - a |x. x \<in> s}" "v\<in>S" "u v \<noteq> 0" "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0" by auto
1.467 def t \<equiv> "(\<lambda>x. x + a) ` S"
1.468
1.469 have inj:"inj_on (\<lambda>x. x + a) S" unfolding inj_on_def by auto
1.470 have "0\<notin>S" using obt(2) assms(2) unfolding subset_eq by auto
1.471 - have fin:"finite t" and "t\<subseteq>s" unfolding t_def using obt(1,2) by auto
1.472 -
1.473 - hence "finite (insert a t)" and "insert a t \<subseteq> insert a s" by auto
1.474 + have fin:"finite t" and "t\<subseteq>s" unfolding t_def using obt(1,2) by auto
1.475 +
1.476 + hence "finite (insert a t)" and "insert a t \<subseteq> insert a s" by auto
1.477 moreover have *:"\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x)) = (\<Sum>x\<in>t. Q x)"
1.478 apply(rule setsum_cong2) using `a\<notin>s` `t\<subseteq>s` by auto
1.479 have "(\<Sum>x\<in>insert a t. if x = a then - (\<Sum>x\<in>t. u (x - a)) else u (x - a)) = 0"
1.480 @@ -1696,13 +1696,13 @@
1.481 apply(rule_tac x="v + a" in bexI) using obt(3,4) and `0\<notin>S` unfolding t_def by auto
1.482 moreover have *:"\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x) *\<^sub>R x) = (\<Sum>x\<in>t. Q x *\<^sub>R x)"
1.483 apply(rule setsum_cong2) using `a\<notin>s` `t\<subseteq>s` by auto
1.484 - have "(\<Sum>x\<in>t. u (x - a)) *\<^sub>R a = (\<Sum>v\<in>t. u (v - a) *\<^sub>R v)"
1.485 + have "(\<Sum>x\<in>t. u (x - a)) *\<^sub>R a = (\<Sum>v\<in>t. u (v - a) *\<^sub>R v)"
1.486 unfolding scaleR_left.setsum unfolding t_def and setsum_reindex[OF inj] and o_def
1.487 using obt(5) by (auto simp add: setsum_addf scaleR_right_distrib)
1.488 hence "(\<Sum>v\<in>insert a t. (if v = a then - (\<Sum>x\<in>t. u (x - a)) else u (v - a)) *\<^sub>R v) = 0"
1.489 unfolding setsum_clauses(2)[OF fin] using `a\<notin>s` `t\<subseteq>s` by (auto simp add: *)
1.490 ultimately show ?thesis unfolding affine_dependent_explicit
1.491 - apply(rule_tac x="insert a t" in exI) by auto
1.492 + apply(rule_tac x="insert a t" in exI) by auto
1.493 qed
1.494
1.495 lemma convex_cone:
1.496 @@ -1722,7 +1722,7 @@
1.497 proof-
1.498 have "s\<noteq>{}" using assms by auto then obtain a where "a\<in>s" by auto
1.499 have *:"{x - a |x. x \<in> s - {a}} = (\<lambda>x. x - a) ` (s - {a})" by auto
1.500 - have "card {x - a |x. x \<in> s - {a}} = card (s - {a})" unfolding *
1.501 + have "card {x - a |x. x \<in> s - {a}} = card (s - {a})" unfolding *
1.502 apply(rule card_image) unfolding inj_on_def by auto
1.503 also have "\<dots> > DIM('a)" using assms(2)
1.504 unfolding card_Diff_singleton[OF assms(1) `a\<in>s`] by auto
1.505 @@ -1737,7 +1737,7 @@
1.506 from assms(2) have "s \<noteq> {}" by auto
1.507 then obtain a where "a\<in>s" by auto
1.508 have *:"{x - a |x. x \<in> s - {a}} = (\<lambda>x. x - a) ` (s - {a})" by auto
1.509 - have **:"card {x - a |x. x \<in> s - {a}} = card (s - {a})" unfolding *
1.510 + have **:"card {x - a |x. x \<in> s - {a}} = card (s - {a})" unfolding *
1.511 apply(rule card_image) unfolding inj_on_def by auto
1.512 have "dim {x - a |x. x \<in> s - {a}} \<le> dim s"
1.513 apply(rule subset_le_dim) unfolding subset_eq
1.514 @@ -1777,14 +1777,14 @@
1.515 qed hence "i\<noteq>{}" unfolding i_def by auto
1.516
1.517 hence "t \<ge> 0" using Min_ge_iff[of i 0 ] and obt(1) unfolding t_def i_def
1.518 - using obt(4)[unfolded le_less] apply auto unfolding divide_le_0_iff by auto
1.519 + using obt(4)[unfolded le_less] apply auto unfolding divide_le_0_iff by auto
1.520 have t:"\<forall>v\<in>s. u v + t * w v \<ge> 0" proof
1.521 fix v assume "v\<in>s" hence v:"0\<le>u v" using obt(4)[THEN bspec[where x=v]] by auto
1.522 show"0 \<le> u v + t * w v" proof(cases "w v < 0")
1.523 - case False thus ?thesis apply(rule_tac add_nonneg_nonneg)
1.524 + case False thus ?thesis apply(rule_tac add_nonneg_nonneg)
1.525 using v apply simp apply(rule mult_nonneg_nonneg) using `t\<ge>0` by auto next
1.526 case True hence "t \<le> u v / (- w v)" using `v\<in>s`
1.527 - unfolding t_def i_def apply(rule_tac Min_le) using obt(1) by auto
1.528 + unfolding t_def i_def apply(rule_tac Min_le) using obt(1) by auto
1.529 thus ?thesis unfolding real_0_le_add_iff
1.530 using pos_le_divide_eq[OF True[unfolded neg_0_less_iff_less[symmetric]]] by auto
1.531 qed qed
1.532 @@ -1793,10 +1793,10 @@
1.533 using Min_in[OF _ `i\<noteq>{}`] and obt(1) unfolding i_def t_def by auto
1.534 hence a:"a\<in>s" "u a + t * w a = 0" by auto
1.535 have *:"\<And>f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)"
1.536 - unfolding setsum_diff1'[OF obt(1) `a\<in>s`] by auto
1.537 + unfolding setsum_diff1'[OF obt(1) `a\<in>s`] by auto
1.538 have "(\<Sum>v\<in>s. u v + t * w v) = 1"
1.539 unfolding setsum_addf wv(1) setsum_right_distrib[symmetric] obt(5) by auto
1.540 - moreover have "(\<Sum>v\<in>s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y"
1.541 + moreover have "(\<Sum>v\<in>s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y"
1.542 unfolding setsum_addf obt(6) scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] wv(4)
1.543 using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp
1.544 ultimately have "?P (n - 1)" apply(rule_tac x="(s - {a})" in exI)
1.545 @@ -1840,7 +1840,7 @@
1.546 moreover have "(%x. a + x) ` S <= (%x. a + x) ` (affine hull S)" using hull_subset[of S] by auto
1.547 ultimately have h1: "affine hull ((%x. a + x) ` S) <= (%x. a + x) ` (affine hull S)" by (metis hull_minimal)
1.548 have "affine((%x. -a + x) ` (affine hull ((%x. a + x) ` S)))" using affine_translation affine_affine_hull by auto
1.549 -moreover have "(%x. -a + x) ` (%x. a + x) ` S <= (%x. -a + x) ` (affine hull ((%x. a + x) ` S))" using hull_subset[of "(%x. a + x) ` S"] by auto
1.550 +moreover have "(%x. -a + x) ` (%x. a + x) ` S <= (%x. -a + x) ` (affine hull ((%x. a + x) ` S))" using hull_subset[of "(%x. a + x) ` S"] by auto
1.551 moreover have "S=(%x. -a + x) ` (%x. a + x) ` S" using translation_assoc[of "-a" a] by auto
1.552 ultimately have "(%x. -a + x) ` (affine hull ((%x. a + x) ` S)) >= (affine hull S)" by (metis hull_minimal)
1.553 hence "affine hull ((%x. a + x) ` S) >= (%x. a + x) ` (affine hull S)" by auto
1.554 @@ -1854,15 +1854,15 @@
1.555 obtain x where x_def: "x : S & x : affine hull (S - {x})" using assms affine_dependent_def by auto
1.556 have "op + a ` (S - {x}) = op + a ` S - {a + x}" by auto
1.557 hence "a+x : affine hull ((%x. a + x) ` S - {a+x})" using affine_hull_translation[of a "S-{x}"] x_def by auto
1.558 -moreover have "a+x : (%x. a + x) ` S" using x_def by auto
1.559 -ultimately show ?thesis unfolding affine_dependent_def by auto
1.560 +moreover have "a+x : (%x. a + x) ` S" using x_def by auto
1.561 +ultimately show ?thesis unfolding affine_dependent_def by auto
1.562 qed
1.563
1.564 lemma affine_dependent_translation_eq:
1.565 "affine_dependent S <-> affine_dependent ((%x. a + x) ` S)"
1.566 proof-
1.567 -{ assume "affine_dependent ((%x. a + x) ` S)"
1.568 - hence "affine_dependent S" using affine_dependent_translation[of "((%x. a + x) ` S)" "-a"] translation_assoc[of "-a" a] by auto
1.569 +{ assume "affine_dependent ((%x. a + x) ` S)"
1.570 + hence "affine_dependent S" using affine_dependent_translation[of "((%x. a + x) ` S)" "-a"] translation_assoc[of "-a" a] by auto
1.571 } from this show ?thesis using affine_dependent_translation by auto
1.572 qed
1.573
1.574 @@ -1871,7 +1871,7 @@
1.575 shows "dependent S"
1.576 proof-
1.577 obtain s u where s_u_def: "finite s & s ~= {} & s <= S & setsum u s = 1 & (SUM v:s. u v *\<^sub>R v) = 0" using assms affine_hull_explicit[of S] by auto
1.578 -hence "EX v:s. u v ~= 0" using setsum_not_0[of "u" "s"] by auto
1.579 +hence "EX v:s. u v ~= 0" using setsum_not_0[of "u" "s"] by auto
1.580 hence "finite s & s <= S & (EX v:s. u v ~= 0 & (SUM v:s. u v *\<^sub>R v) = 0)" using s_u_def by auto
1.581 from this show ?thesis unfolding dependent_explicit[of S] by auto
1.582 qed
1.583 @@ -1887,17 +1887,17 @@
1.584 hence "(x~=0) ==> dependent S" using x_def dependent_def by auto
1.585 moreover
1.586 { assume "x=0" hence "0 : affine hull S" using x_def hull_mono[of "S - {0}" S] by auto
1.587 - hence "dependent S" using affine_hull_0_dependent by auto
1.588 + hence "dependent S" using affine_hull_0_dependent by auto
1.589 } ultimately show ?thesis by auto
1.590 qed
1.591
1.592 lemma affine_dependent_iff_dependent:
1.593 assumes "a ~: S"
1.594 - shows "affine_dependent (insert a S) <-> dependent ((%x. -a + x) ` S)"
1.595 + shows "affine_dependent (insert a S) <-> dependent ((%x. -a + x) ` S)"
1.596 proof-
1.597 have "(op + (- a) ` S)={x - a| x . x : S}" by auto
1.598 -from this show ?thesis using affine_dependent_translation_eq[of "(insert a S)" "-a"]
1.599 - affine_dependent_imp_dependent2 assms
1.600 +from this show ?thesis using affine_dependent_translation_eq[of "(insert a S)" "-a"]
1.601 + affine_dependent_imp_dependent2 assms
1.602 dependent_imp_affine_dependent[of a S] by auto
1.603 qed
1.604
1.605 @@ -1906,25 +1906,25 @@
1.606 shows "affine_dependent S <-> dependent ((%x. -a + x) ` (S-{a}))"
1.607 proof-
1.608 have "insert a (S - {a})=S" using assms by auto
1.609 -from this show ?thesis using assms affine_dependent_iff_dependent[of a "S-{a}"] by auto
1.610 +from this show ?thesis using assms affine_dependent_iff_dependent[of a "S-{a}"] by auto
1.611 qed
1.612
1.613 lemma affine_hull_insert_span_gen:
1.614 - shows "affine hull (insert a s) = (%x. a+x) ` span ((%x. -a+x) ` s)"
1.615 + shows "affine hull (insert a s) = (%x. a+x) ` span ((%x. -a+x) ` s)"
1.616 proof-
1.617 have h1: "{x - a |x. x : s}=((%x. -a+x) ` s)" by auto
1.618 -{ assume "a ~: s" hence ?thesis using affine_hull_insert_span[of a s] h1 by auto}
1.619 +{ assume "a ~: s" hence ?thesis using affine_hull_insert_span[of a s] h1 by auto}
1.620 moreover
1.621 { assume a1: "a : s"
1.622 have "EX x. x:s & -a+x=0" apply (rule exI[of _ a]) using a1 by auto
1.623 hence "insert 0 ((%x. -a+x) ` (s - {a}))=(%x. -a+x) ` s" by auto
1.624 - hence "span ((%x. -a+x) ` (s - {a}))=span ((%x. -a+x) ` s)"
1.625 + hence "span ((%x. -a+x) ` (s - {a}))=span ((%x. -a+x) ` s)"
1.626 using span_insert_0[of "op + (- a) ` (s - {a})"] by auto
1.627 - moreover have "{x - a |x. x : (s - {a})}=((%x. -a+x) ` (s - {a}))" by auto
1.628 + moreover have "{x - a |x. x : (s - {a})}=((%x. -a+x) ` (s - {a}))" by auto
1.629 moreover have "insert a (s - {a})=(insert a s)" using assms by auto
1.630 ultimately have ?thesis using assms affine_hull_insert_span[of "a" "s-{a}"] by auto
1.631 -}
1.632 -ultimately show ?thesis by auto
1.633 +}
1.634 +ultimately show ?thesis by auto
1.635 qed
1.636
1.637 lemma affine_hull_span2:
1.638 @@ -1953,21 +1953,21 @@
1.639 proof-
1.640 obtain a where a_def: "a : S" using assms by auto
1.641 hence h0: "independent ((%x. -a + x) ` (S-{a}))" using affine_dependent_iff_dependent2 assms by auto
1.642 -from this obtain B
1.643 - where B_def: "(%x. -a+x) ` (S - {a}) <= B & B <= (%x. -a+x) ` V & independent B & (%x. -a+x) ` V <= span B"
1.644 +from this obtain B
1.645 + where B_def: "(%x. -a+x) ` (S - {a}) <= B & B <= (%x. -a+x) ` V & independent B & (%x. -a+x) ` V <= span B"
1.646 using maximal_independent_subset_extend[of "(%x. -a+x) ` (S-{a})" "(%x. -a + x) ` V"] assms by blast
1.647 def T == "(%x. a+x) ` (insert 0 B)" hence "T=insert a ((%x. a+x) ` B)" by auto
1.648 hence "affine hull T = (%x. a+x) ` span B" using affine_hull_insert_span_gen[of a "((%x. a+x) ` B)"] translation_assoc[of "-a" a B] by auto
1.649 hence "V <= affine hull T" using B_def assms translation_inverse_subset[of a V "span B"] by auto
1.650 moreover have "T<=V" using T_def B_def a_def assms by auto
1.651 -ultimately have "affine hull T = affine hull V"
1.652 +ultimately have "affine hull T = affine hull V"
1.653 by (metis Int_absorb1 Int_absorb2 hull_hull hull_mono)
1.654 moreover have "S<=T" using T_def B_def translation_inverse_subset[of a "S-{a}" B] by auto
1.655 moreover have "~(affine_dependent T)" using T_def affine_dependent_translation_eq[of "insert 0 B"] affine_dependent_imp_dependent2 B_def by auto
1.656 ultimately show ?thesis using `T<=V` by auto
1.657 qed
1.658
1.659 -lemma affine_basis_exists:
1.660 +lemma affine_basis_exists:
1.661 fixes V :: "('n::euclidean_space) set"
1.662 shows "? B. B <= V & ~(affine_dependent B) & affine hull V = affine hull B"
1.663 proof-
1.664 @@ -1986,7 +1986,7 @@
1.665 definition "aff_dim V = (SOME d :: int. ? B. (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = d+1))"
1.666
1.667 lemma aff_dim_basis_exists:
1.668 - fixes V :: "('n::euclidean_space) set"
1.669 + fixes V :: "('n::euclidean_space) set"
1.670 shows "? B. (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = aff_dim V+1)"
1.671 proof-
1.672 obtain B where B_def: "~(affine_dependent B) & (affine hull B=affine hull V)" using affine_basis_exists[of V] by auto
1.673 @@ -1995,7 +1995,7 @@
1.674
1.675 lemma affine_hull_nonempty: "(S ~= {}) <-> affine hull S ~= {}"
1.676 proof-
1.677 -have "(S = {}) ==> affine hull S = {}"using affine_hull_empty by auto
1.678 +have "(S = {}) ==> affine hull S = {}"using affine_hull_empty by auto
1.679 moreover have "affine hull S = {} ==> S = {}" unfolding hull_def by auto
1.680 ultimately show "(S ~= {}) <-> affine hull S ~= {}" by blast
1.681 qed
1.682 @@ -2003,19 +2003,19 @@
1.683 lemma aff_dim_parallel_subspace_aux:
1.684 fixes B :: "('n::euclidean_space) set"
1.685 assumes "~(affine_dependent B)" "a:B"
1.686 -shows "finite B & ((card B) - 1 = dim (span ((%x. -a+x) ` (B-{a}))))"
1.687 +shows "finite B & ((card B) - 1 = dim (span ((%x. -a+x) ` (B-{a}))))"
1.688 proof-
1.689 have "independent ((%x. -a + x) ` (B-{a}))" using affine_dependent_iff_dependent2 assms by auto
1.690 hence fin: "dim (span ((%x. -a+x) ` (B-{a}))) = card ((%x. -a + x) ` (B-{a}))" "finite ((%x. -a + x) ` (B - {a}))" using indep_card_eq_dim_span[of "(%x. -a+x) ` (B-{a})"] by auto
1.691 -{ assume emp: "(%x. -a + x) ` (B - {a}) = {}"
1.692 +{ assume emp: "(%x. -a + x) ` (B - {a}) = {}"
1.693 have "B=insert a ((%x. a + x) ` (%x. -a + x) ` (B - {a}))" using translation_assoc[of "a" "-a" "(B - {a})"] assms by auto
1.694 hence "B={a}" using emp by auto
1.695 - hence ?thesis using assms fin by auto
1.696 + hence ?thesis using assms fin by auto
1.697 }
1.698 moreover
1.699 { assume "(%x. -a + x) ` (B - {a}) ~= {}"
1.700 hence "card ((%x. -a + x) ` (B - {a}))>0" using fin by auto
1.701 - moreover have h1: "card ((%x. -a + x) ` (B-{a})) = card (B-{a})"
1.702 + moreover have h1: "card ((%x. -a + x) ` (B-{a})) = card (B-{a})"
1.703 apply (rule card_image) using translate_inj_on by auto
1.704 ultimately have "card (B-{a})>0" by auto
1.705 hence "finite(B-{a})" using card_gt_0_iff[of "(B - {a})"] by auto
1.706 @@ -2031,15 +2031,15 @@
1.707 shows "aff_dim V=int(dim L)"
1.708 proof-
1.709 obtain B where B_def: "affine hull B = affine hull V & ~ affine_dependent B & int (card B) = aff_dim V + 1" using aff_dim_basis_exists by auto
1.710 -hence "B~={}" using assms B_def affine_hull_nonempty[of V] affine_hull_nonempty[of B] by auto
1.711 +hence "B~={}" using assms B_def affine_hull_nonempty[of V] affine_hull_nonempty[of B] by auto
1.712 from this obtain a where a_def: "a : B" by auto
1.713 def Lb == "span ((%x. -a+x) ` (B-{a}))"
1.714 moreover have "affine_parallel (affine hull B) Lb"
1.715 using Lb_def B_def assms affine_hull_span2[of a B] a_def affine_parallel_commut[of "Lb" "(affine hull B)"] unfolding affine_parallel_def by auto
1.716 moreover have "subspace Lb" using Lb_def subspace_span by auto
1.717 moreover have "affine hull B ~= {}" using assms B_def affine_hull_nonempty[of V] by auto
1.718 - ultimately have "L=Lb" using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B_def by auto
1.719 - hence "dim L=dim Lb" by auto
1.720 + ultimately have "L=Lb" using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B_def by auto
1.721 + hence "dim L=dim Lb" by auto
1.722 moreover have "(card B) - 1 = dim Lb" "finite B" using Lb_def aff_dim_parallel_subspace_aux a_def B_def by auto
1.723 (* hence "card B=dim Lb+1" using `B~={}` card_gt_0_iff[of B] by auto *)
1.724 ultimately show ?thesis using B_def `B~={}` card_gt_0_iff[of B] by auto
1.725 @@ -2050,23 +2050,23 @@
1.726 assumes "~(affine_dependent B)"
1.727 shows "finite B"
1.728 proof-
1.729 -{ assume "B~={}" from this obtain a where "a:B" by auto
1.730 - hence ?thesis using aff_dim_parallel_subspace_aux assms by auto
1.731 +{ assume "B~={}" from this obtain a where "a:B" by auto
1.732 + hence ?thesis using aff_dim_parallel_subspace_aux assms by auto
1.733 } from this show ?thesis by auto
1.734 qed
1.735
1.736 lemma independent_finite:
1.737 fixes B :: "('n::euclidean_space) set"
1.738 -assumes "independent B"
1.739 +assumes "independent B"
1.740 shows "finite B"
1.741 using affine_dependent_imp_dependent[of B] aff_independent_finite[of B] assms by auto
1.742
1.743 lemma subspace_dim_equal:
1.744 assumes "subspace (S :: ('n::euclidean_space) set)" "subspace T" "S <= T" "dim S >= dim T"
1.745 shows "S=T"
1.746 -proof-
1.747 +proof-
1.748 obtain B where B_def: "B <= S & independent B & S <= span B & (card B = dim S)" using basis_exists[of S] by auto
1.749 -hence "span B <= S" using span_mono[of B S] span_eq[of S] assms by metis
1.750 +hence "span B <= S" using span_mono[of B S] span_eq[of S] assms by metis
1.751 hence "span B = S" using B_def by auto
1.752 have "dim S = dim T" using assms dim_subset[of S T] by auto
1.753 hence "T <= span B" using card_eq_dim[of B T] B_def independent_finite assms by auto
1.754 @@ -2080,18 +2080,18 @@
1.755 have "?A <= ?B" by auto
1.756 moreover have s: "subspace ?B" using subspace_substandard[of "%i. i ~: d"] .
1.757 ultimately have "span ?A <= ?B" using span_mono[of "?A" "?B"] span_eq[of "?B"] by blast
1.758 -moreover have "card d <= dim (span ?A)" using independent_card_le_dim[of "?A" "span ?A"]
1.759 +moreover have "card d <= dim (span ?A)" using independent_card_le_dim[of "?A" "span ?A"]
1.760 independent_substdbasis[OF assms] card_substdbasis[OF assms] span_inc[of "?A"] by auto
1.761 moreover hence "dim ?B <= dim (span ?A)" using dim_substandard[OF assms] by auto
1.762 -ultimately show ?thesis using s subspace_dim_equal[of "span ?A" "?B"]
1.763 +ultimately show ?thesis using s subspace_dim_equal[of "span ?A" "?B"]
1.764 subspace_span[of "?A"] by auto
1.765 qed
1.766
1.767 lemma basis_to_substdbasis_subspace_isomorphism:
1.768 -fixes B :: "('a::euclidean_space) set"
1.769 +fixes B :: "('a::euclidean_space) set"
1.770 assumes "independent B"
1.771 -shows "EX f d. card d = card B & linear f & f ` B = {basis i::'a |i. i : (d :: nat set)} &
1.772 - f ` span B = {x. ALL i<DIM('a). i ~: d --> x $$ i = (0::real)} & inj_on f (span B) \<and> d\<subseteq>{..<DIM('a)}"
1.773 +shows "EX f d. card d = card B & linear f & f ` B = {basis i::'a |i. i : (d :: nat set)} &
1.774 + f ` span B = {x. ALL i<DIM('a). i ~: d --> x $$ i = (0::real)} & inj_on f (span B) \<and> d\<subseteq>{..<DIM('a)}"
1.775 proof-
1.776 have B:"card B=dim B" using dim_unique[of B B "card B"] assms span_inc[of B] by auto
1.777 def d \<equiv> "{..<dim B}" have t:"card d = dim B" unfolding d_def by auto
1.778 @@ -2106,11 +2106,11 @@
1.779 unfolding span_substd_basis[OF d,symmetric] card_substdbasis[OF d] apply(rule span_inc)
1.780 apply(rule independent_substdbasis[OF d]) apply(rule,assumption)
1.781 unfolding t[symmetric] span_substd_basis[OF d] dim_substandard[OF d] by auto
1.782 - from this t `card B=dim B` show ?thesis using d by auto
1.783 + from this t `card B=dim B` show ?thesis using d by auto
1.784 qed
1.785
1.786 lemma aff_dim_empty:
1.787 -fixes S :: "('n::euclidean_space) set"
1.788 +fixes S :: "('n::euclidean_space) set"
1.789 shows "S = {} <-> aff_dim S = -1"
1.790 proof-
1.791 obtain B where "affine hull B = affine hull S & ~ affine_dependent B & int (card B) = aff_dim S + 1" using aff_dim_basis_exists by auto
1.792 @@ -2119,49 +2119,49 @@
1.793 qed
1.794
1.795 lemma aff_dim_affine_hull:
1.796 -shows "aff_dim (affine hull S)=aff_dim S"
1.797 -unfolding aff_dim_def using hull_hull[of _ S] by auto
1.798 +shows "aff_dim (affine hull S)=aff_dim S"
1.799 +unfolding aff_dim_def using hull_hull[of _ S] by auto
1.800
1.801 lemma aff_dim_affine_hull2:
1.802 assumes "affine hull S=affine hull T"
1.803 shows "aff_dim S=aff_dim T" unfolding aff_dim_def using assms by auto
1.804
1.805 -lemma aff_dim_unique:
1.806 -fixes B V :: "('n::euclidean_space) set"
1.807 +lemma aff_dim_unique:
1.808 +fixes B V :: "('n::euclidean_space) set"
1.809 assumes "(affine hull B=affine hull V) & ~(affine_dependent B)"
1.810 shows "of_nat(card B) = aff_dim V+1"
1.811 proof-
1.812 { assume "B={}" hence "V={}" using affine_hull_nonempty[of V] affine_hull_nonempty[of B] assms by auto
1.813 - hence "aff_dim V = (-1::int)" using aff_dim_empty by auto
1.814 + hence "aff_dim V = (-1::int)" using aff_dim_empty by auto
1.815 hence ?thesis using `B={}` by auto
1.816 }
1.817 moreover
1.818 -{ assume "B~={}" from this obtain a where a_def: "a:B" by auto
1.819 +{ assume "B~={}" from this obtain a where a_def: "a:B" by auto
1.820 def Lb == "span ((%x. -a+x) ` (B-{a}))"
1.821 have "affine_parallel (affine hull B) Lb"
1.822 - using Lb_def affine_hull_span2[of a B] a_def affine_parallel_commut[of "Lb" "(affine hull B)"]
1.823 + using Lb_def affine_hull_span2[of a B] a_def affine_parallel_commut[of "Lb" "(affine hull B)"]
1.824 unfolding affine_parallel_def by auto
1.825 moreover have "subspace Lb" using Lb_def subspace_span by auto
1.826 - ultimately have "aff_dim B=int(dim Lb)" using aff_dim_parallel_subspace[of B Lb] `B~={}` by auto
1.827 + ultimately have "aff_dim B=int(dim Lb)" using aff_dim_parallel_subspace[of B Lb] `B~={}` by auto
1.828 moreover have "(card B) - 1 = dim Lb" "finite B" using Lb_def aff_dim_parallel_subspace_aux a_def assms by auto
1.829 ultimately have "(of_nat(card B) = aff_dim B+1)" using `B~={}` card_gt_0_iff[of B] by auto
1.830 hence ?thesis using aff_dim_affine_hull2 assms by auto
1.831 } ultimately show ?thesis by blast
1.832 qed
1.833
1.834 -lemma aff_dim_affine_independent:
1.835 -fixes B :: "('n::euclidean_space) set"
1.836 +lemma aff_dim_affine_independent:
1.837 +fixes B :: "('n::euclidean_space) set"
1.838 assumes "~(affine_dependent B)"
1.839 shows "of_nat(card B) = aff_dim B+1"
1.840 using aff_dim_unique[of B B] assms by auto
1.841
1.842 -lemma aff_dim_sing:
1.843 -fixes a :: "'n::euclidean_space"
1.844 +lemma aff_dim_sing:
1.845 +fixes a :: "'n::euclidean_space"
1.846 shows "aff_dim {a}=0"
1.847 using aff_dim_affine_independent[of "{a}"] affine_independent_sing by auto
1.848
1.849 lemma aff_dim_inner_basis_exists:
1.850 - fixes V :: "('n::euclidean_space) set"
1.851 + fixes V :: "('n::euclidean_space) set"
1.852 shows "? B. B<=V & (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = aff_dim V+1)"
1.853 proof-
1.854 obtain B where B_def: "~(affine_dependent B) & B<=V & (affine hull B=affine hull V)" using affine_basis_exists[of V] by auto
1.855 @@ -2170,11 +2170,11 @@
1.856 qed
1.857
1.858 lemma aff_dim_le_card:
1.859 -fixes V :: "('n::euclidean_space) set"
1.860 +fixes V :: "('n::euclidean_space) set"
1.861 assumes "finite V"
1.862 shows "aff_dim V <= of_nat(card V) - 1"
1.863 proof-
1.864 - obtain B where B_def: "B<=V & (of_nat(card B) = aff_dim V+1)" using aff_dim_inner_basis_exists[of V] by auto
1.865 + obtain B where B_def: "B<=V & (of_nat(card B) = aff_dim V+1)" using aff_dim_inner_basis_exists[of V] by auto
1.866 moreover hence "card B <= card V" using assms card_mono by auto
1.867 ultimately show ?thesis by auto
1.868 qed
1.869 @@ -2184,13 +2184,13 @@
1.870 assumes "affine_parallel (affine hull S) (affine hull T)"
1.871 shows "aff_dim S=aff_dim T"
1.872 proof-
1.873 -{ assume "T~={}" "S~={}"
1.874 - from this obtain L where L_def: "subspace L & affine_parallel (affine hull T) L"
1.875 +{ assume "T~={}" "S~={}"
1.876 + from this obtain L where L_def: "subspace L & affine_parallel (affine hull T) L"
1.877 using affine_parallel_subspace[of "affine hull T"] affine_affine_hull[of T] affine_hull_nonempty by auto
1.878 hence "aff_dim T = int(dim L)" using aff_dim_parallel_subspace `T~={}` by auto
1.879 - moreover have "subspace L & affine_parallel (affine hull S) L"
1.880 + moreover have "subspace L & affine_parallel (affine hull S) L"
1.881 using L_def affine_parallel_assoc[of "affine hull S" "affine hull T" L] assms by auto
1.882 - moreover hence "aff_dim S = int(dim L)" using aff_dim_parallel_subspace `S~={}` by auto
1.883 + moreover hence "aff_dim S = int(dim L)" using aff_dim_parallel_subspace `S~={}` by auto
1.884 ultimately have ?thesis by auto
1.885 }
1.886 moreover
1.887 @@ -2206,21 +2206,21 @@
1.888
1.889 lemma aff_dim_translation_eq:
1.890 fixes a :: "'n::euclidean_space"
1.891 -shows "aff_dim ((%x. a + x) ` S)=aff_dim S"
1.892 +shows "aff_dim ((%x. a + x) ` S)=aff_dim S"
1.893 proof-
1.894 have "affine_parallel (affine hull S) (affine hull ((%x. a + x) ` S))" unfolding affine_parallel_def apply (rule exI[of _ "a"]) using affine_hull_translation[of a S] by auto
1.895 -from this show ?thesis using aff_dim_parallel_eq[of S "(%x. a + x) ` S"] by auto
1.896 +from this show ?thesis using aff_dim_parallel_eq[of S "(%x. a + x) ` S"] by auto
1.897 qed
1.898
1.899 lemma aff_dim_affine:
1.900 fixes S L :: "('n::euclidean_space) set"
1.901 assumes "S ~= {}" "affine S"
1.902 assumes "subspace L" "affine_parallel S L"
1.903 -shows "aff_dim S=int(dim L)"
1.904 +shows "aff_dim S=int(dim L)"
1.905 proof-
1.906 -have 1: "(affine hull S) = S" using assms affine_hull_eq[of S] by auto
1.907 +have 1: "(affine hull S) = S" using assms affine_hull_eq[of S] by auto
1.908 hence "affine_parallel (affine hull S) L" using assms by (simp add:1)
1.909 -from this show ?thesis using assms aff_dim_parallel_subspace[of S L] by blast
1.910 +from this show ?thesis using assms aff_dim_parallel_subspace[of S L] by blast
1.911 qed
1.912
1.913 lemma dim_affine_hull:
1.914 @@ -2236,7 +2236,7 @@
1.915 lemma aff_dim_subspace:
1.916 fixes S :: "('n::euclidean_space) set"
1.917 assumes "S ~= {}" "subspace S"
1.918 -shows "aff_dim S=int(dim S)" using aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] by auto
1.919 +shows "aff_dim S=int(dim S)" using aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] by auto
1.920
1.921 lemma aff_dim_zero:
1.922 fixes S :: "('n::euclidean_space) set"
1.923 @@ -2244,7 +2244,7 @@
1.924 shows "aff_dim S=int(dim S)"
1.925 proof-
1.926 have "subspace(affine hull S)" using subspace_affine[of "affine hull S"] affine_affine_hull assms by auto
1.927 -hence "aff_dim (affine hull S) =int(dim (affine hull S))" using assms aff_dim_subspace[of "affine hull S"] by auto
1.928 +hence "aff_dim (affine hull S) =int(dim (affine hull S))" using assms aff_dim_subspace[of "affine hull S"] by auto
1.929 from this show ?thesis using aff_dim_affine_hull[of S] dim_affine_hull[of S] by auto
1.930 qed
1.931
1.932 @@ -2260,13 +2260,13 @@
1.933 from this show ?thesis by auto
1.934 qed
1.935
1.936 -lemma independent_card_le_aff_dim:
1.937 +lemma independent_card_le_aff_dim:
1.938 assumes "(B::('n::euclidean_space) set) <= V"
1.939 - assumes "~(affine_dependent B)"
1.940 + assumes "~(affine_dependent B)"
1.941 shows "int(card B) <= aff_dim V+1"
1.942 proof-
1.943 -{ assume "B~={}"
1.944 - from this obtain T where T_def: "~(affine_dependent T) & B<=T & T<=V & affine hull T = affine hull V"
1.945 +{ assume "B~={}"
1.946 + from this obtain T where T_def: "~(affine_dependent T) & B<=T & T<=V & affine hull T = affine hull V"
1.947 using assms extend_to_affine_basis[of B V] by auto
1.948 hence "of_nat(card T) = aff_dim V+1" using aff_dim_unique by auto
1.949 hence ?thesis using T_def card_mono[of T B] aff_independent_finite[of T] by auto
1.950 @@ -2291,7 +2291,7 @@
1.951 lemma aff_dim_subset_univ:
1.952 fixes S :: "('n::euclidean_space) set"
1.953 shows "aff_dim S <= int(DIM('n))"
1.954 -proof -
1.955 +proof -
1.956 have "aff_dim (UNIV :: ('n::euclidean_space) set) = int(DIM('n))" using aff_dim_univ by auto
1.957 from this show "aff_dim (S:: ('n::euclidean_space) set) <= int(DIM('n))" using assms aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
1.958 qed
1.959 @@ -2300,21 +2300,21 @@
1.960 assumes "affine (S :: ('n::euclidean_space) set)" "affine T" "S ~= {}" "S <= T" "aff_dim S = aff_dim T"
1.961 shows "S=T"
1.962 proof-
1.963 -obtain a where "a : S" using assms by auto
1.964 +obtain a where "a : S" using assms by auto
1.965 hence "a : T" using assms by auto
1.966 def LS == "{y. ? x : S. (-a)+x=y}"
1.967 -hence ls: "subspace LS & affine_parallel S LS" using assms parallel_subspace_explicit[of S a LS] `a : S` by auto
1.968 +hence ls: "subspace LS & affine_parallel S LS" using assms parallel_subspace_explicit[of S a LS] `a : S` by auto
1.969 hence h1: "int(dim LS) = aff_dim S" using assms aff_dim_affine[of S LS] by auto
1.970 have "T ~= {}" using assms by auto
1.971 -def LT == "{y. ? x : T. (-a)+x=y}"
1.972 +def LT == "{y. ? x : T. (-a)+x=y}"
1.973 hence lt: "subspace LT & affine_parallel T LT" using assms parallel_subspace_explicit[of T a LT] `a : T` by auto
1.974 -hence "int(dim LT) = aff_dim T" using assms aff_dim_affine[of T LT] `T ~= {}` by auto
1.975 +hence "int(dim LT) = aff_dim T" using assms aff_dim_affine[of T LT] `T ~= {}` by auto
1.976 hence "dim LS = dim LT" using h1 assms by auto
1.977 moreover have "LS <= LT" using LS_def LT_def assms by auto
1.978 ultimately have "LS=LT" using subspace_dim_equal[of LS LT] ls lt by auto
1.979 -moreover have "S = {x. ? y : LS. a+y=x}" using LS_def by auto
1.980 +moreover have "S = {x. ? y : LS. a+y=x}" using LS_def by auto
1.981 moreover have "T = {x. ? y : LT. a+y=x}" using LT_def by auto
1.982 -ultimately show ?thesis by auto
1.983 +ultimately show ?thesis by auto
1.984 qed
1.985
1.986 lemma affine_hull_univ:
1.987 @@ -2325,7 +2325,7 @@
1.988 have "S ~= {}" using assms aff_dim_empty[of S] by auto
1.989 have h0: "S <= affine hull S" using hull_subset[of S _] by auto
1.990 have h1: "aff_dim (UNIV :: ('n::euclidean_space) set) = aff_dim S" using aff_dim_univ assms by auto
1.991 -hence h2: "aff_dim (affine hull S) <= aff_dim (UNIV :: ('n::euclidean_space) set)" using aff_dim_subset_univ[of "affine hull S"] assms h0 by auto
1.992 +hence h2: "aff_dim (affine hull S) <= aff_dim (UNIV :: ('n::euclidean_space) set)" using aff_dim_subset_univ[of "affine hull S"] assms h0 by auto
1.993 have h3: "aff_dim S <= aff_dim (affine hull S)" using h0 aff_dim_subset[of S "affine hull S"] assms by auto
1.994 hence h4: "aff_dim (affine hull S) = aff_dim (UNIV :: ('n::euclidean_space) set)" using h0 h1 h2 by auto
1.995 from this show ?thesis using affine_dim_equal[of "affine hull S" "(UNIV :: ('n::euclidean_space) set)"] affine_affine_hull[of S] affine_UNIV assms h4 h0 `S ~= {}` by auto
1.996 @@ -2334,23 +2334,23 @@
1.997 lemma aff_dim_convex_hull:
1.998 fixes S :: "('n::euclidean_space) set"
1.999 shows "aff_dim (convex hull S)=aff_dim S"
1.1000 - using aff_dim_affine_hull[of S] convex_hull_subset_affine_hull[of S]
1.1001 - hull_subset[of S "convex"] aff_dim_subset[of S "convex hull S"]
1.1002 + using aff_dim_affine_hull[of S] convex_hull_subset_affine_hull[of S]
1.1003 + hull_subset[of S "convex"] aff_dim_subset[of S "convex hull S"]
1.1004 aff_dim_subset[of "convex hull S" "affine hull S"] by auto
1.1005
1.1006 lemma aff_dim_cball:
1.1007 -fixes a :: "'n::euclidean_space"
1.1008 +fixes a :: "'n::euclidean_space"
1.1009 assumes "0<e"
1.1010 shows "aff_dim (cball a e) = int (DIM('n))"
1.1011 proof-
1.1012 have "(%x. a + x) ` (cball 0 e)<=cball a e" unfolding cball_def dist_norm by auto
1.1013 hence "aff_dim (cball (0 :: 'n::euclidean_space) e) <= aff_dim (cball a e)"
1.1014 - using aff_dim_translation_eq[of a "cball 0 e"]
1.1015 + using aff_dim_translation_eq[of a "cball 0 e"]
1.1016 aff_dim_subset[of "op + a ` cball 0 e" "cball a e"] by auto
1.1017 -moreover have "aff_dim (cball (0 :: 'n::euclidean_space) e) = int (DIM('n))"
1.1018 - using hull_inc[of "(0 :: 'n::euclidean_space)" "cball 0 e"] centre_in_cball[of "(0 :: 'n::euclidean_space)"] assms
1.1019 +moreover have "aff_dim (cball (0 :: 'n::euclidean_space) e) = int (DIM('n))"
1.1020 + using hull_inc[of "(0 :: 'n::euclidean_space)" "cball 0 e"] centre_in_cball[of "(0 :: 'n::euclidean_space)"] assms
1.1021 by (simp add: dim_cball[of e] aff_dim_zero[of "cball 0 e"])
1.1022 -ultimately show ?thesis using aff_dim_subset_univ[of "cball a e"] by auto
1.1023 +ultimately show ?thesis using aff_dim_subset_univ[of "cball a e"] by auto
1.1024 qed
1.1025
1.1026 lemma aff_dim_open:
1.1027 @@ -2361,7 +2361,7 @@
1.1028 obtain x where "x:S" using assms by auto
1.1029 from this obtain e where e_def: "e>0 & cball x e <= S" using open_contains_cball[of S] assms by auto
1.1030 from this have "aff_dim (cball x e) <= aff_dim S" using aff_dim_subset by auto
1.1031 -from this show ?thesis using aff_dim_cball[of e x] aff_dim_subset_univ[of S] e_def by auto
1.1032 +from this show ?thesis using aff_dim_cball[of e x] aff_dim_subset_univ[of S] e_def by auto
1.1033 qed
1.1034
1.1035 lemma low_dim_interior:
1.1036 @@ -2369,9 +2369,9 @@
1.1037 assumes "~(aff_dim S = int (DIM('n)))"
1.1038 shows "interior S = {}"
1.1039 proof-
1.1040 -have "aff_dim(interior S) <= aff_dim S"
1.1041 - using interior_subset aff_dim_subset[of "interior S" S] by auto
1.1042 -from this show ?thesis using aff_dim_open[of "interior S"] aff_dim_subset_univ[of S] assms by auto
1.1043 +have "aff_dim(interior S) <= aff_dim S"
1.1044 + using interior_subset aff_dim_subset[of "interior S" S] by auto
1.1045 +from this show ?thesis using aff_dim_open[of "interior S"] aff_dim_subset_univ[of S] assms by auto
1.1046 qed
1.1047
1.1048 subsection {* Relative interior of a set *}
1.1049 @@ -2388,8 +2388,8 @@
1.1050 using a h1 by auto
1.1051 qed
1.1052
1.1053 -lemma mem_rel_interior:
1.1054 - "x : rel_interior S <-> (? T. open T & x : (T Int S) & (T Int (affine hull S)) <= S)"
1.1055 +lemma mem_rel_interior:
1.1056 + "x : rel_interior S <-> (? T. open T & x : (T Int S) & (T Int (affine hull S)) <= S)"
1.1057 by (auto simp add: rel_interior)
1.1058
1.1059 lemma mem_rel_interior_ball: "x : rel_interior S <-> x : S & (? e. 0 < e & ((ball x e) Int (affine hull S)) <= S)"
1.1060 @@ -2399,12 +2399,12 @@
1.1061 apply simp
1.1062 done
1.1063
1.1064 -lemma rel_interior_ball:
1.1065 - "rel_interior S = {x : S. ? e. e>0 & ((ball x e) Int (affine hull S)) <= S}"
1.1066 - using mem_rel_interior_ball [of _ S] by auto
1.1067 +lemma rel_interior_ball:
1.1068 + "rel_interior S = {x : S. ? e. e>0 & ((ball x e) Int (affine hull S)) <= S}"
1.1069 + using mem_rel_interior_ball [of _ S] by auto
1.1070
1.1071 lemma mem_rel_interior_cball: "x : rel_interior S <-> x : S & (? e. 0 < e & ((cball x e) Int (affine hull S)) <= S)"
1.1072 - apply (simp add: rel_interior, safe)
1.1073 + apply (simp add: rel_interior, safe)
1.1074 apply (force simp add: open_contains_cball)
1.1075 apply (rule_tac x="ball x e" in exI)
1.1076 apply (simp add: subset_trans [OF ball_subset_cball])
1.1077 @@ -2413,8 +2413,8 @@
1.1078
1.1079 lemma rel_interior_cball: "rel_interior S = {x : S. ? e. e>0 & ((cball x e) Int (affine hull S)) <= S}" using mem_rel_interior_cball [of _ S] by auto
1.1080
1.1081 -lemma rel_interior_empty: "rel_interior {} = {}"
1.1082 - by (auto simp add: rel_interior_def)
1.1083 +lemma rel_interior_empty: "rel_interior {} = {}"
1.1084 + by (auto simp add: rel_interior_def)
1.1085
1.1086 lemma affine_hull_sing: "affine hull {a :: 'n::euclidean_space} = {a}"
1.1087 by (metis affine_hull_eq affine_sing)
1.1088 @@ -2428,15 +2428,15 @@
1.1089 fixes S T :: "('n::euclidean_space) set"
1.1090 assumes "S<=T" "affine hull S=affine hull T"
1.1091 shows "rel_interior S <= rel_interior T"
1.1092 - using assms by (auto simp add: rel_interior_def)
1.1093 -
1.1094 -lemma rel_interior_subset: "rel_interior S <= S"
1.1095 + using assms by (auto simp add: rel_interior_def)
1.1096 +
1.1097 +lemma rel_interior_subset: "rel_interior S <= S"
1.1098 by (auto simp add: rel_interior_def)
1.1099
1.1100 -lemma rel_interior_subset_closure: "rel_interior S <= closure S"
1.1101 - using rel_interior_subset by (auto simp add: closure_def)
1.1102 -
1.1103 -lemma interior_subset_rel_interior: "interior S <= rel_interior S"
1.1104 +lemma rel_interior_subset_closure: "rel_interior S <= closure S"
1.1105 + using rel_interior_subset by (auto simp add: closure_def)
1.1106 +
1.1107 +lemma interior_subset_rel_interior: "interior S <= rel_interior S"
1.1108 by (auto simp add: rel_interior interior_def)
1.1109
1.1110 lemma interior_rel_interior:
1.1111 @@ -2444,7 +2444,7 @@
1.1112 assumes "aff_dim S = int(DIM('n))"
1.1113 shows "rel_interior S = interior S"
1.1114 proof -
1.1115 -have "affine hull S = UNIV" using assms affine_hull_univ[of S] by auto
1.1116 +have "affine hull S = UNIV" using assms affine_hull_univ[of S] by auto
1.1117 from this show ?thesis unfolding rel_interior interior_def by auto
1.1118 qed
1.1119
1.1120 @@ -2459,16 +2459,16 @@
1.1121 shows "interior S = (if aff_dim S = int(DIM('n)) then rel_interior S else {})"
1.1122 by (metis interior_rel_interior low_dim_interior)
1.1123
1.1124 -lemma rel_interior_univ:
1.1125 +lemma rel_interior_univ:
1.1126 fixes S :: "('n::euclidean_space) set"
1.1127 shows "rel_interior (affine hull S) = affine hull S"
1.1128 proof-
1.1129 -have h1: "rel_interior (affine hull S) <= affine hull S" using rel_interior_subset by auto
1.1130 +have h1: "rel_interior (affine hull S) <= affine hull S" using rel_interior_subset by auto
1.1131 { fix x assume x_def: "x : affine hull S"
1.1132 obtain e :: real where "e=1" by auto
1.1133 hence "e>0 & ball x e Int affine hull (affine hull S) <= affine hull S" using hull_hull[of _ S] by auto
1.1134 hence "x : rel_interior (affine hull S)" using x_def rel_interior_ball[of "affine hull S"] by auto
1.1135 -} from this show ?thesis using h1 by auto
1.1136 +} from this show ?thesis using h1 by auto
1.1137 qed
1.1138
1.1139 lemma rel_interior_univ2: "rel_interior (UNIV :: ('n::euclidean_space) set) = UNIV"
1.1140 @@ -2478,25 +2478,25 @@
1.1141 fixes S :: "('a::euclidean_space) set"
1.1142 assumes "convex S" "c : rel_interior S" "x : S" "0 < e" "e <= 1"
1.1143 shows "x - e *\<^sub>R (x - c) : rel_interior S"
1.1144 -proof-
1.1145 -(* Proof is a modified copy of the proof of similar lemma mem_interior_convex_shrink
1.1146 +proof-
1.1147 +(* Proof is a modified copy of the proof of similar lemma mem_interior_convex_shrink
1.1148 *)
1.1149 -obtain d where "d>0" and d:"ball c d Int affine hull S <= S"
1.1150 +obtain d where "d>0" and d:"ball c d Int affine hull S <= S"
1.1151 using assms(2) unfolding mem_rel_interior_ball by auto
1.1152 { fix y assume as:"dist (x - e *\<^sub>R (x - c)) y < e * d & y : affine hull S"
1.1153 have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
1.1154 have "x : affine hull S" using assms hull_subset[of S] by auto
1.1155 - moreover have "1 / e + - ((1 - e) / e) = 1"
1.1156 + moreover have "1 / e + - ((1 - e) / e) = 1"
1.1157 using `e>0` left_diff_distrib[of "1" "(1-e)" "1/e"] by auto
1.1158 ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x : affine hull S"
1.1159 - using as affine_affine_hull[of S] mem_affine[of "affine hull S" y x "(1 / e)" "-((1 - e) / e)"] by (simp add: algebra_simps)
1.1160 + using as affine_affine_hull[of S] mem_affine[of "affine hull S" y x "(1 / e)" "-((1 - e) / e)"] by (simp add: algebra_simps)
1.1161 have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
1.1162 unfolding dist_norm unfolding norm_scaleR[symmetric] apply(rule arg_cong[where f=norm]) using `e>0`
1.1163 - by(auto simp add:euclidean_eq[where 'a='a] field_simps)
1.1164 + by(auto simp add:euclidean_eq[where 'a='a] field_simps)
1.1165 also have "... = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
1.1166 also have "... < d" using as[unfolded dist_norm] and `e>0`
1.1167 by(auto simp add:pos_divide_less_eq[OF `e>0`] mult_commute)
1.1168 - finally have "y : S" apply(subst *)
1.1169 + finally have "y : S" apply(subst *)
1.1170 apply(rule assms(1)[unfolded convex_alt,rule_format])
1.1171 apply(rule d[unfolded subset_eq,rule_format]) unfolding mem_ball using assms(3-5) ** by auto
1.1172 } hence "ball (x - e *\<^sub>R (x - c)) (e*d) Int affine hull S <= S" by auto
1.1173 @@ -2504,7 +2504,7 @@
1.1174 moreover have "c : S" using assms rel_interior_subset by auto
1.1175 moreover hence "x - e *\<^sub>R (x - c) : S"
1.1176 using mem_convex[of S x c e] apply (simp add: algebra_simps) using assms by auto
1.1177 -ultimately show ?thesis
1.1178 +ultimately show ?thesis
1.1179 using mem_rel_interior_ball[of "x - e *\<^sub>R (x - c)" S] `e>0` by auto
1.1180 qed
1.1181
1.1182 @@ -2513,13 +2513,13 @@
1.1183 shows "interior {a..} = {a<..}"
1.1184 proof-
1.1185 { fix y assume "a<y" hence "y : interior {a..}"
1.1186 - apply (simp add: mem_interior) apply (rule_tac x="(y-a)" in exI) apply (auto simp add: dist_norm)
1.1187 + apply (simp add: mem_interior) apply (rule_tac x="(y-a)" in exI) apply (auto simp add: dist_norm)
1.1188 done }
1.1189 moreover
1.1190 { fix y assume "y : interior {a..}" (*hence "a<=y" using interior_subset by auto*)
1.1191 - from this obtain e where e_def: "e>0 & cball y e \<subseteq> {a..}"
1.1192 + from this obtain e where e_def: "e>0 & cball y e \<subseteq> {a..}"
1.1193 using mem_interior_cball[of y "{a..}"] by auto
1.1194 - moreover hence "y-e : cball y e" by (auto simp add: cball_def dist_norm)
1.1195 + moreover hence "y-e : cball y e" by (auto simp add: cball_def dist_norm)
1.1196 ultimately have "a<=y-e" by auto
1.1197 hence "a<y" using e_def by auto
1.1198 } ultimately show ?thesis by auto
1.1199 @@ -2551,25 +2551,25 @@
1.1200 unfolding rel_open_def rel_interior_def apply auto
1.1201 using openin_subopen[of "subtopology euclidean (affine hull S)" S] by auto
1.1202
1.1203 -lemma opein_rel_interior:
1.1204 +lemma opein_rel_interior:
1.1205 "openin (subtopology euclidean (affine hull S)) (rel_interior S)"
1.1206 apply (simp add: rel_interior_def)
1.1207 apply (subst openin_subopen) by blast
1.1208
1.1209 -lemma affine_rel_open:
1.1210 +lemma affine_rel_open:
1.1211 fixes S :: "('n::euclidean_space) set"
1.1212 - assumes "affine S" shows "rel_open S"
1.1213 + assumes "affine S" shows "rel_open S"
1.1214 unfolding rel_open_def using assms rel_interior_univ[of S] affine_hull_eq[of S] by metis
1.1215
1.1216 -lemma affine_closed:
1.1217 +lemma affine_closed:
1.1218 fixes S :: "('n::euclidean_space) set"
1.1219 assumes "affine S" shows "closed S"
1.1220 proof-
1.1221 { assume "S ~= {}"
1.1222 from this obtain L where L_def: "subspace L & affine_parallel S L"
1.1223 using assms affine_parallel_subspace[of S] by auto
1.1224 - from this obtain "a" where a_def: "S=(op + a ` L)"
1.1225 - using affine_parallel_def[of L S] affine_parallel_commut by auto
1.1226 + from this obtain "a" where a_def: "S=(op + a ` L)"
1.1227 + using affine_parallel_def[of L S] affine_parallel_commut by auto
1.1228 have "closed L" using L_def closed_subspace by auto
1.1229 hence "closed S" using closed_translation a_def by auto
1.1230 } from this show ?thesis by auto
1.1231 @@ -2586,17 +2586,17 @@
1.1232 proof-
1.1233 have "affine hull (closure S) <= affine hull S"
1.1234 using hull_mono[of "closure S" "affine hull S" "affine"] closure_affine_hull[of S] hull_hull[of "affine" S] by auto
1.1235 -moreover have "affine hull (closure S) >= affine hull S"
1.1236 +moreover have "affine hull (closure S) >= affine hull S"
1.1237 using hull_mono[of "S" "closure S" "affine"] closure_subset by auto
1.1238 -ultimately show ?thesis by auto
1.1239 -qed
1.1240 -
1.1241 -lemma closure_aff_dim:
1.1242 +ultimately show ?thesis by auto
1.1243 +qed
1.1244 +
1.1245 +lemma closure_aff_dim:
1.1246 fixes S :: "('n::euclidean_space) set"
1.1247 shows "aff_dim (closure S) = aff_dim S"
1.1248 proof-
1.1249 have "aff_dim S <= aff_dim (closure S)" using aff_dim_subset closure_subset by auto
1.1250 -moreover have "aff_dim (closure S) <= aff_dim (affine hull S)"
1.1251 +moreover have "aff_dim (closure S) <= aff_dim (affine hull S)"
1.1252 using aff_dim_subset closure_affine_hull by auto
1.1253 moreover have "aff_dim (affine hull S) = aff_dim S" using aff_dim_affine_hull by auto
1.1254 ultimately show ?thesis by auto
1.1255 @@ -2606,10 +2606,10 @@
1.1256 fixes S :: "(_::euclidean_space) set"
1.1257 assumes "convex S" "c : rel_interior S" "x : closure S" "0 < e" "e <= 1"
1.1258 shows "x - e *\<^sub>R (x - c) : rel_interior S"
1.1259 -proof-
1.1260 +proof-
1.1261 (* Proof is a modified copy of the proof of similar lemma mem_interior_closure_convex_shrink
1.1262 *)
1.1263 -obtain d where "d>0" and d:"ball c d Int affine hull S <= S"
1.1264 +obtain d where "d>0" and d:"ball c d Int affine hull S <= S"
1.1265 using assms(2) unfolding mem_rel_interior_ball by auto
1.1266 have "EX y : S. norm (y - x) * (1 - e) < e * d" proof(cases "x : S")
1.1267 case True thus ?thesis using `e>0` `d>0` by(rule_tac bexI[where x=x], auto intro!: mult_pos_pos) next
1.1268 @@ -2631,18 +2631,18 @@
1.1269 have "x : affine hull S" using closure_affine_hull assms by auto
1.1270 moreover have "y : affine hull S" using `y : S` hull_subset[of S] by auto
1.1271 moreover have "c : affine hull S" using assms rel_interior_subset hull_subset[of S] by auto
1.1272 - ultimately have "z : affine hull S"
1.1273 - using z_def affine_affine_hull[of S]
1.1274 - mem_affine_3_minus [of "affine hull S" c x y "(1 - e) / e"]
1.1275 + ultimately have "z : affine hull S"
1.1276 + using z_def affine_affine_hull[of S]
1.1277 + mem_affine_3_minus [of "affine hull S" c x y "(1 - e) / e"]
1.1278 assms by (auto simp add: field_simps)
1.1279 hence "z : S" using d zball by auto
1.1280 obtain d1 where "d1>0" and d1:"ball z d1 <= ball c d"
1.1281 using zball open_ball[of c d] openE[of "ball c d" z] by auto
1.1282 hence "(ball z d1) Int (affine hull S) <= (ball c d) Int (affine hull S)" by auto
1.1283 - hence "(ball z d1) Int (affine hull S) <= S" using d by auto
1.1284 + hence "(ball z d1) Int (affine hull S) <= S" using d by auto
1.1285 hence "z : rel_interior S" using mem_rel_interior_ball using `d1>0` `z : S` by auto
1.1286 hence "y - e *\<^sub>R (y - z) : rel_interior S" using rel_interior_convex_shrink[of S z y e] assms`y : S` by auto
1.1287 - thus ?thesis using * by auto
1.1288 + thus ?thesis using * by auto
1.1289 qed
1.1290
1.1291 subsubsection{* Relative interior preserves under linear transformations *}
1.1292 @@ -2652,27 +2652,27 @@
1.1293 shows "((%x. a + x) ` rel_interior S) <= rel_interior ((%x. a + x) ` S)"
1.1294 proof-
1.1295 { fix x assume x_def: "x : rel_interior S"
1.1296 - from this obtain T where T_def: "open T & x : (T Int S) & (T Int (affine hull S)) <= S" using mem_rel_interior[of x S] by auto
1.1297 - from this have "open ((%x. a + x) ` T)" and
1.1298 - "(a + x) : (((%x. a + x) ` T) Int ((%x. a + x) ` S))" and
1.1299 - "(((%x. a + x) ` T) Int (affine hull ((%x. a + x) ` S))) <= ((%x. a + x) ` S)"
1.1300 - using affine_hull_translation[of a S] open_translation[of T a] x_def by auto
1.1301 - from this have "(a+x) : rel_interior ((%x. a + x) ` S)"
1.1302 - using mem_rel_interior[of "a+x" "((%x. a + x) ` S)"] by auto
1.1303 -} from this show ?thesis by auto
1.1304 + from this obtain T where T_def: "open T & x : (T Int S) & (T Int (affine hull S)) <= S" using mem_rel_interior[of x S] by auto
1.1305 + from this have "open ((%x. a + x) ` T)" and
1.1306 + "(a + x) : (((%x. a + x) ` T) Int ((%x. a + x) ` S))" and
1.1307 + "(((%x. a + x) ` T) Int (affine hull ((%x. a + x) ` S))) <= ((%x. a + x) ` S)"
1.1308 + using affine_hull_translation[of a S] open_translation[of T a] x_def by auto
1.1309 + from this have "(a+x) : rel_interior ((%x. a + x) ` S)"
1.1310 + using mem_rel_interior[of "a+x" "((%x. a + x) ` S)"] by auto
1.1311 +} from this show ?thesis by auto
1.1312 qed
1.1313
1.1314 lemma rel_interior_translation:
1.1315 fixes a :: "'n::euclidean_space"
1.1316 shows "rel_interior ((%x. a + x) ` S) = ((%x. a + x) ` rel_interior S)"
1.1317 proof-
1.1318 -have "(%x. (-a) + x) ` rel_interior ((%x. a + x) ` S) <= rel_interior S"
1.1319 - using rel_interior_translation_aux[of "-a" "(%x. a + x) ` S"]
1.1320 +have "(%x. (-a) + x) ` rel_interior ((%x. a + x) ` S) <= rel_interior S"
1.1321 + using rel_interior_translation_aux[of "-a" "(%x. a + x) ` S"]
1.1322 translation_assoc[of "-a" "a"] by auto
1.1323 -hence "((%x. a + x) ` rel_interior S) >= rel_interior ((%x. a + x) ` S)"
1.1324 - using translation_inverse_subset[of a "rel_interior (op + a ` S)" "rel_interior S"]
1.1325 +hence "((%x. a + x) ` rel_interior S) >= rel_interior ((%x. a + x) ` S)"
1.1326 + using translation_inverse_subset[of a "rel_interior (op + a ` S)" "rel_interior S"]
1.1327 by auto
1.1328 -from this show ?thesis using rel_interior_translation_aux[of a S] by auto
1.1329 +from this show ?thesis using rel_interior_translation_aux[of a S] by auto
1.1330 qed
1.1331
1.1332
1.1333 @@ -2681,15 +2681,15 @@
1.1334 shows "f ` (affine hull s) = affine hull f ` s"
1.1335 (* Proof is a modified copy of the proof of similar lemma convex_hull_linear_image
1.1336 *)
1.1337 - apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3
1.1338 + apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3
1.1339 apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption
1.1340 apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption
1.1341 proof-
1.1342 interpret f: bounded_linear f by fact
1.1343 - show "affine {x. f x : affine hull f ` s}"
1.1344 + show "affine {x. f x : affine hull f ` s}"
1.1345 unfolding affine_def by(auto simp add: f.scaleR f.add affine_affine_hull[unfolded affine_def, rule_format]) next
1.1346 interpret f: bounded_linear f by fact
1.1347 - show "affine {x. x : f ` (affine hull s)}" using affine_affine_hull[unfolded affine_def, of s]
1.1348 + show "affine {x. x : f ` (affine hull s)}" using affine_affine_hull[unfolded affine_def, of s]
1.1349 unfolding affine_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
1.1350 qed auto
1.1351
1.1352 @@ -2703,61 +2703,61 @@
1.1353 { fix z assume z_def: "z : rel_interior (f ` S)"
1.1354 have "z : f ` S" using z_def rel_interior_subset[of "f ` S"] by auto
1.1355 from this obtain x where x_def: "x : S & (f x = z)" by auto
1.1356 - obtain e2 where e2_def: "e2>0 & cball z e2 Int affine hull (f ` S) <= (f ` S)"
1.1357 + obtain e2 where e2_def: "e2>0 & cball z e2 Int affine hull (f ` S) <= (f ` S)"
1.1358 using z_def rel_interior_cball[of "f ` S"] by auto
1.1359 - obtain K where K_def: "K>0 & (! x. norm (f x) <= norm x * K)"
1.1360 + obtain K where K_def: "K>0 & (! x. norm (f x) <= norm x * K)"
1.1361 using assms RealVector.bounded_linear.pos_bounded[of f] by auto
1.1362 - def e1 == "1/K" hence e1_def: "e1>0 & (! x. e1 * norm (f x) <= norm x)"
1.1363 + def e1 == "1/K" hence e1_def: "e1>0 & (! x. e1 * norm (f x) <= norm x)"
1.1364 using K_def pos_le_divide_eq[of e1] by auto
1.1365 - def e == "e1 * e2" hence "e>0" using e1_def e2_def mult_pos_pos by auto
1.1366 + def e == "e1 * e2" hence "e>0" using e1_def e2_def mult_pos_pos by auto
1.1367 { fix y assume y_def: "y : cball x e Int affine hull S"
1.1368 - from this have h1: "f y : affine hull (f ` S)"
1.1369 - using affine_hull_linear_image[of f S] assms by auto
1.1370 - from y_def have "norm (x-y)<=e1 * e2"
1.1371 + from this have h1: "f y : affine hull (f ` S)"
1.1372 + using affine_hull_linear_image[of f S] assms by auto
1.1373 + from y_def have "norm (x-y)<=e1 * e2"
1.1374 using cball_def[of x e] dist_norm[of x y] e_def by auto
1.1375 moreover have "(f x)-(f y)=f (x-y)"
1.1376 using assms linear_sub[of f x y] linear_conv_bounded_linear[of f] by auto
1.1377 moreover have "e1 * norm (f (x-y)) <= norm (x-y)" using e1_def by auto
1.1378 ultimately have "e1 * norm ((f x)-(f y)) <= e1 * e2" by auto
1.1379 - hence "(f y) : (cball z e2)"
1.1380 + hence "(f y) : (cball z e2)"
1.1381 using cball_def[of "f x" e2] dist_norm[of "f x" "f y"] e1_def x_def by auto
1.1382 hence "f y : (f ` S)" using y_def e2_def h1 by auto
1.1383 - hence "y : S" using assms y_def hull_subset[of S] affine_hull_subset_span
1.1384 + hence "y : S" using assms y_def hull_subset[of S] affine_hull_subset_span
1.1385 inj_on_image_mem_iff[of f "span S" S y] by auto
1.1386 - }
1.1387 + }
1.1388 hence "z : f ` (rel_interior S)" using mem_rel_interior_cball[of x S] `e>0` x_def by auto
1.1389 -}
1.1390 +}
1.1391 moreover
1.1392 { fix x assume x_def: "x : rel_interior S"
1.1393 - from this obtain e2 where e2_def: "e2>0 & cball x e2 Int affine hull S <= S"
1.1394 + from this obtain e2 where e2_def: "e2>0 & cball x e2 Int affine hull S <= S"
1.1395 using rel_interior_cball[of S] by auto
1.1396 have "x : S" using x_def rel_interior_subset by auto
1.1397 hence *: "f x : f ` S" by auto
1.1398 - have "! x:span S. f x = 0 --> x = 0"
1.1399 - using assms subspace_span linear_conv_bounded_linear[of f]
1.1400 + have "! x:span S. f x = 0 --> x = 0"
1.1401 + using assms subspace_span linear_conv_bounded_linear[of f]
1.1402 linear_injective_on_subspace_0[of f "span S"] by auto
1.1403 - from this obtain e1 where e1_def: "e1>0 & (! x : span S. e1 * norm x <= norm (f x))"
1.1404 - using assms injective_imp_isometric[of "span S" f]
1.1405 + from this obtain e1 where e1_def: "e1>0 & (! x : span S. e1 * norm x <= norm (f x))"
1.1406 + using assms injective_imp_isometric[of "span S" f]
1.1407 subspace_span[of S] closed_subspace[of "span S"] by auto
1.1408 - def e == "e1 * e2" hence "e>0" using e1_def e2_def mult_pos_pos by auto
1.1409 + def e == "e1 * e2" hence "e>0" using e1_def e2_def mult_pos_pos by auto
1.1410 { fix y assume y_def: "y : cball (f x) e Int affine hull (f ` S)"
1.1411 - from this have "y : f ` (affine hull S)" using affine_hull_linear_image[of f S] assms by auto
1.1412 + from this have "y : f ` (affine hull S)" using affine_hull_linear_image[of f S] assms by auto
1.1413 from this obtain xy where xy_def: "xy : affine hull S & (f xy = y)" by auto
1.1414 - from this y_def have "norm ((f x)-(f xy))<=e1 * e2"
1.1415 + from this y_def have "norm ((f x)-(f xy))<=e1 * e2"
1.1416 using cball_def[of "f x" e] dist_norm[of "f x" y] e_def by auto
1.1417 moreover have "(f x)-(f xy)=f (x-xy)"
1.1418 using assms linear_sub[of f x xy] linear_conv_bounded_linear[of f] by auto
1.1419 - moreover have "x-xy : span S"
1.1420 - using subspace_sub[of "span S" x xy] subspace_span `x : S` xy_def
1.1421 + moreover have "x-xy : span S"
1.1422 + using subspace_sub[of "span S" x xy] subspace_span `x : S` xy_def
1.1423 affine_hull_subset_span[of S] span_inc by auto
1.1424 moreover hence "e1 * norm (x-xy) <= norm (f (x-xy))" using e1_def by auto
1.1425 ultimately have "e1 * norm (x-xy) <= e1 * e2" by auto
1.1426 hence "xy : (cball x e2)" using cball_def[of x e2] dist_norm[of x xy] e1_def by auto
1.1427 hence "y : (f ` S)" using xy_def e2_def by auto
1.1428 - }
1.1429 - hence "(f x) : rel_interior (f ` S)"
1.1430 + }
1.1431 + hence "(f x) : rel_interior (f ` S)"
1.1432 using mem_rel_interior_cball[of "(f x)" "(f ` S)"] * `e>0` by auto
1.1433 -}
1.1434 +}
1.1435 ultimately show ?thesis by auto
1.1436 qed
1.1437
1.1438 @@ -2765,7 +2765,7 @@
1.1439 fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
1.1440 assumes "bounded_linear f" and "inj f"
1.1441 shows "rel_interior (f ` S) = f ` (rel_interior S)"
1.1442 -using assms rel_interior_injective_on_span_linear_image[of f S]
1.1443 +using assms rel_interior_injective_on_span_linear_image[of f S]
1.1444 subset_inj_on[of f "UNIV" "span S"] by auto
1.1445
1.1446 subsection{* Some Properties of subset of standard basis *}
1.1447 @@ -2882,7 +2882,7 @@
1.1448 case False then obtain w where "w\<in>s" by auto
1.1449 show ?thesis unfolding caratheodory[of s]
1.1450 proof(induct ("DIM('a) + 1"))
1.1451 - have *:"{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}"
1.1452 + have *:"{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}"
1.1453 using compact_empty by auto
1.1454 case 0 thus ?case unfolding * by simp
1.1455 next
1.1456 @@ -2902,11 +2902,11 @@
1.1457 next
1.1458 fix x assume "x\<in>s"
1.1459 thus "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
1.1460 - apply(rule_tac x="{x}" in exI) unfolding convex_hull_singleton by auto
1.1461 + apply(rule_tac x="{x}" in exI) unfolding convex_hull_singleton by auto
1.1462 qed thus ?thesis using assms by simp
1.1463 next
1.1464 case False have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} =
1.1465 - { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u.
1.1466 + { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u.
1.1467 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> {x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> x \<in> convex hull t}}"
1.1468 unfolding set_eq_iff and mem_Collect_eq proof(rule,rule)
1.1469 fix x assume "\<exists>u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \<and>
1.1470 @@ -2943,7 +2943,7 @@
1.1471 qed
1.1472 qed
1.1473 qed
1.1474 - thus ?thesis using compact_convex_combinations[OF assms Suc] by simp
1.1475 + thus ?thesis using compact_convex_combinations[OF assms Suc] by simp
1.1476 qed
1.1477 qed
1.1478 qed
1.1479 @@ -2955,12 +2955,12 @@
1.1480 assumes "d \<noteq> 0"
1.1481 shows "dist a (b + d) > dist a b \<or> dist a (b - d) > dist a b"
1.1482 proof(cases "inner a d - inner b d > 0")
1.1483 - case True hence "0 < inner d d + (inner a d * 2 - inner b d * 2)"
1.1484 + case True hence "0 < inner d d + (inner a d * 2 - inner b d * 2)"
1.1485 apply(rule_tac add_pos_pos) using assms by auto
1.1486 thus ?thesis apply(rule_tac disjI2) unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff
1.1487 by (simp add: algebra_simps inner_commute)
1.1488 next
1.1489 - case False hence "0 < inner d d + (inner b d * 2 - inner a d * 2)"
1.1490 + case False hence "0 < inner d d + (inner b d * 2 - inner a d * 2)"
1.1491 apply(rule_tac add_pos_nonneg) using assms by auto
1.1492 thus ?thesis apply(rule_tac disjI1) unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff
1.1493 by (simp add: algebra_simps inner_commute)
1.1494 @@ -2996,7 +2996,7 @@
1.1495 next
1.1496 assume "u\<noteq>0" "v\<noteq>0"
1.1497 then obtain w where w:"w>0" "w<u" "w<v" using real_lbound_gt_zero[of u v] and obt(1,2) by auto
1.1498 - have "x\<noteq>b" proof(rule ccontr)
1.1499 + have "x\<noteq>b" proof(rule ccontr)
1.1500 assume "\<not> x\<noteq>b" hence "y=b" unfolding obt(5)
1.1501 using obt(3) by(auto simp add: scaleR_left_distrib[symmetric])
1.1502 thus False using obt(4) and False by simp qed
1.1503 @@ -3008,7 +3008,7 @@
1.1504 unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: algebra_simps)
1.1505 moreover have "(u + w) *\<^sub>R x + (v - w) *\<^sub>R b \<in> convex hull insert x s"
1.1506 unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
1.1507 - apply(rule_tac x="u + w" in exI) apply rule defer
1.1508 + apply(rule_tac x="u + w" in exI) apply rule defer
1.1509 apply(rule_tac x="v - w" in exI) using `u\<ge>0` and w and obt(3,4) by auto
1.1510 ultimately show ?thesis by auto
1.1511 next
1.1512 @@ -3017,7 +3017,7 @@
1.1513 unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: algebra_simps)
1.1514 moreover have "(u - w) *\<^sub>R x + (v + w) *\<^sub>R b \<in> convex hull insert x s"
1.1515 unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
1.1516 - apply(rule_tac x="u - w" in exI) apply rule defer
1.1517 + apply(rule_tac x="u - w" in exI) apply rule defer
1.1518 apply(rule_tac x="v + w" in exI) using `u\<ge>0` and w and obt(3,4) by auto
1.1519 ultimately show ?thesis by auto
1.1520 qed
1.1521 @@ -3066,7 +3066,7 @@
1.1522 thus ?thesis using obt(3)[THEN bspec[where x=u], THEN bspec[where x=y]] and obt(1)
1.1523 by (auto simp add: norm_minus_commute)
1.1524 qed auto
1.1525 -qed
1.1526 +qed
1.1527
1.1528 lemma simplex_extremal_le_exists:
1.1529 fixes s :: "('a::real_inner) set"
1.1530 @@ -3083,7 +3083,7 @@
1.1531 lemma closest_point_exists:
1.1532 assumes "closed s" "s \<noteq> {}"
1.1533 shows "closest_point s a \<in> s" "\<forall>y\<in>s. dist a (closest_point s a) \<le> dist a y"
1.1534 - unfolding closest_point_def apply(rule_tac[!] someI2_ex)
1.1535 + unfolding closest_point_def apply(rule_tac[!] someI2_ex)
1.1536 using distance_attains_inf[OF assms(1,2), of a] by auto
1.1537
1.1538 lemma closest_point_in_set:
1.1539 @@ -3096,7 +3096,7 @@
1.1540
1.1541 lemma closest_point_self:
1.1542 assumes "x \<in> s" shows "closest_point s x = x"
1.1543 - unfolding closest_point_def apply(rule some1_equality, rule ex1I[of _ x])
1.1544 + unfolding closest_point_def apply(rule some1_equality, rule ex1I[of _ x])
1.1545 using assms by auto
1.1546
1.1547 lemma closest_point_refl:
1.1548 @@ -3140,7 +3140,7 @@
1.1549 lemma closest_point_unique:
1.1550 assumes "convex s" "closed s" "x \<in> s" "\<forall>z\<in>s. dist a x \<le> dist a z"
1.1551 shows "x = closest_point s a"
1.1552 - using any_closest_point_unique[OF assms(1-3) _ assms(4), of "closest_point s a"]
1.1553 + using any_closest_point_unique[OF assms(1-3) _ assms(4), of "closest_point s a"]
1.1554 using closest_point_exists[OF assms(2)] and assms(3) by auto
1.1555
1.1556 lemma closest_point_dot:
1.1557 @@ -3171,7 +3171,7 @@
1.1558 lemma continuous_at_closest_point:
1.1559 assumes "convex s" "closed s" "s \<noteq> {}"
1.1560 shows "continuous (at x) (closest_point s)"
1.1561 - unfolding continuous_at_eps_delta
1.1562 + unfolding continuous_at_eps_delta
1.1563 using le_less_trans[OF closest_point_lipschitz[OF assms]] by auto
1.1564
1.1565 lemma continuous_on_closest_point:
1.1566 @@ -3265,7 +3265,7 @@
1.1567 hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac Sup) using assms(5) by auto
1.1568 fix x assume "x\<in>t" thus "inner a x < (k + b / 2)" using `0<b` and isLubD2[OF k, of "inner a x"] by auto
1.1569 next
1.1570 - fix x assume "x\<in>s"
1.1571 + fix x assume "x\<in>s"
1.1572 hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac Sup_least) using assms(5)
1.1573 using ab[THEN bspec[where x=x]] by auto
1.1574 thus "k + b / 2 < inner a x" using `0 < b` by auto
1.1575 @@ -3308,16 +3308,16 @@
1.1576 assumes "convex s" "convex (t::('a::euclidean_space) set)" "s \<noteq> {}" "t \<noteq> {}" "s \<inter> t = {}"
1.1577 shows "\<exists>a b. a \<noteq> 0 \<and> (\<forall>x\<in>s. inner a x \<le> b) \<and> (\<forall>x\<in>t. inner a x \<ge> b)"
1.1578 proof- from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
1.1579 - obtain a where "a\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x"
1.1580 - using assms(3-5) by auto
1.1581 + obtain a where "a\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x"
1.1582 + using assms(3-5) by auto
1.1583 hence "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x"
1.1584 by (force simp add: inner_diff)
1.1585 thus ?thesis
1.1586 apply(rule_tac x=a in exI, rule_tac x="Sup ((\<lambda>x. inner a x) ` s)" in exI) using `a\<noteq>0`
1.1587 apply auto
1.1588 - apply (rule Sup[THEN isLubD2])
1.1589 + apply (rule Sup[THEN isLubD2])
1.1590 prefer 4
1.1591 - apply (rule Sup_least)
1.1592 + apply (rule Sup_least)
1.1593 using assms(3-5) apply (auto simp add: setle_def)
1.1594 apply metis
1.1595 done
1.1596 @@ -3339,7 +3339,7 @@
1.1597 assumes "convex s" shows "convex(interior s)"
1.1598 unfolding convex_alt Ball_def mem_interior apply(rule,rule,rule,rule,rule,rule) apply(erule exE | erule conjE)+ proof-
1.1599 fix x y u assume u:"0 \<le> u" "u \<le> (1::real)"
1.1600 - fix e d assume ed:"ball x e \<subseteq> s" "ball y d \<subseteq> s" "0<d" "0<e"
1.1601 + fix e d assume ed:"ball x e \<subseteq> s" "ball y d \<subseteq> s" "0<d" "0<e"
1.1602 show "\<exists>e>0. ball ((1 - u) *\<^sub>R x + u *\<^sub>R y) e \<subseteq> s" apply(rule_tac x="min d e" in exI)
1.1603 apply rule unfolding subset_eq defer apply rule proof-
1.1604 fix z assume "z \<in> ball ((1 - u) *\<^sub>R x + u *\<^sub>R y) (min d e)"
1.1605 @@ -3361,7 +3361,7 @@
1.1606 assumes "(\<forall>s a. (convex hull (up a s)) \<subseteq> up a (convex hull s))"
1.1607 shows "(\<forall>s. up a (up (neg a) s) = s) \<and> (\<forall>s. up (neg a) (up a s) = s) \<and> (\<forall>s t a. s \<subseteq> t \<longrightarrow> up a s \<subseteq> up a t)
1.1608 \<Longrightarrow> \<forall>s. (convex hull (up a s)) = up a (convex hull s)"
1.1609 - using assms by(metis subset_antisym)
1.1610 + using assms by(metis subset_antisym)
1.1611
1.1612 lemma convex_hull_translation:
1.1613 "convex hull ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (convex hull s)"
1.1614 @@ -3439,7 +3439,7 @@
1.1615 fixes s :: "('a::euclidean_space) set"
1.1616 assumes "closed s" "convex s"
1.1617 shows "s = \<Inter> {h. s \<subseteq> h \<and> (\<exists>a b. h = {x. inner a x \<le> b})}"
1.1618 - apply(rule set_eqI, rule) unfolding Inter_iff Ball_def mem_Collect_eq apply(rule,rule,erule conjE) proof-
1.1619 + apply(rule set_eqI, rule) unfolding Inter_iff Ball_def mem_Collect_eq apply(rule,rule,erule conjE) proof-
1.1620 fix x assume "\<forall>xa. s \<subseteq> xa \<and> (\<exists>a b. xa = {x. inner a x \<le> b}) \<longrightarrow> x \<in> xa"
1.1621 hence "\<forall>a b. s \<subseteq> {x. inner a x \<le> b} \<longrightarrow> x \<in> {x. inner a x \<le> b}" by blast
1.1622 thus "x\<in>s" apply(rule_tac ccontr) apply(drule separating_hyperplane_closed_point[OF assms(2,1)])
1.1623 @@ -3466,7 +3466,7 @@
1.1624 assumes "finite s" "setsum f s = 0" "\<forall>x. g x = (0::real) \<longrightarrow> f x = (0::'a::euclidean_space)"
1.1625 shows "(setsum f {x\<in>s. 0 < g x}) = - setsum f {x\<in>s. g x < 0}"
1.1626 proof-
1.1627 - have *:"\<And>x. (if 0 < g x then f x else 0) + (if g x < 0 then f x else 0) = f x" using assms(3) by auto
1.1628 + have *:"\<And>x. (if 0 < g x then f x else 0) + (if g x < 0 then f x else 0) = f x" using assms(3) by auto
1.1629 show ?thesis unfolding eq_neg_iff_add_eq_0 and setsum_restrict_set''[OF assms(1)] and setsum_addf[symmetric] and *
1.1630 using assms(2) by assumption qed
1.1631
1.1632 @@ -3478,7 +3478,7 @@
1.1633 def z \<equiv> "(inverse (setsum u {x\<in>c. u x > 0})) *\<^sub>R setsum (\<lambda>x. u x *\<^sub>R x) {x\<in>c. u x > 0}"
1.1634 have "setsum u {x \<in> c. 0 < u x} \<noteq> 0" proof(cases "u v \<ge> 0")
1.1635 case False hence "u v < 0" by auto
1.1636 - thus ?thesis proof(cases "\<exists>w\<in>{x \<in> c. 0 < u x}. u w > 0")
1.1637 + thus ?thesis proof(cases "\<exists>w\<in>{x \<in> c. 0 < u x}. u w > 0")
1.1638 case True thus ?thesis using setsum_nonneg_eq_0_iff[of _ u, OF fin(1)] by auto
1.1639 next
1.1640 case False hence "setsum u c \<le> setsum (\<lambda>x. if x=v then u v else 0) c" apply(rule_tac setsum_mono) by auto
1.1641 @@ -3490,17 +3490,17 @@
1.1642 "(\<Sum>x\<in>{x \<in> c. 0 < u x} \<union> {x \<in> c. u x < 0}. u x *\<^sub>R x) = (\<Sum>x\<in>c. u x *\<^sub>R x)"
1.1643 using assms(1) apply(rule_tac[!] setsum_mono_zero_left) by auto
1.1644 hence "setsum u {x \<in> c. 0 < u x} = - setsum u {x \<in> c. 0 > u x}"
1.1645 - "(\<Sum>x\<in>{x \<in> c. 0 < u x}. u x *\<^sub>R x) = - (\<Sum>x\<in>{x \<in> c. 0 > u x}. u x *\<^sub>R x)"
1.1646 - unfolding eq_neg_iff_add_eq_0 using uv(1,4) by (auto simp add: setsum_Un_zero[OF fin, symmetric])
1.1647 - moreover have "\<forall>x\<in>{v \<in> c. u v < 0}. 0 \<le> inverse (setsum u {x \<in> c. 0 < u x}) * - u x"
1.1648 + "(\<Sum>x\<in>{x \<in> c. 0 < u x}. u x *\<^sub>R x) = - (\<Sum>x\<in>{x \<in> c. 0 > u x}. u x *\<^sub>R x)"
1.1649 + unfolding eq_neg_iff_add_eq_0 using uv(1,4) by (auto simp add: setsum_Un_zero[OF fin, symmetric])
1.1650 + moreover have "\<forall>x\<in>{v \<in> c. u v < 0}. 0 \<le> inverse (setsum u {x \<in> c. 0 < u x}) * - u x"
1.1651 apply (rule) apply (rule mult_nonneg_nonneg) using * by auto
1.1652
1.1653 ultimately have "z \<in> convex hull {v \<in> c. u v \<le> 0}" unfolding convex_hull_explicit mem_Collect_eq
1.1654 apply(rule_tac x="{v \<in> c. u v < 0}" in exI, rule_tac x="\<lambda>y. inverse (setsum u {x\<in>c. u x > 0}) * - u y" in exI)
1.1655 using assms(1) unfolding scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] and z_def
1.1656 by(auto simp add: setsum_negf setsum_right_distrib[symmetric])
1.1657 - moreover have "\<forall>x\<in>{v \<in> c. 0 < u v}. 0 \<le> inverse (setsum u {x \<in> c. 0 < u x}) * u x"
1.1658 - apply (rule) apply (rule mult_nonneg_nonneg) using * by auto
1.1659 + moreover have "\<forall>x\<in>{v \<in> c. 0 < u v}. 0 \<le> inverse (setsum u {x \<in> c. 0 < u x}) * u x"
1.1660 + apply (rule) apply (rule mult_nonneg_nonneg) using * by auto
1.1661 hence "z \<in> convex hull {v \<in> c. u v > 0}" unfolding convex_hull_explicit mem_Collect_eq
1.1662 apply(rule_tac x="{v \<in> c. 0 < u v}" in exI, rule_tac x="\<lambda>y. inverse (setsum u {x\<in>c. u x > 0}) * u y" in exI)
1.1663 using assms(1) unfolding scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] and z_def using *
1.1664 @@ -3539,7 +3539,7 @@
1.1665 using radon_partition[of "X ` f"] and affine_dependent_biggerset[of "X ` f"]
1.1666 unfolding card_image[OF True] and `card f = Suc n` using Suc(3) `finite f` and ng by auto
1.1667 have "m \<subseteq> X ` f" "p \<subseteq> X ` f" using mp(2) by auto
1.1668 - then obtain g h where gh:"m = X ` g" "p = X ` h" "g \<subseteq> f" "h \<subseteq> f" unfolding subset_image_iff by auto
1.1669 + then obtain g h where gh:"m = X ` g" "p = X ` h" "g \<subseteq> f" "h \<subseteq> f" unfolding subset_image_iff by auto
1.1670 hence "f \<union> (g \<union> h) = f" by auto
1.1671 hence f:"f = g \<union> h" using inj_on_Un_image_eq_iff[of X f "g \<union> h"] and True
1.1672 unfolding mp(2)[unfolded image_Un[symmetric] gh] by auto
1.1673 @@ -3565,7 +3565,7 @@
1.1674
1.1675 lemma compact_frontier_line_lemma:
1.1676 fixes s :: "('a::euclidean_space) set"
1.1677 - assumes "compact s" "0 \<in> s" "x \<noteq> 0"
1.1678 + assumes "compact s" "0 \<in> s" "x \<noteq> 0"
1.1679 obtains u where "0 \<le> u" "(u *\<^sub>R x) \<in> frontier s" "\<forall>v>u. (v *\<^sub>R x) \<notin> s"
1.1680 proof-
1.1681 obtain b where b:"b>0" "\<forall>x\<in>s. norm x \<le> b" using compact_imp_bounded[OF assms(1), unfolded bounded_pos] by auto
1.1682 @@ -3583,11 +3583,11 @@
1.1683
1.1684 have "norm x > 0" using assms(3)[unfolded zero_less_norm_iff[symmetric]] by auto
1.1685 { fix v assume as:"v > u" "v *\<^sub>R x \<in> s"
1.1686 - hence "v \<le> b / norm x" using b(2)[rule_format, OF as(2)]
1.1687 + hence "v \<le> b / norm x" using b(2)[rule_format, OF as(2)]
1.1688 using `u\<ge>0` unfolding pos_le_divide_eq[OF `norm x > 0`] by auto
1.1689 - hence "norm (v *\<^sub>R x) \<le> norm y" apply(rule_tac obt(6)[rule_format, unfolded dist_0_norm]) apply(rule IntI) defer
1.1690 - apply(rule as(2)) unfolding mem_Collect_eq apply(rule_tac x=v in exI)
1.1691 - using as(1) `u\<ge>0` by(auto simp add:field_simps)
1.1692 + hence "norm (v *\<^sub>R x) \<le> norm y" apply(rule_tac obt(6)[rule_format, unfolded dist_0_norm]) apply(rule IntI) defer
1.1693 + apply(rule as(2)) unfolding mem_Collect_eq apply(rule_tac x=v in exI)
1.1694 + using as(1) `u\<ge>0` by(auto simp add:field_simps)
1.1695 hence False unfolding obt(3) using `u\<ge>0` `norm x > 0` `v>u` by(auto simp add:field_simps)
1.1696 } note u_max = this
1.1697
1.1698 @@ -3635,7 +3635,7 @@
1.1699
1.1700 have "\<exists>surf. homeomorphism (frontier s) sphere pi surf"
1.1701 apply(rule homeomorphism_compact) apply(rule compact_frontier[OF assms(1)])
1.1702 - apply(rule continuous_on_subset[OF contpi]) defer apply(rule set_eqI,rule)
1.1703 + apply(rule continuous_on_subset[OF contpi]) defer apply(rule set_eqI,rule)
1.1704 unfolding inj_on_def prefer 3 apply(rule,rule,rule)
1.1705 proof- fix x assume "x\<in>pi ` frontier s" then obtain y where "y\<in>frontier s" "x = pi y" by auto
1.1706 thus "x \<in> sphere" using pi(1)[of y] and `0 \<notin> frontier s` by auto
1.1707 @@ -3645,9 +3645,9 @@
1.1708 thus "x \<in> pi ` frontier s" unfolding image_iff le_less pi_def apply(rule_tac x="u *\<^sub>R x" in bexI) using `norm x = 1` `0\<notin>frontier s` by auto
1.1709 next fix x y assume as:"x \<in> frontier s" "y \<in> frontier s" "pi x = pi y"
1.1710 hence xys:"x\<in>s" "y\<in>s" using fs by auto
1.1711 - from as(1,2) have nor:"norm x \<noteq> 0" "norm y \<noteq> 0" using `0\<notin>frontier s` by auto
1.1712 - from nor have x:"x = norm x *\<^sub>R ((inverse (norm y)) *\<^sub>R y)" unfolding as(3)[unfolded pi_def, symmetric] by auto
1.1713 - from nor have y:"y = norm y *\<^sub>R ((inverse (norm x)) *\<^sub>R x)" unfolding as(3)[unfolded pi_def] by auto
1.1714 + from as(1,2) have nor:"norm x \<noteq> 0" "norm y \<noteq> 0" using `0\<notin>frontier s` by auto
1.1715 + from nor have x:"x = norm x *\<^sub>R ((inverse (norm y)) *\<^sub>R y)" unfolding as(3)[unfolded pi_def, symmetric] by auto
1.1716 + from nor have y:"y = norm y *\<^sub>R ((inverse (norm x)) *\<^sub>R x)" unfolding as(3)[unfolded pi_def] by auto
1.1717 have "0 \<le> norm y * inverse (norm x)" "0 \<le> norm x * inverse (norm y)"
1.1718 unfolding divide_inverse[symmetric] apply(rule_tac[!] divide_nonneg_pos) using nor by auto
1.1719 hence "norm x = norm y" apply(rule_tac ccontr) unfolding neq_iff
1.1720 @@ -3658,12 +3658,12 @@
1.1721 qed(insert `0 \<notin> frontier s`, auto)
1.1722 then obtain surf where surf:"\<forall>x\<in>frontier s. surf (pi x) = x" "pi ` frontier s = sphere" "continuous_on (frontier s) pi"
1.1723 "\<forall>y\<in>sphere. pi (surf y) = y" "surf ` sphere = frontier s" "continuous_on sphere surf" unfolding homeomorphism_def by auto
1.1724 -
1.1725 +
1.1726 have cont_surfpi:"continuous_on (UNIV - {0}) (surf \<circ> pi)" apply(rule continuous_on_compose, rule contpi)
1.1727 apply(rule continuous_on_subset[of sphere], rule surf(6)) using pi(1) by auto
1.1728
1.1729 { fix x assume as:"x \<in> cball (0::'a) 1"
1.1730 - have "norm x *\<^sub>R surf (pi x) \<in> s" proof(cases "x=0 \<or> norm x = 1")
1.1731 + have "norm x *\<^sub>R surf (pi x) \<in> s" proof(cases "x=0 \<or> norm x = 1")
1.1732 case False hence "pi x \<in> sphere" "norm x < 1" using pi(1)[of x] as by(auto simp add: dist_norm)
1.1733 thus ?thesis apply(rule_tac assms(3)[rule_format, THEN DiffD1])
1.1734 apply(rule_tac fs[unfolded subset_eq, rule_format])
1.1735 @@ -3684,7 +3684,7 @@
1.1736 have "norm (surf (pi x)) \<noteq> 0" using ** False by auto
1.1737 hence "norm x = norm ((?a * norm x) *\<^sub>R surf (pi x))"
1.1738 unfolding norm_scaleR abs_mult abs_norm_cancel abs_of_pos[OF `?a > 0`] by auto
1.1739 - moreover have "pi x = pi ((inverse (norm (surf (pi x))) * norm x) *\<^sub>R surf (pi x))"
1.1740 + moreover have "pi x = pi ((inverse (norm (surf (pi x))) * norm x) *\<^sub>R surf (pi x))"
1.1741 unfolding pi(2)[OF *] surf(4)[rule_format, OF pix] ..
1.1742 moreover have "surf (pi x) \<in> frontier s" using surf(5) pix by auto
1.1743 hence "dist 0 (inverse (norm (surf (pi x))) *\<^sub>R x) \<le> 1" unfolding dist_norm
1.1744 @@ -3703,7 +3703,7 @@
1.1745 case False thus ?thesis apply (intro continuous_intros)
1.1746 using cont_surfpi unfolding continuous_on_eq_continuous_at[OF open_delete[OF open_UNIV]] o_def by auto
1.1747 next obtain B where B:"\<forall>x\<in>s. norm x \<le> B" using compact_imp_bounded[OF assms(1)] unfolding bounded_iff by auto
1.1748 - hence "B > 0" using assms(2) unfolding subset_eq apply(erule_tac x="basis 0" in ballE) defer
1.1749 + hence "B > 0" using assms(2) unfolding subset_eq apply(erule_tac x="basis 0" in ballE) defer
1.1750 apply(erule_tac x="basis 0" in ballE)
1.1751 unfolding Ball_def mem_cball dist_norm using DIM_positive[where 'a='a]
1.1752 by auto
1.1753 @@ -3726,13 +3726,13 @@
1.1754 } note surf_0 = this
1.1755 show "inj_on (\<lambda>x. norm x *\<^sub>R surf (pi x)) (cball 0 1)" unfolding inj_on_def proof(rule,rule,rule)
1.1756 fix x y assume as:"x \<in> cball 0 1" "y \<in> cball 0 1" "norm x *\<^sub>R surf (pi x) = norm y *\<^sub>R surf (pi y)"
1.1757 - thus "x=y" proof(cases "x=0 \<or> y=0")
1.1758 + thus "x=y" proof(cases "x=0 \<or> y=0")
1.1759 case True thus ?thesis using as by(auto elim: surf_0) next
1.1760 case False
1.1761 hence "pi (surf (pi x)) = pi (surf (pi y))" using as(3)
1.1762 using pi(2)[of "norm x" "surf (pi x)"] pi(2)[of "norm y" "surf (pi y)"] by auto
1.1763 moreover have "pi x \<in> sphere" "pi y \<in> sphere" using pi(1) False by auto
1.1764 - ultimately have *:"pi x = pi y" using surf(4)[THEN bspec[where x="pi x"]] surf(4)[THEN bspec[where x="pi y"]] by auto
1.1765 + ultimately have *:"pi x = pi y" using surf(4)[THEN bspec[where x="pi x"]] surf(4)[THEN bspec[where x="pi y"]] by auto
1.1766 moreover have "norm x = norm y" using as(3)[unfolded *] using False by(auto dest:surf_0)
1.1767 ultimately show ?thesis using injpi by auto qed qed
1.1768 qed auto qed
1.1769 @@ -3790,7 +3790,7 @@
1.1770 lemma mem_epigraph: "(x, y) \<in> epigraph s f \<longleftrightarrow> x \<in> s \<and> f x \<le> y" unfolding epigraph_def by auto
1.1771
1.1772 (** This might break sooner or later. In fact it did already once. **)
1.1773 -lemma convex_epigraph:
1.1774 +lemma convex_epigraph:
1.1775 "convex(epigraph s f) \<longleftrightarrow> convex_on s f \<and> convex s"
1.1776 unfolding convex_def convex_on_def
1.1777 unfolding Ball_def split_paired_All epigraph_def
1.1778 @@ -3877,16 +3877,16 @@
1.1779 moreover have "a\<in>?halfl" "b\<in>?halfr" using * by (auto simp add: inner_vector_def)
1.1780 hence "?halfl \<inter> s \<noteq> {}" "?halfr \<inter> s \<noteq> {}" using as(2-3) by auto
1.1781 ultimately show False apply(rule_tac notE[OF as(1)[unfolded connected_def]])
1.1782 - apply(rule_tac x="?halfl" in exI, rule_tac x="?halfr" in exI)
1.1783 + apply(rule_tac x="?halfl" in exI, rule_tac x="?halfr" in exI)
1.1784 apply(rule, rule open_halfspace_lt, rule, rule open_halfspace_gt)
1.1785 by(auto simp add: field_simps) qed
1.1786
1.1787 lemma is_interval_convex_1:
1.1788 - "is_interval s \<longleftrightarrow> convex (s::(real^1) set)"
1.1789 + "is_interval s \<longleftrightarrow> convex (s::(real^1) set)"
1.1790 by(metis is_interval_convex convex_connected is_interval_connected_1)
1.1791
1.1792 lemma convex_connected_1:
1.1793 - "connected s \<longleftrightarrow> convex (s::(real^1) set)"
1.1794 + "connected s \<longleftrightarrow> convex (s::(real^1) set)"
1.1795 by(metis is_interval_convex convex_connected is_interval_connected_1)
1.1796 *)
1.1797 subsection {* Another intermediate value theorem formulation *}
1.1798 @@ -3894,7 +3894,7 @@
1.1799 lemma ivt_increasing_component_on_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
1.1800 assumes "a \<le> b" "continuous_on {a .. b} f" "(f a)$$k \<le> y" "y \<le> (f b)$$k"
1.1801 shows "\<exists>x\<in>{a..b}. (f x)$$k = y"
1.1802 -proof- have "f a \<in> f ` {a..b}" "f b \<in> f ` {a..b}" apply(rule_tac[!] imageI)
1.1803 +proof- have "f a \<in> f ` {a..b}" "f b \<in> f ` {a..b}" apply(rule_tac[!] imageI)
1.1804 using assms(1) by auto
1.1805 thus ?thesis using connected_ivt_component[of "f ` {a..b}" "f a" "f b" k y]
1.1806 using connected_continuous_image[OF assms(2) convex_connected[OF convex_real_interval(5)]]
1.1807 @@ -3937,7 +3937,7 @@
1.1808 "{0::'a::ordered_euclidean_space .. (\<chi>\<chi> i. 1)} = convex hull {x. \<forall>i<DIM('a). (x$$i = 0) \<or> (x$$i = 1)}"
1.1809 (is "?int = convex hull ?points")
1.1810 proof- have 01:"{0,(\<chi>\<chi> i. 1)} \<subseteq> convex hull ?points" apply rule apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) by auto
1.1811 - { fix n x assume "x\<in>{0::'a::ordered_euclidean_space .. \<chi>\<chi> i. 1}" "n \<le> DIM('a)" "card {i. i<DIM('a) \<and> x$$i \<noteq> 0} \<le> n"
1.1812 + { fix n x assume "x\<in>{0::'a::ordered_euclidean_space .. \<chi>\<chi> i. 1}" "n \<le> DIM('a)" "card {i. i<DIM('a) \<and> x$$i \<noteq> 0} \<le> n"
1.1813 hence "x\<in>convex hull ?points" proof(induct n arbitrary: x)
1.1814 case 0 hence "x = 0" apply(subst euclidean_eq) apply rule by auto
1.1815 thus "x\<in>convex hull ?points" using 01 by auto
1.1816 @@ -3958,7 +3958,7 @@
1.1817 case True have "\<forall>j\<in>{i. i<DIM('a) \<and> x$$i \<noteq> 0}. x$$j = 1" apply(rule, rule ccontr) unfolding mem_Collect_eq
1.1818 proof(erule conjE) fix j assume as:"x $$ j \<noteq> 0" "x $$ j \<noteq> 1" "j<DIM('a)"
1.1819 hence j:"x$$j \<in> {0<..<1}" using Suc(2) by(auto simp add: eucl_le[where 'a='a] elim!:allE[where x=j])
1.1820 - hence "x$$j \<in> op $$ x ` {i. i<DIM('a) \<and> x $$ i \<noteq> 0}" using as(3) by auto
1.1821 + hence "x$$j \<in> op $$ x ` {i. i<DIM('a) \<and> x $$ i \<noteq> 0}" using as(3) by auto
1.1822 hence "x$$j \<ge> x$$i" unfolding i'(1) xi_def apply(rule_tac Min_le) by auto
1.1823 thus False using True Suc(2) j by(auto simp add: elim!:ballE[where x=j]) qed
1.1824 thus "x\<in>convex hull ?points" apply(rule_tac hull_subset[unfolded subset_eq, rule_format])
1.1825 @@ -3975,7 +3975,7 @@
1.1826 moreover have "i\<in>{j. j<DIM('a) \<and> x$$j \<noteq> 0} - {j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0}"
1.1827 using i01 using i'(3) by auto
1.1828 hence "{j. j<DIM('a) \<and> x$$j \<noteq> 0} \<noteq> {j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0}" using i'(3) by blast
1.1829 - hence **:"{j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0} \<subset> {j. j<DIM('a) \<and> x$$j \<noteq> 0}" apply - apply rule
1.1830 + hence **:"{j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0} \<subset> {j. j<DIM('a) \<and> x$$j \<noteq> 0}" apply - apply rule
1.1831 by auto
1.1832 have "card {j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0} \<le> n"
1.1833 using less_le_trans[OF psubset_card_mono[OF _ **] Suc(4)] by auto
1.1834 @@ -3984,8 +3984,8 @@
1.1835 unfolding mem_interval using i01 Suc(3) by auto
1.1836 qed qed qed } note * = this
1.1837 have **:"DIM('a) = card {..<DIM('a)}" by auto
1.1838 - show ?thesis apply rule defer apply(rule hull_minimal) unfolding subset_eq prefer 3 apply rule
1.1839 - apply(rule_tac n2="DIM('a)" in *) prefer 3 apply(subst(2) **)
1.1840 + show ?thesis apply rule defer apply(rule hull_minimal) unfolding subset_eq prefer 3 apply rule
1.1841 + apply(rule_tac n2="DIM('a)" in *) prefer 3 apply(subst(2) **)
1.1842 apply(rule card_mono) using 01 and convex_interval(1) prefer 5 apply - apply rule
1.1843 unfolding mem_interval apply rule unfolding mem_Collect_eq apply(erule_tac x=i in allE)
1.1844 by auto qed
1.1845 @@ -4020,10 +4020,10 @@
1.1846 "inverse d * (y $$ i * 2) \<le> 2 + inverse d * (x $$ i * 2)" by(auto simp add:field_simps) }
1.1847 hence "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> {0..\<chi>\<chi> i.1}" unfolding mem_interval using assms
1.1848 by(auto simp add: field_simps)
1.1849 - thus "\<exists>z\<in>{0..\<chi>\<chi> i.1}. y = x - ?d + (2 * d) *\<^sub>R z" apply- apply(rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
1.1850 + thus "\<exists>z\<in>{0..\<chi>\<chi> i.1}. y = x - ?d + (2 * d) *\<^sub>R z" apply- apply(rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
1.1851 using assms by auto
1.1852 next
1.1853 - fix y z assume as:"z\<in>{0..\<chi>\<chi> i.1}" "y = x - ?d + (2*d) *\<^sub>R z"
1.1854 + fix y z assume as:"z\<in>{0..\<chi>\<chi> i.1}" "y = x - ?d + (2*d) *\<^sub>R z"
1.1855 have "\<And>i. i<DIM('a) \<Longrightarrow> 0 \<le> d * z $$ i \<and> d * z $$ i \<le> d"
1.1856 using assms as(1)[unfolded mem_interval] apply(erule_tac x=i in allE)
1.1857 apply rule apply(rule mult_nonneg_nonneg) prefer 3 apply(rule mult_right_le_one_le)
1.1858 @@ -4047,41 +4047,41 @@
1.1859 obtain k where "k>0"and k:"cball x k \<subseteq> s" using assms(1)[unfolded open_contains_cball, THEN bspec[where x=x]] using `x\<in>s` by auto
1.1860 show "\<exists>d>0. \<forall>x'. norm (x' - x) < d \<longrightarrow> \<bar>f x' - f x\<bar> < e"
1.1861 apply(rule_tac x="min (k / 2) (e / (2 * B) * k)" in exI) apply rule defer proof(rule,rule)
1.1862 - fix y assume as:"norm (y - x) < min (k / 2) (e / (2 * B) * k)"
1.1863 + fix y assume as:"norm (y - x) < min (k / 2) (e / (2 * B) * k)"
1.1864 show "\<bar>f y - f x\<bar> < e" proof(cases "y=x")
1.1865 case False def t \<equiv> "k / norm (y - x)"
1.1866 have "2 < t" "0<t" unfolding t_def using as False and `k>0` by(auto simp add:field_simps)
1.1867 have "y\<in>s" apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm
1.1868 - apply(rule order_trans[of _ "2 * norm (x - y)"]) using as by(auto simp add: field_simps norm_minus_commute)
1.1869 + apply(rule order_trans[of _ "2 * norm (x - y)"]) using as by(auto simp add: field_simps norm_minus_commute)
1.1870 { def w \<equiv> "x + t *\<^sub>R (y - x)"
1.1871 - have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm
1.1872 + have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm
1.1873 unfolding t_def using `k>0` by auto
1.1874 have "(1 / t) *\<^sub>R x + - x + ((t - 1) / t) *\<^sub>R x = (1 / t - 1 + (t - 1) / t) *\<^sub>R x" by (auto simp add: algebra_simps)
1.1875 also have "\<dots> = 0" using `t>0` by(auto simp add:field_simps)
1.1876 finally have w:"(1 / t) *\<^sub>R w + ((t - 1) / t) *\<^sub>R x = y" unfolding w_def using False and `t>0` by (auto simp add: algebra_simps)
1.1877 - have "2 * B < e * t" unfolding t_def using `0<e` `0<k` `B>0` and as and False by (auto simp add:field_simps)
1.1878 + have "2 * B < e * t" unfolding t_def using `0<e` `0<k` `B>0` and as and False by (auto simp add:field_simps)
1.1879 hence "(f w - f x) / t < e"
1.1880 - using B(2)[OF `w\<in>s`] and B(2)[OF `x\<in>s`] using `t>0` by(auto simp add:field_simps)
1.1881 + using B(2)[OF `w\<in>s`] and B(2)[OF `x\<in>s`] using `t>0` by(auto simp add:field_simps)
1.1882 hence th1:"f y - f x < e" apply- apply(rule le_less_trans) defer apply assumption
1.1883 using assms(2)[unfolded convex_on_def,rule_format,of w x "1/t" "(t - 1)/t", unfolded w]
1.1884 using `0<t` `2<t` and `x\<in>s` `w\<in>s` by(auto simp add:field_simps) }
1.1885 - moreover
1.1886 + moreover
1.1887 { def w \<equiv> "x - t *\<^sub>R (y - x)"
1.1888 - have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm
1.1889 + have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm
1.1890 unfolding t_def using `k>0` by auto
1.1891 have "(1 / (1 + t)) *\<^sub>R x + (t / (1 + t)) *\<^sub>R x = (1 / (1 + t) + t / (1 + t)) *\<^sub>R x" by (auto simp add: algebra_simps)
1.1892 also have "\<dots>=x" using `t>0` by (auto simp add:field_simps)
1.1893 finally have w:"(1 / (1+t)) *\<^sub>R w + (t / (1 + t)) *\<^sub>R y = x" unfolding w_def using False and `t>0` by (auto simp add: algebra_simps)
1.1894 - have "2 * B < e * t" unfolding t_def using `0<e` `0<k` `B>0` and as and False by (auto simp add:field_simps)
1.1895 - hence *:"(f w - f y) / t < e" using B(2)[OF `w\<in>s`] and B(2)[OF `y\<in>s`] using `t>0` by(auto simp add:field_simps)
1.1896 - have "f x \<le> 1 / (1 + t) * f w + (t / (1 + t)) * f y"
1.1897 + have "2 * B < e * t" unfolding t_def using `0<e` `0<k` `B>0` and as and False by (auto simp add:field_simps)
1.1898 + hence *:"(f w - f y) / t < e" using B(2)[OF `w\<in>s`] and B(2)[OF `y\<in>s`] using `t>0` by(auto simp add:field_simps)
1.1899 + have "f x \<le> 1 / (1 + t) * f w + (t / (1 + t)) * f y"
1.1900 using assms(2)[unfolded convex_on_def,rule_format,of w y "1/(1+t)" "t / (1+t)",unfolded w]
1.1901 using `0<t` `2<t` and `y\<in>s` `w\<in>s` by (auto simp add:field_simps)
1.1902 also have "\<dots> = (f w + t * f y) / (1 + t)" using `t>0` unfolding divide_inverse by (auto simp add:field_simps)
1.1903 also have "\<dots> < e + f y" using `t>0` * `e>0` by(auto simp add:field_simps)
1.1904 finally have "f x - f y < e" by auto }
1.1905 - ultimately show ?thesis by auto
1.1906 - qed(insert `0<e`, auto)
1.1907 + ultimately show ?thesis by auto
1.1908 + qed(insert `0<e`, auto)
1.1909 qed(insert `0<e` `0<k` `0<B`, auto simp add:field_simps intro!:mult_pos_pos) qed
1.1910
1.1911 subsection {* Upper bound on a ball implies upper and lower bounds *}
1.1912 @@ -4097,14 +4097,14 @@
1.1913 have "(1 / 2) *\<^sub>R y + (1 / 2) *\<^sub>R z = x" unfolding z_def by (auto simp add: algebra_simps)
1.1914 thus "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>" using assms(1)[unfolded convex_on_def,rule_format, OF y z, of "1/2" "1/2"]
1.1915 using assms(2)[rule_format,OF y] assms(2)[rule_format,OF z] by(auto simp add:field_simps)
1.1916 -next case False fix y assume "y\<in>cball x e"
1.1917 +next case False fix y assume "y\<in>cball x e"
1.1918 hence "dist x y < 0" using False unfolding mem_cball not_le by (auto simp del: dist_not_less_zero)
1.1919 thus "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>" using zero_le_dist[of x y] by auto qed
1.1920
1.1921 subsubsection {* Hence a convex function on an open set is continuous *}
1.1922
1.1923 lemma convex_on_continuous:
1.1924 - assumes "open (s::('a::ordered_euclidean_space) set)" "convex_on s f"
1.1925 + assumes "open (s::('a::ordered_euclidean_space) set)" "convex_on s f"
1.1926 (* FIXME: generalize to euclidean_space *)
1.1927 shows "continuous_on s f"
1.1928 unfolding continuous_on_eq_continuous_at[OF assms(1)] proof
1.1929 @@ -4112,14 +4112,14 @@
1.1930 fix x assume "x\<in>s"
1.1931 then obtain e where e:"cball x e \<subseteq> s" "e>0" using assms(1) unfolding open_contains_cball by auto
1.1932 def d \<equiv> "e / real DIM('a)"
1.1933 - have "0 < d" unfolding d_def using `e>0` dimge1 by(rule_tac divide_pos_pos, auto)
1.1934 + have "0 < d" unfolding d_def using `e>0` dimge1 by(rule_tac divide_pos_pos, auto)
1.1935 let ?d = "(\<chi>\<chi> i. d)::'a"
1.1936 obtain c where c:"finite c" "{x - ?d..x + ?d} = convex hull c" using cube_convex_hull[OF `d>0`, of x] by auto
1.1937 have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by auto
1.1938 hence "c\<noteq>{}" using c by auto
1.1939 def k \<equiv> "Max (f ` c)"
1.1940 have "convex_on {x - ?d..x + ?d} f" apply(rule convex_on_subset[OF assms(2)])
1.1941 - apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof
1.1942 + apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof
1.1943 fix z assume z:"z\<in>{x - ?d..x + ?d}"
1.1944 have e:"e = setsum (\<lambda>i. d) {..<DIM('a)}" unfolding setsum_constant d_def using dimge1
1.1945 unfolding real_eq_of_nat by auto
1.1946 @@ -4132,21 +4132,21 @@
1.1947 have conv:"convex_on (cball x d) f" apply(rule convex_on_subset, rule convex_on_subset[OF assms(2)]) apply(rule e(1)) using dsube by auto
1.1948 hence "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)" apply(rule_tac convex_bounds_lemma) apply assumption proof
1.1949 fix y assume y:"y\<in>cball x d"
1.1950 - { fix i assume "i<DIM('a)" hence "x $$ i - d \<le> y $$ i" "y $$ i \<le> x $$ i + d"
1.1951 + { fix i assume "i<DIM('a)" hence "x $$ i - d \<le> y $$ i" "y $$ i \<le> x $$ i + d"
1.1952 using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by auto }
1.1953 - thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm
1.1954 + thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm
1.1955 by auto qed
1.1956 hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous)
1.1957 apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball)
1.1958 apply force
1.1959 done
1.1960 thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball]
1.1961 - using `d>0` by auto
1.1962 + using `d>0` by auto
1.1963 qed
1.1964
1.1965 subsection {* Line segments, Starlike Sets, etc. *}
1.1966
1.1967 -(* Use the same overloading tricks as for intervals, so that
1.1968 +(* Use the same overloading tricks as for intervals, so that
1.1969 segment[a,b] is closed and segment(a,b) is open relative to affine hull. *)
1.1970
1.1971 definition
1.1972 @@ -4218,7 +4218,7 @@
1.1973 have *:"\<And>x. {x} \<noteq> {}" by auto
1.1974 have **:"\<And>u v. u + v = 1 \<longleftrightarrow> u = 1 - (v::real)" by auto
1.1975 show ?thesis unfolding segment convex_hull_insert[OF *] convex_hull_singleton apply(rule set_eqI)
1.1976 - unfolding mem_Collect_eq apply(rule,erule exE)
1.1977 + unfolding mem_Collect_eq apply(rule,erule exE)
1.1978 apply(rule_tac x="1 - u" in exI) apply rule defer apply(rule_tac x=u in exI) defer
1.1979 apply(erule exE, (erule conjE)?)+ apply(rule_tac x="1 - u" in exI) unfolding ** by auto qed
1.1980
1.1981 @@ -4241,7 +4241,7 @@
1.1982 shows "norm(x - a) \<le> norm(b - a)" "norm(x - b) \<le> norm(b - a)"
1.1983 using segment_furthest_le[OF assms, of a]
1.1984 using segment_furthest_le[OF assms, of b]
1.1985 - by (auto simp add:norm_minus_commute)
1.1986 + by (auto simp add:norm_minus_commute)
1.1987
1.1988 lemma segment_refl:"closed_segment a a = {a}" unfolding segment by (auto simp add: algebra_simps)
1.1989
1.1990 @@ -4252,11 +4252,11 @@
1.1991 proof(cases "a = b")
1.1992 case True thus ?thesis unfolding between_def split_conv
1.1993 by(auto simp add:segment_refl dist_commute) next
1.1994 - case False hence Fal:"norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0" by auto
1.1995 + case False hence Fal:"norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0" by auto
1.1996 have *:"\<And>u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)" by (auto simp add: algebra_simps)
1.1997 show ?thesis unfolding between_def split_conv closed_segment_def mem_Collect_eq
1.1998 apply rule apply(erule exE, (erule conjE)+) apply(subst dist_triangle_eq) proof-
1.1999 - fix u assume as:"x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1"
1.2000 + fix u assume as:"x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1"
1.2001 hence *:"a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)"
1.2002 unfolding as(1) by(auto simp add:algebra_simps)
1.2003 show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)"
1.2004 @@ -4264,7 +4264,7 @@
1.2005 by(auto simp add: field_simps)
1.2006 next assume as:"dist a b = dist a x + dist x b"
1.2007 have "norm (a - x) / norm (a - b) \<le> 1" unfolding divide_le_eq_1_pos[OF Fal2]
1.2008 - unfolding as[unfolded dist_norm] norm_ge_zero by auto
1.2009 + unfolding as[unfolded dist_norm] norm_ge_zero by auto
1.2010 thus "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" apply(rule_tac x="dist a x / dist a b" in exI)
1.2011 unfolding dist_norm apply(subst euclidean_eq) apply rule defer apply(rule, rule divide_nonneg_pos) prefer 4
1.2012 proof(rule,rule) fix i assume i:"i<DIM('a)"
1.2013 @@ -4274,12 +4274,12 @@
1.2014 also have "\<dots> = x$$i" apply(rule divide_eq_imp[OF Fal])
1.2015 unfolding as[unfolded dist_norm] using as[unfolded dist_triangle_eq] apply-
1.2016 apply(subst (asm) euclidean_eq) using i apply(erule_tac x=i in allE) by(auto simp add:field_simps)
1.2017 - finally show "x $$ i = ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $$ i"
1.2018 + finally show "x $$ i = ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $$ i"
1.2019 by auto
1.2020 qed(insert Fal2, auto) qed qed
1.2021
1.2022 lemma between_midpoint: fixes a::"'a::euclidean_space" shows
1.2023 - "between (a,b) (midpoint a b)" (is ?t1)
1.2024 + "between (a,b) (midpoint a b)" (is ?t1)
1.2025 "between (b,a) (midpoint a b)" (is ?t2)
1.2026 proof- have *:"\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y" by auto
1.2027 show ?t1 ?t2 unfolding between midpoint_def dist_norm apply(rule_tac[!] *)
1.2028 @@ -4303,7 +4303,7 @@
1.2029 have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
1.2030 have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
1.2031 unfolding dist_norm unfolding norm_scaleR[symmetric] apply(rule arg_cong[where f=norm]) using `e>0`
1.2032 - by(auto simp add: euclidean_eq[where 'a='a] field_simps)
1.2033 + by(auto simp add: euclidean_eq[where 'a='a] field_simps)
1.2034 also have "\<dots> = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
1.2035 also have "\<dots> < d" using as[unfolded dist_norm] and `e>0`
1.2036 by(auto simp add:pos_divide_less_eq[OF `e>0`] mult_commute)
1.2037 @@ -4334,7 +4334,7 @@
1.2038 have "z\<in>interior s" apply(rule interior_mono[OF d,unfolded subset_eq,rule_format])
1.2039 unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
1.2040 by(auto simp add:field_simps norm_minus_commute)
1.2041 - thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink)
1.2042 + thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink)
1.2043 using assms(1,4-5) `y\<in>s` by auto qed
1.2044
1.2045 subsection {* Some obvious but surprisingly hard simplex lemmas *}
1.2046 @@ -4350,31 +4350,31 @@
1.2047 lemma substd_simplex: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
1.2048 shows "convex hull (insert 0 { basis i | i. i : d}) =
1.2049 {x::'a::euclidean_space . (!i<DIM('a). 0 <= x$$i) & setsum (%i. x$$i) d <= 1 &
1.2050 - (!i<DIM('a). i ~: d --> x$$i = 0)}"
1.2051 + (!i<DIM('a). i ~: d --> x$$i = 0)}"
1.2052 (is "convex hull (insert 0 ?p) = ?s")
1.2053 (* Proof is a modified copy of the proof of similar lemma std_simplex in Convex_Euclidean_Space.thy *)
1.2054 proof- let ?D = d (*"{..<DIM('a::euclidean_space)}"*)
1.2055 have "0 ~: ?p" using assms by (auto simp: image_def)
1.2056 have "{(basis i)::'n::euclidean_space |i. i \<in> ?D} = basis ` ?D" by auto
1.2057 note sumbas = this setsum_reindex[OF basis_inj_on[of d], unfolded o_def, OF assms]
1.2058 - show ?thesis unfolding simplex[OF finite_substdbasis `0 ~: ?p`]
1.2059 + show ?thesis unfolding simplex[OF finite_substdbasis `0 ~: ?p`]
1.2060 apply(rule set_eqI) unfolding mem_Collect_eq apply rule
1.2061 apply(erule exE, (erule conjE)+) apply(erule_tac[2] conjE)+ proof-
1.2062 fix x::"'a::euclidean_space" and u assume as: "\<forall>x\<in>{basis i |i. i \<in>?D}. 0 \<le> u x"
1.2063 "setsum u {basis i |i. i \<in> ?D} \<le> 1" "(\<Sum>x\<in>{basis i |i. i \<in>?D}. u x *\<^sub>R x) = x"
1.2064 - have *:"\<forall>i<DIM('a). i:d --> u (basis i) = x$$i" and "(!i<DIM('a). i ~: d --> x $$ i = 0)" using as(3)
1.2065 + have *:"\<forall>i<DIM('a). i:d --> u (basis i) = x$$i" and "(!i<DIM('a). i ~: d --> x $$ i = 0)" using as(3)
1.2066 unfolding sumbas unfolding substdbasis_expansion_unique[OF assms] by auto
1.2067 - hence **:"setsum u {basis i |i. i \<in> ?D} = setsum (op $$ x) ?D" unfolding sumbas
1.2068 + hence **:"setsum u {basis i |i. i \<in> ?D} = setsum (op $$ x) ?D" unfolding sumbas
1.2069 apply-apply(rule setsum_cong2) using assms by auto
1.2070 - have " (\<forall>i<DIM('a). 0 \<le> x$$i) \<and> setsum (op $$ x) ?D \<le> 1"
1.2071 + have " (\<forall>i<DIM('a). 0 \<le> x$$i) \<and> setsum (op $$ x) ?D \<le> 1"
1.2072 apply - proof(rule,rule,rule)
1.2073 - fix i assume i:"i<DIM('a)" have "i : d ==> 0 \<le> x$$i" unfolding *[rule_format,OF i,symmetric]
1.2074 + fix i assume i:"i<DIM('a)" have "i : d ==> 0 \<le> x$$i" unfolding *[rule_format,OF i,symmetric]
1.2075 apply(rule_tac as(1)[rule_format]) by auto
1.2076 - moreover have "i ~: d ==> 0 \<le> x$$i"
1.2077 + moreover have "i ~: d ==> 0 \<le> x$$i"
1.2078 using `(!i<DIM('a). i ~: d --> x $$ i = 0)`[rule_format, OF i] by auto
1.2079 ultimately show "0 \<le> x$$i" by auto
1.2080 qed(insert as(2)[unfolded **], auto)
1.2081 - from this show " (\<forall>i<DIM('a). 0 \<le> x$$i) \<and> setsum (op $$ x) ?D \<le> 1 & (!i<DIM('a). i ~: d --> x $$ i = 0)"
1.2082 + from this show " (\<forall>i<DIM('a). 0 \<le> x$$i) \<and> setsum (op $$ x) ?D \<le> 1 & (!i<DIM('a). i ~: d --> x $$ i = 0)"
1.2083 using `(!i<DIM('a). i ~: d --> x $$ i = 0)` by auto
1.2084 next fix x::"'a::euclidean_space" assume as:"\<forall>i<DIM('a). 0 \<le> x $$ i" "setsum (op $$ x) ?D \<le> 1"
1.2085 "(!i<DIM('a). i ~: d --> x $$ i = 0)"
1.2086 @@ -4424,9 +4424,9 @@
1.2087 using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add: norm_minus_commute)
1.2088 thus "y $$ i \<le> x $$ i + ?d" by auto qed
1.2089 also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant real_eq_of_nat by(auto simp add: Suc_le_eq)
1.2090 - finally show "(\<forall>i<DIM('a). 0 \<le> y $$ i) \<and> setsum (op $$ y) {..<DIM('a)} \<le> 1"
1.2091 + finally show "(\<forall>i<DIM('a). 0 \<le> y $$ i) \<and> setsum (op $$ y) {..<DIM('a)} \<le> 1"
1.2092 proof safe fix i assume i:"i<DIM('a)"
1.2093 - have "norm (x - y) < x$$i" apply(rule less_le_trans)
1.2094 + have "norm (x - y) < x$$i" apply(rule less_le_trans)
1.2095 apply(rule y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]) using i by auto
1.2096 thus "0 \<le> y$$i" using component_le_norm[of "x - y" i] and as(1)[rule_format, of i] by auto
1.2097 qed qed auto qed
1.2098 @@ -4456,21 +4456,21 @@
1.2099 { assume "d={}" hence ?thesis using rel_interior_sing using euclidean_eq[of _ 0] by auto }
1.2100 moreover
1.2101 { assume "d~={}"
1.2102 -have h0: "affine hull (convex hull (insert 0 ?p))={x::'a::euclidean_space. (!i<DIM('a). i ~: d --> x$$i = 0)}"
1.2103 - using affine_hull_convex_hull affine_hull_substd_basis assms by auto
1.2104 +have h0: "affine hull (convex hull (insert 0 ?p))={x::'a::euclidean_space. (!i<DIM('a). i ~: d --> x$$i = 0)}"
1.2105 + using affine_hull_convex_hull affine_hull_substd_basis assms by auto
1.2106 have aux: "!x::'n::euclidean_space. !i. ((! i:d. 0 <= x$$i) & (!i. i ~: d --> x$$i = 0))--> 0 <= x$$i" by auto
1.2107 { fix x::"'a::euclidean_space" assume x_def: "x : rel_interior (convex hull (insert 0 ?p))"
1.2108 - from this obtain e where e0: "e>0" and
1.2109 - "ball x e Int {xa. (!i<DIM('a). i ~: d --> xa$$i = 0)} <= convex hull (insert 0 ?p)"
1.2110 - using mem_rel_interior_ball[of x "convex hull (insert 0 ?p)"] h0 by auto
1.2111 + from this obtain e where e0: "e>0" and
1.2112 + "ball x e Int {xa. (!i<DIM('a). i ~: d --> xa$$i = 0)} <= convex hull (insert 0 ?p)"
1.2113 + using mem_rel_interior_ball[of x "convex hull (insert 0 ?p)"] h0 by auto
1.2114 hence as: "ALL xa. (dist x xa < e & (!i<DIM('a). i ~: d --> xa$$i = 0)) -->
1.2115 (!i : d. 0 <= xa $$ i) & setsum (op $$ xa) d <= 1"
1.2116 unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto
1.2117 - have x0: "(!i<DIM('a). i ~: d --> x$$i = 0)"
1.2118 + have x0: "(!i<DIM('a). i ~: d --> x$$i = 0)"
1.2119 using x_def rel_interior_subset substd_simplex[OF assms] by auto
1.2120 - have "(!i : d. 0 < x $$ i) & setsum (op $$ x) d < 1 & (!i<DIM('a). i ~: d --> x$$i = 0)" apply(rule,rule)
1.2121 + have "(!i : d. 0 < x $$ i) & setsum (op $$ x) d < 1 & (!i<DIM('a). i ~: d --> x$$i = 0)" apply(rule,rule)
1.2122 proof-
1.2123 - fix i::nat assume "i:d"
1.2124 + fix i::nat assume "i:d"
1.2125 hence "\<forall>ia\<in>d. 0 \<le> (x - (e / 2) *\<^sub>R basis i) $$ ia" apply-apply(rule as[rule_format,THEN conjunct1])
1.2126 unfolding dist_norm using assms `e>0` x0 by auto
1.2127 thus "0 < x $$ i" apply(erule_tac x=i in ballE) using `e>0` `i\<in>d` assms by auto
1.2128 @@ -4488,7 +4488,7 @@
1.2129 have "setsum (op $$ x) d < setsum (op $$ (x + (e / 2) *\<^sub>R basis a)) d" unfolding * setsum_addf
1.2130 using `0<e` `a:d` using `finite d` by(auto simp add: setsum_delta')
1.2131 also have "\<dots> \<le> 1" using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R basis a"] by auto
1.2132 - finally show "setsum (op $$ x) d < 1 & (!i<DIM('a). i ~: d --> x$$i = 0)" using x0 by auto
1.2133 + finally show "setsum (op $$ x) d < 1 & (!i<DIM('a). i ~: d --> x$$i = 0)" using x0 by auto
1.2134 qed
1.2135 }
1.2136 moreover
1.2137 @@ -4496,10 +4496,10 @@
1.2138 fix x::"'a::euclidean_space" assume as: "x : ?s"
1.2139 have "!i. ((0<x$$i) | (0=x$$i) --> 0<=x$$i)" by auto
1.2140 moreover have "!i. (i:d) | (i ~: d)" by auto
1.2141 - ultimately
1.2142 + ultimately
1.2143 have "!i. ( (ALL i:d. 0 < x$$i) & (ALL i. i ~: d --> x$$i = 0) ) --> 0 <= x$$i" by metis
1.2144 - hence h2: "x : convex hull (insert 0 ?p)" using as assms
1.2145 - unfolding substd_simplex[OF assms] by fastforce
1.2146 + hence h2: "x : convex hull (insert 0 ?p)" using as assms
1.2147 + unfolding substd_simplex[OF assms] by fastforce
1.2148 obtain a where a:"a:d" using `d ~= {}` by auto
1.2149 let ?d = "(1 - setsum (op $$ x) d) / real (card d)"
1.2150 have "0 < card d" using `d ~={}` `finite d` by (simp add: card_gt_0_iff)
1.2151 @@ -4521,8 +4521,8 @@
1.2152 also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant real_eq_of_nat
1.2153 using `0 < card d` by auto
1.2154 finally show "setsum (op $$ y) d \<le> 1" .
1.2155 -
1.2156 - fix i assume "i<DIM('a)" thus "0 \<le> y$$i"
1.2157 +
1.2158 + fix i assume "i<DIM('a)" thus "0 \<le> y$$i"
1.2159 proof(cases "i\<in>d") case True
1.2160 have "norm (x - y) < x$$i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
1.2161 using Min_gr_iff[of "op $$ x ` d" "norm (x - y)"] `0 < card d` `i:d`
1.2162 @@ -4548,29 +4548,29 @@
1.2163 hence d1: "0 < real(card d)" using `d ~={}` by auto
1.2164 { fix i assume "i:d" have "?a $$ i = inverse (2 * real (card d))"
1.2165 unfolding * setsum_reindex[OF basis_inj_on, OF assms(2)] o_def
1.2166 - apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real (card d)) else 0) ?D"])
1.2167 + apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real (card d)) else 0) ?D"])
1.2168 unfolding euclidean_component_setsum
1.2169 apply(rule setsum_cong2)
1.2170 using `i:d` `finite d` setsum_delta'[of d i "(%k. inverse (2 * real (card d)))"] d1 assms(2)
1.2171 by (auto simp add: Euclidean_Space.basis_component[of i])}
1.2172 note ** = this
1.2173 show ?thesis apply(rule that[of ?a]) unfolding rel_interior_substd_simplex[OF assms(2)] mem_Collect_eq
1.2174 - proof safe fix i assume "i:d"
1.2175 + proof safe fix i assume "i:d"
1.2176 have "0 < inverse (2 * real (card d))" using d1 by auto
1.2177 also have "...=?a $$ i" using **[of i] `i:d` by auto
1.2178 finally show "0 < ?a $$ i" by auto
1.2179 - next have "setsum (op $$ ?a) ?D = setsum (\<lambda>i. inverse (2 * real (card d))) ?D"
1.2180 - by(rule setsum_cong2, rule **)
1.2181 + next have "setsum (op $$ ?a) ?D = setsum (\<lambda>i. inverse (2 * real (card d))) ?D"
1.2182 + by(rule setsum_cong2, rule **)
1.2183 also have "\<dots> < 1" unfolding setsum_constant real_eq_of_nat divide_real_def[symmetric]
1.2184 by (auto simp add:field_simps)
1.2185 finally show "setsum (op $$ ?a) ?D < 1" by auto
1.2186 next fix i assume "i<DIM('a)" and "i~:d"
1.2187 - have "?a : (span {basis i | i. i : d})"
1.2188 - apply (rule span_setsum[of "{basis i |i. i : d}" "(%b. b /\<^sub>R (2 * real (card d)))" "{basis i |i. i : d}"])
1.2189 - using finite_substdbasis[of d] apply blast
1.2190 + have "?a : (span {basis i | i. i : d})"
1.2191 + apply (rule span_setsum[of "{basis i |i. i : d}" "(%b. b /\<^sub>R (2 * real (card d)))" "{basis i |i. i : d}"])
1.2192 + using finite_substdbasis[of d] apply blast
1.2193 proof-
1.2194 { fix x assume "(x :: 'a::euclidean_space): {basis i |i. i : d}"
1.2195 - hence "x : span {basis i |i. i : d}"
1.2196 + hence "x : span {basis i |i. i : d}"
1.2197 using span_superset[of _ "{basis i |i. i : d}"] by auto
1.2198 hence "(x /\<^sub>R (2 * real (card d))) : (span {basis i |i. i : d})"
1.2199 using span_mul[of x "{basis i |i. i : d}" "(inverse (real (card d)) / 2)"] by auto
1.2200 @@ -4582,47 +4582,47 @@
1.2201
1.2202 subsection {* Relative interior of convex set *}
1.2203
1.2204 -lemma rel_interior_convex_nonempty_aux:
1.2205 -fixes S :: "('n::euclidean_space) set"
1.2206 +lemma rel_interior_convex_nonempty_aux:
1.2207 +fixes S :: "('n::euclidean_space) set"
1.2208 assumes "convex S" and "0 : S"
1.2209 shows "rel_interior S ~= {}"
1.2210 proof-
1.2211 { assume "S = {0}" hence ?thesis using rel_interior_sing by auto }
1.2212 -moreover {
1.2213 +moreover {
1.2214 assume "S ~= {0}"
1.2215 obtain B where B_def: "independent B & B<=S & (S <= span B) & card B = dim S" using basis_exists[of S] by auto
1.2216 hence "B~={}" using B_def assms `S ~= {0}` span_empty by auto
1.2217 have "insert 0 B <= span B" using subspace_span[of B] subspace_0[of "span B"] span_inc by auto
1.2218 -hence "span (insert 0 B) <= span B"
1.2219 +hence "span (insert 0 B) <= span B"
1.2220 using span_span[of B] span_mono[of "insert 0 B" "span B"] by blast
1.2221 -hence "convex hull insert 0 B <= span B"
1.2222 +hence "convex hull insert 0 B <= span B"
1.2223 using convex_hull_subset_span[of "insert 0 B"] by auto
1.2224 hence "span (convex hull insert 0 B) <= span B"
1.2225 using span_span[of B] span_mono[of "convex hull insert 0 B" "span B"] by blast
1.2226 -hence *: "span (convex hull insert 0 B) = span B"
1.2227 +hence *: "span (convex hull insert 0 B) = span B"
1.2228 using span_mono[of B "convex hull insert 0 B"] hull_subset[of "insert 0 B"] by auto
1.2229 hence "span (convex hull insert 0 B) = span S"
1.2230 using B_def span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto
1.2231 moreover have "0 : affine hull (convex hull insert 0 B)"
1.2232 using hull_subset[of "convex hull insert 0 B"] hull_subset[of "insert 0 B"] by auto
1.2233 ultimately have **: "affine hull (convex hull insert 0 B) = affine hull S"
1.2234 - using affine_hull_span_0[of "convex hull insert 0 B"] affine_hull_span_0[of "S"]
1.2235 + using affine_hull_span_0[of "convex hull insert 0 B"] affine_hull_span_0[of "S"]
1.2236 assms hull_subset[of S] by auto
1.2237 -obtain d and f::"'n=>'n" where fd: "card d = card B & linear f & f ` B = {basis i |i. i : (d :: nat set)} &
1.2238 +obtain d and f::"'n=>'n" where fd: "card d = card B & linear f & f ` B = {basis i |i. i : (d :: nat set)} &
1.2239 f ` span B = {x. ALL i<DIM('n). i ~: d --> x $$ i = (0::real)} & inj_on f (span B)" and d:"d\<subseteq>{..<DIM('n)}"
1.2240 using basis_to_substdbasis_subspace_isomorphism[of B,OF _ ] B_def by auto
1.2241 hence "bounded_linear f" using linear_conv_bounded_linear by auto
1.2242 have "d ~={}" using fd B_def `B ~={}` by auto
1.2243 have "(insert 0 {basis i |i. i : d}) = f ` (insert 0 B)" using fd linear_0 by auto
1.2244 hence "(convex hull (insert 0 {basis i |i. i : d})) = f ` (convex hull (insert 0 B))"
1.2245 - using convex_hull_linear_image[of f "(insert 0 {basis i |i. i : d})"]
1.2246 + using convex_hull_linear_image[of f "(insert 0 {basis i |i. i : d})"]
1.2247 convex_hull_linear_image[of f "(insert 0 B)"] `bounded_linear f` by auto
1.2248 -moreover have "rel_interior (f ` (convex hull insert 0 B)) =
1.2249 +moreover have "rel_interior (f ` (convex hull insert 0 B)) =
1.2250 f ` rel_interior (convex hull insert 0 B)"
1.2251 apply (rule rel_interior_injective_on_span_linear_image[of f "(convex hull insert 0 B)"])
1.2252 using `bounded_linear f` fd * by auto
1.2253 ultimately have "rel_interior (convex hull insert 0 B) ~= {}"
1.2254 - using rel_interior_substd_simplex_nonempty[OF `d~={}` d] apply auto by blast
1.2255 + using rel_interior_substd_simplex_nonempty[OF `d~={}` d] apply auto by blast
1.2256 moreover have "convex hull (insert 0 B) <= S"
1.2257 using B_def assms hull_mono[of "insert 0 B" "S" "convex"] convex_hull_eq by auto
1.2258 ultimately have ?thesis using subset_rel_interior[of "convex hull insert 0 B" S] ** by auto
1.2259 @@ -4636,9 +4636,9 @@
1.2260 proof-
1.2261 { assume "S ~= {}" from this obtain a where "a : S" by auto
1.2262 hence "0 : op + (-a) ` S" using assms exI[of "(%x. x:S & -a+x=0)" a] by auto
1.2263 - hence "rel_interior (op + (-a) ` S) ~= {}"
1.2264 - using rel_interior_convex_nonempty_aux[of "op + (-a) ` S"]
1.2265 - convex_translation[of S "-a"] assms by auto
1.2266 + hence "rel_interior (op + (-a) ` S) ~= {}"
1.2267 + using rel_interior_convex_nonempty_aux[of "op + (-a) ` S"]
1.2268 + convex_translation[of S "-a"] assms by auto
1.2269 hence "rel_interior S ~= {}" using rel_interior_translation by auto
1.2270 } from this show ?thesis using rel_interior_empty by auto
1.2271 qed
1.2272 @@ -4653,7 +4653,7 @@
1.2273 hence "x:S" using rel_interior_subset by auto
1.2274 have "x - u *\<^sub>R (x-y) : rel_interior S"
1.2275 proof(cases "0=u")
1.2276 - case False hence "0<u" using assm by auto
1.2277 + case False hence "0<u" using assm by auto
1.2278 thus ?thesis
1.2279 using assm rel_interior_convex_shrink[of S y x u] assms `x:S` by auto
1.2280 next
1.2281 @@ -4663,36 +4663,36 @@
1.2282 } from this show ?thesis unfolding convex_alt by auto
1.2283 qed
1.2284
1.2285 -lemma convex_closure_rel_interior:
1.2286 -fixes S :: "('n::euclidean_space) set"
1.2287 +lemma convex_closure_rel_interior:
1.2288 +fixes S :: "('n::euclidean_space) set"
1.2289 assumes "convex S"
1.2290 shows "closure(rel_interior S) = closure S"
1.2291 proof-
1.2292 -have h1: "closure(rel_interior S) <= closure S"
1.2293 +have h1: "closure(rel_interior S) <= closure S"
1.2294 using closure_mono[of "rel_interior S" S] rel_interior_subset[of S] by auto
1.2295 -{ assume "S ~= {}" from this obtain a where a_def: "a : rel_interior S"
1.2296 +{ assume "S ~= {}" from this obtain a where a_def: "a : rel_interior S"
1.2297 using rel_interior_convex_nonempty assms by auto
1.2298 { fix x assume x_def: "x : closure S"
1.2299 { assume "x=a" hence "x : closure(rel_interior S)" using a_def unfolding closure_def by auto }
1.2300 moreover
1.2301 { assume "x ~= a"
1.2302 - { fix e :: real assume e_def: "e>0"
1.2303 + { fix e :: real assume e_def: "e>0"
1.2304 def e1 == "min 1 (e/norm (x - a))" hence e1_def: "e1>0 & e1<=1 & e1*norm(x-a)<=e"
1.2305 - using `x ~= a` `e>0` divide_pos_pos[of e] le_divide_eq[of e1 e "norm(x-a)"] by simp
1.2306 + using `x ~= a` `e>0` divide_pos_pos[of e] le_divide_eq[of e1 e "norm(x-a)"] by simp
1.2307 hence *: "x - e1 *\<^sub>R (x - a) : rel_interior S"
1.2308 using rel_interior_closure_convex_shrink[of S a x e1] assms x_def a_def e1_def by auto
1.2309 have "EX y. y:rel_interior S & y ~= x & (dist y x) <= e"
1.2310 apply (rule_tac x="x - e1 *\<^sub>R (x - a)" in exI)
1.2311 using * e1_def dist_norm[of "x - e1 *\<^sub>R (x - a)" x] `x ~= a` by simp
1.2312 - } hence "x islimpt rel_interior S" unfolding islimpt_approachable_le by auto
1.2313 - hence "x : closure(rel_interior S)" unfolding closure_def by auto
1.2314 + } hence "x islimpt rel_interior S" unfolding islimpt_approachable_le by auto
1.2315 + hence "x : closure(rel_interior S)" unfolding closure_def by auto
1.2316 } ultimately have "x : closure(rel_interior S)" by auto
1.2317 } hence ?thesis using h1 by auto
1.2318 }
1.2319 moreover
1.2320 { assume "S = {}" hence "rel_interior S = {}" using rel_interior_empty by auto
1.2321 - hence "closure(rel_interior S) = {}" using closure_empty by auto
1.2322 - hence ?thesis using `S={}` by auto
1.2323 + hence "closure(rel_interior S) = {}" using closure_empty by auto
1.2324 + hence ?thesis using `S={}` by auto
1.2325 } ultimately show ?thesis by blast
1.2326 qed
1.2327
1.2328 @@ -4702,7 +4702,7 @@
1.2329 shows "affine hull (rel_interior S) = affine hull S"
1.2330 by (metis assms closure_same_affine_hull convex_closure_rel_interior)
1.2331
1.2332 -lemma rel_interior_aff_dim:
1.2333 +lemma rel_interior_aff_dim:
1.2334 fixes S :: "('n::euclidean_space) set"
1.2335 assumes "convex S"
1.2336 shows "aff_dim (rel_interior S) = aff_dim S"
1.2337 @@ -4741,81 +4741,81 @@
1.2338 ultimately show ?thesis using that[of e] by auto
1.2339 qed
1.2340
1.2341 -lemma convex_rel_interior_closure:
1.2342 - fixes S :: "('n::euclidean_space) set"
1.2343 +lemma convex_rel_interior_closure:
1.2344 + fixes S :: "('n::euclidean_space) set"
1.2345 assumes "convex S"
1.2346 shows "rel_interior (closure S) = rel_interior S"
1.2347 proof-
1.2348 { assume "S={}" hence ?thesis using assms rel_interior_convex_nonempty by auto }
1.2349 moreover
1.2350 { assume "S ~= {}"
1.2351 - have "rel_interior (closure S) >= rel_interior S"
1.2352 + have "rel_interior (closure S) >= rel_interior S"
1.2353 using subset_rel_interior[of S "closure S"] closure_same_affine_hull closure_subset by auto
1.2354 moreover
1.2355 { fix z assume z_def: "z : rel_interior (closure S)"
1.2356 - obtain x where x_def: "x : rel_interior S"
1.2357 - using `S ~= {}` assms rel_interior_convex_nonempty by auto
1.2358 + obtain x where x_def: "x : rel_interior S"
1.2359 + using `S ~= {}` assms rel_interior_convex_nonempty by auto
1.2360 { assume "x=z" hence "z : rel_interior S" using x_def by auto }
1.2361 moreover
1.2362 { assume "x ~= z"
1.2363 - obtain e where e_def: "e > 0 & cball z e Int affine hull closure S <= closure S"
1.2364 + obtain e where e_def: "e > 0 & cball z e Int affine hull closure S <= closure S"
1.2365 using z_def rel_interior_cball[of "closure S"] by auto
1.2366 - hence *: "0 < e/norm(z-x)" using e_def `x ~= z` divide_pos_pos[of e "norm(z-x)"] by auto
1.2367 + hence *: "0 < e/norm(z-x)" using e_def `x ~= z` divide_pos_pos[of e "norm(z-x)"] by auto
1.2368 def y == "z + (e/norm(z-x)) *\<^sub>R (z-x)"
1.2369 have yball: "y : cball z e"
1.2370 - using mem_cball y_def dist_norm[of z y] e_def by auto
1.2371 - have "x : affine hull closure S"
1.2372 + using mem_cball y_def dist_norm[of z y] e_def by auto
1.2373 + have "x : affine hull closure S"
1.2374 using x_def rel_interior_subset_closure hull_inc[of x "closure S"] by auto
1.2375 - moreover have "z : affine hull closure S"
1.2376 + moreover have "z : affine hull closure S"
1.2377 using z_def rel_interior_subset hull_subset[of "closure S"] by auto
1.2378 - ultimately have "y : affine hull closure S"
1.2379 - using y_def affine_affine_hull[of "closure S"]
1.2380 + ultimately have "y : affine hull closure S"
1.2381 + using y_def affine_affine_hull[of "closure S"]
1.2382 mem_affine_3_minus [of "affine hull closure S" z z x "e/norm(z-x)"] by auto
1.2383 hence "y : closure S" using e_def yball by auto
1.2384 have "(1+(e/norm(z-x))) *\<^sub>R z = (e/norm(z-x)) *\<^sub>R x + y"
1.2385 - using y_def by (simp add: algebra_simps)
1.2386 + using y_def by (simp add: algebra_simps)
1.2387 from this obtain e1 where "0 < e1 & e1 <= 1 & z = y - e1 *\<^sub>R (y - x)"
1.2388 - using * convex_rel_interior_closure_aux[of "e / norm (z - x)" 1 z x y]
1.2389 + using * convex_rel_interior_closure_aux[of "e / norm (z - x)" 1 z x y]
1.2390 by (auto simp add: algebra_simps)
1.2391 - hence "z : rel_interior S"
1.2392 + hence "z : rel_interior S"
1.2393 using rel_interior_closure_convex_shrink assms x_def `y : closure S` by auto
1.2394 } ultimately have "z : rel_interior S" by auto
1.2395 } ultimately have ?thesis by auto
1.2396 } ultimately show ?thesis by blast
1.2397 qed
1.2398
1.2399 -lemma convex_interior_closure:
1.2400 -fixes S :: "('n::euclidean_space) set"
1.2401 +lemma convex_interior_closure:
1.2402 +fixes S :: "('n::euclidean_space) set"
1.2403 assumes "convex S"
1.2404 shows "interior (closure S) = interior S"
1.2405 -using closure_aff_dim[of S] interior_rel_interior_gen[of S] interior_rel_interior_gen[of "closure S"]
1.2406 +using closure_aff_dim[of S] interior_rel_interior_gen[of S] interior_rel_interior_gen[of "closure S"]
1.2407 convex_rel_interior_closure[of S] assms by auto
1.2408
1.2409 lemma closure_eq_rel_interior_eq:
1.2410 -fixes S1 S2 :: "('n::euclidean_space) set"
1.2411 +fixes S1 S2 :: "('n::euclidean_space) set"
1.2412 assumes "convex S1" "convex S2"
1.2413 shows "(closure S1 = closure S2) <-> (rel_interior S1 = rel_interior S2)"
1.2414 by (metis convex_rel_interior_closure convex_closure_rel_interior assms)
1.2415
1.2416
1.2417 lemma closure_eq_between:
1.2418 -fixes S1 S2 :: "('n::euclidean_space) set"
1.2419 +fixes S1 S2 :: "('n::euclidean_space) set"
1.2420 assumes "convex S1" "convex S2"
1.2421 -shows "(closure S1 = closure S2) <->
1.2422 +shows "(closure S1 = closure S2) <->
1.2423 ((rel_interior S1 <= S2) & (S2 <= closure S1))" (is "?A <-> ?B")
1.2424 proof-
1.2425 have "?A --> ?B" by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset)
1.2426 -moreover have "?B --> (closure S1 <= closure S2)"
1.2427 +moreover have "?B --> (closure S1 <= closure S2)"
1.2428 by (metis assms(1) convex_closure_rel_interior closure_mono)
1.2429 moreover have "?B --> (closure S1 >= closure S2)" by (metis closed_closure closure_minimal)
1.2430 ultimately show ?thesis by blast
1.2431 qed
1.2432
1.2433 lemma open_inter_closure_rel_interior:
1.2434 -fixes S A :: "('n::euclidean_space) set"
1.2435 +fixes S A :: "('n::euclidean_space) set"
1.2436 assumes "convex S" "open A"
1.2437 shows "((A Int closure S) = {}) <-> ((A Int rel_interior S) = {})"
1.2438 -by (metis assms convex_closure_rel_interior open_inter_closure_eq_empty)
1.2439 +by (metis assms convex_closure_rel_interior open_inter_closure_eq_empty)
1.2440
1.2441 definition "rel_frontier S = closure S - rel_interior S"
1.2442
1.2443 @@ -4824,29 +4824,29 @@
1.2444
1.2445 lemma closed_rel_frontier: "closed(rel_frontier (S :: ('n::euclidean_space) set))"
1.2446 proof-
1.2447 -have *: "closedin (subtopology euclidean (affine hull S)) (closure S - rel_interior S)"
1.2448 -apply (rule closedin_diff[of "subtopology euclidean (affine hull S)""closure S" "rel_interior S"]) using closed_closedin_trans[of "affine hull S" "closure S"] closed_affine_hull[of S]
1.2449 - closure_affine_hull[of S] opein_rel_interior[of S] by auto
1.2450 -show ?thesis apply (rule closedin_closed_trans[of "affine hull S" "rel_frontier S"])
1.2451 - unfolding rel_frontier_def using * closed_affine_hull by auto
1.2452 -qed
1.2453 -
1.2454 +have *: "closedin (subtopology euclidean (affine hull S)) (closure S - rel_interior S)"
1.2455 +apply (rule closedin_diff[of "subtopology euclidean (affine hull S)""closure S" "rel_interior S"]) using closed_closedin_trans[of "affine hull S" "closure S"] closed_affine_hull[of S]
1.2456 + closure_affine_hull[of S] opein_rel_interior[of S] by auto
1.2457 +show ?thesis apply (rule closedin_closed_trans[of "affine hull S" "rel_frontier S"])
1.2458 + unfolding rel_frontier_def using * closed_affine_hull by auto
1.2459 +qed
1.2460 +
1.2461
1.2462 lemma convex_rel_frontier_aff_dim:
1.2463 -fixes S1 S2 :: "('n::euclidean_space) set"
1.2464 +fixes S1 S2 :: "('n::euclidean_space) set"
1.2465 assumes "convex S1" "convex S2" "S2 ~= {}"
1.2466 assumes "S1 <= rel_frontier S2"
1.2467 -shows "aff_dim S1 < aff_dim S2"
1.2468 +shows "aff_dim S1 < aff_dim S2"
1.2469 proof-
1.2470 have "S1 <= closure S2" using assms unfolding rel_frontier_def by auto
1.2471 -hence *: "affine hull S1 <= affine hull S2"
1.2472 +hence *: "affine hull S1 <= affine hull S2"
1.2473 using hull_mono[of "S1" "closure S2"] closure_same_affine_hull[of S2] by auto
1.2474 -hence "aff_dim S1 <= aff_dim S2" using * aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2]
1.2475 +hence "aff_dim S1 <= aff_dim S2" using * aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2]
1.2476 aff_dim_subset[of "affine hull S1" "affine hull S2"] by auto
1.2477 moreover
1.2478 { assume eq: "aff_dim S1 = aff_dim S2"
1.2479 hence "S1 ~= {}" using aff_dim_empty[of S1] aff_dim_empty[of S2] `S2 ~= {}` by auto
1.2480 - have **: "affine hull S1 = affine hull S2"
1.2481 + have **: "affine hull S1 = affine hull S2"
1.2482 apply (rule affine_dim_equal) using * affine_affine_hull apply auto
1.2483 using `S1 ~= {}` hull_subset[of S1] apply auto
1.2484 using eq aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2] by auto
1.2485 @@ -4855,7 +4855,7 @@
1.2486 obtain T where T_def: "open T & a : T Int S1 & T Int affine hull S1 <= S1"
1.2487 using mem_rel_interior[of a S1] a_def by auto
1.2488 hence "a : T Int closure S2" using a_def assms unfolding rel_frontier_def by auto
1.2489 - from this obtain b where b_def: "b : T Int rel_interior S2"
1.2490 + from this obtain b where b_def: "b : T Int rel_interior S2"
1.2491 using open_inter_closure_rel_interior[of S2 T] assms T_def by auto
1.2492 hence "b : affine hull S1" using rel_interior_subset hull_subset[of S2] ** by auto
1.2493 hence "b : S1" using T_def b_def by auto
1.2494 @@ -4865,23 +4865,23 @@
1.2495
1.2496
1.2497 lemma convex_rel_interior_if:
1.2498 -fixes S :: "('n::euclidean_space) set"
1.2499 +fixes S :: "('n::euclidean_space) set"
1.2500 assumes "convex S"
1.2501 assumes "z : rel_interior S"
1.2502 shows "(!x:affine hull S. EX m. m>1 & (!e. (e>1 & e<=m) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S ))"
1.2503 proof-
1.2504 -obtain e1 where e1_def: "e1>0 & cball z e1 Int affine hull S <= S"
1.2505 +obtain e1 where e1_def: "e1>0 & cball z e1 Int affine hull S <= S"
1.2506 using mem_rel_interior_cball[of z S] assms by auto
1.2507 { fix x assume x_def: "x:affine hull S"
1.2508 { assume "x ~= z"
1.2509 - def m == "1+e1/norm(x-z)"
1.2510 - hence "m>1" using e1_def `x ~= z` divide_pos_pos[of e1 "norm (x - z)"] by auto
1.2511 + def m == "1+e1/norm(x-z)"
1.2512 + hence "m>1" using e1_def `x ~= z` divide_pos_pos[of e1 "norm (x - z)"] by auto
1.2513 { fix e assume e_def: "e>1 & e<=m"
1.2514 have "z : affine hull S" using assms rel_interior_subset hull_subset[of S] by auto
1.2515 hence *: "(1-e)*\<^sub>R x+ e *\<^sub>R z : affine hull S"
1.2516 using mem_affine[of "affine hull S" x z "(1-e)" e] affine_affine_hull[of S] x_def by auto
1.2517 have "norm (z + e *\<^sub>R x - (x + e *\<^sub>R z)) = norm ((e - 1) *\<^sub>R (x-z))" by (simp add: algebra_simps)
1.2518 - also have "...= (e - 1) * norm(x-z)" using norm_scaleR e_def by auto
1.2519 + also have "...= (e - 1) * norm(x-z)" using norm_scaleR e_def by auto
1.2520 also have "...<=(m - 1) * norm(x-z)" using e_def mult_right_mono[of _ _ "norm(x-z)"] by auto
1.2521 also have "...= (e1 / norm (x - z)) * norm (x - z)" using m_def by auto
1.2522 also have "...=e1" using `x ~= z` e1_def by simp
1.2523 @@ -4899,21 +4899,21 @@
1.2524 hence "(1-e)*\<^sub>R x+ e *\<^sub>R z : S" using e_def by auto
1.2525 } hence "EX m. m>1 & (!e. (e>1 & e<=m) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S )" using `m>1` by auto
1.2526 } ultimately have "EX m. m>1 & (!e. (e>1 & e<=m) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S )" by auto
1.2527 -} from this show ?thesis by auto
1.2528 +} from this show ?thesis by auto
1.2529 qed
1.2530
1.2531 lemma convex_rel_interior_if2:
1.2532 -fixes S :: "('n::euclidean_space) set"
1.2533 +fixes S :: "('n::euclidean_space) set"
1.2534 assumes "convex S"
1.2535 assumes "z : rel_interior S"
1.2536 shows "(!x:affine hull S. EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S)"
1.2537 using convex_rel_interior_if[of S z] assms by auto
1.2538
1.2539 lemma convex_rel_interior_only_if:
1.2540 -fixes S :: "('n::euclidean_space) set"
1.2541 +fixes S :: "('n::euclidean_space) set"
1.2542 assumes "convex S" "S ~= {}"
1.2543 assumes "(!x:S. EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S)"
1.2544 -shows "z : rel_interior S"
1.2545 +shows "z : rel_interior S"
1.2546 proof-
1.2547 obtain x where x_def: "x : rel_interior S" using rel_interior_convex_nonempty assms by auto
1.2548 hence "x:S" using rel_interior_subset by auto
1.2549 @@ -4921,27 +4921,27 @@
1.2550 def y == "(1 - e) *\<^sub>R x + e *\<^sub>R z" hence "y:S" using e_def by auto
1.2551 def e1 == "1/e" hence "0<e1 & e1<1" using e_def by auto
1.2552 hence "z=y-(1-e1)*\<^sub>R (y-x)" using e1_def y_def by (auto simp add: algebra_simps)
1.2553 -from this show ?thesis
1.2554 +from this show ?thesis
1.2555 using rel_interior_convex_shrink[of S x y "1-e1"] `0<e1 & e1<1` `y:S` x_def assms by auto
1.2556 qed
1.2557
1.2558 lemma convex_rel_interior_iff:
1.2559 -fixes S :: "('n::euclidean_space) set"
1.2560 +fixes S :: "('n::euclidean_space) set"
1.2561 assumes "convex S" "S ~= {}"
1.2562 shows "z : rel_interior S <-> (!x:S. EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S)"
1.2563 -using assms hull_subset[of S "affine"]
1.2564 +using assms hull_subset[of S "affine"]
1.2565 convex_rel_interior_if[of S z] convex_rel_interior_only_if[of S z] by auto
1.2566
1.2567 lemma convex_rel_interior_iff2:
1.2568 -fixes S :: "('n::euclidean_space) set"
1.2569 +fixes S :: "('n::euclidean_space) set"
1.2570 assumes "convex S" "S ~= {}"
1.2571 shows "z : rel_interior S <-> (!x:affine hull S. EX e. e>1 & (1-e)*\<^sub>R x+ e *\<^sub>R z : S)"
1.2572 -using assms hull_subset[of S]
1.2573 +using assms hull_subset[of S]
1.2574 convex_rel_interior_if2[of S z] convex_rel_interior_only_if[of S z] by auto
1.2575
1.2576
1.2577 lemma convex_interior_iff:
1.2578 -fixes S :: "('n::euclidean_space) set"
1.2579 +fixes S :: "('n::euclidean_space) set"
1.2580 assumes "convex S"
1.2581 shows "z : interior S <-> (!x. EX e. e>0 & z+ e *\<^sub>R x : S)"
1.2582 proof-
1.2583 @@ -4961,13 +4961,13 @@
1.2584 hence "z = (e2/(e1+e2)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2"
1.2585 using x1_def x2_def apply (auto simp add: algebra_simps)
1.2586 using scaleR_left_distrib[of "e1/(e1+e2)" "e2/(e1+e2)" z] by auto
1.2587 - hence z: "z : affine hull S"
1.2588 - using mem_affine[of "affine hull S" x1 x2 "e2/(e1+e2)" "e1/(e1+e2)"]
1.2589 + hence z: "z : affine hull S"
1.2590 + using mem_affine[of "affine hull S" x1 x2 "e2/(e1+e2)" "e1/(e1+e2)"]
1.2591 x1 x2 affine_affine_hull[of S] * by auto
1.2592 have "x1-x2 = (e1+e2) *\<^sub>R (x-z)"
1.2593 using x1_def x2_def by (auto simp add: algebra_simps)
1.2594 hence "x=z+(1/(e1+e2)) *\<^sub>R (x1-x2)" using e1_def e2_def by simp
1.2595 - hence "x : affine hull S" using mem_affine_3_minus[of "affine hull S" z x1 x2 "1/(e1+e2)"]
1.2596 + hence "x : affine hull S" using mem_affine_3_minus[of "affine hull S" z x1 x2 "1/(e1+e2)"]
1.2597 x1 x2 z affine_affine_hull[of S] by auto
1.2598 } hence "affine hull S = UNIV" by auto
1.2599 hence "aff_dim S = int DIM('n)" using aff_dim_affine_hull[of S] by (simp add: aff_dim_univ)
1.2600 @@ -5007,7 +5007,7 @@
1.2601 subsubsection {* Relative interior and closure under common operations *}
1.2602
1.2603 lemma rel_interior_inter_aux: "Inter {rel_interior S |S. S : I} <= Inter I"
1.2604 -proof-
1.2605 +proof-
1.2606 { fix y assume "y : Inter {rel_interior S |S. S : I}"
1.2607 hence y_def: "!S : I. y : rel_interior S" by auto
1.2608 { fix S assume "S : I" hence "y : S" using rel_interior_subset y_def by auto }
1.2609 @@ -5016,7 +5016,7 @@
1.2610 qed
1.2611
1.2612 lemma closure_inter: "closure (Inter I) <= Inter {closure S |S. S : I}"
1.2613 -proof-
1.2614 +proof-
1.2615 { fix y assume "y : Inter I" hence y_def: "!S : I. y : S" by auto
1.2616 { fix S assume "S : I" hence "y : closure S" using closure_subset y_def by auto }
1.2617 hence "y : Inter {closure S |S. S : I}" by auto
1.2618 @@ -5027,14 +5027,14 @@
1.2619 hull_minimal[of "Inter I" "Inter {closure S |S. S : I}" "closed"] by auto
1.2620 qed
1.2621
1.2622 -lemma convex_closure_rel_interior_inter:
1.2623 +lemma convex_closure_rel_interior_inter:
1.2624 assumes "!S : I. convex (S :: ('n::euclidean_space) set)"
1.2625 assumes "Inter {rel_interior S |S. S : I} ~= {}"
1.2626 shows "Inter {closure S |S. S : I} <= closure (Inter {rel_interior S |S. S : I})"
1.2627 proof-
1.2628 obtain x where x_def: "!S : I. x : rel_interior S" using assms by auto
1.2629 { fix y assume "y : Inter {closure S |S. S : I}" hence y_def: "!S : I. y : closure S" by auto
1.2630 - { assume "y = x"
1.2631 + { assume "y = x"
1.2632 hence "y : closure (Inter {rel_interior S |S. S : I})"
1.2633 using x_def closure_subset[of "Inter {rel_interior S |S. S : I}"] by auto
1.2634 }
1.2635 @@ -5042,62 +5042,62 @@
1.2636 { assume "y ~= x"
1.2637 { fix e :: real assume e_def: "0 < e"
1.2638 def e1 == "min 1 (e/norm (y - x))" hence e1_def: "e1>0 & e1<=1 & e1*norm(y-x)<=e"
1.2639 - using `y ~= x` `e>0` divide_pos_pos[of e] le_divide_eq[of e1 e "norm(y-x)"] by simp
1.2640 + using `y ~= x` `e>0` divide_pos_pos[of e] le_divide_eq[of e1 e "norm(y-x)"] by simp
1.2641 def z == "y - e1 *\<^sub>R (y - x)"
1.2642 - { fix S assume "S : I"
1.2643 - hence "z : rel_interior S" using rel_interior_closure_convex_shrink[of S x y e1]
1.2644 + { fix S assume "S : I"
1.2645 + hence "z : rel_interior S" using rel_interior_closure_convex_shrink[of S x y e1]
1.2646 assms x_def y_def e1_def z_def by auto
1.2647 } hence *: "z : Inter {rel_interior S |S. S : I}" by auto
1.2648 have "EX z. z:Inter {rel_interior S |S. S : I} & z ~= y & (dist z y) <= e"
1.2649 apply (rule_tac x="z" in exI) using `y ~= x` z_def * e1_def e_def dist_norm[of z y] by simp
1.2650 - } hence "y islimpt Inter {rel_interior S |S. S : I}" unfolding islimpt_approachable_le by blast
1.2651 + } hence "y islimpt Inter {rel_interior S |S. S : I}" unfolding islimpt_approachable_le by blast
1.2652 hence "y : closure (Inter {rel_interior S |S. S : I})" unfolding closure_def by auto
1.2653 } ultimately have "y : closure (Inter {rel_interior S |S. S : I})" by auto
1.2654 } from this show ?thesis by auto
1.2655 qed
1.2656
1.2657
1.2658 -lemma convex_closure_inter:
1.2659 +lemma convex_closure_inter:
1.2660 assumes "!S : I. convex (S :: ('n::euclidean_space) set)"
1.2661 assumes "Inter {rel_interior S |S. S : I} ~= {}"
1.2662 shows "closure (Inter I) = Inter {closure S |S. S : I}"
1.2663 proof-
1.2664 -have "Inter {closure S |S. S : I} <= closure (Inter {rel_interior S |S. S : I})"
1.2665 +have "Inter {closure S |S. S : I} <= closure (Inter {rel_interior S |S. S : I})"
1.2666 using convex_closure_rel_interior_inter assms by auto
1.2667 -moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)"
1.2668 - using rel_interior_inter_aux
1.2669 +moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)"
1.2670 + using rel_interior_inter_aux
1.2671 closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
1.2672 ultimately show ?thesis using closure_inter[of I] by auto
1.2673 qed
1.2674
1.2675 -lemma convex_inter_rel_interior_same_closure:
1.2676 +lemma convex_inter_rel_interior_same_closure:
1.2677 assumes "!S : I. convex (S :: ('n::euclidean_space) set)"
1.2678 assumes "Inter {rel_interior S |S. S : I} ~= {}"
1.2679 shows "closure (Inter {rel_interior S |S. S : I}) = closure (Inter I)"
1.2680 proof-
1.2681 -have "Inter {closure S |S. S : I} <= closure (Inter {rel_interior S |S. S : I})"
1.2682 +have "Inter {closure S |S. S : I} <= closure (Inter {rel_interior S |S. S : I})"
1.2683 using convex_closure_rel_interior_inter assms by auto
1.2684 -moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)"
1.2685 - using rel_interior_inter_aux
1.2686 +moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)"
1.2687 + using rel_interior_inter_aux
1.2688 closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
1.2689 ultimately show ?thesis using closure_inter[of I] by auto
1.2690 qed
1.2691
1.2692 -lemma convex_rel_interior_inter:
1.2693 +lemma convex_rel_interior_inter:
1.2694 assumes "!S : I. convex (S :: ('n::euclidean_space) set)"
1.2695 assumes "Inter {rel_interior S |S. S : I} ~= {}"
1.2696 shows "rel_interior (Inter I) <= Inter {rel_interior S |S. S : I}"
1.2697 proof-
1.2698 have "convex(Inter I)" using assms convex_Inter by auto
1.2699 moreover have "convex(Inter {rel_interior S |S. S : I})" apply (rule convex_Inter)
1.2700 - using assms convex_rel_interior by auto
1.2701 + using assms convex_rel_interior by auto
1.2702 ultimately have "rel_interior (Inter {rel_interior S |S. S : I}) = rel_interior (Inter I)"
1.2703 - using convex_inter_rel_interior_same_closure assms
1.2704 + using convex_inter_rel_interior_same_closure assms
1.2705 closure_eq_rel_interior_eq[of "Inter {rel_interior S |S. S : I}" "Inter I"] by blast
1.2706 from this show ?thesis using rel_interior_subset[of "Inter {rel_interior S |S. S : I}"] by auto
1.2707 qed
1.2708
1.2709 -lemma convex_rel_interior_finite_inter:
1.2710 +lemma convex_rel_interior_finite_inter:
1.2711 assumes "!S : I. convex (S :: ('n::euclidean_space) set)"
1.2712 assumes "Inter {rel_interior S |S. S : I} ~= {}"
1.2713 assumes "finite I"
1.2714 @@ -5110,13 +5110,13 @@
1.2715 { assume "I ~= {}"
1.2716 { fix z assume z_def: "z : Inter {rel_interior S |S. S : I}"
1.2717 { fix x assume x_def: "x : Inter I"
1.2718 - { fix S assume S_def: "S : I" hence "z : rel_interior S" "x : S" using z_def x_def by auto
1.2719 + { fix S assume S_def: "S : I" hence "z : rel_interior S" "x : S" using z_def x_def by auto
1.2720 (*from this obtain e where e_def: "e>1 & (1 - e) *\<^sub>R x + e *\<^sub>R z : S"*)
1.2721 hence "EX m. m>1 & (!e. (e>1 & e<=m) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S )"
1.2722 using convex_rel_interior_if[of S z] S_def assms hull_subset[of S] by auto
1.2723 - } from this obtain mS where mS_def: "!S : I. (mS(S) > (1 :: real) &
1.2724 + } from this obtain mS where mS_def: "!S : I. (mS(S) > (1 :: real) &
1.2725 (!e. (e>1 & e<=mS(S)) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S))" by metis
1.2726 - obtain e where e_def: "e=Min (mS ` I)" by auto
1.2727 + obtain e where e_def: "e=Min (mS ` I)" by auto
1.2728 have "e : (mS ` I)" using e_def assms `I ~= {}` by simp
1.2729 hence "e>(1 :: real)" using mS_def by auto
1.2730 moreover have "!S : I. e<=mS(S)" using e_def assms by auto
1.2731 @@ -5127,43 +5127,43 @@
1.2732 } ultimately show ?thesis by blast
1.2733 qed
1.2734
1.2735 -lemma convex_closure_inter_two:
1.2736 +lemma convex_closure_inter_two:
1.2737 fixes S T :: "('n::euclidean_space) set"
1.2738 assumes "convex S" "convex T"
1.2739 assumes "(rel_interior S) Int (rel_interior T) ~= {}"
1.2740 -shows "closure (S Int T) = (closure S) Int (closure T)"
1.2741 +shows "closure (S Int T) = (closure S) Int (closure T)"
1.2742 using convex_closure_inter[of "{S,T}"] assms by auto
1.2743
1.2744 -lemma convex_rel_interior_inter_two:
1.2745 +lemma convex_rel_interior_inter_two:
1.2746 fixes S T :: "('n::euclidean_space) set"
1.2747 assumes "convex S" "convex T"
1.2748 assumes "(rel_interior S) Int (rel_interior T) ~= {}"
1.2749 -shows "rel_interior (S Int T) = (rel_interior S) Int (rel_interior T)"
1.2750 +shows "rel_interior (S Int T) = (rel_interior S) Int (rel_interior T)"
1.2751 using convex_rel_interior_finite_inter[of "{S,T}"] assms by auto
1.2752
1.2753
1.2754 -lemma convex_affine_closure_inter:
1.2755 +lemma convex_affine_closure_inter:
1.2756 fixes S T :: "('n::euclidean_space) set"
1.2757 assumes "convex S" "affine T"
1.2758 assumes "(rel_interior S) Int T ~= {}"
1.2759 shows "closure (S Int T) = (closure S) Int T"
1.2760 -proof-
1.2761 +proof-
1.2762 have "affine hull T = T" using assms by auto
1.2763 hence "rel_interior T = T" using rel_interior_univ[of T] by metis
1.2764 moreover have "closure T = T" using assms affine_closed[of T] by auto
1.2765 -ultimately show ?thesis using convex_closure_inter_two[of S T] assms affine_imp_convex by auto
1.2766 -qed
1.2767 -
1.2768 -lemma convex_affine_rel_interior_inter:
1.2769 +ultimately show ?thesis using convex_closure_inter_two[of S T] assms affine_imp_convex by auto
1.2770 +qed
1.2771 +
1.2772 +lemma convex_affine_rel_interior_inter:
1.2773 fixes S T :: "('n::euclidean_space) set"
1.2774 assumes "convex S" "affine T"
1.2775 assumes "(rel_interior S) Int T ~= {}"
1.2776 shows "rel_interior (S Int T) = (rel_interior S) Int T"
1.2777 -proof-
1.2778 +proof-
1.2779 have "affine hull T = T" using assms by auto
1.2780 hence "rel_interior T = T" using rel_interior_univ[of T] by metis
1.2781 moreover have "closure T = T" using assms affine_closed[of T] by auto
1.2782 -ultimately show ?thesis using convex_rel_interior_inter_two[of S T] assms affine_imp_convex by auto
1.2783 +ultimately show ?thesis using convex_rel_interior_inter_two[of S T] assms affine_imp_convex by auto
1.2784 qed
1.2785
1.2786 lemma subset_rel_interior_convex:
1.2787 @@ -5175,11 +5175,11 @@
1.2788 proof-
1.2789 have *: "S Int closure T = S" using assms by auto
1.2790 have "~(rel_interior S <= rel_frontier T)"
1.2791 - using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
1.2792 + using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
1.2793 closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
1.2794 -hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}"
1.2795 +hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}"
1.2796 using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto
1.2797 -hence "rel_interior S Int rel_interior T = rel_interior (S Int closure T)" using assms convex_closure
1.2798 +hence "rel_interior S Int rel_interior T = rel_interior (S Int closure T)" using assms convex_closure
1.2799 convex_rel_interior_inter_two[of S "closure T"] convex_rel_interior_closure[of T] by auto
1.2800 also have "...=rel_interior (S)" using * by auto
1.2801 finally show ?thesis by auto
1.2802 @@ -5197,13 +5197,13 @@
1.2803 { assume "S ~= {}"
1.2804 have *: "f ` (rel_interior S) <= f ` S" unfolding image_mono using rel_interior_subset by auto
1.2805 have "f ` S <= f ` (closure S)" unfolding image_mono using closure_subset by auto
1.2806 -also have "... = f ` (closure (rel_interior S))" using convex_closure_rel_interior assms by auto
1.2807 -also have "... <= closure (f ` (rel_interior S))" using closure_linear_image assms by auto
1.2808 +also have "... = f ` (closure (rel_interior S))" using convex_closure_rel_interior assms by auto
1.2809 +also have "... <= closure (f ` (rel_interior S))" using closure_linear_image assms by auto
1.2810 finally have "closure (f ` S) = closure (f ` rel_interior S)"
1.2811 - using closure_mono[of "f ` S" "closure (f ` rel_interior S)"] closure_closure
1.2812 + using closure_mono[of "f ` S" "closure (f ` rel_interior S)"] closure_closure
1.2813 closure_mono[of "f ` rel_interior S" "f ` S"] * by auto
1.2814 hence "rel_interior (f ` S) = rel_interior (f ` rel_interior S)" using assms convex_rel_interior
1.2815 - linear_conv_bounded_linear[of f] convex_linear_image[of S] convex_linear_image[of "rel_interior S"]
1.2816 + linear_conv_bounded_linear[of f] convex_linear_image[of S] convex_linear_image[of "rel_interior S"]
1.2817 closure_eq_rel_interior_eq[of "f ` S" "f ` rel_interior S"] by auto
1.2818 hence "rel_interior (f ` S) <= f ` rel_interior S" using rel_interior_subset by auto
1.2819 moreover
1.2820 @@ -5218,7 +5218,7 @@
1.2821 ultimately have "(1 - e) *\<^sub>R x + e *\<^sub>R z : f ` S"
1.2822 using imageI[of "(1 - e) *\<^sub>R x1 + e *\<^sub>R z1" S f] by auto
1.2823 hence "EX e. (e>1 & (1 - e) *\<^sub>R x + e *\<^sub>R z : f ` S)" using e_def by auto
1.2824 - } from this have "z : rel_interior (f ` S)" using convex_rel_interior_iff[of "f ` S" z] `convex S`
1.2825 + } from this have "z : rel_interior (f ` S)" using convex_rel_interior_iff[of "f ` S" z] `convex S`
1.2826 `linear f` `S ~= {}` convex_linear_image[of S f] linear_conv_bounded_linear[of f] by auto
1.2827 } ultimately have ?thesis by auto
1.2828 } ultimately show ?thesis by blast
1.2829 @@ -5246,7 +5246,7 @@
1.2830 shows "rel_interior (f -` S) = f -` (rel_interior S)"
1.2831 proof-
1.2832 have "S ~= {}" using assms rel_interior_empty by auto
1.2833 -have nonemp: "f -` S ~= {}" by (metis assms(3) rel_interior_subset subset_empty vimage_mono)
1.2834 +have nonemp: "f -` S ~= {}" by (metis assms(3) rel_interior_subset subset_empty vimage_mono)
1.2835 hence "S Int (range f) ~= {}" by auto
1.2836 have conv: "convex (f -` S)" using convex_linear_preimage assms linear_conv_bounded_linear by auto
1.2837 hence "convex (S Int (range f))"
1.2838 @@ -5259,11 +5259,11 @@
1.2839 moreover have "(1-e)*\<^sub>R (f x)+ e *\<^sub>R (f z) = f ((1-e)*\<^sub>R x + e *\<^sub>R z)"
1.2840 using `linear f` by (simp add: linear_def)
1.2841 ultimately have "EX e. e>1 & (1-e)*\<^sub>R x + e *\<^sub>R z : f -` S" using e_def by auto
1.2842 - } hence "z : rel_interior (f -` S)"
1.2843 + } hence "z : rel_interior (f -` S)"
1.2844 using convex_rel_interior_iff[of "f -` S" z] conv nonemp by auto
1.2845 -}
1.2846 +}
1.2847 moreover
1.2848 -{ fix z assume z_def: "z : rel_interior (f -` S)"
1.2849 +{ fix z assume z_def: "z : rel_interior (f -` S)"
1.2850 { fix x assume x_def: "x: S Int (range f)"
1.2851 from this obtain y where y_def: "(f y = x) & (y : f -` S)" by auto
1.2852 from this obtain e where e_def: "e>1 & (1-e)*\<^sub>R y+ e *\<^sub>R z : f -` S"
1.2853 @@ -5276,13 +5276,13 @@
1.2854 `S Int (range f) ~= {}` convex_rel_interior_iff[of "S Int (range f)" "f z"] by auto
1.2855 moreover have "affine (range f)"
1.2856 by (metis assms(1) subspace_UNIV subspace_imp_affine subspace_linear_image)
1.2857 - ultimately have "f z : rel_interior S"
1.2858 + ultimately have "f z : rel_interior S"
1.2859 using convex_affine_rel_interior_inter[of S "range f"] assms by auto
1.2860 hence "z : f -` (rel_interior S)" by auto
1.2861 }
1.2862 ultimately show ?thesis by auto
1.2863 qed
1.2864 -
1.2865 +
1.2866
1.2867 lemma convex_direct_sum:
1.2868 fixes S :: "('n::euclidean_space) set"
1.2869 @@ -5313,9 +5313,9 @@
1.2870 proof-
1.2871 { fix x assume "x : (convex hull S) <*> (convex hull T)"
1.2872 from this obtain xs xt where xst_def: "xs : convex hull S & xt : convex hull T & (xs,xt) = x" by auto
1.2873 - from xst_def obtain sI su where s: "finite sI & sI <= S & (ALL x:sI. 0 <= su x) & setsum su sI = 1
1.2874 + from xst_def obtain sI su where s: "finite sI & sI <= S & (ALL x:sI. 0 <= su x) & setsum su sI = 1
1.2875 & (SUM v:sI. su v *\<^sub>R v) = xs" using convex_hull_explicit[of S] by auto
1.2876 - from xst_def obtain tI tu where t: "finite tI & tI <= T & (ALL x:tI. 0 <= tu x) & setsum tu tI = 1
1.2877 + from xst_def obtain tI tu where t: "finite tI & tI <= T & (ALL x:tI. 0 <= tu x) & setsum tu tI = 1
1.2878 & (SUM v:tI. tu v *\<^sub>R v) = xt" using convex_hull_explicit[of T] by auto
1.2879 def I == "(sI <*> tI)"
1.2880 def u == "(%i. (su (fst i))*(tu(snd i)))"
1.2881 @@ -5342,20 +5342,20 @@
1.2882 finally have h2: "snd (SUM v:sI <*> tI. (su (fst v) * tu (snd v)) *\<^sub>R v)=xt" by auto
1.2883 from h1 h2 have "(SUM v:sI <*> tI. (su (fst v) * tu (snd v)) *\<^sub>R v) = x" using xst_def by auto
1.2884
1.2885 - moreover have "finite I & (I <= S <*> T)" using s t I_def by auto
1.2886 + moreover have "finite I & (I <= S <*> T)" using s t I_def by auto
1.2887 moreover have "!i:I. 0 <= u i" using s t I_def u_def by (simp add: mult_nonneg_nonneg)
1.2888 - moreover have "setsum u I = 1" using u_def I_def setsum_cartesian_product[of "(% x y. (su x)*(tu y))"]
1.2889 + moreover have "setsum u I = 1" using u_def I_def setsum_cartesian_product[of "(% x y. (su x)*(tu y))"]
1.2890 s t setsum_product[of su sI tu tI] by (auto simp add: split_def)
1.2891 - ultimately have "x : convex hull (S <*> T)"
1.2892 + ultimately have "x : convex hull (S <*> T)"
1.2893 apply (subst convex_hull_explicit[of "S <*> T"]) apply rule
1.2894 apply (rule_tac x="I" in exI) apply (rule_tac x="u" in exI)
1.2895 using I_def u_def by auto
1.2896 }
1.2897 hence "convex hull (S <*> T) >= (convex hull S) <*> (convex hull T)" by auto
1.2898 -moreover have "convex ((convex hull S) <*> (convex hull T))"
1.2899 +moreover have "convex ((convex hull S) <*> (convex hull T))"
1.2900 by (simp add: convex_direct_sum convex_convex_hull)
1.2901 -ultimately show ?thesis
1.2902 - using hull_minimal[of "S <*> T" "(convex hull S) <*> (convex hull T)" "convex"]
1.2903 +ultimately show ?thesis
1.2904 + using hull_minimal[of "S <*> T" "(convex hull S) <*> (convex hull T)" "convex"]
1.2905 hull_subset[of S convex] hull_subset[of T convex] by auto
1.2906 qed
1.2907
1.2908 @@ -5373,45 +5373,45 @@
1.2909 hence ri: "rel_interior S ~= {}" "rel_interior T ~= {}" using rel_interior_convex_nonempty assms by auto
1.2910 hence "fst -` rel_interior S ~= {}" using fst_vimage_eq_Times[of "rel_interior S"] by auto
1.2911 hence "rel_interior ((fst :: 'n * 'm => 'n) -` S) = fst -` rel_interior S"
1.2912 - using fst_linear `convex S` rel_interior_convex_linear_preimage[of fst S] by auto
1.2913 + using fst_linear `convex S` rel_interior_convex_linear_preimage[of fst S] by auto
1.2914 hence s: "rel_interior (S <*> (UNIV :: 'm set)) = rel_interior S <*> UNIV" by (simp add: fst_vimage_eq_Times)
1.2915 from ri have "snd -` rel_interior T ~= {}" using snd_vimage_eq_Times[of "rel_interior T"] by auto
1.2916 hence "rel_interior ((snd :: 'n * 'm => 'm) -` T) = snd -` rel_interior T"
1.2917 - using snd_linear `convex T` rel_interior_convex_linear_preimage[of snd T] by auto
1.2918 + using snd_linear `convex T` rel_interior_convex_linear_preimage[of snd T] by auto
1.2919 hence t: "rel_interior ((UNIV :: 'n set) <*> T) = UNIV <*> rel_interior T" by (simp add: snd_vimage_eq_Times)
1.2920 -from s t have *: "rel_interior (S <*> (UNIV :: 'm set)) Int rel_interior ((UNIV :: 'n set) <*> T)
1.2921 +from s t have *: "rel_interior (S <*> (UNIV :: 'm set)) Int rel_interior ((UNIV :: 'n set) <*> T)
1.2922 = rel_interior S <*> rel_interior T" by auto
1.2923 have "(S <*> T) = (S <*> (UNIV :: 'm set)) Int ((UNIV :: 'n set) <*> T)" by auto
1.2924 hence "rel_interior (S <*> T) = rel_interior ((S <*> (UNIV :: 'm set)) Int ((UNIV :: 'n set) <*> T))" by auto
1.2925 -also have "...=rel_interior (S <*> (UNIV :: 'm set)) Int rel_interior ((UNIV :: 'n set) <*> T)"
1.2926 - apply (subst convex_rel_interior_inter_two[of "S <*> (UNIV :: 'm set)" "(UNIV :: 'n set) <*> T"])
1.2927 +also have "...=rel_interior (S <*> (UNIV :: 'm set)) Int rel_interior ((UNIV :: 'n set) <*> T)"
1.2928 + apply (subst convex_rel_interior_inter_two[of "S <*> (UNIV :: 'm set)" "(UNIV :: 'n set) <*> T"])
1.2929 using * ri assms convex_direct_sum by auto
1.2930 finally have ?thesis using * by auto
1.2931 }
1.2932 ultimately show ?thesis by blast
1.2933 qed
1.2934
1.2935 -lemma rel_interior_scaleR:
1.2936 +lemma rel_interior_scaleR:
1.2937 fixes S :: "('n::euclidean_space) set"
1.2938 assumes "c ~= 0"
1.2939 shows "(op *\<^sub>R c) ` (rel_interior S) = rel_interior ((op *\<^sub>R c) ` S)"
1.2940 using rel_interior_injective_linear_image[of "(op *\<^sub>R c)" S]
1.2941 linear_conv_bounded_linear[of "op *\<^sub>R c"] linear_scaleR injective_scaleR[of c] assms by auto
1.2942
1.2943 -lemma rel_interior_convex_scaleR:
1.2944 +lemma rel_interior_convex_scaleR:
1.2945 fixes S :: "('n::euclidean_space) set"
1.2946 assumes "convex S"
1.2947 shows "(op *\<^sub>R c) ` (rel_interior S) = rel_interior ((op *\<^sub>R c) ` S)"
1.2948 by (metis assms linear_scaleR rel_interior_convex_linear_image)
1.2949
1.2950 -lemma convex_rel_open_scaleR:
1.2951 +lemma convex_rel_open_scaleR:
1.2952 fixes S :: "('n::euclidean_space) set"
1.2953 assumes "convex S" "rel_open S"
1.2954 shows "convex ((op *\<^sub>R c) ` S) & rel_open ((op *\<^sub>R c) ` S)"
1.2955 by (metis assms convex_scaling rel_interior_convex_scaleR rel_open_def)
1.2956
1.2957
1.2958 -lemma convex_rel_open_finite_inter:
1.2959 +lemma convex_rel_open_finite_inter:
1.2960 assumes "!S : I. (convex (S :: ('n::euclidean_space) set) & rel_open S)"
1.2961 assumes "finite I"
1.2962 shows "convex (Inter I) & rel_open (Inter I)"
1.2963 @@ -5433,14 +5433,14 @@
1.2964 assumes "linear f"
1.2965 assumes "convex S" "rel_open S"
1.2966 shows "convex (f ` S) & rel_open (f ` S)"
1.2967 -by (metis assms convex_linear_image rel_interior_convex_linear_image
1.2968 +by (metis assms convex_linear_image rel_interior_convex_linear_image
1.2969 linear_conv_bounded_linear rel_open_def)
1.2970
1.2971 lemma convex_rel_open_linear_preimage:
1.2972 fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
1.2973 assumes "linear f"
1.2974 assumes "convex S" "rel_open S"
1.2975 -shows "convex (f -` S) & rel_open (f -` S)"
1.2976 +shows "convex (f -` S) & rel_open (f -` S)"
1.2977 proof-
1.2978 { assume "f -` (rel_interior S) = {}"
1.2979 hence "f -` S = {}" using assms unfolding rel_open_def by auto
1.2980 @@ -5483,21 +5483,21 @@
1.2981 }
1.2982 hence "snd ` (S Int fst -` {y}) = f y" using assms by auto
1.2983 hence ***: "rel_interior (f y) = snd ` rel_interior (S Int fst -` {y})"
1.2984 - using rel_interior_convex_linear_image[of snd "S Int fst -` {y}"] snd_linear conv by auto
1.2985 + using rel_interior_convex_linear_image[of snd "S Int fst -` {y}"] snd_linear conv by auto
1.2986 { fix z assume "z : rel_interior (f y)"
1.2987 hence "z : snd ` rel_interior (S Int fst -` {y})" using *** by auto
1.2988 - moreover have "{y} = fst ` rel_interior (S Int fst -` {y})" using * ** rel_interior_subset by auto
1.2989 + moreover have "{y} = fst ` rel_interior (S Int fst -` {y})" using * ** rel_interior_subset by auto
1.2990 ultimately have "(y,z) : rel_interior (S Int fst -` {y})" by force
1.2991 hence "(y,z) : rel_interior S" using ** by auto
1.2992 }
1.2993 moreover
1.2994 { fix z assume "(y,z) : rel_interior S"
1.2995 hence "(y,z) : rel_interior (S Int fst -` {y})" using ** by auto
1.2996 - hence "z : snd ` rel_interior (S Int fst -` {y})" by (metis Range_iff snd_eq_Range)
1.2997 + hence "z : snd ` rel_interior (S Int fst -` {y})" by (metis Range_iff snd_eq_Range)
1.2998 hence "z : rel_interior (f y)" using *** by auto
1.2999 }
1.3000 ultimately have "!!z. (y,z) : rel_interior S <-> z : rel_interior (f y)" by auto
1.3001 -}
1.3002 +}
1.3003 hence h2: "!!y z. y : rel_interior {t. f t ~= {}} ==> ((y, z) : rel_interior S) = (z : rel_interior (f y))"
1.3004 by auto
1.3005 { fix y z assume asm: "(y, z) : rel_interior S"
1.3006 @@ -5528,13 +5528,13 @@
1.3007 lemma rel_interior_convex_cone_aux:
1.3008 fixes S :: "('m::euclidean_space) set"
1.3009 assumes "convex S"
1.3010 -shows "(c,x) : rel_interior (cone hull ({(1 :: real)} <*> S)) <->
1.3011 +shows "(c,x) : rel_interior (cone hull ({(1 :: real)} <*> S)) <->
1.3012 c>0 & x : ((op *\<^sub>R c) ` (rel_interior S))"
1.3013 proof-
1.3014 -{ assume "S={}" hence ?thesis by (simp add: rel_interior_empty cone_hull_empty) }
1.3015 +{ assume "S={}" hence ?thesis by (simp add: rel_interior_empty cone_hull_empty) }
1.3016 moreover
1.3017 { assume "S ~= {}" from this obtain s where "s : S" by auto
1.3018 -have conv: "convex ({(1 :: real)} <*> S)" using convex_direct_sum[of "{(1 :: real)}" S]
1.3019 +have conv: "convex ({(1 :: real)} <*> S)" using convex_direct_sum[of "{(1 :: real)}" S]
1.3020 assms convex_singleton[of "1 :: real"] by auto
1.3021 def f == "(%y. {z. (y,z) : cone hull ({(1 :: real)} <*> S)})"
1.3022 hence *: "(c, x) : rel_interior (cone hull ({(1 :: real)} <*> S)) =
1.3023 @@ -5561,17 +5561,17 @@
1.3024 lemma rel_interior_convex_cone:
1.3025 fixes S :: "('m::euclidean_space) set"
1.3026 assumes "convex S"
1.3027 -shows "rel_interior (cone hull ({(1 :: real)} <*> S)) =
1.3028 +shows "rel_interior (cone hull ({(1 :: real)} <*> S)) =
1.3029 {(c,c *\<^sub>R x) |c x. c>0 & x : (rel_interior S)}"
1.3030 (is "?lhs=?rhs")
1.3031 proof-
1.3032 -{ fix z assume "z:?lhs"
1.3033 - have *: "z=(fst z,snd z)" by auto
1.3034 +{ fix z assume "z:?lhs"
1.3035 + have *: "z=(fst z,snd z)" by auto
1.3036 have "z:?rhs" using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms `z:?lhs` apply auto
1.3037 apply (rule_tac x="fst z" in exI) apply (rule_tac x="x" in exI) using * by auto
1.3038 }
1.3039 moreover
1.3040 -{ fix z assume "z:?rhs" hence "z:?lhs"
1.3041 +{ fix z assume "z:?rhs" hence "z:?lhs"
1.3042 using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms by auto
1.3043 }
1.3044 ultimately show ?thesis by blast
1.3045 @@ -5580,12 +5580,12 @@
1.3046 lemma convex_hull_finite_union:
1.3047 assumes "finite I"
1.3048 assumes "!i:I. (convex (S i) & (S i) ~= {})"
1.3049 -shows "convex hull (Union (S ` I)) =
1.3050 +shows "convex hull (Union (S ` I)) =
1.3051 {setsum (%i. c i *\<^sub>R s i) I |c s. (!i:I. c i >= 0) & (setsum c I = 1) & (!i:I. s i : S i)}"
1.3052 (is "?lhs = ?rhs")
1.3053 proof-
1.3054 -{ fix x assume "x : ?rhs"
1.3055 - from this obtain c s
1.3056 +{ fix x assume "x : ?rhs"
1.3057 + from this obtain c s
1.3058 where *: "setsum (%i. c i *\<^sub>R s i) I=x" "(setsum c I = 1)"
1.3059 "(!i:I. c i >= 0) & (!i:I. s i : S i)" by auto
1.3060 hence "!i:I. s i : convex hull (Union (S ` I))" using hull_subset[of "Union (S ` I)" convex] by auto
1.3061 @@ -5596,7 +5596,7 @@
1.3062
1.3063 { fix i assume "i:I"
1.3064 from this assms have "EX p. p : S i" by auto
1.3065 -}
1.3066 +}
1.3067 from this obtain p where p_def: "!i:I. p i : S i" by metis
1.3068
1.3069 { fix i assume "i:I"
1.3070 @@ -5606,10 +5606,10 @@
1.3071 def s == "(%j. if (j=i) then x else p j)"
1.3072 hence "!j. c j *\<^sub>R s j = (if (j=i) then x else 0)" using c_def by (auto simp add: algebra_simps)
1.3073 hence "x = setsum (%i. c i *\<^sub>R s i) I"
1.3074 - using s_def c_def `finite I` `i:I` setsum_delta[of I i "(%(j::'a). x)"] by auto
1.3075 + using s_def c_def `finite I` `i:I` setsum_delta[of I i "(%(j::'a). x)"] by auto
1.3076 hence "x : ?rhs" apply auto
1.3077 - apply (rule_tac x="c" in exI)
1.3078 - apply (rule_tac x="s" in exI) using * c_def s_def p_def `x : S i` by auto
1.3079 + apply (rule_tac x="c" in exI)
1.3080 + apply (rule_tac x="s" in exI) using * c_def s_def p_def `x : S i` by auto
1.3081 } hence "?rhs >= S i" by auto
1.3082 } hence *: "?rhs >= Union (S ` I)" by auto
1.3083
1.3084 @@ -5624,21 +5624,21 @@
1.3085 have "setsum (%i. u * c i) I = u * setsum c I" by (simp add: setsum_right_distrib)
1.3086 moreover have "setsum (%i. v * d i) I = v * setsum d I" by (simp add: setsum_right_distrib)
1.3087 ultimately have sum1: "setsum e I = 1" using e_def xc yc uv by (simp add: setsum_addf)
1.3088 - def q == "(%i. if (e i = 0) then (p i)
1.3089 + def q == "(%i. if (e i = 0) then (p i)
1.3090 else (u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i))"
1.3091 { fix i assume "i:I"
1.3092 { assume "e i = 0" hence "q i : S i" using `i:I` p_def q_def by auto }
1.3093 moreover
1.3094 - { assume "e i ~= 0"
1.3095 - hence "q i : S i" using mem_convex_alt[of "S i" "s i" "t i" "u * (c i)" "v * (d i)"]
1.3096 + { assume "e i ~= 0"
1.3097 + hence "q i : S i" using mem_convex_alt[of "S i" "s i" "t i" "u * (c i)" "v * (d i)"]
1.3098 mult_nonneg_nonneg[of u "c i"] mult_nonneg_nonneg[of v "d i"]
1.3099 assms q_def e_def `i:I` `e i ~= 0` xc yc uv by auto
1.3100 } ultimately have "q i : S i" by auto
1.3101 } hence qs: "!i:I. q i : S i" by auto
1.3102 { fix i assume "i:I"
1.3103 - { assume "e i = 0"
1.3104 + { assume "e i = 0"
1.3105 have ge: "u * (c i) >= 0 & v * (d i) >= 0" using xc yc uv `i:I` by (simp add: mult_nonneg_nonneg)
1.3106 - moreover hence "u * (c i) <= 0 & v * (d i) <= 0" using `e i = 0` e_def `i:I` by simp
1.3107 + moreover hence "u * (c i) <= 0 & v * (d i) <= 0" using `e i = 0` e_def `i:I` by simp
1.3108 ultimately have "u * (c i) = 0 & v * (d i) = 0" by auto
1.3109 hence "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)"
1.3110 using `e i = 0` by auto
1.3111 @@ -5651,7 +5651,7 @@
1.3112 = (e i) *\<^sub>R (q i)" by auto
1.3113 hence "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)"
1.3114 using `e i ~= 0` by (simp add: algebra_simps)
1.3115 - } ultimately have
1.3116 + } ultimately have
1.3117 "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)" by blast
1.3118 } hence *: "!i:I.
1.3119 (u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)" by auto
1.3120 @@ -5662,7 +5662,7 @@
1.3121 finally have "u *\<^sub>R x + v *\<^sub>R y = setsum (%i. (e i) *\<^sub>R (q i)) I" by auto
1.3122 hence "u *\<^sub>R x + v *\<^sub>R y : ?rhs" using ge0 sum1 qs by auto
1.3123 } hence "convex ?rhs" unfolding convex_def by auto
1.3124 -from this show ?thesis using `?lhs >= ?rhs` *
1.3125 +from this show ?thesis using `?lhs >= ?rhs` *
1.3126 hull_minimal[of "Union (S ` I)" "?rhs" "convex"] by blast
1.3127 qed
1.3128
1.3129 @@ -5679,13 +5679,13 @@
1.3130 moreover have "convex hull Union (s ` I) =
1.3131 {SUM i:I. c i *\<^sub>R sa i |c sa. (ALL i:I. 0 <= c i) & setsum c I = 1 & (ALL i:I. sa i : s i)}"
1.3132 apply (subst convex_hull_finite_union[of I s]) using assms s_def I_def by auto
1.3133 -moreover have
1.3134 +moreover have
1.3135 "{SUM i:I. c i *\<^sub>R sa i |c sa. (ALL i:I. 0 <= c i) & setsum c I = 1 & (ALL i:I. sa i : s i)} <=
1.3136 ?rhs"
1.3137 using s_def I_def by auto
1.3138 -ultimately have "?lhs<=?rhs" by auto
1.3139 -{ fix x assume "x : ?rhs"
1.3140 - from this obtain u v s t
1.3141 +ultimately have "?lhs<=?rhs" by auto
1.3142 +{ fix x assume "x : ?rhs"
1.3143 + from this obtain u v s t
1.3144 where *: "x=u *\<^sub>R s + v *\<^sub>R t & u>=0 & v>=0 & u+v=1 & s:S & t:T" by auto
1.3145 hence "x : convex hull {s,t}" using convex_hull_2[of s t] by auto
1.3146 hence "x : convex hull (S Un T)" using * hull_mono[of "{s, t}" "S Un T"] by auto