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.7 -lemma convex_add[intro]:
     1.8 +lemma convex_on_add [intro]:
     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.50 +    by (simp add: convex_def f.scaleR [symmetric] f.add [symmetric])
    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.67 +    by (simp add: convex_def f.add f.scaleR)
    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.99 +    by (auto intro: linearI simp add: scaleR_add_right)
   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