|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
mfourier.mli
Sprache: SML
|
|
(* Title: HOL/Analysis/Starlike.thy
Author: L C Paulson, University of Cambridge
Author: Robert Himmelmann, TU Muenchen
Author: Bogdan Grechuk, University of Edinburgh
Author: Armin Heller, TU Muenchen
Author: Johannes Hoelzl, TU Muenchen
*)
chapter \<open>Unsorted\<close>
theory Starlike
imports
Convex_Euclidean_Space
Line_Segment
begin
lemma affine_hull_closed_segment [simp]:
"affine hull (closed_segment a b) = affine hull {a,b}"
by (simp add: segment_convex_hull)
lemma affine_hull_open_segment [simp]:
fixes a :: "'a::euclidean_space"
shows "affine hull (open_segment a b) = (if a = b then {} else affine hull {a,b})"
by (metis affine_hull_convex_hull affine_hull_empty closure_open_segment closure_same_affine_hull segment_convex_hull)
lemma rel_interior_closure_convex_segment:
fixes S :: "_::euclidean_space set"
assumes "convex S" "a \ rel_interior S" "b \ closure S"
shows "open_segment a b \ rel_interior S"
proof
fix x
have [simp]: "(1 - u) *\<^sub>R a + u *\<^sub>R b = b - (1 - u) *\<^sub>R (b - a)" for u
by (simp add: algebra_simps)
assume "x \ open_segment a b"
then show "x \ rel_interior S"
unfolding closed_segment_def open_segment_def using assms
by (auto intro: rel_interior_closure_convex_shrink)
qed
lemma convex_hull_insert_segments:
"convex hull (insert a S) =
(if S = {} then {a} else \<Union>x \<in> convex hull S. closed_segment a x)"
by (force simp add: convex_hull_insert_alt in_segment)
lemma Int_convex_hull_insert_rel_exterior:
fixes z :: "'a::euclidean_space"
assumes "convex C" "T \ C" and z: "z \ rel_interior C" and dis: "disjnt S (rel_interior C)"
shows "S \ (convex hull (insert z T)) = S \ (convex hull T)" (is "?lhs = ?rhs")
proof
have "T = {} \ z \ S"
using dis z by (auto simp add: disjnt_def)
then show "?lhs \ ?rhs"
proof (clarsimp simp add: convex_hull_insert_segments)
fix x y
assume "x \ S" and y: "y \ convex hull T" and "x \ closed_segment z y"
have "y \ closure C"
by (metis y \<open>convex C\<close> \<open>T \<subseteq> C\<close> closure_subset contra_subsetD convex_hull_eq hull_mono)
moreover have "x \ rel_interior C"
by (meson \<open>x \<in> S\<close> dis disjnt_iff)
moreover have "x \ open_segment z y \ {z, y}"
using \<open>x \<in> closed_segment z y\<close> closed_segment_eq_open by blast
ultimately show "x \ convex hull T"
using rel_interior_closure_convex_segment [OF \<open>convex C\<close> z]
using y z by blast
qed
show "?rhs \ ?lhs"
by (meson hull_mono inf_mono subset_insertI subset_refl)
qed
subsection\<^marker>\<open>tag unimportant\<close> \<open>Shrinking towards the interior of a convex set\<close>
lemma mem_interior_convex_shrink:
fixes S :: "'a::euclidean_space set"
assumes "convex S"
and "c \ interior S"
and "x \ S"
and "0 < e"
and "e \ 1"
shows "x - e *\<^sub>R (x - c) \ interior S"
proof -
obtain d where "d > 0" and d: "ball c d \ S"
using assms(2) unfolding mem_interior by auto
show ?thesis
unfolding mem_interior
proof (intro exI subsetI conjI)
fix y
assume "y \ ball (x - e *\<^sub>R (x - c)) (e*d)"
then have as: "dist (x - e *\<^sub>R (x - c)) y < e * d"
by simp
have *: "y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x"
using \<open>e > 0\<close> by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
have "c - ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = (1 / e) *\<^sub>R (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
using \<open>e > 0\<close>
by (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
then have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = \1/e\ * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
by (simp add: dist_norm)
also have "\ = \1/e\ * norm (x - e *\<^sub>R (x - c) - y)"
by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
also have "\ < d"
using as[unfolded dist_norm] and \<open>e > 0\<close>
by (auto simp add:pos_divide_less_eq[OF \<open>e > 0\<close>] mult.commute)
finally have "(1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x \ S"
using assms(3-5) d
by (intro convexD_alt [OF \<open>convex S\<close>]) (auto intro: convexD_alt [OF \<open>convex S\<close>])
with \<open>e > 0\<close> show "y \<in> S"
by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
qed (use \<open>e>0\<close> \<open>d>0\<close> in auto)
qed
lemma mem_interior_closure_convex_shrink:
fixes S :: "'a::euclidean_space set"
assumes "convex S"
and "c \ interior S"
and "x \ closure S"
and "0 < e"
and "e \ 1"
shows "x - e *\<^sub>R (x - c) \ interior S"
proof -
obtain d where "d > 0" and d: "ball c d \ S"
using assms(2) unfolding mem_interior by auto
have "\y\S. norm (y - x) * (1 - e) < e * d"
proof (cases "x \ S")
case True
then show ?thesis
using \<open>e > 0\<close> \<open>d > 0\<close> by force
next
case False
then have x: "x islimpt S"
using assms(3)[unfolded closure_def] by auto
show ?thesis
proof (cases "e = 1")
case True
obtain y where "y \ S" "y \ x" "dist y x < 1"
using x[unfolded islimpt_approachable,THEN spec[where x=1]] by auto
then show ?thesis
using True \<open>0 < d\<close> by auto
next
case False
then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
using \<open>e \<le> 1\<close> \<open>e > 0\<close> \<open>d > 0\<close> by auto
then obtain y where "y \ S" "y \ x" "dist y x < e * d / (1 - e)"
using islimpt_approachable x by blast
then have "norm (y - x) * (1 - e) < e * d"
by (metis "*" dist_norm mult_imp_div_pos_le not_less)
then show ?thesis
using \<open>y \<in> S\<close> by blast
qed
qed
then obtain y where "y \ S" and y: "norm (y - x) * (1 - e) < e * d"
by auto
define z where "z = c + ((1 - e) / e) *\<^sub>R (x - y)"
have *: "x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)"
unfolding z_def using \<open>e > 0\<close>
by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
have "(1 - e) * norm (x - y) / e < d"
using y \<open>0 < e\<close> by (simp add: field_simps norm_minus_commute)
then have "z \ interior (ball c d)"
using \<open>0 < e\<close> \<open>e \<le> 1\<close> by (simp add: interior_open[OF open_ball] z_def dist_norm)
then have "z \ interior S"
using d interiorI interior_ball by blast
then show ?thesis
unfolding * using mem_interior_convex_shrink \<open>y \<in> S\<close> assms by blast
qed
lemma in_interior_closure_convex_segment:
fixes S :: "'a::euclidean_space set"
assumes "convex S" and a: "a \ interior S" and b: "b \ closure S"
shows "open_segment a b \ interior S"
proof (clarsimp simp: in_segment)
fix u::real
assume u: "0 < u" "u < 1"
have "(1 - u) *\<^sub>R a + u *\<^sub>R b = b - (1 - u) *\<^sub>R (b - a)"
by (simp add: algebra_simps)
also have "... \ interior S" using mem_interior_closure_convex_shrink [OF assms] u
by simp
finally show "(1 - u) *\<^sub>R a + u *\<^sub>R b \ interior S" .
qed
lemma convex_closure_interior:
fixes S :: "'a::euclidean_space set"
assumes "convex S" and int: "interior S \ {}"
shows "closure(interior S) = closure S"
proof -
obtain a where a: "a \ interior S"
using int by auto
have "closure S \ closure(interior S)"
proof
fix x
assume x: "x \ closure S"
show "x \ closure (interior S)"
proof (cases "x=a")
case True
then show ?thesis
using \<open>a \<in> interior S\<close> closure_subset by blast
next
case False
show ?thesis
proof (clarsimp simp add: closure_def islimpt_approachable)
fix e::real
assume xnotS: "x \ interior S" and "0 < e"
show "\x'\interior S. x' \ x \ dist x' x < e"
proof (intro bexI conjI)
show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \ x"
using False \<open>0 < e\<close> by (auto simp: algebra_simps min_def)
show "dist (x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a)) x < e"
using \<open>0 < e\<close> by (auto simp: dist_norm min_def)
show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \ interior S"
using \<open>0 < e\<close> False
by (auto simp add: min_def a intro: mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a x])
qed
qed
qed
qed
then show ?thesis
by (simp add: closure_mono interior_subset subset_antisym)
qed
lemma closure_convex_Int_superset:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "interior S \ {}" "interior S \ closure T"
shows "closure(S \ T) = closure S"
proof -
have "closure S \ closure(interior S)"
by (simp add: convex_closure_interior assms)
also have "... \ closure (S \ T)"
using interior_subset [of S] assms
by (metis (no_types, lifting) Int_assoc Int_lower2 closure_mono closure_open_Int_superset inf.orderE open_interior)
finally show ?thesis
by (simp add: closure_mono dual_order.antisym)
qed
subsection\<^marker>\<open>tag unimportant\<close> \<open>Some obvious but surprisingly hard simplex lemmas\<close>
lemma simplex:
assumes "finite S"
and "0 \ S"
shows "convex hull (insert 0 S) = {y. \u. (\x\S. 0 \ u x) \ sum u S \ 1 \ sum (\x. u x *\<^sub>R x) S = y}"
proof (simp add: convex_hull_finite set_eq_iff assms, safe)
fix x and u :: "'a \ real"
assume "0 \ u 0" "\x\S. 0 \ u x" "u 0 + sum u S = 1"
then show "\v. (\x\S. 0 \ v x) \ sum v S \ 1 \ (\x\S. v x *\<^sub>R x) = (\x\S. u x *\<^sub>R x)"
by force
next
fix x and u :: "'a \ real"
assume "\x\S. 0 \ u x" "sum u S \ 1"
then show "\v. 0 \ v 0 \ (\x\S. 0 \ v x) \ v 0 + sum v S = 1 \ (\x\S. v x *\<^sub>R x) = (\x\S. u x *\<^sub>R x)"
by (rule_tac x="\x. if x = 0 then 1 - sum u S else u x" in exI) (auto simp: sum_delta_notmem assms if_smult)
qed
lemma substd_simplex:
assumes d: "d \ Basis"
shows "convex hull (insert 0 d) =
{x. (\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> (\<Sum>i\<in>d. x\<bullet>i) \<le> 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)}"
(is "convex hull (insert 0 ?p) = ?s")
proof -
let ?D = d
have "0 \ ?p"
using assms by (auto simp: image_def)
from d have "finite d"
by (blast intro: finite_subset finite_Basis)
show ?thesis
unfolding simplex[OF \<open>finite d\<close> \<open>0 \<notin> ?p\<close>]
proof (intro set_eqI; safe)
fix u :: "'a \ real"
assume as: "\x\?D. 0 \ u x" "sum u ?D \ 1"
let ?x = "(\x\?D. u x *\<^sub>R x)"
have ind: "\i\Basis. i \ d \ u i = ?x \ i"
and notind: "(\i\Basis. i \ d \ ?x \ i = 0)"
using substdbasis_expansion_unique[OF assms] by blast+
then have **: "sum u ?D = sum ((\) ?x) ?D"
using assms by (auto intro!: sum.cong)
show "0 \ ?x \ i" if "i \ Basis" for i
using as(1) ind notind that by fastforce
show "sum ((\) ?x) ?D \ 1"
using "**" as(2) by linarith
show "?x \ i = 0" if "i \ Basis" "i \ d" for i
using notind that by blast
next
fix x
assume "\i\Basis. 0 \ x \ i" "sum ((\) x) ?D \ 1" "(\i\Basis. i \ d \ x \ i = 0)"
with d show "\u. (\x\?D. 0 \ u x) \ sum u ?D \ 1 \ (\x\?D. u x *\<^sub>R x) = x"
unfolding substdbasis_expansion_unique[OF assms]
by (rule_tac x="inner x" in exI) auto
qed
qed
lemma std_simplex:
"convex hull (insert 0 Basis) =
{x::'a::euclidean_space. (\i\Basis. 0 \ x\i) \ sum (\i. x\i) Basis \ 1}"
using substd_simplex[of Basis] by auto
lemma interior_std_simplex:
"interior (convex hull (insert 0 Basis)) =
{x::'a::euclidean_space. (\i\Basis. 0 < x\i) \ sum (\i. x\i) Basis < 1}"
unfolding set_eq_iff mem_interior std_simplex
proof (intro allI iffI CollectI; clarify)
fix x :: 'a
fix e
assume "e > 0" and as: "ball x e \ {x. (\i\Basis. 0 \ x \ i) \ sum ((\) x) Basis \ 1}"
show "(\i\Basis. 0 < x \ i) \ sum ((\) x) Basis < 1"
proof safe
fix i :: 'a
assume i: "i \ Basis"
then show "0 < x \ i"
using as[THEN subsetD[where c="x - (e/2) *\<^sub>R i"]] and \e > 0\
by (force simp add: inner_simps)
next
have **: "dist x (x + (e/2) *\<^sub>R (SOME i. i\Basis)) < e" using \e > 0\
unfolding dist_norm
by (auto intro!: mult_strict_left_mono simp: SOME_Basis)
have "\i. i \ Basis \ (x + (e/2) *\<^sub>R (SOME i. i\Basis)) \ i =
x\<bullet>i + (if i = (SOME i. i\<in>Basis) then e/2 else 0)"
by (auto simp: SOME_Basis inner_Basis inner_simps)
then have *: "sum ((\) (x + (e/2) *\<^sub>R (SOME i. i\Basis))) Basis =
sum (\<lambda>i. x\<bullet>i + (if (SOME i. i\<in>Basis) = i then e/2 else 0)) Basis"
by (auto simp: intro!: sum.cong)
have "sum ((\) x) Basis < sum ((\) (x + (e/2) *\<^sub>R (SOME i. i\Basis))) Basis"
using \<open>e > 0\<close> DIM_positive by (auto simp: SOME_Basis sum.distrib *)
also have "\ \ 1"
using ** as by force
finally show "sum ((\) x) Basis < 1" by auto
qed
next
fix x :: 'a
assume as: "\i\Basis. 0 < x \ i" "sum ((\) x) Basis < 1"
obtain a :: 'b where "a \ UNIV" using UNIV_witness ..
let ?d = "(1 - sum ((\) x) Basis) / real (DIM('a))"
show "\e>0. ball x e \ {x. (\i\Basis. 0 \ x \ i) \ sum ((\) x) Basis \ 1}"
proof (rule_tac x="min (Min (((\) x) ` Basis)) D" for D in exI, intro conjI subsetI CollectI)
fix y
assume y: "y \ ball x (min (Min ((\) x ` Basis)) ?d)"
have "sum ((\) y) Basis \ sum (\i. x\i + ?d) Basis"
proof (rule sum_mono)
fix i :: 'a
assume i: "i \ Basis"
have "\y\i - x\i\ \ norm (y - x)"
by (metis Basis_le_norm i inner_commute inner_diff_right)
also have "... < ?d"
using y by (simp add: dist_norm norm_minus_commute)
finally have "\y\i - x\i\ < ?d" .
then show "y \ i \ x \ i + ?d" by auto
qed
also have "\ \ 1"
unfolding sum.distrib sum_constant
by (auto simp add: Suc_le_eq)
finally show "sum ((\) y) Basis \ 1" .
show "(\i\Basis. 0 \ y \ i)"
proof safe
fix i :: 'a
assume i: "i \ Basis"
have "norm (x - y) < Min (((\) x) ` Basis)"
using y by (auto simp: dist_norm less_eq_real_def)
also have "... \ x\i"
using i by auto
finally have "norm (x - y) < x\i" .
then show "0 \ y\i"
using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format, OF i]
by (auto simp: inner_simps)
qed
next
have "Min (((\) x) ` Basis) > 0"
using as by simp
moreover have "?d > 0"
using as by (auto simp: Suc_le_eq)
ultimately show "0 < min (Min ((\) x ` Basis)) ((1 - sum ((\) x) Basis) / real DIM('a))"
by linarith
qed
qed
lemma interior_std_simplex_nonempty:
obtains a :: "'a::euclidean_space" where
"a \ interior(convex hull (insert 0 Basis))"
proof -
let ?D = "Basis :: 'a set"
let ?a = "sum (\b::'a. inverse (2 * real DIM('a)) *\<^sub>R b) Basis"
{
fix i :: 'a
assume i: "i \ Basis"
have "?a \ i = inverse (2 * real DIM('a))"
by (rule trans[of _ "sum (\j. if i = j then inverse (2 * real DIM('a)) else 0) ?D"])
(simp_all add: sum.If_cases i) }
note ** = this
show ?thesis
proof
show "?a \ interior(convex hull (insert 0 Basis))"
unfolding interior_std_simplex mem_Collect_eq
proof safe
fix i :: 'a
assume i: "i \ Basis"
show "0 < ?a \ i"
unfolding **[OF i] by (auto simp add: Suc_le_eq)
next
have "sum ((\) ?a) ?D = sum (\i. inverse (2 * real DIM('a))) ?D"
by (auto intro: sum.cong)
also have "\ < 1"
unfolding sum_constant divide_inverse[symmetric]
by (auto simp add: field_simps)
finally show "sum ((\) ?a) ?D < 1" by auto
qed
qed
qed
lemma rel_interior_substd_simplex:
assumes D: "D \ Basis"
shows "rel_interior (convex hull (insert 0 D)) =
{x::'a::euclidean_space. (\i\D. 0 < x\i) \ (\i\D. x\i) < 1 \ (\i\Basis. i \ D \ x\i = 0)}"
(is "_ = ?s")
proof -
have "finite D"
using D finite_Basis finite_subset by blast
show ?thesis
proof (cases "D = {}")
case True
then show ?thesis
using rel_interior_sing using euclidean_eq_iff[of _ 0] by auto
next
case False
have h0: "affine hull (convex hull (insert 0 D)) =
{x::'a::euclidean_space. (\i\Basis. i \ D \ x\i = 0)}"
using affine_hull_convex_hull affine_hull_substd_basis assms by auto
have aux: "\x::'a. \i\Basis. (\i\D. 0 \ x\i) \ (\i\Basis. i \ D \ x\i = 0) \ 0 \ x\i"
by auto
{
fix x :: "'a::euclidean_space"
assume x: "x \ rel_interior (convex hull (insert 0 D))"
then obtain e where "e > 0" and
"ball x e \ {xa. (\i\Basis. i \ D \ xa\i = 0)} \ convex hull (insert 0 D)"
using mem_rel_interior_ball[of x "convex hull (insert 0 D)"] h0 by auto
then have as: "\y. \dist x y < e \ (\i\Basis. i \ D \ y\i = 0)\ \
(\<forall>i\<in>D. 0 \<le> y \<bullet> i) \<and> sum ((\<bullet>) y) D \<le> 1"
using assms by (force simp: substd_simplex)
have x0: "(\i\Basis. i \ D \ x\i = 0)"
using x rel_interior_subset substd_simplex[OF assms] by auto
have "(\i\D. 0 < x \ i) \ sum ((\) x) D < 1 \ (\i\Basis. i \ D \ x\i = 0)"
proof (intro conjI ballI)
fix i :: 'a
assume "i \ D"
then have "\j\D. 0 \ (x - (e/2) *\<^sub>R i) \ j"
using D \<open>e > 0\<close> x0
by (intro as[THEN conjunct1]) (force simp: dist_norm inner_simps inner_Basis)
then show "0 < x \ i"
using \<open>e > 0\<close> \<open>i \<in> D\<close> D by (force simp: inner_simps inner_Basis)
next
obtain a where a: "a \ D"
using \<open>D \<noteq> {}\<close> by auto
then have **: "dist x (x + (e/2) *\<^sub>R a) < e"
using \<open>e > 0\<close> norm_Basis[of a] D by (auto simp: dist_norm)
have "\i. i \ Basis \ (x + (e/2) *\<^sub>R a) \ i = x\i + (if i = a then e/2 else 0)"
using a D by (auto simp: inner_simps inner_Basis)
then have *: "sum ((\) (x + (e/2) *\<^sub>R a)) D = sum (\i. x\i + (if a = i then e/2 else 0)) D"
using D by (intro sum.cong) auto
have "a \ Basis"
using \<open>a \<in> D\<close> D by auto
then have h1: "(\i\Basis. i \ D \ (x + (e/2) *\<^sub>R a) \ i = 0)"
using x0 D \<open>a\<in>D\<close> by (auto simp add: inner_add_left inner_Basis)
have "sum ((\) x) D < sum ((\) (x + (e/2) *\<^sub>R a)) D"
using \<open>e > 0\<close> \<open>a \<in> D\<close> \<open>finite D\<close> by (auto simp add: * sum.distrib)
also have "\ \ 1"
using ** h1 as[rule_format, of "x + (e/2) *\<^sub>R a"]
by auto
finally show "sum ((\) x) D < 1" "\i. i\Basis \ i \ D \ x\i = 0"
using x0 by auto
qed
}
moreover
{
fix x :: "'a::euclidean_space"
assume as: "x \ ?s"
have "\i. 0 < x\i \ 0 = x\i \ 0 \ x\i"
by auto
moreover have "\i. i \ D \ i \ D" by auto
ultimately
have "\i. (\i\D. 0 < x\i) \ (\i. i \ D \ x\i = 0) \ 0 \ x\i"
by metis
then have h2: "x \ convex hull (insert 0 D)"
using as assms by (force simp add: substd_simplex)
obtain a where a: "a \ D"
using \<open>D \<noteq> {}\<close> by auto
define d where "d \ (1 - sum ((\) x) D) / real (card D)"
have "\e>0. ball x e \ {x. \i\Basis. i \ D \ x \ i = 0} \ convex hull insert 0 D"
unfolding substd_simplex[OF assms]
proof (intro exI; safe)
have "0 < card D" using \<open>D \<noteq> {}\<close> \<open>finite D\<close>
by (simp add: card_gt_0_iff)
have "Min (((\) x) ` D) > 0"
using as \<open>D \<noteq> {}\<close> \<open>finite D\<close> by (simp)
moreover have "d > 0"
using as \<open>0 < card D\<close> by (auto simp: d_def)
ultimately show "min (Min (((\) x) ` D)) d > 0"
by auto
fix y :: 'a
assume y2: "\i\Basis. i \ D \ y\i = 0"
assume "y \ ball x (min (Min ((\) x ` D)) d)"
then have y: "dist x y < min (Min ((\) x ` D)) d"
by auto
have "sum ((\) y) D \ sum (\i. x\i + d) D"
proof (rule sum_mono)
fix i
assume "i \ D"
with D have i: "i \ Basis"
by auto
have "\y\i - x\i\ \ norm (y - x)"
by (metis i inner_commute inner_diff_right norm_bound_Basis_le order_refl)
also have "... < d"
by (metis dist_norm min_less_iff_conj norm_minus_commute y)
finally have "\y\i - x\i\ < d" .
then show "y \ i \ x \ i + d" by auto
qed
also have "\ \ 1"
unfolding sum.distrib sum_constant d_def using \<open>0 < card D\<close>
by auto
finally show "sum ((\) y) D \ 1" .
fix i :: 'a
assume i: "i \ Basis"
then show "0 \ y\i"
proof (cases "i\D")
case True
have "norm (x - y) < x\i"
using y Min_gr_iff[of "(\) x ` D" "norm (x - y)"] \0 < card D\ \i \ D\
by (simp add: dist_norm card_gt_0_iff)
then show "0 \ y\i"
using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format]
by (auto simp: inner_simps)
qed (use y2 in auto)
qed
then have "x \ rel_interior (convex hull (insert 0 D))"
using h0 h2 rel_interior_ball by force
}
ultimately have
"\x. x \ rel_interior (convex hull insert 0 D) \
x \<in> {x. (\<forall>i\<in>D. 0 < x \<bullet> i) \<and> sum ((\<bullet>) x) D < 1 \<and> (\<forall>i\<in>Basis. i \<notin> D \<longrightarrow> x \<bullet> i = 0)}"
by blast
then show ?thesis by (rule set_eqI)
qed
qed
lemma rel_interior_substd_simplex_nonempty:
assumes "D \ {}"
and "D \ Basis"
obtains a :: "'a::euclidean_space"
where "a \ rel_interior (convex hull (insert 0 D))"
proof -
let ?a = "sum (\b::'a::euclidean_space. inverse (2 * real (card D)) *\<^sub>R b) D"
have "finite D"
using assms finite_Basis infinite_super by blast
then have d1: "0 < real (card D)"
using \<open>D \<noteq> {}\<close> by auto
{
fix i
assume "i \ D"
have "?a \ i = sum (\j. if i = j then inverse (2 * real (card D)) else 0) D"
unfolding inner_sum_left
using \<open>i \<in> D\<close> by (auto simp: inner_Basis subsetD[OF assms(2)] intro: sum.cong)
also have "... = inverse (2 * real (card D))"
using \<open>i \<in> D\<close> \<open>finite D\<close> by auto
finally have "?a \ i = inverse (2 * real (card D))" .
}
note ** = this
show ?thesis
proof
show "?a \ rel_interior (convex hull (insert 0 D))"
unfolding rel_interior_substd_simplex[OF assms(2)]
proof safe
fix i
assume "i \ D"
have "0 < inverse (2 * real (card D))"
using d1 by auto
also have "\ = ?a \ i" using **[of i] \i \ D\
by auto
finally show "0 < ?a \ i" by auto
next
have "sum ((\) ?a) D = sum (\i. inverse (2 * real (card D))) D"
by (rule sum.cong) (rule refl, rule **)
also have "\ < 1"
unfolding sum_constant divide_real_def[symmetric]
by (auto simp add: field_simps)
finally show "sum ((\) ?a) D < 1" by auto
next
fix i
assume "i \ Basis" and "i \ D"
have "?a \ span D"
proof (rule span_sum[of D "(\b. b /\<^sub>R (2 * real (card D)))" D])
{
fix x :: "'a::euclidean_space"
assume "x \ D"
then have "x \ span D"
using span_base[of _ "D"] by auto
then have "x /\<^sub>R (2 * real (card D)) \ span D"
using span_mul[of x "D" "(inverse (real (card D)) / 2)"] by auto
}
then show "\x. x\D \ x /\<^sub>R (2 * real (card D)) \ span D"
by auto
qed
then show "?a \ i = 0 "
using \<open>i \<notin> D\<close> unfolding span_substd_basis[OF assms(2)] using \<open>i \<in> Basis\<close> by auto
qed
qed
qed
subsection\<^marker>\<open>tag unimportant\<close> \<open>Relative interior of convex set\<close>
lemma rel_interior_convex_nonempty_aux:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
and "0 \ S"
shows "rel_interior S \ {}"
proof (cases "S = {0}")
case True
then show ?thesis using rel_interior_sing by auto
next
case False
obtain B where B: "independent B \ B \ S \ S \ span B \ card B = dim S"
using basis_exists[of S] by metis
then have "B \ {}"
using B assms \<open>S \<noteq> {0}\<close> span_empty by auto
have "insert 0 B \ span B"
using subspace_span[of B] subspace_0[of "span B"]
span_superset by auto
then have "span (insert 0 B) \ span B"
using span_span[of B] span_mono[of "insert 0 B" "span B"] by blast
then have "convex hull insert 0 B \ span B"
using convex_hull_subset_span[of "insert 0 B"] by auto
then have "span (convex hull insert 0 B) \ span B"
using span_span[of B]
span_mono[of "convex hull insert 0 B" "span B"] by blast
then have *: "span (convex hull insert 0 B) = span B"
using span_mono[of B "convex hull insert 0 B"] hull_subset[of "insert 0 B"] by auto
then have "span (convex hull insert 0 B) = span S"
using B span_mono[of B S] span_mono[of S "span B"]
span_span[of B] by auto
moreover have "0 \ affine hull (convex hull insert 0 B)"
using hull_subset[of "convex hull insert 0 B"] hull_subset[of "insert 0 B"] by auto
ultimately have **: "affine hull (convex hull insert 0 B) = affine hull S"
using affine_hull_span_0[of "convex hull insert 0 B"] affine_hull_span_0[of "S"]
assms hull_subset[of S]
by auto
obtain d and f :: "'n \ 'n" where
fd: "card d = card B" "linear f" "f ` B = d"
"f ` span B = {x. \i\Basis. i \ d \ x \ i = (0::real)} \ inj_on f (span B)"
and d: "d \ Basis"
using basis_to_substdbasis_subspace_isomorphism[of B,OF _ ] B by auto
then have "bounded_linear f"
using linear_conv_bounded_linear by auto
have "d \ {}"
using fd B \<open>B \<noteq> {}\<close> by auto
have "insert 0 d = f ` (insert 0 B)"
using fd linear_0 by auto
then have "(convex hull (insert 0 d)) = f ` (convex hull (insert 0 B))"
using convex_hull_linear_image[of f "(insert 0 d)"]
convex_hull_linear_image[of f "(insert 0 B)"] \<open>linear f\<close>
by auto
moreover have "rel_interior (f ` (convex hull insert 0 B)) = f ` rel_interior (convex hull insert 0 B)"
proof (rule rel_interior_injective_on_span_linear_image[OF \<open>bounded_linear f\<close>])
show "inj_on f (span (convex hull insert 0 B))"
using fd * by auto
qed
ultimately have "rel_interior (convex hull insert 0 B) \ {}"
using rel_interior_substd_simplex_nonempty[OF \<open>d \<noteq> {}\<close> d] by fastforce
moreover have "convex hull (insert 0 B) \ S"
using B assms hull_mono[of "insert 0 B" "S" "convex"] convex_hull_eq by auto
ultimately show ?thesis
using subset_rel_interior[of "convex hull insert 0 B" S] ** by auto
qed
lemma rel_interior_eq_empty:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
shows "rel_interior S = {} \ S = {}"
proof -
{
assume "S \ {}"
then obtain a where "a \ S" by auto
then have "0 \ (+) (-a) ` S"
using assms exI[of "(\x. x \ S \ - a + x = 0)" a] by auto
then have "rel_interior ((+) (-a) ` S) \ {}"
using rel_interior_convex_nonempty_aux[of "(+) (-a) ` S"]
convex_translation[of S "-a"] assms
by auto
then have "rel_interior S \ {}"
using rel_interior_translation [of "- a"] by simp
}
then show ?thesis by auto
qed
lemma interior_simplex_nonempty:
fixes S :: "'N :: euclidean_space set"
assumes "independent S" "finite S" "card S = DIM('N)"
obtains a where "a \ interior (convex hull (insert 0 S))"
proof -
have "affine hull (insert 0 S) = UNIV"
by (simp add: hull_inc affine_hull_span_0 dim_eq_full[symmetric]
assms(1) assms(3) dim_eq_card_independent)
moreover have "rel_interior (convex hull insert 0 S) \ {}"
using rel_interior_eq_empty [of "convex hull (insert 0 S)"] by auto
ultimately have "interior (convex hull insert 0 S) \ {}"
by (simp add: rel_interior_interior)
with that show ?thesis
by auto
qed
lemma convex_rel_interior:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
shows "convex (rel_interior S)"
proof -
{
fix x y and u :: real
assume assm: "x \ rel_interior S" "y \ rel_interior S" "0 \ u" "u \ 1"
then have "x \ S"
using rel_interior_subset by auto
have "x - u *\<^sub>R (x-y) \ rel_interior S"
proof (cases "0 = u")
case False
then have "0 < u" using assm by auto
then show ?thesis
using assm rel_interior_convex_shrink[of S y x u] assms \<open>x \<in> S\<close> by auto
next
case True
then show ?thesis using assm by auto
qed
then have "(1 - u) *\<^sub>R x + u *\<^sub>R y \ rel_interior S"
by (simp add: algebra_simps)
}
then show ?thesis
unfolding convex_alt by auto
qed
lemma convex_closure_rel_interior:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
shows "closure (rel_interior S) = closure S"
proof -
have h1: "closure (rel_interior S) \ closure S"
using closure_mono[of "rel_interior S" S] rel_interior_subset[of S] by auto
show ?thesis
proof (cases "S = {}")
case False
then obtain a where a: "a \ rel_interior S"
using rel_interior_eq_empty assms by auto
{ fix x
assume x: "x \ closure S"
{
assume "x = a"
then have "x \ closure (rel_interior S)"
using a unfolding closure_def by auto
}
moreover
{
assume "x \ a"
{
fix e :: real
assume "e > 0"
define e1 where "e1 = min 1 (e/norm (x - a))"
then have e1: "e1 > 0" "e1 \ 1" "e1 * norm (x - a) \ e"
using \<open>x \<noteq> a\<close> \<open>e > 0\<close> le_divide_eq[of e1 e "norm (x - a)"]
by simp_all
then have *: "x - e1 *\<^sub>R (x - a) \ rel_interior S"
using rel_interior_closure_convex_shrink[of S a x e1] assms x a e1_def
by auto
have "\y. y \ rel_interior S \ y \ x \ dist y x \ e"
using "*" \<open>x \<noteq> a\<close> e1 by force
}
then have "x islimpt rel_interior S"
unfolding islimpt_approachable_le by auto
then have "x \ closure(rel_interior S)"
unfolding closure_def by auto
}
ultimately have "x \ closure(rel_interior S)" by auto
}
then show ?thesis using h1 by auto
qed auto
qed
lemma rel_interior_same_affine_hull:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
shows "affine hull (rel_interior S) = affine hull S"
by (metis assms closure_same_affine_hull convex_closure_rel_interior)
lemma rel_interior_aff_dim:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
shows "aff_dim (rel_interior S) = aff_dim S"
by (metis aff_dim_affine_hull2 assms rel_interior_same_affine_hull)
lemma rel_interior_rel_interior:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
shows "rel_interior (rel_interior S) = rel_interior S"
proof -
have "openin (top_of_set (affine hull (rel_interior S))) (rel_interior S)"
using openin_rel_interior[of S] rel_interior_same_affine_hull[of S] assms by auto
then show ?thesis
using rel_interior_def by auto
qed
lemma rel_interior_rel_open:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
shows "rel_open (rel_interior S)"
unfolding rel_open_def using rel_interior_rel_interior assms by auto
lemma convex_rel_interior_closure_aux:
fixes x y z :: "'n::euclidean_space"
assumes "0 < a" "0 < b" "(a + b) *\<^sub>R z = a *\<^sub>R x + b *\<^sub>R y"
obtains e where "0 < e" "e < 1" "z = y - e *\<^sub>R (y - x)"
proof -
define e where "e = a / (a + b)"
have "z = (1 / (a + b)) *\<^sub>R ((a + b) *\<^sub>R z)"
using assms by (simp add: eq_vector_fraction_iff)
also have "\ = (1 / (a + b)) *\<^sub>R (a *\<^sub>R x + b *\<^sub>R y)"
using assms scaleR_cancel_left[of "1/(a+b)" "(a + b) *\<^sub>R z" "a *\<^sub>R x + b *\<^sub>R y"]
by auto
also have "\ = y - e *\<^sub>R (y-x)"
using e_def assms
by (simp add: divide_simps vector_fraction_eq_iff) (simp add: algebra_simps)
finally have "z = y - e *\<^sub>R (y-x)"
by auto
moreover have "e > 0" "e < 1" using e_def assms by auto
ultimately show ?thesis using that[of e] by auto
qed
lemma convex_rel_interior_closure:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
shows "rel_interior (closure S) = rel_interior S"
proof (cases "S = {}")
case True
then show ?thesis
using assms rel_interior_eq_empty by auto
next
case False
have "rel_interior (closure S) \ rel_interior S"
using subset_rel_interior[of S "closure S"] closure_same_affine_hull closure_subset
by auto
moreover
{
fix z
assume z: "z \ rel_interior (closure S)"
obtain x where x: "x \ rel_interior S"
using \<open>S \<noteq> {}\<close> assms rel_interior_eq_empty by auto
have "z \ rel_interior S"
proof (cases "x = z")
case True
then show ?thesis using x by auto
next
case False
obtain e where e: "e > 0" "cball z e \ affine hull closure S \ closure S"
using z rel_interior_cball[of "closure S"] by auto
hence *: "0 < e/norm(z-x)" using e False by auto
define y where "y = z + (e/norm(z-x)) *\<^sub>R (z-x)"
have yball: "y \ cball z e"
using y_def dist_norm[of z y] e by auto
have "x \ affine hull closure S"
using x rel_interior_subset_closure hull_inc[of x "closure S"] by blast
moreover have "z \ affine hull closure S"
using z rel_interior_subset hull_subset[of "closure S"] by blast
ultimately have "y \ affine hull closure S"
using y_def affine_affine_hull[of "closure S"]
mem_affine_3_minus [of "affine hull closure S" z z x "e/norm(z-x)"] by auto
then have "y \ closure S" using e yball by auto
have "(1 + (e/norm(z-x))) *\<^sub>R z = (e/norm(z-x)) *\<^sub>R x + y"
using y_def by (simp add: algebra_simps)
then obtain e1 where "0 < e1" "e1 < 1" "z = y - e1 *\<^sub>R (y - x)"
using * convex_rel_interior_closure_aux[of "e / norm (z - x)" 1 z x y]
by (auto simp add: algebra_simps)
then show ?thesis
using rel_interior_closure_convex_shrink assms x \<open>y \<in> closure S\<close>
by fastforce
qed
}
ultimately show ?thesis by auto
qed
lemma convex_interior_closure:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
shows "interior (closure S) = interior S"
using closure_aff_dim[of S] interior_rel_interior_gen[of S]
interior_rel_interior_gen[of "closure S"]
convex_rel_interior_closure[of S] assms
by auto
lemma closure_eq_rel_interior_eq:
fixes S1 S2 :: "'n::euclidean_space set"
assumes "convex S1"
and "convex S2"
shows "closure S1 = closure S2 \ rel_interior S1 = rel_interior S2"
by (metis convex_rel_interior_closure convex_closure_rel_interior assms)
lemma closure_eq_between:
fixes S1 S2 :: "'n::euclidean_space set"
assumes "convex S1"
and "convex S2"
shows "closure S1 = closure S2 \ rel_interior S1 \ S2 \ S2 \ closure S1"
(is "?A \ ?B")
proof
assume ?A
then show ?B
by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset)
next
assume ?B
then have "closure S1 \ closure S2"
by (metis assms(1) convex_closure_rel_interior closure_mono)
moreover from \<open>?B\<close> have "closure S1 \<supseteq> closure S2"
by (metis closed_closure closure_minimal)
ultimately show ?A ..
qed
lemma open_inter_closure_rel_interior:
fixes S A :: "'n::euclidean_space set"
assumes "convex S"
and "open A"
shows "A \ closure S = {} \ A \ rel_interior S = {}"
by (metis assms convex_closure_rel_interior open_Int_closure_eq_empty)
lemma rel_interior_open_segment:
fixes a :: "'a :: euclidean_space"
shows "rel_interior(open_segment a b) = open_segment a b"
proof (cases "a = b")
case True then show ?thesis by auto
next
case False then
have "open_segment a b = affine hull {a, b} \ ball ((a + b) /\<^sub>R 2) (norm (b - a) / 2)"
by (simp add: open_segment_as_ball)
then show ?thesis
unfolding rel_interior_eq openin_open
by (metis Elementary_Metric_Spaces.open_ball False affine_hull_open_segment)
qed
lemma rel_interior_closed_segment:
fixes a :: "'a :: euclidean_space"
shows "rel_interior(closed_segment a b) =
(if a = b then {a} else open_segment a b)"
proof (cases "a = b")
case True then show ?thesis by auto
next
case False then show ?thesis
by simp
(metis closure_open_segment convex_open_segment convex_rel_interior_closure
rel_interior_open_segment)
qed
lemmas rel_interior_segment = rel_interior_closed_segment rel_interior_open_segment
subsection\<open>The relative frontier of a set\<close>
definition\<^marker>\<open>tag important\<close> "rel_frontier S = closure S - rel_interior S"
lemma rel_frontier_empty [simp]: "rel_frontier {} = {}"
by (simp add: rel_frontier_def)
lemma rel_frontier_eq_empty:
fixes S :: "'n::euclidean_space set"
shows "rel_frontier S = {} \ affine S"
unfolding rel_frontier_def
using rel_interior_subset_closure by (auto simp add: rel_interior_eq_closure [symmetric])
lemma rel_frontier_sing [simp]:
fixes a :: "'n::euclidean_space"
shows "rel_frontier {a} = {}"
by (simp add: rel_frontier_def)
lemma rel_frontier_affine_hull:
fixes S :: "'a::euclidean_space set"
shows "rel_frontier S \ affine hull S"
using closure_affine_hull rel_frontier_def by fastforce
lemma rel_frontier_cball [simp]:
fixes a :: "'n::euclidean_space"
shows "rel_frontier(cball a r) = (if r = 0 then {} else sphere a r)"
proof (cases rule: linorder_cases [of r 0])
case less then show ?thesis
by (force simp: sphere_def)
next
case equal then show ?thesis by simp
next
case greater then show ?thesis
by simp (metis centre_in_ball empty_iff frontier_cball frontier_def interior_cball interior_rel_interior_gen rel_frontier_def)
qed
lemma rel_frontier_translation:
fixes a :: "'a::euclidean_space"
shows "rel_frontier((\x. a + x) ` S) = (\x. a + x) ` (rel_frontier S)"
by (simp add: rel_frontier_def translation_diff rel_interior_translation closure_translation)
lemma rel_frontier_nonempty_interior:
fixes S :: "'n::euclidean_space set"
shows "interior S \ {} \ rel_frontier S = frontier S"
by (metis frontier_def interior_rel_interior_gen rel_frontier_def)
lemma rel_frontier_frontier:
fixes S :: "'n::euclidean_space set"
shows "affine hull S = UNIV \ rel_frontier S = frontier S"
by (simp add: frontier_def rel_frontier_def rel_interior_interior)
lemma closest_point_in_rel_frontier:
"\closed S; S \ {}; x \ affine hull S - rel_interior S\
\<Longrightarrow> closest_point S x \<in> rel_frontier S"
by (simp add: closest_point_in_rel_interior closest_point_in_set rel_frontier_def)
lemma closed_rel_frontier [iff]:
fixes S :: "'n::euclidean_space set"
shows "closed (rel_frontier S)"
proof -
have *: "closedin (top_of_set (affine hull S)) (closure S - rel_interior S)"
by (simp add: closed_subset closedin_diff closure_affine_hull openin_rel_interior)
show ?thesis
proof (rule closedin_closed_trans[of "affine hull S" "rel_frontier S"])
show "closedin (top_of_set (affine hull S)) (rel_frontier S)"
by (simp add: "*" rel_frontier_def)
qed simp
qed
lemma closed_rel_boundary:
fixes S :: "'n::euclidean_space set"
shows "closed S \ closed(S - rel_interior S)"
by (metis closed_rel_frontier closure_closed rel_frontier_def)
lemma compact_rel_boundary:
fixes S :: "'n::euclidean_space set"
shows "compact S \ compact(S - rel_interior S)"
by (metis bounded_diff closed_rel_boundary closure_eq compact_closure compact_imp_closed)
lemma bounded_rel_frontier:
fixes S :: "'n::euclidean_space set"
shows "bounded S \ bounded(rel_frontier S)"
by (simp add: bounded_closure bounded_diff rel_frontier_def)
lemma compact_rel_frontier_bounded:
fixes S :: "'n::euclidean_space set"
shows "bounded S \ compact(rel_frontier S)"
using bounded_rel_frontier closed_rel_frontier compact_eq_bounded_closed by blast
lemma compact_rel_frontier:
fixes S :: "'n::euclidean_space set"
shows "compact S \ compact(rel_frontier S)"
by (meson compact_eq_bounded_closed compact_rel_frontier_bounded)
lemma convex_same_rel_interior_closure:
fixes S :: "'n::euclidean_space set"
shows "\convex S; convex T\
\<Longrightarrow> rel_interior S = rel_interior T \<longleftrightarrow> closure S = closure T"
by (simp add: closure_eq_rel_interior_eq)
lemma convex_same_rel_interior_closure_straddle:
fixes S :: "'n::euclidean_space set"
shows "\convex S; convex T\
\<Longrightarrow> rel_interior S = rel_interior T \<longleftrightarrow>
rel_interior S \<subseteq> T \<and> T \<subseteq> closure S"
by (simp add: closure_eq_between convex_same_rel_interior_closure)
lemma convex_rel_frontier_aff_dim:
fixes S1 S2 :: "'n::euclidean_space set"
assumes "convex S1"
and "convex S2"
and "S2 \ {}"
and "S1 \ rel_frontier S2"
shows "aff_dim S1 < aff_dim S2"
proof -
have "S1 \ closure S2"
using assms unfolding rel_frontier_def by auto
then have *: "affine hull S1 \ affine hull S2"
using hull_mono[of "S1" "closure S2"] closure_same_affine_hull[of S2] by blast
then have "aff_dim S1 \ aff_dim S2"
using * aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2]
aff_dim_subset[of "affine hull S1" "affine hull S2"]
by auto
moreover
{
assume eq: "aff_dim S1 = aff_dim S2"
then have "S1 \ {}"
using aff_dim_empty[of S1] aff_dim_empty[of S2] \<open>S2 \<noteq> {}\<close> by auto
have **: "affine hull S1 = affine hull S2"
by (simp_all add: * eq \<open>S1 \<noteq> {}\<close> affine_dim_equal)
obtain a where a: "a \ rel_interior S1"
using \<open>S1 \<noteq> {}\<close> rel_interior_eq_empty assms by auto
obtain T where T: "open T" "a \ T \ S1" "T \ affine hull S1 \ S1"
using mem_rel_interior[of a S1] a by auto
then have "a \ T \ closure S2"
using a assms unfolding rel_frontier_def by auto
then obtain b where b: "b \ T \ rel_interior S2"
using open_inter_closure_rel_interior[of S2 T] assms T by auto
then have "b \ affine hull S1"
using rel_interior_subset hull_subset[of S2] ** by auto
then have "b \ S1"
using T b by auto
then have False
using b assms unfolding rel_frontier_def by auto
}
ultimately show ?thesis
using less_le by auto
qed
lemma convex_rel_interior_if:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
and "z \ rel_interior S"
shows "\x\affine hull S. \m. m > 1 \ (\e. e > 1 \ e \ m \ (1 - e) *\<^sub>R x + e *\<^sub>R z \ S)"
proof -
obtain e1 where e1: "e1 > 0 \ cball z e1 \ affine hull S \ S"
using mem_rel_interior_cball[of z S] assms by auto
{
fix x
assume x: "x \ affine hull S"
{
assume "x \ z"
define m where "m = 1 + e1/norm(x-z)"
hence "m > 1" using e1 \<open>x \<noteq> z\<close> by auto
{
fix e
assume e: "e > 1 \ e \ m"
have "z \ affine hull S"
using assms rel_interior_subset hull_subset[of S] by auto
then have *: "(1 - e)*\<^sub>R x + e *\<^sub>R z \ affine hull S"
using mem_affine[of "affine hull S" x z "(1-e)" e] affine_affine_hull[of S] x
by auto
have "norm (z + e *\<^sub>R x - (x + e *\<^sub>R z)) = norm ((e - 1) *\<^sub>R (x - z))"
by (simp add: algebra_simps)
also have "\ = (e - 1) * norm (x-z)"
using norm_scaleR e by auto
also have "\ \ (m - 1) * norm (x - z)"
using e mult_right_mono[of _ _ "norm(x-z)"] by auto
also have "\ = (e1 / norm (x - z)) * norm (x - z)"
using m_def by auto
also have "\ = e1"
using \<open>x \<noteq> z\<close> e1 by simp
finally have **: "norm (z + e *\<^sub>R x - (x + e *\<^sub>R z)) \ e1"
by auto
have "(1 - e)*\<^sub>R x+ e *\<^sub>R z \ cball z e1"
using m_def **
unfolding cball_def dist_norm
by (auto simp add: algebra_simps)
then have "(1 - e) *\<^sub>R x+ e *\<^sub>R z \ S"
using e * e1 by auto
}
then have "\m. m > 1 \ (\e. e > 1 \ e \ m \ (1 - e) *\<^sub>R x + e *\<^sub>R z \ S )"
using \<open>m> 1 \<close> by auto
}
moreover
{
assume "x = z"
define m where "m = 1 + e1"
then have "m > 1"
using e1 by auto
{
fix e
assume e: "e > 1 \ e \ m"
then have "(1 - e) *\<^sub>R x + e *\<^sub>R z \ S"
using e1 x \<open>x = z\<close> by (auto simp add: algebra_simps)
then have "(1 - e) *\<^sub>R x + e *\<^sub>R z \ S"
using e by auto
}
then have "\m. m > 1 \ (\e. e > 1 \ e \ m \ (1 - e) *\<^sub>R x + e *\<^sub>R z \ S)"
using \<open>m > 1\<close> by auto
}
ultimately have "\m. m > 1 \ (\e. e > 1 \ e \ m \ (1 - e) *\<^sub>R x + e *\<^sub>R z \ S )"
by blast
}
then show ?thesis by auto
qed
lemma convex_rel_interior_if2:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
assumes "z \ rel_interior S"
shows "\x\affine hull S. \e. e > 1 \ (1 - e)*\<^sub>R x + e *\<^sub>R z \ S"
using convex_rel_interior_if[of S z] assms by auto
lemma convex_rel_interior_only_if:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
and "S \ {}"
assumes "\x\S. \e. e > 1 \ (1 - e) *\<^sub>R x + e *\<^sub>R z \ S"
shows "z \ rel_interior S"
proof -
obtain x where x: "x \ rel_interior S"
using rel_interior_eq_empty assms by auto
then have "x \ S"
using rel_interior_subset by auto
then obtain e where e: "e > 1 \ (1 - e) *\<^sub>R x + e *\<^sub>R z \ S"
using assms by auto
define y where [abs_def]: "y = (1 - e) *\<^sub>R x + e *\<^sub>R z"
then have "y \ S" using e by auto
define e1 where "e1 = 1/e"
then have "0 < e1 \ e1 < 1" using e by auto
then have "z =y - (1 - e1) *\<^sub>R (y - x)"
using e1_def y_def by (auto simp add: algebra_simps)
then show ?thesis
using rel_interior_convex_shrink[of S x y "1-e1"] \<open>0 < e1 \<and> e1 < 1\<close> \<open>y \<in> S\<close> x assms
by auto
qed
lemma convex_rel_interior_iff:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
and "S \ {}"
shows "z \ rel_interior S \ (\x\S. \e. e > 1 \ (1 - e) *\<^sub>R x + e *\<^sub>R z \ S)"
using assms hull_subset[of S "affine"]
convex_rel_interior_if[of S z] convex_rel_interior_only_if[of S z]
by auto
lemma convex_rel_interior_iff2:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
and "S \ {}"
shows "z \ rel_interior S \ (\x\affine hull S. \e. e > 1 \ (1 - e) *\<^sub>R x + e *\<^sub>R z \ S)"
using assms hull_subset[of S] convex_rel_interior_if2[of S z] convex_rel_interior_only_if[of S z]
by auto
lemma convex_interior_iff:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
shows "z \ interior S \ (\x. \e. e > 0 \ z + e *\<^sub>R x \ S)"
proof (cases "aff_dim S = int DIM('n)")
case False
{ assume "z \ interior S"
then have False
using False interior_rel_interior_gen[of S] by auto }
moreover
{ assume r: "\x. \e. e > 0 \ z + e *\<^sub>R x \ S"
{ fix x
obtain e1 where e1: "e1 > 0 \ z + e1 *\<^sub>R (x - z) \ S"
using r by auto
obtain e2 where e2: "e2 > 0 \ z + e2 *\<^sub>R (z - x) \ S"
using r by auto
define x1 where [abs_def]: "x1 = z + e1 *\<^sub>R (x - z)"
then have x1: "x1 \ affine hull S"
using e1 hull_subset[of S] by auto
define x2 where [abs_def]: "x2 = z + e2 *\<^sub>R (z - x)"
then have x2: "x2 \ affine hull S"
using e2 hull_subset[of S] by auto
have *: "e1/(e1+e2) + e2/(e1+e2) = 1"
using add_divide_distrib[of e1 e2 "e1+e2"] e1 e2 by simp
then have "z = (e2/(e1+e2)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2"
by (simp add: x1_def x2_def algebra_simps) (simp add: "*" pth_8)
then have z: "z \ affine hull S"
using mem_affine[of "affine hull S" x1 x2 "e2/(e1+e2)" "e1/(e1+e2)"]
x1 x2 affine_affine_hull[of S] *
by auto
have "x1 - x2 = (e1 + e2) *\<^sub>R (x - z)"
using x1_def x2_def by (auto simp add: algebra_simps)
then have "x = z+(1/(e1+e2)) *\<^sub>R (x1-x2)"
using e1 e2 by simp
then have "x \ affine hull S"
using mem_affine_3_minus[of "affine hull S" z x1 x2 "1/(e1+e2)"]
x1 x2 z affine_affine_hull[of S]
by auto
}
then have "affine hull S = UNIV"
by auto
then have "aff_dim S = int DIM('n)"
using aff_dim_affine_hull[of S] by (simp)
then have False
using False by auto
}
ultimately show ?thesis by auto
next
case True
then have "S \ {}"
using aff_dim_empty[of S] by auto
have *: "affine hull S = UNIV"
using True affine_hull_UNIV by auto
{
assume "z \ interior S"
then have "z \ rel_interior S"
using True interior_rel_interior_gen[of S] by auto
then have **: "\x. \e. e > 1 \ (1 - e) *\<^sub>R x + e *\<^sub>R z \ S"
using convex_rel_interior_iff2[of S z] assms \<open>S \<noteq> {}\<close> * by auto
fix x
obtain e1 where e1: "e1 > 1" "(1 - e1) *\<^sub>R (z - x) + e1 *\<^sub>R z \ S"
using **[rule_format, of "z-x"] by auto
define e where [abs_def]: "e = e1 - 1"
then have "(1 - e1) *\<^sub>R (z - x) + e1 *\<^sub>R z = z + e *\<^sub>R x"
by (simp add: algebra_simps)
then have "e > 0" "z + e *\<^sub>R x \ S"
using e1 e_def by auto
then have "\e. e > 0 \ z + e *\<^sub>R x \ S"
by auto
}
moreover
{
assume r: "\x. \e. e > 0 \ z + e *\<^sub>R x \ S"
{
fix x
obtain e1 where e1: "e1 > 0" "z + e1 *\<^sub>R (z - x) \ S"
using r[rule_format, of "z-x"] by auto
define e where "e = e1 + 1"
then have "z + e1 *\<^sub>R (z - x) = (1 - e) *\<^sub>R x + e *\<^sub>R z"
by (simp add: algebra_simps)
then have "e > 1" "(1 - e)*\<^sub>R x + e *\<^sub>R z \ S"
using e1 e_def by auto
then have "\e. e > 1 \ (1 - e) *\<^sub>R x + e *\<^sub>R z \ S" by auto
}
then have "z \ rel_interior S"
using convex_rel_interior_iff2[of S z] assms \<open>S \<noteq> {}\<close> by auto
then have "z \ interior S"
using True interior_rel_interior_gen[of S] by auto
}
ultimately show ?thesis by auto
qed
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Relative interior and closure under common operations\<close>
lemma rel_interior_inter_aux: "\{rel_interior S |S. S \ I} \ \I"
proof -
{
fix y
assume "y \ \{rel_interior S |S. S \ I}"
then have y: "\S \ I. y \ rel_interior S"
by auto
{
fix S
assume "S \ I"
then have "y \ S"
using rel_interior_subset y by auto
}
then have "y \ \I" by auto
}
then show ?thesis by auto
qed
lemma convex_closure_rel_interior_inter:
assumes "\S\I. convex (S :: 'n::euclidean_space set)"
and "\{rel_interior S |S. S \ I} \ {}"
shows "\{closure S |S. S \ I} \ closure (\{rel_interior S |S. S \ I})"
proof -
obtain x where x: "\S\I. x \ rel_interior S"
using assms by auto
{
fix y
assume "y \ \{closure S |S. S \ I}"
then have y: "\S \ I. y \ closure S"
by auto
{
assume "y = x"
then have "y \ closure (\{rel_interior S |S. S \ I})"
using x closure_subset[of "\{rel_interior S |S. S \ I}"] by auto
}
moreover
{
assume "y \ x"
{ fix e :: real
assume e: "e > 0"
define e1 where "e1 = min 1 (e/norm (y - x))"
then have e1: "e1 > 0" "e1 \ 1" "e1 * norm (y - x) \ e"
using \<open>y \<noteq> x\<close> \<open>e > 0\<close> le_divide_eq[of e1 e "norm (y - x)"]
by simp_all
define z where "z = y - e1 *\<^sub>R (y - x)"
{
fix S
assume "S \ I"
then have "z \ rel_interior S"
using rel_interior_closure_convex_shrink[of S x y e1] assms x y e1 z_def
by auto
}
then have *: "z \ \{rel_interior S |S. S \ I}"
by auto
have "\z. z \ \{rel_interior S |S. S \ I} \ z \ y \ dist z y \ e"
using \<open>y \<noteq> x\<close> z_def * e1 e dist_norm[of z y]
by (rule_tac x="z" in exI) auto
}
then have "y islimpt \{rel_interior S |S. S \ I}"
unfolding islimpt_approachable_le by blast
then have "y \ closure (\{rel_interior S |S. S \ I})"
unfolding closure_def by auto
}
ultimately have "y \ closure (\{rel_interior S |S. S \ I})"
by auto
}
then show ?thesis by auto
qed
lemma convex_closure_inter:
assumes "\S\I. convex (S :: 'n::euclidean_space set)"
and "\{rel_interior S |S. S \ I} \ {}"
shows "closure (\I) = \{closure S |S. S \ I}"
proof -
have "\{closure S |S. S \ I} \ closure (\{rel_interior S |S. S \ I})"
using convex_closure_rel_interior_inter assms by auto
moreover
have "closure (\{rel_interior S |S. S \ I}) \ closure (\I)"
using rel_interior_inter_aux closure_mono[of "\{rel_interior S |S. S \ I}" "\I"]
by auto
ultimately show ?thesis
using closure_Int[of I] by auto
qed
lemma convex_inter_rel_interior_same_closure:
assumes "\S\I. convex (S :: 'n::euclidean_space set)"
and "\{rel_interior S |S. S \ I} \ {}"
shows "closure (\{rel_interior S |S. S \ I}) = closure (\I)"
proof -
have "\{closure S |S. S \ I} \ closure (\{rel_interior S |S. S \ I})"
using convex_closure_rel_interior_inter assms by auto
moreover
have "closure (\{rel_interior S |S. S \ I}) \ closure (\I)"
using rel_interior_inter_aux closure_mono[of "\{rel_interior S |S. S \ I}" "\I"]
by auto
ultimately show ?thesis
using closure_Int[of I] by auto
qed
lemma convex_rel_interior_inter:
assumes "\S\I. convex (S :: 'n::euclidean_space set)"
and "\{rel_interior S |S. S \ I} \ {}"
shows "rel_interior (\I) \ \{rel_interior S |S. S \ I}"
proof -
have "convex (\I)"
using assms convex_Inter by auto
moreover
have "convex (\{rel_interior S |S. S \ I})"
using assms convex_rel_interior by (force intro: convex_Inter)
ultimately
have "rel_interior (\{rel_interior S |S. S \ I}) = rel_interior (\I)"
using convex_inter_rel_interior_same_closure assms
closure_eq_rel_interior_eq[of "\{rel_interior S |S. S \ I}" "\I"]
by blast
then show ?thesis
using rel_interior_subset[of "\{rel_interior S |S. S \ I}"] by auto
qed
lemma convex_rel_interior_finite_inter:
assumes "\S\I. convex (S :: 'n::euclidean_space set)"
and "\{rel_interior S |S. S \ I} \ {}"
and "finite I"
shows "rel_interior (\I) = \{rel_interior S |S. S \ I}"
proof -
have "\I \ {}"
using assms rel_interior_inter_aux[of I] by auto
have "convex (\I)"
using convex_Inter assms by auto
show ?thesis
proof (cases "I = {}")
case True
then show ?thesis
using Inter_empty rel_interior_UNIV by auto
next
case False
{
fix z
assume z: "z \ \{rel_interior S |S. S \ I}"
{
fix x
assume x: "x \ \I"
{
fix S
assume S: "S \ I"
then have "z \ rel_interior S" "x \ S"
using z x by auto
then have "\m. m > 1 \ (\e. e > 1 \ e \ m \ (1 - e)*\<^sub>R x + e *\<^sub>R z \ S)"
using convex_rel_interior_if[of S z] S assms hull_subset[of S] by auto
}
then obtain mS where
mS: "\S\I. mS S > 1 \ (\e. e > 1 \ e \ mS S \ (1 - e) *\<^sub>R x + e *\<^sub>R z \ S)" by metis
define e where "e = Min (mS ` I)"
then have "e \ mS ` I" using assms \I \ {}\ by simp
then have "e > 1" using mS by auto
moreover have "\S\I. e \ mS S"
using e_def assms by auto
ultimately have "\e > 1. (1 - e) *\<^sub>R x + e *\<^sub>R z \ \I"
using mS by auto
}
then have "z \ rel_interior (\I)"
using convex_rel_interior_iff[of "\I" z] \\I \ {}\ \convex (\I)\ by auto
}
then show ?thesis
using convex_rel_interior_inter[of I] assms by auto
qed
qed
lemma convex_closure_inter_two:
fixes S T :: "'n::euclidean_space set"
assumes "convex S"
and "convex T"
assumes "rel_interior S \ rel_interior T \ {}"
shows "closure (S \ T) = closure S \ closure T"
using convex_closure_inter[of "{S,T}"] assms by auto
lemma convex_rel_interior_inter_two:
fixes S T :: "'n::euclidean_space set"
assumes "convex S"
and "convex T"
and "rel_interior S \ rel_interior T \ {}"
shows "rel_interior (S \ T) = rel_interior S \ rel_interior T"
using convex_rel_interior_finite_inter[of "{S,T}"] assms by auto
lemma convex_affine_closure_Int:
fixes S T :: "'n::euclidean_space set"
assumes "convex S"
and "affine T"
and "rel_interior S \ T \ {}"
shows "closure (S \ T) = closure S \ T"
proof -
have "affine hull T = T"
using assms by auto
then have "rel_interior T = T"
using rel_interior_affine_hull[of T] by metis
moreover have "closure T = T"
using assms affine_closed[of T] by auto
ultimately show ?thesis
using convex_closure_inter_two[of S T] assms affine_imp_convex by auto
qed
lemma connected_component_1_gen:
fixes S :: "'a :: euclidean_space set"
assumes "DIM('a) = 1"
shows "connected_component S a b \ closed_segment a b \ S"
unfolding connected_component_def
by (metis (no_types, lifting) assms subsetD subsetI convex_contains_segment convex_segment(1)
ends_in_segment connected_convex_1_gen)
lemma connected_component_1:
fixes S :: "real set"
shows "connected_component S a b \ closed_segment a b \ S"
by (simp add: connected_component_1_gen)
lemma convex_affine_rel_interior_Int:
fixes S T :: "'n::euclidean_space set"
assumes "convex S"
and "affine T"
and "rel_interior S \ T \ {}"
shows "rel_interior (S \ T) = rel_interior S \ T"
proof -
have "affine hull T = T"
using assms by auto
then have "rel_interior T = T"
using rel_interior_affine_hull[of T] by metis
moreover have "closure T = T"
using assms affine_closed[of T] by auto
ultimately show ?thesis
using convex_rel_interior_inter_two[of S T] assms affine_imp_convex by auto
qed
lemma convex_affine_rel_frontier_Int:
fixes S T :: "'n::euclidean_space set"
assumes "convex S"
and "affine T"
and "interior S \ T \ {}"
shows "rel_frontier(S \ T) = frontier S \ T"
using assms
unfolding rel_frontier_def frontier_def
using convex_affine_closure_Int convex_affine_rel_interior_Int rel_interior_nonempty_interior by fastforce
lemma rel_interior_convex_Int_affine:
fixes S :: "'a::euclidean_space set"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.71 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
