src/HOL/Library/Convex.thy
changeset 61531 ab2e862263e7
parent 61520 8f85bb443d33
child 61585 a9599d3d7610
     1.1 --- a/src/HOL/Library/Convex.thy	Thu Oct 29 15:40:52 2015 +0100
     1.2 +++ b/src/HOL/Library/Convex.thy	Mon Nov 02 11:56:28 2015 +0100
     1.3 @@ -304,6 +304,42 @@
     1.4    where "convex_on s f \<longleftrightarrow>
     1.5      (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y)"
     1.6  
     1.7 +lemma convex_onI [intro?]:
     1.8 +  assumes "\<And>t x y. t > 0 \<Longrightarrow> t < 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
     1.9 +             f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
    1.10 +  shows   "convex_on A f"
    1.11 +  unfolding convex_on_def
    1.12 +proof clarify
    1.13 +  fix x y u v assume A: "x \<in> A" "y \<in> A" "(u::real) \<ge> 0" "v \<ge> 0" "u + v = 1"
    1.14 +  from A(5) have [simp]: "v = 1 - u" by (simp add: algebra_simps)
    1.15 +  from A(1-4) show "f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y" using assms[of u y x]
    1.16 +    by (cases "u = 0 \<or> u = 1") (auto simp: algebra_simps)
    1.17 +qed
    1.18 +
    1.19 +lemma convex_on_linorderI [intro?]:
    1.20 +  fixes A :: "('a::{linorder,real_vector}) set"
    1.21 +  assumes "\<And>t x y. t > 0 \<Longrightarrow> t < 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x < y \<Longrightarrow>
    1.22 +             f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
    1.23 +  shows   "convex_on A f"
    1.24 +proof
    1.25 +  fix t x y assume A: "x \<in> A" "y \<in> A" "(t::real) > 0" "t < 1"
    1.26 +  case (goal1 t x y)
    1.27 +  with goal1 assms[of t x y] assms[of "1 - t" y x]
    1.28 +    show ?case by (cases x y rule: linorder_cases) (auto simp: algebra_simps)
    1.29 +qed
    1.30 +
    1.31 +lemma convex_onD:
    1.32 +  assumes "convex_on A f"
    1.33 +  shows   "\<And>t x y. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
    1.34 +             f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
    1.35 +  using assms unfolding convex_on_def by auto
    1.36 +
    1.37 +lemma convex_onD_Icc:
    1.38 +  assumes "convex_on {x..y} f" "x \<le> (y :: _ :: {real_vector,preorder})"
    1.39 +  shows   "\<And>t. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow>
    1.40 +             f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
    1.41 +  using assms(2) by (intro convex_onD[OF assms(1)]) simp_all
    1.42 +
    1.43  lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f"
    1.44    unfolding convex_on_def by auto
    1.45  
    1.46 @@ -835,4 +871,91 @@
    1.47    show ?thesis by auto
    1.48  qed
    1.49  
    1.50 +
    1.51 +subsection \<open>Convexity of real functions\<close>
    1.52 +
    1.53 +lemma convex_on_realI:
    1.54 +  assumes "connected A"
    1.55 +  assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
    1.56 +  assumes "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<le> y \<Longrightarrow> f' x \<le> f' y"
    1.57 +  shows   "convex_on A f"
    1.58 +proof (rule convex_on_linorderI)
    1.59 +  fix t x y :: real
    1.60 +  assume t: "t > 0" "t < 1" and xy: "x \<in> A" "y \<in> A" "x < y"
    1.61 +  def z \<equiv> "(1 - t) * x + t * y"
    1.62 +  with `connected A` and xy have ivl: "{x..y} \<subseteq> A" using connected_contains_Icc by blast
    1.63 +  
    1.64 +  from xy t have xz: "z > x" by (simp add: z_def algebra_simps)
    1.65 +  have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps)
    1.66 +  also from xy t have "... > 0" by (intro mult_pos_pos) simp_all
    1.67 +  finally have yz: "z < y" by simp
    1.68 +    
    1.69 +  from assms xz yz ivl t have "\<exists>\<xi>. \<xi> > x \<and> \<xi> < z \<and> f z - f x = (z - x) * f' \<xi>"
    1.70 +    by (intro MVT2) (auto intro!: assms(2))
    1.71 +  then obtain \<xi> where \<xi>: "\<xi> > x" "\<xi> < z" "f' \<xi> = (f z - f x) / (z - x)" by auto
    1.72 +  from assms xz yz ivl t have "\<exists>\<eta>. \<eta> > z \<and> \<eta> < y \<and> f y - f z = (y - z) * f' \<eta>"
    1.73 +    by (intro MVT2) (auto intro!: assms(2))
    1.74 +  then obtain \<eta> where \<eta>: "\<eta> > z" "\<eta> < y" "f' \<eta> = (f y - f z) / (y - z)" by auto
    1.75 +  
    1.76 +  from \<eta>(3) have "(f y - f z) / (y - z) = f' \<eta>" ..
    1.77 +  also from \<xi> \<eta> ivl have "\<xi> \<in> A" "\<eta> \<in> A" by auto
    1.78 +  with \<xi> \<eta> have "f' \<eta> \<ge> f' \<xi>" by (intro assms(3)) auto
    1.79 +  also from \<xi>(3) have "f' \<xi> = (f z - f x) / (z - x)" .
    1.80 +  finally have "(f y - f z) * (z - x) \<ge> (f z - f x) * (y - z)"
    1.81 +    using xz yz by (simp add: field_simps)
    1.82 +  also have "z - x = t * (y - x)" by (simp add: z_def algebra_simps)
    1.83 +  also have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps)
    1.84 +  finally have "(f y - f z) * t \<ge> (f z - f x) * (1 - t)" using xy by simp
    1.85 +  thus "(1 - t) * f x + t * f y \<ge> f ((1 - t) *\<^sub>R x + t *\<^sub>R y)"
    1.86 +    by (simp add: z_def algebra_simps)
    1.87 +qed
    1.88 +
    1.89 +lemma convex_on_inverse:
    1.90 +  assumes "A \<subseteq> {0<..}"
    1.91 +  shows   "convex_on A (inverse :: real \<Rightarrow> real)"
    1.92 +proof (rule convex_on_subset[OF _ assms], intro convex_on_realI[of _ _ "\<lambda>x. -inverse (x^2)"])
    1.93 +  fix u v :: real assume "u \<in> {0<..}" "v \<in> {0<..}" "u \<le> v"
    1.94 +  with assms show "-inverse (u^2) \<le> -inverse (v^2)"
    1.95 +    by (intro le_imp_neg_le le_imp_inverse_le power_mono) (simp_all)
    1.96 +qed (insert assms, auto intro!: derivative_eq_intros simp: divide_simps power2_eq_square)
    1.97 +
    1.98 +lemma convex_onD_Icc':
    1.99 +  assumes "convex_on {x..y} f" "c \<in> {x..y}"
   1.100 +  defines "d \<equiv> y - x"
   1.101 +  shows   "f c \<le> (f y - f x) / d * (c - x) + f x"
   1.102 +proof (cases y x rule: linorder_cases)
   1.103 +  assume less: "x < y"
   1.104 +  hence d: "d > 0" by (simp add: d_def)
   1.105 +  from assms(2) less have A: "0 \<le> (c - x) / d" "(c - x) / d \<le> 1" 
   1.106 +    by (simp_all add: d_def divide_simps)
   1.107 +  have "f c = f (x + (c - x) * 1)" by simp
   1.108 +  also from less have "1 = ((y - x) / d)" by (simp add: d_def)
   1.109 +  also from d have "x + (c - x) * \<dots> = (1 - (c - x) / d) *\<^sub>R x + ((c - x) / d) *\<^sub>R y" 
   1.110 +    by (simp add: field_simps)
   1.111 +  also have "f \<dots> \<le> (1 - (c - x) / d) * f x + (c - x) / d * f y" using assms less
   1.112 +    by (intro convex_onD_Icc) simp_all
   1.113 +  also from d have "\<dots> = (f y - f x) / d * (c - x) + f x" by (simp add: field_simps)
   1.114 +  finally show ?thesis .
   1.115 +qed (insert assms(2), simp_all)
   1.116 +
   1.117 +lemma convex_onD_Icc'':
   1.118 +  assumes "convex_on {x..y} f" "c \<in> {x..y}"
   1.119 +  defines "d \<equiv> y - x"
   1.120 +  shows   "f c \<le> (f x - f y) / d * (y - c) + f y"
   1.121 +proof (cases y x rule: linorder_cases)
   1.122 +  assume less: "x < y"
   1.123 +  hence d: "d > 0" by (simp add: d_def)
   1.124 +  from assms(2) less have A: "0 \<le> (y - c) / d" "(y - c) / d \<le> 1" 
   1.125 +    by (simp_all add: d_def divide_simps)
   1.126 +  have "f c = f (y - (y - c) * 1)" by simp
   1.127 +  also from less have "1 = ((y - x) / d)" by (simp add: d_def)
   1.128 +  also from d have "y - (y - c) * \<dots> = (1 - (1 - (y - c) / d)) *\<^sub>R x + (1 - (y - c) / d) *\<^sub>R y" 
   1.129 +    by (simp add: field_simps)
   1.130 +  also have "f \<dots> \<le> (1 - (1 - (y - c) / d)) * f x + (1 - (y - c) / d) * f y" using assms less
   1.131 +    by (intro convex_onD_Icc) (simp_all add: field_simps)
   1.132 +  also from d have "\<dots> = (f x - f y) / d * (y - c) + f y" by (simp add: field_simps)
   1.133 +  finally show ?thesis .
   1.134 +qed (insert assms(2), simp_all)
   1.135 +
   1.136 +
   1.137  end