src/HOL/Library/Convex.thy
 changeset 53620 3c7f5e7926dc parent 53596 d29d63460d84 child 53676 476ef9b468d2
```     1.1 --- a/src/HOL/Library/Convex.thy	Fri Sep 13 16:50:35 2013 +0200
1.2 +++ b/src/HOL/Library/Convex.thy	Fri Sep 13 11:16:13 2013 -0700
1.3 @@ -244,7 +244,7 @@
1.4  lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f"
1.5    unfolding convex_on_def by auto
1.6
1.9    assumes "convex_on s f" "convex_on s g"
1.10    shows "convex_on s (\<lambda>x. f x + g x)"
1.11  proof -
1.12 @@ -262,7 +262,7 @@
1.13    then show ?thesis unfolding convex_on_def by auto
1.14  qed
1.15
1.16 -lemma convex_cmul[intro]:
1.17 +lemma convex_on_cmul [intro]:
1.18    assumes "0 \<le> (c::real)" "convex_on s f"
1.19    shows "convex_on s (\<lambda>x. c * f x)"
1.20  proof-
1.21 @@ -284,7 +284,7 @@
1.22      using assms unfolding convex_on_def by fastforce
1.23  qed
1.24
1.25 -lemma convex_distance[intro]:
1.26 +lemma convex_on_dist [intro]:
1.27    fixes s :: "'a::real_normed_vector set"
1.28    shows "convex_on s (\<lambda>x. dist a x)"
1.29  proof (auto simp add: convex_on_def dist_norm)
1.30 @@ -304,42 +304,47 @@
1.31
1.32  subsection {* Arithmetic operations on sets preserve convexity. *}
1.33
1.34 -lemma convex_scaling:
1.35 -  assumes "convex s"
1.36 -  shows"convex ((\<lambda>x. c *\<^sub>R x) ` s)"
1.37 -  using assms unfolding convex_def image_iff
1.38 -proof safe
1.39 -  fix x xa y xb :: "'a::real_vector"
1.40 -  fix u v :: real
1.41 -  assume asm: "\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s"
1.42 -    "xa \<in> s" "xb \<in> s" "0 \<le> u" "0 \<le> v" "u + v = 1"
1.43 -  show "\<exists>x\<in>s. u *\<^sub>R c *\<^sub>R xa + v *\<^sub>R c *\<^sub>R xb = c *\<^sub>R x"
1.44 -    using bexI[of _ "u *\<^sub>R xa +v *\<^sub>R xb"] asm by (auto simp add: algebra_simps)
1.45 +lemma convex_linear_image:
1.46 +  assumes "linear f" and "convex s" shows "convex (f ` s)"
1.47 +proof -
1.48 +  interpret f: linear f by fact
1.49 +  from `convex s` show "convex (f ` s)"
1.51  qed
1.52
1.53 -lemma convex_negations: "convex s \<Longrightarrow> convex ((\<lambda>x. -x)` s)"
1.54 -  using assms unfolding convex_def image_iff
1.55 -proof safe
1.56 -  fix x xa y xb :: "'a::real_vector"
1.57 -  fix u v :: real
1.58 -  assume asm: "\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s"
1.59 -    "xa \<in> s" "xb \<in> s" "0 \<le> u" "0 \<le> v" "u + v = 1"
1.60 -  show "\<exists>x\<in>s. u *\<^sub>R - xa + v *\<^sub>R - xb = - x"
1.61 -    using bexI[of _ "u *\<^sub>R xa +v *\<^sub>R xb"] asm by auto
1.62 +lemma convex_linear_vimage:
1.63 +  assumes "linear f" and "convex s" shows "convex (f -` s)"
1.64 +proof -
1.65 +  interpret f: linear f by fact
1.66 +  from `convex s` show "convex (f -` s)"
1.68 +qed
1.69 +
1.70 +lemma convex_scaling:
1.71 +  assumes "convex s" shows "convex ((\<lambda>x. c *\<^sub>R x) ` s)"
1.72 +proof -
1.73 +  have "linear (\<lambda>x. c *\<^sub>R x)" by (simp add: linearI scaleR_add_right)
1.74 +  then show ?thesis using `convex s` by (rule convex_linear_image)
1.75 +qed
1.76 +
1.77 +lemma convex_negations:
1.78 +  assumes "convex s" shows "convex ((\<lambda>x. - x) ` s)"
1.79 +proof -
1.80 +  have "linear (\<lambda>x. - x)" by (simp add: linearI)
1.81 +  then show ?thesis using `convex s` by (rule convex_linear_image)
1.82  qed
1.83
1.84  lemma convex_sums:
1.85 -  assumes "convex s" "convex t"
1.86 +  assumes "convex s" and "convex t"
1.87    shows "convex {x + y| x y. x \<in> s \<and> y \<in> t}"
1.88 -  using assms unfolding convex_def image_iff
1.89 -proof safe
1.90 -  fix xa xb ya yb
1.91 -  assume xy:"xa\<in>s" "xb\<in>s" "ya\<in>t" "yb\<in>t"
1.92 -  fix u v :: real
1.93 -  assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
1.94 -  show "\<exists>x y. u *\<^sub>R (xa + ya) + v *\<^sub>R (xb + yb) = x + y \<and> x \<in> s \<and> y \<in> t"
1.95 -    using exI[of _ "u *\<^sub>R xa + v *\<^sub>R xb"] exI[of _ "u *\<^sub>R ya + v *\<^sub>R yb"]
1.96 -      assms[unfolded convex_def] uv xy by (auto simp add:scaleR_right_distrib)
1.97 +proof -
1.98 +  have "linear (\<lambda>(x, y). x + y)"
1.100 +  with assms have "convex ((\<lambda>(x, y). x + y) ` (s \<times> t))"
1.101 +    by (intro convex_linear_image convex_Times)
1.102 +  also have "((\<lambda>(x, y). x + y) ` (s \<times> t)) = {x + y| x y. x \<in> s \<and> y \<in> t}"
1.103 +    by auto
1.104 +  finally show ?thesis .
1.105  qed
1.106
1.107  lemma convex_differences:
1.108 @@ -347,17 +352,7 @@
1.109    shows "convex {x - y| x y. x \<in> s \<and> y \<in> t}"
1.110  proof -
1.111    have "{x - y| x y. x \<in> s \<and> y \<in> t} = {x + y |x y. x \<in> s \<and> y \<in> uminus ` t}"
1.112 -  proof safe
1.113 -    fix x x' y
1.114 -    assume "x' \<in> s" "y \<in> t"
1.115 -    then show "\<exists>x y'. x' - y = x + y' \<and> x \<in> s \<and> y' \<in> uminus ` t"
1.116 -      using exI[of _ x'] exI[of _ "-y"] by auto
1.117 -  next
1.118 -    fix x x' y y'
1.119 -    assume "x' \<in> s" "y' \<in> t"
1.120 -    then show "\<exists>x y. x' + - y' = x - y \<and> x \<in> s \<and> y \<in> t"
1.121 -      using exI[of _ x'] exI[of _ y'] by auto
1.122 -  qed
1.123 +    unfolding diff_def by auto
1.124    then show ?thesis
1.125      using convex_sums[OF assms(1) convex_negations[OF assms(2)]] by auto
1.126  qed
1.127 @@ -380,21 +375,6 @@
1.128      using convex_translation[OF convex_scaling[OF assms], of a c] by auto
1.129  qed
1.130
1.131 -lemma convex_linear_image:
1.132 -  assumes c:"convex s" and l:"bounded_linear f"
1.133 -  shows "convex(f ` s)"
1.134 -proof (auto simp add: convex_def)
1.135 -  interpret f: bounded_linear f by fact
1.136 -  fix x y
1.137 -  assume xy: "x \<in> s" "y \<in> s"
1.138 -  fix u v :: real
1.139 -  assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
1.140 -  show "u *\<^sub>R f x + v *\<^sub>R f y \<in> f ` s" unfolding image_iff
1.141 -    using bexI[of _ "u *\<^sub>R x + v *\<^sub>R y"] f.add f.scaleR
1.142 -      c[unfolded convex_def] xy uv by auto
1.143 -qed
1.144 -
1.145 -
1.146  lemma pos_is_convex: "convex {0 :: real <..}"
1.147    unfolding convex_alt
1.148  proof safe
```