author wenzelm Thu, 27 Feb 2014 17:24:46 +0100 changeset 55787 41a73a41f6c8 parent 55786 96861130f922 child 55788 67699e08e969
more symbols;
```--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Feb 27 17:24:16 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Feb 27 17:24:46 2014 +0100
@@ -8137,7 +8137,7 @@
then have "rel_interior (S \<times> T) = rel_interior ((S \<times> (UNIV :: 'm set)) \<inter> ((UNIV :: 'n set) \<times> T))"
by auto
also have "\<dots> = rel_interior (S \<times> (UNIV :: 'm set)) \<inter> rel_interior ((UNIV :: 'n set) \<times> T)"
-       apply (subst convex_rel_interior_inter_two[of "S \<times> (UNIV :: 'm set)" "(UNIV :: 'n set) <*> T"])
+       apply (subst convex_rel_interior_inter_two[of "S \<times> (UNIV :: 'm set)" "(UNIV :: 'n set) \<times> T"])
using * ri assms convex_Times
apply auto
done
@@ -8338,7 +8338,7 @@
lemma rel_interior_convex_cone_aux:
fixes S :: "'m::euclidean_space set"
assumes "convex S"
-  shows "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} <*> S)) \<longleftrightarrow>
+  shows "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} \<times> S)) \<longleftrightarrow>
c > 0 \<and> x \<in> ((op *\<^sub>R c) ` (rel_interior S))"
proof (cases "S = {}")
case True
@@ -8347,33 +8347,33 @@
next
case False
then obtain s where "s \<in> S" by auto
-  have conv: "convex ({(1 :: real)} <*> S)"
+  have conv: "convex ({(1 :: real)} \<times> S)"
using convex_Times[of "{(1 :: real)}" S] assms convex_singleton[of "1 :: real"]
by auto
-  def f \<equiv> "\<lambda>y. {z. (y, z) \<in> cone hull ({1 :: real} <*> S)}"
-  then have *: "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} <*> S)) =
+  def f \<equiv> "\<lambda>y. {z. (y, z) \<in> cone hull ({1 :: real} \<times> S)}"
+  then have *: "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} \<times> S)) =
(c \<in> rel_interior {y. f y \<noteq> {}} \<and> x \<in> rel_interior (f c))"
-    apply (subst rel_interior_projection[of "cone hull ({(1 :: real)} <*> S)" f c x])
-    using convex_cone_hull[of "{(1 :: real)} <*> S"] conv
+    apply (subst rel_interior_projection[of "cone hull ({(1 :: real)} \<times> S)" f c x])
+    using convex_cone_hull[of "{(1 :: real)} \<times> S"] conv
apply auto
done
{
fix y :: real
assume "y \<ge> 0"
-    then have "y *\<^sub>R (1,s) \<in> cone hull ({1 :: real} <*> S)"
-      using cone_hull_expl[of "{(1 :: real)} <*> S"] `s \<in> S` by auto
+    then have "y *\<^sub>R (1,s) \<in> cone hull ({1 :: real} \<times> S)"
+      using cone_hull_expl[of "{(1 :: real)} \<times> S"] `s \<in> S` by auto
then have "f y \<noteq> {}"
using f_def by auto
}
then have "{y. f y \<noteq> {}} = {0..}"
-    using f_def cone_hull_expl[of "{1 :: real} <*> S"] by auto
+    using f_def cone_hull_expl[of "{1 :: real} \<times> S"] by auto
then have **: "rel_interior {y. f y \<noteq> {}} = {0<..}"
using rel_interior_real_semiline by auto
{
fix c :: real
assume "c > 0"
then have "f c = (op *\<^sub>R c ` S)"
-      using f_def cone_hull_expl[of "{1 :: real} <*> S"] by auto
+      using f_def cone_hull_expl[of "{1 :: real} \<times> S"] by auto
then have "rel_interior (f c) = op *\<^sub>R c ` rel_interior S"
using rel_interior_convex_scaleR[of S c] assms by auto
}
@@ -8383,7 +8383,7 @@
lemma rel_interior_convex_cone:
fixes S :: "'m::euclidean_space set"
assumes "convex S"
-  shows "rel_interior (cone hull ({1 :: real} <*> S)) =
+  shows "rel_interior (cone hull ({1 :: real} \<times> S)) =
{(c, c *\<^sub>R x) | c x. c > 0 \<and> x \<in> rel_interior S}"
(is "?lhs = ?rhs")
proof -
@@ -8621,13 +8621,13 @@
fixes S T :: "'n::euclidean_space set"
shows "convex hull (S + T) = convex hull S + convex hull T"
proof -
-  have "convex hull S + convex hull T = (\<lambda>(x,y). x + y) ` ((convex hull S) <*> (convex hull T))"
+  have "convex hull S + convex hull T = (\<lambda>(x,y). x + y) ` ((convex hull S) \<times> (convex hull T))"
-  also have "\<dots> = (\<lambda>(x,y). x + y) ` (convex hull (S <*> T))"
+  also have "\<dots> = (\<lambda>(x,y). x + y) ` (convex hull (S \<times> T))"
using convex_hull_Times by auto
also have "\<dots> = convex hull (S + T)"
using fst_snd_linear linear_conv_bounded_linear
-      convex_hull_linear_image[of "(\<lambda>(x,y). x + y)" "S <*> T"]
+      convex_hull_linear_image[of "(\<lambda>(x,y). x + y)" "S \<times> T"]
finally show ?thesis ..
qed
@@ -8638,13 +8638,13 @@
and "convex T"
shows "rel_interior (S + T) = rel_interior S + rel_interior T"
proof -
-  have "rel_interior S + rel_interior T = (\<lambda>(x,y). x + y) ` (rel_interior S <*> rel_interior T)"
+  have "rel_interior S + rel_interior T = (\<lambda>(x,y). x + y) ` (rel_interior S \<times> rel_interior T)"
-  also have "\<dots> = (\<lambda>(x,y). x + y) ` rel_interior (S <*> T)"
+  also have "\<dots> = (\<lambda>(x,y). x + y) ` rel_interior (S \<times> T)"
using rel_interior_direct_sum assms by auto
also have "\<dots> = rel_interior (S + T)"
using fst_snd_linear convex_Times assms
-      rel_interior_convex_linear_image[of "(\<lambda>(x,y). x + y)" "S <*> T"]
+      rel_interior_convex_linear_image[of "(\<lambda>(x,y). x + y)" "S \<times> T"]
finally show ?thesis ..
qed
@@ -8685,7 +8685,7 @@
and "rel_open S"
and "convex T"
and "rel_open T"
-  shows "convex (S <*> T) \<and> rel_open (S <*> T)"
+  shows "convex (S \<times> T) \<and> rel_open (S \<times> T)"
by (metis assms convex_Times rel_interior_direct_sum rel_open_def)

