src/HOL/Library/Convex.thy
changeset 56536 aefb4a8da31f
parent 56479 91958d4b30f7
child 56541 0e3abadbef39
equal deleted inserted replaced
56535:34023a586608 56536:aefb4a8da31f
   604     finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3" by simp
   604     finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3" by simp
   605     have A': "y - z1 \<ge> 0" using z1 by auto
   605     have A': "y - z1 \<ge> 0" using z1 by auto
   606     have "z3 \<in> C" using z3 asm atMostAtLeast_subset_convex
   606     have "z3 \<in> C" using z3 asm atMostAtLeast_subset_convex
   607       `convex C` `x \<in> C` `z1 \<in> C` `x < z1` by fastforce
   607       `convex C` `x \<in> C` `z1 \<in> C` `x < z1` by fastforce
   608     then have B': "f'' z3 \<ge> 0" using assms by auto
   608     then have B': "f'' z3 \<ge> 0" using assms by auto
   609     from A' B' have "(y - z1) * f'' z3 \<ge> 0" using mult_nonneg_nonneg by auto
   609     from A' B' have "(y - z1) * f'' z3 \<ge> 0" by auto
   610     from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
   610     from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
   611     from mult_right_mono_neg[OF this le(2)]
   611     from mult_right_mono_neg[OF this le(2)]
   612     have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"
   612     have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"
   613       by (simp add: algebra_simps)
   613       by (simp add: algebra_simps)
   614     then have "f' y * (x - y) - (f x - f y) \<le> 0" using le by auto
   614     then have "f' y * (x - y) - (f x - f y) \<le> 0" using le by auto
   619     finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2" by simp
   619     finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2" by simp
   620     have A: "z1 - x \<ge> 0" using z1 by auto
   620     have A: "z1 - x \<ge> 0" using z1 by auto
   621     have "z2 \<in> C" using z2 z1 asm atMostAtLeast_subset_convex
   621     have "z2 \<in> C" using z2 z1 asm atMostAtLeast_subset_convex
   622       `convex C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastforce
   622       `convex C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastforce
   623     then have B: "f'' z2 \<ge> 0" using assms by auto
   623     then have B: "f'' z2 \<ge> 0" using assms by auto
   624     from A B have "(z1 - x) * f'' z2 \<ge> 0" using mult_nonneg_nonneg by auto
   624     from A B have "(z1 - x) * f'' z2 \<ge> 0" by auto
   625     from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
   625     from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
   626     from mult_right_mono[OF this ge(2)]
   626     from mult_right_mono[OF this ge(2)]
   627     have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)"
   627     have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)"
   628       by (simp add: algebra_simps)
   628       by (simp add: algebra_simps)
   629     then have "f y - f x - f' x * (y - x) \<ge> 0" using ge by auto
   629     then have "f y - f x - f' x * (y - x) \<ge> 0" using ge by auto