author hoelzl Thu Jun 09 11:50:16 2011 +0200 (2011-06-09) changeset 43337 57a1c19f8e3b parent 43336 05aa7380f7fc child 43338 a150d16bf77c
lemma about differences of convex functions
```     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"
```