changeset 54465 | 2f7867850cc3 |
parent 54263 | c4159fe6fa46 |
child 54775 | 2d3df8633dad |
54464:b0074321bf14 | 54465:2f7867850cc3 |
---|---|
275 lemma closure_injective_linear_image: |
275 lemma closure_injective_linear_image: |
276 fixes f :: "'n::euclidean_space \<Rightarrow> 'n::euclidean_space" |
276 fixes f :: "'n::euclidean_space \<Rightarrow> 'n::euclidean_space" |
277 assumes "linear f" "inj f" |
277 assumes "linear f" "inj f" |
278 shows "f ` (closure S) = closure (f ` S)" |
278 shows "f ` (closure S) = closure (f ` S)" |
279 proof - |
279 proof - |
280 obtain f' where f'_def: "linear f' \<and> f \<circ> f' = id \<and> f' \<circ> f = id" |
280 obtain f' where f': "linear f' \<and> f \<circ> f' = id \<and> f' \<circ> f = id" |
281 using assms linear_injective_isomorphism[of f] isomorphism_expand by auto |
281 using assms linear_injective_isomorphism[of f] isomorphism_expand by auto |
282 then have "f' ` closure (f ` S) \<le> closure (S)" |
282 then have "f' ` closure (f ` S) \<le> closure (S)" |
283 using closure_linear_image[of f' "f ` S"] image_compose[of f' f] by auto |
283 using closure_linear_image[of f' "f ` S"] image_compose[of f' f] by auto |
284 then have "f ` f' ` closure (f ` S) \<le> f ` closure S" by auto |
284 then have "f ` f' ` closure (f ` S) \<le> f ` closure S" by auto |
285 then have "closure (f ` S) \<le> f ` closure S" |
285 then have "closure (f ` S) \<le> f ` closure S" |
286 using image_compose[of f f' "closure (f ` S)"] f'_def by auto |
286 using image_compose[of f f' "closure (f ` S)"] f' by auto |
287 then show ?thesis using closure_linear_image[of f S] assms by auto |
287 then show ?thesis using closure_linear_image[of f S] assms by auto |
288 qed |
288 qed |
289 |
289 |
290 lemma closure_scaleR: |
290 lemma closure_scaleR: |
291 fixes S :: "'a::real_normed_vector set" |
291 fixes S :: "'a::real_normed_vector set" |
302 unfolding linear_iff by (simp add: algebra_simps) |
302 unfolding linear_iff by (simp add: algebra_simps) |
303 |
303 |
304 lemma snd_linear: "linear snd" |
304 lemma snd_linear: "linear snd" |
305 unfolding linear_iff by (simp add: algebra_simps) |
305 unfolding linear_iff by (simp add: algebra_simps) |
306 |
306 |
307 lemma fst_snd_linear: "linear (%(x,y). x + y)" |
307 lemma fst_snd_linear: "linear (\<lambda>(x,y). x + y)" |
308 unfolding linear_iff by (simp add: algebra_simps) |
308 unfolding linear_iff by (simp add: algebra_simps) |
309 |
309 |
310 lemma scaleR_2: |
310 lemma scaleR_2: |
311 fixes x :: "'a::real_vector" |
311 fixes x :: "'a::real_vector" |
312 shows "scaleR 2 x = x + x" |
312 shows "scaleR 2 x = x + x" |
936 using subspace_imp_affine[of S] subspace_0 by auto |
936 using subspace_imp_affine[of S] subspace_0 by auto |
937 { |
937 { |
938 assume assm: "affine S \<and> 0 \<in> S" |
938 assume assm: "affine S \<and> 0 \<in> S" |
939 { |
939 { |
940 fix c :: real |
940 fix c :: real |
941 fix x assume x_def: "x \<in> S" |
941 fix x |
942 assume x: "x \<in> S" |
|
942 have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto |
943 have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto |
943 moreover |
944 moreover |
944 have "(1 - c) *\<^sub>R 0 + c *\<^sub>R x \<in> S" |
945 have "(1 - c) *\<^sub>R 0 + c *\<^sub>R x \<in> S" |
945 using affine_alt[of S] assm x_def by auto |
946 using affine_alt[of S] assm x by auto |
946 ultimately have "c *\<^sub>R x \<in> S" by auto |
947 ultimately have "c *\<^sub>R x \<in> S" by auto |
947 } |
948 } |
948 then have h1: "\<forall>c. \<forall>x \<in> S. c *\<^sub>R x \<in> S" by auto |
949 then have h1: "\<forall>c. \<forall>x \<in> S. c *\<^sub>R x \<in> S" by auto |
949 |
950 |
950 { |
951 { |
951 fix x y |
952 fix x y |
952 assume xy_def: "x \<in> S" "y \<in> S" |
953 assume xy: "x \<in> S" "y \<in> S" |
953 def u == "(1 :: real)/2" |
954 def u == "(1 :: real)/2" |
954 have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)" |
955 have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)" |
955 by auto |
956 by auto |
956 moreover |
957 moreover |
957 have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y" |
958 have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y" |
958 by (simp add: algebra_simps) |
959 by (simp add: algebra_simps) |
959 moreover |
960 moreover |
960 have "(1-u) *\<^sub>R x + u *\<^sub>R y \<in> S" |
961 have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> S" |
961 using affine_alt[of S] assm xy_def by auto |
962 using affine_alt[of S] assm xy by auto |
962 ultimately |
963 ultimately |
963 have "(1/2) *\<^sub>R (x+y) \<in> S" |
964 have "(1/2) *\<^sub>R (x+y) \<in> S" |
964 using u_def by auto |
965 using u_def by auto |
965 moreover |
966 moreover |
966 have "(x+y) = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))" |
967 have "x + y = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))" |
967 by auto |
968 by auto |
968 ultimately |
969 ultimately |
969 have "(x+y) \<in> S" |
970 have "x + y \<in> S" |
970 using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto |
971 using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto |
971 } |
972 } |
972 then have "\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S" |
973 then have "\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S" |
973 by auto |
974 by auto |
974 then have "subspace S" |
975 then have "subspace S" |
988 using assms exI[of "(\<lambda>x. x\<in>S \<and> -a+x = 0)" a] by auto |
989 using assms exI[of "(\<lambda>x. x\<in>S \<and> -a+x = 0)" a] by auto |
989 ultimately show ?thesis using subspace_affine by auto |
990 ultimately show ?thesis using subspace_affine by auto |
990 qed |
991 qed |
991 |
992 |
992 lemma parallel_subspace_explicit: |
993 lemma parallel_subspace_explicit: |
993 assumes "affine S" "a : S" |
994 assumes "affine S" |
994 assumes "L \<equiv> {y. \<exists>x \<in> S. (-a)+x=y}" |
995 and "a \<in> S" |
995 shows "subspace L & affine_parallel S L" |
996 assumes "L \<equiv> {y. \<exists>x \<in> S. (-a) + x = y}" |
997 shows "subspace L \<and> affine_parallel S L" |
|
996 proof - |
998 proof - |
997 from assms have "L = plus (- a) ` S" by auto |
999 from assms have "L = plus (- a) ` S" by auto |
998 then have par: "affine_parallel S L" |
1000 then have par: "affine_parallel S L" |
999 unfolding affine_parallel_def .. |
1001 unfolding affine_parallel_def .. |
1000 then have "affine L" using assms parallel_is_affine by auto |
1002 then have "affine L" using assms parallel_is_affine by auto |
1001 moreover have "0 \<in> L" |
1003 moreover have "0 \<in> L" |
1002 using assms by auto |
1004 using assms by auto |
1003 ultimately show ?thesis |
1005 ultimately show ?thesis |
1004 using subspace_affine par by auto |
1006 using subspace_affine par by auto |
1008 assumes "subspace A" |
1010 assumes "subspace A" |
1009 and "subspace B" |
1011 and "subspace B" |
1010 and "affine_parallel A B" |
1012 and "affine_parallel A B" |
1011 shows "A \<supseteq> B" |
1013 shows "A \<supseteq> B" |
1012 proof - |
1014 proof - |
1013 from assms obtain a where a_def: "\<forall>x. x \<in> A \<longleftrightarrow> a + x \<in> B" |
1015 from assms obtain a where a: "\<forall>x. x \<in> A \<longleftrightarrow> a + x \<in> B" |
1014 using affine_parallel_expl[of A B] by auto |
1016 using affine_parallel_expl[of A B] by auto |
1015 then have "-a \<in> A" |
1017 then have "-a \<in> A" |
1016 using assms subspace_0[of B] by auto |
1018 using assms subspace_0[of B] by auto |
1017 then have "a \<in> A" |
1019 then have "a \<in> A" |
1018 using assms subspace_neg[of A "-a"] by auto |
1020 using assms subspace_neg[of A "-a"] by auto |
1019 then show ?thesis |
1021 then show ?thesis |
1020 using assms a_def unfolding subspace_def by auto |
1022 using assms a unfolding subspace_def by auto |
1021 qed |
1023 qed |
1022 |
1024 |
1023 lemma parallel_subspace: |
1025 lemma parallel_subspace: |
1024 assumes "subspace A" |
1026 assumes "subspace A" |
1025 and "subspace B" |
1027 and "subspace B" |
1114 fix x |
1116 fix x |
1115 assume "x \<in> S" |
1117 assume "x \<in> S" |
1116 then have "x \<in> (op *\<^sub>R c) ` S" |
1118 then have "x \<in> (op *\<^sub>R c) ` S" |
1117 unfolding image_def |
1119 unfolding image_def |
1118 using `cone S` `c>0` mem_cone[of S x "1/c"] |
1120 using `cone S` `c>0` mem_cone[of S x "1/c"] |
1119 exI[of "(%t. t:S & x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"] |
1121 exI[of "(\<lambda>t. t \<in> S \<and> x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"] |
1120 by auto |
1122 by auto |
1121 } |
1123 } |
1122 moreover |
1124 moreover |
1123 { |
1125 { |
1124 fix x |
1126 fix x |
1167 (is "?lhs = ?rhs") |
1169 (is "?lhs = ?rhs") |
1168 proof - |
1170 proof - |
1169 { |
1171 { |
1170 fix x |
1172 fix x |
1171 assume "x \<in> ?rhs" |
1173 assume "x \<in> ?rhs" |
1172 then obtain cx :: real and xx where x_def: "x = cx *\<^sub>R xx" "cx \<ge> 0" "xx \<in> S" |
1174 then obtain cx :: real and xx where x: "x = cx *\<^sub>R xx" "cx \<ge> 0" "xx \<in> S" |
1173 by auto |
1175 by auto |
1174 fix c :: real |
1176 fix c :: real |
1175 assume c: "c \<ge> 0" |
1177 assume c: "c \<ge> 0" |
1176 then have "c *\<^sub>R x = (c * cx) *\<^sub>R xx" |
1178 then have "c *\<^sub>R x = (c * cx) *\<^sub>R xx" |
1177 using x_def by (simp add: algebra_simps) |
1179 using x by (simp add: algebra_simps) |
1178 moreover |
1180 moreover |
1179 have "c * cx \<ge> 0" |
1181 have "c * cx \<ge> 0" |
1180 using c x_def using mult_nonneg_nonneg by auto |
1182 using c x using mult_nonneg_nonneg by auto |
1181 ultimately |
1183 ultimately |
1182 have "c *\<^sub>R x \<in> ?rhs" using x_def by auto |
1184 have "c *\<^sub>R x \<in> ?rhs" using x by auto |
1183 } |
1185 } |
1184 then have "cone ?rhs" |
1186 then have "cone ?rhs" |
1185 unfolding cone_def by auto |
1187 unfolding cone_def by auto |
1186 then have "?rhs \<in> Collect cone" |
1188 then have "?rhs \<in> Collect cone" |
1187 unfolding mem_Collect_eq by auto |
1189 unfolding mem_Collect_eq by auto |
1200 using `?rhs \<in> Collect cone` hull_minimal[of S "?rhs" "cone"] by auto |
1202 using `?rhs \<in> Collect cone` hull_minimal[of S "?rhs" "cone"] by auto |
1201 moreover |
1203 moreover |
1202 { |
1204 { |
1203 fix x |
1205 fix x |
1204 assume "x \<in> ?rhs" |
1206 assume "x \<in> ?rhs" |
1205 then obtain cx :: real and xx where x_def: "x = cx *\<^sub>R xx" "cx \<ge> 0" "xx \<in> S" |
1207 then obtain cx :: real and xx where x: "x = cx *\<^sub>R xx" "cx \<ge> 0" "xx \<in> S" |
1206 by auto |
1208 by auto |
1207 then have "xx \<in> cone hull S" |
1209 then have "xx \<in> cone hull S" |
1208 using hull_subset[of S] by auto |
1210 using hull_subset[of S] by auto |
1209 then have "x \<in> ?lhs" |
1211 then have "x \<in> ?lhs" |
1210 using x_def cone_cone_hull[of S] cone_def[of "cone hull S"] by auto |
1212 using x cone_cone_hull[of S] cone_def[of "cone hull S"] by auto |
1211 } |
1213 } |
1212 ultimately show ?thesis by auto |
1214 ultimately show ?thesis by auto |
1213 qed |
1215 qed |
1214 |
1216 |
1215 lemma cone_closure: |
1217 lemma cone_closure: |
2396 using translation_assoc[of "-a" a] by auto |
2398 using translation_assoc[of "-a" a] by auto |
2397 ultimately have "(\<lambda>x. -a + x) ` (affine hull ((\<lambda>x. a + x) ` S)) >= (affine hull S)" |
2399 ultimately have "(\<lambda>x. -a + x) ` (affine hull ((\<lambda>x. a + x) ` S)) >= (affine hull S)" |
2398 by (metis hull_minimal) |
2400 by (metis hull_minimal) |
2399 then have "affine hull ((\<lambda>x. a + x) ` S) >= (\<lambda>x. a + x) ` (affine hull S)" |
2401 then have "affine hull ((\<lambda>x. a + x) ` S) >= (\<lambda>x. a + x) ` (affine hull S)" |
2400 by auto |
2402 by auto |
2401 from this show ?thesis using h1 by auto |
2403 then show ?thesis using h1 by auto |
2402 qed |
2404 qed |
2403 |
2405 |
2404 lemma affine_dependent_translation: |
2406 lemma affine_dependent_translation: |
2405 assumes "affine_dependent S" |
2407 assumes "affine_dependent S" |
2406 shows "affine_dependent ((\<lambda>x. a + x) ` S)" |
2408 shows "affine_dependent ((\<lambda>x. a + x) ` S)" |
2407 proof - |
2409 proof - |
2408 obtain x where x_def: "x \<in> S \<and> x \<in> affine hull (S - {x})" |
2410 obtain x where x: "x \<in> S \<and> x \<in> affine hull (S - {x})" |
2409 using assms affine_dependent_def by auto |
2411 using assms affine_dependent_def by auto |
2410 have "op + a ` (S - {x}) = op + a ` S - {a + x}" |
2412 have "op + a ` (S - {x}) = op + a ` S - {a + x}" |
2411 by auto |
2413 by auto |
2412 then have "a + x \<in> affine hull ((\<lambda>x. a + x) ` S - {a + x})" |
2414 then have "a + x \<in> affine hull ((\<lambda>x. a + x) ` S - {a + x})" |
2413 using affine_hull_translation[of a "S - {x}"] x_def by auto |
2415 using affine_hull_translation[of a "S - {x}"] x by auto |
2414 moreover have "a + x \<in> (\<lambda>x. a + x) ` S" |
2416 moreover have "a + x \<in> (\<lambda>x. a + x) ` S" |
2415 using x_def by auto |
2417 using x by auto |
2416 ultimately show ?thesis |
2418 ultimately show ?thesis |
2417 unfolding affine_dependent_def by auto |
2419 unfolding affine_dependent_def by auto |
2418 qed |
2420 qed |
2419 |
2421 |
2420 lemma affine_dependent_translation_eq: |
2422 lemma affine_dependent_translation_eq: |
2421 "affine_dependent S <-> affine_dependent ((\<lambda>x. a + x) ` S)" |
2423 "affine_dependent S \<longleftrightarrow> affine_dependent ((\<lambda>x. a + x) ` S)" |
2422 proof - |
2424 proof - |
2423 { |
2425 { |
2424 assume "affine_dependent ((\<lambda>x. a + x) ` S)" |
2426 assume "affine_dependent ((\<lambda>x. a + x) ` S)" |
2425 then have "affine_dependent S" |
2427 then have "affine_dependent S" |
2426 using affine_dependent_translation[of "((\<lambda>x. a + x) ` S)" "-a"] translation_assoc[of "-a" a] |
2428 using affine_dependent_translation[of "((\<lambda>x. a + x) ` S)" "-a"] translation_assoc[of "-a" a] |
2432 |
2434 |
2433 lemma affine_hull_0_dependent: |
2435 lemma affine_hull_0_dependent: |
2434 assumes "0 \<in> affine hull S" |
2436 assumes "0 \<in> affine hull S" |
2435 shows "dependent S" |
2437 shows "dependent S" |
2436 proof - |
2438 proof - |
2437 obtain s u where s_u_def: "finite s \<and> s \<noteq> {} \<and> s \<subseteq> S \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0" |
2439 obtain s u where s_u: "finite s \<and> s \<noteq> {} \<and> s \<subseteq> S \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0" |
2438 using assms affine_hull_explicit[of S] by auto |
2440 using assms affine_hull_explicit[of S] by auto |
2439 then have "\<exists>v\<in>s. u v \<noteq> 0" |
2441 then have "\<exists>v\<in>s. u v \<noteq> 0" |
2440 using setsum_not_0[of "u" "s"] by auto |
2442 using setsum_not_0[of "u" "s"] by auto |
2441 then have "finite s \<and> s \<subseteq> S \<and> (\<exists>v\<in>s. u v \<noteq> 0 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0)" |
2443 then have "finite s \<and> s \<subseteq> S \<and> (\<exists>v\<in>s. u v \<noteq> 0 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0)" |
2442 using s_u_def by auto |
2444 using s_u by auto |
2443 then show ?thesis |
2445 then show ?thesis |
2444 unfolding dependent_explicit[of S] by auto |
2446 unfolding dependent_explicit[of S] by auto |
2445 qed |
2447 qed |
2446 |
2448 |
2447 lemma affine_dependent_imp_dependent2: |
2449 lemma affine_dependent_imp_dependent2: |
2448 assumes "affine_dependent (insert 0 S)" |
2450 assumes "affine_dependent (insert 0 S)" |
2449 shows "dependent S" |
2451 shows "dependent S" |
2450 proof - |
2452 proof - |
2451 obtain x where x_def: "x \<in> insert 0 S \<and> x \<in> affine hull (insert 0 S - {x})" |
2453 obtain x where x: "x \<in> insert 0 S \<and> x \<in> affine hull (insert 0 S - {x})" |
2452 using affine_dependent_def[of "(insert 0 S)"] assms by blast |
2454 using affine_dependent_def[of "(insert 0 S)"] assms by blast |
2453 then have "x \<in> span (insert 0 S - {x})" |
2455 then have "x \<in> span (insert 0 S - {x})" |
2454 using affine_hull_subset_span by auto |
2456 using affine_hull_subset_span by auto |
2455 moreover have "span (insert 0 S - {x}) = span (S - {x})" |
2457 moreover have "span (insert 0 S - {x}) = span (S - {x})" |
2456 using insert_Diff_if[of "0" S "{x}"] span_insert_0[of "S-{x}"] by auto |
2458 using insert_Diff_if[of "0" S "{x}"] span_insert_0[of "S-{x}"] by auto |
2457 ultimately have "x \<in> span (S - {x})" by auto |
2459 ultimately have "x \<in> span (S - {x})" by auto |
2458 then have "x \<noteq> 0 \<Longrightarrow> dependent S" |
2460 then have "x \<noteq> 0 \<Longrightarrow> dependent S" |
2459 using x_def dependent_def by auto |
2461 using x dependent_def by auto |
2460 moreover |
2462 moreover |
2461 { |
2463 { |
2462 assume "x = 0" |
2464 assume "x = 0" |
2463 then have "0 \<in> affine hull S" |
2465 then have "0 \<in> affine hull S" |
2464 using x_def hull_mono[of "S - {0}" S] by auto |
2466 using x hull_mono[of "S - {0}" S] by auto |
2465 then have "dependent S" |
2467 then have "dependent S" |
2466 using affine_hull_0_dependent by auto |
2468 using affine_hull_0_dependent by auto |
2467 } |
2469 } |
2468 ultimately show ?thesis by auto |
2470 ultimately show ?thesis by auto |
2469 qed |
2471 qed |
2547 lemma extend_to_affine_basis: |
2549 lemma extend_to_affine_basis: |
2548 fixes S V :: "'n::euclidean_space set" |
2550 fixes S V :: "'n::euclidean_space set" |
2549 assumes "\<not> affine_dependent S" "S \<subseteq> V" "S \<noteq> {}" |
2551 assumes "\<not> affine_dependent S" "S \<subseteq> V" "S \<noteq> {}" |
2550 shows "\<exists>T. \<not> affine_dependent T \<and> S \<subseteq> T \<and> T \<subseteq> V \<and> affine hull T = affine hull V" |
2552 shows "\<exists>T. \<not> affine_dependent T \<and> S \<subseteq> T \<and> T \<subseteq> V \<and> affine hull T = affine hull V" |
2551 proof - |
2553 proof - |
2552 obtain a where a_def: "a \<in> S" |
2554 obtain a where a: "a \<in> S" |
2553 using assms by auto |
2555 using assms by auto |
2554 then have h0: "independent ((\<lambda>x. -a + x) ` (S-{a}))" |
2556 then have h0: "independent ((\<lambda>x. -a + x) ` (S-{a}))" |
2555 using affine_dependent_iff_dependent2 assms by auto |
2557 using affine_dependent_iff_dependent2 assms by auto |
2556 then obtain B where B_def: |
2558 then obtain B where B: |
2557 "(\<lambda>x. -a+x) ` (S - {a}) \<subseteq> B \<and> B \<subseteq> (\<lambda>x. -a+x) ` V \<and> independent B \<and> (\<lambda>x. -a+x) ` V \<subseteq> span B" |
2559 "(\<lambda>x. -a+x) ` (S - {a}) \<subseteq> B \<and> B \<subseteq> (\<lambda>x. -a+x) ` V \<and> independent B \<and> (\<lambda>x. -a+x) ` V \<subseteq> span B" |
2558 using maximal_independent_subset_extend[of "(\<lambda>x. -a+x) ` (S-{a})" "(\<lambda>x. -a + x) ` V"] assms |
2560 using maximal_independent_subset_extend[of "(\<lambda>x. -a+x) ` (S-{a})" "(\<lambda>x. -a + x) ` V"] assms |
2559 by blast |
2561 by blast |
2560 def T \<equiv> "(\<lambda>x. a+x) ` insert 0 B" |
2562 def T \<equiv> "(\<lambda>x. a+x) ` insert 0 B" |
2561 then have "T = insert a ((\<lambda>x. a+x) ` B)" |
2563 then have "T = insert a ((\<lambda>x. a+x) ` B)" |
2562 by auto |
2564 by auto |
2563 then have "affine hull T = (\<lambda>x. a+x) ` span B" |
2565 then have "affine hull T = (\<lambda>x. a+x) ` span B" |
2564 using affine_hull_insert_span_gen[of a "((\<lambda>x. a+x) ` B)"] translation_assoc[of "-a" a B] |
2566 using affine_hull_insert_span_gen[of a "((\<lambda>x. a+x) ` B)"] translation_assoc[of "-a" a B] |
2565 by auto |
2567 by auto |
2566 then have "V \<subseteq> affine hull T" |
2568 then have "V \<subseteq> affine hull T" |
2567 using B_def assms translation_inverse_subset[of a V "span B"] |
2569 using B assms translation_inverse_subset[of a V "span B"] |
2568 by auto |
2570 by auto |
2569 moreover have "T \<subseteq> V" |
2571 moreover have "T \<subseteq> V" |
2570 using T_def B_def a_def assms by auto |
2572 using T_def B a assms by auto |
2571 ultimately have "affine hull T = affine hull V" |
2573 ultimately have "affine hull T = affine hull V" |
2572 by (metis Int_absorb1 Int_absorb2 hull_hull hull_mono) |
2574 by (metis Int_absorb1 Int_absorb2 hull_hull hull_mono) |
2573 moreover have "S \<subseteq> T" |
2575 moreover have "S \<subseteq> T" |
2574 using T_def B_def translation_inverse_subset[of a "S-{a}" B] |
2576 using T_def B translation_inverse_subset[of a "S-{a}" B] |
2575 by auto |
2577 by auto |
2576 moreover have "\<not> affine_dependent T" |
2578 moreover have "\<not> affine_dependent T" |
2577 using T_def affine_dependent_translation_eq[of "insert 0 B"] |
2579 using T_def affine_dependent_translation_eq[of "insert 0 B"] |
2578 affine_dependent_imp_dependent2 B_def |
2580 affine_dependent_imp_dependent2 B |
2579 by auto |
2581 by auto |
2580 ultimately show ?thesis using `T \<subseteq> V` by auto |
2582 ultimately show ?thesis using `T \<subseteq> V` by auto |
2581 qed |
2583 qed |
2582 |
2584 |
2583 lemma affine_basis_exists: |
2585 lemma affine_basis_exists: |
2668 and "subspace L" |
2670 and "subspace L" |
2669 and "affine_parallel (affine hull V) L" |
2671 and "affine_parallel (affine hull V) L" |
2670 shows "aff_dim V = int (dim L)" |
2672 shows "aff_dim V = int (dim L)" |
2671 proof - |
2673 proof - |
2672 obtain B where |
2674 obtain B where |
2673 B_def: "affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> int (card B) = aff_dim V + 1" |
2675 B: "affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> int (card B) = aff_dim V + 1" |
2674 using aff_dim_basis_exists by auto |
2676 using aff_dim_basis_exists by auto |
2675 then have "B \<noteq> {}" |
2677 then have "B \<noteq> {}" |
2676 using assms B_def affine_hull_nonempty[of V] affine_hull_nonempty[of B] |
2678 using assms B affine_hull_nonempty[of V] affine_hull_nonempty[of B] |
2677 by auto |
2679 by auto |
2678 then obtain a where a_def: "a \<in> B" by auto |
2680 then obtain a where a: "a \<in> B" by auto |
2679 def Lb \<equiv> "span ((\<lambda>x. -a+x) ` (B-{a}))" |
2681 def Lb \<equiv> "span ((\<lambda>x. -a+x) ` (B-{a}))" |
2680 moreover have "affine_parallel (affine hull B) Lb" |
2682 moreover have "affine_parallel (affine hull B) Lb" |
2681 using Lb_def B_def assms affine_hull_span2[of a B] a_def |
2683 using Lb_def B assms affine_hull_span2[of a B] a |
2682 affine_parallel_commut[of "Lb" "(affine hull B)"] |
2684 affine_parallel_commut[of "Lb" "(affine hull B)"] |
2683 unfolding affine_parallel_def |
2685 unfolding affine_parallel_def |
2684 by auto |
2686 by auto |
2685 moreover have "subspace Lb" |
2687 moreover have "subspace Lb" |
2686 using Lb_def subspace_span by auto |
2688 using Lb_def subspace_span by auto |
2687 moreover have "affine hull B \<noteq> {}" |
2689 moreover have "affine hull B \<noteq> {}" |
2688 using assms B_def affine_hull_nonempty[of V] by auto |
2690 using assms B affine_hull_nonempty[of V] by auto |
2689 ultimately have "L = Lb" |
2691 ultimately have "L = Lb" |
2690 using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B_def |
2692 using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B |
2691 by auto |
2693 by auto |
2692 then have "dim L = dim Lb" |
2694 then have "dim L = dim Lb" |
2693 by auto |
2695 by auto |
2694 moreover have "card B - 1 = dim Lb" and "finite B" |
2696 moreover have "card B - 1 = dim Lb" and "finite B" |
2695 using Lb_def aff_dim_parallel_subspace_aux a_def B_def by auto |
2697 using Lb_def aff_dim_parallel_subspace_aux a B by auto |
2696 ultimately show ?thesis |
2698 ultimately show ?thesis |
2697 using B_def `B \<noteq> {}` card_gt_0_iff[of B] by auto |
2699 using B `B \<noteq> {}` card_gt_0_iff[of B] by auto |
2698 qed |
2700 qed |
2699 |
2701 |
2700 lemma aff_independent_finite: |
2702 lemma aff_independent_finite: |
2701 fixes B :: "'n::euclidean_space set" |
2703 fixes B :: "'n::euclidean_space set" |
2702 assumes "\<not> affine_dependent B" |
2704 assumes "\<not> affine_dependent B" |
2780 apply (rule span_inc) |
2782 apply (rule span_inc) |
2781 apply (rule assms) |
2783 apply (rule assms) |
2782 defer |
2784 defer |
2783 unfolding dim_span[of B] |
2785 unfolding dim_span[of B] |
2784 apply(rule B) |
2786 apply(rule B) |
2785 unfolding span_substd_basis[OF d, symmetric] |
2787 unfolding span_substd_basis[OF d, symmetric] |
2786 apply (rule span_inc) |
2788 apply (rule span_inc) |
2787 apply (rule independent_substdbasis[OF d]) |
2789 apply (rule independent_substdbasis[OF d]) |
2788 apply rule |
2790 apply rule |
2789 apply assumption |
2791 apply assumption |
2790 unfolding t[symmetric] span_substd_basis[OF d] dim_substandard[OF d] |
2792 unfolding t[symmetric] span_substd_basis[OF d] dim_substandard[OF d] |
2829 using aff_dim_empty by auto |
2831 using aff_dim_empty by auto |
2830 then show ?thesis |
2832 then show ?thesis |
2831 using `B = {}` by auto |
2833 using `B = {}` by auto |
2832 next |
2834 next |
2833 case False |
2835 case False |
2834 then obtain a where a_def: "a \<in> B" by auto |
2836 then obtain a where a: "a \<in> B" by auto |
2835 def Lb \<equiv> "span ((\<lambda>x. -a+x) ` (B-{a}))" |
2837 def Lb \<equiv> "span ((\<lambda>x. -a+x) ` (B-{a}))" |
2836 have "affine_parallel (affine hull B) Lb" |
2838 have "affine_parallel (affine hull B) Lb" |
2837 using Lb_def affine_hull_span2[of a B] a_def |
2839 using Lb_def affine_hull_span2[of a B] a |
2838 affine_parallel_commut[of "Lb" "(affine hull B)"] |
2840 affine_parallel_commut[of "Lb" "(affine hull B)"] |
2839 unfolding affine_parallel_def by auto |
2841 unfolding affine_parallel_def by auto |
2840 moreover have "subspace Lb" |
2842 moreover have "subspace Lb" |
2841 using Lb_def subspace_span by auto |
2843 using Lb_def subspace_span by auto |
2842 ultimately have "aff_dim B = int(dim Lb)" |
2844 ultimately have "aff_dim B = int(dim Lb)" |
2843 using aff_dim_parallel_subspace[of B Lb] `B \<noteq> {}` by auto |
2845 using aff_dim_parallel_subspace[of B Lb] `B \<noteq> {}` by auto |
2844 moreover have "(card B) - 1 = dim Lb" "finite B" |
2846 moreover have "(card B) - 1 = dim Lb" "finite B" |
2845 using Lb_def aff_dim_parallel_subspace_aux a_def assms by auto |
2847 using Lb_def aff_dim_parallel_subspace_aux a assms by auto |
2846 ultimately have "of_nat (card B) = aff_dim B + 1" |
2848 ultimately have "of_nat (card B) = aff_dim B + 1" |
2847 using `B \<noteq> {}` card_gt_0_iff[of B] by auto |
2849 using `B \<noteq> {}` card_gt_0_iff[of B] by auto |
2848 then show ?thesis |
2850 then show ?thesis |
2849 using aff_dim_affine_hull2 assms by auto |
2851 using aff_dim_affine_hull2 assms by auto |
2850 qed |
2852 qed |
3169 proof - |
3171 proof - |
3170 fix x T |
3172 fix x T |
3171 assume *: "x \<in> S" "open T" "x \<in> T" "T \<inter> affine hull S \<subseteq> S" |
3173 assume *: "x \<in> S" "open T" "x \<in> T" "T \<inter> affine hull S \<subseteq> S" |
3172 then have **: "x \<in> T \<inter> affine hull S" |
3174 then have **: "x \<in> T \<inter> affine hull S" |
3173 using hull_inc by auto |
3175 using hull_inc by auto |
3174 show "\<exists>Tb. (\<exists>Ta. open Ta \<and> Tb = affine hull S Int Ta) \<and> x \<in> Tb \<and> Tb \<subseteq> S" |
3176 show "\<exists>Tb. (\<exists>Ta. open Ta \<and> Tb = affine hull S \<inter> Ta) \<and> x \<in> Tb \<and> Tb \<subseteq> S" |
3175 apply (rule_tac x="T Int (affine hull S)" in exI) |
3177 apply (rule_tac x = "T \<inter> (affine hull S)" in exI) |
3176 using * ** |
3178 using * ** |
3177 apply auto |
3179 apply auto |
3178 done |
3180 done |
3179 qed |
3181 qed |
3180 |
3182 |
3285 and "x \<in> S" |
3287 and "x \<in> S" |
3286 and "0 < e" |
3288 and "0 < e" |
3287 and "e \<le> 1" |
3289 and "e \<le> 1" |
3288 shows "x - e *\<^sub>R (x - c) \<in> rel_interior S" |
3290 shows "x - e *\<^sub>R (x - c) \<in> rel_interior S" |
3289 proof - |
3291 proof - |
3290 obtain d where "d > 0" and d: "ball c d Int affine hull S \<subseteq> S" |
3292 obtain d where "d > 0" and d: "ball c d \<inter> affine hull S \<subseteq> S" |
3291 using assms(2) unfolding mem_rel_interior_ball by auto |
3293 using assms(2) unfolding mem_rel_interior_ball by auto |
3292 { |
3294 { |
3293 fix y |
3295 fix y |
3294 assume as: "dist (x - e *\<^sub>R (x - c)) y < e * d" "y \<in> affine hull S" |
3296 assume as: "dist (x - e *\<^sub>R (x - c)) y < e * d" "y \<in> affine hull S" |
3295 have *: "y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" |
3297 have *: "y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" |
3655 } |
3657 } |
3656 moreover |
3658 moreover |
3657 { |
3659 { |
3658 fix x |
3660 fix x |
3659 assume x: "x \<in> rel_interior S" |
3661 assume x: "x \<in> rel_interior S" |
3660 then obtain e2 where e2: "e2 > 0" "cball x e2 Int affine hull S \<subseteq> S" |
3662 then obtain e2 where e2: "e2 > 0" "cball x e2 \<inter> affine hull S \<subseteq> S" |
3661 using rel_interior_cball[of S] by auto |
3663 using rel_interior_cball[of S] by auto |
3662 have "x \<in> S" using x rel_interior_subset by auto |
3664 have "x \<in> S" using x rel_interior_subset by auto |
3663 then have *: "f x \<in> f ` S" by auto |
3665 then have *: "f x \<in> f ` S" by auto |
3664 have "\<forall>x\<in>span S. f x = 0 \<longrightarrow> x = 0" |
3666 have "\<forall>x\<in>span S. f x = 0 \<longrightarrow> x = 0" |
3665 using assms subspace_span linear_conv_bounded_linear[of f] |
3667 using assms subspace_span linear_conv_bounded_linear[of f] |
3784 then have "x + (y - a) \<in> cball x (b x)" |
3786 then have "x + (y - a) \<in> cball x (b x)" |
3785 using y unfolding mem_cball dist_norm by auto |
3787 using y unfolding mem_cball dist_norm by auto |
3786 moreover from `x\<in>t` have "x \<in> s" |
3788 moreover from `x\<in>t` have "x \<in> s" |
3787 using obt(2) by auto |
3789 using obt(2) by auto |
3788 ultimately have "x + (y - a) \<in> s" |
3790 ultimately have "x + (y - a) \<in> s" |
3789 using y and b[THEN bspec[where x=x]] unfolding subset_eq by fast |
3791 using y and b[THEN bspec[where x=x]] unfolding subset_eq by fast |
3790 } |
3792 } |
3791 moreover |
3793 moreover |
3792 have *: "inj_on (\<lambda>v. v + (y - a)) t" |
3794 have *: "inj_on (\<lambda>v. v + (y - a)) t" |
3793 unfolding inj_on_def by auto |
3795 unfolding inj_on_def by auto |
3794 have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a))) = 1" |
3796 have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a))) = 1" |
4754 proof (cases "S = {}") |
4756 proof (cases "S = {}") |
4755 case True |
4757 case True |
4756 then show ?thesis by auto |
4758 then show ?thesis by auto |
4757 next |
4759 next |
4758 case False |
4760 case False |
4759 then have *: "0 \<in> S & (!c. c>0 --> op *\<^sub>R c ` S = S)" using cone_iff[of S] assms by auto |
4761 then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` S = S)" |
4762 using cone_iff[of S] assms by auto |
|
4760 { |
4763 { |
4761 fix c :: real |
4764 fix c :: real |
4762 assume "c > 0" |
4765 assume "c > 0" |
4763 then have "op *\<^sub>R c ` (convex hull S) = convex hull (op *\<^sub>R c ` S)" |
4766 then have "op *\<^sub>R c ` (convex hull S) = convex hull (op *\<^sub>R c ` S)" |
4764 using convex_hull_scaling[of _ S] by auto |
4767 using convex_hull_scaling[of _ S] by auto |
4782 apply (rule set_eqI) |
4785 apply (rule set_eqI) |
4783 apply rule |
4786 apply rule |
4784 unfolding Inter_iff Ball_def mem_Collect_eq |
4787 unfolding Inter_iff Ball_def mem_Collect_eq |
4785 apply (rule,rule,erule conjE) |
4788 apply (rule,rule,erule conjE) |
4786 proof - |
4789 proof - |
4787 fix x |
4790 fix x |
4788 assume "\<forall>xa. s \<subseteq> xa \<and> (\<exists>a b. xa = {x. inner a x \<le> b}) \<longrightarrow> x \<in> xa" |
4791 assume "\<forall>xa. s \<subseteq> xa \<and> (\<exists>a b. xa = {x. inner a x \<le> b}) \<longrightarrow> x \<in> xa" |
4789 then have "\<forall>a b. s \<subseteq> {x. inner a x \<le> b} \<longrightarrow> x \<in> {x. inner a x \<le> b}" |
4792 then have "\<forall>a b. s \<subseteq> {x. inner a x \<le> b} \<longrightarrow> x \<in> {x. inner a x \<le> b}" |
4790 by blast |
4793 by blast |
4791 then show "x \<in> s" |
4794 then show "x \<in> s" |
4792 apply (rule_tac ccontr) |
4795 apply (rule_tac ccontr) |
5673 |
5676 |
5674 lemma is_interval_1: |
5677 lemma is_interval_1: |
5675 "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)" |
5678 "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)" |
5676 unfolding is_interval_def by auto |
5679 unfolding is_interval_def by auto |
5677 |
5680 |
5678 lemma is_interval_connected_1: "is_interval s \<longleftrightarrow> connected (s::real set)" |
5681 lemma is_interval_connected_1: |
5679 apply(rule, rule is_interval_connected, assumption) unfolding is_interval_1 |
5682 fixes s :: "real set" |
5680 apply(rule,rule,rule,rule,erule conjE,rule ccontr) proof- |
5683 shows "is_interval s \<longleftrightarrow> connected s" |
5681 fix a b x assume as:"connected s" "a \<in> s" "b \<in> s" "a \<le> x" "x \<le> b" "x\<notin>s" |
5684 apply rule |
5682 hence *:"a < x" "x < b" unfolding not_le [symmetric] by auto |
5685 apply (rule is_interval_connected, assumption) |
5683 let ?halfl = "{..<x} " and ?halfr = "{x<..} " |
5686 unfolding is_interval_1 |
5684 { fix y assume "y \<in> s" with `x \<notin> s` have "x \<noteq> y" by auto |
5687 apply rule |
5685 then have "y \<in> ?halfr \<union> ?halfl" by auto } |
5688 apply rule |
5686 moreover have "a\<in>?halfl" "b\<in>?halfr" using * by auto |
5689 apply rule |
5687 hence "?halfl \<inter> s \<noteq> {}" "?halfr \<inter> s \<noteq> {}" using as(2-3) by auto |
5690 apply rule |
5688 ultimately show False apply(rule_tac notE[OF as(1)[unfolded connected_def]]) |
5691 apply (erule conjE) |
5689 apply(rule_tac x="?halfl" in exI, rule_tac x="?halfr" in exI) |
5692 apply (rule ccontr) |
5690 apply(rule, rule open_lessThan, rule, rule open_greaterThan) |
5693 proof - |
5691 by auto qed |
5694 fix a b x |
5695 assume as: "connected s" "a \<in> s" "b \<in> s" "a \<le> x" "x \<le> b" "x \<notin> s" |
|
5696 then have *: "a < x" "x < b" |
|
5697 unfolding not_le [symmetric] by auto |
|
5698 let ?halfl = "{..<x} " |
|
5699 let ?halfr = "{x<..}" |
|
5700 { |
|
5701 fix y |
|
5702 assume "y \<in> s" |
|
5703 with `x \<notin> s` have "x \<noteq> y" by auto |
|
5704 then have "y \<in> ?halfr \<union> ?halfl" by auto |
|
5705 } |
|
5706 moreover have "a \<in> ?halfl" "b \<in> ?halfr" using * by auto |
|
5707 then have "?halfl \<inter> s \<noteq> {}" "?halfr \<inter> s \<noteq> {}" |
|
5708 using as(2-3) by auto |
|
5709 ultimately show False |
|
5710 apply (rule_tac notE[OF as(1)[unfolded connected_def]]) |
|
5711 apply (rule_tac x = ?halfl in exI) |
|
5712 apply (rule_tac x = ?halfr in exI) |
|
5713 apply rule |
|
5714 apply (rule open_lessThan) |
|
5715 apply rule |
|
5716 apply (rule open_greaterThan) |
|
5717 apply auto |
|
5718 done |
|
5719 qed |
|
5692 |
5720 |
5693 lemma is_interval_convex_1: |
5721 lemma is_interval_convex_1: |
5694 "is_interval s \<longleftrightarrow> convex (s::real set)" |
5722 fixes s :: "real set" |
5695 by(metis is_interval_convex convex_connected is_interval_connected_1) |
5723 shows "is_interval s \<longleftrightarrow> convex s" |
5724 by (metis is_interval_convex convex_connected is_interval_connected_1) |
|
5696 |
5725 |
5697 lemma convex_connected_1: |
5726 lemma convex_connected_1: |
5698 "connected s \<longleftrightarrow> convex (s::real set)" |
5727 fixes s :: "real set" |
5699 by(metis is_interval_convex convex_connected is_interval_connected_1) |
5728 shows "connected s \<longleftrightarrow> convex s" |
5729 by (metis is_interval_convex convex_connected is_interval_connected_1) |
|
5700 |
5730 |
5701 |
5731 |
5702 subsection {* Another intermediate value theorem formulation *} |
5732 subsection {* Another intermediate value theorem formulation *} |
5703 |
5733 |
5704 lemma ivt_increasing_component_on_1: |
5734 lemma ivt_increasing_component_on_1: |
6602 done |
6632 done |
6603 |
6633 |
6604 lemma substd_simplex: |
6634 lemma substd_simplex: |
6605 assumes d: "d \<subseteq> Basis" |
6635 assumes d: "d \<subseteq> Basis" |
6606 shows "convex hull (insert 0 d) = |
6636 shows "convex hull (insert 0 d) = |
6607 {x. (\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> (\<Sum>i\<in>d. x\<bullet>i) \<le> 1 \<and> (\<forall>i\<in>Basis. i \<notin> d --> x\<bullet>i = 0)}" |
6637 {x. (\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> (\<Sum>i\<in>d. x\<bullet>i) \<le> 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)}" |
6608 (is "convex hull (insert 0 ?p) = ?s") |
6638 (is "convex hull (insert 0 ?p) = ?s") |
6609 proof - |
6639 proof - |
6610 let ?D = d |
6640 let ?D = d |
6611 have "0 \<notin> ?p" |
6641 have "0 \<notin> ?p" |
6612 using assms by (auto simp: image_def) |
6642 using assms by (auto simp: image_def) |
6613 from d have "finite d" |
6643 from d have "finite d" |
6614 by (blast intro: finite_subset finite_Basis) |
6644 by (blast intro: finite_subset finite_Basis) |
6615 show ?thesis |
6645 show ?thesis |
6616 unfolding simplex[OF `finite d` `0 ~: ?p`] |
6646 unfolding simplex[OF `finite d` `0 \<notin> ?p`] |
6617 apply (rule set_eqI) |
6647 apply (rule set_eqI) |
6618 unfolding mem_Collect_eq |
6648 unfolding mem_Collect_eq |
6619 apply rule |
6649 apply rule |
6620 apply (elim exE conjE) |
6650 apply (elim exE conjE) |
6621 apply (erule_tac[2] conjE)+ |
6651 apply (erule_tac[2] conjE)+ |
6622 proof - |
6652 proof - |
6623 fix x :: "'a::euclidean_space" |
6653 fix x :: "'a::euclidean_space" |
6624 fix u |
6654 fix u |
6625 assume as: "\<forall>x\<in>?D. 0 \<le> u x" "setsum u ?D \<le> 1" "(\<Sum>x\<in>?D. u x *\<^sub>R x) = x" |
6655 assume as: "\<forall>x\<in>?D. 0 \<le> u x" "setsum u ?D \<le> 1" "(\<Sum>x\<in>?D. u x *\<^sub>R x) = x" |
6626 have *: "\<forall>i\<in>Basis. i:d \<longrightarrow> u i = x\<bullet>i" |
6656 have *: "\<forall>i\<in>Basis. i:d \<longrightarrow> u i = x\<bullet>i" |
6627 and "(\<forall>i\<in>Basis. i ~: d --> x \<bullet> i = 0)" |
6657 and "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)" |
6628 using as(3) |
6658 using as(3) |
6629 unfolding substdbasis_expansion_unique[OF assms] |
6659 unfolding substdbasis_expansion_unique[OF assms] |
6630 by auto |
6660 by auto |
6631 then have **: "setsum u ?D = setsum (op \<bullet> x) ?D" |
6661 then have **: "setsum u ?D = setsum (op \<bullet> x) ?D" |
6632 apply - |
6662 apply - |
6836 then have as: "\<forall>xa. dist x xa < e \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> xa\<bullet>i = 0) \<longrightarrow> |
6866 then have as: "\<forall>xa. dist x xa < e \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> xa\<bullet>i = 0) \<longrightarrow> |
6837 (\<forall>i\<in>d. 0 \<le> xa \<bullet> i) \<and> setsum (op \<bullet> xa) d \<le> 1" |
6867 (\<forall>i\<in>d. 0 \<le> xa \<bullet> i) \<and> setsum (op \<bullet> xa) d \<le> 1" |
6838 unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto |
6868 unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto |
6839 have x0: "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)" |
6869 have x0: "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)" |
6840 using x rel_interior_subset substd_simplex[OF assms] by auto |
6870 using x rel_interior_subset substd_simplex[OF assms] by auto |
6841 have "(\<forall>i\<in>d. 0 < x \<bullet> i) \<and> setsum (op \<bullet> x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d --> x\<bullet>i = 0)" |
6871 have "(\<forall>i\<in>d. 0 < x \<bullet> i) \<and> setsum (op \<bullet> x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)" |
6842 apply (rule, rule) |
6872 apply rule |
6873 apply rule |
|
6843 proof - |
6874 proof - |
6844 fix i :: 'a |
6875 fix i :: 'a |
6845 assume "i \<in> d" |
6876 assume "i \<in> d" |
6846 then have "\<forall>ia\<in>d. 0 \<le> (x - (e / 2) *\<^sub>R i) \<bullet> ia" |
6877 then have "\<forall>ia\<in>d. 0 \<le> (x - (e / 2) *\<^sub>R i) \<bullet> ia" |
6847 apply - |
6878 apply - |
6889 assume as: "x \<in> ?s" |
6920 assume as: "x \<in> ?s" |
6890 have "\<forall>i. 0 < x\<bullet>i \<or> 0 = x\<bullet>i \<longrightarrow> 0 \<le> x\<bullet>i" |
6921 have "\<forall>i. 0 < x\<bullet>i \<or> 0 = x\<bullet>i \<longrightarrow> 0 \<le> x\<bullet>i" |
6891 by auto |
6922 by auto |
6892 moreover have "\<forall>i. i \<in> d \<or> i \<notin> d" by auto |
6923 moreover have "\<forall>i. i \<in> d \<or> i \<notin> d" by auto |
6893 ultimately |
6924 ultimately |
6894 have "\<forall>i. (\<forall>i\<in>d. 0 < x\<bullet>i) \<and> (\<forall>i. i \<notin> d \<longrightarrow> x\<bullet>i = 0) --> 0 \<le> x\<bullet>i" |
6925 have "\<forall>i. (\<forall>i\<in>d. 0 < x\<bullet>i) \<and> (\<forall>i. i \<notin> d \<longrightarrow> x\<bullet>i = 0) \<longrightarrow> 0 \<le> x\<bullet>i" |
6895 by metis |
6926 by metis |
6896 then have h2: "x \<in> convex hull (insert 0 ?p)" |
6927 then have h2: "x \<in> convex hull (insert 0 ?p)" |
6897 using as assms |
6928 using as assms |
6898 unfolding substd_simplex[OF assms] by fastforce |
6929 unfolding substd_simplex[OF assms] by fastforce |
6899 obtain a where a: "a \<in> d" |
6930 obtain a where a: "a \<in> d" |
6906 moreover have "?d > 0" |
6937 moreover have "?d > 0" |
6907 apply (rule divide_pos_pos) |
6938 apply (rule divide_pos_pos) |
6908 using as using `0 < card d` by auto |
6939 using as using `0 < card d` by auto |
6909 ultimately have h3: "min (Min ((op \<bullet> x) ` d)) ?d > 0" |
6940 ultimately have h3: "min (Min ((op \<bullet> x) ` d)) ?d > 0" |
6910 by auto |
6941 by auto |
6911 |
6942 |
6912 have "x \<in> rel_interior (convex hull (insert 0 ?p))" |
6943 have "x \<in> rel_interior (convex hull (insert 0 ?p))" |
6913 unfolding rel_interior_ball mem_Collect_eq h0 |
6944 unfolding rel_interior_ball mem_Collect_eq h0 |
6914 apply (rule,rule h2) |
6945 apply (rule,rule h2) |
6915 unfolding substd_simplex[OF assms] |
6946 unfolding substd_simplex[OF assms] |
6916 apply (rule_tac x="min (Min ((op \<bullet> x) ` d)) ?d" in exI) |
6947 apply (rule_tac x="min (Min ((op \<bullet> x) ` d)) ?d" in exI) |
6938 also have "\<dots> \<le> 1" |
6969 also have "\<dots> \<le> 1" |
6939 unfolding setsum_addf setsum_constant real_eq_of_nat |
6970 unfolding setsum_addf setsum_constant real_eq_of_nat |
6940 using `0 < card d` |
6971 using `0 < card d` |
6941 by auto |
6972 by auto |
6942 finally show "setsum (op \<bullet> y) d \<le> 1" . |
6973 finally show "setsum (op \<bullet> y) d \<le> 1" . |
6943 |
6974 |
6944 fix i :: 'a |
6975 fix i :: 'a |
6945 assume i: "i \<in> Basis" |
6976 assume i: "i \<in> Basis" |
6946 then show "0 \<le> y\<bullet>i" |
6977 then show "0 \<le> y\<bullet>i" |
6947 proof (cases "i\<in>d") |
6978 proof (cases "i\<in>d") |
6948 case True |
6979 case True |
7278 using subset_rel_interior[of S "closure S"] closure_same_affine_hull closure_subset |
7309 using subset_rel_interior[of S "closure S"] closure_same_affine_hull closure_subset |
7279 by auto |
7310 by auto |
7280 moreover |
7311 moreover |
7281 { |
7312 { |
7282 fix z |
7313 fix z |
7283 assume z: "z : rel_interior (closure S)" |
7314 assume z: "z \<in> rel_interior (closure S)" |
7284 obtain x where x: "x \<in> rel_interior S" |
7315 obtain x where x: "x \<in> rel_interior S" |
7285 using `S \<noteq> {}` assms rel_interior_convex_nonempty by auto |
7316 using `S \<noteq> {}` assms rel_interior_convex_nonempty by auto |
7286 have "z \<in> rel_interior S" |
7317 have "z \<in> rel_interior S" |
7287 proof (cases "x = z") |
7318 proof (cases "x = z") |
7288 case True |
7319 case True |
7289 then show ?thesis using x by auto |
7320 then show ?thesis using x by auto |
7290 next |
7321 next |
7291 case False |
7322 case False |
7292 obtain e where e: "e > 0" "cball z e Int affine hull closure S \<le> closure S" |
7323 obtain e where e: "e > 0" "cball z e \<inter> affine hull closure S \<le> closure S" |
7293 using z rel_interior_cball[of "closure S"] by auto |
7324 using z rel_interior_cball[of "closure S"] by auto |
7294 then have *: "0 < e/norm(z-x)" |
7325 then have *: "0 < e/norm(z-x)" |
7295 using e False divide_pos_pos[of e "norm(z-x)"] by auto |
7326 using e False divide_pos_pos[of e "norm(z-x)"] by auto |
7296 def y \<equiv> "z + (e/norm(z-x)) *\<^sub>R (z-x)" |
7327 def y \<equiv> "z + (e/norm(z-x)) *\<^sub>R (z-x)" |
7297 have yball: "y \<in> cball z e" |
7328 have yball: "y \<in> cball z e" |
7336 lemma closure_eq_between: |
7367 lemma closure_eq_between: |
7337 fixes S1 S2 :: "'n::euclidean_space set" |
7368 fixes S1 S2 :: "'n::euclidean_space set" |
7338 assumes "convex S1" |
7369 assumes "convex S1" |
7339 and "convex S2" |
7370 and "convex S2" |
7340 shows "closure S1 = closure S2 \<longleftrightarrow> rel_interior S1 \<le> S2 \<and> S2 \<subseteq> closure S1" |
7371 shows "closure S1 = closure S2 \<longleftrightarrow> rel_interior S1 \<le> S2 \<and> S2 \<subseteq> closure S1" |
7341 (is "?A <-> ?B") |
7372 (is "?A \<longleftrightarrow> ?B") |
7342 proof |
7373 proof |
7343 assume ?A |
7374 assume ?A |
7344 then show ?B |
7375 then show ?B |
7345 by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset) |
7376 by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset) |
7346 next |
7377 next |
7420 using `S1 \<noteq> {}` rel_interior_convex_nonempty assms by auto |
7451 using `S1 \<noteq> {}` rel_interior_convex_nonempty assms by auto |
7421 obtain T where T: "open T" "a \<in> T \<inter> S1" "T \<inter> affine hull S1 \<subseteq> S1" |
7452 obtain T where T: "open T" "a \<in> T \<inter> S1" "T \<inter> affine hull S1 \<subseteq> S1" |
7422 using mem_rel_interior[of a S1] a by auto |
7453 using mem_rel_interior[of a S1] a by auto |
7423 then have "a \<in> T \<inter> closure S2" |
7454 then have "a \<in> T \<inter> closure S2" |
7424 using a assms unfolding rel_frontier_def by auto |
7455 using a assms unfolding rel_frontier_def by auto |
7425 then obtain b where b: "b \<in> T Int rel_interior S2" |
7456 then obtain b where b: "b \<in> T \<inter> rel_interior S2" |
7426 using open_inter_closure_rel_interior[of S2 T] assms T by auto |
7457 using open_inter_closure_rel_interior[of S2 T] assms T by auto |
7427 then have "b \<in> affine hull S1" |
7458 then have "b \<in> affine hull S1" |
7428 using rel_interior_subset hull_subset[of S2] ** by auto |
7459 using rel_interior_subset hull_subset[of S2] ** by auto |
7429 then have "b \<in> S1" |
7460 then have "b \<in> S1" |
7430 using T b by auto |
7461 using T b by auto |
7440 fixes S :: "'n::euclidean_space set" |
7471 fixes S :: "'n::euclidean_space set" |
7441 assumes "convex S" |
7472 assumes "convex S" |
7442 and "z \<in> rel_interior S" |
7473 and "z \<in> rel_interior S" |
7443 shows "\<forall>x\<in>affine hull S. \<exists>m. m > 1 \<and> (\<forall>e. e > 1 \<and> e \<le> m \<longrightarrow> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S)" |
7474 shows "\<forall>x\<in>affine hull S. \<exists>m. m > 1 \<and> (\<forall>e. e > 1 \<and> e \<le> m \<longrightarrow> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S)" |
7444 proof - |
7475 proof - |
7445 obtain e1 where e1: "e1>0 & cball z e1 Int affine hull S <= S" |
7476 obtain e1 where e1: "e1 > 0 \<and> cball z e1 \<inter> affine hull S \<subseteq> S" |
7446 using mem_rel_interior_cball[of z S] assms by auto |
7477 using mem_rel_interior_cball[of z S] assms by auto |
7447 { |
7478 { |
7448 fix x |
7479 fix x |
7449 assume x: "x \<in> affine hull S" |
7480 assume x: "x \<in> affine hull S" |
7450 { assume "x ~= z" |
7481 { |
7482 assume "x \<noteq> z" |
|
7451 def m \<equiv> "1 + e1/norm(x-z)" |
7483 def m \<equiv> "1 + e1/norm(x-z)" |
7452 then have "m > 1" |
7484 then have "m > 1" |
7453 using e1 `x \<noteq> z` divide_pos_pos[of e1 "norm (x - z)"] by auto |
7485 using e1 `x \<noteq> z` divide_pos_pos[of e1 "norm (x - z)"] by auto |
7454 { |
7486 { |
7455 fix e |
7487 fix e |
7566 moreover |
7598 moreover |
7567 { |
7599 { |
7568 assume r: "\<forall>x. \<exists>e. e > 0 \<and> z + e *\<^sub>R x \<in> S" |
7600 assume r: "\<forall>x. \<exists>e. e > 0 \<and> z + e *\<^sub>R x \<in> S" |
7569 { |
7601 { |
7570 fix x |
7602 fix x |
7571 obtain e1 where e1_def: "e1 > 0 \<and> z + e1 *\<^sub>R (x - z) \<in> S" |
7603 obtain e1 where e1: "e1 > 0 \<and> z + e1 *\<^sub>R (x - z) \<in> S" |
7572 using r by auto |
7604 using r by auto |
7573 obtain e2 where e2_def: "e2 > 0 \<and> z + e2 *\<^sub>R (z - x) \<in> S" |
7605 obtain e2 where e2: "e2 > 0 \<and> z + e2 *\<^sub>R (z - x) \<in> S" |
7574 using r by auto |
7606 using r by auto |
7575 def x1 \<equiv> "z + e1 *\<^sub>R (x - z)" |
7607 def x1 \<equiv> "z + e1 *\<^sub>R (x - z)" |
7576 then have x1: "x1 \<in> affine hull S" |
7608 then have x1: "x1 \<in> affine hull S" |
7577 using e1_def hull_subset[of S] by auto |
7609 using e1 hull_subset[of S] by auto |
7578 def x2 \<equiv> "z + e2 *\<^sub>R (z - x)" |
7610 def x2 \<equiv> "z + e2 *\<^sub>R (z - x)" |
7579 then have x2: "x2 \<in> affine hull S" |
7611 then have x2: "x2 \<in> affine hull S" |
7580 using e2_def hull_subset[of S] by auto |
7612 using e2 hull_subset[of S] by auto |
7581 have *: "e1/(e1+e2) + e2/(e1+e2) = 1" |
7613 have *: "e1/(e1+e2) + e2/(e1+e2) = 1" |
7582 using add_divide_distrib[of e1 e2 "e1+e2"] e1_def e2_def by simp |
7614 using add_divide_distrib[of e1 e2 "e1+e2"] e1 e2 by simp |
7583 then have "z = (e2/(e1+e2)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2" |
7615 then have "z = (e2/(e1+e2)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2" |
7584 using x1_def x2_def |
7616 using x1_def x2_def |
7585 apply (auto simp add: algebra_simps) |
7617 apply (auto simp add: algebra_simps) |
7586 using scaleR_left_distrib[of "e1/(e1+e2)" "e2/(e1+e2)" z] |
7618 using scaleR_left_distrib[of "e1/(e1+e2)" "e2/(e1+e2)" z] |
7587 apply auto |
7619 apply auto |
7591 x1 x2 affine_affine_hull[of S] * |
7623 x1 x2 affine_affine_hull[of S] * |
7592 by auto |
7624 by auto |
7593 have "x1 - x2 = (e1 + e2) *\<^sub>R (x - z)" |
7625 have "x1 - x2 = (e1 + e2) *\<^sub>R (x - z)" |
7594 using x1_def x2_def by (auto simp add: algebra_simps) |
7626 using x1_def x2_def by (auto simp add: algebra_simps) |
7595 then have "x = z+(1/(e1+e2)) *\<^sub>R (x1-x2)" |
7627 then have "x = z+(1/(e1+e2)) *\<^sub>R (x1-x2)" |
7596 using e1_def e2_def by simp |
7628 using e1 e2 by simp |
7597 then have "x \<in> affine hull S" |
7629 then have "x \<in> affine hull S" |
7598 using mem_affine_3_minus[of "affine hull S" z x1 x2 "1/(e1+e2)"] |
7630 using mem_affine_3_minus[of "affine hull S" z x1 x2 "1/(e1+e2)"] |
7599 x1 x2 z affine_affine_hull[of S] |
7631 x1 x2 z affine_affine_hull[of S] |
7600 by auto |
7632 by auto |
7601 } |
7633 } |
7688 then have "y \<in> \<Inter>{closure S |S. S \<in> I}" |
7720 then have "y \<in> \<Inter>{closure S |S. S \<in> I}" |
7689 by auto |
7721 by auto |
7690 } |
7722 } |
7691 then have "\<Inter>I \<subseteq> \<Inter>{closure S |S. S \<in> I}" |
7723 then have "\<Inter>I \<subseteq> \<Inter>{closure S |S. S \<in> I}" |
7692 by auto |
7724 by auto |
7693 moreover have "closed (Inter {closure S |S. S \<in> I})" |
7725 moreover have "closed (\<Inter>{closure S |S. S \<in> I})" |
7694 unfolding closed_Inter closed_closure by auto |
7726 unfolding closed_Inter closed_closure by auto |
7695 ultimately show ?thesis using closure_hull[of "Inter I"] |
7727 ultimately show ?thesis using closure_hull[of "\<Inter>I"] |
7696 hull_minimal[of "\<Inter>I" "\<Inter>{closure S |S. S \<in> I}" "closed"] by auto |
7728 hull_minimal[of "\<Inter>I" "\<Inter>{closure S |S. S \<in> I}" "closed"] by auto |
7697 qed |
7729 qed |
7698 |
7730 |
7699 lemma convex_closure_rel_interior_inter: |
7731 lemma convex_closure_rel_interior_inter: |
7700 assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)" |
7732 assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)" |
7709 then have y: "\<forall>S \<in> I. y \<in> closure S" |
7741 then have y: "\<forall>S \<in> I. y \<in> closure S" |
7710 by auto |
7742 by auto |
7711 { |
7743 { |
7712 assume "y = x" |
7744 assume "y = x" |
7713 then have "y \<in> closure (\<Inter>{rel_interior S |S. S \<in> I})" |
7745 then have "y \<in> closure (\<Inter>{rel_interior S |S. S \<in> I})" |
7714 using x closure_subset[of "Inter {rel_interior S |S. S \<in> I}"] by auto |
7746 using x closure_subset[of "\<Inter>{rel_interior S |S. S \<in> I}"] by auto |
7715 } |
7747 } |
7716 moreover |
7748 moreover |
7717 { |
7749 { |
7718 assume "y \<noteq> x" |
7750 assume "y \<noteq> x" |
7719 { fix e :: real |
7751 { fix e :: real |
7751 |
7783 |
7752 |
7784 |
7753 lemma convex_closure_inter: |
7785 lemma convex_closure_inter: |
7754 assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)" |
7786 assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)" |
7755 and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}" |
7787 and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}" |
7756 shows "closure (Inter I) = Inter {closure S |S. S \<in> I}" |
7788 shows "closure (\<Inter>I) = \<Inter>{closure S |S. S \<in> I}" |
7757 proof - |
7789 proof - |
7758 have "\<Inter>{closure S |S. S \<in> I} \<le> closure (\<Inter>{rel_interior S |S. S \<in> I})" |
7790 have "\<Inter>{closure S |S. S \<in> I} \<le> closure (\<Inter>{rel_interior S |S. S \<in> I})" |
7759 using convex_closure_rel_interior_inter assms by auto |
7791 using convex_closure_rel_interior_inter assms by auto |
7760 moreover |
7792 moreover |
7761 have "closure (Inter {rel_interior S |S. S \<in> I}) \<le> closure (Inter I)" |
7793 have "closure (\<Inter>{rel_interior S |S. S \<in> I}) \<le> closure (\<Inter> I)" |
7762 using rel_interior_inter_aux closure_mono[of "Inter {rel_interior S |S. S \<in> I}" "\<Inter>I"] |
7794 using rel_interior_inter_aux closure_mono[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"] |
7763 by auto |
7795 by auto |
7764 ultimately show ?thesis |
7796 ultimately show ?thesis |
7765 using closure_inter[of I] by auto |
7797 using closure_inter[of I] by auto |
7766 qed |
7798 qed |
7767 |
7799 |
7768 lemma convex_inter_rel_interior_same_closure: |
7800 lemma convex_inter_rel_interior_same_closure: |
7769 assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)" |
7801 assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)" |
7770 and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}" |
7802 and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}" |
7771 shows "closure (Inter {rel_interior S |S. S \<in> I}) = closure (\<Inter>I)" |
7803 shows "closure (\<Inter>{rel_interior S |S. S \<in> I}) = closure (\<Inter>I)" |
7772 proof - |
7804 proof - |
7773 have "\<Inter>{closure S |S. S \<in> I} \<le> closure (\<Inter>{rel_interior S |S. S \<in> I})" |
7805 have "\<Inter>{closure S |S. S \<in> I} \<le> closure (\<Inter>{rel_interior S |S. S \<in> I})" |
7774 using convex_closure_rel_interior_inter assms by auto |
7806 using convex_closure_rel_interior_inter assms by auto |
7775 moreover |
7807 moreover |
7776 have "closure (\<Inter>{rel_interior S |S. S \<in> I}) \<le> closure (\<Inter>I)" |
7808 have "closure (\<Inter>{rel_interior S |S. S \<in> I}) \<le> closure (\<Inter>I)" |
7777 using rel_interior_inter_aux closure_mono[of "Inter {rel_interior S |S. S \<in> I}" "\<Inter>I"] |
7809 using rel_interior_inter_aux closure_mono[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"] |
7778 by auto |
7810 by auto |
7779 ultimately show ?thesis |
7811 ultimately show ?thesis |
7780 using closure_inter[of I] by auto |
7812 using closure_inter[of I] by auto |
7781 qed |
7813 qed |
7782 |
7814 |
7783 lemma convex_rel_interior_inter: |
7815 lemma convex_rel_interior_inter: |
7784 assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)" |
7816 assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)" |
7785 and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}" |
7817 and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}" |
7786 shows "rel_interior (Inter I) \<le> Inter {rel_interior S |S. S \<in> I}" |
7818 shows "rel_interior (\<Inter>I) \<subseteq> \<Inter>{rel_interior S |S. S \<in> I}" |
7787 proof - |
7819 proof - |
7788 have "convex (\<Inter>I)" |
7820 have "convex (\<Inter>I)" |
7789 using assms convex_Inter by auto |
7821 using assms convex_Inter by auto |
7790 moreover |
7822 moreover |
7791 have "convex(Inter {rel_interior S |S. S \<in> I})" |
7823 have "convex (\<Inter>{rel_interior S |S. S \<in> I})" |
7792 apply (rule convex_Inter) |
7824 apply (rule convex_Inter) |
7793 using assms convex_rel_interior |
7825 using assms convex_rel_interior |
7794 apply auto |
7826 apply auto |
7795 done |
7827 done |
7796 ultimately |
7828 ultimately |
7966 then obtain z1 where z1: "z1 \<in> rel_interior S" "f z1 = z" by auto |
7998 then obtain z1 where z1: "z1 \<in> rel_interior S" "f z1 = z" by auto |
7967 { |
7999 { |
7968 fix x |
8000 fix x |
7969 assume "x \<in> f ` S" |
8001 assume "x \<in> f ` S" |
7970 then obtain x1 where x1: "x1 \<in> S" "f x1 = x" by auto |
8002 then obtain x1 where x1: "x1 \<in> S" "f x1 = x" by auto |
7971 then obtain e where e_def: "e > 1" "(1 - e) *\<^sub>R x1 + e *\<^sub>R z1 : S" |
8003 then obtain e where e: "e > 1" "(1 - e) *\<^sub>R x1 + e *\<^sub>R z1 : S" |
7972 using convex_rel_interior_iff[of S z1] `convex S` x1 z1 by auto |
8004 using convex_rel_interior_iff[of S z1] `convex S` x1 z1 by auto |
7973 moreover have "f ((1 - e) *\<^sub>R x1 + e *\<^sub>R z1) = (1 - e) *\<^sub>R x + e *\<^sub>R z" |
8005 moreover have "f ((1 - e) *\<^sub>R x1 + e *\<^sub>R z1) = (1 - e) *\<^sub>R x + e *\<^sub>R z" |
7974 using x1 z1 `linear f` by (simp add: linear_add_cmul) |
8006 using x1 z1 `linear f` by (simp add: linear_add_cmul) |
7975 ultimately have "(1 - e) *\<^sub>R x + e *\<^sub>R z : f ` S" |
8007 ultimately have "(1 - e) *\<^sub>R x + e *\<^sub>R z : f ` S" |
7976 using imageI[of "(1 - e) *\<^sub>R x1 + e *\<^sub>R z1" S f] by auto |
8008 using imageI[of "(1 - e) *\<^sub>R x1 + e *\<^sub>R z1" S f] by auto |
7977 then have "\<exists>e. e > 1 \<and> (1 - e) *\<^sub>R x + e *\<^sub>R z : f ` S" |
8009 then have "\<exists>e. e > 1 \<and> (1 - e) *\<^sub>R x + e *\<^sub>R z : f ` S" |
7978 using e_def by auto |
8010 using e by auto |
7979 } |
8011 } |
7980 then have "z \<in> rel_interior (f ` S)" |
8012 then have "z \<in> rel_interior (f ` S)" |
7981 using convex_rel_interior_iff[of "f ` S" z] `convex S` |
8013 using convex_rel_interior_iff[of "f ` S" z] `convex S` |
7982 `linear f` `S ~= {}` convex_linear_image[of f S] linear_conv_bounded_linear[of f] |
8014 `linear f` `S \<noteq> {}` convex_linear_image[of f S] linear_conv_bounded_linear[of f] |
7983 by auto |
8015 by auto |
7984 } |
8016 } |
7985 ultimately show ?thesis by auto |
8017 ultimately show ?thesis by auto |
7986 qed |
8018 qed |
7987 |
8019 |
8020 } |
8052 } |
8021 then have "z \<in> rel_interior (f -` S)" |
8053 then have "z \<in> rel_interior (f -` S)" |
8022 using convex_rel_interior_iff[of "f -` S" z] conv nonemp by auto |
8054 using convex_rel_interior_iff[of "f -` S" z] conv nonemp by auto |
8023 } |
8055 } |
8024 moreover |
8056 moreover |
8025 { |
8057 { |
8026 fix z |
8058 fix z |
8027 assume z: "z \<in> rel_interior (f -` S)" |
8059 assume z: "z \<in> rel_interior (f -` S)" |
8028 { |
8060 { |
8029 fix x |
8061 fix x |
8030 assume "x \<in> S \<inter> range f" |
8062 assume "x \<in> S \<inter> range f" |
8035 using `linear f` y by (simp add: linear_iff) |
8067 using `linear f` y by (simp add: linear_iff) |
8036 ultimately have "\<exists>e. e > 1 \<and> (1 - e) *\<^sub>R x + e *\<^sub>R f z \<in> S \<inter> range f" |
8068 ultimately have "\<exists>e. e > 1 \<and> (1 - e) *\<^sub>R x + e *\<^sub>R f z \<in> S \<inter> range f" |
8037 using e by auto |
8069 using e by auto |
8038 } |
8070 } |
8039 then have "f z \<in> rel_interior (S \<inter> range f)" |
8071 then have "f z \<in> rel_interior (S \<inter> range f)" |
8040 using `convex (S Int (range f))` `S \<inter> range f \<noteq> {}` |
8072 using `convex (S \<inter> (range f))` `S \<inter> range f \<noteq> {}` |
8041 convex_rel_interior_iff[of "S \<inter> (range f)" "f z"] |
8073 convex_rel_interior_iff[of "S \<inter> (range f)" "f z"] |
8042 by auto |
8074 by auto |
8043 moreover have "affine (range f)" |
8075 moreover have "affine (range f)" |
8044 by (metis assms(1) subspace_UNIV subspace_imp_affine subspace_linear_image) |
8076 by (metis assms(1) subspace_UNIV subspace_imp_affine subspace_linear_image) |
8045 ultimately have "f z \<in> rel_interior S" |
8077 ultimately have "f z \<in> rel_interior S" |
8130 |
8162 |
8131 lemma convex_rel_open_finite_inter: |
8163 lemma convex_rel_open_finite_inter: |
8132 assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set) \<and> rel_open S" |
8164 assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set) \<and> rel_open S" |
8133 and "finite I" |
8165 and "finite I" |
8134 shows "convex (\<Inter>I) \<and> rel_open (\<Inter>I)" |
8166 shows "convex (\<Inter>I) \<and> rel_open (\<Inter>I)" |
8135 proof (cases "Inter {rel_interior S |S. S : I} = {}") |
8167 proof (cases "\<Inter>{rel_interior S |S. S \<in> I} = {}") |
8136 case True |
8168 case True |
8137 then have "\<Inter>I = {}" |
8169 then have "\<Inter>I = {}" |
8138 using assms unfolding rel_open_def by auto |
8170 using assms unfolding rel_open_def by auto |
8139 then show ?thesis |
8171 then show ?thesis |
8140 unfolding rel_open_def using rel_interior_empty by auto |
8172 unfolding rel_open_def using rel_interior_empty by auto |
8141 next |
8173 next |
8142 case False |
8174 case False |
8143 then have "rel_open (Inter I)" |
8175 then have "rel_open (\<Inter>I)" |
8144 using assms unfolding rel_open_def |
8176 using assms unfolding rel_open_def |
8145 using convex_rel_interior_finite_inter[of I] |
8177 using convex_rel_interior_finite_inter[of I] |
8146 by auto |
8178 by auto |
8147 then show ?thesis |
8179 then show ?thesis |
8148 using convex_Inter assms by auto |
8180 using convex_Inter assms by auto |
8288 next |
8320 next |
8289 case False |
8321 case False |
8290 then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` S = S)" |
8322 then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` S = S)" |
8291 using cone_iff[of S] assms by auto |
8323 using cone_iff[of S] assms by auto |
8292 then have *: "0 \<in> ({0} \<union> rel_interior S)" |
8324 then have *: "0 \<in> ({0} \<union> rel_interior S)" |
8293 and "\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` ({0} \<union> rel_interior S) = ({0} Un rel_interior S)" |
8325 and "\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` ({0} \<union> rel_interior S) = ({0} \<union> rel_interior S)" |
8294 by (auto simp add: rel_interior_scaleR) |
8326 by (auto simp add: rel_interior_scaleR) |
8295 then show ?thesis |
8327 then show ?thesis |
8296 using cone_iff[of "{0} Un rel_interior S"] by auto |
8328 using cone_iff[of "{0} \<union> rel_interior S"] by auto |
8297 qed |
8329 qed |
8298 |
8330 |
8299 lemma rel_interior_convex_cone_aux: |
8331 lemma rel_interior_convex_cone_aux: |
8300 fixes S :: "('m::euclidean_space) set" |
8332 fixes S :: "'m::euclidean_space set" |
8301 assumes "convex S" |
8333 assumes "convex S" |
8302 shows "(c,x) : rel_interior (cone hull ({(1 :: real)} <*> S)) <-> |
8334 shows "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} <*> S)) \<longleftrightarrow> |
8303 c>0 & x : ((op *\<^sub>R c) ` (rel_interior S))" |
8335 c > 0 \<and> x \<in> ((op *\<^sub>R c) ` (rel_interior S))" |
8304 proof- |
8336 proof (cases "S = {}") |
8305 { assume "S={}" hence ?thesis by (simp add: rel_interior_empty cone_hull_empty) } |
8337 case True |
8306 moreover |
8338 then show ?thesis |
8307 { assume "S ~= {}" from this obtain s where "s : S" by auto |
8339 by (simp add: rel_interior_empty cone_hull_empty) |
8308 have conv: "convex ({(1 :: real)} <*> S)" using convex_Times[of "{(1 :: real)}" S] |
8340 next |
8309 assms convex_singleton[of "1 :: real"] by auto |
8341 case False |
8310 def f == "(%y. {z. (y,z) : cone hull ({(1 :: real)} <*> S)})" |
8342 then obtain s where "s \<in> S" by auto |
8311 hence *: "(c, x) : rel_interior (cone hull ({(1 :: real)} <*> S)) = |
8343 have conv: "convex ({(1 :: real)} <*> S)" |
8312 (c : rel_interior {y. f y ~= {}} & x : rel_interior (f c))" |
8344 using convex_Times[of "{(1 :: real)}" S] assms convex_singleton[of "1 :: real"] |
8313 apply (subst rel_interior_projection[of "cone hull ({(1 :: real)} <*> S)" f c x]) |
8345 by auto |
8314 using convex_cone_hull[of "{(1 :: real)} <*> S"] conv by auto |
8346 def f \<equiv> "\<lambda>y. {z. (y, z) \<in> cone hull ({1 :: real} <*> S)}" |
8315 { fix y assume "(y :: real)>=0" |
8347 then have *: "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} <*> S)) = |
8316 hence "y *\<^sub>R (1,s) : cone hull ({(1 :: real)} <*> S)" |
8348 (c \<in> rel_interior {y. f y \<noteq> {}} \<and> x \<in> rel_interior (f c))" |
8317 using cone_hull_expl[of "{(1 :: real)} <*> S"] `s:S` by auto |
8349 apply (subst rel_interior_projection[of "cone hull ({(1 :: real)} <*> S)" f c x]) |
8318 hence "f y ~= {}" using f_def by auto |
8350 using convex_cone_hull[of "{(1 :: real)} <*> S"] conv |
8319 } |
8351 apply auto |
8320 hence "{y. f y ~= {}} = {0..}" using f_def cone_hull_expl[of "{(1 :: real)} <*> S"] by auto |
8352 done |
8321 hence **: "rel_interior {y. f y ~= {}} = {0<..}" using rel_interior_real_semiline by auto |
8353 { |
8322 { fix c assume "c>(0 :: real)" |
8354 fix y :: real |
8323 hence "f c = (op *\<^sub>R c ` S)" using f_def cone_hull_expl[of "{(1 :: real)} <*> S"] by auto |
8355 assume "y \<ge> 0" |
8324 hence "rel_interior (f c)= (op *\<^sub>R c ` rel_interior S)" |
8356 then have "y *\<^sub>R (1,s) \<in> cone hull ({1 :: real} <*> S)" |
8325 using rel_interior_convex_scaleR[of S c] assms by auto |
8357 using cone_hull_expl[of "{(1 :: real)} <*> S"] `s \<in> S` by auto |
8326 } |
8358 then have "f y \<noteq> {}" |
8327 hence ?thesis using * ** by auto |
8359 using f_def by auto |
8328 } ultimately show ?thesis by blast |
8360 } |
8329 qed |
8361 then have "{y. f y \<noteq> {}} = {0..}" |
8330 |
8362 using f_def cone_hull_expl[of "{1 :: real} <*> S"] by auto |
8363 then have **: "rel_interior {y. f y \<noteq> {}} = {0<..}" |
|
8364 using rel_interior_real_semiline by auto |
|
8365 { |
|
8366 fix c :: real |
|
8367 assume "c > 0" |
|
8368 then have "f c = (op *\<^sub>R c ` S)" |
|
8369 using f_def cone_hull_expl[of "{1 :: real} <*> S"] by auto |
|
8370 then have "rel_interior (f c) = op *\<^sub>R c ` rel_interior S" |
|
8371 using rel_interior_convex_scaleR[of S c] assms by auto |
|
8372 } |
|
8373 then show ?thesis using * ** by auto |
|
8374 qed |
|
8331 |
8375 |
8332 lemma rel_interior_convex_cone: |
8376 lemma rel_interior_convex_cone: |
8333 fixes S :: "('m::euclidean_space) set" |
8377 fixes S :: "'m::euclidean_space set" |
8334 assumes "convex S" |
8378 assumes "convex S" |
8335 shows "rel_interior (cone hull ({(1 :: real)} <*> S)) = |
8379 shows "rel_interior (cone hull ({1 :: real} <*> S)) = |
8336 {(c,c *\<^sub>R x) |c x. c>0 & x : (rel_interior S)}" |
8380 {(c, c *\<^sub>R x) | c x. c > 0 \<and> x \<in> rel_interior S}" |
8337 (is "?lhs=?rhs") |
8381 (is "?lhs = ?rhs") |
8338 proof- |
8382 proof - |
8339 { fix z assume "z:?lhs" |
8383 { |
8340 have *: "z=(fst z,snd z)" by auto |
8384 fix z |
8341 have "z:?rhs" using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms `z:?lhs` apply auto |
8385 assume "z \<in> ?lhs" |
8342 apply (rule_tac x="fst z" in exI) apply (rule_tac x="x" in exI) using * by auto |
8386 have *: "z = (fst z, snd z)" |
8343 } |
8387 by auto |
8344 moreover |
8388 have "z \<in> ?rhs" |
8345 { fix z assume "z:?rhs" hence "z:?lhs" |
8389 using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms `z \<in> ?lhs` |
8346 using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms by auto |
8390 apply auto |
8347 } |
8391 apply (rule_tac x = "fst z" in exI) |
8348 ultimately show ?thesis by blast |
8392 apply (rule_tac x = x in exI) |
8393 using * |
|
8394 apply auto |
|
8395 done |
|
8396 } |
|
8397 moreover |
|
8398 { |
|
8399 fix z |
|
8400 assume "z \<in> ?rhs" |
|
8401 then have "z \<in> ?lhs" |
|
8402 using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms |
|
8403 by auto |
|
8404 } |
|
8405 ultimately show ?thesis by blast |
|
8349 qed |
8406 qed |
8350 |
8407 |
8351 lemma convex_hull_finite_union: |
8408 lemma convex_hull_finite_union: |
8352 assumes "finite I" |
8409 assumes "finite I" |
8353 assumes "!i:I. (convex (S i) & (S i) ~= {})" |
8410 assumes "\<forall>i\<in>I. convex (S i) \<and> (S i) \<noteq> {}" |
8354 shows "convex hull (Union (S ` I)) = |
8411 shows "convex hull (\<Union>(S ` I)) = |
8355 {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)}" |
8412 {setsum (\<lambda>i. c i *\<^sub>R s i) I | c s. (\<forall>i\<in>I. c i \<ge> 0) \<and> setsum c I = 1 \<and> (\<forall>i\<in>I. s i \<in> S i)}" |
8356 (is "?lhs = ?rhs") |
8413 (is "?lhs = ?rhs") |
8357 proof- |
8414 proof - |
8358 { fix x assume "x : ?rhs" |
8415 have "?lhs \<supseteq> ?rhs" |
8359 from this obtain c s |
8416 proof |
8360 where *: "setsum (%i. c i *\<^sub>R s i) I=x" "(setsum c I = 1)" |
8417 fix x |
8361 "(!i:I. c i >= 0) & (!i:I. s i : S i)" by auto |
8418 assume "x : ?rhs" |
8362 hence "!i:I. s i : convex hull (Union (S ` I))" using hull_subset[of "Union (S ` I)" convex] by auto |
8419 then obtain c s where *: "setsum (\<lambda>i. c i *\<^sub>R s i) I = x" "setsum c I = 1" |
8363 hence "x : ?lhs" unfolding *(1)[symmetric] |
8420 "(\<forall>i\<in>I. c i \<ge> 0) \<and> (\<forall>i\<in>I. s i \<in> S i)" by auto |
8364 apply (subst convex_setsum[of I "convex hull Union (S ` I)" c s]) |
8421 then have "\<forall>i\<in>I. s i \<in> convex hull (\<Union>(S ` I))" |
8365 using * assms convex_convex_hull by auto |
8422 using hull_subset[of "\<Union>(S ` I)" convex] by auto |
8366 } hence "?lhs >= ?rhs" by auto |
8423 then show "x \<in> ?lhs" |
8367 |
8424 unfolding *(1)[symmetric] |
8368 { fix i assume "i:I" |
8425 apply (subst convex_setsum[of I "convex hull \<Union>(S ` I)" c s]) |
8369 from this assms have "EX p. p : S i" by auto |
8426 using * assms convex_convex_hull |
8370 } |
8427 apply auto |
8371 from this obtain p where p_def: "!i:I. p i : S i" by metis |
8428 done |
8372 |
8429 qed |
8373 { fix i assume "i:I" |
8430 |
8374 { fix x assume "x : S i" |
8431 { |
8375 def c == "(%j. if (j=i) then (1::real) else 0)" |
8432 fix i |
8376 hence *: "setsum c I = 1" using `finite I` `i:I` setsum_delta[of I i "(%(j::'a). (1::real))"] by auto |
8433 assume "i \<in> I" |
8377 def s == "(%j. if (j=i) then x else p j)" |
8434 with assms have "\<exists>p. p \<in> S i" by auto |
8378 hence "!j. c j *\<^sub>R s j = (if (j=i) then x else 0)" using c_def by (auto simp add: algebra_simps) |
8435 } |
8379 hence "x = setsum (%i. c i *\<^sub>R s i) I" |
8436 then obtain p where p: "\<forall>i\<in>I. p i \<in> S i" by metis |
8380 using s_def c_def `finite I` `i:I` setsum_delta[of I i "(%(j::'a). x)"] by auto |
8437 |
8381 hence "x : ?rhs" apply auto |
8438 { |
8382 apply (rule_tac x="c" in exI) |
8439 fix i |
8383 apply (rule_tac x="s" in exI) using * c_def s_def p_def `x : S i` by auto |
8440 assume "i \<in> I" |
8384 } hence "?rhs >= S i" by auto |
8441 { |
8385 } hence *: "?rhs >= Union (S ` I)" by auto |
8442 fix x |
8386 |
8443 assume "x \<in> S i" |
8387 { fix u v assume uv: "(u :: real)>=0 & v>=0 & u+v=1" |
8444 def c \<equiv> "\<lambda>j. if j = i then 1::real else 0" |
8388 fix x y assume xy: "(x : ?rhs) & (y : ?rhs)" |
8445 then have *: "setsum c I = 1" |
8389 from xy obtain c s where xc: "x=setsum (%i. c i *\<^sub>R s i) I & |
8446 using `finite I` `i \<in> I` setsum_delta[of I i "\<lambda>j::'a. 1::real"] |
8390 (!i:I. c i >= 0) & (setsum c I = 1) & (!i:I. s i : S i)" by auto |
8447 by auto |
8391 from xy obtain d t where yc: "y=setsum (%i. d i *\<^sub>R t i) I & |
8448 def s \<equiv> "\<lambda>j. if j = i then x else p j" |
8392 (!i:I. d i >= 0) & (setsum d I = 1) & (!i:I. t i : S i)" by auto |
8449 then have "\<forall>j. c j *\<^sub>R s j = (if j = i then x else 0)" |
8393 def e == "(%i. u * (c i)+v * (d i))" |
8450 using c_def by (auto simp add: algebra_simps) |
8394 have ge0: "!i:I. e i >= 0" using e_def xc yc uv by (simp add: mult_nonneg_nonneg) |
8451 then have "x = setsum (\<lambda>i. c i *\<^sub>R s i) I" |
8395 have "setsum (%i. u * c i) I = u * setsum c I" by (simp add: setsum_right_distrib) |
8452 using s_def c_def `finite I` `i \<in> I` setsum_delta[of I i "\<lambda>j::'a. x"] |
8396 moreover have "setsum (%i. v * d i) I = v * setsum d I" by (simp add: setsum_right_distrib) |
8453 by auto |
8397 ultimately have sum1: "setsum e I = 1" using e_def xc yc uv by (simp add: setsum_addf) |
8454 then have "x \<in> ?rhs" |
8398 def q == "(%i. if (e i = 0) then (p i) |
8455 apply auto |
8399 else (u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i))" |
8456 apply (rule_tac x = c in exI) |
8400 { fix i assume "i:I" |
8457 apply (rule_tac x = s in exI) |
8401 { assume "e i = 0" hence "q i : S i" using `i:I` p_def q_def by auto } |
8458 using * c_def s_def p `x \<in> S i` |
8402 moreover |
8459 apply auto |
8403 { assume "e i ~= 0" |
8460 done |
8404 hence "q i : S i" using mem_convex_alt[of "S i" "s i" "t i" "u * (c i)" "v * (d i)"] |
|
8405 mult_nonneg_nonneg[of u "c i"] mult_nonneg_nonneg[of v "d i"] |
|
8406 assms q_def e_def `i:I` `e i ~= 0` xc yc uv by auto |
|
8407 } ultimately have "q i : S i" by auto |
|
8408 } hence qs: "!i:I. q i : S i" by auto |
|
8409 { fix i assume "i:I" |
|
8410 { assume "e i = 0" |
|
8411 have ge: "u * (c i) >= 0 & v * (d i) >= 0" using xc yc uv `i:I` by (simp add: mult_nonneg_nonneg) |
|
8412 moreover from ge have "u * (c i) <= 0 & v * (d i) <= 0" using `e i = 0` e_def `i:I` by simp |
|
8413 ultimately have "u * (c i) = 0 & v * (d i) = 0" by auto |
|
8414 hence "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)" |
|
8415 using `e i = 0` by auto |
|
8416 } |
8461 } |
8417 moreover |
8462 then have "?rhs \<supseteq> S i" by auto |
8418 { assume "e i ~= 0" |
8463 } |
8419 hence "(u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i) = q i" |
8464 then have *: "?rhs \<supseteq> \<Union>(S ` I)" by auto |
8420 using q_def by auto |
8465 |
8421 hence "e i *\<^sub>R ((u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i)) |
8466 { |
8422 = (e i) *\<^sub>R (q i)" by auto |
8467 fix u v :: real |
8423 hence "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)" |
8468 assume uv: "u \<ge> 0 \<and> v \<ge> 0 \<and> u + v = 1" |
8424 using `e i ~= 0` by (simp add: algebra_simps) |
8469 fix x y |
8425 } ultimately have |
8470 assume xy: "x \<in> ?rhs \<and> y \<in> ?rhs" |
8426 "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)" by blast |
8471 from xy obtain c s where |
8427 } hence *: "!i:I. |
8472 xc: "x = setsum (\<lambda>i. c i *\<^sub>R s i) I \<and> (\<forall>i\<in>I. c i \<ge> 0) \<and> setsum c I = 1 \<and> (\<forall>i\<in>I. s i \<in> S i)" |
8428 (u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)" by auto |
8473 by auto |
8429 have "u *\<^sub>R x + v *\<^sub>R y = |
8474 from xy obtain d t where |
8430 setsum (%i. (u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i)) I" |
8475 yc: "y = setsum (\<lambda>i. d i *\<^sub>R t i) I \<and> (\<forall>i\<in>I. d i \<ge> 0) \<and> setsum d I = 1 \<and> (\<forall>i\<in>I. t i \<in> S i)" |
8431 using xc yc by (simp add: algebra_simps scaleR_right.setsum setsum_addf) |
8476 by auto |
8432 also have "...=setsum (%i. (e i) *\<^sub>R (q i)) I" using * by auto |
8477 def e \<equiv> "\<lambda>i. u * c i + v * d i" |
8433 finally have "u *\<^sub>R x + v *\<^sub>R y = setsum (%i. (e i) *\<^sub>R (q i)) I" by auto |
8478 have ge0: "\<forall>i\<in>I. e i \<ge> 0" |
8434 hence "u *\<^sub>R x + v *\<^sub>R y : ?rhs" using ge0 sum1 qs by auto |
8479 using e_def xc yc uv by (simp add: mult_nonneg_nonneg) |
8435 } hence "convex ?rhs" unfolding convex_def by auto |
8480 have "setsum (\<lambda>i. u * c i) I = u * setsum c I" |
8436 from this show ?thesis using `?lhs >= ?rhs` * |
8481 by (simp add: setsum_right_distrib) |
8437 hull_minimal[of "Union (S ` I)" "?rhs" "convex"] by blast |
8482 moreover have "setsum (\<lambda>i. v * d i) I = v * setsum d I" |
8483 by (simp add: setsum_right_distrib) |
|
8484 ultimately have sum1: "setsum e I = 1" |
|
8485 using e_def xc yc uv by (simp add: setsum_addf) |
|
8486 def q \<equiv> "\<lambda>i. if e i = 0 then p i else (u * c i / e i) *\<^sub>R s i + (v * d i / e i) *\<^sub>R t i" |
|
8487 { |
|
8488 fix i |
|
8489 assume i: "i \<in> I" |
|
8490 have "q i \<in> S i" |
|
8491 proof (cases "e i = 0") |
|
8492 case True |
|
8493 then show ?thesis using i p q_def by auto |
|
8494 next |
|
8495 case False |
|
8496 then show ?thesis |
|
8497 using mem_convex_alt[of "S i" "s i" "t i" "u * (c i)" "v * (d i)"] |
|
8498 mult_nonneg_nonneg[of u "c i"] mult_nonneg_nonneg[of v "d i"] |
|
8499 assms q_def e_def i False xc yc uv |
|
8500 by auto |
|
8501 qed |
|
8502 } |
|
8503 then have qs: "\<forall>i\<in>I. q i \<in> S i" by auto |
|
8504 { |
|
8505 fix i |
|
8506 assume i: "i \<in> I" |
|
8507 have "(u * c i) *\<^sub>R s i + (v * d i) *\<^sub>R t i = e i *\<^sub>R q i" |
|
8508 proof (cases "e i = 0") |
|
8509 case True |
|
8510 have ge: "u * (c i) \<ge> 0 \<and> v * d i \<ge> 0" |
|
8511 using xc yc uv i by (simp add: mult_nonneg_nonneg) |
|
8512 moreover from ge have "u * c i \<le> 0 \<and> v * d i \<le> 0" |
|
8513 using True e_def i by simp |
|
8514 ultimately have "u * c i = 0 \<and> v * d i = 0" by auto |
|
8515 with True show ?thesis by auto |
|
8516 next |
|
8517 case False |
|
8518 then have "(u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i) = q i" |
|
8519 using q_def by auto |
|
8520 then have "e i *\<^sub>R ((u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i)) |
|
8521 = (e i) *\<^sub>R (q i)" by auto |
|
8522 with False show ?thesis by (simp add: algebra_simps) |
|
8523 qed |
|
8524 } |
|
8525 then have *: "\<forall>i\<in>I. (u * c i) *\<^sub>R s i + (v * d i) *\<^sub>R t i = e i *\<^sub>R q i" |
|
8526 by auto |
|
8527 have "u *\<^sub>R x + v *\<^sub>R y = setsum (\<lambda>i. (u * c i) *\<^sub>R s i + (v * d i) *\<^sub>R t i) I" |
|
8528 using xc yc by (simp add: algebra_simps scaleR_right.setsum setsum_addf) |
|
8529 also have "\<dots> = setsum (\<lambda>i. e i *\<^sub>R q i) I" |
|
8530 using * by auto |
|
8531 finally have "u *\<^sub>R x + v *\<^sub>R y = setsum (\<lambda>i. (e i) *\<^sub>R (q i)) I" |
|
8532 by auto |
|
8533 then have "u *\<^sub>R x + v *\<^sub>R y \<in> ?rhs" |
|
8534 using ge0 sum1 qs by auto |
|
8535 } |
|
8536 then have "convex ?rhs" unfolding convex_def by auto |
|
8537 then show ?thesis |
|
8538 using `?lhs \<supseteq> ?rhs` * hull_minimal[of "\<Union>(S ` I)" ?rhs convex] |
|
8539 by blast |
|
8438 qed |
8540 qed |
8439 |
8541 |
8440 lemma convex_hull_union_two: |
8542 lemma convex_hull_union_two: |
8441 fixes S T :: "('m::euclidean_space) set" |
8543 fixes S T :: "'m::euclidean_space set" |
8442 assumes "convex S" "S ~= {}" "convex T" "T ~= {}" |
8544 assumes "convex S" |
8443 shows "convex hull (S Un T) = {u *\<^sub>R s + v *\<^sub>R t |u v s t. u>=0 & v>=0 & u+v=1 & s:S & t:T}" |
8545 and "S \<noteq> {}" |
8546 and "convex T" |
|
8547 and "T \<noteq> {}" |
|
8548 shows "convex hull (S \<union> T) = |
|
8549 {u *\<^sub>R s + v *\<^sub>R t | u v s t. u \<ge> 0 \<and> v \<ge> 0 \<and> u + v = 1 \<and> s \<in> S \<and> t \<in> T}" |
|
8444 (is "?lhs = ?rhs") |
8550 (is "?lhs = ?rhs") |
8445 proof- |
8551 proof |
8446 def I == "{(1::nat),2}" |
8552 def I \<equiv> "{1::nat, 2}" |
8447 def s == "(%i. (if i=(1::nat) then S else T))" |
8553 def s \<equiv> "\<lambda>i. if i = (1::nat) then S else T" |
8448 have "Union (s ` I) = S Un T" using s_def I_def by auto |
8554 have "\<Union>(s ` I) = S \<union> T" |
8449 hence "convex hull (Union (s ` I)) = convex hull (S Un T)" by auto |
8555 using s_def I_def by auto |
8450 moreover have "convex hull Union (s ` I) = |
8556 then have "convex hull (\<Union>(s ` I)) = convex hull (S \<union> T)" |
8451 {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)}" |
8557 by auto |
8452 apply (subst convex_hull_finite_union[of I s]) using assms s_def I_def by auto |
8558 moreover have "convex hull \<Union>(s ` I) = |
8453 moreover have |
8559 {\<Sum> i\<in>I. c i *\<^sub>R sa i | c sa. (\<forall>i\<in>I. 0 \<le> c i) \<and> setsum c I = 1 \<and> (\<forall>i\<in>I. sa i \<in> s i)}" |
8454 "{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)} <= |
8560 apply (subst convex_hull_finite_union[of I s]) |
8455 ?rhs" |
8561 using assms s_def I_def |
8456 using s_def I_def by auto |
8562 apply auto |
8457 ultimately have "?lhs<=?rhs" by auto |
8563 done |
8458 { fix x assume "x : ?rhs" |
8564 moreover have |
8459 from this obtain u v s t |
8565 "{\<Sum>i\<in>I. c i *\<^sub>R sa i | c sa. (\<forall>i\<in>I. 0 \<le> c i) \<and> setsum c I = 1 \<and> (\<forall>i\<in>I. sa i \<in> s i)} \<le> ?rhs" |
8460 where *: "x=u *\<^sub>R s + v *\<^sub>R t & u>=0 & v>=0 & u+v=1 & s:S & t:T" by auto |
8566 using s_def I_def by auto |
8461 hence "x : convex hull {s,t}" using convex_hull_2[of s t] by auto |
8567 ultimately show "?lhs \<subseteq> ?rhs" by auto |
8462 hence "x : convex hull (S Un T)" using * hull_mono[of "{s, t}" "S Un T"] by auto |
8568 { |
8463 } hence "?lhs >= ?rhs" by blast |
8569 fix x |
8464 from this show ?thesis using `?lhs<=?rhs` by auto |
8570 assume "x \<in> ?rhs" |
8465 qed |
8571 then obtain u v s t where *: "x = u *\<^sub>R s + v *\<^sub>R t \<and> u \<ge> 0 \<and> v \<ge> 0 \<and> u + v = 1 \<and> s \<in> S \<and> t \<in> T" |
8572 by auto |
|
8573 then have "x \<in> convex hull {s, t}" |
|
8574 using convex_hull_2[of s t] by auto |
|
8575 then have "x \<in> convex hull (S \<union> T)" |
|
8576 using * hull_mono[of "{s, t}" "S \<union> T"] by auto |
|
8577 } |
|
8578 then show "?lhs \<supseteq> ?rhs" by blast |
|
8579 qed |
|
8580 |
|
8466 |
8581 |
8467 subsection {* Convexity on direct sums *} |
8582 subsection {* Convexity on direct sums *} |
8468 |
8583 |
8469 lemma closure_sum: |
8584 lemma closure_sum: |
8470 fixes S T :: "('n::euclidean_space) set" |
8585 fixes S T :: "'n::euclidean_space set" |
8471 shows "closure S + closure T \<subseteq> closure (S + T)" |
8586 shows "closure S + closure T \<subseteq> closure (S + T)" |
8472 proof- |
8587 proof - |
8473 have "(closure S) + (closure T) = (\<lambda>(x,y). x + y) ` (closure S \<times> closure T)" |
8588 have "closure S + closure T = (\<lambda>(x,y). x + y) ` (closure S \<times> closure T)" |
8474 by (simp add: set_plus_image) |
8589 by (simp add: set_plus_image) |
8475 also have "... = (\<lambda>(x,y). x + y) ` closure (S \<times> T)" |
8590 also have "\<dots> = (\<lambda>(x,y). x + y) ` closure (S \<times> T)" |
8476 using closure_Times by auto |
8591 using closure_Times by auto |
8477 also have "... \<subseteq> closure (S + T)" |
8592 also have "\<dots> \<subseteq> closure (S + T)" |
8478 using fst_snd_linear closure_linear_image[of "(\<lambda>(x,y). x + y)" "S \<times> T"] |
8593 using fst_snd_linear closure_linear_image[of "(\<lambda>(x,y). x + y)" "S \<times> T"] |
8479 by (auto simp: set_plus_image) |
8594 by (auto simp: set_plus_image) |
8480 finally show ?thesis |
8595 finally show ?thesis |
8481 by auto |
8596 by auto |
8482 qed |
8597 qed |
8483 |
8598 |
8484 lemma convex_oplus: |
8599 lemma convex_oplus: |
8485 fixes S T :: "('n::euclidean_space) set" |
8600 fixes S T :: "'n::euclidean_space set" |
8486 assumes "convex S" "convex T" |
8601 assumes "convex S" |
8487 shows "convex (S + T)" |
8602 and "convex T" |
8488 proof- |
8603 shows "convex (S + T)" |
8489 have "{x + y |x y. x : S & y : T} = {c. EX a:S. EX b:T. c = a + b}" by auto |
8604 proof - |
8490 thus ?thesis unfolding set_plus_def using convex_sums[of S T] assms by auto |
8605 have "{x + y |x y. x \<in> S \<and> y \<in> T} = {c. \<exists>a\<in>S. \<exists>b\<in>T. c = a + b}" |
8606 by auto |
|
8607 then show ?thesis |
|
8608 unfolding set_plus_def |
|
8609 using convex_sums[of S T] assms |
|
8610 by auto |
|
8491 qed |
8611 qed |
8492 |
8612 |
8493 lemma convex_hull_sum: |
8613 lemma convex_hull_sum: |
8494 fixes S T :: "('n::euclidean_space) set" |
8614 fixes S T :: "'n::euclidean_space set" |
8495 shows "convex hull (S + T) = (convex hull S) + (convex hull T)" |
8615 shows "convex hull (S + T) = convex hull S + convex hull T" |
8496 proof- |
8616 proof - |
8497 have "(convex hull S) + (convex hull T) = |
8617 have "convex hull S + convex hull T = (\<lambda>(x,y). x + y) ` ((convex hull S) <*> (convex hull T))" |
8498 (%(x,y). x + y) ` ((convex hull S) <*> (convex hull T))" |
8618 by (simp add: set_plus_image) |
8499 by (simp add: set_plus_image) |
8619 also have "\<dots> = (\<lambda>(x,y). x + y) ` (convex hull (S <*> T))" |
8500 also have "... = (%(x,y). x + y) ` (convex hull (S <*> T))" using convex_hull_Times by auto |
8620 using convex_hull_Times by auto |
8501 also have "...= convex hull (S + T)" using fst_snd_linear linear_conv_bounded_linear |
8621 also have "\<dots> = convex hull (S + T)" |
8502 convex_hull_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image) |
8622 using fst_snd_linear linear_conv_bounded_linear |
8503 finally show ?thesis by auto |
8623 convex_hull_linear_image[of "(\<lambda>(x,y). x + y)" "S <*> T"] |
8624 by (auto simp add: set_plus_image) |
|
8625 finally show ?thesis .. |
|
8504 qed |
8626 qed |
8505 |
8627 |
8506 lemma rel_interior_sum: |
8628 lemma rel_interior_sum: |
8507 fixes S T :: "('n::euclidean_space) set" |
8629 fixes S T :: "'n::euclidean_space set" |
8508 assumes "convex S" "convex T" |
8630 assumes "convex S" |
8509 shows "rel_interior (S + T) = (rel_interior S) + (rel_interior T)" |
8631 and "convex T" |
8510 proof- |
8632 shows "rel_interior (S + T) = rel_interior S + rel_interior T" |
8511 have "(rel_interior S) + (rel_interior T) = (%(x,y). x + y) ` (rel_interior S <*> rel_interior T)" |
8633 proof - |
8512 by (simp add: set_plus_image) |
8634 have "rel_interior S + rel_interior T = (\<lambda>(x,y). x + y) ` (rel_interior S <*> rel_interior T)" |
8513 also have "... = (%(x,y). x + y) ` rel_interior (S <*> T)" using rel_interior_direct_sum assms by auto |
8635 by (simp add: set_plus_image) |
8514 also have "...= rel_interior (S + T)" using fst_snd_linear convex_Times assms |
8636 also have "\<dots> = (\<lambda>(x,y). x + y) ` rel_interior (S <*> T)" |
8515 rel_interior_convex_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image) |
8637 using rel_interior_direct_sum assms by auto |
8516 finally show ?thesis by auto |
8638 also have "\<dots> = rel_interior (S + T)" |
8639 using fst_snd_linear convex_Times assms |
|
8640 rel_interior_convex_linear_image[of "(\<lambda>(x,y). x + y)" "S <*> T"] |
|
8641 by (auto simp add: set_plus_image) |
|
8642 finally show ?thesis .. |
|
8517 qed |
8643 qed |
8518 |
8644 |
8519 lemma convex_sum_gen: |
8645 lemma convex_sum_gen: |
8520 fixes S :: "'a \<Rightarrow> 'n::euclidean_space set" |
8646 fixes S :: "'a \<Rightarrow> 'n::euclidean_space set" |
8521 assumes "\<And>i. i \<in> I \<Longrightarrow> (convex (S i))" |
8647 assumes "\<And>i. i \<in> I \<Longrightarrow> (convex (S i))" |
8522 shows "convex (setsum S I)" |
8648 shows "convex (setsum S I)" |
8523 proof cases |
8649 proof (cases "finite I") |
8524 assume "finite I" from this assms show ?thesis |
8650 case True |
8651 from this and assms show ?thesis |
|
8525 by induct (auto simp: convex_oplus) |
8652 by induct (auto simp: convex_oplus) |
8526 qed auto |
8653 next |
8654 case False |
|
8655 then show ?thesis by auto |
|
8656 qed |
|
8527 |
8657 |
8528 lemma convex_hull_sum_gen: |
8658 lemma convex_hull_sum_gen: |
8529 fixes S :: "'a => ('n::euclidean_space) set" |
8659 fixes S :: "'a \<Rightarrow> 'n::euclidean_space set" |
8530 shows "convex hull (setsum S I) = setsum (%i. (convex hull (S i))) I" |
8660 shows "convex hull (setsum S I) = setsum (\<lambda>i. convex hull (S i)) I" |
8531 apply (subst setsum_set_linear) using convex_hull_sum convex_hull_singleton by auto |
8661 apply (subst setsum_set_linear) |
8532 |
8662 using convex_hull_sum convex_hull_singleton |
8663 apply auto |
|
8664 done |
|
8533 |
8665 |
8534 lemma rel_interior_sum_gen: |
8666 lemma rel_interior_sum_gen: |
8535 fixes S :: "'a => ('n::euclidean_space) set" |
8667 fixes S :: "'a \<Rightarrow> 'n::euclidean_space set" |
8536 assumes "!i:I. (convex (S i))" |
8668 assumes "\<forall>i\<in>I. convex (S i)" |
8537 shows "rel_interior (setsum S I) = setsum (%i. (rel_interior (S i))) I" |
8669 shows "rel_interior (setsum S I) = setsum (\<lambda>i. rel_interior (S i)) I" |
8538 apply (subst setsum_set_cond_linear[of convex]) |
8670 apply (subst setsum_set_cond_linear[of convex]) |
8539 using rel_interior_sum rel_interior_sing[of "0"] assms by (auto simp add: convex_oplus) |
8671 using rel_interior_sum rel_interior_sing[of "0"] assms |
8672 apply (auto simp add: convex_oplus) |
|
8673 done |
|
8540 |
8674 |
8541 lemma convex_rel_open_direct_sum: |
8675 lemma convex_rel_open_direct_sum: |
8542 fixes S T :: "('n::euclidean_space) set" |
8676 fixes S T :: "'n::euclidean_space set" |
8543 assumes "convex S" "rel_open S" "convex T" "rel_open T" |
8677 assumes "convex S" |
8544 shows "convex (S <*> T) & rel_open (S <*> T)" |
8678 and "rel_open S" |
8545 by (metis assms convex_Times rel_interior_direct_sum rel_open_def) |
8679 and "convex T" |
8680 and "rel_open T" |
|
8681 shows "convex (S <*> T) \<and> rel_open (S <*> T)" |
|
8682 by (metis assms convex_Times rel_interior_direct_sum rel_open_def) |
|
8546 |
8683 |
8547 lemma convex_rel_open_sum: |
8684 lemma convex_rel_open_sum: |
8548 fixes S T :: "('n::euclidean_space) set" |
8685 fixes S T :: "'n::euclidean_space set" |
8549 assumes "convex S" "rel_open S" "convex T" "rel_open T" |
8686 assumes "convex S" |
8550 shows "convex (S + T) & rel_open (S + T)" |
8687 and "rel_open S" |
8551 by (metis assms convex_oplus rel_interior_sum rel_open_def) |
8688 and "convex T" |
8689 and "rel_open T" |
|
8690 shows "convex (S + T) \<and> rel_open (S + T)" |
|
8691 by (metis assms convex_oplus rel_interior_sum rel_open_def) |
|
8552 |
8692 |
8553 lemma convex_hull_finite_union_cones: |
8693 lemma convex_hull_finite_union_cones: |
8554 assumes "finite I" "I ~= {}" |
8694 assumes "finite I" |
8555 assumes "!i:I. (convex (S i) & cone (S i) & (S i) ~= {})" |
8695 and "I \<noteq> {}" |
8556 shows "convex hull (Union (S ` I)) = setsum S I" |
8696 assumes "\<forall>i\<in>I. convex (S i) \<and> cone (S i) \<and> S i \<noteq> {}" |
8697 shows "convex hull (\<Union>(S ` I)) = setsum S I" |
|
8557 (is "?lhs = ?rhs") |
8698 (is "?lhs = ?rhs") |
8558 proof- |
8699 proof - |
8559 { fix x assume "x : ?lhs" |
8700 { |
8560 from this obtain c xs where x_def: "x=setsum (%i. c i *\<^sub>R xs i) I & |
8701 fix x |
8561 (!i:I. c i >= 0) & (setsum c I = 1) & (!i:I. xs i : S i)" |
8702 assume "x \<in> ?lhs" |
8562 using convex_hull_finite_union[of I S] assms by auto |
8703 then obtain c xs where |
8563 def s == "(%i. c i *\<^sub>R xs i)" |
8704 x: "x = setsum (\<lambda>i. c i *\<^sub>R xs i) I \<and> (\<forall>i\<in>I. c i \<ge> 0) \<and> setsum c I = 1 \<and> (\<forall>i\<in>I. xs i \<in> S i)" |
8564 { fix i assume "i:I" |
8705 using convex_hull_finite_union[of I S] assms by auto |
8565 hence "s i : S i" using s_def x_def assms mem_cone[of "S i" "xs i" "c i"] by auto |
8706 def s \<equiv> "\<lambda>i. c i *\<^sub>R xs i" |
8566 } hence "!i:I. s i : S i" by auto |
8707 { |
8567 moreover have "x = setsum s I" using x_def s_def by auto |
8708 fix i |
8568 ultimately have "x : ?rhs" using set_setsum_alt[of I S] assms by auto |
8709 assume "i \<in> I" |
8569 } |
8710 then have "s i \<in> S i" |
8570 moreover |
8711 using s_def x assms mem_cone[of "S i" "xs i" "c i"] by auto |
8571 { fix x assume "x : ?rhs" |
|
8572 from this obtain s where x_def: "x=setsum s I & (!i:I. s i : S i)" |
|
8573 using set_setsum_alt[of I S] assms by auto |
|
8574 def xs == "(%i. of_nat(card I) *\<^sub>R s i)" |
|
8575 hence "x=setsum (%i. ((1 :: real)/of_nat(card I)) *\<^sub>R xs i) I" using x_def assms by auto |
|
8576 moreover have "!i:I. xs i : S i" using x_def xs_def assms by (simp add: cone_def) |
|
8577 moreover have "(!i:I. (1 :: real)/of_nat(card I) >= 0)" by auto |
|
8578 moreover have "setsum (%i. (1 :: real)/of_nat(card I)) I = 1" using assms by auto |
|
8579 ultimately have "x : ?lhs" apply (subst convex_hull_finite_union[of I S]) |
|
8580 using assms apply blast |
|
8581 using assms apply blast |
|
8582 apply rule apply (rule_tac x="(%i. (1 :: real)/of_nat(card I))" in exI) by auto |
|
8583 } ultimately show ?thesis by auto |
|
8584 qed |
|
8585 |
|
8586 lemma convex_hull_union_cones_two: |
|
8587 fixes S T :: "('m::euclidean_space) set" |
|
8588 assumes "convex S" "cone S" "S ~= {}" |
|
8589 assumes "convex T" "cone T" "T ~= {}" |
|
8590 shows "convex hull (S Un T) = S + T" |
|
8591 proof- |
|
8592 def I == "{(1::nat),2}" |
|
8593 def A == "(%i. (if i=(1::nat) then S else T))" |
|
8594 have "Union (A ` I) = S Un T" using A_def I_def by auto |
|
8595 hence "convex hull (Union (A ` I)) = convex hull (S Un T)" by auto |
|
8596 moreover have "convex hull Union (A ` I) = setsum A I" |
|
8597 apply (subst convex_hull_finite_union_cones[of I A]) using assms A_def I_def by auto |
|
8598 moreover have |
|
8599 "setsum A I = S + T" using A_def I_def |
|
8600 unfolding set_plus_def apply auto unfolding set_plus_def by auto |
|
8601 ultimately show ?thesis by auto |
|
8602 qed |
|
8603 |
|
8604 lemma rel_interior_convex_hull_union: |
|
8605 fixes S :: "'a => ('n::euclidean_space) set" |
|
8606 assumes "finite I" |
|
8607 assumes "!i:I. convex (S i) & (S i) ~= {}" |
|
8608 shows "rel_interior (convex hull (Union (S ` I))) = {setsum (%i. c i *\<^sub>R s i) I |
|
8609 |c s. (!i:I. c i > 0) & (setsum c I = 1) & (!i:I. s i : rel_interior(S i))}" |
|
8610 (is "?lhs=?rhs") |
|
8611 proof- |
|
8612 { assume "I={}" hence ?thesis using convex_hull_empty rel_interior_empty by auto } |
|
8613 moreover |
|
8614 { assume "I ~= {}" |
|
8615 def C0 == "convex hull (Union (S ` I))" |
|
8616 have "!i:I. C0 >= S i" unfolding C0_def using hull_subset[of "Union (S ` I)"] by auto |
|
8617 def K0 == "cone hull ({(1 :: real)} <*> C0)" |
|
8618 def K == "(%i. cone hull ({(1 :: real)} <*> (S i)))" |
|
8619 have "!i:I. K i ~= {}" unfolding K_def using assms by (simp add: cone_hull_empty_iff[symmetric]) |
|
8620 { fix i assume "i:I" |
|
8621 hence "convex (K i)" unfolding K_def apply (subst convex_cone_hull) apply (subst convex_Times) |
|
8622 using assms by auto |
|
8623 } |
|
8624 hence convK: "!i:I. convex (K i)" by auto |
|
8625 { fix i assume "i:I" |
|
8626 hence "K0 >= K i" unfolding K0_def K_def apply (subst hull_mono) using `!i:I. C0 >= S i` by auto |
|
8627 } |
|
8628 hence "K0 >= Union (K ` I)" by auto |
|
8629 moreover have "convex K0" unfolding K0_def |
|
8630 apply (subst convex_cone_hull) apply (subst convex_Times) |
|
8631 unfolding C0_def using convex_convex_hull by auto |
|
8632 ultimately have geq: "K0 >= convex hull (Union (K ` I))" using hull_minimal[of _ "K0" "convex"] by blast |
|
8633 have "!i:I. K i >= {(1 :: real)} <*> (S i)" using K_def by (simp add: hull_subset) |
|
8634 hence "Union (K ` I) >= {(1 :: real)} <*> Union (S ` I)" by auto |
|
8635 hence "convex hull Union (K ` I) >= convex hull ({(1 :: real)} <*> Union (S ` I))" by (simp add: hull_mono) |
|
8636 hence "convex hull Union (K ` I) >= {(1 :: real)} <*> C0" unfolding C0_def |
|
8637 using convex_hull_Times[of "{(1 :: real)}" "Union (S ` I)"] convex_hull_singleton by auto |
|
8638 moreover have "cone (convex hull(Union (K ` I)))" apply (subst cone_convex_hull) |
|
8639 using cone_Union[of "K ` I"] apply auto unfolding K_def using cone_cone_hull by auto |
|
8640 ultimately have "convex hull (Union (K ` I)) >= K0" |
|
8641 unfolding K0_def using hull_minimal[of _ "convex hull (Union (K ` I))" "cone"] by blast |
|
8642 hence "K0 = convex hull (Union (K ` I))" using geq by auto |
|
8643 also have "...=setsum K I" |
|
8644 apply (subst convex_hull_finite_union_cones[of I K]) |
|
8645 using assms apply blast |
|
8646 using `I ~= {}` apply blast |
|
8647 unfolding K_def apply rule |
|
8648 apply (subst convex_cone_hull) apply (subst convex_Times) |
|
8649 using assms cone_cone_hull `!i:I. K i ~= {}` K_def by auto |
|
8650 finally have "K0 = setsum K I" by auto |
|
8651 hence *: "rel_interior K0 = setsum (%i. (rel_interior (K i))) I" |
|
8652 using rel_interior_sum_gen[of I K] convK by auto |
|
8653 { fix x assume "x : ?lhs" |
|
8654 hence "((1::real),x) : rel_interior K0" using K0_def C0_def |
|
8655 rel_interior_convex_cone_aux[of C0 "(1::real)" x] convex_convex_hull by auto |
|
8656 from this obtain k where k_def: "((1::real),x) = setsum k I & (!i:I. k i : rel_interior (K i))" |
|
8657 using `finite I` * set_setsum_alt[of I "(%i. rel_interior (K i))"] by auto |
|
8658 { fix i assume "i:I" |
|
8659 hence "(convex (S i)) & k i : rel_interior (cone hull {1} <*> S i)" using k_def K_def assms by auto |
|
8660 hence "EX ci si. k i = (ci, ci *\<^sub>R si) & 0 < ci & si : rel_interior (S i)" |
|
8661 using rel_interior_convex_cone[of "S i"] by auto |
|
8662 } |
8712 } |
8663 from this obtain c s where cs_def: "!i:I. (k i = (c i, c i *\<^sub>R s i) & 0 < c i |
8713 then have "\<forall>i\<in>I. s i \<in> S i" by auto |
8664 & s i : rel_interior (S i))" by metis |
8714 moreover have "x = setsum s I" using x s_def by auto |
8665 hence "x = (SUM i:I. c i *\<^sub>R s i) & setsum c I = 1" using k_def by (simp add: setsum_prod) |
8715 ultimately have "x \<in> ?rhs" |
8666 hence "x : ?rhs" using k_def apply auto |
8716 using set_setsum_alt[of I S] assms by auto |
8667 apply (rule_tac x="c" in exI) apply (rule_tac x="s" in exI) using cs_def by auto |
|
8668 } |
8717 } |
8669 moreover |
8718 moreover |
8670 { fix x assume "x : ?rhs" |
8719 { |
8671 from this obtain c s where cs_def: "x=setsum (%i. c i *\<^sub>R s i) I & |
8720 fix x |
8672 (!i:I. c i > 0) & (setsum c I = 1) & (!i:I. s i : rel_interior(S i))" by auto |
8721 assume "x \<in> ?rhs" |
8673 def k == "(%i. (c i, c i *\<^sub>R s i))" |
8722 then obtain s where x: "x = setsum s I \<and> (\<forall>i\<in>I. s i \<in> S i)" |
8674 { fix i assume "i:I" |
8723 using set_setsum_alt[of I S] assms by auto |
8675 hence "k i : rel_interior (K i)" |
8724 def xs \<equiv> "\<lambda>i. of_nat(card I) *\<^sub>R s i" |
8676 using k_def K_def assms cs_def rel_interior_convex_cone[of "S i"] by auto |
8725 then have "x = setsum (\<lambda>i. ((1 :: real) / of_nat(card I)) *\<^sub>R xs i) I" |
8726 using x assms by auto |
|
8727 moreover have "\<forall>i\<in>I. xs i \<in> S i" |
|
8728 using x xs_def assms by (simp add: cone_def) |
|
8729 moreover have "\<forall>i\<in>I. (1 :: real) / of_nat (card I) \<ge> 0" |
|
8730 by auto |
|
8731 moreover have "setsum (\<lambda>i. (1 :: real) / of_nat (card I)) I = 1" |
|
8732 using assms by auto |
|
8733 ultimately have "x \<in> ?lhs" |
|
8734 apply (subst convex_hull_finite_union[of I S]) |
|
8735 using assms |
|
8736 apply blast |
|
8737 using assms |
|
8738 apply blast |
|
8739 apply rule |
|
8740 apply (rule_tac x = "(\<lambda>i. (1 :: real) / of_nat (card I))" in exI) |
|
8741 apply auto |
|
8742 done |
|
8743 } |
|
8744 ultimately show ?thesis by auto |
|
8745 qed |
|
8746 |
|
8747 lemma convex_hull_union_cones_two: |
|
8748 fixes S T :: "'m::euclidean_space set" |
|
8749 assumes "convex S" |
|
8750 and "cone S" |
|
8751 and "S \<noteq> {}" |
|
8752 assumes "convex T" |
|
8753 and "cone T" |
|
8754 and "T \<noteq> {}" |
|
8755 shows "convex hull (S \<union> T) = S + T" |
|
8756 proof - |
|
8757 def I \<equiv> "{1::nat, 2}" |
|
8758 def A \<equiv> "(\<lambda>i. if i = (1::nat) then S else T)" |
|
8759 have "\<Union>(A ` I) = S \<union> T" |
|
8760 using A_def I_def by auto |
|
8761 then have "convex hull (\<Union>(A ` I)) = convex hull (S \<union> T)" |
|
8762 by auto |
|
8763 moreover have "convex hull \<Union>(A ` I) = setsum A I" |
|
8764 apply (subst convex_hull_finite_union_cones[of I A]) |
|
8765 using assms A_def I_def |
|
8766 apply auto |
|
8767 done |
|
8768 moreover have "setsum A I = S + T" |
|
8769 using A_def I_def |
|
8770 unfolding set_plus_def |
|
8771 apply auto |
|
8772 unfolding set_plus_def |
|
8773 apply auto |
|
8774 done |
|
8775 ultimately show ?thesis by auto |
|
8776 qed |
|
8777 |
|
8778 lemma rel_interior_convex_hull_union: |
|
8779 fixes S :: "'a \<Rightarrow> 'n::euclidean_space set" |
|
8780 assumes "finite I" |
|
8781 and "\<forall>i\<in>I. convex (S i) \<and> S i \<noteq> {}" |
|
8782 shows "rel_interior (convex hull (\<Union>(S ` I))) = |
|
8783 {setsum (\<lambda>i. c i *\<^sub>R s i) I | c s. (\<forall>i\<in>I. c i > 0) \<and> setsum c I = 1 \<and> |
|
8784 (\<forall>i\<in>I. s i \<in> rel_interior(S i))}" |
|
8785 (is "?lhs = ?rhs") |
|
8786 proof (cases "I = {}") |
|
8787 case True |
|
8788 then show ?thesis |
|
8789 using convex_hull_empty rel_interior_empty by auto |
|
8790 next |
|
8791 case False |
|
8792 def C0 \<equiv> "convex hull (\<Union>(S ` I))" |
|
8793 have "\<forall>i\<in>I. C0 \<ge> S i" |
|
8794 unfolding C0_def using hull_subset[of "\<Union>(S ` I)"] by auto |
|
8795 def K0 \<equiv> "cone hull ({1 :: real} <*> C0)" |
|
8796 def K \<equiv> "\<lambda>i. cone hull ({1 :: real} <*> S i)" |
|
8797 have "\<forall>i\<in>I. K i \<noteq> {}" |
|
8798 unfolding K_def using assms |
|
8799 by (simp add: cone_hull_empty_iff[symmetric]) |
|
8800 { |
|
8801 fix i |
|
8802 assume "i \<in> I" |
|
8803 then have "convex (K i)" |
|
8804 unfolding K_def |
|
8805 apply (subst convex_cone_hull) |
|
8806 apply (subst convex_Times) |
|
8807 using assms |
|
8808 apply auto |
|
8809 done |
|
8810 } |
|
8811 then have convK: "\<forall>i\<in>I. convex (K i)" |
|
8812 by auto |
|
8813 { |
|
8814 fix i |
|
8815 assume "i \<in> I" |
|
8816 then have "K0 \<supseteq> K i" |
|
8817 unfolding K0_def K_def |
|
8818 apply (subst hull_mono) |
|
8819 using `\<forall>i\<in>I. C0 \<ge> S i` |
|
8820 apply auto |
|
8821 done |
|
8822 } |
|
8823 then have "K0 \<supseteq> \<Union>(K ` I)" by auto |
|
8824 moreover have "convex K0" |
|
8825 unfolding K0_def |
|
8826 apply (subst convex_cone_hull) |
|
8827 apply (subst convex_Times) |
|
8828 unfolding C0_def |
|
8829 using convex_convex_hull |
|
8830 apply auto |
|
8831 done |
|
8832 ultimately have geq: "K0 \<supseteq> convex hull (\<Union>(K ` I))" |
|
8833 using hull_minimal[of _ "K0" "convex"] by blast |
|
8834 have "\<forall>i\<in>I. K i \<supseteq> {1 :: real} <*> S i" |
|
8835 using K_def by (simp add: hull_subset) |
|
8836 then have "\<Union>(K ` I) \<supseteq> {1 :: real} <*> \<Union>(S ` I)" |
|
8837 by auto |
|
8838 then have "convex hull \<Union>(K ` I) \<supseteq> convex hull ({1 :: real} <*> \<Union>(S ` I))" |
|
8839 by (simp add: hull_mono) |
|
8840 then have "convex hull \<Union>(K ` I) \<supseteq> {1 :: real} <*> C0" |
|
8841 unfolding C0_def |
|
8842 using convex_hull_Times[of "{(1 :: real)}" "\<Union>(S ` I)"] convex_hull_singleton |
|
8843 by auto |
|
8844 moreover have "cone (convex hull (\<Union>(K ` I)))" |
|
8845 apply (subst cone_convex_hull) |
|
8846 using cone_Union[of "K ` I"] |
|
8847 apply auto |
|
8848 unfolding K_def |
|
8849 using cone_cone_hull |
|
8850 apply auto |
|
8851 done |
|
8852 ultimately have "convex hull (\<Union>(K ` I)) \<supseteq> K0" |
|
8853 unfolding K0_def |
|
8854 using hull_minimal[of _ "convex hull (\<Union> (K ` I))" "cone"] |
|
8855 by blast |
|
8856 then have "K0 = convex hull (\<Union>(K ` I))" |
|
8857 using geq by auto |
|
8858 also have "\<dots> = setsum K I" |
|
8859 apply (subst convex_hull_finite_union_cones[of I K]) |
|
8860 using assms |
|
8861 apply blast |
|
8862 using False |
|
8863 apply blast |
|
8864 unfolding K_def |
|
8865 apply rule |
|
8866 apply (subst convex_cone_hull) |
|
8867 apply (subst convex_Times) |
|
8868 using assms cone_cone_hull `\<forall>i\<in>I. K i \<noteq> {}` K_def |
|
8869 apply auto |
|
8870 done |
|
8871 finally have "K0 = setsum K I" by auto |
|
8872 then have *: "rel_interior K0 = setsum (\<lambda>i. (rel_interior (K i))) I" |
|
8873 using rel_interior_sum_gen[of I K] convK by auto |
|
8874 { |
|
8875 fix x |
|
8876 assume "x \<in> ?lhs" |
|
8877 then have "(1::real, x) \<in> rel_interior K0" |
|
8878 using K0_def C0_def rel_interior_convex_cone_aux[of C0 "1::real" x] convex_convex_hull |
|
8879 by auto |
|
8880 then obtain k where k: "(1::real, x) = setsum k I \<and> (\<forall>i\<in>I. k i \<in> rel_interior (K i))" |
|
8881 using `finite I` * set_setsum_alt[of I "\<lambda>i. rel_interior (K i)"] by auto |
|
8882 { |
|
8883 fix i |
|
8884 assume "i \<in> I" |
|
8885 then have "convex (S i) \<and> k i \<in> rel_interior (cone hull {1} <*> S i)" |
|
8886 using k K_def assms by auto |
|
8887 then have "\<exists>ci si. k i = (ci, ci *\<^sub>R si) \<and> 0 < ci \<and> si \<in> rel_interior (S i)" |
|
8888 using rel_interior_convex_cone[of "S i"] by auto |
|
8677 } |
8889 } |
8678 hence "((1::real),x) : rel_interior K0" |
8890 then obtain c s where |
8679 using K0_def * set_setsum_alt[of I "(%i. rel_interior (K i))"] assms k_def cs_def |
8891 cs: "\<forall>i\<in>I. k i = (c i, c i *\<^sub>R s i) \<and> 0 < c i \<and> s i \<in> rel_interior (S i)" |
8680 apply auto apply (rule_tac x="k" in exI) by (simp add: setsum_prod) |
8892 by metis |
8681 hence "x : ?lhs" using K0_def C0_def |
8893 then have "x = (\<Sum>i\<in>I. c i *\<^sub>R s i) \<and> setsum c I = 1" |
8682 rel_interior_convex_cone_aux[of C0 "(1::real)" x] by (auto simp add: convex_convex_hull) |
8894 using k by (simp add: setsum_prod) |
8895 then have "x \<in> ?rhs" |
|
8896 using k |
|
8897 apply auto |
|
8898 apply (rule_tac x = c in exI) |
|
8899 apply (rule_tac x = s in exI) |
|
8900 using cs |
|
8901 apply auto |
|
8902 done |
|
8683 } |
8903 } |
8684 ultimately have ?thesis by blast |
8904 moreover |
8685 } ultimately show ?thesis by blast |
8905 { |
8906 fix x |
|
8907 assume "x \<in> ?rhs" |
|
8908 then obtain c s where cs: "x = setsum (\<lambda>i. c i *\<^sub>R s i) I \<and> |
|
8909 (\<forall>i\<in>I. c i > 0) \<and> setsum c I = 1 \<and> (\<forall>i\<in>I. s i \<in> rel_interior (S i))" |
|
8910 by auto |
|
8911 def k \<equiv> "\<lambda>i. (c i, c i *\<^sub>R s i)" |
|
8912 { |
|
8913 fix i assume "i:I" |
|
8914 then have "k i \<in> rel_interior (K i)" |
|
8915 using k_def K_def assms cs rel_interior_convex_cone[of "S i"] |
|
8916 by auto |
|
8917 } |
|
8918 then have "(1::real, x) \<in> rel_interior K0" |
|
8919 using K0_def * set_setsum_alt[of I "(\<lambda>i. rel_interior (K i))"] assms k_def cs |
|
8920 apply auto |
|
8921 apply (rule_tac x = k in exI) |
|
8922 apply (simp add: setsum_prod) |
|
8923 done |
|
8924 then have "x \<in> ?lhs" |
|
8925 using K0_def C0_def rel_interior_convex_cone_aux[of C0 1 x] |
|
8926 by (auto simp add: convex_convex_hull) |
|
8927 } |
|
8928 ultimately show ?thesis by blast |
|
8686 qed |
8929 qed |
8687 |
8930 |
8688 |
8931 |
8689 lemma convex_le_Inf_differential: |
8932 lemma convex_le_Inf_differential: |
8690 fixes f :: "real \<Rightarrow> real" |
8933 fixes f :: "real \<Rightarrow> real" |
8691 assumes "convex_on I f" |
8934 assumes "convex_on I f" |
8692 assumes "x \<in> interior I" "y \<in> I" |
8935 and "x \<in> interior I" |
8936 and "y \<in> I" |
|
8693 shows "f y \<ge> f x + Inf ((\<lambda>t. (f x - f t) / (x - t)) ` ({x<..} \<inter> I)) * (y - x)" |
8937 shows "f y \<ge> f x + Inf ((\<lambda>t. (f x - f t) / (x - t)) ` ({x<..} \<inter> I)) * (y - x)" |
8694 (is "_ \<ge> _ + Inf (?F x) * (y - x)") |
8938 (is "_ \<ge> _ + Inf (?F x) * (y - x)") |
8695 proof (cases rule: linorder_cases) |
8939 proof (cases rule: linorder_cases) |
8696 assume "x < y" |
8940 assume "x < y" |
8697 moreover |
8941 moreover |
8698 have "open (interior I)" by auto |
8942 have "open (interior I)" by auto |
8699 from openE[OF this `x \<in> interior I`] guess e . note e = this |
8943 from openE[OF this `x \<in> interior I`] guess e . note e = this |
8703 with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto |
8947 with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto |
8704 |
8948 |
8705 have "open (interior I)" by auto |
8949 have "open (interior I)" by auto |
8706 from openE[OF this `x \<in> interior I`] guess e . |
8950 from openE[OF this `x \<in> interior I`] guess e . |
8707 moreover def K \<equiv> "x - e / 2" |
8951 moreover def K \<equiv> "x - e / 2" |
8708 with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: dist_real_def) |
8952 with `0 < e` have "K \<in> ball x e" "K < x" |
8953 by (auto simp: dist_real_def) |
|
8709 ultimately have "K \<in> I" "K < x" "x \<in> I" |
8954 ultimately have "K \<in> I" "K < x" "x \<in> I" |
8710 using interior_subset[of I] `x \<in> interior I` by auto |
8955 using interior_subset[of I] `x \<in> interior I` by auto |
8711 |
8956 |
8712 have "Inf (?F x) \<le> (f x - f y) / (x - y)" |
8957 have "Inf (?F x) \<le> (f x - f y) / (x - y)" |
8713 proof (intro bdd_belowI cInf_lower2) |
8958 proof (intro bdd_belowI cInf_lower2) |
8714 show "(f x - f t) / (x - t) \<in> ?F x" |
8959 show "(f x - f t) / (x - t) \<in> ?F x" |
8715 using `t \<in> I` `x < t` by auto |
8960 using `t \<in> I` `x < t` by auto |
8716 show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)" |
8961 show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)" |
8717 using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y` by (rule convex_on_diff) |
8962 using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y` |
8963 by (rule convex_on_diff) |
|
8718 next |
8964 next |
8719 fix y assume "y \<in> ?F x" |
8965 fix y |
8966 assume "y \<in> ?F x" |
|
8720 with order_trans[OF convex_on_diff[OF `convex_on I f` `K \<in> I` _ `K < x` _]] |
8967 with order_trans[OF convex_on_diff[OF `convex_on I f` `K \<in> I` _ `K < x` _]] |
8721 show "(f K - f x) / (K - x) \<le> y" by auto |
8968 show "(f K - f x) / (K - x) \<le> y" by auto |
8722 qed |
8969 qed |
8723 then show ?thesis |
8970 then show ?thesis |
8724 using `x < y` by (simp add: field_simps) |
8971 using `x < y` by (simp add: field_simps) |
8735 have "(f x - f y) / (x - y) \<le> Inf (?F x)" |
8982 have "(f x - f y) / (x - y) \<le> Inf (?F x)" |
8736 proof (rule cInf_greatest) |
8983 proof (rule cInf_greatest) |
8737 have "(f x - f y) / (x - y) = (f y - f x) / (y - x)" |
8984 have "(f x - f y) / (x - y) = (f y - f x) / (y - x)" |
8738 using `y < x` by (auto simp: field_simps) |
8985 using `y < x` by (auto simp: field_simps) |
8739 also |
8986 also |
8740 fix z assume "z \<in> ?F x" |
8987 fix z |
8988 assume "z \<in> ?F x" |
|
8741 with order_trans[OF convex_on_diff[OF `convex_on I f` `y \<in> I` _ `y < x`]] |
8989 with order_trans[OF convex_on_diff[OF `convex_on I f` `y \<in> I` _ `y < x`]] |
8742 have "(f y - f x) / (y - x) \<le> z" by auto |
8990 have "(f y - f x) / (y - x) \<le> z" |
8991 by auto |
|
8743 finally show "(f x - f y) / (x - y) \<le> z" . |
8992 finally show "(f x - f y) / (x - y) \<le> z" . |
8744 next |
8993 next |
8745 have "open (interior I)" by auto |
8994 have "open (interior I)" by auto |
8746 from openE[OF this `x \<in> interior I`] guess e . note e = this |
8995 from openE[OF this `x \<in> interior I`] guess e . note e = this |
8747 then have "x + e / 2 \<in> ball x e" by (auto simp: dist_real_def) |
8996 then have "x + e / 2 \<in> ball x e" |
8748 with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I" by auto |
8997 by (auto simp: dist_real_def) |
8749 then show "?F x \<noteq> {}" by blast |
8998 with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I" |
8999 by auto |
|
9000 then show "?F x \<noteq> {}" |
|
9001 by blast |
|
8750 qed |
9002 qed |
8751 then show ?thesis |
9003 then show ?thesis |
8752 using `y < x` by (simp add: field_simps) |
9004 using `y < x` by (simp add: field_simps) |
8753 qed simp |
9005 qed simp |
8754 |
9006 |