src/HOL/Library/Convex.thy
 changeset 38642 8fa437809c67 parent 36778 739a9379e29b child 43337 57a1c19f8e3b
```     1.1 --- a/src/HOL/Library/Convex.thy	Sun Aug 22 14:27:30 2010 +0200
1.2 +++ b/src/HOL/Library/Convex.thy	Mon Aug 23 11:17:13 2010 +0200
1.3 @@ -244,7 +244,7 @@
1.4    shows "convex_on s (\<lambda>x. c * f x)"
1.5  proof-
1.6    have *:"\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: field_simps)
1.7 -  show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto
1.8 +  show ?thesis using assms(2) and mult_left_mono [OF _ assms(1)] unfolding convex_on_def and * by auto
1.9  qed
1.10
1.11  lemma convex_lower:
1.12 @@ -253,7 +253,7 @@
1.13  proof-
1.14    let ?m = "max (f x) (f y)"
1.15    have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)"
1.18    also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto
1.19    finally show ?thesis
1.20      using assms unfolding convex_on_def by fastsimp
1.21 @@ -481,8 +481,8 @@
1.22    hence xpos: "?x \<in> C" using asm unfolding convex_alt by fastsimp
1.23    have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x)
1.24              \<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
1.25 -    using add_mono[OF mult_mono1[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
1.26 -      mult_mono1[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
1.27 +    using add_mono[OF mult_left_mono[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
1.28 +      mult_left_mono[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
1.29    hence "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"