349 |
398 |
350 lemma affine_Int: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)" |
399 lemma affine_Int: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)" |
351 unfolding affine_def by auto |
400 unfolding affine_def by auto |
352 |
401 |
353 lemma affine_affine_hull: "affine(affine hull s)" |
402 lemma affine_affine_hull: "affine(affine hull s)" |
354 unfolding hull_def using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"] |
403 unfolding hull_def |
355 by auto |
404 using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"] by auto |
356 |
405 |
357 lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s" |
406 lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s" |
358 by (metis affine_affine_hull hull_same) |
407 by (metis affine_affine_hull hull_same) |
|
408 |
359 |
409 |
360 subsubsection {* Some explicit formulations (from Lars Schewe) *} |
410 subsubsection {* Some explicit formulations (from Lars Schewe) *} |
361 |
411 |
362 lemma affine: fixes V::"'a::real_vector set" |
412 lemma affine: |
363 shows "affine V \<longleftrightarrow> (\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (setsum (\<lambda>x. (u x) *\<^sub>R x)) s \<in> V)" |
413 fixes V::"'a::real_vector set" |
364 unfolding affine_def apply rule apply(rule, rule, rule) apply(erule conjE)+ |
414 shows "affine V \<longleftrightarrow> |
365 defer apply(rule, rule, rule, rule, rule) proof- |
415 (\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (setsum (\<lambda>x. (u x) *\<^sub>R x)) s \<in> V)" |
366 fix x y u v assume as:"x \<in> V" "y \<in> V" "u + v = (1::real)" |
416 unfolding affine_def |
|
417 apply rule |
|
418 apply(rule, rule, rule) |
|
419 apply(erule conjE)+ |
|
420 defer |
|
421 apply (rule, rule, rule, rule, rule) |
|
422 proof - |
|
423 fix x y u v |
|
424 assume as: "x \<in> V" "y \<in> V" "u + v = (1::real)" |
367 "\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" |
425 "\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" |
368 thus "u *\<^sub>R x + v *\<^sub>R y \<in> V" apply(cases "x=y") |
426 then show "u *\<^sub>R x + v *\<^sub>R y \<in> V" |
369 using as(4)[THEN spec[where x="{x,y}"], THEN spec[where x="\<lambda>w. if w = x then u else v"]] and as(1-3) |
427 apply (cases "x = y") |
370 by(auto simp add: scaleR_left_distrib[THEN sym]) |
428 using as(4)[THEN spec[where x="{x,y}"], THEN spec[where x="\<lambda>w. if w = x then u else v"]] |
|
429 and as(1-3) |
|
430 by (auto simp add: scaleR_left_distrib[THEN sym]) |
371 next |
431 next |
372 fix s u assume as:"\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V" |
432 fix s u |
|
433 assume as: "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V" |
373 "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = (1::real)" |
434 "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = (1::real)" |
374 def n \<equiv> "card s" |
435 def n \<equiv> "card s" |
375 have "card s = 0 \<or> card s = 1 \<or> card s = 2 \<or> card s > 2" by auto |
436 have "card s = 0 \<or> card s = 1 \<or> card s = 2 \<or> card s > 2" by auto |
376 thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" proof(auto simp only: disjE) |
437 then show "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" |
377 assume "card s = 2" hence "card s = Suc (Suc 0)" by auto |
438 proof (auto simp only: disjE) |
|
439 assume "card s = 2" |
|
440 then have "card s = Suc (Suc 0)" by auto |
378 then obtain a b where "s = {a, b}" unfolding card_Suc_eq by auto |
441 then obtain a b where "s = {a, b}" unfolding card_Suc_eq by auto |
379 thus ?thesis using as(1)[THEN bspec[where x=a], THEN bspec[where x=b]] using as(4,5) |
442 then show ?thesis |
380 by(auto simp add: setsum_clauses(2)) |
443 using as(1)[THEN bspec[where x=a], THEN bspec[where x=b]] using as(4,5) |
381 next assume "card s > 2" thus ?thesis using as and n_def proof(induct n arbitrary: u s) |
444 by (auto simp add: setsum_clauses(2)) |
382 case (Suc n) fix s::"'a set" and u::"'a \<Rightarrow> real" |
445 next |
383 assume IA:"\<And>u s. \<lbrakk>2 < card s; \<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V; finite s; |
446 assume "card s > 2" |
384 s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n = card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" and |
447 then show ?thesis using as and n_def |
385 as:"Suc n = card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V" |
448 proof (induct n arbitrary: u s) |
|
449 case 0 |
|
450 then show ?case by auto |
|
451 next |
|
452 case (Suc n) |
|
453 fix s :: "'a set" and u :: "'a \<Rightarrow> real" |
|
454 assume IA: |
|
455 "\<And>u s. \<lbrakk>2 < card s; \<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V; finite s; |
|
456 s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n = card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" |
|
457 and as: |
|
458 "Suc n = card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V" |
386 "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = 1" |
459 "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = 1" |
387 have "\<exists>x\<in>s. u x \<noteq> 1" proof(rule_tac ccontr) |
460 have "\<exists>x\<in>s. u x \<noteq> 1" |
388 assume " \<not> (\<exists>x\<in>s. u x \<noteq> 1)" hence "setsum u s = real_of_nat (card s)" unfolding card_eq_setsum by auto |
461 proof (rule ccontr) |
389 thus False using as(7) and `card s > 2` by (metis One_nat_def |
462 assume "\<not> ?thesis" |
390 less_Suc0 Zero_not_Suc of_nat_1 of_nat_eq_iff numeral_2_eq_2) |
463 then have "setsum u s = real_of_nat (card s)" unfolding card_eq_setsum by auto |
|
464 then show False |
|
465 using as(7) and `card s > 2` |
|
466 by (metis One_nat_def less_Suc0 Zero_not_Suc of_nat_1 of_nat_eq_iff numeral_2_eq_2) |
391 qed |
467 qed |
392 then obtain x where x:"x\<in>s" "u x \<noteq> 1" by auto |
468 then obtain x where x:"x\<in>s" "u x \<noteq> 1" by auto |
393 |
469 |
394 have c:"card (s - {x}) = card s - 1" apply(rule card_Diff_singleton) using `x\<in>s` as(4) by auto |
470 have c: "card (s - {x}) = card s - 1" |
395 have *:"s = insert x (s - {x})" "finite (s - {x})" using `x\<in>s` and as(4) by auto |
471 apply (rule card_Diff_singleton) using `x\<in>s` as(4) by auto |
396 have **:"setsum u (s - {x}) = 1 - u x" |
472 have *: "s = insert x (s - {x})" "finite (s - {x})" |
|
473 using `x\<in>s` and as(4) by auto |
|
474 have **: "setsum u (s - {x}) = 1 - u x" |
397 using setsum_clauses(2)[OF *(2), of u x, unfolded *(1)[THEN sym] as(7)] by auto |
475 using setsum_clauses(2)[OF *(2), of u x, unfolded *(1)[THEN sym] as(7)] by auto |
398 have ***:"inverse (1 - u x) * setsum u (s - {x}) = 1" unfolding ** using `u x \<noteq> 1` by auto |
476 have ***: "inverse (1 - u x) * setsum u (s - {x}) = 1" |
399 have "(\<Sum>xa\<in>s - {x}. (inverse (1 - u x) * u xa) *\<^sub>R xa) \<in> V" proof(cases "card (s - {x}) > 2") |
477 unfolding ** using `u x \<noteq> 1` by auto |
400 case True hence "s - {x} \<noteq> {}" "card (s - {x}) = n" unfolding c and as(1)[symmetric] proof(rule_tac ccontr) |
478 have "(\<Sum>xa\<in>s - {x}. (inverse (1 - u x) * u xa) *\<^sub>R xa) \<in> V" |
401 assume "\<not> s - {x} \<noteq> {}" hence "card (s - {x}) = 0" unfolding card_0_eq[OF *(2)] by simp |
479 proof (cases "card (s - {x}) > 2") |
402 thus False using True by auto qed auto |
480 case True |
403 thus ?thesis apply(rule_tac IA[of "s - {x}" "\<lambda>y. (inverse (1 - u x) * u y)"]) |
481 then have "s - {x} \<noteq> {}" "card (s - {x}) = n" |
404 unfolding setsum_right_distrib[THEN sym] using as and *** and True by auto |
482 unfolding c and as(1)[symmetric] |
405 next case False hence "card (s - {x}) = Suc (Suc 0)" using as(2) and c by auto |
483 proof (rule_tac ccontr) |
|
484 assume "\<not> s - {x} \<noteq> {}" |
|
485 then have "card (s - {x}) = 0" unfolding card_0_eq[OF *(2)] by simp |
|
486 then show False using True by auto |
|
487 qed auto |
|
488 then show ?thesis |
|
489 apply (rule_tac IA[of "s - {x}" "\<lambda>y. (inverse (1 - u x) * u y)"]) |
|
490 unfolding setsum_right_distrib[THEN sym] using as and *** and True |
|
491 apply auto |
|
492 done |
|
493 next |
|
494 case False |
|
495 then have "card (s - {x}) = Suc (Suc 0)" using as(2) and c by auto |
406 then obtain a b where "(s - {x}) = {a, b}" "a\<noteq>b" unfolding card_Suc_eq by auto |
496 then obtain a b where "(s - {x}) = {a, b}" "a\<noteq>b" unfolding card_Suc_eq by auto |
407 thus ?thesis using as(3)[THEN bspec[where x=a], THEN bspec[where x=b]] |
497 then show ?thesis using as(3)[THEN bspec[where x=a], THEN bspec[where x=b]] |
408 using *** *(2) and `s \<subseteq> V` unfolding setsum_right_distrib by(auto simp add: setsum_clauses(2)) qed |
498 using *** *(2) and `s \<subseteq> V` |
409 hence "u x + (1 - u x) = 1 \<Longrightarrow> u x *\<^sub>R x + (1 - u x) *\<^sub>R ((\<Sum>xa\<in>s - {x}. u xa *\<^sub>R xa) /\<^sub>R (1 - u x)) \<in> V" |
499 unfolding setsum_right_distrib by (auto simp add: setsum_clauses(2)) |
410 apply-apply(rule as(3)[rule_format]) |
500 qed |
411 unfolding RealVector.scaleR_right.setsum using x(1) as(6) by auto |
501 then have "u x + (1 - u x) = 1 \<Longrightarrow> |
412 thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] |
502 u x *\<^sub>R x + (1 - u x) *\<^sub>R ((\<Sum>xa\<in>s - {x}. u xa *\<^sub>R xa) /\<^sub>R (1 - u x)) \<in> V" |
413 apply(subst *) unfolding setsum_clauses(2)[OF *(2)] |
503 apply - |
414 using `u x \<noteq> 1` by auto |
504 apply (rule as(3)[rule_format]) |
415 qed auto |
505 unfolding RealVector.scaleR_right.setsum |
416 next assume "card s = 1" then obtain a where "s={a}" by(auto simp add: card_Suc_eq) |
506 using x(1) as(6) apply auto |
417 thus ?thesis using as(4,5) by simp |
507 done |
418 qed(insert `s\<noteq>{}` `finite s`, auto) |
508 then show "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" |
|
509 unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] |
|
510 apply (subst *) |
|
511 unfolding setsum_clauses(2)[OF *(2)] |
|
512 using `u x \<noteq> 1` apply auto |
|
513 done |
|
514 qed |
|
515 next |
|
516 assume "card s = 1" |
|
517 then obtain a where "s={a}" by (auto simp add: card_Suc_eq) |
|
518 then show ?thesis using as(4,5) by simp |
|
519 qed (insert `s\<noteq>{}` `finite s`, auto) |
419 qed |
520 qed |
420 |
521 |
421 lemma affine_hull_explicit: |
522 lemma affine_hull_explicit: |
422 "affine hull p = {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> setsum (\<lambda>v. (u v) *\<^sub>R v) s = y}" |
523 "affine hull p = {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> setsum (\<lambda>v. (u v) *\<^sub>R v) s = y}" |
423 apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq |
524 apply (rule hull_unique) |
424 apply (erule exE)+ apply(erule conjE)+ prefer 2 apply rule proof- |
525 apply (subst subset_eq) |
425 fix x assume "x\<in>p" thus "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" |
526 prefer 3 |
426 apply(rule_tac x="{x}" in exI, rule_tac x="\<lambda>x. 1" in exI) by auto |
527 apply rule |
|
528 unfolding mem_Collect_eq |
|
529 apply (erule exE)+ |
|
530 apply (erule conjE)+ |
|
531 prefer 2 |
|
532 apply rule |
|
533 proof - |
|
534 fix x |
|
535 assume "x\<in>p" |
|
536 then show "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" |
|
537 apply (rule_tac x="{x}" in exI, rule_tac x="\<lambda>x. 1" in exI) |
|
538 apply auto |
|
539 done |
427 next |
540 next |
428 fix t x s u assume as:"p \<subseteq> t" "affine t" "finite s" "s \<noteq> {}" "s \<subseteq> p" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x" |
541 fix t x s u |
429 thus "x \<in> t" using as(2)[unfolded affine, THEN spec[where x=s], THEN spec[where x=u]] by auto |
542 assume as: "p \<subseteq> t" "affine t" "finite s" "s \<noteq> {}" "s \<subseteq> p" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x" |
|
543 then show "x \<in> t" |
|
544 using as(2)[unfolded affine, THEN spec[where x=s], THEN spec[where x=u]] by auto |
430 next |
545 next |
431 show "affine {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y}" unfolding affine_def |
546 show "affine {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y}" |
432 apply(rule,rule,rule,rule,rule) unfolding mem_Collect_eq proof- |
547 unfolding affine_def |
433 fix u v ::real assume uv:"u + v = 1" |
548 apply (rule, rule, rule, rule, rule) |
434 fix x assume "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" |
549 unfolding mem_Collect_eq |
435 then obtain sx ux where x:"finite sx" "sx \<noteq> {}" "sx \<subseteq> p" "setsum ux sx = 1" "(\<Sum>v\<in>sx. ux v *\<^sub>R v) = x" by auto |
550 proof - |
|
551 fix u v :: real |
|
552 assume uv: "u + v = 1" |
|
553 fix x |
|
554 assume "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" |
|
555 then obtain sx ux where |
|
556 x: "finite sx" "sx \<noteq> {}" "sx \<subseteq> p" "setsum ux sx = 1" "(\<Sum>v\<in>sx. ux v *\<^sub>R v) = x" by auto |
436 fix y assume "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y" |
557 fix y assume "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y" |
437 then obtain sy uy where y:"finite sy" "sy \<noteq> {}" "sy \<subseteq> p" "setsum uy sy = 1" "(\<Sum>v\<in>sy. uy v *\<^sub>R v) = y" by auto |
558 then obtain sy uy where |
438 have xy:"finite (sx \<union> sy)" using x(1) y(1) by auto |
559 y: "finite sy" "sy \<noteq> {}" "sy \<subseteq> p" "setsum uy sy = 1" "(\<Sum>v\<in>sy. uy v *\<^sub>R v) = y" by auto |
439 have **:"(sx \<union> sy) \<inter> sx = sx" "(sx \<union> sy) \<inter> sy = sy" by auto |
560 have xy: "finite (sx \<union> sy)" using x(1) y(1) by auto |
440 show "\<exists>s ua. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum ua s = 1 \<and> (\<Sum>v\<in>s. ua v *\<^sub>R v) = u *\<^sub>R x + v *\<^sub>R y" |
561 have **: "(sx \<union> sy) \<inter> sx = sx" "(sx \<union> sy) \<inter> sy = sy" by auto |
441 apply(rule_tac x="sx \<union> sy" in exI) |
562 show "\<exists>s ua. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> |
442 apply(rule_tac x="\<lambda>a. (if a\<in>sx then u * ux a else 0) + (if a\<in>sy then v * uy a else 0)" in exI) |
563 setsum ua s = 1 \<and> (\<Sum>v\<in>s. ua v *\<^sub>R v) = u *\<^sub>R x + v *\<^sub>R y" |
443 unfolding scaleR_left_distrib setsum_addf if_smult scaleR_zero_left ** setsum_restrict_set[OF xy, THEN sym] |
564 apply (rule_tac x="sx \<union> sy" in exI) |
|
565 apply (rule_tac x="\<lambda>a. (if a\<in>sx then u * ux a else 0) + (if a\<in>sy then v * uy a else 0)" in exI) |
|
566 unfolding scaleR_left_distrib setsum_addf if_smult scaleR_zero_left ** setsum_restrict_set[OF xy, THEN sym] |
444 unfolding scaleR_scaleR[THEN sym] RealVector.scaleR_right.setsum [symmetric] and setsum_right_distrib[THEN sym] |
567 unfolding scaleR_scaleR[THEN sym] RealVector.scaleR_right.setsum [symmetric] and setsum_right_distrib[THEN sym] |
445 unfolding x y using x(1-3) y(1-3) uv by simp qed qed |
568 unfolding x y |
|
569 using x(1-3) y(1-3) uv apply simp |
|
570 done |
|
571 qed |
|
572 qed |
446 |
573 |
447 lemma affine_hull_finite: |
574 lemma affine_hull_finite: |
448 assumes "finite s" |
575 assumes "finite s" |
449 shows "affine hull s = {y. \<exists>u. setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" |
576 shows "affine hull s = {y. \<exists>u. setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" |
450 unfolding affine_hull_explicit and set_eq_iff and mem_Collect_eq apply (rule,rule) |
577 unfolding affine_hull_explicit and set_eq_iff and mem_Collect_eq apply (rule,rule) |
451 apply(erule exE)+ apply(erule conjE)+ defer apply(erule exE) apply(erule conjE) proof- |
578 apply(erule exE)+ |
452 fix x u assume "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x" |
579 apply(erule conjE)+ |
453 thus "\<exists>sa u. finite sa \<and> \<not> (\<forall>x. (x \<in> sa) = (x \<in> {})) \<and> sa \<subseteq> s \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = x" |
580 defer |
454 apply(rule_tac x=s in exI, rule_tac x=u in exI) using assms by auto |
581 apply (erule exE) |
|
582 apply (erule conjE) |
|
583 proof - |
|
584 fix x u |
|
585 assume "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x" |
|
586 then show "\<exists>sa u. finite sa \<and> |
|
587 \<not> (\<forall>x. (x \<in> sa) = (x \<in> {})) \<and> sa \<subseteq> s \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = x" |
|
588 apply (rule_tac x=s in exI, rule_tac x=u in exI) |
|
589 using assms apply auto |
|
590 done |
455 next |
591 next |
456 fix x t u assume "t \<subseteq> s" hence *:"s \<inter> t = t" by auto |
592 fix x t u |
|
593 assume "t \<subseteq> s" |
|
594 then have *: "s \<inter> t = t" by auto |
457 assume "finite t" "\<not> (\<forall>x. (x \<in> t) = (x \<in> {}))" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x" |
595 assume "finite t" "\<not> (\<forall>x. (x \<in> t) = (x \<in> {}))" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x" |
458 thus "\<exists>u. setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI) |
596 then show "\<exists>u. setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" |
459 unfolding if_smult scaleR_zero_left and setsum_restrict_set[OF assms, THEN sym] and * by auto qed |
597 apply (rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI) |
|
598 unfolding if_smult scaleR_zero_left and setsum_restrict_set[OF assms, THEN sym] and * |
|
599 apply auto |
|
600 done |
|
601 qed |
|
602 |
460 |
603 |
461 subsubsection {* Stepping theorems and hence small special cases *} |
604 subsubsection {* Stepping theorems and hence small special cases *} |
462 |
605 |
463 lemma affine_hull_empty[simp]: "affine hull {} = {}" |
606 lemma affine_hull_empty[simp]: "affine hull {} = {}" |
464 apply(rule hull_unique) by auto |
607 by (rule hull_unique) auto |
465 |
608 |
466 lemma affine_hull_finite_step: |
609 lemma affine_hull_finite_step: |
467 fixes y :: "'a::real_vector" |
610 fixes y :: "'a::real_vector" |
468 shows "(\<exists>u. setsum u {} = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) {} = y) \<longleftrightarrow> w = 0 \<and> y = 0" (is ?th1) |
611 shows |
469 "finite s \<Longrightarrow> (\<exists>u. setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y) \<longleftrightarrow> |
612 "(\<exists>u. setsum u {} = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) {} = y) \<longleftrightarrow> w = 0 \<and> y = 0" (is ?th1) |
470 (\<exists>v u. setsum u s = w - v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?as \<Longrightarrow> (?lhs = ?rhs)") |
613 "finite s \<Longrightarrow> |
471 proof- |
614 (\<exists>u. setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y) \<longleftrightarrow> |
|
615 (\<exists>v u. setsum u s = w - v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?as \<Longrightarrow> (?lhs = ?rhs)") |
|
616 proof - |
472 show ?th1 by simp |
617 show ?th1 by simp |
473 assume ?as |
618 assume ?as |
474 { assume ?lhs |
619 { assume ?lhs |
475 then obtain u where u:"setsum u (insert a s) = w \<and> (\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y" by auto |
620 then obtain u where u:"setsum u (insert a s) = w \<and> (\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y" by auto |
476 have ?rhs proof(cases "a\<in>s") |
621 have ?rhs |
477 case True hence *:"insert a s = s" by auto |
622 proof (cases "a \<in> s") |
|
623 case True |
|
624 then have *: "insert a s = s" by auto |
478 show ?thesis using u[unfolded *] apply(rule_tac x=0 in exI) by auto |
625 show ?thesis using u[unfolded *] apply(rule_tac x=0 in exI) by auto |
479 next |
626 next |
480 case False thus ?thesis apply(rule_tac x="u a" in exI) using u and `?as` by auto |
627 case False |
481 qed } moreover |
628 then show ?thesis |
|
629 apply (rule_tac x="u a" in exI) |
|
630 using u and `?as` apply auto |
|
631 done |
|
632 qed } |
|
633 moreover |
482 { assume ?rhs |
634 { assume ?rhs |
483 then obtain v u where vu:"setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto |
635 then obtain v u where vu:"setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto |
484 have *:"\<And>x M. (if x = a then v else M) *\<^sub>R x = (if x = a then v *\<^sub>R x else M *\<^sub>R x)" by auto |
636 have *: "\<And>x M. (if x = a then v else M) *\<^sub>R x = (if x = a then v *\<^sub>R x else M *\<^sub>R x)" by auto |
485 have ?lhs proof(cases "a\<in>s") |
637 have ?lhs |
486 case True thus ?thesis |
638 proof (cases "a \<in> s") |
487 apply(rule_tac x="\<lambda>x. (if x=a then v else 0) + u x" in exI) |
639 case True |
488 unfolding setsum_clauses(2)[OF `?as`] apply simp |
640 then show ?thesis |
|
641 apply (rule_tac x="\<lambda>x. (if x=a then v else 0) + u x" in exI) |
|
642 unfolding setsum_clauses(2)[OF `?as`] apply simp |
489 unfolding scaleR_left_distrib and setsum_addf |
643 unfolding scaleR_left_distrib and setsum_addf |
490 unfolding vu and * and scaleR_zero_left |
644 unfolding vu and * and scaleR_zero_left |
491 by (auto simp add: setsum_delta[OF `?as`]) |
645 apply (auto simp add: setsum_delta[OF `?as`]) |
|
646 done |
492 next |
647 next |
493 case False |
648 case False |
494 hence **:"\<And>x. x \<in> s \<Longrightarrow> u x = (if x = a then v else u x)" |
649 then have **: |
495 "\<And>x. x \<in> s \<Longrightarrow> u x *\<^sub>R x = (if x = a then v *\<^sub>R x else u x *\<^sub>R x)" by auto |
650 "\<And>x. x \<in> s \<Longrightarrow> u x = (if x = a then v else u x)" |
|
651 "\<And>x. x \<in> s \<Longrightarrow> u x *\<^sub>R x = (if x = a then v *\<^sub>R x else u x *\<^sub>R x)" by auto |
496 from False show ?thesis |
652 from False show ?thesis |
497 apply(rule_tac x="\<lambda>x. if x=a then v else u x" in exI) |
653 apply (rule_tac x="\<lambda>x. if x=a then v else u x" in exI) |
498 unfolding setsum_clauses(2)[OF `?as`] and * using vu |
654 unfolding setsum_clauses(2)[OF `?as`] and * using vu |
499 using setsum_cong2[of s "\<lambda>x. u x *\<^sub>R x" "\<lambda>x. if x = a then v *\<^sub>R x else u x *\<^sub>R x", OF **(2)] |
655 using setsum_cong2[of s "\<lambda>x. u x *\<^sub>R x" "\<lambda>x. if x = a then v *\<^sub>R x else u x *\<^sub>R x", OF **(2)] |
500 using setsum_cong2[of s u "\<lambda>x. if x = a then v else u x", OF **(1)] by auto |
656 using setsum_cong2[of s u "\<lambda>x. if x = a then v else u x", OF **(1)] |
501 qed } |
657 apply auto |
|
658 done |
|
659 qed |
|
660 } |
502 ultimately show "?lhs = ?rhs" by blast |
661 ultimately show "?lhs = ?rhs" by blast |
503 qed |
662 qed |
504 |
663 |
505 lemma affine_hull_2: |
664 lemma affine_hull_2: |
506 fixes a b :: "'a::real_vector" |
665 fixes a b :: "'a::real_vector" |
507 shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs") |
666 shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs") |
508 proof- |
667 proof - |
509 have *:"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" |
668 have *: |
510 "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto |
669 "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" |
|
670 "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto |
511 have "?lhs = {y. \<exists>u. setsum u {a, b} = 1 \<and> (\<Sum>v\<in>{a, b}. u v *\<^sub>R v) = y}" |
671 have "?lhs = {y. \<exists>u. setsum u {a, b} = 1 \<and> (\<Sum>v\<in>{a, b}. u v *\<^sub>R v) = y}" |
512 using affine_hull_finite[of "{a,b}"] by auto |
672 using affine_hull_finite[of "{a,b}"] by auto |
513 also have "\<dots> = {y. \<exists>v u. u b = 1 - v \<and> u b *\<^sub>R b = y - v *\<^sub>R a}" |
673 also have "\<dots> = {y. \<exists>v u. u b = 1 - v \<and> u b *\<^sub>R b = y - v *\<^sub>R a}" |
514 by(simp add: affine_hull_finite_step(2)[of "{b}" a]) |
674 by (simp add: affine_hull_finite_step(2)[of "{b}" a]) |
515 also have "\<dots> = ?rhs" unfolding * by auto |
675 also have "\<dots> = ?rhs" unfolding * by auto |
516 finally show ?thesis by auto |
676 finally show ?thesis by auto |
517 qed |
677 qed |
518 |
678 |
519 lemma affine_hull_3: |
679 lemma affine_hull_3: |
520 fixes a b c :: "'a::real_vector" |
680 fixes a b c :: "'a::real_vector" |
521 shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" (is "?lhs = ?rhs") |
681 shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" (is "?lhs = ?rhs") |
522 proof- |
682 proof - |
523 have *:"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" |
683 have *: |
524 "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto |
684 "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" |
525 show ?thesis apply(simp add: affine_hull_finite affine_hull_finite_step) |
685 "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto |
526 unfolding * apply auto |
686 show ?thesis |
527 apply(rule_tac x=v in exI) apply(rule_tac x=va in exI) apply auto |
687 apply (simp add: affine_hull_finite affine_hull_finite_step) |
528 apply(rule_tac x=u in exI) by force |
688 unfolding * |
|
689 apply auto |
|
690 apply (rule_tac x=v in exI) apply(rule_tac x=va in exI) apply auto |
|
691 apply (rule_tac x=u in exI) apply force |
|
692 done |
529 qed |
693 qed |
530 |
694 |
531 lemma mem_affine: |
695 lemma mem_affine: |
532 assumes "affine S" "x : S" "y : S" "u+v=1" |
696 assumes "affine S" "x : S" "y : S" "u+v=1" |
533 shows "(u *\<^sub>R x + v *\<^sub>R y) : S" |
697 shows "(u *\<^sub>R x + v *\<^sub>R y) : S" |
534 using assms affine_def[of S] by auto |
698 using assms affine_def[of S] by auto |
535 |
699 |
536 lemma mem_affine_3: |
700 lemma mem_affine_3: |
537 assumes "affine S" "x : S" "y : S" "z : S" "u+v+w=1" |
701 assumes "affine S" "x : S" "y : S" "z : S" "u+v+w=1" |
538 shows "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : S" |
702 shows "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : S" |
539 proof- |
703 proof - |
540 have "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : affine hull {x, y, z}" |
704 have "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : affine hull {x, y, z}" |
541 using affine_hull_3[of x y z] assms by auto |
705 using affine_hull_3[of x y z] assms by auto |
542 moreover have " affine hull {x, y, z} <= affine hull S" |
706 moreover |
543 using hull_mono[of "{x, y, z}" "S"] assms by auto |
707 have "affine hull {x, y, z} <= affine hull S" |
544 moreover have "affine hull S = S" |
708 using hull_mono[of "{x, y, z}" "S"] assms by auto |
545 using assms affine_hull_eq[of S] by auto |
709 moreover |
546 ultimately show ?thesis by auto |
710 have "affine hull S = S" using assms affine_hull_eq[of S] by auto |
|
711 ultimately show ?thesis by auto |
547 qed |
712 qed |
548 |
713 |
549 lemma mem_affine_3_minus: |
714 lemma mem_affine_3_minus: |
550 assumes "affine S" "x : S" "y : S" "z : S" |
715 assumes "affine S" "x : S" "y : S" "z : S" |
551 shows "x + v *\<^sub>R (y-z) : S" |
716 shows "x + v *\<^sub>R (y-z) : S" |
552 using mem_affine_3[of S x y z 1 v "-v"] assms by (simp add: algebra_simps) |
717 using mem_affine_3[of S x y z 1 v "-v"] assms by (simp add: algebra_simps) |
553 |
718 |
554 |
719 |
555 subsubsection {* Some relations between affine hull and subspaces *} |
720 subsubsection {* Some relations between affine hull and subspaces *} |
556 |
721 |
557 lemma affine_hull_insert_subset_span: |
722 lemma affine_hull_insert_subset_span: |
558 shows "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}" |
723 "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}" |
559 unfolding subset_eq Ball_def unfolding affine_hull_explicit span_explicit mem_Collect_eq |
724 unfolding subset_eq Ball_def |
560 apply(rule,rule) apply(erule exE)+ apply(erule conjE)+ proof- |
725 unfolding affine_hull_explicit span_explicit mem_Collect_eq |
561 fix x t u assume as:"finite t" "t \<noteq> {}" "t \<subseteq> insert a s" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x" |
726 apply (rule, rule) apply (erule exE)+ apply (erule conjE)+ |
|
727 proof - |
|
728 fix x t u |
|
729 assume as: "finite t" "t \<noteq> {}" "t \<subseteq> insert a s" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x" |
562 have "(\<lambda>x. x - a) ` (t - {a}) \<subseteq> {x - a |x. x \<in> s}" using as(3) by auto |
730 have "(\<lambda>x. x - a) ` (t - {a}) \<subseteq> {x - a |x. x \<in> s}" using as(3) by auto |
563 thus "\<exists>v. x = a + v \<and> (\<exists>S u. finite S \<and> S \<subseteq> {x - a |x. x \<in> s} \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = v)" |
731 then show "\<exists>v. x = a + v \<and> (\<exists>S u. finite S \<and> S \<subseteq> {x - a |x. x \<in> s} \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = v)" |
564 apply(rule_tac x="x - a" in exI) |
732 apply (rule_tac x="x - a" in exI) |
565 apply (rule conjI, simp) |
733 apply (rule conjI, simp) |
566 apply(rule_tac x="(\<lambda>x. x - a) ` (t - {a})" in exI) |
734 apply (rule_tac x="(\<lambda>x. x - a) ` (t - {a})" in exI) |
567 apply(rule_tac x="\<lambda>x. u (x + a)" in exI) |
735 apply (rule_tac x="\<lambda>x. u (x + a)" in exI) |
568 apply (rule conjI) using as(1) apply simp |
736 apply (rule conjI) using as(1) apply simp |
569 apply (erule conjI) |
737 apply (erule conjI) |
570 using as(1) |
738 using as(1) |
571 apply (simp add: setsum_reindex[unfolded inj_on_def] scaleR_right_diff_distrib setsum_subtractf scaleR_left.setsum[THEN sym] setsum_diff1 scaleR_left_diff_distrib) |
739 apply (simp add: setsum_reindex[unfolded inj_on_def] scaleR_right_diff_distrib |
572 unfolding as by simp qed |
740 setsum_subtractf scaleR_left.setsum[THEN sym] setsum_diff1 scaleR_left_diff_distrib) |
|
741 unfolding as |
|
742 apply simp |
|
743 done |
|
744 qed |
573 |
745 |
574 lemma affine_hull_insert_span: |
746 lemma affine_hull_insert_span: |
575 assumes "a \<notin> s" |
747 assumes "a \<notin> s" |
576 shows "affine hull (insert a s) = |
748 shows "affine hull (insert a s) = {a + v | v . v \<in> span {x - a | x. x \<in> s}}" |
577 {a + v | v . v \<in> span {x - a | x. x \<in> s}}" |
749 apply (rule, rule affine_hull_insert_subset_span) |
578 apply(rule, rule affine_hull_insert_subset_span) unfolding subset_eq Ball_def |
750 unfolding subset_eq Ball_def |
579 unfolding affine_hull_explicit and mem_Collect_eq proof(rule,rule,erule exE,erule conjE) |
751 unfolding affine_hull_explicit and mem_Collect_eq |
580 fix y v assume "y = a + v" "v \<in> span {x - a |x. x \<in> s}" |
752 proof (rule, rule, erule exE, erule conjE) |
581 then obtain t u where obt:"finite t" "t \<subseteq> {x - a |x. x \<in> s}" "a + (\<Sum>v\<in>t. u v *\<^sub>R v) = y" unfolding span_explicit by auto |
753 fix y v |
|
754 assume "y = a + v" "v \<in> span {x - a |x. x \<in> s}" |
|
755 then obtain t u where obt:"finite t" "t \<subseteq> {x - a |x. x \<in> s}" "a + (\<Sum>v\<in>t. u v *\<^sub>R v) = y" |
|
756 unfolding span_explicit by auto |
582 def f \<equiv> "(\<lambda>x. x + a) ` t" |
757 def f \<equiv> "(\<lambda>x. x + a) ` t" |
583 have f:"finite f" "f \<subseteq> s" "(\<Sum>v\<in>f. u (v - a) *\<^sub>R (v - a)) = y - a" unfolding f_def using obt |
758 have f:"finite f" "f \<subseteq> s" "(\<Sum>v\<in>f. u (v - a) *\<^sub>R (v - a)) = y - a" |
584 by(auto simp add: setsum_reindex[unfolded inj_on_def]) |
759 unfolding f_def using obt by (auto simp add: setsum_reindex[unfolded inj_on_def]) |
585 have *:"f \<inter> {a} = {}" "f \<inter> - {a} = f" using f(2) assms by auto |
760 have *: "f \<inter> {a} = {}" "f \<inter> - {a} = f" using f(2) assms by auto |
586 show "\<exists>sa u. finite sa \<and> sa \<noteq> {} \<and> sa \<subseteq> insert a s \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = y" |
761 show "\<exists>sa u. finite sa \<and> sa \<noteq> {} \<and> sa \<subseteq> insert a s \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = y" |
587 apply(rule_tac x="insert a f" in exI) |
762 apply (rule_tac x = "insert a f" in exI) |
588 apply(rule_tac x="\<lambda>x. if x=a then 1 - setsum (\<lambda>x. u (x - a)) f else u (x - a)" in exI) |
763 apply (rule_tac x = "\<lambda>x. if x=a then 1 - setsum (\<lambda>x. u (x - a)) f else u (x - a)" in exI) |
589 using assms and f unfolding setsum_clauses(2)[OF f(1)] and if_smult |
764 using assms and f unfolding setsum_clauses(2)[OF f(1)] and if_smult |
590 unfolding setsum_cases[OF f(1), of "\<lambda>x. x = a"] |
765 unfolding setsum_cases[OF f(1), of "\<lambda>x. x = a"] |
591 by (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps *) qed |
766 apply (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps *) |
|
767 done |
|
768 qed |
592 |
769 |
593 lemma affine_hull_span: |
770 lemma affine_hull_span: |
594 assumes "a \<in> s" |
771 assumes "a \<in> s" |
595 shows "affine hull s = {a + v | v. v \<in> span {x - a | x. x \<in> s - {a}}}" |
772 shows "affine hull s = {a + v | v. v \<in> span {x - a | x. x \<in> s - {a}}}" |
596 using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto |
773 using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto |
597 |
774 |
|
775 |
598 subsubsection {* Parallel affine sets *} |
776 subsubsection {* Parallel affine sets *} |
599 |
777 |
600 definition affine_parallel :: "'a::real_vector set => 'a::real_vector set => bool" |
778 definition affine_parallel :: "'a::real_vector set => 'a::real_vector set => bool" |
601 where "affine_parallel S T = (? a. T = ((%x. a + x) ` S))" |
779 where "affine_parallel S T = (? a. T = ((%x. a + x) ` S))" |
602 |
780 |
603 lemma affine_parallel_expl_aux: |
781 lemma affine_parallel_expl_aux: |
604 fixes S T :: "'a::real_vector set" |
782 fixes S T :: "'a::real_vector set" |
605 assumes "!x. (x : S <-> (a+x) : T)" |
783 assumes "!x. (x : S <-> (a+x) : T)" |
606 shows "T = ((%x. a + x) ` S)" |
784 shows "T = ((%x. a + x) ` S)" |
607 proof- |
785 proof - |
608 { fix x assume "x : T" hence "(-a)+x : S" using assms by auto |
786 { fix x |
609 hence " x : ((%x. a + x) ` S)" using imageI[of "-a+x" S "(%x. a+x)"] by auto} |
787 assume "x : T" |
610 moreover have "T >= ((%x. a + x) ` S)" using assms by auto |
788 then have "(-a)+x : S" using assms by auto |
611 ultimately show ?thesis by auto |
789 then have "x : ((%x. a + x) ` S)" |
612 qed |
790 using imageI[of "-a+x" S "(%x. a+x)"] by auto } |
613 |
791 moreover have "T >= ((%x. a + x) ` S)" using assms by auto |
614 lemma affine_parallel_expl: |
792 ultimately show ?thesis by auto |
615 "affine_parallel S T = (? a. !x. (x : S <-> (a+x) : T))" |
793 qed |
616 unfolding affine_parallel_def using affine_parallel_expl_aux[of S _ T] by auto |
794 |
617 |
795 lemma affine_parallel_expl: "affine_parallel S T = (? a. !x. (x : S <-> (a+x) : T))" |
618 lemma affine_parallel_reflex: "affine_parallel S S" unfolding affine_parallel_def apply (rule exI[of _ "0"]) by auto |
796 unfolding affine_parallel_def |
|
797 using affine_parallel_expl_aux[of S _ T] by auto |
|
798 |
|
799 lemma affine_parallel_reflex: "affine_parallel S S" |
|
800 unfolding affine_parallel_def apply (rule exI[of _ "0"]) by auto |
619 |
801 |
620 lemma affine_parallel_commut: |
802 lemma affine_parallel_commut: |
621 assumes "affine_parallel A B" shows "affine_parallel B A" |
803 assumes "affine_parallel A B" |
622 proof- |
804 shows "affine_parallel B A" |
623 from assms obtain a where "B=((%x. a + x) ` A)" unfolding affine_parallel_def by auto |
805 proof - |
624 from this show ?thesis using translation_galois[of B a A] unfolding affine_parallel_def by auto |
806 from assms obtain a where "B=((%x. a + x) ` A)" |
|
807 unfolding affine_parallel_def by auto |
|
808 then show ?thesis |
|
809 using translation_galois[of B a A] unfolding affine_parallel_def by auto |
625 qed |
810 qed |
626 |
811 |
627 lemma affine_parallel_assoc: |
812 lemma affine_parallel_assoc: |
628 assumes "affine_parallel A B" "affine_parallel B C" |
813 assumes "affine_parallel A B" "affine_parallel B C" |
629 shows "affine_parallel A C" |
814 shows "affine_parallel A C" |
630 proof- |
815 proof - |
631 from assms obtain ab where "B=((%x. ab + x) ` A)" unfolding affine_parallel_def by auto |
816 from assms obtain ab where "B=((%x. ab + x) ` A)" |
632 moreover |
817 unfolding affine_parallel_def by auto |
633 from assms obtain bc where "C=((%x. bc + x) ` B)" unfolding affine_parallel_def by auto |
818 moreover |
634 ultimately show ?thesis using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto |
819 from assms obtain bc where "C=((%x. bc + x) ` B)" |
|
820 unfolding affine_parallel_def by auto |
|
821 ultimately show ?thesis |
|
822 using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto |
635 qed |
823 qed |
636 |
824 |
637 lemma affine_translation_aux: |
825 lemma affine_translation_aux: |
638 fixes a :: "'a::real_vector" |
826 fixes a :: "'a::real_vector" |
639 assumes "affine ((%x. a + x) ` S)" shows "affine S" |
827 assumes "affine ((%x. a + x) ` S)" shows "affine S" |
640 proof- |
828 proof- |
641 { fix x y u v |
829 { fix x y u v |
642 assume xy: "x : S" "y : S" "(u :: real)+v=1" |
830 assume xy: "x : S" "y : S" "(u :: real)+v=1" |
643 hence "(a+x):((%x. a + x) ` S)" "(a+y):((%x. a + x) ` S)" by auto |
831 then have "(a+x):((%x. a + x) ` S)" "(a+y):((%x. a + x) ` S)" by auto |
644 hence h1: "u *\<^sub>R (a+x) + v *\<^sub>R (a+y) : ((%x. a + x) ` S)" using xy assms unfolding affine_def by auto |
832 then have h1: "u *\<^sub>R (a+x) + v *\<^sub>R (a+y) : ((%x. a + x) ` S)" |
645 have "u *\<^sub>R (a+x) + v *\<^sub>R (a+y) = (u+v) *\<^sub>R a + (u *\<^sub>R x + v *\<^sub>R y)" by (simp add:algebra_simps) |
833 using xy assms unfolding affine_def by auto |
646 also have "...= a + (u *\<^sub>R x + v *\<^sub>R y)" using `u+v=1` by auto |
834 have "u *\<^sub>R (a+x) + v *\<^sub>R (a+y) = (u+v) *\<^sub>R a + (u *\<^sub>R x + v *\<^sub>R y)" |
647 ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) : ((%x. a + x) ` S)" using h1 by auto |
835 by (simp add: algebra_simps) |
648 hence "u *\<^sub>R x + v *\<^sub>R y : S" by auto |
836 also have "...= a + (u *\<^sub>R x + v *\<^sub>R y)" using `u+v=1` by auto |
649 } from this show ?thesis unfolding affine_def by auto |
837 ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) : ((%x. a + x) ` S)" using h1 by auto |
|
838 then have "u *\<^sub>R x + v *\<^sub>R y : S" by auto |
|
839 } |
|
840 then show ?thesis unfolding affine_def by auto |
650 qed |
841 qed |
651 |
842 |
652 lemma affine_translation: |
843 lemma affine_translation: |
653 fixes a :: "'a::real_vector" |
844 fixes a :: "'a::real_vector" |
654 shows "affine S <-> affine ((%x. a + x) ` S)" |
845 shows "affine S <-> affine ((%x. a + x) ` S)" |
655 proof- |
846 proof - |
656 have "affine S ==> affine ((%x. a + x) ` S)" using affine_translation_aux[of "-a" "((%x. a + x) ` S)"] using translation_assoc[of "-a" a S] by auto |
847 have "affine S ==> affine ((%x. a + x) ` S)" |
657 from this show ?thesis using affine_translation_aux by auto |
848 using affine_translation_aux[of "-a" "((%x. a + x) ` S)"] |
|
849 using translation_assoc[of "-a" a S] by auto |
|
850 then show ?thesis using affine_translation_aux by auto |
658 qed |
851 qed |
659 |
852 |
660 lemma parallel_is_affine: |
853 lemma parallel_is_affine: |
661 fixes S T :: "'a::real_vector set" |
854 fixes S T :: "'a::real_vector set" |
662 assumes "affine S" "affine_parallel S T" |
855 assumes "affine S" "affine_parallel S T" |
663 shows "affine T" |
856 shows "affine T" |
664 proof- |
857 proof - |
665 from assms obtain a where "T=((%x. a + x) ` S)" unfolding affine_parallel_def by auto |
858 from assms obtain a where "T=((%x. a + x) ` S)" |
666 from this show ?thesis using affine_translation assms by auto |
859 unfolding affine_parallel_def by auto |
|
860 then show ?thesis using affine_translation assms by auto |
667 qed |
861 qed |
668 |
862 |
669 lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s" |
863 lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s" |
670 unfolding subspace_def affine_def by auto |
864 unfolding subspace_def affine_def by auto |
671 |
865 |
|
866 |
672 subsubsection {* Subspace parallel to an affine set *} |
867 subsubsection {* Subspace parallel to an affine set *} |
673 |
868 |
674 lemma subspace_affine: |
869 lemma subspace_affine: "subspace S <-> (affine S & 0 : S)" |
675 shows "subspace S <-> (affine S & 0 : S)" |
870 proof - |
676 proof- |
871 have h0: "subspace S ==> (affine S & 0 : S)" |
677 have h0: "subspace S ==> (affine S & 0 : S)" using subspace_imp_affine[of S] subspace_0 by auto |
872 using subspace_imp_affine[of S] subspace_0 by auto |
678 { assume assm: "affine S & 0 : S" |
873 { assume assm: "affine S & 0 : S" |
679 { fix c :: real |
874 { fix c :: real |
680 fix x assume x_def: "x : S" |
875 fix x assume x_def: "x : S" |
681 have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto |
876 have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto |
682 moreover have "(1-c) *\<^sub>R 0 + c *\<^sub>R x : S" using affine_alt[of S] assm x_def by auto |
877 moreover |
683 ultimately have "c *\<^sub>R x : S" by auto |
878 have "(1-c) *\<^sub>R 0 + c *\<^sub>R x : S" using affine_alt[of S] assm x_def by auto |
684 } hence h1: "!c. !x : S. c *\<^sub>R x : S" by auto |
879 ultimately have "c *\<^sub>R x : S" by auto |
685 { fix x y assume xy_def: "x : S" "y : S" |
880 } |
686 def u == "(1 :: real)/2" |
881 then have h1: "!c. !x : S. c *\<^sub>R x : S" by auto |
687 have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)" by auto |
882 |
688 moreover have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y" by (simp add: algebra_simps) |
883 { fix x y assume xy_def: "x : S" "y : S" |
689 moreover have "(1-u) *\<^sub>R x + u *\<^sub>R y : S" using affine_alt[of S] assm xy_def by auto |
884 def u == "(1 :: real)/2" |
690 ultimately have "(1/2) *\<^sub>R (x+y) : S" using u_def by auto |
885 have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)" by auto |
691 moreover have "(x+y) = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))" by auto |
886 moreover |
692 ultimately have "(x+y) : S" using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto |
887 have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y" by (simp add: algebra_simps) |
693 } hence "!x : S. !y : S. (x+y) : S" by auto |
888 moreover |
694 hence "subspace S" using h1 assm unfolding subspace_def by auto |
889 have "(1-u) *\<^sub>R x + u *\<^sub>R y : S" using affine_alt[of S] assm xy_def by auto |
695 } from this show ?thesis using h0 by metis |
890 ultimately |
|
891 have "(1/2) *\<^sub>R (x+y) : S" using u_def by auto |
|
892 moreover |
|
893 have "(x+y) = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))" by auto |
|
894 ultimately |
|
895 have "(x+y) : S" using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto |
|
896 } |
|
897 then have "!x : S. !y : S. (x+y) : S" by auto |
|
898 then have "subspace S" using h1 assm unfolding subspace_def by auto |
|
899 } |
|
900 then show ?thesis using h0 by metis |
696 qed |
901 qed |
697 |
902 |
698 lemma affine_diffs_subspace: |
903 lemma affine_diffs_subspace: |
699 assumes "affine S" "a : S" |
904 assumes "affine S" "a : S" |
700 shows "subspace ((%x. (-a)+x) ` S)" |
905 shows "subspace ((%x. (-a)+x) ` S)" |
701 proof- |
906 proof - |
702 have "affine ((%x. (-a)+x) ` S)" using affine_translation assms by auto |
907 have "affine ((%x. (-a)+x) ` S)" |
703 moreover have "0 : ((%x. (-a)+x) ` S)" using assms exI[of "(%x. x:S & -a+x=0)" a] by auto |
908 using affine_translation assms by auto |
704 ultimately show ?thesis using subspace_affine by auto |
909 moreover have "0 : ((%x. (-a)+x) ` S)" |
|
910 using assms exI[of "(%x. x:S & -a+x=0)" a] by auto |
|
911 ultimately show ?thesis using subspace_affine by auto |
705 qed |
912 qed |
706 |
913 |
707 lemma parallel_subspace_explicit: |
914 lemma parallel_subspace_explicit: |
708 assumes "affine S" "a : S" |
915 assumes "affine S" "a : S" |
709 assumes "L == {y. ? x : S. (-a)+x=y}" |
916 assumes "L == {y. ? x : S. (-a)+x=y}" |
710 shows "subspace L & affine_parallel S L" |
917 shows "subspace L & affine_parallel S L" |
711 proof- |
918 proof - |
712 have par: "affine_parallel S L" unfolding affine_parallel_def using assms by auto |
919 have par: "affine_parallel S L" |
713 hence "affine L" using assms parallel_is_affine by auto |
920 unfolding affine_parallel_def using assms by auto |
714 moreover have "0 : L" using assms apply auto using exI[of "(%x. x:S & -a+x=0)" a] by auto |
921 then have "affine L" using assms parallel_is_affine by auto |
715 ultimately show ?thesis using subspace_affine par by auto |
922 moreover have "0 : L" |
|
923 using assms apply auto |
|
924 using exI[of "(%x. x:S & -a+x=0)" a] apply auto |
|
925 done |
|
926 ultimately show ?thesis using subspace_affine par by auto |
716 qed |
927 qed |
717 |
928 |
718 lemma parallel_subspace_aux: |
929 lemma parallel_subspace_aux: |
719 assumes "subspace A" "subspace B" "affine_parallel A B" |
930 assumes "subspace A" "subspace B" "affine_parallel A B" |
720 shows "A>=B" |
931 shows "A>=B" |
721 proof- |
932 proof - |
722 from assms obtain a where a_def: "!x. (x : A <-> (a+x) : B)" using affine_parallel_expl[of A B] by auto |
933 from assms obtain a where a_def: "!x. (x : A <-> (a+x) : B)" |
723 hence "-a : A" using assms subspace_0[of B] by auto |
934 using affine_parallel_expl[of A B] by auto |
724 hence "a : A" using assms subspace_neg[of A "-a"] by auto |
935 then have "-a : A" using assms subspace_0[of B] by auto |
725 from this show ?thesis using assms a_def unfolding subspace_def by auto |
936 then have "a : A" using assms subspace_neg[of A "-a"] by auto |
|
937 then show ?thesis using assms a_def unfolding subspace_def by auto |
726 qed |
938 qed |
727 |
939 |
728 lemma parallel_subspace: |
940 lemma parallel_subspace: |
729 assumes "subspace A" "subspace B" "affine_parallel A B" |
941 assumes "subspace A" "subspace B" "affine_parallel A B" |
730 shows "A=B" |
942 shows "A = B" |
731 proof- |
943 proof |
732 have "A>=B" using assms parallel_subspace_aux by auto |
944 show "A >= B" |
733 moreover have "A<=B" using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto |
945 using assms parallel_subspace_aux by auto |
734 ultimately show ?thesis by auto |
946 show "A <= B" |
|
947 using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto |
735 qed |
948 qed |
736 |
949 |
737 lemma affine_parallel_subspace: |
950 lemma affine_parallel_subspace: |
738 assumes "affine S" "S ~= {}" |
951 assumes "affine S" "S ~= {}" |
739 shows "?!L. subspace L & affine_parallel S L" |
952 shows "?!L. subspace L & affine_parallel S L" |
740 proof- |
953 proof - |
741 have ex: "? L. subspace L & affine_parallel S L" using assms parallel_subspace_explicit by auto |
954 have ex: "? L. subspace L & affine_parallel S L" |
742 { fix L1 L2 assume ass: "subspace L1 & affine_parallel S L1" "subspace L2 & affine_parallel S L2" |
955 using assms parallel_subspace_explicit by auto |
743 hence "affine_parallel L1 L2" using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto |
956 { fix L1 L2 |
744 hence "L1=L2" using ass parallel_subspace by auto |
957 assume ass: "subspace L1 & affine_parallel S L1" "subspace L2 & affine_parallel S L2" |
745 } from this show ?thesis using ex by auto |
958 then have "affine_parallel L1 L2" |
746 qed |
959 using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto |
|
960 then have "L1 = L2" |
|
961 using ass parallel_subspace by auto |
|
962 } |
|
963 then show ?thesis using ex by auto |
|
964 qed |
|
965 |
747 |
966 |
748 subsection {* Cones *} |
967 subsection {* Cones *} |
749 |
968 |
750 definition |
969 definition cone :: "'a::real_vector set \<Rightarrow> bool" |
751 cone :: "'a::real_vector set \<Rightarrow> bool" where |
970 where "cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. (c *\<^sub>R x) \<in> s)" |
752 "cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. (c *\<^sub>R x) \<in> s)" |
|
753 |
971 |
754 lemma cone_empty[intro, simp]: "cone {}" |
972 lemma cone_empty[intro, simp]: "cone {}" |
755 unfolding cone_def by auto |
973 unfolding cone_def by auto |
756 |
974 |
757 lemma cone_univ[intro, simp]: "cone UNIV" |
975 lemma cone_univ[intro, simp]: "cone UNIV" |
758 unfolding cone_def by auto |
976 unfolding cone_def by auto |
759 |
977 |
760 lemma cone_Inter[intro]: "(\<forall>s\<in>f. cone s) \<Longrightarrow> cone(\<Inter> f)" |
978 lemma cone_Inter[intro]: "(\<forall>s\<in>f. cone s) \<Longrightarrow> cone(\<Inter> f)" |
761 unfolding cone_def by auto |
979 unfolding cone_def by auto |
762 |
980 |
|
981 |
763 subsubsection {* Conic hull *} |
982 subsubsection {* Conic hull *} |
764 |
983 |
765 lemma cone_cone_hull: "cone (cone hull s)" |
984 lemma cone_cone_hull: "cone (cone hull s)" |
766 unfolding hull_def by auto |
985 unfolding hull_def by auto |
767 |
986 |
768 lemma cone_hull_eq: "(cone hull s = s) \<longleftrightarrow> cone s" |
987 lemma cone_hull_eq: "(cone hull s = s) \<longleftrightarrow> cone s" |
769 apply(rule hull_eq) |
988 apply (rule hull_eq) |
770 using cone_Inter unfolding subset_eq by auto |
989 using cone_Inter unfolding subset_eq apply auto |
|
990 done |
771 |
991 |
772 lemma mem_cone: |
992 lemma mem_cone: |
773 assumes "cone S" "x : S" "c>=0" |
993 assumes "cone S" "x : S" "c>=0" |
774 shows "c *\<^sub>R x : S" |
994 shows "c *\<^sub>R x : S" |
775 using assms cone_def[of S] by auto |
995 using assms cone_def[of S] by auto |
776 |
996 |
777 lemma cone_contains_0: |
997 lemma cone_contains_0: |
778 assumes "cone S" |
998 assumes "cone S" |
779 shows "(S ~= {}) <-> (0 : S)" |
999 shows "(S ~= {}) <-> (0 : S)" |
780 proof- |
1000 proof - |
781 { assume "S ~= {}" from this obtain a where "a:S" by auto |
1001 { assume "S ~= {}" then obtain a where "a:S" by auto |
782 hence "0 : S" using assms mem_cone[of S a 0] by auto |
1002 then have "0 : S" using assms mem_cone[of S a 0] by auto |
783 } from this show ?thesis by auto |
1003 } |
|
1004 then show ?thesis by auto |
784 qed |
1005 qed |
785 |
1006 |
786 lemma cone_0: "cone {0}" |
1007 lemma cone_0: "cone {0}" |
787 unfolding cone_def by auto |
1008 unfolding cone_def by auto |
788 |
1009 |
789 lemma cone_Union[intro]: "(!s:f. cone s) --> (cone (Union f))" |
1010 lemma cone_Union[intro]: "(!s:f. cone s) --> (cone (Union f))" |
790 unfolding cone_def by blast |
1011 unfolding cone_def by blast |
791 |
1012 |
792 lemma cone_iff: |
1013 lemma cone_iff: |
793 assumes "S ~= {}" |
1014 assumes "S ~= {}" |
794 shows "cone S <-> 0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)" |
1015 shows "cone S <-> 0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)" |
795 proof- |
1016 proof - |
796 { assume "cone S" |
1017 { assume "cone S" |
797 { fix c assume "(c :: real)>0" |
1018 { fix c |
798 { fix x assume "x : S" hence "x : (op *\<^sub>R c) ` S" unfolding image_def |
1019 assume "(c :: real) > 0" |
799 using `cone S` `c>0` mem_cone[of S x "1/c"] |
1020 { fix x |
800 exI[of "(%t. t:S & x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"] by auto |
1021 assume "x : S" |
|
1022 then have "x : (op *\<^sub>R c) ` S" |
|
1023 unfolding image_def |
|
1024 using `cone S` `c>0` mem_cone[of S x "1/c"] |
|
1025 exI[of "(%t. t:S & x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"] apply auto |
|
1026 done |
|
1027 } |
|
1028 moreover |
|
1029 { fix x assume "x : (op *\<^sub>R c) ` S" |
|
1030 (*from this obtain t where "t:S & x = c *\<^sub>R t" by auto*) |
|
1031 then have "x:S" |
|
1032 using `cone S` `c>0` unfolding cone_def image_def `c>0` by auto |
|
1033 } |
|
1034 ultimately have "((op *\<^sub>R c) ` S) = S" by auto |
801 } |
1035 } |
802 moreover |
1036 then have "0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)" |
803 { fix x assume "x : (op *\<^sub>R c) ` S" |
1037 using `cone S` cone_contains_0[of S] assms by auto |
804 (*from this obtain t where "t:S & x = c *\<^sub>R t" by auto*) |
1038 } |
805 hence "x:S" using `cone S` `c>0` unfolding cone_def image_def `c>0` by auto |
1039 moreover |
|
1040 { assume a: "0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)" |
|
1041 { fix x assume "x:S" |
|
1042 fix c1 |
|
1043 assume "(c1 :: real) >= 0" |
|
1044 then have "(c1=0) | (c1>0)" by auto |
|
1045 then have "c1 *\<^sub>R x : S" using a `x:S` by auto |
806 } |
1046 } |
807 ultimately have "((op *\<^sub>R c) ` S) = S" by auto |
1047 then have "cone S" unfolding cone_def by auto |
808 } hence "0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)" using `cone S` cone_contains_0[of S] assms by auto |
|
809 } |
|
810 moreover |
|
811 { assume a: "0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)" |
|
812 { fix x assume "x:S" |
|
813 fix c1 assume "(c1 :: real)>=0" |
|
814 hence "(c1=0) | (c1>0)" by auto |
|
815 hence "c1 *\<^sub>R x : S" using a `x:S` by auto |
|
816 } |
1048 } |
817 hence "cone S" unfolding cone_def by auto |
1049 ultimately show ?thesis by blast |
818 } ultimately show ?thesis by blast |
1050 qed |
819 qed |
1051 |
820 |
1052 lemma cone_hull_empty: "cone hull {} = {}" |
821 lemma cone_hull_empty: |
1053 by (metis cone_empty cone_hull_eq) |
822 "cone hull {} = {}" |
1054 |
823 by (metis cone_empty cone_hull_eq) |
1055 lemma cone_hull_empty_iff: "(S = {}) <-> (cone hull S = {})" |
824 |
1056 by (metis bot_least cone_hull_empty hull_subset xtrans(5)) |
825 lemma cone_hull_empty_iff: |
1057 |
826 shows "(S = {}) <-> (cone hull S = {})" |
1058 lemma cone_hull_contains_0: "(S ~= {}) <-> (0 : cone hull S)" |
827 by (metis bot_least cone_hull_empty hull_subset xtrans(5)) |
1059 using cone_cone_hull[of S] cone_contains_0[of "cone hull S"] cone_hull_empty_iff[of S] |
828 |
1060 by auto |
829 lemma cone_hull_contains_0: |
|
830 shows "(S ~= {}) <-> (0 : cone hull S)" |
|
831 using cone_cone_hull[of S] cone_contains_0[of "cone hull S"] cone_hull_empty_iff[of S] by auto |
|
832 |
1061 |
833 lemma mem_cone_hull: |
1062 lemma mem_cone_hull: |
834 assumes "x : S" "c>=0" |
1063 assumes "x : S" "c>=0" |
835 shows "c *\<^sub>R x : cone hull S" |
1064 shows "c *\<^sub>R x : cone hull S" |
836 by (metis assms cone_cone_hull hull_inc mem_cone) |
1065 by (metis assms cone_cone_hull hull_inc mem_cone) |
837 |
1066 |
838 lemma cone_hull_expl: |
1067 lemma cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c>=0 & x : S}" (is "?lhs = ?rhs") |
839 shows "cone hull S = {c *\<^sub>R x | c x. c>=0 & x : S}" (is "?lhs = ?rhs") |
1068 proof - |
840 proof- |
1069 { fix x |
841 { fix x assume "x : ?rhs" |
1070 assume "x : ?rhs" |
842 from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto |
1071 then obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" |
843 fix c assume c_def: "(c :: real)>=0" |
1072 by auto |
844 hence "c *\<^sub>R x = (c*cx) *\<^sub>R xx" using x_def by (simp add: algebra_simps) |
1073 fix c |
845 moreover have "(c*cx) >= 0" using c_def x_def using mult_nonneg_nonneg by auto |
1074 assume c_def: "(c :: real) >= 0" |
846 ultimately have "c *\<^sub>R x : ?rhs" using x_def by auto |
1075 then have "c *\<^sub>R x = (c*cx) *\<^sub>R xx" |
847 } hence "cone ?rhs" unfolding cone_def by auto |
1076 using x_def by (simp add: algebra_simps) |
848 hence "?rhs : Collect cone" unfolding mem_Collect_eq by auto |
1077 moreover |
849 { fix x assume "x : S" hence "1 *\<^sub>R x : ?rhs" apply auto apply(rule_tac x="1" in exI) by auto |
1078 have "(c*cx) >= 0" |
850 hence "x : ?rhs" by auto |
1079 using c_def x_def using mult_nonneg_nonneg by auto |
851 } hence "S <= ?rhs" by auto |
1080 ultimately |
852 hence "?lhs <= ?rhs" using `?rhs : Collect cone` hull_minimal[of S "?rhs" "cone"] by auto |
1081 have "c *\<^sub>R x : ?rhs" using x_def by auto |
853 moreover |
1082 } then have "cone ?rhs" unfolding cone_def by auto |
854 { fix x assume "x : ?rhs" |
1083 then have "?rhs : Collect cone" unfolding mem_Collect_eq by auto |
855 from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto |
1084 { fix x |
856 hence "xx : cone hull S" using hull_subset[of S] by auto |
1085 assume "x : S" |
857 hence "x : ?lhs" using x_def cone_cone_hull[of S] cone_def[of "cone hull S"] by auto |
1086 then have "1 *\<^sub>R x : ?rhs" |
858 } ultimately show ?thesis by auto |
1087 apply auto |
|
1088 apply (rule_tac x="1" in exI) |
|
1089 apply auto |
|
1090 done |
|
1091 then have "x : ?rhs" by auto |
|
1092 } then have "S <= ?rhs" by auto |
|
1093 then have "?lhs <= ?rhs" |
|
1094 using `?rhs : Collect cone` hull_minimal[of S "?rhs" "cone"] by auto |
|
1095 moreover |
|
1096 { fix x |
|
1097 assume "x : ?rhs" |
|
1098 then obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto |
|
1099 then have "xx : cone hull S" using hull_subset[of S] by auto |
|
1100 then have "x : ?lhs" |
|
1101 using x_def cone_cone_hull[of S] cone_def[of "cone hull S"] by auto |
|
1102 } |
|
1103 ultimately show ?thesis by auto |
859 qed |
1104 qed |
860 |
1105 |
861 lemma cone_closure: |
1106 lemma cone_closure: |
862 fixes S :: "('a::real_normed_vector) set" |
1107 fixes S :: "('a::real_normed_vector) set" |
863 assumes "cone S" shows "cone (closure S)" |
1108 assumes "cone S" |
864 proof- |
1109 shows "cone (closure S)" |
865 { assume "S = {}" hence ?thesis by auto } |
1110 proof (cases "S = {}") |
866 moreover |
1111 case True |
867 { assume "S ~= {}" hence "0:S & (!c. c>0 --> op *\<^sub>R c ` S = S)" using cone_iff[of S] assms by auto |
1112 then show ?thesis by auto |
868 hence "0:(closure S) & (!c. c>0 --> op *\<^sub>R c ` (closure S) = (closure S))" |
1113 next |
869 using closure_subset by (auto simp add: closure_scaleR) |
1114 case False |
870 hence ?thesis using cone_iff[of "closure S"] by auto |
1115 then have "0:S & (!c. c>0 --> op *\<^sub>R c ` S = S)" |
871 } |
1116 using cone_iff[of S] assms by auto |
872 ultimately show ?thesis by blast |
1117 then have "0:(closure S) & (!c. c>0 --> op *\<^sub>R c ` (closure S) = (closure S))" |
873 qed |
1118 using closure_subset by (auto simp add: closure_scaleR) |
|
1119 then show ?thesis using cone_iff[of "closure S"] by auto |
|
1120 qed |
|
1121 |
874 |
1122 |
875 subsection {* Affine dependence and consequential theorems (from Lars Schewe) *} |
1123 subsection {* Affine dependence and consequential theorems (from Lars Schewe) *} |
876 |
1124 |
877 definition |
1125 definition affine_dependent :: "'a::real_vector set \<Rightarrow> bool" |
878 affine_dependent :: "'a::real_vector set \<Rightarrow> bool" where |
1126 where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> (affine hull (s - {x})))" |
879 "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> (affine hull (s - {x})))" |
|
880 |
1127 |
881 lemma affine_dependent_explicit: |
1128 lemma affine_dependent_explicit: |
882 "affine_dependent p \<longleftrightarrow> |
1129 "affine_dependent p \<longleftrightarrow> |
883 (\<exists>s u. finite s \<and> s \<subseteq> p \<and> setsum u s = 0 \<and> |
1130 (\<exists>s u. finite s \<and> s \<subseteq> p \<and> setsum u s = 0 \<and> |
884 (\<exists>v\<in>s. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = 0)" |
1131 (\<exists>v\<in>s. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = 0)" |
885 unfolding affine_dependent_def affine_hull_explicit mem_Collect_eq apply(rule) |
1132 unfolding affine_dependent_def affine_hull_explicit mem_Collect_eq |
886 apply(erule bexE,erule exE,erule exE) apply(erule conjE)+ defer apply(erule exE,erule exE) apply(erule conjE)+ apply(erule bexE) |
1133 apply rule |
887 proof- |
1134 apply (erule bexE, erule exE, erule exE) |
888 fix x s u assume as:"x \<in> p" "finite s" "s \<noteq> {}" "s \<subseteq> p - {x}" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x" |
1135 apply (erule conjE)+ |
|
1136 defer |
|
1137 apply (erule exE, erule exE) |
|
1138 apply (erule conjE)+ |
|
1139 apply (erule bexE) |
|
1140 proof - |
|
1141 fix x s u |
|
1142 assume as: "x \<in> p" "finite s" "s \<noteq> {}" "s \<subseteq> p - {x}" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x" |
889 have "x\<notin>s" using as(1,4) by auto |
1143 have "x\<notin>s" using as(1,4) by auto |
890 show "\<exists>s u. finite s \<and> s \<subseteq> p \<and> setsum u s = 0 \<and> (\<exists>v\<in>s. u v \<noteq> 0) \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0" |
1144 show "\<exists>s u. finite s \<and> s \<subseteq> p \<and> setsum u s = 0 \<and> (\<exists>v\<in>s. u v \<noteq> 0) \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0" |
891 apply(rule_tac x="insert x s" in exI, rule_tac x="\<lambda>v. if v = x then - 1 else u v" in exI) |
1145 apply (rule_tac x="insert x s" in exI, rule_tac x="\<lambda>v. if v = x then - 1 else u v" in exI) |
892 unfolding if_smult and setsum_clauses(2)[OF as(2)] and setsum_delta_notmem[OF `x\<notin>s`] and as using as by auto |
1146 unfolding if_smult and setsum_clauses(2)[OF as(2)] and setsum_delta_notmem[OF `x\<notin>s`] and as |
|
1147 using as apply auto |
|
1148 done |
893 next |
1149 next |
894 fix s u v assume as:"finite s" "s \<subseteq> p" "setsum u s = 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0" "v \<in> s" "u v \<noteq> 0" |
1150 fix s u v |
|
1151 assume as:"finite s" "s \<subseteq> p" "setsum u s = 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0" "v \<in> s" "u v \<noteq> 0" |
895 have "s \<noteq> {v}" using as(3,6) by auto |
1152 have "s \<noteq> {v}" using as(3,6) by auto |
896 thus "\<exists>x\<in>p. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p - {x} \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" |
1153 then show "\<exists>x\<in>p. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p - {x} \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" |
897 apply(rule_tac x=v in bexI, rule_tac x="s - {v}" in exI, rule_tac x="\<lambda>x. - (1 / u v) * u x" in exI) |
1154 apply (rule_tac x=v in bexI, rule_tac x="s - {v}" in exI, |
898 unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] unfolding setsum_right_distrib[THEN sym] and setsum_diff1[OF as(1)] using as by auto |
1155 rule_tac x="\<lambda>x. - (1 / u v) * u x" in exI) |
|
1156 unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] |
|
1157 unfolding setsum_right_distrib[THEN sym] and setsum_diff1[OF as(1)] |
|
1158 using as apply auto |
|
1159 done |
899 qed |
1160 qed |
900 |
1161 |
901 lemma affine_dependent_explicit_finite: |
1162 lemma affine_dependent_explicit_finite: |
902 fixes s :: "'a::real_vector set" assumes "finite s" |
1163 fixes s :: "'a::real_vector set" |
|
1164 assumes "finite s" |
903 shows "affine_dependent s \<longleftrightarrow> (\<exists>u. setsum u s = 0 \<and> (\<exists>v\<in>s. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = 0)" |
1165 shows "affine_dependent s \<longleftrightarrow> (\<exists>u. setsum u s = 0 \<and> (\<exists>v\<in>s. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = 0)" |
904 (is "?lhs = ?rhs") |
1166 (is "?lhs = ?rhs") |
905 proof |
1167 proof |
906 have *:"\<And>vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else (0::'a))" by auto |
1168 have *: "\<And>vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else (0::'a))" |
|
1169 by auto |
907 assume ?lhs |
1170 assume ?lhs |
908 then obtain t u v where "finite t" "t \<subseteq> s" "setsum u t = 0" "v\<in>t" "u v \<noteq> 0" "(\<Sum>v\<in>t. u v *\<^sub>R v) = 0" |
1171 then obtain t u v where |
|
1172 "finite t" "t \<subseteq> s" "setsum u t = 0" "v\<in>t" "u v \<noteq> 0" "(\<Sum>v\<in>t. u v *\<^sub>R v) = 0" |
909 unfolding affine_dependent_explicit by auto |
1173 unfolding affine_dependent_explicit by auto |
910 thus ?rhs apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI) |
1174 then show ?rhs |
|
1175 apply (rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI) |
911 apply auto unfolding * and setsum_restrict_set[OF assms, THEN sym] |
1176 apply auto unfolding * and setsum_restrict_set[OF assms, THEN sym] |
912 unfolding Int_absorb1[OF `t\<subseteq>s`] by auto |
1177 unfolding Int_absorb1[OF `t\<subseteq>s`] |
|
1178 apply auto |
|
1179 done |
913 next |
1180 next |
914 assume ?rhs |
1181 assume ?rhs |
915 then obtain u v where "setsum u s = 0" "v\<in>s" "u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0" by auto |
1182 then obtain u v where "setsum u s = 0" "v\<in>s" "u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0" by auto |
916 thus ?lhs unfolding affine_dependent_explicit using assms by auto |
1183 then show ?lhs unfolding affine_dependent_explicit |
917 qed |
1184 using assms by auto |
|
1185 qed |
|
1186 |
918 |
1187 |
919 subsection {* Connectedness of convex sets *} |
1188 subsection {* Connectedness of convex sets *} |
920 |
1189 |
921 lemma connected_real_lemma: |
1190 lemma connected_real_lemma: |
922 fixes f :: "real \<Rightarrow> 'a::metric_space" |
1191 fixes f :: "real \<Rightarrow> 'a::metric_space" |
923 assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2" |
1192 assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2" |
924 and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y - x) < d \<longrightarrow> dist(f y) (f x) < e" |
1193 and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y - x) < d \<longrightarrow> dist(f y) (f x) < e" |
925 and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1" |
1194 and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1" |
926 and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2" |
1195 and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2" |
927 and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)" |
1196 and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)" |
928 shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x") |
1197 shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x") |
929 proof- |
1198 proof - |
930 let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}" |
1199 let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}" |
931 have Se: " \<exists>x. x \<in> ?S" apply (rule exI[where x=a]) by (auto simp add: fa) |
1200 have Se: " \<exists>x. x \<in> ?S" apply (rule exI[where x=a]) by (auto simp add: fa) |
932 have Sub: "\<exists>y. isUb UNIV ?S y" |
1201 have Sub: "\<exists>y. isUb UNIV ?S y" |
933 apply (rule exI[where x= b]) |
1202 apply (rule exI[where x= b]) |
934 using ab fb e12 by (auto simp add: isUb_def setle_def) |
1203 using ab fb e12 by (auto simp add: isUb_def setle_def) |