1275 have *: "\<forall>i\<in>Basis. i:d \<longrightarrow> u i = x\<bullet>i" |
1275 have *: "\<forall>i\<in>Basis. i:d \<longrightarrow> u i = x\<bullet>i" |
1276 and "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)" |
1276 and "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)" |
1277 using as(3) |
1277 using as(3) |
1278 unfolding substdbasis_expansion_unique[OF assms] |
1278 unfolding substdbasis_expansion_unique[OF assms] |
1279 by auto |
1279 by auto |
1280 then have **: "sum u ?D = sum (op \<bullet> x) ?D" |
1280 then have **: "sum u ?D = sum ((\<bullet>) x) ?D" |
1281 apply - |
1281 apply - |
1282 apply (rule sum.cong) |
1282 apply (rule sum.cong) |
1283 using assms |
1283 using assms |
1284 apply auto |
1284 apply auto |
1285 done |
1285 done |
1286 have "(\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> sum (op \<bullet> x) ?D \<le> 1" |
1286 have "(\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> sum ((\<bullet>) x) ?D \<le> 1" |
1287 proof (rule,rule) |
1287 proof (rule,rule) |
1288 fix i :: 'a |
1288 fix i :: 'a |
1289 assume i: "i \<in> Basis" |
1289 assume i: "i \<in> Basis" |
1290 have "i \<in> d \<Longrightarrow> 0 \<le> x\<bullet>i" |
1290 have "i \<in> d \<Longrightarrow> 0 \<le> x\<bullet>i" |
1291 unfolding *[rule_format,OF i,symmetric] |
1291 unfolding *[rule_format,OF i,symmetric] |
1294 done |
1294 done |
1295 moreover have "i \<notin> d \<Longrightarrow> 0 \<le> x\<bullet>i" |
1295 moreover have "i \<notin> d \<Longrightarrow> 0 \<le> x\<bullet>i" |
1296 using \<open>(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)\<close>[rule_format, OF i] by auto |
1296 using \<open>(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)\<close>[rule_format, OF i] by auto |
1297 ultimately show "0 \<le> x\<bullet>i" by auto |
1297 ultimately show "0 \<le> x\<bullet>i" by auto |
1298 qed (insert as(2)[unfolded **], auto) |
1298 qed (insert as(2)[unfolded **], auto) |
1299 then show "(\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> sum (op \<bullet> x) ?D \<le> 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)" |
1299 then show "(\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> sum ((\<bullet>) x) ?D \<le> 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)" |
1300 using \<open>(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)\<close> by auto |
1300 using \<open>(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)\<close> by auto |
1301 next |
1301 next |
1302 fix x :: "'a::euclidean_space" |
1302 fix x :: "'a::euclidean_space" |
1303 assume as: "\<forall>i\<in>Basis. 0 \<le> x \<bullet> i" "sum (op \<bullet> x) ?D \<le> 1" "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)" |
1303 assume as: "\<forall>i\<in>Basis. 0 \<le> x \<bullet> i" "sum ((\<bullet>) x) ?D \<le> 1" "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)" |
1304 show "\<exists>u. (\<forall>x\<in>?D. 0 \<le> u x) \<and> sum u ?D \<le> 1 \<and> (\<Sum>x\<in>?D. u x *\<^sub>R x) = x" |
1304 show "\<exists>u. (\<forall>x\<in>?D. 0 \<le> u x) \<and> sum u ?D \<le> 1 \<and> (\<Sum>x\<in>?D. u x *\<^sub>R x) = x" |
1305 using as d |
1305 using as d |
1306 unfolding substdbasis_expansion_unique[OF assms] |
1306 unfolding substdbasis_expansion_unique[OF assms] |
1307 apply (rule_tac x="inner x" in exI) |
1307 apply (rule_tac x="inner x" in exI) |
1308 apply auto |
1308 apply auto |
1344 unfolding dist_norm |
1344 unfolding dist_norm |
1345 by (auto intro!: mult_strict_left_mono simp: SOME_Basis) |
1345 by (auto intro!: mult_strict_left_mono simp: SOME_Basis) |
1346 have "\<And>i. i \<in> Basis \<Longrightarrow> (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis)) \<bullet> i = |
1346 have "\<And>i. i \<in> Basis \<Longrightarrow> (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis)) \<bullet> i = |
1347 x\<bullet>i + (if i = (SOME i. i\<in>Basis) then e/2 else 0)" |
1347 x\<bullet>i + (if i = (SOME i. i\<in>Basis) then e/2 else 0)" |
1348 by (auto simp: SOME_Basis inner_Basis inner_simps) |
1348 by (auto simp: SOME_Basis inner_Basis inner_simps) |
1349 then have *: "sum (op \<bullet> (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis))) Basis = |
1349 then have *: "sum ((\<bullet>) (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis))) Basis = |
1350 sum (\<lambda>i. x\<bullet>i + (if (SOME i. i\<in>Basis) = i then e/2 else 0)) Basis" |
1350 sum (\<lambda>i. x\<bullet>i + (if (SOME i. i\<in>Basis) = i then e/2 else 0)) Basis" |
1351 apply (rule_tac sum.cong) |
1351 apply (rule_tac sum.cong) |
1352 apply auto |
1352 apply auto |
1353 done |
1353 done |
1354 have "sum (op \<bullet> x) Basis < sum (op \<bullet> (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis))) Basis" |
1354 have "sum ((\<bullet>) x) Basis < sum ((\<bullet>) (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis))) Basis" |
1355 unfolding * sum.distrib |
1355 unfolding * sum.distrib |
1356 using \<open>e > 0\<close> DIM_positive[where 'a='a] |
1356 using \<open>e > 0\<close> DIM_positive[where 'a='a] |
1357 apply (subst sum.delta') |
1357 apply (subst sum.delta') |
1358 apply (auto simp: SOME_Basis) |
1358 apply (auto simp: SOME_Basis) |
1359 done |
1359 done |
1360 also have "\<dots> \<le> 1" |
1360 also have "\<dots> \<le> 1" |
1361 using ** |
1361 using ** |
1362 apply (drule_tac as[rule_format]) |
1362 apply (drule_tac as[rule_format]) |
1363 apply auto |
1363 apply auto |
1364 done |
1364 done |
1365 finally show "sum (op \<bullet> x) Basis < 1" by auto |
1365 finally show "sum ((\<bullet>) x) Basis < 1" by auto |
1366 qed |
1366 qed |
1367 next |
1367 next |
1368 fix x :: 'a |
1368 fix x :: 'a |
1369 assume as: "\<forall>i\<in>Basis. 0 < x \<bullet> i" "sum (op \<bullet> x) Basis < 1" |
1369 assume as: "\<forall>i\<in>Basis. 0 < x \<bullet> i" "sum ((\<bullet>) x) Basis < 1" |
1370 obtain a :: 'b where "a \<in> UNIV" using UNIV_witness .. |
1370 obtain a :: 'b where "a \<in> UNIV" using UNIV_witness .. |
1371 let ?d = "(1 - sum (op \<bullet> x) Basis) / real (DIM('a))" |
1371 let ?d = "(1 - sum ((\<bullet>) x) Basis) / real (DIM('a))" |
1372 show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> (\<forall>i\<in>Basis. 0 \<le> y \<bullet> i) \<and> sum (op \<bullet> y) Basis \<le> 1" |
1372 show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> (\<forall>i\<in>Basis. 0 \<le> y \<bullet> i) \<and> sum ((\<bullet>) y) Basis \<le> 1" |
1373 proof (rule_tac x="min (Min ((op \<bullet> x) ` Basis)) D" for D in exI, intro conjI impI allI) |
1373 proof (rule_tac x="min (Min (((\<bullet>) x) ` Basis)) D" for D in exI, intro conjI impI allI) |
1374 fix y |
1374 fix y |
1375 assume y: "dist x y < min (Min (op \<bullet> x ` Basis)) ?d" |
1375 assume y: "dist x y < min (Min ((\<bullet>) x ` Basis)) ?d" |
1376 have "sum (op \<bullet> y) Basis \<le> sum (\<lambda>i. x\<bullet>i + ?d) Basis" |
1376 have "sum ((\<bullet>) y) Basis \<le> sum (\<lambda>i. x\<bullet>i + ?d) Basis" |
1377 proof (rule sum_mono) |
1377 proof (rule sum_mono) |
1378 fix i :: 'a |
1378 fix i :: 'a |
1379 assume i: "i \<in> Basis" |
1379 assume i: "i \<in> Basis" |
1380 then have "\<bar>y\<bullet>i - x\<bullet>i\<bar> < ?d" |
1380 then have "\<bar>y\<bullet>i - x\<bullet>i\<bar> < ?d" |
1381 apply - |
1381 apply - |
1387 then show "y \<bullet> i \<le> x \<bullet> i + ?d" by auto |
1387 then show "y \<bullet> i \<le> x \<bullet> i + ?d" by auto |
1388 qed |
1388 qed |
1389 also have "\<dots> \<le> 1" |
1389 also have "\<dots> \<le> 1" |
1390 unfolding sum.distrib sum_constant |
1390 unfolding sum.distrib sum_constant |
1391 by (auto simp add: Suc_le_eq) |
1391 by (auto simp add: Suc_le_eq) |
1392 finally show "sum (op \<bullet> y) Basis \<le> 1" . |
1392 finally show "sum ((\<bullet>) y) Basis \<le> 1" . |
1393 show "(\<forall>i\<in>Basis. 0 \<le> y \<bullet> i)" |
1393 show "(\<forall>i\<in>Basis. 0 \<le> y \<bullet> i)" |
1394 proof safe |
1394 proof safe |
1395 fix i :: 'a |
1395 fix i :: 'a |
1396 assume i: "i \<in> Basis" |
1396 assume i: "i \<in> Basis" |
1397 have "norm (x - y) < x\<bullet>i" |
1397 have "norm (x - y) < x\<bullet>i" |
1403 then show "0 \<le> y\<bullet>i" |
1403 then show "0 \<le> y\<bullet>i" |
1404 using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format, OF i] |
1404 using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format, OF i] |
1405 by (auto simp: inner_simps) |
1405 by (auto simp: inner_simps) |
1406 qed |
1406 qed |
1407 next |
1407 next |
1408 have "Min ((op \<bullet> x) ` Basis) > 0" |
1408 have "Min (((\<bullet>) x) ` Basis) > 0" |
1409 using as by simp |
1409 using as by simp |
1410 moreover have "?d > 0" |
1410 moreover have "?d > 0" |
1411 using as by (auto simp: Suc_le_eq) |
1411 using as by (auto simp: Suc_le_eq) |
1412 ultimately show "0 < min (Min (op \<bullet> x ` Basis)) ((1 - sum (op \<bullet> x) Basis) / real DIM('a))" |
1412 ultimately show "0 < min (Min ((\<bullet>) x ` Basis)) ((1 - sum ((\<bullet>) x) Basis) / real DIM('a))" |
1413 by linarith |
1413 by linarith |
1414 qed |
1414 qed |
1415 qed |
1415 qed |
1416 |
1416 |
1417 lemma interior_std_simplex_nonempty: |
1417 lemma interior_std_simplex_nonempty: |
1434 fix i :: 'a |
1434 fix i :: 'a |
1435 assume i: "i \<in> Basis" |
1435 assume i: "i \<in> Basis" |
1436 show "0 < ?a \<bullet> i" |
1436 show "0 < ?a \<bullet> i" |
1437 unfolding **[OF i] by (auto simp add: Suc_le_eq DIM_positive) |
1437 unfolding **[OF i] by (auto simp add: Suc_le_eq DIM_positive) |
1438 next |
1438 next |
1439 have "sum (op \<bullet> ?a) ?D = sum (\<lambda>i. inverse (2 * real DIM('a))) ?D" |
1439 have "sum ((\<bullet>) ?a) ?D = sum (\<lambda>i. inverse (2 * real DIM('a))) ?D" |
1440 apply (rule sum.cong) |
1440 apply (rule sum.cong) |
1441 apply rule |
1441 apply rule |
1442 apply auto |
1442 apply auto |
1443 done |
1443 done |
1444 also have "\<dots> < 1" |
1444 also have "\<dots> < 1" |
1445 unfolding sum_constant divide_inverse[symmetric] |
1445 unfolding sum_constant divide_inverse[symmetric] |
1446 by (auto simp add: field_simps) |
1446 by (auto simp add: field_simps) |
1447 finally show "sum (op \<bullet> ?a) ?D < 1" by auto |
1447 finally show "sum ((\<bullet>) ?a) ?D < 1" by auto |
1448 qed |
1448 qed |
1449 qed |
1449 qed |
1450 |
1450 |
1451 lemma rel_interior_substd_simplex: |
1451 lemma rel_interior_substd_simplex: |
1452 assumes d: "d \<subseteq> Basis" |
1452 assumes d: "d \<subseteq> Basis" |
1476 assume x: "x \<in> rel_interior (convex hull (insert 0 ?p))" |
1476 assume x: "x \<in> rel_interior (convex hull (insert 0 ?p))" |
1477 then obtain e where e0: "e > 0" and |
1477 then obtain e where e0: "e > 0" and |
1478 "ball x e \<inter> {xa. (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> xa\<bullet>i = 0)} \<subseteq> convex hull (insert 0 ?p)" |
1478 "ball x e \<inter> {xa. (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> xa\<bullet>i = 0)} \<subseteq> convex hull (insert 0 ?p)" |
1479 using mem_rel_interior_ball[of x "convex hull (insert 0 ?p)"] h0 by auto |
1479 using mem_rel_interior_ball[of x "convex hull (insert 0 ?p)"] h0 by auto |
1480 then have as: "\<forall>xa. dist x xa < e \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> xa\<bullet>i = 0) \<longrightarrow> |
1480 then have as: "\<forall>xa. dist x xa < e \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> xa\<bullet>i = 0) \<longrightarrow> |
1481 (\<forall>i\<in>d. 0 \<le> xa \<bullet> i) \<and> sum (op \<bullet> xa) d \<le> 1" |
1481 (\<forall>i\<in>d. 0 \<le> xa \<bullet> i) \<and> sum ((\<bullet>) xa) d \<le> 1" |
1482 unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto |
1482 unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto |
1483 have x0: "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)" |
1483 have x0: "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)" |
1484 using x rel_interior_subset substd_simplex[OF assms] by auto |
1484 using x rel_interior_subset substd_simplex[OF assms] by auto |
1485 have "(\<forall>i\<in>d. 0 < x \<bullet> i) \<and> sum (op \<bullet> x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)" |
1485 have "(\<forall>i\<in>d. 0 < x \<bullet> i) \<and> sum ((\<bullet>) x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)" |
1486 apply rule |
1486 apply rule |
1487 apply rule |
1487 apply rule |
1488 proof - |
1488 proof - |
1489 fix i :: 'a |
1489 fix i :: 'a |
1490 assume "i \<in> d" |
1490 assume "i \<in> d" |
1507 using \<open>e > 0\<close> norm_Basis[of a] d |
1507 using \<open>e > 0\<close> norm_Basis[of a] d |
1508 unfolding dist_norm |
1508 unfolding dist_norm |
1509 by auto |
1509 by auto |
1510 have "\<And>i. i \<in> Basis \<Longrightarrow> (x + (e / 2) *\<^sub>R a) \<bullet> i = x\<bullet>i + (if i = a then e/2 else 0)" |
1510 have "\<And>i. i \<in> Basis \<Longrightarrow> (x + (e / 2) *\<^sub>R a) \<bullet> i = x\<bullet>i + (if i = a then e/2 else 0)" |
1511 using a d by (auto simp: inner_simps inner_Basis) |
1511 using a d by (auto simp: inner_simps inner_Basis) |
1512 then have *: "sum (op \<bullet> (x + (e / 2) *\<^sub>R a)) d = |
1512 then have *: "sum ((\<bullet>) (x + (e / 2) *\<^sub>R a)) d = |
1513 sum (\<lambda>i. x\<bullet>i + (if a = i then e/2 else 0)) d" |
1513 sum (\<lambda>i. x\<bullet>i + (if a = i then e/2 else 0)) d" |
1514 using d by (intro sum.cong) auto |
1514 using d by (intro sum.cong) auto |
1515 have "a \<in> Basis" |
1515 have "a \<in> Basis" |
1516 using \<open>a \<in> d\<close> d by auto |
1516 using \<open>a \<in> d\<close> d by auto |
1517 then have h1: "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> (x + (e / 2) *\<^sub>R a) \<bullet> i = 0)" |
1517 then have h1: "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> (x + (e / 2) *\<^sub>R a) \<bullet> i = 0)" |
1518 using x0 d \<open>a\<in>d\<close> by (auto simp add: inner_add_left inner_Basis) |
1518 using x0 d \<open>a\<in>d\<close> by (auto simp add: inner_add_left inner_Basis) |
1519 have "sum (op \<bullet> x) d < sum (op \<bullet> (x + (e / 2) *\<^sub>R a)) d" |
1519 have "sum ((\<bullet>) x) d < sum ((\<bullet>) (x + (e / 2) *\<^sub>R a)) d" |
1520 unfolding * sum.distrib |
1520 unfolding * sum.distrib |
1521 using \<open>e > 0\<close> \<open>a \<in> d\<close> |
1521 using \<open>e > 0\<close> \<open>a \<in> d\<close> |
1522 using \<open>finite d\<close> |
1522 using \<open>finite d\<close> |
1523 by (auto simp add: sum.delta') |
1523 by (auto simp add: sum.delta') |
1524 also have "\<dots> \<le> 1" |
1524 also have "\<dots> \<le> 1" |
1525 using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R a"] |
1525 using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R a"] |
1526 by auto |
1526 by auto |
1527 finally show "sum (op \<bullet> x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)" |
1527 finally show "sum ((\<bullet>) x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)" |
1528 using x0 by auto |
1528 using x0 by auto |
1529 qed |
1529 qed |
1530 } |
1530 } |
1531 moreover |
1531 moreover |
1532 { |
1532 { |
1541 then have h2: "x \<in> convex hull (insert 0 ?p)" |
1541 then have h2: "x \<in> convex hull (insert 0 ?p)" |
1542 using as assms |
1542 using as assms |
1543 unfolding substd_simplex[OF assms] by fastforce |
1543 unfolding substd_simplex[OF assms] by fastforce |
1544 obtain a where a: "a \<in> d" |
1544 obtain a where a: "a \<in> d" |
1545 using \<open>d \<noteq> {}\<close> by auto |
1545 using \<open>d \<noteq> {}\<close> by auto |
1546 let ?d = "(1 - sum (op \<bullet> x) d) / real (card d)" |
1546 let ?d = "(1 - sum ((\<bullet>) x) d) / real (card d)" |
1547 have "0 < card d" using \<open>d \<noteq> {}\<close> \<open>finite d\<close> |
1547 have "0 < card d" using \<open>d \<noteq> {}\<close> \<open>finite d\<close> |
1548 by (simp add: card_gt_0_iff) |
1548 by (simp add: card_gt_0_iff) |
1549 have "Min ((op \<bullet> x) ` d) > 0" |
1549 have "Min (((\<bullet>) x) ` d) > 0" |
1550 using as \<open>d \<noteq> {}\<close> \<open>finite d\<close> by (simp add: Min_gr_iff) |
1550 using as \<open>d \<noteq> {}\<close> \<open>finite d\<close> by (simp add: Min_gr_iff) |
1551 moreover have "?d > 0" using as using \<open>0 < card d\<close> by auto |
1551 moreover have "?d > 0" using as using \<open>0 < card d\<close> by auto |
1552 ultimately have h3: "min (Min ((op \<bullet> x) ` d)) ?d > 0" |
1552 ultimately have h3: "min (Min (((\<bullet>) x) ` d)) ?d > 0" |
1553 by auto |
1553 by auto |
1554 |
1554 |
1555 have "x \<in> rel_interior (convex hull (insert 0 ?p))" |
1555 have "x \<in> rel_interior (convex hull (insert 0 ?p))" |
1556 unfolding rel_interior_ball mem_Collect_eq h0 |
1556 unfolding rel_interior_ball mem_Collect_eq h0 |
1557 apply (rule,rule h2) |
1557 apply (rule,rule h2) |
1558 unfolding substd_simplex[OF assms] |
1558 unfolding substd_simplex[OF assms] |
1559 apply (rule_tac x="min (Min ((op \<bullet> x) ` d)) ?d" in exI) |
1559 apply (rule_tac x="min (Min (((\<bullet>) x) ` d)) ?d" in exI) |
1560 apply (rule, rule h3) |
1560 apply (rule, rule h3) |
1561 apply safe |
1561 apply safe |
1562 unfolding mem_ball |
1562 unfolding mem_ball |
1563 proof - |
1563 proof - |
1564 fix y :: 'a |
1564 fix y :: 'a |
1565 assume y: "dist x y < min (Min (op \<bullet> x ` d)) ?d" |
1565 assume y: "dist x y < min (Min ((\<bullet>) x ` d)) ?d" |
1566 assume y2: "\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> y\<bullet>i = 0" |
1566 assume y2: "\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> y\<bullet>i = 0" |
1567 have "sum (op \<bullet> y) d \<le> sum (\<lambda>i. x\<bullet>i + ?d) d" |
1567 have "sum ((\<bullet>) y) d \<le> sum (\<lambda>i. x\<bullet>i + ?d) d" |
1568 proof (rule sum_mono) |
1568 proof (rule sum_mono) |
1569 fix i |
1569 fix i |
1570 assume "i \<in> d" |
1570 assume "i \<in> d" |
1571 with d have i: "i \<in> Basis" |
1571 with d have i: "i \<in> Basis" |
1572 by auto |
1572 by auto |
1579 then show "y \<bullet> i \<le> x \<bullet> i + ?d" by auto |
1579 then show "y \<bullet> i \<le> x \<bullet> i + ?d" by auto |
1580 qed |
1580 qed |
1581 also have "\<dots> \<le> 1" |
1581 also have "\<dots> \<le> 1" |
1582 unfolding sum.distrib sum_constant using \<open>0 < card d\<close> |
1582 unfolding sum.distrib sum_constant using \<open>0 < card d\<close> |
1583 by auto |
1583 by auto |
1584 finally show "sum (op \<bullet> y) d \<le> 1" . |
1584 finally show "sum ((\<bullet>) y) d \<le> 1" . |
1585 |
1585 |
1586 fix i :: 'a |
1586 fix i :: 'a |
1587 assume i: "i \<in> Basis" |
1587 assume i: "i \<in> Basis" |
1588 then show "0 \<le> y\<bullet>i" |
1588 then show "0 \<le> y\<bullet>i" |
1589 proof (cases "i\<in>d") |
1589 proof (cases "i\<in>d") |
1590 case True |
1590 case True |
1591 have "norm (x - y) < x\<bullet>i" |
1591 have "norm (x - y) < x\<bullet>i" |
1592 using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1] |
1592 using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1] |
1593 using Min_gr_iff[of "op \<bullet> x ` d" "norm (x - y)"] \<open>0 < card d\<close> \<open>i:d\<close> |
1593 using Min_gr_iff[of "(\<bullet>) x ` d" "norm (x - y)"] \<open>0 < card d\<close> \<open>i:d\<close> |
1594 by (simp add: card_gt_0_iff) |
1594 by (simp add: card_gt_0_iff) |
1595 then show "0 \<le> y\<bullet>i" |
1595 then show "0 \<le> y\<bullet>i" |
1596 using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format] |
1596 using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format] |
1597 by (auto simp: inner_simps) |
1597 by (auto simp: inner_simps) |
1598 qed (insert y2, auto) |
1598 qed (insert y2, auto) |
1599 qed |
1599 qed |
1600 } |
1600 } |
1601 ultimately have |
1601 ultimately have |
1602 "\<And>x. x \<in> rel_interior (convex hull insert 0 d) \<longleftrightarrow> |
1602 "\<And>x. x \<in> rel_interior (convex hull insert 0 d) \<longleftrightarrow> |
1603 x \<in> {x. (\<forall>i\<in>d. 0 < x \<bullet> i) \<and> sum (op \<bullet> x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)}" |
1603 x \<in> {x. (\<forall>i\<in>d. 0 < x \<bullet> i) \<and> sum ((\<bullet>) x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)}" |
1604 by blast |
1604 by blast |
1605 then show ?thesis by (rule set_eqI) |
1605 then show ?thesis by (rule set_eqI) |
1606 qed |
1606 qed |
1607 qed |
1607 qed |
1608 |
1608 |
1643 using d1 by auto |
1643 using d1 by auto |
1644 also have "\<dots> = ?a \<bullet> i" using **[of i] \<open>i \<in> d\<close> |
1644 also have "\<dots> = ?a \<bullet> i" using **[of i] \<open>i \<in> d\<close> |
1645 by auto |
1645 by auto |
1646 finally show "0 < ?a \<bullet> i" by auto |
1646 finally show "0 < ?a \<bullet> i" by auto |
1647 next |
1647 next |
1648 have "sum (op \<bullet> ?a) ?D = sum (\<lambda>i. inverse (2 * real (card d))) ?D" |
1648 have "sum ((\<bullet>) ?a) ?D = sum (\<lambda>i. inverse (2 * real (card d))) ?D" |
1649 by (rule sum.cong) (rule refl, rule **) |
1649 by (rule sum.cong) (rule refl, rule **) |
1650 also have "\<dots> < 1" |
1650 also have "\<dots> < 1" |
1651 unfolding sum_constant divide_real_def[symmetric] |
1651 unfolding sum_constant divide_real_def[symmetric] |
1652 by (auto simp add: field_simps) |
1652 by (auto simp add: field_simps) |
1653 finally show "sum (op \<bullet> ?a) ?D < 1" by auto |
1653 finally show "sum ((\<bullet>) ?a) ?D < 1" by auto |
1654 next |
1654 next |
1655 fix i |
1655 fix i |
1656 assume "i \<in> Basis" and "i \<notin> d" |
1656 assume "i \<in> Basis" and "i \<notin> d" |
1657 have "?a \<in> span d" |
1657 have "?a \<in> span d" |
1658 proof (rule span_sum[of d "(\<lambda>b. b /\<^sub>R (2 * real (card d)))" d]) |
1658 proof (rule span_sum[of d "(\<lambda>b. b /\<^sub>R (2 * real (card d)))" d]) |
1746 shows "rel_interior S = {} \<longleftrightarrow> S = {}" |
1746 shows "rel_interior S = {} \<longleftrightarrow> S = {}" |
1747 proof - |
1747 proof - |
1748 { |
1748 { |
1749 assume "S \<noteq> {}" |
1749 assume "S \<noteq> {}" |
1750 then obtain a where "a \<in> S" by auto |
1750 then obtain a where "a \<in> S" by auto |
1751 then have "0 \<in> op + (-a) ` S" |
1751 then have "0 \<in> (+) (-a) ` S" |
1752 using assms exI[of "(\<lambda>x. x \<in> S \<and> - a + x = 0)" a] by auto |
1752 using assms exI[of "(\<lambda>x. x \<in> S \<and> - a + x = 0)" a] by auto |
1753 then have "rel_interior (op + (-a) ` S) \<noteq> {}" |
1753 then have "rel_interior ((+) (-a) ` S) \<noteq> {}" |
1754 using rel_interior_convex_nonempty_aux[of "op + (-a) ` S"] |
1754 using rel_interior_convex_nonempty_aux[of "(+) (-a) ` S"] |
1755 convex_translation[of S "-a"] assms |
1755 convex_translation[of S "-a"] assms |
1756 by auto |
1756 by auto |
1757 then have "rel_interior S \<noteq> {}" |
1757 then have "rel_interior S \<noteq> {}" |
1758 using rel_interior_translation by auto |
1758 using rel_interior_translation by auto |
1759 } |
1759 } |
2956 qed |
2956 qed |
2957 |
2957 |
2958 lemma rel_interior_scaleR: |
2958 lemma rel_interior_scaleR: |
2959 fixes S :: "'n::euclidean_space set" |
2959 fixes S :: "'n::euclidean_space set" |
2960 assumes "c \<noteq> 0" |
2960 assumes "c \<noteq> 0" |
2961 shows "(op *\<^sub>R c) ` (rel_interior S) = rel_interior ((op *\<^sub>R c) ` S)" |
2961 shows "(( *\<^sub>R) c) ` (rel_interior S) = rel_interior ((( *\<^sub>R) c) ` S)" |
2962 using rel_interior_injective_linear_image[of "(op *\<^sub>R c)" S] |
2962 using rel_interior_injective_linear_image[of "(( *\<^sub>R) c)" S] |
2963 linear_conv_bounded_linear[of "op *\<^sub>R c"] linear_scaleR injective_scaleR[of c] assms |
2963 linear_conv_bounded_linear[of "( *\<^sub>R) c"] linear_scaleR injective_scaleR[of c] assms |
2964 by auto |
2964 by auto |
2965 |
2965 |
2966 lemma rel_interior_convex_scaleR: |
2966 lemma rel_interior_convex_scaleR: |
2967 fixes S :: "'n::euclidean_space set" |
2967 fixes S :: "'n::euclidean_space set" |
2968 assumes "convex S" |
2968 assumes "convex S" |
2969 shows "(op *\<^sub>R c) ` (rel_interior S) = rel_interior ((op *\<^sub>R c) ` S)" |
2969 shows "(( *\<^sub>R) c) ` (rel_interior S) = rel_interior ((( *\<^sub>R) c) ` S)" |
2970 by (metis assms linear_scaleR rel_interior_convex_linear_image) |
2970 by (metis assms linear_scaleR rel_interior_convex_linear_image) |
2971 |
2971 |
2972 lemma convex_rel_open_scaleR: |
2972 lemma convex_rel_open_scaleR: |
2973 fixes S :: "'n::euclidean_space set" |
2973 fixes S :: "'n::euclidean_space set" |
2974 assumes "convex S" |
2974 assumes "convex S" |
2975 and "rel_open S" |
2975 and "rel_open S" |
2976 shows "convex ((op *\<^sub>R c) ` S) \<and> rel_open ((op *\<^sub>R c) ` S)" |
2976 shows "convex ((( *\<^sub>R) c) ` S) \<and> rel_open ((( *\<^sub>R) c) ` S)" |
2977 by (metis assms convex_scaling rel_interior_convex_scaleR rel_open_def) |
2977 by (metis assms convex_scaling rel_interior_convex_scaleR rel_open_def) |
2978 |
2978 |
2979 lemma convex_rel_open_finite_inter: |
2979 lemma convex_rel_open_finite_inter: |
2980 assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set) \<and> rel_open S" |
2980 assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set) \<and> rel_open S" |
2981 and "finite I" |
2981 and "finite I" |
3140 case True |
3140 case True |
3141 then show ?thesis |
3141 then show ?thesis |
3142 by (simp add: rel_interior_empty cone_0) |
3142 by (simp add: rel_interior_empty cone_0) |
3143 next |
3143 next |
3144 case False |
3144 case False |
3145 then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` S = S)" |
3145 then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)" |
3146 using cone_iff[of S] assms by auto |
3146 using cone_iff[of S] assms by auto |
3147 then have *: "0 \<in> ({0} \<union> rel_interior S)" |
3147 then have *: "0 \<in> ({0} \<union> rel_interior S)" |
3148 and "\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` ({0} \<union> rel_interior S) = ({0} \<union> rel_interior S)" |
3148 and "\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` ({0} \<union> rel_interior S) = ({0} \<union> rel_interior S)" |
3149 by (auto simp add: rel_interior_scaleR) |
3149 by (auto simp add: rel_interior_scaleR) |
3150 then show ?thesis |
3150 then show ?thesis |
3151 using cone_iff[of "{0} \<union> rel_interior S"] by auto |
3151 using cone_iff[of "{0} \<union> rel_interior S"] by auto |
3152 qed |
3152 qed |
3153 |
3153 |
3154 lemma rel_interior_convex_cone_aux: |
3154 lemma rel_interior_convex_cone_aux: |
3155 fixes S :: "'m::euclidean_space set" |
3155 fixes S :: "'m::euclidean_space set" |
3156 assumes "convex S" |
3156 assumes "convex S" |
3157 shows "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} \<times> S)) \<longleftrightarrow> |
3157 shows "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} \<times> S)) \<longleftrightarrow> |
3158 c > 0 \<and> x \<in> ((op *\<^sub>R c) ` (rel_interior S))" |
3158 c > 0 \<and> x \<in> ((( *\<^sub>R) c) ` (rel_interior S))" |
3159 proof (cases "S = {}") |
3159 proof (cases "S = {}") |
3160 case True |
3160 case True |
3161 then show ?thesis |
3161 then show ?thesis |
3162 by (simp add: rel_interior_empty cone_hull_empty) |
3162 by (simp add: rel_interior_empty cone_hull_empty) |
3163 next |
3163 next |
3186 then have **: "rel_interior {y. f y \<noteq> {}} = {0<..}" |
3186 then have **: "rel_interior {y. f y \<noteq> {}} = {0<..}" |
3187 using rel_interior_real_semiline by auto |
3187 using rel_interior_real_semiline by auto |
3188 { |
3188 { |
3189 fix c :: real |
3189 fix c :: real |
3190 assume "c > 0" |
3190 assume "c > 0" |
3191 then have "f c = (op *\<^sub>R c ` S)" |
3191 then have "f c = (( *\<^sub>R) c ` S)" |
3192 using f_def cone_hull_expl[of "{1 :: real} \<times> S"] by auto |
3192 using f_def cone_hull_expl[of "{1 :: real} \<times> S"] by auto |
3193 then have "rel_interior (f c) = op *\<^sub>R c ` rel_interior S" |
3193 then have "rel_interior (f c) = ( *\<^sub>R) c ` rel_interior S" |
3194 using rel_interior_convex_scaleR[of S c] assms by auto |
3194 using rel_interior_convex_scaleR[of S c] assms by auto |
3195 } |
3195 } |
3196 then show ?thesis using * ** by auto |
3196 then show ?thesis using * ** by auto |
3197 qed |
3197 qed |
3198 |
3198 |
5152 then obtain N where "open N" and "K \<subseteq> N" |
5152 then obtain N where "open N" and "K \<subseteq> N" |
5153 by blast |
5153 by blast |
5154 let ?\<C> = "insert (U \<union> V) ((\<lambda>S. N - S) ` \<F>)" |
5154 let ?\<C> = "insert (U \<union> V) ((\<lambda>S. N - S) ` \<F>)" |
5155 obtain \<D> where "\<D> \<subseteq> ?\<C>" "finite \<D>" "K \<subseteq> \<Union>\<D>" |
5155 obtain \<D> where "\<D> \<subseteq> ?\<C>" "finite \<D>" "K \<subseteq> \<Union>\<D>" |
5156 proof (rule compactE [OF \<open>compact K\<close>]) |
5156 proof (rule compactE [OF \<open>compact K\<close>]) |
5157 show "K \<subseteq> \<Union>insert (U \<union> V) (op - N ` \<F>)" |
5157 show "K \<subseteq> \<Union>insert (U \<union> V) ((-) N ` \<F>)" |
5158 using \<open>K \<subseteq> N\<close> ABeq \<open>A \<subseteq> U\<close> \<open>B \<subseteq> V\<close> by auto |
5158 using \<open>K \<subseteq> N\<close> ABeq \<open>A \<subseteq> U\<close> \<open>B \<subseteq> V\<close> by auto |
5159 show "\<And>B. B \<in> insert (U \<union> V) (op - N ` \<F>) \<Longrightarrow> open B" |
5159 show "\<And>B. B \<in> insert (U \<union> V) ((-) N ` \<F>) \<Longrightarrow> open B" |
5160 by (auto simp: \<open>open U\<close> \<open>open V\<close> open_Un \<open>open N\<close> cc compact_imp_closed open_Diff) |
5160 by (auto simp: \<open>open U\<close> \<open>open V\<close> open_Un \<open>open N\<close> cc compact_imp_closed open_Diff) |
5161 qed |
5161 qed |
5162 then have "finite(\<D> - {U \<union> V})" |
5162 then have "finite(\<D> - {U \<union> V})" |
5163 by blast |
5163 by blast |
5164 moreover have "\<D> - {U \<union> V} \<subseteq> (\<lambda>S. N - S) ` \<F>" |
5164 moreover have "\<D> - {U \<union> V} \<subseteq> (\<lambda>S. N - S) ` \<F>" |
5232 proof - |
5232 proof - |
5233 have "\<Inter>\<F> = (\<Inter>T\<in>\<F>. X \<inter> T)" |
5233 have "\<Inter>\<F> = (\<Inter>T\<in>\<F>. X \<inter> T)" |
5234 using X by blast |
5234 using X by blast |
5235 moreover have "connected (\<Inter>T\<in>\<F>. X \<inter> T)" |
5235 moreover have "connected (\<Inter>T\<in>\<F>. X \<inter> T)" |
5236 proof (rule connected_chain) |
5236 proof (rule connected_chain) |
5237 show "\<And>T. T \<in> op \<inter> X ` \<F> \<Longrightarrow> compact T \<and> connected T" |
5237 show "\<And>T. T \<in> (\<inter>) X ` \<F> \<Longrightarrow> compact T \<and> connected T" |
5238 using cc X by auto (metis inf.absorb2 inf.orderE local.linear) |
5238 using cc X by auto (metis inf.absorb2 inf.orderE local.linear) |
5239 show "\<And>S T. S \<in> op \<inter> X ` \<F> \<and> T \<in> op \<inter> X ` \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S" |
5239 show "\<And>S T. S \<in> (\<inter>) X ` \<F> \<and> T \<in> (\<inter>) X ` \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S" |
5240 using local.linear by blast |
5240 using local.linear by blast |
5241 qed |
5241 qed |
5242 ultimately show ?thesis |
5242 ultimately show ?thesis |
5243 by metis |
5243 by metis |
5244 qed |
5244 qed |
5597 next |
5597 next |
5598 obtain a where "a \<in> S" "a \<in> T" and at: "a \<in> interior T" |
5598 obtain a where "a \<in> S" "a \<in> T" and at: "a \<in> interior T" |
5599 using assms interior_subset by blast |
5599 using assms interior_subset by blast |
5600 then obtain e where "e > 0" and e: "cball a e \<subseteq> T" |
5600 then obtain e where "e > 0" and e: "cball a e \<subseteq> T" |
5601 using mem_interior_cball by blast |
5601 using mem_interior_cball by blast |
5602 have *: "x \<in> op + a ` span ((\<lambda>x. x - a) ` (S \<inter> T))" if "x \<in> S" for x |
5602 have *: "x \<in> (+) a ` span ((\<lambda>x. x - a) ` (S \<inter> T))" if "x \<in> S" for x |
5603 proof (cases "x = a") |
5603 proof (cases "x = a") |
5604 case True with that span_0 eq_add_iff image_def mem_Collect_eq show ?thesis |
5604 case True with that span_0 eq_add_iff image_def mem_Collect_eq show ?thesis |
5605 by blast |
5605 by blast |
5606 next |
5606 next |
5607 case False |
5607 case False |
5868 apply (rule ex_cong) |
5868 apply (rule ex_cong) |
5869 apply (metis (mono_tags) span_0 \<open>c = 0\<close> image_add_0 inner_zero_right mem_Collect_eq) |
5869 apply (metis (mono_tags) span_0 \<open>c = 0\<close> image_add_0 inner_zero_right mem_Collect_eq) |
5870 done |
5870 done |
5871 next |
5871 next |
5872 case False |
5872 case False |
5873 have xc_im: "x \<in> op + c ` {y. a \<bullet> y = 0}" if "a \<bullet> x = a \<bullet> c" for a x |
5873 have xc_im: "x \<in> (+) c ` {y. a \<bullet> y = 0}" if "a \<bullet> x = a \<bullet> c" for a x |
5874 proof - |
5874 proof - |
5875 have "\<exists>y. a \<bullet> y = 0 \<and> c + y = x" |
5875 have "\<exists>y. a \<bullet> y = 0 \<and> c + y = x" |
5876 by (metis that add.commute diff_add_cancel inner_commute inner_diff_left right_minus_eq) |
5876 by (metis that add.commute diff_add_cancel inner_commute inner_diff_left right_minus_eq) |
5877 then show "x \<in> op + c ` {y. a \<bullet> y = 0}" |
5877 then show "x \<in> (+) c ` {y. a \<bullet> y = 0}" |
5878 by blast |
5878 by blast |
5879 qed |
5879 qed |
5880 have 2: "span ((\<lambda>x. x - c) ` S) = {x. a \<bullet> x = 0}" |
5880 have 2: "span ((\<lambda>x. x - c) ` S) = {x. a \<bullet> x = 0}" |
5881 if "op + c ` span ((\<lambda>x. x - c) ` S) = {x. a \<bullet> x = b}" for a b |
5881 if "(+) c ` span ((\<lambda>x. x - c) ` S) = {x. a \<bullet> x = b}" for a b |
5882 proof - |
5882 proof - |
5883 have "b = a \<bullet> c" |
5883 have "b = a \<bullet> c" |
5884 using span_0 that by fastforce |
5884 using span_0 that by fastforce |
5885 with that have "op + c ` span ((\<lambda>x. x - c) ` S) = {x. a \<bullet> x = a \<bullet> c}" |
5885 with that have "(+) c ` span ((\<lambda>x. x - c) ` S) = {x. a \<bullet> x = a \<bullet> c}" |
5886 by simp |
5886 by simp |
5887 then have "span ((\<lambda>x. x - c) ` S) = (\<lambda>x. x - c) ` {x. a \<bullet> x = a \<bullet> c}" |
5887 then have "span ((\<lambda>x. x - c) ` S) = (\<lambda>x. x - c) ` {x. a \<bullet> x = a \<bullet> c}" |
5888 by (metis (no_types) image_cong translation_galois uminus_add_conv_diff) |
5888 by (metis (no_types) image_cong translation_galois uminus_add_conv_diff) |
5889 also have "... = {x. a \<bullet> x = 0}" |
5889 also have "... = {x. a \<bullet> x = 0}" |
5890 by (force simp: inner_distrib inner_diff_right |
5890 by (force simp: inner_distrib inner_diff_right |
6181 obtains a b where "(z + a) \<in> affine hull (insert z S)" |
6181 obtains a b where "(z + a) \<in> affine hull (insert z S)" |
6182 and "a \<noteq> 0" and "a \<bullet> z \<le> b" |
6182 and "a \<noteq> 0" and "a \<bullet> z \<le> b" |
6183 and "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b" |
6183 and "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b" |
6184 proof - |
6184 proof - |
6185 from separating_hyperplane_set_0_inspan [of "image (\<lambda>x. -z + x) S"] |
6185 from separating_hyperplane_set_0_inspan [of "image (\<lambda>x. -z + x) S"] |
6186 have "convex (op + (- z) ` S)" |
6186 have "convex ((+) (- z) ` S)" |
6187 by (simp add: \<open>convex S\<close>) |
6187 by (simp add: \<open>convex S\<close>) |
6188 moreover have "op + (- z) ` S \<noteq> {}" |
6188 moreover have "(+) (- z) ` S \<noteq> {}" |
6189 by (simp add: \<open>S \<noteq> {}\<close>) |
6189 by (simp add: \<open>S \<noteq> {}\<close>) |
6190 moreover have "0 \<notin> op + (- z) ` S" |
6190 moreover have "0 \<notin> (+) (- z) ` S" |
6191 using zno by auto |
6191 using zno by auto |
6192 ultimately obtain a where "a \<in> span (op + (- z) ` S)" "a \<noteq> 0" |
6192 ultimately obtain a where "a \<in> span ((+) (- z) ` S)" "a \<noteq> 0" |
6193 and a: "\<And>x. x \<in> (op + (- z) ` S) \<Longrightarrow> 0 \<le> a \<bullet> x" |
6193 and a: "\<And>x. x \<in> ((+) (- z) ` S) \<Longrightarrow> 0 \<le> a \<bullet> x" |
6194 using separating_hyperplane_set_0_inspan [of "image (\<lambda>x. -z + x) S"] |
6194 using separating_hyperplane_set_0_inspan [of "image (\<lambda>x. -z + x) S"] |
6195 by blast |
6195 by blast |
6196 then have szx: "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> z \<le> a \<bullet> x" |
6196 then have szx: "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> z \<le> a \<bullet> x" |
6197 by (metis (no_types, lifting) imageI inner_minus_right inner_right_distrib minus_add neg_le_0_iff_le neg_le_iff_le real_add_le_0_iff) |
6197 by (metis (no_types, lifting) imageI inner_minus_right inner_right_distrib minus_add neg_le_0_iff_le neg_le_iff_le real_add_le_0_iff) |
6198 show ?thesis |
6198 show ?thesis |
6199 apply (rule_tac a=a and b = "a \<bullet> z" in that, simp_all) |
6199 apply (rule_tac a=a and b = "a \<bullet> z" in that, simp_all) |
6200 using \<open>a \<in> span (op + (- z) ` S)\<close> affine_hull_insert_span_gen apply blast |
6200 using \<open>a \<in> span ((+) (- z) ` S)\<close> affine_hull_insert_span_gen apply blast |
6201 apply (simp_all add: \<open>a \<noteq> 0\<close> szx) |
6201 apply (simp_all add: \<open>a \<noteq> 0\<close> szx) |
6202 done |
6202 done |
6203 qed |
6203 qed |
6204 |
6204 |
6205 proposition supporting_hyperplane_rel_boundary: |
6205 proposition supporting_hyperplane_rel_boundary: |
6214 and ageb: "\<And>u. u \<in> (rel_interior S) \<Longrightarrow> a \<bullet> u \<ge> b" |
6214 and ageb: "\<And>u. u \<in> (rel_interior S) \<Longrightarrow> a \<bullet> u \<ge> b" |
6215 using separating_hyperplane_set_point_inaff [of "rel_interior S" x] assms |
6215 using separating_hyperplane_set_point_inaff [of "rel_interior S" x] assms |
6216 by (auto simp: rel_interior_eq_empty convex_rel_interior) |
6216 by (auto simp: rel_interior_eq_empty convex_rel_interior) |
6217 have le_ay: "a \<bullet> x \<le> a \<bullet> y" if "y \<in> S" for y |
6217 have le_ay: "a \<bullet> x \<le> a \<bullet> y" if "y \<in> S" for y |
6218 proof - |
6218 proof - |
6219 have con: "continuous_on (closure (rel_interior S)) (op \<bullet> a)" |
6219 have con: "continuous_on (closure (rel_interior S)) ((\<bullet>) a)" |
6220 by (rule continuous_intros continuous_on_subset | blast)+ |
6220 by (rule continuous_intros continuous_on_subset | blast)+ |
6221 have y: "y \<in> closure (rel_interior S)" |
6221 have y: "y \<in> closure (rel_interior S)" |
6222 using \<open>convex S\<close> closure_def convex_closure_rel_interior \<open>y \<in> S\<close> |
6222 using \<open>convex S\<close> closure_def convex_closure_rel_interior \<open>y \<in> S\<close> |
6223 by fastforce |
6223 by fastforce |
6224 show ?thesis |
6224 show ?thesis |
6699 next |
6699 next |
6700 case False |
6700 case False |
6701 obtain c where "c \<in> S" and c: "a \<bullet> c = b" |
6701 obtain c where "c \<in> S" and c: "a \<bullet> c = b" |
6702 using assms by force |
6702 using assms by force |
6703 with affine_diffs_subspace [OF \<open>affine S\<close>] |
6703 with affine_diffs_subspace [OF \<open>affine S\<close>] |
6704 have "subspace (op + (- c) ` S)" by blast |
6704 have "subspace ((+) (- c) ` S)" by blast |
6705 then have aff: "affine (op + (- c) ` S)" |
6705 then have aff: "affine ((+) (- c) ` S)" |
6706 by (simp add: subspace_imp_affine) |
6706 by (simp add: subspace_imp_affine) |
6707 have 0: "0 \<in> op + (- c) ` S" |
6707 have 0: "0 \<in> (+) (- c) ` S" |
6708 by (simp add: \<open>c \<in> S\<close>) |
6708 by (simp add: \<open>c \<in> S\<close>) |
6709 obtain d where "d \<in> S" and "a \<bullet> d \<noteq> b" and dc: "d-c \<in> op + (- c) ` S" |
6709 obtain d where "d \<in> S" and "a \<bullet> d \<noteq> b" and dc: "d-c \<in> (+) (- c) ` S" |
6710 using assms by auto |
6710 using assms by auto |
6711 then have adc: "a \<bullet> (d - c) \<noteq> 0" |
6711 then have adc: "a \<bullet> (d - c) \<noteq> 0" |
6712 by (simp add: c inner_diff_right) |
6712 by (simp add: c inner_diff_right) |
6713 let ?U = "op + (c+c) ` {x + y |x y. x \<in> op + (- c) ` S \<and> a \<bullet> y = 0}" |
6713 let ?U = "(+) (c+c) ` {x + y |x y. x \<in> (+) (- c) ` S \<and> a \<bullet> y = 0}" |
6714 have "u + v \<in> op + (c + c) ` {x + v |x v. x \<in> op + (- c) ` S \<and> a \<bullet> v = 0}" |
6714 have "u + v \<in> (+) (c + c) ` {x + v |x v. x \<in> (+) (- c) ` S \<and> a \<bullet> v = 0}" |
6715 if "u \<in> S" "b = a \<bullet> v" for u v |
6715 if "u \<in> S" "b = a \<bullet> v" for u v |
6716 apply (rule_tac x="u+v-c-c" in image_eqI) |
6716 apply (rule_tac x="u+v-c-c" in image_eqI) |
6717 apply (simp_all add: algebra_simps) |
6717 apply (simp_all add: algebra_simps) |
6718 apply (rule_tac x="u-c" in exI) |
6718 apply (rule_tac x="u-c" in exI) |
6719 apply (rule_tac x="v-c" in exI) |
6719 apply (rule_tac x="v-c" in exI) |
6722 moreover have "\<lbrakk>a \<bullet> v = 0; u \<in> S\<rbrakk> |
6722 moreover have "\<lbrakk>a \<bullet> v = 0; u \<in> S\<rbrakk> |
6723 \<Longrightarrow> \<exists>x ya. v + (u + c) = x + ya \<and> x \<in> S \<and> a \<bullet> ya = b" for v u |
6723 \<Longrightarrow> \<exists>x ya. v + (u + c) = x + ya \<and> x \<in> S \<and> a \<bullet> ya = b" for v u |
6724 by (metis add.left_commute c inner_right_distrib pth_d) |
6724 by (metis add.left_commute c inner_right_distrib pth_d) |
6725 ultimately have "{x + y |x y. x \<in> S \<and> a \<bullet> y = b} = ?U" |
6725 ultimately have "{x + y |x y. x \<in> S \<and> a \<bullet> y = b} = ?U" |
6726 by (fastforce simp: algebra_simps) |
6726 by (fastforce simp: algebra_simps) |
6727 also have "... = op + (c+c) ` UNIV" |
6727 also have "... = (+) (c+c) ` UNIV" |
6728 by (simp add: affine_hyperplane_sums_eq_UNIV_0 [OF aff 0 dc adc]) |
6728 by (simp add: affine_hyperplane_sums_eq_UNIV_0 [OF aff 0 dc adc]) |
6729 also have "... = UNIV" |
6729 also have "... = UNIV" |
6730 by (simp add: translation_UNIV) |
6730 by (simp add: translation_UNIV) |
6731 finally show ?thesis . |
6731 finally show ?thesis . |
6732 qed |
6732 qed |
6854 and "affine T" |
6854 and "affine T" |
6855 and "S \<inter> T \<noteq> {}" |
6855 and "S \<inter> T \<noteq> {}" |
6856 shows "aff_dim {x + y| x y. x \<in> S \<and> y \<in> T} = (aff_dim S + aff_dim T) - aff_dim(S \<inter> T)" |
6856 shows "aff_dim {x + y| x y. x \<in> S \<and> y \<in> T} = (aff_dim S + aff_dim T) - aff_dim(S \<inter> T)" |
6857 proof - |
6857 proof - |
6858 obtain a where a: "a \<in> S" "a \<in> T" using assms by force |
6858 obtain a where a: "a \<in> S" "a \<in> T" using assms by force |
6859 have aff: "affine (op+ (-a) ` S)" "affine (op+ (-a) ` T)" |
6859 have aff: "affine ((+) (-a) ` S)" "affine ((+) (-a) ` T)" |
6860 using assms by (auto simp: affine_translation [symmetric]) |
6860 using assms by (auto simp: affine_translation [symmetric]) |
6861 have zero: "0 \<in> (op+ (-a) ` S)" "0 \<in> (op+ (-a) ` T)" |
6861 have zero: "0 \<in> ((+) (-a) ` S)" "0 \<in> ((+) (-a) ` T)" |
6862 using a assms by auto |
6862 using a assms by auto |
6863 have [simp]: "{x + y |x y. x \<in> op + (- a) ` S \<and> y \<in> op + (- a) ` T} = |
6863 have [simp]: "{x + y |x y. x \<in> (+) (- a) ` S \<and> y \<in> (+) (- a) ` T} = |
6864 op + (- 2 *\<^sub>R a) ` {x + y| x y. x \<in> S \<and> y \<in> T}" |
6864 (+) (- 2 *\<^sub>R a) ` {x + y| x y. x \<in> S \<and> y \<in> T}" |
6865 by (force simp: algebra_simps scaleR_2) |
6865 by (force simp: algebra_simps scaleR_2) |
6866 have [simp]: "op + (- a) ` S \<inter> op + (- a) ` T = op + (- a) ` (S \<inter> T)" |
6866 have [simp]: "(+) (- a) ` S \<inter> (+) (- a) ` T = (+) (- a) ` (S \<inter> T)" |
6867 by auto |
6867 by auto |
6868 show ?thesis |
6868 show ?thesis |
6869 using aff_dim_sums_Int_0 [OF aff zero] |
6869 using aff_dim_sums_Int_0 [OF aff zero] |
6870 by (auto simp: aff_dim_translation_eq) |
6870 by (auto simp: aff_dim_translation_eq) |
6871 qed |
6871 qed |
7455 then show ?thesis |
7455 then show ?thesis |
7456 by (metis Diff_triv affine_hull_eq \<open>affine S\<close> closure_same_affine_hull closure_subset hull_subset subset_antisym) |
7456 by (metis Diff_triv affine_hull_eq \<open>affine S\<close> closure_same_affine_hull closure_subset hull_subset subset_antisym) |
7457 next |
7457 next |
7458 case False |
7458 case False |
7459 then obtain z where z: "z \<in> S \<inter> T" by blast |
7459 then obtain z where z: "z \<in> S \<inter> T" by blast |
7460 then have "subspace (op + (- z) ` S)" |
7460 then have "subspace ((+) (- z) ` S)" |
7461 by (meson IntD1 affine_diffs_subspace \<open>affine S\<close>) |
7461 by (meson IntD1 affine_diffs_subspace \<open>affine S\<close>) |
7462 moreover have "int (dim (op + (- z) ` T)) < int (dim (op + (- z) ` S))" |
7462 moreover have "int (dim ((+) (- z) ` T)) < int (dim ((+) (- z) ` S))" |
7463 using z less by (simp add: aff_dim_eq_dim [symmetric] hull_inc) |
7463 using z less by (simp add: aff_dim_eq_dim [symmetric] hull_inc) |
7464 ultimately have "closure((op + (- z) ` S) - (op + (- z) ` T)) = (op + (- z) ` S)" |
7464 ultimately have "closure(((+) (- z) ` S) - ((+) (- z) ` T)) = ((+) (- z) ` S)" |
7465 by (simp add: dense_complement_subspace) |
7465 by (simp add: dense_complement_subspace) |
7466 then show ?thesis |
7466 then show ?thesis |
7467 by (metis closure_translation translation_diff translation_invert) |
7467 by (metis closure_translation translation_diff translation_invert) |
7468 qed |
7468 qed |
7469 |
7469 |
7533 next |
7533 next |
7534 case False |
7534 case False |
7535 then obtain z where "z \<in> S" and z: "a \<bullet> z = b" |
7535 then obtain z where "z \<in> S" and z: "a \<bullet> z = b" |
7536 using assms by auto |
7536 using assms by auto |
7537 with affine_diffs_subspace [OF \<open>affine S\<close>] |
7537 with affine_diffs_subspace [OF \<open>affine S\<close>] |
7538 have sub: "subspace (op + (- z) ` S)" by blast |
7538 have sub: "subspace ((+) (- z) ` S)" by blast |
7539 then have aff: "affine (op + (- z) ` S)" and span: "span (op + (- z) ` S) = (op + (- z) ` S)" |
7539 then have aff: "affine ((+) (- z) ` S)" and span: "span ((+) (- z) ` S) = ((+) (- z) ` S)" |
7540 by (auto simp: subspace_imp_affine) |
7540 by (auto simp: subspace_imp_affine) |
7541 obtain a' a'' where a': "a' \<in> span (op + (- z) ` S)" and a: "a = a' + a''" |
7541 obtain a' a'' where a': "a' \<in> span ((+) (- z) ` S)" and a: "a = a' + a''" |
7542 and "\<And>w. w \<in> span (op + (- z) ` S) \<Longrightarrow> orthogonal a'' w" |
7542 and "\<And>w. w \<in> span ((+) (- z) ` S) \<Longrightarrow> orthogonal a'' w" |
7543 using orthogonal_subspace_decomp_exists [of "op + (- z) ` S" "a"] by metis |
7543 using orthogonal_subspace_decomp_exists [of "(+) (- z) ` S" "a"] by metis |
7544 then have "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> (w-z) = 0" |
7544 then have "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> (w-z) = 0" |
7545 by (simp add: imageI orthogonal_def span) |
7545 by (simp add: imageI orthogonal_def span) |
7546 then have a'': "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> w = (a - a') \<bullet> z" |
7546 then have a'': "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> w = (a - a') \<bullet> z" |
7547 by (simp add: a inner_diff_right) |
7547 by (simp add: a inner_diff_right) |
7548 then have ba'': "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> w = b - a' \<bullet> z" |
7548 then have ba'': "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> w = b - a' \<bullet> z" |
7549 by (simp add: inner_diff_left z) |
7549 by (simp add: inner_diff_left z) |
7550 have "\<And>w. w \<in> op + (- z) ` S \<Longrightarrow> (w + a') \<in> op + (- z) ` S" |
7550 have "\<And>w. w \<in> (+) (- z) ` S \<Longrightarrow> (w + a') \<in> (+) (- z) ` S" |
7551 by (metis subspace_add a' span_eq sub) |
7551 by (metis subspace_add a' span_eq sub) |
7552 then have Sclo: "\<And>w. w \<in> S \<Longrightarrow> (w + a') \<in> S" |
7552 then have Sclo: "\<And>w. w \<in> S \<Longrightarrow> (w + a') \<in> S" |
7553 by fastforce |
7553 by fastforce |
7554 show ?thesis |
7554 show ?thesis |
7555 proof (cases "a' = 0") |
7555 proof (cases "a' = 0") |
7703 case True with assms show ?thesis |
7703 case True with assms show ?thesis |
7704 by (metis aff_dim_empty affine_empty bot.extremum that eq_iff) |
7704 by (metis aff_dim_empty affine_empty bot.extremum that eq_iff) |
7705 next |
7705 next |
7706 case False |
7706 case False |
7707 with assms obtain a where "a \<in> S" "0 \<le> d" by auto |
7707 with assms obtain a where "a \<in> S" "0 \<le> d" by auto |
7708 with assms have ss: "subspace (op + (- a) ` S)" |
7708 with assms have ss: "subspace ((+) (- a) ` S)" |
7709 by (simp add: affine_diffs_subspace) |
7709 by (simp add: affine_diffs_subspace) |
7710 have "nat d \<le> dim (op + (- a) ` S)" |
7710 have "nat d \<le> dim ((+) (- a) ` S)" |
7711 by (metis aff_dim_subspace aff_dim_translation_eq dle nat_int nat_mono ss) |
7711 by (metis aff_dim_subspace aff_dim_translation_eq dle nat_int nat_mono ss) |
7712 then obtain T where "subspace T" and Tsb: "T \<subseteq> span (op + (- a) ` S)" |
7712 then obtain T where "subspace T" and Tsb: "T \<subseteq> span ((+) (- a) ` S)" |
7713 and Tdim: "dim T = nat d" |
7713 and Tdim: "dim T = nat d" |
7714 using choose_subspace_of_subspace [of "nat d" "op + (- a) ` S"] by blast |
7714 using choose_subspace_of_subspace [of "nat d" "(+) (- a) ` S"] by blast |
7715 then have "affine T" |
7715 then have "affine T" |
7716 using subspace_affine by blast |
7716 using subspace_affine by blast |
7717 then have "affine (op + a ` T)" |
7717 then have "affine ((+) a ` T)" |
7718 by (metis affine_hull_eq affine_hull_translation) |
7718 by (metis affine_hull_eq affine_hull_translation) |
7719 moreover have "op + a ` T \<subseteq> S" |
7719 moreover have "(+) a ` T \<subseteq> S" |
7720 proof - |
7720 proof - |
7721 have "T \<subseteq> op + (- a) ` S" |
7721 have "T \<subseteq> (+) (- a) ` S" |
7722 by (metis (no_types) span_eq Tsb ss) |
7722 by (metis (no_types) span_eq Tsb ss) |
7723 then show "op + a ` T \<subseteq> S" |
7723 then show "(+) a ` T \<subseteq> S" |
7724 using add_ac by auto |
7724 using add_ac by auto |
7725 qed |
7725 qed |
7726 moreover have "aff_dim (op + a ` T) = d" |
7726 moreover have "aff_dim ((+) a ` T) = d" |
7727 by (simp add: aff_dim_subspace Tdim \<open>0 \<le> d\<close> \<open>subspace T\<close> aff_dim_translation_eq) |
7727 by (simp add: aff_dim_subspace Tdim \<open>0 \<le> d\<close> \<open>subspace T\<close> aff_dim_translation_eq) |
7728 ultimately show ?thesis |
7728 ultimately show ?thesis |
7729 by (rule that) |
7729 by (rule that) |
7730 qed |
7730 qed |
7731 |
7731 |