# HG changeset patch
# User hoelzl
# Date 1307613016 -7200
# Node ID 57a1c19f8e3bde67dde50dcd10f83d52b1568ed2
# Parent  05aa7380f7fca818c2c485003038146574c2c4fe
lemma about differences of convex functions

diff -r 05aa7380f7fc -r 57a1c19f8e3b src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Thu Jun 09 11:50:16 2011 +0200
+++ b/src/HOL/Library/Convex.thy	Thu Jun 09 11:50:16 2011 +0200
@@ -465,6 +465,25 @@
   thus "convex_on C f" unfolding convex_on_def by auto
 qed
 
+lemma convex_on_diff:
+  fixes f :: "real \<Rightarrow> real"
+  assumes f: "convex_on I f" and I: "x\<in>I" "y\<in>I" and t: "x < t" "t < y"
+  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)"
+proof -
+  def a \<equiv> "(t - y) / (x - y)"
+  with t have "0 \<le> a" "0 \<le> 1 - a" by (auto simp: field_simps)
+  with f `x \<in> I` `y \<in> I` have cvx: "f (a * x + (1 - a) * y) \<le> a * f x + (1 - a) * f y"
+    by (auto simp: convex_on_def)
+  have "a * x + (1 - a) * y = a * (x - y) + y" by (simp add: field_simps)
+  also have "\<dots> = t" unfolding a_def using `x < t` `t < y` by simp
+  finally have "f t \<le> a * f x + (1 - a) * f y" using cvx by simp
+  also have "\<dots> = a * (f x - f y) + f y" by (simp add: field_simps)
+  finally have "f t - f y \<le> a * (f x - f y)" by simp
+  with t show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
+    by (simp add: times_divide_eq le_divide_eq divide_le_eq field_simps a_def)
+  with t show "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
+    by (simp add: times_divide_eq le_divide_eq divide_le_eq field_simps)
+qed
 
 lemma pos_convex_function:
   fixes f :: "real \<Rightarrow> real"