10660 using closure_subset by force |
10691 using closure_subset by force |
10661 |
10692 |
10662 lemma setdist_le_sing: "x \<in> s ==> setdist s t \<le> setdist {x} t" |
10693 lemma setdist_le_sing: "x \<in> s ==> setdist s t \<le> setdist {x} t" |
10663 using setdist_subset_left by auto |
10694 using setdist_subset_left by auto |
10664 |
10695 |
|
10696 |
|
10697 subsection\<open>Basic lemmas about hyperplanes and halfspaces\<close> |
|
10698 |
|
10699 lemma hyperplane_eq_Ex: |
|
10700 assumes "a \<noteq> 0" obtains x where "a \<bullet> x = b" |
|
10701 by (rule_tac x = "(b / (a \<bullet> a)) *\<^sub>R a" in that) (simp add: assms) |
|
10702 |
|
10703 lemma hyperplane_eq_empty: |
|
10704 "{x. a \<bullet> x = b} = {} \<longleftrightarrow> a = 0 \<and> b \<noteq> 0" |
|
10705 using hyperplane_eq_Ex apply auto[1] |
|
10706 using inner_zero_right by blast |
|
10707 |
|
10708 lemma hyperplane_eq_UNIV: |
|
10709 "{x. a \<bullet> x = b} = UNIV \<longleftrightarrow> a = 0 \<and> b = 0" |
|
10710 proof - |
|
10711 have "UNIV \<subseteq> {x. a \<bullet> x = b} \<Longrightarrow> a = 0 \<and> b = 0" |
|
10712 apply (drule_tac c = "((b+1) / (a \<bullet> a)) *\<^sub>R a" in subsetD) |
|
10713 apply simp_all |
|
10714 by (metis add_cancel_right_right divide_1 zero_neq_one) |
|
10715 then show ?thesis by force |
|
10716 qed |
|
10717 |
|
10718 lemma halfspace_eq_empty_lt: |
|
10719 "{x. a \<bullet> x < b} = {} \<longleftrightarrow> a = 0 \<and> b \<le> 0" |
|
10720 proof - |
|
10721 have "{x. a \<bullet> x < b} \<subseteq> {} \<Longrightarrow> a = 0 \<and> b \<le> 0" |
|
10722 apply (rule ccontr) |
|
10723 apply (drule_tac c = "((b-1) / (a \<bullet> a)) *\<^sub>R a" in subsetD) |
|
10724 apply force+ |
|
10725 done |
|
10726 then show ?thesis by force |
|
10727 qed |
|
10728 |
|
10729 lemma halfspace_eq_empty_gt: |
|
10730 "{x. a \<bullet> x > b} = {} \<longleftrightarrow> a = 0 \<and> b \<ge> 0" |
|
10731 using halfspace_eq_empty_lt [of "-a" "-b"] |
|
10732 by simp |
|
10733 |
|
10734 lemma halfspace_eq_empty_le: |
|
10735 "{x. a \<bullet> x \<le> b} = {} \<longleftrightarrow> a = 0 \<and> b < 0" |
|
10736 proof - |
|
10737 have "{x. a \<bullet> x \<le> b} \<subseteq> {} \<Longrightarrow> a = 0 \<and> b < 0" |
|
10738 apply (rule ccontr) |
|
10739 apply (drule_tac c = "((b-1) / (a \<bullet> a)) *\<^sub>R a" in subsetD) |
|
10740 apply force+ |
|
10741 done |
|
10742 then show ?thesis by force |
|
10743 qed |
|
10744 |
|
10745 lemma halfspace_eq_empty_ge: |
|
10746 "{x. a \<bullet> x \<ge> b} = {} \<longleftrightarrow> a = 0 \<and> b > 0" |
|
10747 using halfspace_eq_empty_le [of "-a" "-b"] |
|
10748 by simp |
|
10749 |
|
10750 subsubsection\<open>Representing affine hull as a finite intersection of hyperplanes\<close> |
|
10751 |
|
10752 proposition affine_hull_convex_Int_nonempty_interior: |
|
10753 fixes S :: "'a::real_normed_vector set" |
|
10754 assumes "convex S" "S \<inter> interior T \<noteq> {}" |
|
10755 shows "affine hull (S \<inter> T) = affine hull S" |
|
10756 proof |
|
10757 show "affine hull (S \<inter> T) \<subseteq> affine hull S" |
|
10758 by (simp add: hull_mono) |
|
10759 next |
|
10760 obtain a where "a \<in> S" "a \<in> T" and at: "a \<in> interior T" |
|
10761 using assms interior_subset by blast |
|
10762 then obtain e where "e > 0" and e: "cball a e \<subseteq> T" |
|
10763 using mem_interior_cball by blast |
|
10764 have *: "x \<in> op + a ` span ((\<lambda>x. x - a) ` (S \<inter> T))" if "x \<in> S" for x |
|
10765 proof (cases "x = a") |
|
10766 case True with that span_0 eq_add_iff image_def mem_Collect_eq show ?thesis |
|
10767 by blast |
|
10768 next |
|
10769 case False |
|
10770 def k \<equiv> "min (1/2) (e / norm (x-a))" |
|
10771 have k: "0 < k" "k < 1" |
|
10772 using \<open>e > 0\<close> False by (auto simp: k_def) |
|
10773 then have xa: "(x-a) = inverse k *\<^sub>R k *\<^sub>R (x-a)" |
|
10774 by simp |
|
10775 have "e / norm (x - a) \<ge> k" |
|
10776 using k_def by linarith |
|
10777 then have "a + k *\<^sub>R (x - a) \<in> cball a e" |
|
10778 using \<open>0 < k\<close> False by (simp add: dist_norm field_simps) |
|
10779 then have T: "a + k *\<^sub>R (x - a) \<in> T" |
|
10780 using e by blast |
|
10781 have S: "a + k *\<^sub>R (x - a) \<in> S" |
|
10782 using k \<open>a \<in> S\<close> convexD [OF \<open>convex S\<close> \<open>a \<in> S\<close> \<open>x \<in> S\<close>, of "1-k" k] |
|
10783 by (simp add: algebra_simps) |
|
10784 have "inverse k *\<^sub>R k *\<^sub>R (x-a) \<in> span ((\<lambda>x. x - a) ` (S \<inter> T))" |
|
10785 apply (rule span_mul) |
|
10786 apply (rule span_superset) |
|
10787 apply (rule image_eqI [where x = "a + k *\<^sub>R (x - a)"]) |
|
10788 apply (auto simp: S T) |
|
10789 done |
|
10790 with xa image_iff show ?thesis by fastforce |
|
10791 qed |
|
10792 show "affine hull S \<subseteq> affine hull (S \<inter> T)" |
|
10793 apply (simp add: subset_hull) |
|
10794 apply (simp add: \<open>a \<in> S\<close> \<open>a \<in> T\<close> hull_inc affine_hull_span_gen [of a]) |
|
10795 apply (force simp: *) |
|
10796 done |
|
10797 qed |
|
10798 |
|
10799 corollary affine_hull_convex_Int_open: |
|
10800 fixes S :: "'a::real_normed_vector set" |
|
10801 assumes "convex S" "open T" "S \<inter> T \<noteq> {}" |
|
10802 shows "affine hull (S \<inter> T) = affine hull S" |
|
10803 using affine_hull_convex_Int_nonempty_interior assms interior_eq by blast |
|
10804 |
|
10805 corollary affine_hull_affine_Int_nonempty_interior: |
|
10806 fixes S :: "'a::real_normed_vector set" |
|
10807 assumes "affine S" "S \<inter> interior T \<noteq> {}" |
|
10808 shows "affine hull (S \<inter> T) = affine hull S" |
|
10809 by (simp add: affine_hull_convex_Int_nonempty_interior affine_imp_convex assms) |
|
10810 |
|
10811 corollary affine_hull_affine_inter_open: |
|
10812 fixes S :: "'a::real_normed_vector set" |
|
10813 assumes "affine S" "open T" "S \<inter> T \<noteq> {}" |
|
10814 shows "affine hull (S \<inter> T) = affine hull S" |
|
10815 by (simp add: affine_hull_convex_Int_open affine_imp_convex assms) |
|
10816 |
|
10817 corollary affine_hull_convex_Int_openin: |
|
10818 fixes S :: "'a::real_normed_vector set" |
|
10819 assumes "convex S" "openin (subtopology euclidean (affine hull S)) T" "S \<inter> T \<noteq> {}" |
|
10820 shows "affine hull (S \<inter> T) = affine hull S" |
|
10821 using assms unfolding openin_open |
|
10822 by (metis affine_hull_convex_Int_open hull_subset inf.orderE inf_assoc) |
|
10823 |
|
10824 corollary affine_hull_open_in: |
|
10825 fixes S :: "'a::real_normed_vector set" |
|
10826 assumes "openin (subtopology euclidean (affine hull T)) S" "S \<noteq> {}" |
|
10827 shows "affine hull S = affine hull T" |
|
10828 using assms unfolding openin_open |
|
10829 by (metis affine_affine_hull affine_hull_affine_inter_open hull_hull) |
|
10830 |
|
10831 corollary affine_hull_open: |
|
10832 fixes S :: "'a::real_normed_vector set" |
|
10833 assumes "open S" "S \<noteq> {}" |
|
10834 shows "affine hull S = UNIV" |
|
10835 by (metis affine_hull_convex_Int_nonempty_interior assms convex_UNIV hull_UNIV inf_top.left_neutral interior_open) |
|
10836 |
|
10837 lemma aff_dim_convex_Int_nonempty_interior: |
|
10838 fixes S :: "'a::euclidean_space set" |
|
10839 shows "\<lbrakk>convex S; S \<inter> interior T \<noteq> {}\<rbrakk> \<Longrightarrow> aff_dim(S \<inter> T) = aff_dim S" |
|
10840 using aff_dim_affine_hull2 affine_hull_convex_Int_nonempty_interior by blast |
|
10841 |
|
10842 lemma aff_dim_convex_Int_open: |
|
10843 fixes S :: "'a::euclidean_space set" |
|
10844 shows "\<lbrakk>convex S; open T; S \<inter> T \<noteq> {}\<rbrakk> \<Longrightarrow> aff_dim(S \<inter> T) = aff_dim S" |
|
10845 using aff_dim_convex_Int_nonempty_interior interior_eq by blast |
|
10846 |
|
10847 lemma affine_hull_halfspace_lt: |
|
10848 fixes a :: "'a::euclidean_space" |
|
10849 shows "affine hull {x. a \<bullet> x < r} = (if a = 0 \<and> r \<le> 0 then {} else UNIV)" |
|
10850 using halfspace_eq_empty_lt [of a r] |
|
10851 by (simp add: open_halfspace_lt affine_hull_open) |
|
10852 |
|
10853 lemma affine_hull_halfspace_le: |
|
10854 fixes a :: "'a::euclidean_space" |
|
10855 shows "affine hull {x. a \<bullet> x \<le> r} = (if a = 0 \<and> r < 0 then {} else UNIV)" |
|
10856 proof (cases "a = 0") |
|
10857 case True then show ?thesis by simp |
|
10858 next |
|
10859 case False |
|
10860 then have "affine hull closure {x. a \<bullet> x < r} = UNIV" |
|
10861 using affine_hull_halfspace_lt closure_same_affine_hull by fastforce |
|
10862 moreover have "{x. a \<bullet> x < r} \<subseteq> {x. a \<bullet> x \<le> r}" |
|
10863 by (simp add: Collect_mono) |
|
10864 ultimately show ?thesis using False antisym_conv hull_mono top_greatest |
|
10865 by (metis affine_hull_halfspace_lt) |
|
10866 qed |
|
10867 |
|
10868 lemma affine_hull_halfspace_gt: |
|
10869 fixes a :: "'a::euclidean_space" |
|
10870 shows "affine hull {x. a \<bullet> x > r} = (if a = 0 \<and> r \<ge> 0 then {} else UNIV)" |
|
10871 using halfspace_eq_empty_gt [of r a] |
|
10872 by (simp add: open_halfspace_gt affine_hull_open) |
|
10873 |
|
10874 lemma affine_hull_halfspace_ge: |
|
10875 fixes a :: "'a::euclidean_space" |
|
10876 shows "affine hull {x. a \<bullet> x \<ge> r} = (if a = 0 \<and> r > 0 then {} else UNIV)" |
|
10877 using affine_hull_halfspace_le [of "-a" "-r"] by simp |
|
10878 |
|
10879 lemma aff_dim_halfspace_lt: |
|
10880 fixes a :: "'a::euclidean_space" |
|
10881 shows "aff_dim {x. a \<bullet> x < r} = |
|
10882 (if a = 0 \<and> r \<le> 0 then -1 else DIM('a))" |
|
10883 by simp (metis aff_dim_open halfspace_eq_empty_lt open_halfspace_lt) |
|
10884 |
|
10885 lemma aff_dim_halfspace_le: |
|
10886 fixes a :: "'a::euclidean_space" |
|
10887 shows "aff_dim {x. a \<bullet> x \<le> r} = |
|
10888 (if a = 0 \<and> r < 0 then -1 else DIM('a))" |
|
10889 proof - |
|
10890 have "int (DIM('a)) = aff_dim (UNIV::'a set)" |
|
10891 by (simp add: aff_dim_univ) |
|
10892 then have "aff_dim (affine hull {x. a \<bullet> x \<le> r}) = DIM('a)" if "(a = 0 \<longrightarrow> r \<ge> 0)" |
|
10893 using that by (simp add: affine_hull_halfspace_le not_less) |
|
10894 then show ?thesis |
|
10895 by (force simp: aff_dim_affine_hull) |
|
10896 qed |
|
10897 |
|
10898 lemma aff_dim_halfspace_gt: |
|
10899 fixes a :: "'a::euclidean_space" |
|
10900 shows "aff_dim {x. a \<bullet> x > r} = |
|
10901 (if a = 0 \<and> r \<ge> 0 then -1 else DIM('a))" |
|
10902 by simp (metis aff_dim_open halfspace_eq_empty_gt open_halfspace_gt) |
|
10903 |
|
10904 lemma aff_dim_halfspace_ge: |
|
10905 fixes a :: "'a::euclidean_space" |
|
10906 shows "aff_dim {x. a \<bullet> x \<ge> r} = |
|
10907 (if a = 0 \<and> r > 0 then -1 else DIM('a))" |
|
10908 using aff_dim_halfspace_le [of "-a" "-r"] by simp |
|
10909 |
|
10910 subsection\<open>Properties of special hyperplanes\<close> |
|
10911 |
|
10912 lemma subspace_hyperplane: "subspace {x. a \<bullet> x = 0}" |
|
10913 by (simp add: subspace_def inner_right_distrib) |
|
10914 |
|
10915 lemma special_hyperplane_span: |
|
10916 fixes S :: "'n::euclidean_space set" |
|
10917 assumes "k \<in> Basis" |
|
10918 shows "{x. k \<bullet> x = 0} = span (Basis - {k})" |
|
10919 proof - |
|
10920 have *: "x \<in> span (Basis - {k})" if "k \<bullet> x = 0" for x |
|
10921 proof - |
|
10922 have "x = (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b)" |
|
10923 by (simp add: euclidean_representation) |
|
10924 also have "... = (\<Sum>b \<in> Basis - {k}. (x \<bullet> b) *\<^sub>R b)" |
|
10925 by (auto simp: setsum.remove [of _ k] inner_commute assms that) |
|
10926 finally have "x = (\<Sum>b\<in>Basis - {k}. (x \<bullet> b) *\<^sub>R b)" . |
|
10927 then show ?thesis |
|
10928 by (simp add: Linear_Algebra.span_finite) metis |
|
10929 qed |
|
10930 show ?thesis |
|
10931 apply (rule span_subspace [symmetric]) |
|
10932 using assms |
|
10933 apply (auto simp: inner_not_same_Basis intro: * subspace_hyperplane) |
|
10934 done |
|
10935 qed |
|
10936 |
|
10937 lemma dim_special_hyperplane: |
|
10938 fixes k :: "'n::euclidean_space" |
|
10939 shows "k \<in> Basis \<Longrightarrow> dim {x. k \<bullet> x = 0} = DIM('n) - 1" |
|
10940 apply (simp add: special_hyperplane_span) |
|
10941 apply (rule Linear_Algebra.dim_unique [OF subset_refl]) |
|
10942 apply (auto simp: Diff_subset independent_substdbasis) |
|
10943 apply (metis member_remove remove_def span_clauses(1)) |
|
10944 done |
|
10945 |
|
10946 proposition dim_hyperplane: |
|
10947 fixes a :: "'a::euclidean_space" |
|
10948 assumes "a \<noteq> 0" |
|
10949 shows "dim {x. a \<bullet> x = 0} = DIM('a) - 1" |
|
10950 proof - |
|
10951 have span0: "span {x. a \<bullet> x = 0} = {x. a \<bullet> x = 0}" |
|
10952 by (rule span_unique) (auto simp: subspace_hyperplane) |
|
10953 then obtain B where "independent B" |
|
10954 and Bsub: "B \<subseteq> {x. a \<bullet> x = 0}" |
|
10955 and subspB: "{x. a \<bullet> x = 0} \<subseteq> span B" |
|
10956 and card0: "(card B = dim {x. a \<bullet> x = 0})" |
|
10957 and ortho: "pairwise orthogonal B" |
|
10958 using orthogonal_basis_exists by metis |
|
10959 with assms have "a \<notin> span B" |
|
10960 by (metis (mono_tags, lifting) span_eq inner_eq_zero_iff mem_Collect_eq span0 span_subspace) |
|
10961 then have ind: "independent (insert a B)" |
|
10962 by (simp add: \<open>independent B\<close> independent_insert) |
|
10963 have "finite B" |
|
10964 using \<open>independent B\<close> independent_bound by blast |
|
10965 have "UNIV \<subseteq> span (insert a B)" |
|
10966 proof fix y::'a |
|
10967 obtain r z where z: "y = r *\<^sub>R a + z" "a \<bullet> z = 0" |
|
10968 apply (rule_tac r="(a \<bullet> y) / (a \<bullet> a)" and z = "y - ((a \<bullet> y) / (a \<bullet> a)) *\<^sub>R a" in that) |
|
10969 using assms |
|
10970 by (auto simp: algebra_simps) |
|
10971 show "y \<in> span (insert a B)" |
|
10972 by (metis (mono_tags, lifting) z Bsub Convex_Euclidean_Space.span_eq |
|
10973 add_diff_cancel_left' mem_Collect_eq span0 span_breakdown_eq span_subspace subspB) |
|
10974 qed |
|
10975 then have dima: "DIM('a) = dim(insert a B)" |
|
10976 by (metis antisym dim_UNIV dim_subset_UNIV subset_le_dim) |
|
10977 then show ?thesis |
|
10978 by (metis (mono_tags, lifting) Bsub Diff_insert_absorb \<open>a \<notin> span B\<close> ind card0 card_Diff_singleton dim_span indep_card_eq_dim_span insertI1 subsetCE subspB) |
|
10979 qed |
|
10980 |
|
10981 lemma lowdim_eq_hyperplane: |
|
10982 fixes S :: "'a::euclidean_space set" |
|
10983 assumes "dim S = DIM('a) - 1" |
|
10984 obtains a where "a \<noteq> 0" and "span S = {x. a \<bullet> x = 0}" |
|
10985 proof - |
|
10986 have [simp]: "dim S < DIM('a)" |
|
10987 by (simp add: DIM_positive assms) |
|
10988 then obtain b where b: "b \<noteq> 0" "span S \<subseteq> {a. b \<bullet> a = 0}" |
|
10989 using lowdim_subset_hyperplane [of S] by fastforce |
|
10990 show ?thesis |
|
10991 using b that real_vector_class.subspace_span [of S] |
|
10992 by (simp add: assms dim_hyperplane subspace_dim_equal subspace_hyperplane) |
|
10993 qed |
|
10994 |
|
10995 lemma dim_eq_hyperplane: |
|
10996 fixes S :: "'n::euclidean_space set" |
|
10997 shows "dim S = DIM('n) - 1 \<longleftrightarrow> (\<exists>a. a \<noteq> 0 \<and> span S = {x. a \<bullet> x = 0})" |
|
10998 by (metis One_nat_def dim_hyperplane dim_span lowdim_eq_hyperplane) |
|
10999 |
|
11000 proposition aff_dim_eq_hyperplane: |
|
11001 fixes S :: "'a::euclidean_space set" |
|
11002 shows "aff_dim S = DIM('a) - 1 \<longleftrightarrow> (\<exists>a b. a \<noteq> 0 \<and> affine hull S = {x. a \<bullet> x = b})" |
|
11003 proof (cases "S = {}") |
|
11004 case True then show ?thesis |
|
11005 by (auto simp: dest: hyperplane_eq_Ex) |
|
11006 next |
|
11007 case False |
|
11008 then obtain c where "c \<in> S" by blast |
|
11009 show ?thesis |
|
11010 proof (cases "c = 0") |
|
11011 case True show ?thesis |
|
11012 apply (simp add: aff_dim_eq_dim [of c] affine_hull_span_gen [of c] \<open>c \<in> S\<close> hull_inc dim_eq_hyperplane |
|
11013 del: One_nat_def) |
|
11014 apply (rule ex_cong) |
|
11015 using span_0 |
|
11016 apply (force simp: \<open>c = 0\<close>) |
|
11017 done |
|
11018 next |
|
11019 case False |
|
11020 have xc_im: "x \<in> op + c ` {y. a \<bullet> y = 0}" if "a \<bullet> x = a \<bullet> c" for a x |
|
11021 proof - |
|
11022 have "\<exists>y. a \<bullet> y = 0 \<and> c + y = x" |
|
11023 by (metis that add.commute diff_add_cancel inner_commute inner_diff_left right_minus_eq) |
|
11024 then show "x \<in> op + c ` {y. a \<bullet> y = 0}" |
|
11025 by blast |
|
11026 qed |
|
11027 have 2: "span ((\<lambda>x. x - c) ` S) = {x. a \<bullet> x = 0}" |
|
11028 if "op + c ` span ((\<lambda>x. x - c) ` S) = {x. a \<bullet> x = b}" for a b |
|
11029 proof - |
|
11030 have "b = a \<bullet> c" |
|
11031 using span_0 that by fastforce |
|
11032 with that have "op + c ` span ((\<lambda>x. x - c) ` S) = {x. a \<bullet> x = a \<bullet> c}" |
|
11033 by simp |
|
11034 then have "span ((\<lambda>x. x - c) ` S) = (\<lambda>x. x - c) ` {x. a \<bullet> x = a \<bullet> c}" |
|
11035 by (metis (no_types) image_cong translation_galois uminus_add_conv_diff) |
|
11036 also have "... = {x. a \<bullet> x = 0}" |
|
11037 by (force simp: inner_distrib inner_diff_right |
|
11038 intro: image_eqI [where x="x+c" for x]) |
|
11039 finally show ?thesis . |
|
11040 qed |
|
11041 show ?thesis |
|
11042 apply (simp add: aff_dim_eq_dim [of c] affine_hull_span_gen [of c] \<open>c \<in> S\<close> hull_inc dim_eq_hyperplane |
|
11043 del: One_nat_def, safe) |
|
11044 apply (fastforce simp add: inner_distrib intro: xc_im) |
|
11045 apply (force simp: intro!: 2) |
|
11046 done |
|
11047 qed |
|
11048 qed |
|
11049 |
|
11050 corollary aff_dim_hyperplane: |
|
11051 fixes a :: "'a::euclidean_space" |
|
11052 shows "a \<noteq> 0 \<Longrightarrow> aff_dim {x. a \<bullet> x = r} = DIM('a) - 1" |
|
11053 by (metis aff_dim_eq_hyperplane affine_hull_eq affine_hyperplane) |
|
11054 |
|
11055 subsection\<open>Some stepping theorems\<close> |
|
11056 |
|
11057 lemma dim_empty [simp]: "dim ({} :: 'a::euclidean_space set) = 0" |
|
11058 by (force intro!: dim_unique) |
|
11059 |
|
11060 lemma dim_insert: |
|
11061 fixes x :: "'a::euclidean_space" |
|
11062 shows "dim (insert x S) = (if x \<in> span S then dim S else dim S + 1)" |
|
11063 proof - |
|
11064 show ?thesis |
|
11065 proof (cases "x \<in> span S") |
|
11066 case True then show ?thesis |
|
11067 by (metis dim_span span_redundant) |
|
11068 next |
|
11069 case False |
|
11070 obtain B where B: "B \<subseteq> span S" "independent B" "span S \<subseteq> span B" "card B = dim (span S)" |
|
11071 using basis_exists [of "span S"] by blast |
|
11072 have 1: "insert x B \<subseteq> span (insert x S)" |
|
11073 by (meson \<open>B \<subseteq> span S\<close> dual_order.trans insertI1 insert_subsetI span_mono span_superset subset_insertI) |
|
11074 have 2: "span (insert x S) \<subseteq> span (insert x B)" |
|
11075 by (metis \<open>B \<subseteq> span S\<close> \<open>span S \<subseteq> span B\<close> span_breakdown_eq span_subspace subsetI subspace_span) |
|
11076 have 3: "independent (insert x B)" |
|
11077 by (metis B independent_insert span_subspace subspace_span False) |
|
11078 have "dim (span (insert x S)) = Suc (dim S)" |
|
11079 apply (rule dim_unique [OF 1 2 3]) |
|
11080 by (metis B False card_insert_disjoint dim_span independent_imp_finite subsetCE) |
|
11081 then show ?thesis |
|
11082 by (simp add: False) |
|
11083 qed |
|
11084 qed |
|
11085 |
|
11086 lemma dim_singleton [simp]: |
|
11087 fixes x :: "'a::euclidean_space" |
|
11088 shows "dim{x} = (if x = 0 then 0 else 1)" |
|
11089 by (simp add: dim_insert) |
|
11090 |
|
11091 lemma dim_eq_0 [simp]: |
|
11092 fixes S :: "'a::euclidean_space set" |
|
11093 shows "dim S = 0 \<longleftrightarrow> S \<subseteq> {0}" |
|
11094 apply safe |
|
11095 apply (metis DIM_positive DIM_real card_ge_dim_independent contra_subsetD dim_empty dim_insert dim_singleton empty_subsetI independent_empty less_not_refl zero_le) |
|
11096 by (metis dim_singleton dim_subset le_0_eq) |
|
11097 |
|
11098 lemma aff_dim_insert: |
|
11099 fixes a :: "'a::euclidean_space" |
|
11100 shows "aff_dim (insert a S) = (if a \<in> affine hull S then aff_dim S else aff_dim S + 1)" |
|
11101 proof (cases "S = {}") |
|
11102 case True then show ?thesis |
|
11103 by simp |
|
11104 next |
|
11105 case False |
|
11106 then obtain x s' where S: "S = insert x s'" "x \<notin> s'" |
|
11107 by (meson Set.set_insert all_not_in_conv) |
|
11108 show ?thesis using S |
|
11109 apply (simp add: hull_redundant cong: aff_dim_affine_hull2) |
|
11110 apply (simp add: affine_hull_insert_span_gen hull_inc) |
|
11111 apply (simp add: insert_commute [of a] hull_inc aff_dim_eq_dim [of x] dim_insert span_0) |
|
11112 apply (metis (no_types, lifting) add_minus_cancel image_iff uminus_add_conv_diff) |
|
11113 done |
|
11114 qed |
|
11115 |
|
11116 lemma subspace_bounded_eq_trivial: |
|
11117 fixes S :: "'a::real_normed_vector set" |
|
11118 assumes "subspace S" |
|
11119 shows "bounded S \<longleftrightarrow> S = {0}" |
|
11120 proof - |
|
11121 have "False" if "bounded S" "x \<in> S" "x \<noteq> 0" for x |
|
11122 proof - |
|
11123 obtain B where B: "\<And>y. y \<in> S \<Longrightarrow> norm y < B" "B > 0" |
|
11124 using \<open>bounded S\<close> by (force simp: bounded_pos_less) |
|
11125 have "(B / norm x) *\<^sub>R x \<in> S" |
|
11126 using assms subspace_mul \<open>x \<in> S\<close> by auto |
|
11127 moreover have "norm ((B / norm x) *\<^sub>R x) = B" |
|
11128 using that B by (simp add: algebra_simps) |
|
11129 ultimately show False using B by force |
|
11130 qed |
|
11131 then have "bounded S \<Longrightarrow> S = {0}" |
|
11132 using assms subspace_0 by fastforce |
|
11133 then show ?thesis |
|
11134 by blast |
|
11135 qed |
|
11136 |
|
11137 lemma affine_bounded_eq_trivial: |
|
11138 fixes S :: "'a::real_normed_vector set" |
|
11139 assumes "affine S" |
|
11140 shows "bounded S \<longleftrightarrow> S = {} \<or> (\<exists>a. S = {a})" |
|
11141 proof (cases "S = {}") |
|
11142 case True then show ?thesis |
|
11143 by simp |
|
11144 next |
|
11145 case False |
|
11146 then obtain b where "b \<in> S" by blast |
|
11147 with False assms show ?thesis |
|
11148 apply safe |
|
11149 using affine_diffs_subspace [OF assms \<open>b \<in> S\<close>] |
|
11150 apply (metis (no_types, lifting) subspace_bounded_eq_trivial ab_left_minus bounded_translation |
|
11151 image_empty image_insert translation_invert) |
|
11152 apply force |
|
11153 done |
|
11154 qed |
|
11155 |
|
11156 lemma affine_bounded_eq_lowdim: |
|
11157 fixes S :: "'a::euclidean_space set" |
|
11158 assumes "affine S" |
|
11159 shows "bounded S \<longleftrightarrow> aff_dim S \<le> 0" |
|
11160 apply safe |
|
11161 using affine_bounded_eq_trivial assms apply fastforce |
|
11162 by (metis aff_dim_sing aff_dim_subset affine_dim_equal affine_sing all_not_in_conv assms bounded_empty bounded_insert dual_order.antisym empty_subsetI insert_subset) |
|
11163 |
|
11164 |
|
11165 lemma bounded_hyperplane_eq_trivial_0: |
|
11166 fixes a :: "'a::euclidean_space" |
|
11167 assumes "a \<noteq> 0" |
|
11168 shows "bounded {x. a \<bullet> x = 0} \<longleftrightarrow> DIM('a) = 1" |
|
11169 proof |
|
11170 assume "bounded {x. a \<bullet> x = 0}" |
|
11171 then have "aff_dim {x. a \<bullet> x = 0} \<le> 0" |
|
11172 by (simp add: affine_bounded_eq_lowdim affine_hyperplane) |
|
11173 with assms show "DIM('a) = 1" |
|
11174 by (simp add: le_Suc_eq aff_dim_hyperplane) |
|
11175 next |
|
11176 assume "DIM('a) = 1" |
|
11177 then show "bounded {x. a \<bullet> x = 0}" |
|
11178 by (simp add: aff_dim_hyperplane affine_bounded_eq_lowdim affine_hyperplane assms) |
|
11179 qed |
|
11180 |
|
11181 lemma bounded_hyperplane_eq_trivial: |
|
11182 fixes a :: "'a::euclidean_space" |
|
11183 shows "bounded {x. a \<bullet> x = r} \<longleftrightarrow> (if a = 0 then r \<noteq> 0 else DIM('a) = 1)" |
|
11184 proof (simp add: bounded_hyperplane_eq_trivial_0, clarify) |
|
11185 assume "r \<noteq> 0" "a \<noteq> 0" |
|
11186 have "aff_dim {x. y \<bullet> x = 0} = aff_dim {x. a \<bullet> x = r}" if "y \<noteq> 0" for y::'a |
|
11187 by (metis that \<open>a \<noteq> 0\<close> aff_dim_hyperplane) |
|
11188 then show "bounded {x. a \<bullet> x = r} = (DIM('a) = Suc 0)" |
|
11189 by (metis One_nat_def \<open>a \<noteq> 0\<close> affine_bounded_eq_lowdim affine_hyperplane bounded_hyperplane_eq_trivial_0) |
|
11190 qed |
|
11191 |
|
11192 subsection\<open>General case without assuming closure and getting non-strict separation\<close> |
|
11193 |
|
11194 proposition separating_hyperplane_closed_point_inset: |
|
11195 fixes S :: "'a::euclidean_space set" |
|
11196 assumes "convex S" "closed S" "S \<noteq> {}" "z \<notin> S" |
|
11197 obtains a b where "a \<in> S" "(a - z) \<bullet> z < b" "\<And>x. x \<in> S \<Longrightarrow> b < (a - z) \<bullet> x" |
|
11198 proof - |
|
11199 obtain y where "y \<in> S" and y: "\<And>u. u \<in> S \<Longrightarrow> dist z y \<le> dist z u" |
|
11200 using distance_attains_inf [of S z] assms by auto |
|
11201 then have *: "(y - z) \<bullet> z < (y - z) \<bullet> z + (norm (y - z))\<^sup>2 / 2" |
|
11202 using \<open>y \<in> S\<close> \<open>z \<notin> S\<close> by auto |
|
11203 show ?thesis |
|
11204 proof (rule that [OF \<open>y \<in> S\<close> *]) |
|
11205 fix x |
|
11206 assume "x \<in> S" |
|
11207 have yz: "0 < (y - z) \<bullet> (y - z)" |
|
11208 using \<open>y \<in> S\<close> \<open>z \<notin> S\<close> by auto |
|
11209 { assume 0: "0 < ((z - y) \<bullet> (x - y))" |
|
11210 with any_closest_point_dot [OF \<open>convex S\<close> \<open>closed S\<close>] |
|
11211 have False |
|
11212 using y \<open>x \<in> S\<close> \<open>y \<in> S\<close> not_less by blast |
|
11213 } |
|
11214 then have "0 \<le> ((y - z) \<bullet> (x - y))" |
|
11215 by (force simp: not_less inner_diff_left) |
|
11216 with yz have "0 < 2 * ((y - z) \<bullet> (x - y)) + (y - z) \<bullet> (y - z)" |
|
11217 by (simp add: algebra_simps) |
|
11218 then show "(y - z) \<bullet> z + (norm (y - z))\<^sup>2 / 2 < (y - z) \<bullet> x" |
|
11219 by (simp add: field_simps inner_diff_left inner_diff_right dot_square_norm [symmetric]) |
|
11220 qed |
|
11221 qed |
|
11222 |
|
11223 lemma separating_hyperplane_closed_0_inset: |
|
11224 fixes S :: "'a::euclidean_space set" |
|
11225 assumes "convex S" "closed S" "S \<noteq> {}" "0 \<notin> S" |
|
11226 obtains a b where "a \<in> S" "a \<noteq> 0" "0 < b" "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> x > b" |
|
11227 using separating_hyperplane_closed_point_inset [OF assms] |
|
11228 by simp (metis \<open>0 \<notin> S\<close>) |
|
11229 |
|
11230 |
|
11231 proposition separating_hyperplane_set_0_inspan: |
|
11232 fixes S :: "'a::euclidean_space set" |
|
11233 assumes "convex S" "S \<noteq> {}" "0 \<notin> S" |
|
11234 obtains a where "a \<in> span S" "a \<noteq> 0" "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> a \<bullet> x" |
|
11235 proof - |
|
11236 def k \<equiv> "\<lambda>c::'a. {x. 0 \<le> c \<bullet> x}" |
|
11237 have *: "span S \<inter> frontier (cball 0 1) \<inter> \<Inter>f' \<noteq> {}" |
|
11238 if f': "finite f'" "f' \<subseteq> k ` S" for f' |
|
11239 proof - |
|
11240 obtain C where "C \<subseteq> S" "finite C" and C: "f' = k ` C" |
|
11241 using finite_subset_image [OF f'] by blast |
|
11242 obtain a where "a \<in> S" "a \<noteq> 0" |
|
11243 using \<open>S \<noteq> {}\<close> \<open>0 \<notin> S\<close> ex_in_conv by blast |
|
11244 then have "norm (a /\<^sub>R (norm a)) = 1" |
|
11245 by simp |
|
11246 moreover have "a /\<^sub>R (norm a) \<in> span S" |
|
11247 by (simp add: \<open>a \<in> S\<close> span_mul span_superset) |
|
11248 ultimately have ass: "a /\<^sub>R (norm a) \<in> span S \<inter> sphere 0 1" |
|
11249 by simp |
|
11250 show ?thesis |
|
11251 proof (cases "C = {}") |
|
11252 case True with C ass show ?thesis |
|
11253 by auto |
|
11254 next |
|
11255 case False |
|
11256 have "closed (convex hull C)" |
|
11257 using \<open>finite C\<close> compact_eq_bounded_closed finite_imp_compact_convex_hull by auto |
|
11258 moreover have "convex hull C \<noteq> {}" |
|
11259 by (simp add: False) |
|
11260 moreover have "0 \<notin> convex hull C" |
|
11261 by (metis \<open>C \<subseteq> S\<close> \<open>convex S\<close> \<open>0 \<notin> S\<close> convex_hull_subset hull_same insert_absorb insert_subset) |
|
11262 ultimately obtain a b |
|
11263 where "a \<in> convex hull C" "a \<noteq> 0" "0 < b" |
|
11264 and ab: "\<And>x. x \<in> convex hull C \<Longrightarrow> a \<bullet> x > b" |
|
11265 using separating_hyperplane_closed_0_inset by blast |
|
11266 then have "a \<in> S" |
|
11267 by (metis \<open>C \<subseteq> S\<close> assms(1) subsetCE subset_hull) |
|
11268 moreover have "norm (a /\<^sub>R (norm a)) = 1" |
|
11269 using \<open>a \<noteq> 0\<close> by simp |
|
11270 moreover have "a /\<^sub>R (norm a) \<in> span S" |
|
11271 by (simp add: \<open>a \<in> S\<close> span_mul span_superset) |
|
11272 ultimately have ass: "a /\<^sub>R (norm a) \<in> span S \<inter> sphere 0 1" |
|
11273 by simp |
|
11274 have aa: "a /\<^sub>R (norm a) \<in> (\<Inter>c\<in>C. {x. 0 \<le> c \<bullet> x})" |
|
11275 apply (clarsimp simp add: divide_simps) |
|
11276 using ab \<open>0 < b\<close> |
|
11277 by (metis hull_inc inner_commute less_eq_real_def less_trans) |
|
11278 show ?thesis |
|
11279 apply (simp add: C k_def) |
|
11280 using ass aa Int_iff empty_iff by blast |
|
11281 qed |
|
11282 qed |
|
11283 have "(span S \<inter> frontier(cball 0 1)) \<inter> (\<Inter> (k ` S)) \<noteq> {}" |
|
11284 apply (rule compact_imp_fip) |
|
11285 apply (blast intro: compact_cball) |
|
11286 using closed_halfspace_ge k_def apply blast |
|
11287 apply (metis *) |
|
11288 done |
|
11289 then show ?thesis |
|
11290 unfolding set_eq_iff k_def |
|
11291 by simp (metis inner_commute norm_eq_zero that zero_neq_one) |
|
11292 qed |
|
11293 |
|
11294 |
|
11295 lemma separating_hyperplane_set_point_inaff: |
|
11296 fixes S :: "'a::euclidean_space set" |
|
11297 assumes "convex S" "S \<noteq> {}" and zno: "z \<notin> S" |
|
11298 obtains a b where "(z + a) \<in> affine hull (insert z S)" |
|
11299 and "a \<noteq> 0" and "a \<bullet> z \<le> b" |
|
11300 and "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b" |
|
11301 proof - |
|
11302 from separating_hyperplane_set_0_inspan [of "image (\<lambda>x. -z + x) S"] |
|
11303 have "convex (op + (- z) ` S)" |
|
11304 by (simp add: \<open>convex S\<close>) |
|
11305 moreover have "op + (- z) ` S \<noteq> {}" |
|
11306 by (simp add: \<open>S \<noteq> {}\<close>) |
|
11307 moreover have "0 \<notin> op + (- z) ` S" |
|
11308 using zno by auto |
|
11309 ultimately obtain a where "a \<in> span (op + (- z) ` S)" "a \<noteq> 0" |
|
11310 and a: "\<And>x. x \<in> (op + (- z) ` S) \<Longrightarrow> 0 \<le> a \<bullet> x" |
|
11311 using separating_hyperplane_set_0_inspan [of "image (\<lambda>x. -z + x) S"] |
|
11312 by blast |
|
11313 then have szx: "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> z \<le> a \<bullet> x" |
|
11314 by (metis (no_types, lifting) imageI inner_minus_right inner_right_distrib minus_add neg_le_0_iff_le neg_le_iff_le real_add_le_0_iff) |
|
11315 show ?thesis |
|
11316 apply (rule_tac a=a and b = "a \<bullet> z" in that, simp_all) |
|
11317 using \<open>a \<in> span (op + (- z) ` S)\<close> affine_hull_insert_span_gen apply blast |
|
11318 apply (simp_all add: \<open>a \<noteq> 0\<close> szx) |
|
11319 done |
|
11320 qed |
|
11321 |
|
11322 proposition supporting_hyperplane_relative_boundary: |
|
11323 fixes S :: "'a::euclidean_space set" |
|
11324 assumes "convex S" "x \<in> S" and xno: "x \<notin> rel_interior S" |
|
11325 obtains a where "a \<noteq> 0" |
|
11326 and "\<And>y. y \<in> S \<Longrightarrow> a \<bullet> x \<le> a \<bullet> y" |
|
11327 and "\<And>y. y \<in> rel_interior S \<Longrightarrow> a \<bullet> x < a \<bullet> y" |
|
11328 proof - |
|
11329 obtain a b where aff: "(x + a) \<in> affine hull (insert x (rel_interior S))" |
|
11330 and "a \<noteq> 0" and "a \<bullet> x \<le> b" |
|
11331 and ageb: "\<And>u. u \<in> (rel_interior S) \<Longrightarrow> a \<bullet> u \<ge> b" |
|
11332 using separating_hyperplane_set_point_inaff [of "rel_interior S" x] assms |
|
11333 by (auto simp: rel_interior_eq_empty convex_rel_interior) |
|
11334 have le_ay: "a \<bullet> x \<le> a \<bullet> y" if "y \<in> S" for y |
|
11335 proof - |
|
11336 have con: "continuous_on (closure (rel_interior S)) (op \<bullet> a)" |
|
11337 by (rule continuous_intros continuous_on_subset | blast)+ |
|
11338 have y: "y \<in> closure (rel_interior S)" |
|
11339 using \<open>convex S\<close> closure_def convex_closure_rel_interior \<open>y \<in> S\<close> |
|
11340 by fastforce |
|
11341 show ?thesis |
|
11342 using continuous_ge_on_closure [OF con y] ageb \<open>a \<bullet> x \<le> b\<close> |
|
11343 by fastforce |
|
11344 qed |
|
11345 have 3: "a \<bullet> x < a \<bullet> y" if "y \<in> rel_interior S" for y |
|
11346 proof - |
|
11347 obtain e where "0 < e" "y \<in> S" and e: "cball y e \<inter> affine hull S \<subseteq> S" |
|
11348 using \<open>y \<in> rel_interior S\<close> by (force simp: rel_interior_cball) |
|
11349 def y' \<equiv> "y - (e / norm a) *\<^sub>R ((x + a) - x)" |
|
11350 have "y' \<in> cball y e" |
|
11351 unfolding y'_def using \<open>0 < e\<close> by force |
|
11352 moreover have "y' \<in> affine hull S" |
|
11353 unfolding y'_def |
|
11354 by (metis \<open>x \<in> S\<close> \<open>y \<in> S\<close> \<open>convex S\<close> aff affine_affine_hull hull_redundant |
|
11355 rel_interior_same_affine_hull hull_inc mem_affine_3_minus2) |
|
11356 ultimately have "y' \<in> S" |
|
11357 using e by auto |
|
11358 have "a \<bullet> x \<le> a \<bullet> y" |
|
11359 using le_ay \<open>a \<noteq> 0\<close> \<open>y \<in> S\<close> by blast |
|
11360 moreover have "a \<bullet> x \<noteq> a \<bullet> y" |
|
11361 using le_ay [OF \<open>y' \<in> S\<close>] \<open>a \<noteq> 0\<close> |
|
11362 apply (simp add: y'_def inner_diff dot_square_norm power2_eq_square) |
|
11363 by (metis \<open>0 < e\<close> add_le_same_cancel1 inner_commute inner_real_def inner_zero_left le_diff_eq norm_le_zero_iff real_mult_le_cancel_iff2) |
|
11364 ultimately show ?thesis by force |
|
11365 qed |
|
11366 show ?thesis |
|
11367 by (rule that [OF \<open>a \<noteq> 0\<close> le_ay 3]) |
|
11368 qed |
|
11369 |
|
11370 lemma supporting_hyperplane_relative_frontier: |
|
11371 fixes S :: "'a::euclidean_space set" |
|
11372 assumes "convex S" "x \<in> closure S" "x \<notin> rel_interior S" |
|
11373 obtains a where "a \<noteq> 0" |
|
11374 and "\<And>y. y \<in> closure S \<Longrightarrow> a \<bullet> x \<le> a \<bullet> y" |
|
11375 and "\<And>y. y \<in> rel_interior S \<Longrightarrow> a \<bullet> x < a \<bullet> y" |
|
11376 using supporting_hyperplane_relative_boundary [of "closure S" x] |
|
11377 by (metis assms convex_closure convex_rel_interior_closure) |
|
11378 |
|
11379 subsection\<open> Some results on decomposing convex hulls, e.g. simplicial subdivision\<close> |
|
11380 |
|
11381 lemma |
|
11382 fixes s :: "'a::euclidean_space set" |
|
11383 assumes "~ (affine_dependent(s \<union> t))" |
|
11384 shows convex_hull_Int_subset: "convex hull s \<inter> convex hull t \<subseteq> convex hull (s \<inter> t)" (is ?C) |
|
11385 and affine_hull_Int_subset: "affine hull s \<inter> affine hull t \<subseteq> affine hull (s \<inter> t)" (is ?A) |
|
11386 proof - |
|
11387 have [simp]: "finite s" "finite t" |
|
11388 using aff_independent_finite assms by blast+ |
|
11389 have "setsum u (s \<inter> t) = 1 \<and> |
|
11390 (\<Sum>v\<in>s \<inter> t. u v *\<^sub>R v) = (\<Sum>v\<in>s. u v *\<^sub>R v)" |
|
11391 if [simp]: "setsum u s = 1" |
|
11392 "setsum v t = 1" |
|
11393 and eq: "(\<Sum>x\<in>t. v x *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x)" for u v |
|
11394 proof - |
|
11395 def f \<equiv> "\<lambda>x. (if x \<in> s then u x else 0) - (if x \<in> t then v x else 0)" |
|
11396 have "setsum f (s \<union> t) = 0" |
|
11397 apply (simp add: f_def setsum_Un setsum_subtractf) |
|
11398 apply (simp add: setsum.inter_restrict [symmetric] Int_commute) |
|
11399 done |
|
11400 moreover have "(\<Sum>x\<in>(s \<union> t). f x *\<^sub>R x) = 0" |
|
11401 apply (simp add: f_def setsum_Un scaleR_left_diff_distrib setsum_subtractf) |
|
11402 apply (simp add: if_smult setsum.inter_restrict [symmetric] Int_commute eq cong del: if_cong) |
|
11403 done |
|
11404 ultimately have "\<And>v. v \<in> s \<union> t \<Longrightarrow> f v = 0" |
|
11405 using aff_independent_finite assms unfolding affine_dependent_explicit |
|
11406 by blast |
|
11407 then have u [simp]: "\<And>x. x \<in> s \<Longrightarrow> u x = (if x \<in> t then v x else 0)" |
|
11408 by (simp add: f_def) presburger |
|
11409 have "setsum u (s \<inter> t) = setsum u s" |
|
11410 by (simp add: setsum.inter_restrict) |
|
11411 then have "setsum u (s \<inter> t) = 1" |
|
11412 using that by linarith |
|
11413 moreover have "(\<Sum>v\<in>s \<inter> t. u v *\<^sub>R v) = (\<Sum>v\<in>s. u v *\<^sub>R v)" |
|
11414 by (auto simp: if_smult setsum.inter_restrict intro: setsum.cong) |
|
11415 ultimately show ?thesis |
|
11416 by force |
|
11417 qed |
|
11418 then show ?A ?C |
|
11419 by (auto simp: convex_hull_finite affine_hull_finite) |
|
11420 qed |
|
11421 |
|
11422 |
|
11423 proposition affine_hull_Int: |
|
11424 fixes s :: "'a::euclidean_space set" |
|
11425 assumes "~ (affine_dependent(s \<union> t))" |
|
11426 shows "affine hull (s \<inter> t) = affine hull s \<inter> affine hull t" |
|
11427 apply (rule subset_antisym) |
|
11428 apply (simp add: hull_mono) |
|
11429 by (simp add: affine_hull_Int_subset assms) |
|
11430 |
|
11431 proposition convex_hull_Int: |
|
11432 fixes s :: "'a::euclidean_space set" |
|
11433 assumes "~ (affine_dependent(s \<union> t))" |
|
11434 shows "convex hull (s \<inter> t) = convex hull s \<inter> convex hull t" |
|
11435 apply (rule subset_antisym) |
|
11436 apply (simp add: hull_mono) |
|
11437 by (simp add: convex_hull_Int_subset assms) |
|
11438 |
|
11439 proposition |
|
11440 fixes s :: "'a::euclidean_space set set" |
|
11441 assumes "~ (affine_dependent (\<Union>s))" |
|
11442 shows affine_hull_Inter: "affine hull (\<Inter>s) = (\<Inter>t\<in>s. affine hull t)" (is "?A") |
|
11443 and convex_hull_Inter: "convex hull (\<Inter>s) = (\<Inter>t\<in>s. convex hull t)" (is "?C") |
|
11444 proof - |
|
11445 have "finite s" |
|
11446 using aff_independent_finite assms finite_UnionD by blast |
|
11447 then have "?A \<and> ?C" using assms |
|
11448 proof (induction s rule: finite_induct) |
|
11449 case empty then show ?case by auto |
|
11450 next |
|
11451 case (insert t F) |
|
11452 then show ?case |
|
11453 proof (cases "F={}") |
|
11454 case True then show ?thesis by simp |
|
11455 next |
|
11456 case False |
|
11457 with "insert.prems" have [simp]: "\<not> affine_dependent (t \<union> \<Inter>F)" |
|
11458 by (auto intro: affine_dependent_subset) |
|
11459 have [simp]: "\<not> affine_dependent (\<Union>F)" |
|
11460 using affine_independent_subset insert.prems by fastforce |
|
11461 show ?thesis |
|
11462 by (simp add: affine_hull_Int convex_hull_Int insert.IH) |
|
11463 qed |
|
11464 qed |
|
11465 then show "?A" "?C" |
|
11466 by auto |
|
11467 qed |
|
11468 |
|
11469 lemma affine_hull_finite_intersection_hyperplanes: |
|
11470 fixes s :: "'a::euclidean_space set" |
|
11471 obtains f where |
|
11472 "finite f" |
|
11473 "of_nat (card f) + aff_dim s = DIM('a)" |
|
11474 "affine hull s = \<Inter>f" |
|
11475 "\<And>h. h \<in> f \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x = b}" |
|
11476 proof - |
|
11477 obtain b where "b \<subseteq> s" |
|
11478 and indb: "\<not> affine_dependent b" |
|
11479 and eq: "affine hull s = affine hull b" |
|
11480 using affine_basis_exists by blast |
|
11481 obtain c where indc: "\<not> affine_dependent c" and "b \<subseteq> c" |
|
11482 and affc: "affine hull c = UNIV" |
|
11483 by (metis extend_to_affine_basis affine_UNIV hull_same indb subset_UNIV) |
|
11484 then have "finite c" |
|
11485 by (simp add: aff_independent_finite) |
|
11486 then have fbc: "finite b" "card b \<le> card c" |
|
11487 using \<open>b \<subseteq> c\<close> infinite_super by (auto simp: card_mono) |
|
11488 have imeq: "(\<lambda>x. affine hull x) ` ((\<lambda>a. c - {a}) ` (c - b)) = ((\<lambda>a. affine hull (c - {a})) ` (c - b))" |
|
11489 by blast |
|
11490 have card1: "card ((\<lambda>a. affine hull (c - {a})) ` (c - b)) = card (c - b)" |
|
11491 apply (rule card_image [OF inj_onI]) |
|
11492 by (metis Diff_eq_empty_iff Diff_iff indc affine_dependent_def hull_subset insert_iff) |
|
11493 have card2: "(card (c - b)) + aff_dim s = DIM('a)" |
|
11494 proof - |
|
11495 have aff: "aff_dim (UNIV::'a set) = aff_dim c" |
|
11496 by (metis aff_dim_affine_hull affc) |
|
11497 have "aff_dim b = aff_dim s" |
|
11498 by (metis (no_types) aff_dim_affine_hull eq) |
|
11499 then have "int (card b) = 1 + aff_dim s" |
|
11500 by (simp add: aff_dim_affine_independent indb) |
|
11501 then show ?thesis |
|
11502 using fbc aff |
|
11503 by (simp add: \<open>\<not> affine_dependent c\<close> \<open>b \<subseteq> c\<close> aff_dim_affine_independent aff_dim_univ card_Diff_subset of_nat_diff) |
|
11504 qed |
|
11505 show ?thesis |
|
11506 proof (cases "c = b") |
|
11507 case True show ?thesis |
|
11508 apply (rule_tac f="{}" in that) |
|
11509 using True affc |
|
11510 apply (simp_all add: eq [symmetric]) |
|
11511 by (metis aff_dim_univ aff_dim_affine_hull) |
|
11512 next |
|
11513 case False |
|
11514 have ind: "\<not> affine_dependent (\<Union>a\<in>c - b. c - {a})" |
|
11515 by (rule affine_independent_subset [OF indc]) auto |
|
11516 have affeq: "affine hull s = (\<Inter>x\<in>(\<lambda>a. c - {a}) ` (c - b). affine hull x)" |
|
11517 using \<open>b \<subseteq> c\<close> False |
|
11518 apply (subst affine_hull_Inter [OF ind, symmetric]) |
|
11519 apply (simp add: eq double_diff) |
|
11520 done |
|
11521 have *: "1 + aff_dim (c - {t}) = int (DIM('a))" |
|
11522 if t: "t \<in> c" for t |
|
11523 proof - |
|
11524 have "insert t c = c" |
|
11525 using t by blast |
|
11526 then show ?thesis |
|
11527 by (metis (full_types) add.commute aff_dim_affine_hull aff_dim_insert aff_dim_univ affc affine_dependent_def indc insert_Diff_single t) |
|
11528 qed |
|
11529 show ?thesis |
|
11530 apply (rule_tac f = "(\<lambda>x. affine hull x) ` ((\<lambda>a. c - {a}) ` (c - b))" in that) |
|
11531 using \<open>finite c\<close> apply blast |
|
11532 apply (simp add: imeq card1 card2) |
|
11533 apply (simp add: affeq, clarify) |
|
11534 apply (metis DIM_positive One_nat_def Suc_leI add_diff_cancel_left' of_nat_1 aff_dim_eq_hyperplane of_nat_diff *) |
|
11535 done |
|
11536 qed |
|
11537 qed |
|
11538 |
10665 end |
11539 end |