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
```