662 |
662 |
663 lemma convex_affinity: |
663 lemma convex_affinity: |
664 assumes "convex S" |
664 assumes "convex S" |
665 shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` S)" |
665 shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` S)" |
666 proof - |
666 proof - |
667 have "(\<lambda>x. a + c *\<^sub>R x) ` S = (+) a ` ( *\<^sub>R) c ` S" |
667 have "(\<lambda>x. a + c *\<^sub>R x) ` S = (+) a ` (*\<^sub>R) c ` S" |
668 by auto |
668 by auto |
669 then show ?thesis |
669 then show ?thesis |
670 using convex_translation[OF convex_scaling[OF assms], of a c] by auto |
670 using convex_translation[OF convex_scaling[OF assms], of a c] by auto |
671 qed |
671 qed |
672 |
672 |
1227 apply (rule closure_minimal, simp add: closure_subset image_mono) |
1227 apply (rule closure_minimal, simp add: closure_subset image_mono) |
1228 by (meson bounded_closure closed_closure compact_continuous_image compact_eq_bounded_closed linear_continuous_on linear_conv_bounded_linear) |
1228 by (meson bounded_closure closed_closure compact_continuous_image compact_eq_bounded_closed linear_continuous_on linear_conv_bounded_linear) |
1229 |
1229 |
1230 lemma closure_scaleR: |
1230 lemma closure_scaleR: |
1231 fixes S :: "'a::real_normed_vector set" |
1231 fixes S :: "'a::real_normed_vector set" |
1232 shows "(( *\<^sub>R) c) ` (closure S) = closure ((( *\<^sub>R) c) ` S)" |
1232 shows "((*\<^sub>R) c) ` (closure S) = closure (((*\<^sub>R) c) ` S)" |
1233 proof |
1233 proof |
1234 show "(( *\<^sub>R) c) ` (closure S) \<subseteq> closure ((( *\<^sub>R) c) ` S)" |
1234 show "((*\<^sub>R) c) ` (closure S) \<subseteq> closure (((*\<^sub>R) c) ` S)" |
1235 using bounded_linear_scaleR_right |
1235 using bounded_linear_scaleR_right |
1236 by (rule closure_bounded_linear_image_subset) |
1236 by (rule closure_bounded_linear_image_subset) |
1237 show "closure ((( *\<^sub>R) c) ` S) \<subseteq> (( *\<^sub>R) c) ` (closure S)" |
1237 show "closure (((*\<^sub>R) c) ` S) \<subseteq> ((*\<^sub>R) c) ` (closure S)" |
1238 by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure) |
1238 by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure) |
1239 qed |
1239 qed |
1240 |
1240 |
1241 lemma fst_linear: "linear fst" |
1241 lemma fst_linear: "linear fst" |
1242 unfolding linear_iff by (simp add: algebra_simps) |
1242 unfolding linear_iff by (simp add: algebra_simps) |
1943 lemma cone_Union[intro]: "(\<forall>s\<in>f. cone s) \<longrightarrow> cone (\<Union>f)" |
1943 lemma cone_Union[intro]: "(\<forall>s\<in>f. cone s) \<longrightarrow> cone (\<Union>f)" |
1944 unfolding cone_def by blast |
1944 unfolding cone_def by blast |
1945 |
1945 |
1946 lemma cone_iff: |
1946 lemma cone_iff: |
1947 assumes "S \<noteq> {}" |
1947 assumes "S \<noteq> {}" |
1948 shows "cone S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (( *\<^sub>R) c) ` S = S)" |
1948 shows "cone S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)" |
1949 proof - |
1949 proof - |
1950 { |
1950 { |
1951 assume "cone S" |
1951 assume "cone S" |
1952 { |
1952 { |
1953 fix c :: real |
1953 fix c :: real |
1954 assume "c > 0" |
1954 assume "c > 0" |
1955 { |
1955 { |
1956 fix x |
1956 fix x |
1957 assume "x \<in> S" |
1957 assume "x \<in> S" |
1958 then have "x \<in> (( *\<^sub>R) c) ` S" |
1958 then have "x \<in> ((*\<^sub>R) c) ` S" |
1959 unfolding image_def |
1959 unfolding image_def |
1960 using \<open>cone S\<close> \<open>c>0\<close> mem_cone[of S x "1/c"] |
1960 using \<open>cone S\<close> \<open>c>0\<close> mem_cone[of S x "1/c"] |
1961 exI[of "(\<lambda>t. t \<in> S \<and> x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"] |
1961 exI[of "(\<lambda>t. t \<in> S \<and> x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"] |
1962 by auto |
1962 by auto |
1963 } |
1963 } |
1964 moreover |
1964 moreover |
1965 { |
1965 { |
1966 fix x |
1966 fix x |
1967 assume "x \<in> (( *\<^sub>R) c) ` S" |
1967 assume "x \<in> ((*\<^sub>R) c) ` S" |
1968 then have "x \<in> S" |
1968 then have "x \<in> S" |
1969 using \<open>cone S\<close> \<open>c > 0\<close> |
1969 using \<open>cone S\<close> \<open>c > 0\<close> |
1970 unfolding cone_def image_def \<open>c > 0\<close> by auto |
1970 unfolding cone_def image_def \<open>c > 0\<close> by auto |
1971 } |
1971 } |
1972 ultimately have "(( *\<^sub>R) c) ` S = S" by auto |
1972 ultimately have "((*\<^sub>R) c) ` S = S" by auto |
1973 } |
1973 } |
1974 then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (( *\<^sub>R) c) ` S = S)" |
1974 then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)" |
1975 using \<open>cone S\<close> cone_contains_0[of S] assms by auto |
1975 using \<open>cone S\<close> cone_contains_0[of S] assms by auto |
1976 } |
1976 } |
1977 moreover |
1977 moreover |
1978 { |
1978 { |
1979 assume a: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (( *\<^sub>R) c) ` S = S)" |
1979 assume a: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)" |
1980 { |
1980 { |
1981 fix x |
1981 fix x |
1982 assume "x \<in> S" |
1982 assume "x \<in> S" |
1983 fix c1 :: real |
1983 fix c1 :: real |
1984 assume "c1 \<ge> 0" |
1984 assume "c1 \<ge> 0" |
2059 proof (cases "S = {}") |
2059 proof (cases "S = {}") |
2060 case True |
2060 case True |
2061 then show ?thesis by auto |
2061 then show ?thesis by auto |
2062 next |
2062 next |
2063 case False |
2063 case False |
2064 then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)" |
2064 then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)" |
2065 using cone_iff[of S] assms by auto |
2065 using cone_iff[of S] assms by auto |
2066 then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` closure S = closure S)" |
2066 then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` closure S = closure S)" |
2067 using closure_subset by (auto simp: closure_scaleR) |
2067 using closure_subset by (auto simp: closure_scaleR) |
2068 then show ?thesis |
2068 then show ?thesis |
2069 using False cone_iff[of "closure S"] by auto |
2069 using False cone_iff[of "closure S"] by auto |
2070 qed |
2070 qed |
2071 |
2071 |
5703 proof (cases "S = {}") |
5703 proof (cases "S = {}") |
5704 case True |
5704 case True |
5705 then show ?thesis by auto |
5705 then show ?thesis by auto |
5706 next |
5706 next |
5707 case False |
5707 case False |
5708 then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)" |
5708 then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)" |
5709 using cone_iff[of S] assms by auto |
5709 using cone_iff[of S] assms by auto |
5710 { |
5710 { |
5711 fix c :: real |
5711 fix c :: real |
5712 assume "c > 0" |
5712 assume "c > 0" |
5713 then have "( *\<^sub>R) c ` (convex hull S) = convex hull (( *\<^sub>R) c ` S)" |
5713 then have "(*\<^sub>R) c ` (convex hull S) = convex hull ((*\<^sub>R) c ` S)" |
5714 using convex_hull_scaling[of _ S] by auto |
5714 using convex_hull_scaling[of _ S] by auto |
5715 also have "\<dots> = convex hull S" |
5715 also have "\<dots> = convex hull S" |
5716 using * \<open>c > 0\<close> by auto |
5716 using * \<open>c > 0\<close> by auto |
5717 finally have "( *\<^sub>R) c ` (convex hull S) = convex hull S" |
5717 finally have "(*\<^sub>R) c ` (convex hull S) = convex hull S" |
5718 by auto |
5718 by auto |
5719 } |
5719 } |
5720 then have "0 \<in> convex hull S" "\<And>c. c > 0 \<Longrightarrow> (( *\<^sub>R) c ` (convex hull S)) = (convex hull S)" |
5720 then have "0 \<in> convex hull S" "\<And>c. c > 0 \<Longrightarrow> ((*\<^sub>R) c ` (convex hull S)) = (convex hull S)" |
5721 using * hull_subset[of S convex] by auto |
5721 using * hull_subset[of S convex] by auto |
5722 then show ?thesis |
5722 then show ?thesis |
5723 using \<open>S \<noteq> {}\<close> cone_iff[of "convex hull S"] by auto |
5723 using \<open>S \<noteq> {}\<close> cone_iff[of "convex hull S"] by auto |
5724 qed |
5724 qed |
5725 |
5725 |
6401 proof (intro set_eqI iffI) |
6401 proof (intro set_eqI iffI) |
6402 fix y |
6402 fix y |
6403 assume "y \<in> cbox (x - ?d) (x + ?d)" |
6403 assume "y \<in> cbox (x - ?d) (x + ?d)" |
6404 then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)" |
6404 then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)" |
6405 using assms by (simp add: mem_box field_simps inner_simps) |
6405 using assms by (simp add: mem_box field_simps inner_simps) |
6406 with \<open>0 < d\<close> show "y \<in> (\<lambda>y. x - sum (( *\<^sub>R) d) Basis + (2 * d) *\<^sub>R y) ` cbox 0 One" |
6406 with \<open>0 < d\<close> show "y \<in> (\<lambda>y. x - sum ((*\<^sub>R) d) Basis + (2 * d) *\<^sub>R y) ` cbox 0 One" |
6407 by (auto intro: image_eqI[where x= "inverse (2 * d) *\<^sub>R (y - (x - ?d))"]) |
6407 by (auto intro: image_eqI[where x= "inverse (2 * d) *\<^sub>R (y - (x - ?d))"]) |
6408 next |
6408 next |
6409 fix y |
6409 fix y |
6410 assume "y \<in> (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` cbox 0 One" |
6410 assume "y \<in> (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` cbox 0 One" |
6411 then obtain z where z: "z \<in> cbox 0 One" "y = x - ?d + (2*d) *\<^sub>R z" |
6411 then obtain z where z: "z \<in> cbox 0 One" "y = x - ?d + (2*d) *\<^sub>R z" |