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.16 -    using assms(4,5) by(auto simp add: mult_mono1 add_mono)
    1.17 +    using assms(4,5) by (auto simp add: mult_left_mono add_mono)
    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"
    1.30      by (auto simp add:field_simps)
    1.31    thus "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"