lemma convex_rel_open_sum:
@@ -8799,8 +8799,8 @@
def C0 \<equiv> "convex hull (\<Union>(S ` I))"
have "\<forall>i\<in>I. C0 \<ge> S i"
unfolding C0_def using hull_subset[of "\<Union>(S ` I)"] by auto
-  def K0 \<equiv> "cone hull ({1 :: real} <*> C0)"
-  def K \<equiv> "\<lambda>i. cone hull ({1 :: real} <*> S i)"
+  def K0 \<equiv> "cone hull ({1 :: real} \<times> C0)"
+  def K \<equiv> "\<lambda>i. cone hull ({1 :: real} \<times> S i)"
have "\<forall>i\<in>I. K i \<noteq> {}"
unfolding K_def using assms
@@ -8838,13 +8838,13 @@
done
ultimately have geq: "K0 \<supseteq> convex hull (\<Union>(K ` I))"
using hull_minimal[of _ "K0" "convex"] by blast
-  have "\<forall>i\<in>I. K i \<supseteq> {1 :: real} <*> S i"
+  have "\<forall>i\<in>I. K i \<supseteq> {1 :: real} \<times> S i"
using K_def by (simp add: hull_subset)
-  then have "\<Union>(K ` I) \<supseteq> {1 :: real} <*> \<Union>(S ` I)"
+  then have "\<Union>(K ` I) \<supseteq> {1 :: real} \<times> \<Union>(S ` I)"
by auto
-  then have "convex hull \<Union>(K ` I) \<supseteq> convex hull ({1 :: real} <*> \<Union>(S ` I))"
+  then have "convex hull \<Union>(K ` I) \<supseteq> convex hull ({1 :: real} \<times> \<Union>(S ` I))"
-  then have "convex hull \<Union>(K ` I) \<supseteq> {1 :: real} <*> C0"
+  then have "convex hull \<Union>(K ` I) \<supseteq> {1 :: real} \<times> C0"
unfolding C0_def
using convex_hull_Times[of "{(1 :: real)}" "\<Union>(S ` I)"] convex_hull_singleton
by auto
@@ -8889,7 +8889,7 @@
{
fix i
assume "i \<in> I"
-      then have "convex (S i) \<and> k i \<in> rel_interior (cone hull {1} <*> S i)"
+      then have "convex (S i) \<and> k i \<in> rel_interior (cone hull {1} \<times> S i)"
using k K_def assms by auto
then have "\<exists>ci si. k i = (ci, ci *\<^sub>R si) \<and> 0 < ci \<and> si \<in> rel_interior (S i)"
using rel_interior_convex_cone[of "S i"] by auto```