22 lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_le_def Cart_lambda_beta basis_component vector_uminus_component |
22 lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_le_def Cart_lambda_beta basis_component vector_uminus_component |
23 |
23 |
24 lemma dest_vec1_simps[simp]: fixes a::"real^1" |
24 lemma dest_vec1_simps[simp]: fixes a::"real^1" |
25 shows "a$1 = 0 \<longleftrightarrow> a = 0" (*"a \<le> 1 \<longleftrightarrow> dest_vec1 a \<le> 1" "0 \<le> a \<longleftrightarrow> 0 \<le> dest_vec1 a"*) |
25 shows "a$1 = 0 \<longleftrightarrow> a = 0" (*"a \<le> 1 \<longleftrightarrow> dest_vec1 a \<le> 1" "0 \<le> a \<longleftrightarrow> 0 \<le> dest_vec1 a"*) |
26 "a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1" |
26 "a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1" |
27 by(auto simp add:vector_component_simps forall_1 Cart_eq) |
27 by(auto simp add: vector_le_def Cart_eq) |
28 |
28 |
29 lemma norm_not_0:"(x::real^'n)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto |
29 lemma norm_not_0:"(x::real^'n)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto |
30 |
30 |
31 lemma setsum_delta_notmem: assumes "x\<notin>s" |
31 lemma setsum_delta_notmem: assumes "x\<notin>s" |
32 shows "setsum (\<lambda>y. if (y = x) then P x else Q y) s = setsum Q s" |
32 shows "setsum (\<lambda>y. if (y = x) then P x else Q y) s = setsum Q s" |
48 lemma if_smult:"(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)" by auto |
48 lemma if_smult:"(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)" by auto |
49 |
49 |
50 lemma mem_interval_1: fixes x :: "real^1" shows |
50 lemma mem_interval_1: fixes x :: "real^1" shows |
51 "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)" |
51 "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)" |
52 "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)" |
52 "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)" |
53 by(simp_all add: Cart_eq vector_less_def vector_le_def forall_1) |
53 by(simp_all add: Cart_eq vector_less_def vector_le_def) |
54 |
54 |
55 lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n)) ` {a..b} = |
55 lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n)) ` {a..b} = |
56 (if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})" |
56 (if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})" |
57 using image_affinity_interval[of m 0 a b] by auto |
57 using image_affinity_interval[of m 0 a b] by auto |
58 |
58 |
64 apply(rule_tac [!] equalityI) |
64 apply(rule_tac [!] equalityI) |
65 unfolding subset_eq Ball_def Bex_def mem_interval_1 image_iff |
65 unfolding subset_eq Ball_def Bex_def mem_interval_1 image_iff |
66 apply(rule_tac [!] allI)apply(rule_tac [!] impI) |
66 apply(rule_tac [!] allI)apply(rule_tac [!] impI) |
67 apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI) |
67 apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI) |
68 apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI) |
68 apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI) |
69 by (auto simp add: vector_less_def vector_le_def forall_1 |
69 by (auto simp add: vector_less_def vector_le_def) |
70 vec1_dest_vec1[unfolded One_nat_def]) |
|
71 |
70 |
72 lemma dest_vec1_setsum: assumes "finite S" |
71 lemma dest_vec1_setsum: assumes "finite S" |
73 shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S" |
72 shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S" |
74 using dest_vec1_sum[OF assms] by auto |
73 using dest_vec1_sum[OF assms] by auto |
75 |
74 |
478 case True show ?thesis unfolding True and scaleR_left_distrib[THEN sym] using as(3,6) by auto next |
477 case True show ?thesis unfolding True and scaleR_left_distrib[THEN sym] using as(3,6) by auto next |
479 case False thus ?thesis using as(1)[THEN spec[where x="{x,y}"], THEN spec[where x="\<lambda>z. if z=x then u else v"]] and as(2-) by auto qed |
478 case False thus ?thesis using as(1)[THEN spec[where x="{x,y}"], THEN spec[where x="\<lambda>z. if z=x then u else v"]] and as(2-) by auto qed |
480 next |
479 next |
481 fix t u assume asm:"\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s" "finite (t::'a set)" |
480 fix t u assume asm:"\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s" "finite (t::'a set)" |
482 (*"finite t" "t \<subseteq> s" "\<forall>x\<in>t. (0::real) \<le> u x" "setsum u t = 1"*) |
481 (*"finite t" "t \<subseteq> s" "\<forall>x\<in>t. (0::real) \<le> u x" "setsum u t = 1"*) |
483 from this(2) have "\<forall>u. t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" apply(induct_tac t rule:finite_induct) |
482 from this(2) have "\<forall>u. t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" apply(induct t rule:finite_induct) |
484 prefer 3 apply (rule,rule) apply(erule conjE)+ proof- |
483 prefer 2 apply (rule,rule) apply(erule conjE)+ proof- |
485 fix x f u assume ind:"\<forall>u. f \<subseteq> s \<and> (\<forall>x\<in>f. 0 \<le> u x) \<and> setsum u f = 1 \<longrightarrow> (\<Sum>x\<in>f. u x *\<^sub>R x) \<in> s" |
484 fix x f u assume ind:"\<forall>u. f \<subseteq> s \<and> (\<forall>x\<in>f. 0 \<le> u x) \<and> setsum u f = 1 \<longrightarrow> (\<Sum>x\<in>f. u x *\<^sub>R x) \<in> s" |
486 assume as:"finite f" "x \<notin> f" "insert x f \<subseteq> s" "\<forall>x\<in>insert x f. 0 \<le> u x" "setsum u (insert x f) = (1::real)" |
485 assume as:"finite f" "x \<notin> f" "insert x f \<subseteq> s" "\<forall>x\<in>insert x f. 0 \<le> u x" "setsum u (insert x f) = (1::real)" |
487 show "(\<Sum>x\<in>insert x f. u x *\<^sub>R x) \<in> s" proof(cases "u x = 1") |
486 show "(\<Sum>x\<in>insert x f. u x *\<^sub>R x) \<in> s" proof(cases "u x = 1") |
488 case True hence "setsum (\<lambda>x. u x *\<^sub>R x) f = 0" apply(rule_tac setsum_0') apply(rule ccontr) unfolding ball_simps apply(erule bexE) proof- |
487 case True hence "setsum (\<lambda>x. u x *\<^sub>R x) f = 0" apply(rule_tac setsum_0') apply(rule ccontr) unfolding ball_simps apply(erule bexE) proof- |
489 fix y assume y:"y \<in> f" "u y *\<^sub>R y \<noteq> 0" |
488 fix y assume y:"y \<in> f" "u y *\<^sub>R y \<noteq> 0" |
774 qed |
773 qed |
775 |
774 |
776 lemma convex_cball: |
775 lemma convex_cball: |
777 fixes x :: "'a::real_normed_vector" |
776 fixes x :: "'a::real_normed_vector" |
778 shows "convex(cball x e)" |
777 shows "convex(cball x e)" |
779 proof(auto simp add: convex_def Ball_def mem_cball) |
778 proof(auto simp add: convex_def Ball_def) |
780 fix y z assume yz:"dist x y \<le> e" "dist x z \<le> e" |
779 fix y z assume yz:"dist x y \<le> e" "dist x z \<le> e" |
781 fix u v ::real assume uv:" 0 \<le> u" "0 \<le> v" "u + v = 1" |
780 fix u v ::real assume uv:" 0 \<le> u" "0 \<le> v" "u + v = 1" |
782 have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz |
781 have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz |
783 using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto |
782 using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto |
784 thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" using real_convex_bound_le[OF yz uv] by auto |
783 thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" using real_convex_bound_le[OF yz uv] by auto |
1142 { fix x y assume "x\<in>s" "y\<in>s" and ?lhs |
1141 { fix x y assume "x\<in>s" "y\<in>s" and ?lhs |
1143 hence "2 *\<^sub>R x \<in>s" "2 *\<^sub>R y \<in> s" unfolding cone_def by auto |
1142 hence "2 *\<^sub>R x \<in>s" "2 *\<^sub>R y \<in> s" unfolding cone_def by auto |
1144 hence "x + y \<in> s" using `?lhs`[unfolded convex_def, THEN conjunct1] |
1143 hence "x + y \<in> s" using `?lhs`[unfolded convex_def, THEN conjunct1] |
1145 apply(erule_tac x="2*\<^sub>R x" in ballE) apply(erule_tac x="2*\<^sub>R y" in ballE) |
1144 apply(erule_tac x="2*\<^sub>R x" in ballE) apply(erule_tac x="2*\<^sub>R y" in ballE) |
1146 apply(erule_tac x="1/2" in allE) apply simp apply(erule_tac x="1/2" in allE) by auto } |
1145 apply(erule_tac x="1/2" in allE) apply simp apply(erule_tac x="1/2" in allE) by auto } |
1147 thus ?thesis unfolding convex_def cone_def by auto |
1146 thus ?thesis unfolding convex_def cone_def by blast |
1148 qed |
1147 qed |
1149 |
1148 |
1150 lemma affine_dependent_biggerset: fixes s::"(real^'n) set" |
1149 lemma affine_dependent_biggerset: fixes s::"(real^'n) set" |
1151 assumes "finite s" "card s \<ge> CARD('n) + 2" |
1150 assumes "finite s" "card s \<ge> CARD('n) + 2" |
1152 shows "affine_dependent s" |
1151 shows "affine_dependent s" |
1257 |
1256 |
1258 lemma open_convex_hull[intro]: |
1257 lemma open_convex_hull[intro]: |
1259 fixes s :: "'a::real_normed_vector set" |
1258 fixes s :: "'a::real_normed_vector set" |
1260 assumes "open s" |
1259 assumes "open s" |
1261 shows "open(convex hull s)" |
1260 shows "open(convex hull s)" |
1262 unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(10) |
1261 unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(10) |
1263 proof(rule, rule) fix a |
1262 proof(rule, rule) fix a |
1264 assume "\<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = a" |
1263 assume "\<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = a" |
1265 then obtain t u where obt:"finite t" "t\<subseteq>s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = a" by auto |
1264 then obtain t u where obt:"finite t" "t\<subseteq>s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = a" by auto |
1266 |
1265 |
1267 from assms[unfolded open_contains_cball] obtain b where b:"\<forall>x\<in>s. 0 < b x \<and> cball x (b x) \<subseteq> s" |
1266 from assms[unfolded open_contains_cball] obtain b where b:"\<forall>x\<in>s. 0 < b x \<and> cball x (b x) \<subseteq> s" |
1277 hence y:"norm (a - y) \<le> Min i" unfolding dist_norm[THEN sym] by auto |
1276 hence y:"norm (a - y) \<le> Min i" unfolding dist_norm[THEN sym] by auto |
1278 { fix x assume "x\<in>t" |
1277 { fix x assume "x\<in>t" |
1279 hence "Min i \<le> b x" unfolding i_def apply(rule_tac Min_le) using obt(1) by auto |
1278 hence "Min i \<le> b x" unfolding i_def apply(rule_tac Min_le) using obt(1) by auto |
1280 hence "x + (y - a) \<in> cball x (b x)" using y unfolding mem_cball dist_norm by auto |
1279 hence "x + (y - a) \<in> cball x (b x)" using y unfolding mem_cball dist_norm by auto |
1281 moreover from `x\<in>t` have "x\<in>s" using obt(2) by auto |
1280 moreover from `x\<in>t` have "x\<in>s" using obt(2) by auto |
1282 ultimately have "x + (y - a) \<in> s" using y and b[THEN bspec[where x=x]] unfolding subset_eq by auto } |
1281 ultimately have "x + (y - a) \<in> s" using y and b[THEN bspec[where x=x]] unfolding subset_eq by fast } |
1283 moreover |
1282 moreover |
1284 have *:"inj_on (\<lambda>v. v + (y - a)) t" unfolding inj_on_def by auto |
1283 have *:"inj_on (\<lambda>v. v + (y - a)) t" unfolding inj_on_def by auto |
1285 have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a))) = 1" |
1284 have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a))) = 1" |
1286 unfolding setsum_reindex[OF *] o_def using obt(4) by auto |
1285 unfolding setsum_reindex[OF *] o_def using obt(4) by auto |
1287 moreover have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a)) *\<^sub>R v) = y" |
1286 moreover have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a)) *\<^sub>R v) = y" |
1347 next |
1346 next |
1348 case False then obtain w where "w\<in>s" by auto |
1347 case False then obtain w where "w\<in>s" by auto |
1349 show ?thesis unfolding caratheodory[of s] |
1348 show ?thesis unfolding caratheodory[of s] |
1350 proof(induct ("CARD('n) + 1")) |
1349 proof(induct ("CARD('n) + 1")) |
1351 have *:"{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}" |
1350 have *:"{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}" |
1352 using compact_empty by (auto simp add: convex_hull_empty) |
1351 using compact_empty by auto |
1353 case 0 thus ?case unfolding * by simp |
1352 case 0 thus ?case unfolding * by simp |
1354 next |
1353 next |
1355 case (Suc n) |
1354 case (Suc n) |
1356 show ?case proof(cases "n=0") |
1355 show ?case proof(cases "n=0") |
1357 case True have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} = s" |
1356 case True have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} = s" |
1358 unfolding expand_set_eq and mem_Collect_eq proof(rule, rule) |
1357 unfolding expand_set_eq and mem_Collect_eq proof(rule, rule) |
1359 fix x assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t" |
1358 fix x assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t" |
1360 then obtain t where t:"finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t" by auto |
1359 then obtain t where t:"finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t" by auto |
1361 show "x\<in>s" proof(cases "card t = 0") |
1360 show "x\<in>s" proof(cases "card t = 0") |
1362 case True thus ?thesis using t(4) unfolding card_0_eq[OF t(1)] by(simp add: convex_hull_empty) |
1361 case True thus ?thesis using t(4) unfolding card_0_eq[OF t(1)] by simp |
1363 next |
1362 next |
1364 case False hence "card t = Suc 0" using t(3) `n=0` by auto |
1363 case False hence "card t = Suc 0" using t(3) `n=0` by auto |
1365 then obtain a where "t = {a}" unfolding card_Suc_eq by auto |
1364 then obtain a where "t = {a}" unfolding card_Suc_eq by auto |
1366 thus ?thesis using t(2,4) by (simp add: convex_hull_singleton) |
1365 thus ?thesis using t(2,4) by simp |
1367 qed |
1366 qed |
1368 next |
1367 next |
1369 fix x assume "x\<in>s" |
1368 fix x assume "x\<in>s" |
1370 thus "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t" |
1369 thus "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t" |
1371 apply(rule_tac x="{x}" in exI) unfolding convex_hull_singleton by auto |
1370 apply(rule_tac x="{x}" in exI) unfolding convex_hull_singleton by auto |
1396 next |
1395 next |
1397 case True then obtain a u where au:"t = insert a u" "a\<notin>u" apply(drule_tac card_eq_SucD) by auto |
1396 case True then obtain a u where au:"t = insert a u" "a\<notin>u" apply(drule_tac card_eq_SucD) by auto |
1398 show ?P proof(cases "u={}") |
1397 show ?P proof(cases "u={}") |
1399 case True hence "x=a" using t(4)[unfolded au] by auto |
1398 case True hence "x=a" using t(4)[unfolded au] by auto |
1400 show ?P unfolding `x=a` apply(rule_tac x=a in exI, rule_tac x=a in exI, rule_tac x=1 in exI) |
1399 show ?P unfolding `x=a` apply(rule_tac x=a in exI, rule_tac x=a in exI, rule_tac x=1 in exI) |
1401 using t and `n\<noteq>0` unfolding au by(auto intro!: exI[where x="{a}"] simp add: convex_hull_singleton) |
1400 using t and `n\<noteq>0` unfolding au by(auto intro!: exI[where x="{a}"]) |
1402 next |
1401 next |
1403 case False obtain ux vx b where obt:"ux\<ge>0" "vx\<ge>0" "ux + vx = 1" "b \<in> convex hull u" "x = ux *\<^sub>R a + vx *\<^sub>R b" |
1402 case False obtain ux vx b where obt:"ux\<ge>0" "vx\<ge>0" "ux + vx = 1" "b \<in> convex hull u" "x = ux *\<^sub>R a + vx *\<^sub>R b" |
1404 using t(4)[unfolded au convex_hull_insert[OF False]] by auto |
1403 using t(4)[unfolded au convex_hull_insert[OF False]] by auto |
1405 have *:"1 - vx = ux" using obt(3) by auto |
1404 have *:"1 - vx = ux" using obt(3) by auto |
1406 show ?P apply(rule_tac x=a in exI, rule_tac x=b in exI, rule_tac x=vx in exI) |
1405 show ?P apply(rule_tac x=a in exI, rule_tac x=b in exI, rule_tac x=vx in exI) |
1849 by (metis convex_convex_hull convex_scaling hull_subset mem_def subset_hull subset_image_iff) |
1848 by (metis convex_convex_hull convex_scaling hull_subset mem_def subset_hull subset_image_iff) |
1850 |
1849 |
1851 lemma convex_hull_scaling: |
1850 lemma convex_hull_scaling: |
1852 "convex hull ((\<lambda>x. c *\<^sub>R x) ` s) = (\<lambda>x. c *\<^sub>R x) ` (convex hull s)" |
1851 "convex hull ((\<lambda>x. c *\<^sub>R x) ` s) = (\<lambda>x. c *\<^sub>R x) ` (convex hull s)" |
1853 apply(cases "c=0") defer apply(rule convex_hull_bilemma[rule_format, of _ _ inverse]) apply(rule convex_hull_scaling_lemma) |
1852 apply(cases "c=0") defer apply(rule convex_hull_bilemma[rule_format, of _ _ inverse]) apply(rule convex_hull_scaling_lemma) |
1854 unfolding image_image scaleR_scaleR by(auto simp add:image_constant_conv convex_hull_eq_empty) |
1853 unfolding image_image scaleR_scaleR by(auto simp add:image_constant_conv) |
1855 |
1854 |
1856 lemma convex_hull_affinity: |
1855 lemma convex_hull_affinity: |
1857 "convex hull ((\<lambda>x. a + c *\<^sub>R x) ` s) = (\<lambda>x. a + c *\<^sub>R x) ` (convex hull s)" |
1856 "convex hull ((\<lambda>x. a + c *\<^sub>R x) ` s) = (\<lambda>x. a + c *\<^sub>R x) ` (convex hull s)" |
1858 by(simp only: image_image[THEN sym] convex_hull_scaling convex_hull_translation) |
1857 by(simp only: image_image[THEN sym] convex_hull_scaling convex_hull_translation) |
1859 |
1858 |
2311 { fix a b assume "\<not> u * a + v * b \<le> a" |
2310 { fix a b assume "\<not> u * a + v * b \<le> a" |
2312 hence "v * b > (1 - u) * a" unfolding not_le using as(4) by(auto simp add: field_simps) |
2311 hence "v * b > (1 - u) * a" unfolding not_le using as(4) by(auto simp add: field_simps) |
2313 hence "a < b" unfolding * using as(4) apply(rule_tac mult_left_less_imp_less) by(auto simp add: ring_simps) |
2312 hence "a < b" unfolding * using as(4) apply(rule_tac mult_left_less_imp_less) by(auto simp add: ring_simps) |
2314 hence "u * a + v * b \<le> b" unfolding ** using **(2) as(3) by(auto simp add: field_simps intro!:mult_right_mono) } |
2313 hence "u * a + v * b \<le> b" unfolding ** using **(2) as(3) by(auto simp add: field_simps intro!:mult_right_mono) } |
2315 ultimately show "u *\<^sub>R x + v *\<^sub>R y \<in> s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)]) |
2314 ultimately show "u *\<^sub>R x + v *\<^sub>R y \<in> s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)]) |
2316 using as(3-) dimindex_ge_1 apply- by(auto simp add: vector_component) qed |
2315 using as(3-) dimindex_ge_1 by auto qed |
2317 |
2316 |
2318 lemma is_interval_connected: |
2317 lemma is_interval_connected: |
2319 fixes s :: "(real ^ _) set" |
2318 fixes s :: "(real ^ _) set" |
2320 shows "is_interval s \<Longrightarrow> connected s" |
2319 shows "is_interval s \<Longrightarrow> connected s" |
2321 using is_interval_convex convex_connected by auto |
2320 using is_interval_convex convex_connected by auto |
2334 apply(rule,rule,rule,rule,erule conjE,rule ccontr) proof- |
2333 apply(rule,rule,rule,rule,erule conjE,rule ccontr) proof- |
2335 fix a b x assume as:"connected s" "a \<in> s" "b \<in> s" "dest_vec1 a \<le> dest_vec1 x" "dest_vec1 x \<le> dest_vec1 b" "x\<notin>s" |
2334 fix a b x assume as:"connected s" "a \<in> s" "b \<in> s" "dest_vec1 a \<le> dest_vec1 x" "dest_vec1 x \<le> dest_vec1 b" "x\<notin>s" |
2336 hence *:"dest_vec1 a < dest_vec1 x" "dest_vec1 x < dest_vec1 b" apply(rule_tac [!] ccontr) unfolding not_less by auto |
2335 hence *:"dest_vec1 a < dest_vec1 x" "dest_vec1 x < dest_vec1 b" apply(rule_tac [!] ccontr) unfolding not_less by auto |
2337 let ?halfl = "{z. inner (basis 1) z < dest_vec1 x} " and ?halfr = "{z. inner (basis 1) z > dest_vec1 x} " |
2336 let ?halfl = "{z. inner (basis 1) z < dest_vec1 x} " and ?halfr = "{z. inner (basis 1) z > dest_vec1 x} " |
2338 { fix y assume "y \<in> s" have "y \<in> ?halfr \<union> ?halfl" apply(rule ccontr) |
2337 { fix y assume "y \<in> s" have "y \<in> ?halfr \<union> ?halfl" apply(rule ccontr) |
2339 using as(6) `y\<in>s` by (auto simp add: inner_vector_def dest_vec1_eq) } |
2338 using as(6) `y\<in>s` by (auto simp add: inner_vector_def) } |
2340 moreover have "a\<in>?halfl" "b\<in>?halfr" using * by (auto simp add: inner_vector_def) |
2339 moreover have "a\<in>?halfl" "b\<in>?halfr" using * by (auto simp add: inner_vector_def) |
2341 hence "?halfl \<inter> s \<noteq> {}" "?halfr \<inter> s \<noteq> {}" using as(2-3) by auto |
2340 hence "?halfl \<inter> s \<noteq> {}" "?halfr \<inter> s \<noteq> {}" using as(2-3) by auto |
2342 ultimately show False apply(rule_tac notE[OF as(1)[unfolded connected_def]]) |
2341 ultimately show False apply(rule_tac notE[OF as(1)[unfolded connected_def]]) |
2343 apply(rule_tac x="?halfl" in exI, rule_tac x="?halfr" in exI) |
2342 apply(rule_tac x="?halfl" in exI, rule_tac x="?halfr" in exI) |
2344 apply(rule, rule open_halfspace_lt, rule, rule open_halfspace_gt) |
2343 apply(rule, rule open_halfspace_lt, rule, rule open_halfspace_gt) |
2372 lemma ivt_decreasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n" |
2371 lemma ivt_decreasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n" |
2373 assumes "dest_vec1 a \<le> dest_vec1 b" "continuous_on {a .. b} f" "(f b)$k \<le> y" "y \<le> (f a)$k" |
2372 assumes "dest_vec1 a \<le> dest_vec1 b" "continuous_on {a .. b} f" "(f b)$k \<le> y" "y \<le> (f a)$k" |
2374 shows "\<exists>x\<in>{a..b}. (f x)$k = y" |
2373 shows "\<exists>x\<in>{a..b}. (f x)$k = y" |
2375 apply(subst neg_equal_iff_equal[THEN sym]) unfolding vector_uminus_component[THEN sym] |
2374 apply(subst neg_equal_iff_equal[THEN sym]) unfolding vector_uminus_component[THEN sym] |
2376 apply(rule ivt_increasing_component_on_1) using assms using continuous_on_neg |
2375 apply(rule ivt_increasing_component_on_1) using assms using continuous_on_neg |
2377 by(auto simp add:vector_uminus_component) |
2376 by auto |
2378 |
2377 |
2379 lemma ivt_decreasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n" |
2378 lemma ivt_decreasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n" |
2380 shows "dest_vec1 a \<le> dest_vec1 b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f |
2379 shows "dest_vec1 a \<le> dest_vec1 b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f |
2381 \<Longrightarrow> f b$k \<le> y \<Longrightarrow> y \<le> f a$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$k = y" |
2380 \<Longrightarrow> f b$k \<le> y \<Longrightarrow> y \<le> f a$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$k = y" |
2382 by(rule ivt_decreasing_component_on_1) |
2381 by(rule ivt_decreasing_component_on_1) |
2413 then obtain i where i':"x$i = xi" "x$i \<noteq> 0" by auto |
2412 then obtain i where i':"x$i = xi" "x$i \<noteq> 0" by auto |
2414 have i:"\<And>j. x$j > 0 \<Longrightarrow> x$i \<le> x$j" |
2413 have i:"\<And>j. x$j > 0 \<Longrightarrow> x$i \<le> x$j" |
2415 unfolding i'(1) xi_def apply(rule_tac Min_le) unfolding image_iff |
2414 unfolding i'(1) xi_def apply(rule_tac Min_le) unfolding image_iff |
2416 defer apply(rule_tac x=j in bexI) using i' by auto |
2415 defer apply(rule_tac x=j in bexI) using i' by auto |
2417 have i01:"x$i \<le> 1" "x$i > 0" using Suc(2)[unfolded mem_interval,rule_format,of i] using i'(2) `x$i \<noteq> 0` |
2416 have i01:"x$i \<le> 1" "x$i > 0" using Suc(2)[unfolded mem_interval,rule_format,of i] using i'(2) `x$i \<noteq> 0` |
2418 by(auto simp add: Cart_lambda_beta) |
2417 by auto |
2419 show ?thesis proof(cases "x$i=1") |
2418 show ?thesis proof(cases "x$i=1") |
2420 case True have "\<forall>j\<in>{i. x$i \<noteq> 0}. x$j = 1" apply(rule, rule ccontr) unfolding mem_Collect_eq proof- |
2419 case True have "\<forall>j\<in>{i. x$i \<noteq> 0}. x$j = 1" apply(rule, rule ccontr) unfolding mem_Collect_eq proof- |
2421 fix j assume "x $ j \<noteq> 0" "x $ j \<noteq> 1" |
2420 fix j assume "x $ j \<noteq> 0" "x $ j \<noteq> 1" |
2422 hence j:"x$j \<in> {0<..<1}" using Suc(2) by(auto simp add: vector_le_def elim!:allE[where x=j]) |
2421 hence j:"x$j \<in> {0<..<1}" using Suc(2) by(auto simp add: vector_le_def elim!:allE[where x=j]) |
2423 hence "x$j \<in> op $ x ` {i. x $ i \<noteq> 0}" by auto |
2422 hence "x$j \<in> op $ x ` {i. x $ i \<noteq> 0}" by auto |
2424 hence "x$j \<ge> x$i" unfolding i'(1) xi_def apply(rule_tac Min_le) by auto |
2423 hence "x$j \<ge> x$i" unfolding i'(1) xi_def apply(rule_tac Min_le) by auto |
2425 thus False using True Suc(2) j by(auto simp add: vector_le_def elim!:ballE[where x=j]) qed |
2424 thus False using True Suc(2) j by(auto simp add: vector_le_def elim!:ballE[where x=j]) qed |
2426 thus "x\<in>convex hull ?points" apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) |
2425 thus "x\<in>convex hull ?points" apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) |
2427 by(auto simp add: Cart_lambda_beta) |
2426 by auto |
2428 next let ?y = "\<lambda>j. if x$j = 0 then 0 else (x$j - x$i) / (1 - x$i)" |
2427 next let ?y = "\<lambda>j. if x$j = 0 then 0 else (x$j - x$i) / (1 - x$i)" |
2429 case False hence *:"x = x$i *\<^sub>R (\<chi> j. if x$j = 0 then 0 else 1) + (1 - x$i) *\<^sub>R (\<chi> j. ?y j)" unfolding Cart_eq |
2428 case False hence *:"x = x$i *\<^sub>R (\<chi> j. if x$j = 0 then 0 else 1) + (1 - x$i) *\<^sub>R (\<chi> j. ?y j)" unfolding Cart_eq |
2430 by(auto simp add: Cart_lambda_beta vector_add_component vector_smult_component vector_minus_component field_simps) |
2429 by(auto simp add: field_simps) |
2431 { fix j have "x$j \<noteq> 0 \<Longrightarrow> 0 \<le> (x $ j - x $ i) / (1 - x $ i)" "(x $ j - x $ i) / (1 - x $ i) \<le> 1" |
2430 { fix j have "x$j \<noteq> 0 \<Longrightarrow> 0 \<le> (x $ j - x $ i) / (1 - x $ i)" "(x $ j - x $ i) / (1 - x $ i) \<le> 1" |
2432 apply(rule_tac divide_nonneg_pos) using i(1)[of j] using False i01 |
2431 apply(rule_tac divide_nonneg_pos) using i(1)[of j] using False i01 |
2433 using Suc(2)[unfolded mem_interval, rule_format, of j] by(auto simp add:field_simps Cart_lambda_beta) |
2432 using Suc(2)[unfolded mem_interval, rule_format, of j] by(auto simp add:field_simps) |
2434 hence "0 \<le> ?y j \<and> ?y j \<le> 1" by auto } |
2433 hence "0 \<le> ?y j \<and> ?y j \<le> 1" by auto } |
2435 moreover have "i\<in>{j. x$j \<noteq> 0} - {j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0}" using i01 by(auto simp add: Cart_lambda_beta) |
2434 moreover have "i\<in>{j. x$j \<noteq> 0} - {j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0}" using i01 by auto |
2436 hence "{j. x$j \<noteq> 0} \<noteq> {j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0}" by auto |
2435 hence "{j. x$j \<noteq> 0} \<noteq> {j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0}" by auto |
2437 hence **:"{j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0} \<subset> {j. x$j \<noteq> 0}" apply - apply rule by(auto simp add: Cart_lambda_beta) |
2436 hence **:"{j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0} \<subset> {j. x$j \<noteq> 0}" apply - apply rule by auto |
2438 have "card {j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0} \<le> n" using less_le_trans[OF psubset_card_mono[OF _ **] Suc(4)] by auto |
2437 have "card {j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0} \<le> n" using less_le_trans[OF psubset_card_mono[OF _ **] Suc(4)] by auto |
2439 ultimately show ?thesis apply(subst *) apply(rule convex_convex_hull[unfolded convex_def, rule_format]) |
2438 ultimately show ?thesis apply(subst *) apply(rule convex_convex_hull[unfolded convex_def, rule_format]) |
2440 apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) defer apply(rule Suc(1)) |
2439 apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) defer apply(rule Suc(1)) |
2441 unfolding mem_interval using i01 Suc(3) by (auto simp add: Cart_lambda_beta) |
2440 unfolding mem_interval using i01 Suc(3) by auto |
2442 qed qed qed } note * = this |
2441 qed qed qed } note * = this |
2443 show ?thesis apply rule defer apply(rule hull_minimal) unfolding subset_eq prefer 3 apply rule |
2442 show ?thesis apply rule defer apply(rule hull_minimal) unfolding subset_eq prefer 3 apply rule |
2444 apply(rule_tac n2="CARD('n)" in *) prefer 3 apply(rule card_mono) using 01 and convex_interval(1) prefer 5 apply - apply rule |
2443 apply(rule_tac n2="CARD('n)" in *) prefer 3 apply(rule card_mono) using 01 and convex_interval(1) prefer 5 apply - apply rule |
2445 unfolding mem_interval apply rule unfolding mem_Collect_eq apply(erule_tac x=i in allE) |
2444 unfolding mem_interval apply rule unfolding mem_Collect_eq apply(erule_tac x=i in allE) |
2446 by(auto simp add: vector_le_def mem_def[of _ convex]) qed |
2445 by(auto simp add: vector_le_def mem_def[of _ convex]) qed |
2451 apply(rule that[of "{x::real^'n. \<forall>i. x$i=0 \<or> x$i=1}"]) |
2450 apply(rule that[of "{x::real^'n. \<forall>i. x$i=0 \<or> x$i=1}"]) |
2452 apply(rule finite_subset[of _ "(\<lambda>s. (\<chi> i. if i\<in>s then 1::real else 0)::real^'n) ` UNIV"]) |
2451 apply(rule finite_subset[of _ "(\<lambda>s. (\<chi> i. if i\<in>s then 1::real else 0)::real^'n) ` UNIV"]) |
2453 prefer 3 apply(rule unit_interval_convex_hull) apply rule unfolding mem_Collect_eq proof- |
2452 prefer 3 apply(rule unit_interval_convex_hull) apply rule unfolding mem_Collect_eq proof- |
2454 fix x::"real^'n" assume as:"\<forall>i. x $ i = 0 \<or> x $ i = 1" |
2453 fix x::"real^'n" assume as:"\<forall>i. x $ i = 0 \<or> x $ i = 1" |
2455 show "x \<in> (\<lambda>s. \<chi> i. if i \<in> s then 1 else 0) ` UNIV" apply(rule image_eqI[where x="{i. x$i = 1}"]) |
2454 show "x \<in> (\<lambda>s. \<chi> i. if i \<in> s then 1 else 0) ` UNIV" apply(rule image_eqI[where x="{i. x$i = 1}"]) |
2456 unfolding Cart_eq using as by(auto simp add:Cart_lambda_beta) qed auto |
2455 unfolding Cart_eq using as by auto qed auto |
2457 |
2456 |
2458 subsection {* Hence any cube (could do any nonempty interval). *} |
2457 subsection {* Hence any cube (could do any nonempty interval). *} |
2459 |
2458 |
2460 lemma cube_convex_hull: |
2459 lemma cube_convex_hull: |
2461 assumes "0 < d" obtains s::"(real^'n) set" where "finite s" "{x - (\<chi> i. d) .. x + (\<chi> i. d)} = convex hull s" proof- |
2460 assumes "0 < d" obtains s::"(real^'n) set" where "finite s" "{x - (\<chi> i. d) .. x + (\<chi> i. d)} = convex hull s" proof- |
2462 let ?d = "(\<chi> i. d)::real^'n" |
2461 let ?d = "(\<chi> i. d)::real^'n" |
2463 have *:"{x - ?d .. x + ?d} = (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` {0 .. 1}" apply(rule set_ext, rule) |
2462 have *:"{x - ?d .. x + ?d} = (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` {0 .. 1}" apply(rule set_ext, rule) |
2464 unfolding image_iff defer apply(erule bexE) proof- |
2463 unfolding image_iff defer apply(erule bexE) proof- |
2465 fix y assume as:"y\<in>{x - ?d .. x + ?d}" |
2464 fix y assume as:"y\<in>{x - ?d .. x + ?d}" |
2466 { fix i::'n have "x $ i \<le> d + y $ i" "y $ i \<le> d + x $ i" using as[unfolded mem_interval, THEN spec[where x=i]] |
2465 { fix i::'n have "x $ i \<le> d + y $ i" "y $ i \<le> d + x $ i" using as[unfolded mem_interval, THEN spec[where x=i]] |
2467 by(auto simp add: vector_component) |
2466 by auto |
2468 hence "1 \<ge> inverse d * (x $ i - y $ i)" "1 \<ge> inverse d * (y $ i - x $ i)" |
2467 hence "1 \<ge> inverse d * (x $ i - y $ i)" "1 \<ge> inverse d * (y $ i - x $ i)" |
2469 apply(rule_tac[!] mult_left_le_imp_le[OF _ assms]) unfolding mult_assoc[THEN sym] |
2468 apply(rule_tac[!] mult_left_le_imp_le[OF _ assms]) unfolding mult_assoc[THEN sym] |
2470 using assms by(auto simp add: field_simps right_inverse) |
2469 using assms by(auto simp add: field_simps) |
2471 hence "inverse d * (x $ i * 2) \<le> 2 + inverse d * (y $ i * 2)" |
2470 hence "inverse d * (x $ i * 2) \<le> 2 + inverse d * (y $ i * 2)" |
2472 "inverse d * (y $ i * 2) \<le> 2 + inverse d * (x $ i * 2)" by(auto simp add:field_simps) } |
2471 "inverse d * (y $ i * 2) \<le> 2 + inverse d * (x $ i * 2)" by(auto simp add:field_simps) } |
2473 hence "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> {0..1}" unfolding mem_interval using assms |
2472 hence "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> {0..1}" unfolding mem_interval using assms |
2474 by(auto simp add: Cart_eq vector_component_simps field_simps) |
2473 by(auto simp add: Cart_eq field_simps) |
2475 thus "\<exists>z\<in>{0..1}. y = x - ?d + (2 * d) *\<^sub>R z" apply- apply(rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI) |
2474 thus "\<exists>z\<in>{0..1}. y = x - ?d + (2 * d) *\<^sub>R z" apply- apply(rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI) |
2476 using assms by(auto simp add: Cart_eq vector_le_def Cart_lambda_beta) |
2475 using assms by(auto simp add: Cart_eq vector_le_def) |
2477 next |
2476 next |
2478 fix y z assume as:"z\<in>{0..1}" "y = x - ?d + (2*d) *\<^sub>R z" |
2477 fix y z assume as:"z\<in>{0..1}" "y = x - ?d + (2*d) *\<^sub>R z" |
2479 have "\<And>i. 0 \<le> d * z $ i \<and> d * z $ i \<le> d" using assms as(1)[unfolded mem_interval] apply(erule_tac x=i in allE) |
2478 have "\<And>i. 0 \<le> d * z $ i \<and> d * z $ i \<le> d" using assms as(1)[unfolded mem_interval] apply(erule_tac x=i in allE) |
2480 apply rule apply(rule mult_nonneg_nonneg) prefer 3 apply(rule mult_right_le_one_le) |
2479 apply rule apply(rule mult_nonneg_nonneg) prefer 3 apply(rule mult_right_le_one_le) |
2481 using assms by(auto simp add: vector_component_simps Cart_eq) |
2480 using assms by(auto simp add: Cart_eq) |
2482 thus "y \<in> {x - ?d..x + ?d}" unfolding as(2) mem_interval apply- apply rule using as(1)[unfolded mem_interval] |
2481 thus "y \<in> {x - ?d..x + ?d}" unfolding as(2) mem_interval apply- apply rule using as(1)[unfolded mem_interval] |
2483 apply(erule_tac x=i in allE) using assms by(auto simp add: vector_component_simps Cart_eq) qed |
2482 apply(erule_tac x=i in allE) using assms by(auto simp add: Cart_eq) qed |
2484 obtain s where "finite s" "{0..1::real^'n} = convex hull s" using unit_cube_convex_hull by auto |
2483 obtain s where "finite s" "{0..1::real^'n} = convex hull s" using unit_cube_convex_hull by auto |
2485 thus ?thesis apply(rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` s"]) unfolding * and convex_hull_affinity by auto qed |
2484 thus ?thesis apply(rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` s"]) unfolding * and convex_hull_affinity by auto qed |
2486 |
2485 |
2487 subsection {* Bounded convex function on open set is continuous. *} |
2486 subsection {* Bounded convex function on open set is continuous. *} |
2488 |
2487 |
2568 then obtain e where e:"cball x e \<subseteq> s" "e>0" using assms(1) unfolding open_contains_cball by auto |
2567 then obtain e where e:"cball x e \<subseteq> s" "e>0" using assms(1) unfolding open_contains_cball by auto |
2569 def d \<equiv> "e / real CARD('n)" |
2568 def d \<equiv> "e / real CARD('n)" |
2570 have "0 < d" unfolding d_def using `e>0` dimge1 by(rule_tac divide_pos_pos, auto) |
2569 have "0 < d" unfolding d_def using `e>0` dimge1 by(rule_tac divide_pos_pos, auto) |
2571 let ?d = "(\<chi> i. d)::real^'n" |
2570 let ?d = "(\<chi> i. d)::real^'n" |
2572 obtain c where c:"finite c" "{x - ?d..x + ?d} = convex hull c" using cube_convex_hull[OF `d>0`, of x] by auto |
2571 obtain c where c:"finite c" "{x - ?d..x + ?d} = convex hull c" using cube_convex_hull[OF `d>0`, of x] by auto |
2573 have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by(auto simp add:vector_component_simps) |
2572 have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by auto |
2574 hence "c\<noteq>{}" using c by(auto simp add:convex_hull_empty) |
2573 hence "c\<noteq>{}" using c by auto |
2575 def k \<equiv> "Max (f ` c)" |
2574 def k \<equiv> "Max (f ` c)" |
2576 have "convex_on {x - ?d..x + ?d} f" apply(rule convex_on_subset[OF assms(2)]) |
2575 have "convex_on {x - ?d..x + ?d} f" apply(rule convex_on_subset[OF assms(2)]) |
2577 apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof |
2576 apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof |
2578 fix z assume z:"z\<in>{x - ?d..x + ?d}" |
2577 fix z assume z:"z\<in>{x - ?d..x + ?d}" |
2579 have e:"e = setsum (\<lambda>i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1 |
2578 have e:"e = setsum (\<lambda>i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1 |
2580 by (metis eq_divide_imp mult_frac_num real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute) |
2579 by (metis eq_divide_imp mult_frac_num real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute) |
2581 show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono) |
2580 show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono) |
2582 using z[unfolded mem_interval] apply(erule_tac x=i in allE) by(auto simp add:field_simps vector_component_simps) qed |
2581 using z[unfolded mem_interval] apply(erule_tac x=i in allE) by auto qed |
2583 hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption |
2582 hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption |
2584 unfolding k_def apply(rule, rule Max_ge) using c(1) by auto |
2583 unfolding k_def apply(rule, rule Max_ge) using c(1) by auto |
2585 have "d \<le> e" unfolding d_def apply(rule mult_imp_div_pos_le) using `e>0` dimge1 unfolding mult_le_cancel_left1 using real_dimindex_ge_1 by auto |
2584 have "d \<le> e" unfolding d_def apply(rule mult_imp_div_pos_le) using `e>0` dimge1 unfolding mult_le_cancel_left1 using real_dimindex_ge_1 by auto |
2586 hence dsube:"cball x d \<subseteq> cball x e" unfolding subset_eq Ball_def mem_cball by auto |
2585 hence dsube:"cball x d \<subseteq> cball x e" unfolding subset_eq Ball_def mem_cball by auto |
2587 have conv:"convex_on (cball x d) f" apply(rule convex_on_subset, rule convex_on_subset[OF assms(2)]) apply(rule e(1)) using dsube by auto |
2586 have conv:"convex_on (cball x d) f" apply(rule convex_on_subset, rule convex_on_subset[OF assms(2)]) apply(rule e(1)) using dsube by auto |
2588 hence "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)" apply(rule_tac convex_bounds_lemma) apply assumption proof |
2587 hence "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)" apply(rule_tac convex_bounds_lemma) apply assumption proof |
2589 fix y assume y:"y\<in>cball x d" |
2588 fix y assume y:"y\<in>cball x d" |
2590 { fix i::'n have "x $ i - d \<le> y $ i" "y $ i \<le> x $ i + d" |
2589 { fix i::'n have "x $ i - d \<le> y $ i" "y $ i \<le> x $ i + d" |
2591 using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by(auto simp add: vector_component) } |
2590 using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by auto } |
2592 thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm |
2591 thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm |
2593 by(auto simp add: vector_component_simps) qed |
2592 by auto qed |
2594 hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous) |
2593 hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous) |
2595 apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball) |
2594 apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball) |
2596 apply force |
2595 apply force |
2597 done |
2596 done |
2598 thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball] |
2597 thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball] |
2714 fix u assume as:"x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1" |
2713 fix u assume as:"x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1" |
2715 hence *:"a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)" |
2714 hence *:"a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)" |
2716 unfolding as(1) by(auto simp add:algebra_simps) |
2715 unfolding as(1) by(auto simp add:algebra_simps) |
2717 show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)" |
2716 show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)" |
2718 unfolding norm_minus_commute[of x a] * Cart_eq using as(2,3) |
2717 unfolding norm_minus_commute[of x a] * Cart_eq using as(2,3) |
2719 by(auto simp add: vector_component_simps field_simps) |
2718 by(auto simp add: field_simps) |
2720 next assume as:"dist a b = dist a x + dist x b" |
2719 next assume as:"dist a b = dist a x + dist x b" |
2721 have "norm (a - x) / norm (a - b) \<le> 1" unfolding divide_le_eq_1_pos[OF Fal2] unfolding as[unfolded dist_norm] norm_ge_zero by auto |
2720 have "norm (a - x) / norm (a - b) \<le> 1" unfolding divide_le_eq_1_pos[OF Fal2] unfolding as[unfolded dist_norm] norm_ge_zero by auto |
2722 thus "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" apply(rule_tac x="dist a x / dist a b" in exI) |
2721 thus "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" apply(rule_tac x="dist a x / dist a b" in exI) |
2723 unfolding dist_norm Cart_eq apply- apply rule defer apply(rule, rule divide_nonneg_pos) prefer 4 proof rule |
2722 unfolding dist_norm Cart_eq apply- apply rule defer apply(rule, rule divide_nonneg_pos) prefer 4 proof rule |
2724 fix i::'n have "((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $ i = |
2723 fix i::'n have "((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $ i = |
2725 ((norm (a - b) - norm (a - x)) * (a $ i) + norm (a - x) * (b $ i)) / norm (a - b)" |
2724 ((norm (a - b) - norm (a - x)) * (a $ i) + norm (a - x) * (b $ i)) / norm (a - b)" |
2726 using Fal by(auto simp add:vector_component_simps field_simps) |
2725 using Fal by(auto simp add: field_simps) |
2727 also have "\<dots> = x$i" apply(rule divide_eq_imp[OF Fal]) |
2726 also have "\<dots> = x$i" apply(rule divide_eq_imp[OF Fal]) |
2728 unfolding as[unfolded dist_norm] using as[unfolded dist_triangle_eq Cart_eq,rule_format, of i] |
2727 unfolding as[unfolded dist_norm] using as[unfolded dist_triangle_eq Cart_eq,rule_format, of i] |
2729 by(auto simp add:field_simps vector_component_simps) |
2728 by(auto simp add:field_simps) |
2730 finally show "x $ i = ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $ i" by auto |
2729 finally show "x $ i = ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $ i" by auto |
2731 qed(insert Fal2, auto) qed qed |
2730 qed(insert Fal2, auto) qed qed |
2732 |
2731 |
2733 lemma between_midpoint: fixes a::"real^'n" shows |
2732 lemma between_midpoint: fixes a::"real^'n" shows |
2734 "between (a,b) (midpoint a b)" (is ?t1) |
2733 "between (a,b) (midpoint a b)" (is ?t1) |
2735 "between (b,a) (midpoint a b)" (is ?t2) |
2734 "between (b,a) (midpoint a b)" (is ?t2) |
2736 proof- have *:"\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y" by auto |
2735 proof- have *:"\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y" by auto |
2737 show ?t1 ?t2 unfolding between midpoint_def dist_norm apply(rule_tac[!] *) |
2736 show ?t1 ?t2 unfolding between midpoint_def dist_norm apply(rule_tac[!] *) |
2738 by(auto simp add:field_simps Cart_eq vector_component_simps) qed |
2737 by(auto simp add:field_simps Cart_eq) qed |
2739 |
2738 |
2740 lemma between_mem_convex_hull: |
2739 lemma between_mem_convex_hull: |
2741 "between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}" |
2740 "between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}" |
2742 unfolding between_mem_segment segment_convex_hull .. |
2741 unfolding between_mem_segment segment_convex_hull .. |
2743 |
2742 |
2752 apply(rule) defer unfolding subset_eq Ball_def mem_ball proof(rule,rule) |
2751 apply(rule) defer unfolding subset_eq Ball_def mem_ball proof(rule,rule) |
2753 fix y assume as:"dist (x - e *\<^sub>R (x - c)) y < e * d" |
2752 fix y assume as:"dist (x - e *\<^sub>R (x - c)) y < e * d" |
2754 have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib) |
2753 have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib) |
2755 have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)" |
2754 have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)" |
2756 unfolding dist_norm unfolding norm_scaleR[THEN sym] apply(rule norm_eqI) using `e>0` |
2755 unfolding dist_norm unfolding norm_scaleR[THEN sym] apply(rule norm_eqI) using `e>0` |
2757 by(auto simp add:vector_component_simps Cart_eq field_simps) |
2756 by(auto simp add: Cart_eq field_simps) |
2758 also have "\<dots> = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:norm_eqI simp add: algebra_simps) |
2757 also have "\<dots> = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:norm_eqI simp add: algebra_simps) |
2759 also have "\<dots> < d" using as[unfolded dist_norm] and `e>0` |
2758 also have "\<dots> < d" using as[unfolded dist_norm] and `e>0` |
2760 by(auto simp add:pos_divide_less_eq[OF `e>0`] real_mult_commute) |
2759 by(auto simp add:pos_divide_less_eq[OF `e>0`] real_mult_commute) |
2761 finally show "y \<in> s" apply(subst *) apply(rule assms(1)[unfolded convex_alt,rule_format]) |
2760 finally show "y \<in> s" apply(subst *) apply(rule assms(1)[unfolded convex_alt,rule_format]) |
2762 apply(rule d[unfolded subset_eq,rule_format]) unfolding mem_ball using assms(3-5) by auto |
2761 apply(rule d[unfolded subset_eq,rule_format]) unfolding mem_ball using assms(3-5) by auto |
2824 apply(rule set_ext) unfolding mem_interior std_simplex unfolding subset_eq mem_Collect_eq Ball_def mem_ball |
2823 apply(rule set_ext) unfolding mem_interior std_simplex unfolding subset_eq mem_Collect_eq Ball_def mem_ball |
2825 unfolding Ball_def[symmetric] apply rule apply(erule exE, (erule conjE)+) defer apply(erule conjE) proof- |
2824 unfolding Ball_def[symmetric] apply rule apply(erule exE, (erule conjE)+) defer apply(erule conjE) proof- |
2826 fix x::"real^'n" and e assume "0<e" and as:"\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x. 0 \<le> xa $ x) \<and> setsum (op $ xa) UNIV \<le> 1" |
2825 fix x::"real^'n" and e assume "0<e" and as:"\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x. 0 \<le> xa $ x) \<and> setsum (op $ xa) UNIV \<le> 1" |
2827 show "(\<forall>xa. 0 < x $ xa) \<and> setsum (op $ x) UNIV < 1" apply(rule,rule) proof- |
2826 show "(\<forall>xa. 0 < x $ xa) \<and> setsum (op $ x) UNIV < 1" apply(rule,rule) proof- |
2828 fix i::'n show "0 < x $ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0` |
2827 fix i::'n show "0 < x $ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0` |
2829 unfolding dist_norm by(auto simp add: norm_basis vector_component_simps basis_component elim:allE[where x=i]) |
2828 unfolding dist_norm by(auto simp add: norm_basis elim:allE[where x=i]) |
2830 next guess a using UNIV_witness[where 'a='n] .. |
2829 next guess a using UNIV_witness[where 'a='n] .. |
2831 have **:"dist x (x + (e / 2) *\<^sub>R basis a) < e" using `e>0` and norm_basis[of a] |
2830 have **:"dist x (x + (e / 2) *\<^sub>R basis a) < e" using `e>0` and norm_basis[of a] |
2832 unfolding dist_norm by(auto simp add: vector_component_simps basis_component intro!: mult_strict_left_mono_comm) |
2831 unfolding dist_norm by(auto intro!: mult_strict_left_mono_comm) |
2833 have "\<And>i. (x + (e / 2) *\<^sub>R basis a) $ i = x$i + (if i = a then e/2 else 0)" by(auto simp add:vector_component_simps) |
2832 have "\<And>i. (x + (e / 2) *\<^sub>R basis a) $ i = x$i + (if i = a then e/2 else 0)" by auto |
2834 hence *:"setsum (op $ (x + (e / 2) *\<^sub>R basis a)) UNIV = setsum (\<lambda>i. x$i + (if a = i then e/2 else 0)) UNIV" by(rule_tac setsum_cong, auto) |
2833 hence *:"setsum (op $ (x + (e / 2) *\<^sub>R basis a)) UNIV = setsum (\<lambda>i. x$i + (if a = i then e/2 else 0)) UNIV" by(rule_tac setsum_cong, auto) |
2835 have "setsum (op $ x) UNIV < setsum (op $ (x + (e / 2) *\<^sub>R basis a)) UNIV" unfolding * setsum_addf |
2834 have "setsum (op $ x) UNIV < setsum (op $ (x + (e / 2) *\<^sub>R basis a)) UNIV" unfolding * setsum_addf |
2836 using `0<e` dimindex_ge_1 by(auto simp add: setsum_delta') |
2835 using `0<e` dimindex_ge_1 by(auto simp add: setsum_delta') |
2837 also have "\<dots> \<le> 1" using ** apply(drule_tac as[rule_format]) by auto |
2836 also have "\<dots> \<le> 1" using ** apply(drule_tac as[rule_format]) by auto |
2838 finally show "setsum (op $ x) UNIV < 1" by auto qed |
2837 finally show "setsum (op $ x) UNIV < 1" by auto qed |
2845 ultimately show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> (\<forall>i. 0 \<le> y $ i) \<and> setsum (op $ y) UNIV \<le> 1" |
2844 ultimately show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> (\<forall>i. 0 \<le> y $ i) \<and> setsum (op $ y) UNIV \<le> 1" |
2846 apply(rule_tac x="min (Min ((op $ x) ` UNIV)) ?D" in exI) apply rule defer apply(rule,rule) proof- |
2845 apply(rule_tac x="min (Min ((op $ x) ` UNIV)) ?D" in exI) apply rule defer apply(rule,rule) proof- |
2847 fix y assume y:"dist x y < min (Min (op $ x ` UNIV)) ?d" |
2846 fix y assume y:"dist x y < min (Min (op $ x ` UNIV)) ?d" |
2848 have "setsum (op $ y) UNIV \<le> setsum (\<lambda>i. x$i + ?d) UNIV" proof(rule setsum_mono) |
2847 have "setsum (op $ y) UNIV \<le> setsum (\<lambda>i. x$i + ?d) UNIV" proof(rule setsum_mono) |
2849 fix i::'n have "abs (y$i - x$i) < ?d" apply(rule le_less_trans) using component_le_norm[of "y - x" i] |
2848 fix i::'n have "abs (y$i - x$i) < ?d" apply(rule le_less_trans) using component_le_norm[of "y - x" i] |
2850 using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add:vector_component_simps norm_minus_commute) |
2849 using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add: norm_minus_commute) |
2851 thus "y $ i \<le> x $ i + ?d" by auto qed |
2850 thus "y $ i \<le> x $ i + ?d" by auto qed |
2852 also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat using dimindex_ge_1 by(auto simp add: Suc_le_eq) |
2851 also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat using dimindex_ge_1 by(auto simp add: Suc_le_eq) |
2853 finally show "(\<forall>i. 0 \<le> y $ i) \<and> setsum (op $ y) UNIV \<le> 1" apply- proof(rule,rule) |
2852 finally show "(\<forall>i. 0 \<le> y $ i) \<and> setsum (op $ y) UNIV \<le> 1" apply- proof(rule,rule) |
2854 fix i::'n have "norm (x - y) < x$i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1] |
2853 fix i::'n have "norm (x - y) < x$i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1] |
2855 using Min_gr_iff[of "op $ x ` dimset x"] dimindex_ge_1 by auto |
2854 by auto |
2856 thus "0 \<le> y$i" using component_le_norm[of "x - y" i] and as(1)[rule_format, of i] by(auto simp add: vector_component_simps) |
2855 thus "0 \<le> y$i" using component_le_norm[of "x - y" i] and as(1)[rule_format, of i] by auto |
2857 qed auto qed auto qed |
2856 qed auto qed auto qed |
2858 |
2857 |
2859 lemma interior_std_simplex_nonempty: obtains a::"real^'n" where |
2858 lemma interior_std_simplex_nonempty: obtains a::"real^'n" where |
2860 "a \<in> interior(convex hull (insert 0 {basis i | i . i \<in> UNIV}))" proof- |
2859 "a \<in> interior(convex hull (insert 0 {basis i | i . i \<in> UNIV}))" proof- |
2861 let ?D = "UNIV::'n set" let ?a = "setsum (\<lambda>b::real^'n. inverse (2 * real CARD('n)) *\<^sub>R b) {(basis i) | i. i \<in> ?D}" |
2860 let ?D = "UNIV::'n set" let ?a = "setsum (\<lambda>b::real^'n. inverse (2 * real CARD('n)) *\<^sub>R b) {(basis i) | i. i \<in> ?D}" |
3037 |
3036 |
3038 lemma simple_path_reversepath: assumes "simple_path g" shows "simple_path (reversepath g)" |
3037 lemma simple_path_reversepath: assumes "simple_path g" shows "simple_path (reversepath g)" |
3039 using assms unfolding simple_path_def reversepath_def apply- apply(rule ballI)+ |
3038 using assms unfolding simple_path_def reversepath_def apply- apply(rule ballI)+ |
3040 apply(erule_tac x="1-x" in ballE, erule_tac x="1-y" in ballE) |
3039 apply(erule_tac x="1-x" in ballE, erule_tac x="1-y" in ballE) |
3041 unfolding mem_interval_1 by auto |
3040 unfolding mem_interval_1 by auto |
3042 |
|
3043 (** move this **) |
|
3044 declare vector_scaleR_component[simp] |
|
3045 |
3041 |
3046 lemma simple_path_join_loop: |
3042 lemma simple_path_join_loop: |
3047 assumes "injective_path g1" "injective_path g2" "pathfinish g2 = pathstart g1" |
3043 assumes "injective_path g1" "injective_path g2" "pathfinish g2 = pathstart g1" |
3048 "(path_image g1 \<inter> path_image g2) \<subseteq> {pathstart g1,pathstart g2}" |
3044 "(path_image g1 \<inter> path_image g2) \<subseteq> {pathstart g1,pathstart g2}" |
3049 shows "simple_path(g1 +++ g2)" |
3045 shows "simple_path(g1 +++ g2)" |
3388 case (Suc k) show ?case proof(cases "k = 1") |
3384 case (Suc k) show ?case proof(cases "k = 1") |
3389 case False from Suc have d:"k \<in> {1..CARD('n)}" "Suc k \<in> {1..CARD('n)}" by auto |
3385 case False from Suc have d:"k \<in> {1..CARD('n)}" "Suc k \<in> {1..CARD('n)}" by auto |
3390 hence "\<psi> k \<noteq> \<psi> (Suc k)" using \<psi>[unfolded bij_betw_def inj_on_def, THEN conjunct1, THEN bspec[where x=k]] by auto |
3386 hence "\<psi> k \<noteq> \<psi> (Suc k)" using \<psi>[unfolded bij_betw_def inj_on_def, THEN conjunct1, THEN bspec[where x=k]] by auto |
3391 hence **:"?basis k + ?basis (Suc k) \<in> {x. 0 < inner (?basis (Suc k)) x} \<inter> (?A k)" |
3387 hence **:"?basis k + ?basis (Suc k) \<in> {x. 0 < inner (?basis (Suc k)) x} \<inter> (?A k)" |
3392 "?basis k - ?basis (Suc k) \<in> {x. 0 > inner (?basis (Suc k)) x} \<inter> ({x. 0 < inner (?basis (Suc k)) x} \<union> (?A k))" using d |
3388 "?basis k - ?basis (Suc k) \<in> {x. 0 > inner (?basis (Suc k)) x} \<inter> ({x. 0 < inner (?basis (Suc k)) x} \<union> (?A k))" using d |
3393 by(auto simp add: inner_basis vector_component_simps intro!:bexI[where x=k]) |
3389 by(auto simp add: inner_basis intro!:bexI[where x=k]) |
3394 show ?thesis unfolding * Un_assoc apply(rule path_connected_Un) defer apply(rule path_connected_Un) |
3390 show ?thesis unfolding * Un_assoc apply(rule path_connected_Un) defer apply(rule path_connected_Un) |
3395 prefer 5 apply(rule_tac[1-2] convex_imp_path_connected, rule convex_halfspace_lt, rule convex_halfspace_gt) |
3391 prefer 5 apply(rule_tac[1-2] convex_imp_path_connected, rule convex_halfspace_lt, rule convex_halfspace_gt) |
3396 apply(rule Suc(1)) using d ** False by auto |
3392 apply(rule Suc(1)) using d ** False by auto |
3397 next case True hence d:"1\<in>{1..CARD('n)}" "2\<in>{1..CARD('n)}" using Suc(2) by auto |
3393 next case True hence d:"1\<in>{1..CARD('n)}" "2\<in>{1..CARD('n)}" using Suc(2) by auto |
3398 have ***:"Suc 1 = 2" by auto |
3394 have ***:"Suc 1 = 2" by auto |
3402 thus ?thesis unfolding * True unfolding ** neq_iff bex_disj_distrib apply - |
3398 thus ?thesis unfolding * True unfolding ** neq_iff bex_disj_distrib apply - |
3403 apply(rule path_connected_Un, rule_tac[1-2] path_connected_Un) defer 3 apply(rule_tac[1-4] convex_imp_path_connected) |
3399 apply(rule path_connected_Un, rule_tac[1-2] path_connected_Un) defer 3 apply(rule_tac[1-4] convex_imp_path_connected) |
3404 apply(rule_tac[5] x=" ?basis 1 + ?basis 2" in nequals0I) |
3400 apply(rule_tac[5] x=" ?basis 1 + ?basis 2" in nequals0I) |
3405 apply(rule_tac[6] x="-?basis 1 + ?basis 2" in nequals0I) |
3401 apply(rule_tac[6] x="-?basis 1 + ?basis 2" in nequals0I) |
3406 apply(rule_tac[7] x="-?basis 1 - ?basis 2" in nequals0I) |
3402 apply(rule_tac[7] x="-?basis 1 - ?basis 2" in nequals0I) |
3407 using d unfolding *** by(auto intro!: convex_halfspace_gt convex_halfspace_lt, auto simp add:vector_component_simps inner_basis) |
3403 using d unfolding *** by(auto intro!: convex_halfspace_gt convex_halfspace_lt, auto simp add: inner_basis) |
3408 qed qed auto qed note lem = this |
3404 qed qed auto qed note lem = this |
3409 |
3405 |
3410 have ***:"\<And>x::real^'n. (\<exists>i\<in>{1..CARD('n)}. inner (basis (\<psi> i)) x \<noteq> 0) \<longleftrightarrow> (\<exists>i. inner (basis i) x \<noteq> 0)" |
3406 have ***:"\<And>x::real^'n. (\<exists>i\<in>{1..CARD('n)}. inner (basis (\<psi> i)) x \<noteq> 0) \<longleftrightarrow> (\<exists>i. inner (basis i) x \<noteq> 0)" |
3411 apply rule apply(erule bexE) apply(rule_tac x="\<psi> i" in exI) defer apply(erule exE) proof- |
3407 apply rule apply(erule bexE) apply(rule_tac x="\<psi> i" in exI) defer apply(erule exE) proof- |
3412 fix x::"real^'n" and i assume as:"inner (basis i) x \<noteq> 0" |
3408 fix x::"real^'n" and i assume as:"inner (basis i) x \<noteq> 0" |
3430 unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto split:split_if_asm) |
3426 unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto split:split_if_asm) |
3431 have "continuous_on (UNIV - {0}) (\<lambda>x::real^'n. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within |
3427 have "continuous_on (UNIV - {0}) (\<lambda>x::real^'n. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within |
3432 apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within) |
3428 apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within) |
3433 apply(rule continuous_at_norm[unfolded o_def]) by auto |
3429 apply(rule continuous_at_norm[unfolded o_def]) by auto |
3434 thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms] |
3430 thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms] |
3435 by(auto intro!: path_connected_continuous_image continuous_on_intros continuous_on_mul) qed |
3431 by(auto intro!: path_connected_continuous_image continuous_on_intros) qed |
3436 |
3432 |
3437 lemma connected_sphere: "2 \<le> CARD('n) \<Longrightarrow> connected {x::real^'n. norm(x - a) = r}" |
3433 lemma connected_sphere: "2 \<le> CARD('n) \<Longrightarrow> connected {x::real^'n. norm(x - a) = r}" |
3438 using path_connected_sphere path_connected_imp_connected by auto |
3434 using path_connected_sphere path_connected_imp_connected by auto |
3439 |
3435 |
3440 end |
3436 end |