equal
deleted
inserted
replaced
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 |