644 fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1" |
644 fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1" |
645 ultimately have "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> (u * f x + v * f y) + (u * g x + v * g y)" |
645 ultimately have "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> (u * f x + v * f y) + (u * g x + v * g y)" |
646 using assms(1)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]] |
646 using assms(1)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]] |
647 using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]] |
647 using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]] |
648 apply - apply(rule add_mono) by auto |
648 apply - apply(rule add_mono) by auto |
649 hence "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> u * (f x + g x) + v * (f y + g y)" by (simp add: ring_simps) } |
649 hence "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> u * (f x + g x) + v * (f y + g y)" by (simp add: field_simps) } |
650 thus ?thesis unfolding convex_on_def by auto |
650 thus ?thesis unfolding convex_on_def by auto |
651 qed |
651 qed |
652 |
652 |
653 lemma convex_cmul[intro]: |
653 lemma convex_cmul[intro]: |
654 assumes "0 \<le> (c::real)" "convex_on s f" |
654 assumes "0 \<le> (c::real)" "convex_on s f" |
655 shows "convex_on s (\<lambda>x. c * f x)" |
655 shows "convex_on s (\<lambda>x. c * f x)" |
656 proof- |
656 proof- |
657 have *:"\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: ring_simps) |
657 have *:"\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: field_simps) |
658 show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto |
658 show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto |
659 qed |
659 qed |
660 |
660 |
661 lemma convex_lower: |
661 lemma convex_lower: |
662 assumes "convex_on s f" "x\<in>s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = 1" |
662 assumes "convex_on s f" "x\<in>s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = 1" |
1058 lemma convex_hull_3: |
1058 lemma convex_hull_3: |
1059 "convex hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c | u v w. 0 \<le> u \<and> 0 \<le> v \<and> 0 \<le> w \<and> u + v + w = 1}" |
1059 "convex hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c | u v w. 0 \<le> u \<and> 0 \<le> v \<and> 0 \<le> w \<and> u + v + w = 1}" |
1060 proof- |
1060 proof- |
1061 have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto |
1061 have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto |
1062 have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" |
1062 have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" |
1063 "\<And>x y z ::real^_. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by (auto simp add: ring_simps) |
1063 "\<And>x y z ::real^_. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by (auto simp add: field_simps) |
1064 show ?thesis unfolding convex_hull_finite[OF fin(1)] and Collect_def and convex_hull_finite_step[OF fin(2)] and * |
1064 show ?thesis unfolding convex_hull_finite[OF fin(1)] and Collect_def and convex_hull_finite_step[OF fin(2)] and * |
1065 unfolding convex_hull_finite_step[OF fin(3)] apply(rule ext) apply simp apply auto |
1065 unfolding convex_hull_finite_step[OF fin(3)] apply(rule ext) apply simp apply auto |
1066 apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp |
1066 apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp |
1067 apply(rule_tac x="1 - v - w" in exI) apply simp apply(rule_tac x=v in exI) apply simp apply(rule_tac x="\<lambda>x. w" in exI) by simp qed |
1067 apply(rule_tac x="1 - v - w" in exI) apply simp apply(rule_tac x=v in exI) apply simp apply(rule_tac x="\<lambda>x. w" in exI) by simp qed |
1068 |
1068 |
2308 hence "a < b" unfolding * using as(4) *(2) apply(rule_tac mult_left_less_imp_less[of "1 - v"]) by(auto simp add: field_simps) |
2308 hence "a < b" unfolding * using as(4) *(2) apply(rule_tac mult_left_less_imp_less[of "1 - v"]) by(auto simp add: field_simps) |
2309 hence "a \<le> u * a + v * b" unfolding * using as(4) by (auto simp add: field_simps intro!:mult_right_mono) |
2309 hence "a \<le> u * a + v * b" unfolding * using as(4) by (auto simp add: field_simps intro!:mult_right_mono) |
2310 } moreover |
2310 } moreover |
2311 { fix a b assume "\<not> u * a + v * b \<le> a" |
2311 { fix a b assume "\<not> u * a + v * b \<le> a" |
2312 hence "v * b > (1 - u) * a" unfolding not_le using as(4) by(auto simp add: field_simps) |
2312 hence "v * b > (1 - u) * a" unfolding not_le using as(4) by(auto simp add: field_simps) |
2313 hence "a < b" unfolding * using as(4) apply(rule_tac mult_left_less_imp_less) by(auto simp add: ring_simps) |
2313 hence "a < b" unfolding * using as(4) apply(rule_tac mult_left_less_imp_less) by(auto simp add: field_simps) |
2314 hence "u * a + v * b \<le> b" unfolding ** using **(2) as(3) by(auto simp add: field_simps intro!:mult_right_mono) } |
2314 hence "u * a + v * b \<le> b" unfolding ** using **(2) as(3) by(auto simp add: field_simps intro!:mult_right_mono) } |
2315 ultimately show "u *\<^sub>R x + v *\<^sub>R y \<in> s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)]) |
2315 ultimately show "u *\<^sub>R x + v *\<^sub>R y \<in> s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)]) |
2316 using as(3-) dimindex_ge_1 apply- by(auto simp add: vector_component) qed |
2316 using as(3-) dimindex_ge_1 apply- by(auto simp add: vector_component) qed |
2317 |
2317 |
2318 lemma is_interval_connected: |
2318 lemma is_interval_connected: |