4504 apply rule |
4504 apply rule |
4505 apply rule |
4505 apply rule |
4506 apply (erule_tac x="x - y" in ballE) |
4506 apply (erule_tac x="x - y" in ballE) |
4507 apply (auto simp add: inner_diff) |
4507 apply (auto simp add: inner_diff) |
4508 done |
4508 done |
4509 def k \<equiv> "Sup ((\<lambda>x. inner a x) ` t)" |
4509 def k \<equiv> "SUP x:t. a \<bullet> x" |
4510 show ?thesis |
4510 show ?thesis |
4511 apply (rule_tac x="-a" in exI) |
4511 apply (rule_tac x="-a" in exI) |
4512 apply (rule_tac x="-(k + b / 2)" in exI) |
4512 apply (rule_tac x="-(k + b / 2)" in exI) |
4513 apply rule |
4513 apply (intro conjI ballI) |
4514 apply rule |
|
4515 defer |
|
4516 apply rule |
|
4517 unfolding inner_minus_left and neg_less_iff_less |
4514 unfolding inner_minus_left and neg_less_iff_less |
4518 proof - |
4515 proof - |
4519 from ab have "((\<lambda>x. inner a x) ` t) *<= (inner a y - b)" |
4516 fix x assume "x \<in> t" |
4520 apply (erule_tac x=y in ballE) |
4517 then have "inner a x - b / 2 < k" |
4521 apply (rule setleI) |
|
4522 using `y \<in> s` |
|
4523 apply auto |
|
4524 done |
|
4525 then have k: "isLub UNIV ((\<lambda>x. inner a x) ` t) k" |
|
4526 unfolding k_def |
4518 unfolding k_def |
4527 apply (rule_tac isLub_cSup) |
4519 proof (subst less_cSUP_iff) |
4528 using assms(5) |
4520 show "t \<noteq> {}" by fact |
4529 apply auto |
4521 show "bdd_above (op \<bullet> a ` t)" |
4530 done |
4522 using ab[rule_format, of y] `y \<in> s` |
4531 fix x |
4523 by (intro bdd_aboveI2[where M="inner a y - b"]) (auto simp: field_simps intro: less_imp_le) |
4532 assume "x \<in> t" |
4524 qed (auto intro!: bexI[of _ x] `0<b`) |
4533 then show "inner a x < (k + b / 2)" |
4525 then show "inner a x < k + b / 2" |
4534 using `0<b` and isLubD2[OF k, of "inner a x"] by auto |
4526 by auto |
4535 next |
4527 next |
4536 fix x |
4528 fix x |
4537 assume "x \<in> s" |
4529 assume "x \<in> s" |
4538 then have "k \<le> inner a x - b" |
4530 then have "k \<le> inner a x - b" |
4539 unfolding k_def |
4531 unfolding k_def |
4540 apply (rule_tac cSup_least) |
4532 apply (rule_tac cSUP_least) |
4541 using assms(5) |
4533 using assms(5) |
4542 using ab[THEN bspec[where x=x]] |
4534 using ab[THEN bspec[where x=x]] |
4543 apply auto |
4535 apply auto |
4544 done |
4536 done |
4545 then show "k + b / 2 < inner a x" |
4537 then show "k + b / 2 < inner a x" |
4624 shows "\<exists>a b. a \<noteq> 0 \<and> (\<forall>x\<in>s. inner a x \<le> b) \<and> (\<forall>x\<in>t. inner a x \<ge> b)" |
4616 shows "\<exists>a b. a \<noteq> 0 \<and> (\<forall>x\<in>s. inner a x \<le> b) \<and> (\<forall>x\<in>t. inner a x \<ge> b)" |
4625 proof - |
4617 proof - |
4626 from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]] |
4618 from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]] |
4627 obtain a where "a \<noteq> 0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x" |
4619 obtain a where "a \<noteq> 0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x" |
4628 using assms(3-5) by auto |
4620 using assms(3-5) by auto |
4629 then have "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x" |
4621 then have *: "\<And>x y. x \<in> t \<Longrightarrow> y \<in> s \<Longrightarrow> inner a y \<le> inner a x" |
4630 by (force simp add: inner_diff) |
4622 by (force simp add: inner_diff) |
4631 then show ?thesis |
4623 then have bdd: "bdd_above ((op \<bullet> a)`s)" |
4632 apply (rule_tac x=a in exI) |
4624 using `t \<noteq> {}` by (auto intro: bdd_aboveI2[OF *]) |
4633 apply (rule_tac x="Sup ((\<lambda>x. inner a x) ` s)" in exI) |
4625 show ?thesis |
4634 using `a\<noteq>0` |
4626 using `a\<noteq>0` |
4635 apply auto |
4627 by (intro exI[of _ a] exI[of _ "SUP x:s. a \<bullet> x"]) |
4636 apply (rule isLub_cSup[THEN isLubD2]) |
4628 (auto intro!: cSUP_upper bdd cSUP_least `a \<noteq> 0` `s \<noteq> {}` *) |
4637 prefer 4 |
|
4638 apply (rule cSup_least) |
|
4639 using assms(3-5) |
|
4640 apply (auto simp add: setle_def) |
|
4641 apply metis |
|
4642 done |
|
4643 qed |
4629 qed |
4644 |
4630 |
4645 |
4631 |
4646 subsection {* More convexity generalities *} |
4632 subsection {* More convexity generalities *} |
4647 |
4633 |