src/HOL/Library/Convex.thy
changeset 43337 57a1c19f8e3b
parent 38642 8fa437809c67
child 44142 8e27e0177518
     1.1 --- a/src/HOL/Library/Convex.thy	Thu Jun 09 11:50:16 2011 +0200
     1.2 +++ b/src/HOL/Library/Convex.thy	Thu Jun 09 11:50:16 2011 +0200
     1.3 @@ -465,6 +465,25 @@
     1.4    thus "convex_on C f" unfolding convex_on_def by auto
     1.5  qed
     1.6  
     1.7 +lemma convex_on_diff:
     1.8 +  fixes f :: "real \<Rightarrow> real"
     1.9 +  assumes f: "convex_on I f" and I: "x\<in>I" "y\<in>I" and t: "x < t" "t < y"
    1.10 +  shows "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)" "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
    1.11 +proof -
    1.12 +  def a \<equiv> "(t - y) / (x - y)"
    1.13 +  with t have "0 \<le> a" "0 \<le> 1 - a" by (auto simp: field_simps)
    1.14 +  with f `x \<in> I` `y \<in> I` have cvx: "f (a * x + (1 - a) * y) \<le> a * f x + (1 - a) * f y"
    1.15 +    by (auto simp: convex_on_def)
    1.16 +  have "a * x + (1 - a) * y = a * (x - y) + y" by (simp add: field_simps)
    1.17 +  also have "\<dots> = t" unfolding a_def using `x < t` `t < y` by simp
    1.18 +  finally have "f t \<le> a * f x + (1 - a) * f y" using cvx by simp
    1.19 +  also have "\<dots> = a * (f x - f y) + f y" by (simp add: field_simps)
    1.20 +  finally have "f t - f y \<le> a * (f x - f y)" by simp
    1.21 +  with t show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
    1.22 +    by (simp add: times_divide_eq le_divide_eq divide_le_eq field_simps a_def)
    1.23 +  with t show "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
    1.24 +    by (simp add: times_divide_eq le_divide_eq divide_le_eq field_simps)
    1.25 +qed
    1.26  
    1.27  lemma pos_convex_function:
    1.28    fixes f :: "real \<Rightarrow> real"