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) *R a + u *R b = b - (1 - u) *R (b - a)"for u by (simp add: algebra_simps) assume"x ∈ open_segment a b" thenshow"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 ∪x ∈ 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)
{ 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 ‹convex C›‹T ⊆ C› closure_subset contra_subsetD convex_hull_eq hull_mono) moreoverhave"x ∉ rel_interior C" by (meson ‹x ∈ S› dis disjnt_iff) moreoverhave"x ∈ open_segment z y ∪ {z, y}" using‹x ∈ closed_segment z y› closed_segment_eq_open by blast ultimatelyhave"x ∈ convex hull T" using rel_interior_closure_convex_segment [OF ‹convex C› z] using y z by blast
} with * show"?lhs ⊆ ?rhs" by (auto simp add: convex_hull_insert_segments) show"?rhs ⊆ ?lhs" by (meson hull_mono inf_mono subset_insertI subset_refl) qed
subsection✐‹tag unimportant›‹Shrinking towards the interior of a convex set›
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 *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 *R (x - c)) (e*d)" thenhave as: "dist (x - e *R (x - c)) y < e * d" by simp have *: "y = (1 - (1 - e)) *R ((1 / e) *R y - ((1 - e) / e) *R x) + (1 - e) *R x" using‹e > 0›by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib) have"c - ((1 / e) *R y - ((1 - e) / e) *R x) = (1 / e) *R (e *R c - y + (1 - e) *R x)" using‹e > 0› by (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps) thenhave"dist c ((1 / e) *R y - ((1 - e) / e) *R x) = ∣1/e∣ * norm (e *R c - y + (1 - e) *R x)" by (simp add: dist_norm) alsohave"… = ∣1/e∣ * norm (x - e *R (x - c) - y)" by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps) alsohave"… < d" using as[unfolded dist_norm] and‹e > 0› by (auto simp add:pos_divide_less_eq[OF ‹e > 0›] mult.commute) finallyhave"(1 - (1 - e)) *R ((1 / e) *R y - ((1 - e) / e) *R x) + (1 - e) *R x ∈ S" using assms(3-5) d by (intro convexD_alt [OF ‹convex S›]) (auto intro: convexD_alt [OF ‹convex S›]) with‹e > 0›show"y ∈ S" by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib) qed (use‹e>0›‹d>0›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 *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 thenshow ?thesis using‹e > 0›‹d > 0›by force next case False thenhave 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 thenshow ?thesis using True ‹0 < d›by auto next case False thenhave"0 < e * d / (1 - e)"and *: "1 - e > 0" using‹e ≤ 1›‹e > 0›‹d > 0›by auto thenobtain y where"y ∈ S""y ≠ x""dist y x < e * d / (1 - e)" using islimpt_approachable x by blast thenhave"norm (y - x) * (1 - e) < e * d" by (metis "*" dist_norm mult_imp_div_pos_le not_less) thenshow ?thesis using‹y ∈ S›by blast qed qed thenobtain y where"y ∈ S"and y: "norm (y - x) * (1 - e) < e * d" by auto define z where"z = c + ((1 - e) / e) *R (x - y)" have *: "x - e *R (x - c) = y - e *R (y - z)" unfolding z_def using‹e > 0› 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 ‹0 < e›by (simp add: field_simps norm_minus_commute) thenhave"z ∈ interior (ball c d)" using‹0 < e›‹e ≤ 1›by (simp add: interior_open[OF open_ball] z_def dist_norm) thenhave"z ∈ interior S" using d interiorI interior_ball by blast thenshow ?thesis unfolding * using mem_interior_convex_shrink ‹y ∈ S› 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 -
{ fix u::real assume u: "0 < u""u < 1" have"(1 - u) *R a + u *R b = b - (1 - u) *R (b - a)" by (simp add: algebra_simps) alsohave"... ∈ interior S"using mem_interior_closure_convex_shrink [OF assms] u by simp finallyhave"(1 - u) *R a + u *R b ∈ interior S" .
} thenshow ?thesis by (clarsimp simp: in_segment) 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 thenshow ?thesis using‹a ∈ interior S› closure_subset by blast next case False
{ fix e::real assume xnotS: "x ∉ interior S"and"0 < e" have"∃x'∈interior S. x' ≠ x ∧ dist x' x < e" proof (intro bexI conjI) show"x - min (e/2 / norm (x - a)) 1 *R (x - a) ≠ x" using False ‹0 < e›by (auto simp: algebra_simps min_def) show"dist (x - min (e/2 / norm (x - a)) 1 *R (x - a)) x < e" using‹0 < e›by (auto simp: dist_norm min_def) show"x - min (e/2 / norm (x - a)) 1 *R (x - a) ∈ interior S" using‹0 < e› False by (auto simp add: min_def a intro: mem_interior_closure_convex_shrink [OF ‹convex S› a x]) qed
} thenshow ?thesis by (auto simp add: closure_def islimpt_approachable) qed qed thenshow ?thesis by (simp add: closure_mono interior_subset subset_antisym) qed
lemma openin_subset_relative_interior: fixes S :: "'a::euclidean_space set" shows"openin (top_of_set (affine hull T)) S ==> (S ⊆ rel_interior T) = (S ⊆ T)" by (meson order.trans rel_interior_maximal rel_interior_subset)
lemma conic_hull_eq_span_affine_hull: fixes S :: "'a::euclidean_space set" assumes"0 ∈ rel_interior S" shows"conic hull S = span S ∧ conic hull S = affine hull S" proof - obtain ε where"ε>0"and ε: "cball 0 ε ∩ affine hull S ⊆ S" using assms mem_rel_interior_cball by blast have *: "affine hull S = span S" by (meson affine_hull_span_0 assms hull_inc mem_rel_interior_cball) moreover have"conic hull S ⊆ span S" by (simp add: hull_minimal span_superset) moreover
{ fix x assume"x ∈ affine hull S" have"x ∈ conic hull S" proof (cases "x=0") case True thenshow ?thesis using‹x ∈ affine hull S›by auto next case False thenhave"(ε / norm x) *R x ∈ cball 0 ε ∩ affine hull S" using‹0 < \ε›‹x ∈ affine hull S› * span_mul by fastforce thenhave"(ε / norm x) *R x ∈ S" by (meson ε subsetD) thenhave"∃c xa. x = c *R xa ∧ 0 ≤ c ∧ xa ∈ S" by (smt (verit, del_insts) ‹0 < \ε› divide_nonneg_nonneg eq_vector_fraction_iff norm_eq_zero norm_ge_zero) thenshow ?thesis by (simp add: conic_hull_explicit) qed
} thenhave"affine hull S ⊆ conic hull S" by auto ultimatelyshow ?thesis by blast qed
lemma conic_hull_eq_span: fixes S :: "'a::euclidean_space set" assumes"0 ∈ rel_interior S" shows"conic hull S = span S" by (simp add: assms conic_hull_eq_span_affine_hull)
lemma conic_hull_eq_affine_hull: fixes S :: "'a::euclidean_space set" assumes"0 ∈ rel_interior S" shows"conic hull S = affine hull S" using assms conic_hull_eq_span_affine_hull by blast
lemma conic_hull_eq_span_eq: fixes S :: "'a::euclidean_space set" shows"0 ∈ rel_interior(conic hull S) ⟷ conic hull S = span S" (is"?lhs = ?rhs") proof show"?lhs ==> ?rhs" by (metis conic_hull_eq_span conic_span hull_hull hull_minimal hull_subset span_eq) show"?rhs ==> ?lhs" by (metis rel_interior_affine subspace_affine subspace_span) qed
lemma aff_dim_eq_full_gen: "S ⊆ T ==> (aff_dim S = aff_dim T ⟷ affine hull S = affine hull T)" by (smt (verit, del_insts) aff_dim_affine_hull2 aff_dim_psubset hull_mono psubsetI)
lemma aff_dim_eq_full: fixes S :: "'n::euclidean_space set" shows"aff_dim S = (DIM('n)) ⟷ affine hull S = UNIV" by (metis aff_dim_UNIV aff_dim_affine_hull affine_hull_UNIV)
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) alsohave"... ⊆ 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) finallyshow ?thesis by (simp add: closure_mono dual_order.antisym) qed
subsection✐‹tag unimportant›‹Some obvious but surprisingly hard simplex lemmas›
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 *R x) S = y}" proof -
{ fix x and u :: "'a → real" assume"∀x∈S. 0 ≤ u x""sum u S ≤ 1" thenhave"∃v. 0 ≤ v 0 ∧ (∀x∈S. 0 ≤ v x) ∧ v 0 + sum v S = 1 ∧ (∑x∈S. v x *R x) = (∑x∈S. u x *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)
} thenshow ?thesis by (auto simp: convex_hull_finite set_eq_iff assms) qed
lemma substd_simplex: assumes d: "d ⊆ Basis" shows"convex hull (insert 0 d) = {x. (∀i∈Basis. 0 ≤ x∙i) ∧ (∑i∈d. x∙i) ≤ 1 ∧ (∀i∈Basis. i ∉ d ⟶ x∙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 ‹finite d›‹0 ∉ ?p›] 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 *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+ thenhave **: "sum u ?D = sum ((∙) ?x) ?D" using assms by (meson subset_iff 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 *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 (intro strip conjI) fix i :: 'a assume i: "i ∈ Basis" thenshow"0 < x ∙ i" using as[THEN subsetD[where c="x - (e/2) *R i"]] and‹e > 0› by (force simp add: inner_simps) next obtain i::'a where i: "i ∈ Basis" using nonempty_Basis by blast have **: "dist x (x + (e/2) *R i) < e"using‹e > 0› unfolding dist_norm by (auto intro!: mult_strict_left_mono simp: i) have"∧i. i ∈ Basis ==> (x + (e/2) *R i) ∙ i = x∙i + (if i = i then e/2 else 0)" by (auto simp: inner_simps) thenhave *: "sum ((∙) (x + (e/2) *R i)) Basis = sum (λj. x∙j + (if j = i then e/2 else 0)) Basis" using i by (auto simp: inner_Basis inner_left_distrib intro!: sum.cong) have"sum ((∙) x) Basis < sum ((∙) (x + (e/2) *R i)) Basis" using‹e > 0› DIM_positive by (auto simp: i sum.distrib *) alsohave"…≤ 1" using ** as by force finallyshow"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 (intro exI 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) alsohave"... < ?d" using y by (simp add: dist_norm norm_minus_commute) finallyhave"∣y∙i - x∙i∣ < ?d" . thenshow"y ∙ i ≤ x ∙ i + ?d"by auto qed alsohave"…≤ 1" unfolding sum.distrib sum_constant by (auto simp add: Suc_le_eq) finallyshow"sum ((∙) y) Basis ≤ 1" . show"(∀i∈Basis. 0 ≤ y ∙ i)" proof (intro strip) 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) alsohave"... ≤ x∙i" using i by auto finallyhave"norm (x - y) < x∙i" . thenshow"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 moreoverhave"?d > 0" using as by (auto simp: Suc_le_eq) ultimatelyshow"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)) *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 simp alsohave"… < 1" unfolding sum_constant divide_inverse[symmetric] by (auto simp add: field_simps) finallyshow"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 thenshow ?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))" thenobtain 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 thenhave as: "∧y. [dist x y < e ∧ (∀i∈Basis. i ∉ D ⟶ y∙i = 0)]==> (∀i∈D. 0 ≤ y ∙ i) ∧ sum ((∙) y) D ≤ 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" thenhave"∀j∈D. 0 ≤ (x - (e/2) *R i) ∙ j" using D ‹e > 0› x0 by (intro as[THEN conjunct1]) (force simp: dist_norm inner_simps inner_Basis) thenshow"0 < x ∙ i" using‹e > 0›‹i ∈ D› D by (force simp: inner_simps inner_Basis) next obtain a where a: "a ∈ D" using‹D ≠ {}›by auto thenhave **: "dist x (x + (e/2) *R a) < e" using‹e > 0› norm_Basis[of a] D by (auto simp: dist_norm) have"∧i. i ∈ Basis ==> (x + (e/2) *R a) ∙ i = x∙i + (if i = a then e/2 else 0)" using a D by (auto simp: inner_simps inner_Basis) thenhave *: "sum ((∙) (x + (e/2) *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‹a ∈ D› D by auto thenhave h1: "(∀i∈Basis. i ∉ D ⟶ (x + (e/2) *R a) ∙ i = 0)" using x0 D ‹a∈D›by (auto simp add: inner_add_left inner_Basis) have"sum ((∙) x) D < sum ((∙) (x + (e/2) *R a)) D" using‹e > 0›‹a ∈ D›‹finite D›by (auto simp add: * sum.distrib) alsohave"…≤ 1" using ** h1 as[rule_format, of "x + (e/2) *R a"] by auto finallyshow"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 moreoverhave"∀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 thenhave h2: "x ∈ convex hull (insert 0 D)" using as assms by (force simp add: substd_simplex) obtain a where a: "a ∈ D" using‹D ≠ {}›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‹D ≠ {}›‹finite D› by (simp add: card_gt_0_iff) have"Min (((∙) x) ` D) > 0" using as ‹D ≠ {}›‹finite D›by (simp) moreoverhave"d > 0" using as ‹0 < card D›by (auto simp: d_def) ultimatelyshow"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)" thenhave 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) alsohave"... < d" by (metis dist_norm min_less_iff_conj norm_minus_commute y) finallyhave"∣y∙i - x∙i∣ < d" . thenshow"y ∙ i ≤ x ∙ i + d"by auto qed alsohave"…≤ 1" unfolding sum.distrib sum_constant d_def using‹0 < card D› by auto finallyshow"sum ((∙) y) D ≤ 1" .
fix i :: 'a assume i: "i ∈ Basis" thenshow"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) thenshow"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 thenhave"x ∈ rel_interior (convex hull (insert 0 D))" using h0 h2 rel_interior_ball by force
} ultimatelyhave "∧x. x ∈ rel_interior (convex hull insert 0 D) ⟷ x ∈ {x. (∀i∈D. 0 < x ∙ i) ∧ sum ((∙) x) D < 1 ∧ (∀i∈Basis. i ∉ D ⟶ x ∙ i = 0)}" by blast thenshow ?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 = "(∑b∈D. b /R (2 * real (card D)))" have"finite D" using assms finite_Basis infinite_super by blast thenhave d1: "0 < real (card D)" using‹D ≠ {}›by auto
{ fix i assume"i ∈ D" have"?a ∙ i = (∑j∈D. if i = j then inverse (2 * real (card D)) else 0)" unfolding inner_sum_left using‹i ∈ D›by (auto simp: inner_Basis subsetD[OF assms(2)] intro: sum.cong) alsohave"... = inverse (2 * real (card D))" using‹i ∈ D›‹finite D›by auto finallyhave"?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 alsohave"… = ?a ∙ i"using **[of i] ‹i ∈ D› by auto finallyshow"0 < ?a ∙ i"by auto next have"sum ((∙) ?a) D = sum (λi. inverse (2 * real (card D))) D" by (rule sum.cong [OF refl **]) alsohave"… < 1" unfolding sum_constant divide_real_def[symmetric] by (auto simp add: field_simps) finallyshow"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 /R (2 * real (card D)))" D])
{ fix x :: "'a::euclidean_space" assume"x ∈ D" thenhave"x ∈ span D" using span_base[of _ "D"] by auto thenhave"x /R (2 * real (card D)) ∈ span D" using span_mul[of x "D""(inverse (real (card D)) / 2)"] by auto
} thenshow"∧x. x∈D ==> x /R (2 * real (card D)) ∈ span D" by auto qed thenshow"?a ∙ i = 0 " using‹i ∉ D›unfolding span_substd_basis[OF assms(2)] using‹i ∈ Basis›by auto qed qed qed
subsection✐‹tag unimportant›‹Relative interior of convex set›
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 thenshow ?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 thenhave"B ≠ {}" using B assms ‹S ≠ {0}› span_empty by auto have"insert 0 B ≤ span B" using subspace_span[of B] subspace_0[of "span B"]
span_superset by auto thenhave"span (insert 0 B) ≤ span B" using span_span[of B] span_mono[of "insert 0 B""span B"] by blast thenhave"convex hull insert 0 B ≤ span B" using convex_hull_subset_span[of "insert 0 B"] by auto thenhave"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 thenhave *: "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 thenhave"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 moreoverhave"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 ultimatelyhave **: "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 thenhave"bounded_linear f" using linear_conv_bounded_linear by auto have"d ≠ {}" using fd B ‹B ≠ {}›by auto have"insert 0 d = f ` (insert 0 B)" using fd linear_0 by auto thenhave"(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)"] ‹linear f› by auto moreoverhave"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 ‹bounded_linear f›]) show"inj_on f (span (convex hull insert 0 B))" using fd * by auto qed ultimatelyhave"rel_interior (convex hull insert 0 B) ≠ {}" using rel_interior_substd_simplex_nonempty[OF ‹d ≠ {}› d] by fastforce moreoverhave"convex hull (insert 0 B) ⊆ S" using B assms hull_mono[of "insert 0 B""S""convex"] convex_hull_eq by auto ultimatelyshow ?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 ≠ {}" thenobtain a where"a ∈ S"by auto thenhave"0 ∈ (+) (-a) ` S" using assms exI[of "(λx. x ∈ S ∧ - a + x = 0)" a] by auto thenhave"rel_interior ((+) (-a) ` S) ≠ {}" using rel_interior_convex_nonempty_aux[of "(+) (-a) ` S"]
convex_translation[of S "-a"] assms by auto thenhave"rel_interior S ≠ {}" using rel_interior_translation [of "- a"] by simp
} thenshow ?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) moreoverhave"rel_interior (convex hull insert 0 S) ≠ {}" using rel_interior_eq_empty [of "convex hull (insert 0 S)"] by auto ultimatelyhave"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" thenhave"x ∈ S" using rel_interior_subset by auto have"x - u *R (x-y) ∈ rel_interior S" proof (cases "0 = u") case False thenhave"0 < u"using assm by auto thenshow ?thesis using assm rel_interior_convex_shrink[of S y x u] assms ‹x ∈ S›by auto next case True thenshow ?thesis using assm by auto qed thenhave"(1 - u) *R x + u *R y ∈ rel_interior S" by (simp add: algebra_simps)
} thenshow ?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 thenobtain 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" thenhave"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))" thenhave e1: "e1 > 0""e1 ≤ 1""e1 * norm (x - a) ≤ e" using‹x ≠ a›‹e > 0› le_divide_eq[of e1 e "norm (x - a)"] by simp_all thenhave *: "x - e1 *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"*"‹x ≠ a› e1 by force
} thenhave"x islimpt rel_interior S" unfolding islimpt_approachable_le by auto thenhave"x ∈ closure(rel_interior S)" unfolding closure_def by auto
} ultimatelyhave"x ∈ closure(rel_interior S)"by auto
} thenshow ?thesis using h1 by auto qed auto qed
lemma empty_interior_subset_hyperplane_aux: fixes S :: "'a::euclidean_space set" assumes"convex S""0 ∈ S"and empty_int: "interior S = {}" shows"∃a b. a≠0 ∧ S ⊆ {x. a ∙ x = b}" proof - have False if"∧a. a = 0 ∨ (∀b. ∃T ∈ S. a ∙ T ≠ b)" proof - have rel_int: "rel_interior S ≠ {}" using assms rel_interior_eq_empty by auto moreover have"dim S ≠ dim (UNIV::'a set)" by (metis aff_dim_zero affine_hull_UNIV ‹0 ∈ S› dim_UNIV empty_int hull_inc rel_int rel_interior_interior) thenobtain a where"a ≠ 0"and a: "span S ⊆ {x. a ∙ x = 0}" using lowdim_subset_hyperplane by (metis dim_UNIV dim_subset_UNIV order_less_le) have"span UNIV = span S" by (metis span_base span_not_UNIV_orthogonal that) thenhave"UNIV ⊆ affine hull S" by (simp add: ‹0 ∈ S› hull_inc affine_hull_span_0) ultimatelyshow False using‹rel_interior S ≠ {}› empty_int rel_interior_interior by blast qed thenshow ?thesis by blast qed
lemma empty_interior_subset_hyperplane: fixes S :: "'a::euclidean_space set" assumes"convex S"and int: "interior S = {}" obtains a b where"a ≠ 0""S ⊆ {x. a ∙ x = b}" proof (cases "S = {}") case True thenshow ?thesis using that by blast next case False thenobtain u where"u ∈ S" by blast have"∃a b. a ≠ 0 ∧ (λx. x - u) ` S ⊆ {x. a ∙ x = b}" proof (rule empty_interior_subset_hyperplane_aux) show"convex ((λx. x - u) ` S)" using‹convex S›by force show"0 ∈ (λx. x - u) ` S" by (simp add: ‹u ∈ S›) show"interior ((λx. x - u) ` S) = {}" by (simp add: int interior_translation_subtract) qed thenobtain a b where"a ≠ 0"and ab: "(λx. x - u) ` S ⊆ {x. a ∙ x = b}" by metis thenhave"S ⊆ {x. a ∙ x = b + (a ∙ u)}" using ab by (auto simp: algebra_simps) thenshow ?thesis using‹a ≠ 0› that by auto qed
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 thenshow ?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) *R z = a *R x + b *R y" obtains e where"0 < e""e < 1""z = y - e *R (y - x)" proof - define e where"e = a / (a + b)" have"z = (1 / (a + b)) *R ((a + b) *R z)" using assms by (simp add: eq_vector_fraction_iff) alsohave"… = (1 / (a + b)) *R (a *R x + b *R y)" using assms scaleR_cancel_left[of "1/(a+b)""(a + b) *R z""a *R x + b *R y"] by auto alsohave"… = y - e *R (y-x)" using e_def assms by (simp add: divide_simps vector_fraction_eq_iff) (simp add: algebra_simps) finallyhave"z = y - e *R (y-x)" by auto moreoverhave"e > 0""e < 1"using e_def assms by auto ultimatelyshow ?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 thenshow ?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‹S ≠ {}› assms rel_interior_eq_empty by auto have"z ∈ rel_interior S" proof (cases "x = z") case True thenshow ?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)) *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 moreoverhave"z ∈ affine hull closure S" using z rel_interior_subset hull_subset[of "closure S"] by blast ultimatelyhave"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 thenhave"y ∈ closure S"using e yball by auto have"(1 + (e/norm(z-x))) *R z = (e/norm(z-x)) *R x + y" using y_def by (simp add: algebra_simps) thenobtain e1 where"0 < e1""e1 < 1""z = y - e1 *R (y - x)" using * convex_rel_interior_closure_aux[of "e / norm (z - x)"1 z x y] by (auto simp add: algebra_simps) thenshow ?thesis using rel_interior_closure_convex_shrink assms x ‹y ∈ closure S› by fastforce qed
} ultimatelyshow ?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 open_subset_closure_of_interval: assumes"open U""is_interval S" shows"U ⊆ closure S ⟷ U ⊆ interior S" by (metis assms convex_interior_closure is_interval_convex open_subset_interior)
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 thenshow ?thesis by auto next case False then have"open_segment a b = affine hull {a, b} ∩ ball ((a + b) /R 2) (norm (b - a) / 2)" by (simp add: open_segment_as_ball) thenshow ?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 thenshow ?thesis by auto next case False thenshow ?thesis by simp
(metis closure_open_segment convex_open_segment convex_rel_interior_closure
rel_interior_open_segment) qed
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 thenshow ?thesis by (force simp: sphere_def) next case equal thenshow ?thesis by simp next case greater thenshow ?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] ==> closest_point S x ∈ 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] ==> rel_interior S = rel_interior T ⟷ 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] ==> rel_interior S = rel_interior T ⟷ rel_interior S ⊆ T ∧ T ⊆ 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 thenhave *: "affine hull S1 ⊆ affine hull S2" using hull_mono[of "S1""closure S2"] closure_same_affine_hull[of S2] by blast thenhave"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" thenhave"S1 ≠ {}" using aff_dim_empty[of S1] aff_dim_empty[of S2] ‹S2 ≠ {}›by auto have **: "affine hull S1 = affine hull S2" by (simp_all add: * eq ‹S1 ≠ {}› affine_dim_equal) obtain a where a: "a ∈ rel_interior S1" using‹S1 ≠ {}› 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 thenhave"a ∈ T ∩ closure S2" using a assms unfolding rel_frontier_def by auto thenobtain b where b: "b ∈ T ∩ rel_interior S2" using open_inter_closure_rel_interior[of S2 T] assms T by auto thenhave"b ∈ affine hull S1" using rel_interior_subset hull_subset[of S2] ** by auto thenhave"b ∈ S1" using T b by auto thenhave False using b assms unfolding rel_frontier_def by auto
} ultimatelyshow ?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) *R x + e *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 ‹x ≠ z›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 thenhave *: "(1 - e)*R x + e *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 *R x - (x + e *R z)) = norm ((e - 1) *R (x - z))" by (simp add: algebra_simps) alsohave"… = (e - 1) * norm (x-z)" using norm_scaleR e by auto alsohave"…≤ (m - 1) * norm (x - z)" using e mult_right_mono[of _ _ "norm(x-z)"] by auto alsohave"… = (e1 / norm (x - z)) * norm (x - z)" using m_def by auto alsohave"… = e1" using‹x ≠ z› e1 by simp finallyhave **: "norm (z + e *R x - (x + e *R z)) ≤ e1" by auto have"(1 - e)*R x+ e *R z ∈ cball z e1" using m_def ** unfolding cball_def dist_norm by (auto simp add: algebra_simps) thenhave"(1 - e) *R x+ e *R z ∈ S" using e * e1 by auto
} thenhave"∃m. m > 1 ∧ (∀e. e > 1 ∧ e ≤ m ⟶ (1 - e) *R x + e *R z ∈ S )" using‹m> 1 ›by auto
} moreover
{ assume"x = z" define m where"m = 1 + e1" thenhave"m > 1" using e1 by auto
{ fix e assume e: "e > 1 ∧ e ≤ m" thenhave"(1 - e) *R x + e *R z ∈ S" using e1 x ‹x = z›by (auto simp add: algebra_simps) thenhave"(1 - e) *R x + e *R z ∈ S" using e by auto
} thenhave"∃m. m > 1 ∧ (∀e. e > 1 ∧ e ≤ m ⟶ (1 - e) *R x + e *R z ∈ S)" using‹m > 1›by auto
} ultimatelyhave"∃m. m > 1 ∧ (∀e. e > 1 ∧ e ≤ m ⟶ (1 - e) *R x + e *R z ∈ S )" by blast
} thenshow ?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)*R x + e *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) *R x + e *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 thenhave"x ∈ S" using rel_interior_subset by auto thenobtain e where e: "e > 1 ∧ (1 - e) *R x + e *R z ∈ S" using assms by auto define y where [abs_def]: "y = (1 - e) *R x + e *R z" thenhave"y ∈ S"using e by auto define e1 where"e1 = 1/e" thenhave"0 < e1 ∧ e1 < 1"using e by auto thenhave"z =y - (1 - e1) *R (y - x)" using e1_def y_def by (auto simp add: algebra_simps) thenshow ?thesis using rel_interior_convex_shrink[of S x y "1-e1"] ‹0 < e1 ∧ e1 < 1›‹y ∈ S› 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) *R x + e *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) *R x + e *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 *R x ∈ S)" proof (cases "aff_dim S = int DIM('n)") case False
{ assume"z ∈ interior S" thenhave False using False interior_rel_interior_gen[of S] by auto } moreover
{ assume r: "∀x. ∃e. e > 0 ∧ z + e *R x ∈ S"
{ fix x obtain e1 where e1: "e1 > 0 ∧ z + e1 *R (x - z) ∈ S" using r by auto obtain e2 where e2: "e2 > 0 ∧ z + e2 *R (z - x) ∈ S" using r by auto define x1 where [abs_def]: "x1 = z + e1 *R (x - z)" thenhave x1: "x1 ∈ affine hull S" using e1 hull_subset[of S] by auto define x2 where [abs_def]: "x2 = z + e2 *R (z - x)" thenhave 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 thenhave"z = (e2/(e1+e2)) *R x1 + (e1/(e1+e2)) *R x2" by (simp add: x1_def x2_def algebra_simps) (simp add: "*" pth_8) thenhave 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) *R (x - z)" using x1_def x2_def by (auto simp add: algebra_simps) thenhave"x = z+(1/(e1+e2)) *R (x1-x2)" using e1 e2 by simp thenhave"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
} thenhave"affine hull S = UNIV" by auto thenhave"aff_dim S = int DIM('n)" using aff_dim_affine_hull[of S] by (simp) thenhave False using False by auto
} ultimatelyshow ?thesis by auto next case True thenhave"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" thenhave"z ∈ rel_interior S" using True interior_rel_interior_gen[of S] by auto thenhave **: "∀x. ∃e. e > 1 ∧ (1 - e) *R x + e *R z ∈ S" using convex_rel_interior_iff2[of S z] assms ‹S ≠ {}› * by auto fix x obtain e1 where e1: "e1 > 1""(1 - e1) *R (z - x) + e1 *R z ∈ S" using **[rule_format, of "z-x"] by auto define e where [abs_def]: "e = e1 - 1" thenhave"(1 - e1) *R (z - x) + e1 *R z = z + e *R x" by (simp add: algebra_simps) thenhave"e > 0""z + e *R x ∈ S" using e1 e_def by auto thenhave"∃e. e > 0 ∧ z + e *R x ∈ S" by auto
} moreover
{ assume r: "∀x. ∃e. e > 0 ∧ z + e *R x ∈ S"
{ fix x obtain e1 where e1: "e1 > 0""z + e1 *R (z - x) ∈ S" using r[rule_format, of "z-x"] by auto define e where"e = e1 + 1" thenhave"z + e1 *R (z - x) = (1 - e) *R x + e *R z" by (simp add: algebra_simps) thenhave"e > 1""(1 - e)*R x + e *R z ∈ S" using e1 e_def by auto thenhave"∃e. e > 1 ∧ (1 - e) *R x + e *R z ∈ S"by auto
} thenhave"z ∈ rel_interior S" using convex_rel_interior_iff2[of S z] assms ‹S ≠ {}›by auto thenhave"z ∈ interior S" using True interior_rel_interior_gen[of S] by auto
} ultimatelyshow ?thesis by auto qed
subsubsection✐‹tag unimportant›‹Relative interior and closure under common operations›
lemma rel_interior_inter_aux: "∩{rel_interior S |S. S ∈ I} ⊆∩I" proof -
{ fix y assume"y ∈∩{rel_interior S |S. S ∈ I}" thenhave y: "∀S ∈ I. y ∈ rel_interior S" by auto
{ fix S assume"S ∈ I" thenhave"y ∈ S" using rel_interior_subset y by auto
} thenhave"y ∈∩I"by auto
} thenshow ?thesis by auto qed
lemma convex_closure_rel_interior_Int: assumes"∧S. S∈F==> convex (S :: 'n::euclidean_space set)" and"∩(rel_interior ` F) ≠ {}" shows"∩(closure ` F) ⊆ closure (∩(rel_interior ` F))" proof - obtain x where x: "∀S∈F. x ∈ rel_interior S" using assms by auto show ?thesis proof fix y assume y: "y ∈∩ (closure ` F)" show"y ∈ closure (∩(rel_interior ` F))" proof (cases "y=x") case True with closure_subset x show ?thesis by fastforce next case False show ?thesis proof (clarsimp simp: closure_approachable_le) fix ε :: real assume e: "ε > 0" define e1 where"e1 = min 1 (ε/norm (y - x))" thenhave e1: "e1 > 0""e1 ≤ 1""e1 * norm (y - x) ≤ ε" using‹y ≠ x›‹ε > 0› le_divide_eq[of e1 ε "norm (y - x)"] by simp_all define z where"z = y - e1 *R (y - x)"
{ fix S assume"S ∈F" thenhave"z ∈ rel_interior S" using rel_interior_closure_convex_shrink[of S x y e1] assms x y e1 z_def by auto
} thenhave *: "z ∈∩(rel_interior ` F)" by auto show"∃x∈∩ (rel_interior ` F). dist x y ≤ ε" using‹y ≠ x› z_def * e1 e dist_norm[of z y] by force qed qed qed qed
lemma closure_Inter_convex: fixesF :: "'n::euclidean_space set set" assumes"∧S. S ∈F==> convex S"and"∩(rel_interior ` F) ≠ {}" shows"closure(∩F) = ∩(closure ` F)" proof - have"∩(closure ` F) ≤ closure (∩(rel_interior ` F))" by (meson assms convex_closure_rel_interior_Int) moreover have"closure (∩(rel_interior ` F)) ⊆ closure (∩F)" using rel_interior_inter_aux closure_mono[of "∩(rel_interior ` F)""∩F"] by auto ultimatelyshow ?thesis using closure_Int[of F] by blast qed
lemma closure_Inter_convex_open: "(∧S::'n::euclidean_space set. S ∈F==> convex S ∧ open S) ==> closure(∩F) = (if ∩F = {} then {} else ∩(closure ` F))" by (simp add: closure_Inter_convex rel_interior_open)
lemma convex_Inter_rel_interior_same_closure: fixesF :: "'n::euclidean_space set set" assumes"∧S. S ∈F==> convex S" and"∩(rel_interior ` F) ≠ {}" shows"closure (∩(rel_interior ` F)) = closure (∩F)" proof - have"∩(closure ` F) ⊆ closure (∩(rel_interior ` F))" by (meson assms convex_closure_rel_interior_Int) moreover have"closure (∩(rel_interior ` F)) ⊆ closure (∩F)" by (metis Setcompr_eq_image closure_mono rel_interior_inter_aux) ultimatelyshow ?thesis by (simp add: assms closure_Inter_convex) qed
lemma convex_rel_interior_Inter: fixesF :: "'n::euclidean_space set set" assumes"∧S. S ∈F==> convex S" and"∩(rel_interior ` F) ≠ {}" shows"rel_interior (∩F) ⊆∩(rel_interior ` F)" proof - have"convex (∩F)" using assms convex_Inter by auto moreover have"convex (∩(rel_interior ` F))" using assms by (metis convex_rel_interior convex_INT) ultimately have"rel_interior (∩(rel_interior ` F)) = rel_interior (∩F)" using convex_Inter_rel_interior_same_closure assms
closure_eq_rel_interior_eq[of "∩(rel_interior ` F)""∩F"] by blast thenshow ?thesis using rel_interior_subset[of "∩(rel_interior ` F)"] by auto qed
lemma convex_rel_interior_finite_Inter: fixesF :: "'n::euclidean_space set set" assumes"∧S. S ∈F==> convex S" and"∩(rel_interior ` F) ≠ {}" and"finite F" shows"rel_interior (∩F) = ∩(rel_interior ` F)" proof - have"∩F≠ {}" using assms rel_interior_inter_aux[of F] by auto have"convex (∩F)" using convex_Inter assms by auto show ?thesis proof (cases "F = {}") case True thenshow ?thesis using Inter_empty rel_interior_UNIV by auto next case False
{ fix z assume z: "z ∈∩(rel_interior ` F)"
{ fix x assume x: "x ∈∩F"
{ fix S assume S: "S ∈F" thenhave"z ∈ rel_interior S""x ∈ S" using z x by auto thenhave"∃m. m > 1 ∧ (∀e. e > 1 ∧ e ≤ m ⟶ (1 - e)*R x + e *R z ∈ S)" using convex_rel_interior_if[of S z] S assms hull_subset[of S] by auto
} thenobtain mS where
mS: "∀S∈F. mS S > 1 ∧ (∀e. e > 1 ∧ e ≤ mS S ⟶ (1 - e) *R x + e *R z ∈ S)"by metis define e where"e = Min (mS ` F)" thenhave"e ∈ mS ` F"using assms ‹F≠ {}›by simp thenhave"e > 1"using mS by auto moreoverhave"∀S∈F. e ≤ mS S" using e_def assms by auto ultimatelyhave"∃e > 1. (1 - e) *R x + e *R z ∈∩F" using mS by auto
} thenhave"z ∈ rel_interior (∩F)" using convex_rel_interior_iff[of "∩F" z] ‹∩F≠ {}›‹convex (∩F)›by auto
} thenshow ?thesis using convex_rel_interior_Inter[of F] assms by auto qed qed
lemma closure_Int_convex: 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 closure_Inter_convex[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" by (metis affine_imp_convex assms closure_Int_convex rel_interior_affine rel_interior_eq_closure)
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" by (simp add: affine_imp_convex assms convex_rel_interior_inter_two rel_interior_affine)
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" assumes"convex S""affine T""interior S ∩ T ≠ {}" shows"rel_interior(S ∩ T) = interior S ∩ T" by (metis Int_emptyI assms convex_affine_rel_interior_Int empty_iff interior_rel_interior_gen)
lemma subset_rel_interior_convex: fixes S T :: "'n::euclidean_space set" assumes"convex S" and"convex T" and"S ≤ closure T" and"¬ S ⊆ rel_frontier T" shows"rel_interior S ⊆ rel_interior T" proof - have *: "S ∩ closure T = S" using assms by auto have"¬ rel_interior S ⊆ rel_frontier T" using closure_mono[of "rel_interior S""rel_frontier T"] closed_rel_frontier[of T]
closure_closed[of S] convex_closure_rel_interior[of S] closure_subset[of S] assms by auto thenhave"rel_interior S ∩ rel_interior (closure T) ≠ {}" using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto thenhave"rel_interior S ∩ rel_interior T = rel_interior (S ∩ closure T)" using assms convex_closure convex_rel_interior_inter_two[of S "closure T"]
convex_rel_interior_closure[of T] by auto alsohave"… = rel_interior S" using * by auto finallyshow ?thesis by auto qed
lemma rel_interior_convex_linear_image: fixes f :: "'m::euclidean_space → 'n::euclidean_space" assumes"linear f" and"convex S" shows"f ` (rel_interior S) = rel_interior (f ` S)" proof (cases "S = {}") case True thenshow ?thesis using assms by auto next case False interpret linear f by fact have *: "f ` (rel_interior S) ⊆ f ` S" unfolding image_mono using rel_interior_subset by auto have"f ` S ⊆ f ` (closure S)" unfolding image_mono using closure_subset by auto alsohave"… = f ` (closure (rel_interior S))" using convex_closure_rel_interior assms by auto alsohave"…⊆ closure (f ` (rel_interior S))" using closure_linear_image_subset assms by auto finallyhave"closure (f ` S) = closure (f ` rel_interior S)" using closure_mono[of "f ` S""closure (f ` rel_interior S)"] closure_closure
closure_mono[of "f ` rel_interior S""f ` S"] * by auto thenhave"rel_interior (f ` S) = rel_interior (f ` rel_interior S)" using assms convex_rel_interior
linear_conv_bounded_linear[of f] convex_linear_image[of _ S]
convex_linear_image[of _ "rel_interior S"]
closure_eq_rel_interior_eq[of "f ` S""f ` rel_interior S"] by auto thenhave"rel_interior (f ` S) ⊆ f ` rel_interior S" using rel_interior_subset by auto moreover
{ fix z assume"z ∈ f ` rel_interior S" thenobtain z1 where z1: "z1 ∈ rel_interior S""f z1 = z"by auto
{ fix x assume"x ∈ f ` S" thenobtain x1 where x1: "x1 ∈ S""f x1 = x"by auto thenobtain e where e: "e > 1""(1 - e) *R x1 + e *R z1 ∈ S" using convex_rel_interior_iff[of S z1] ‹convex S› x1 z1 by auto moreoverhave"f ((1 - e) *R x1 + e *R z1) = (1 - e) *R x + e *R z" using x1 z1 by (simp add: linear_add linear_scale ‹linear f›) ultimatelyhave"(1 - e) *R x + e *R z ∈ f ` S" using imageI[of "(1 - e) *R x1 + e *R z1" S f] by auto thenhave"∃e. e > 1 ∧ (1 - e) *R x + e *R z ∈ f ` S" using e by auto
} thenhave"z ∈ rel_interior (f ` S)" using convex_rel_interior_iff[of "f ` S" z] ‹convex S›‹linear f› ‹S ≠ {}› convex_linear_image[of f S] linear_conv_bounded_linear[of f] by auto
} ultimatelyshow ?thesis by auto qed
lemma rel_interior_convex_linear_preimage: fixes f :: "'m::euclidean_space → 'n::euclidean_space" assumes"linear f" and"convex S" and"f -` (rel_interior S) ≠ {}" shows"rel_interior (f -` S) = f -` (rel_interior S)" proof - interpret linear f by fact have"S ≠ {}" using assms by auto have nonemp: "f -` S ≠ {}" by (metis assms(3) rel_interior_subset subset_empty vimage_mono) thenhave"S ∩ (range f) ≠ {}" by auto have conv: "convex (f -` S)" using convex_linear_vimage assms by auto thenhave"convex (S ∩ range f)" by (simp add: assms(2) convex_Int convex_linear_image linear_axioms)
{ fix z assume"z ∈ f -` (rel_interior S)" thenhave z: "f z ∈ rel_interior S" by auto
{ fix x assume"x ∈ f -` S" thenhave"f x ∈ S"by auto thenobtain e where e: "e > 1""(1 - e) *R f x + e *R f z ∈ S" using convex_rel_interior_iff[of S "f z"] z assms ‹S ≠ {}›by auto moreoverhave"(1 - e) *R f x + e *R f z = f ((1 - e) *R x + e *R z)" using‹linear f›by (simp add: linear_iff) ultimatelyhave"∃e. e > 1 ∧ (1 - e) *R x + e *R z ∈ f -` S" using e by auto
} thenhave"z ∈ rel_interior (f -` S)" using convex_rel_interior_iff[of "f -` S" z] conv nonemp by auto
} moreover
{ fix z assume z: "z ∈ rel_interior (f -` S)"
{ fix x assume"x ∈ S ∩ range f" thenobtain y where y: "f y = x""y ∈ f -` S"by auto thenobtain e where e: "e > 1""(1 - e) *R y + e *R z ∈ f -` S" using convex_rel_interior_iff[of "f -` S" z] z conv by auto moreoverhave"(1 - e) *R x + e *R f z = f ((1 - e) *R y + e *R z)" using‹linear f› y by (simp add: linear_iff) ultimatelyhave"∃e. e > 1 ∧ (1 - e) *R x + e *R f z ∈ S ∩ range f" using e by auto
} thenhave"f z ∈ rel_interior (S ∩ range f)" using‹convex (S ∩ (range f))›‹S ∩ range f ≠ {}›
convex_rel_interior_iff[of "S ∩ (range f)""f z"] by auto moreoverhave"affine (range f)" by (simp add: linear_axioms linear_subspace_image subspace_imp_affine) ultimatelyhave"f z ∈ rel_interior S" using convex_affine_rel_interior_Int[of S "range f"] assms by auto thenhave"z ∈ f -` (rel_interior S)" by auto
} ultimatelyshow ?thesis by auto qed
lemma rel_interior_Times: fixes S :: "'n::euclidean_space set" and T :: "'m::euclidean_space set" assumes"convex S" and"convex T" shows"rel_interior (S × T) = rel_interior S × rel_interior T" proof (cases "S = {} ∨ T = {}") case True thenshow ?thesis by auto next case False thenhave"S ≠ {}""T ≠ {}" by auto thenhave ri: "rel_interior S ≠ {}""rel_interior T ≠ {}" using rel_interior_eq_empty assms by auto thenhave"fst -` rel_interior S ≠ {}" using fst_vimage_eq_Times[of "rel_interior S"] by auto thenhave"rel_interior ((fst :: 'n * 'm → 'n) -` S) = fst -` rel_interior S" using linear_fst ‹convex S› rel_interior_convex_linear_preimage[of fst S] by auto thenhave s: "rel_interior (S × (UNIV :: 'm set)) = rel_interior S × UNIV" by (simp add: fst_vimage_eq_Times) from ri have"snd -` rel_interior T ≠ {}" using snd_vimage_eq_Times[of "rel_interior T"] by auto thenhave"rel_interior ((snd :: 'n * 'm → 'm) -` T) = snd -` rel_interior T" using linear_snd ‹convex T› rel_interior_convex_linear_preimage[of snd T] by auto thenhave t: "rel_interior ((UNIV :: 'n set) × T) = UNIV × rel_interior T" by (simp add: snd_vimage_eq_Times) from s t have *: "rel_interior (S × (UNIV :: 'm set)) ∩ rel_interior ((UNIV :: 'n set) × T) = rel_interior S × rel_interior T"by auto have"S × T = S × (UNIV :: 'm set) ∩ (UNIV :: 'n set) × T" by auto thenhave"rel_interior (S × T) = rel_interior ((S × (UNIV :: 'm set)) ∩ ((UNIV :: 'n set) × T))" by auto alsohave"… = rel_interior (S × (UNIV :: 'm set)) ∩ rel_interior ((UNIV :: 'n set) × T)" using * ri assms convex_Times by (subst convex_rel_interior_inter_two) auto finallyshow ?thesis using * by auto qed
lemma rel_interior_scaleR: fixes S :: "'n::euclidean_space set" assumes"c ≠ 0" shows"((*R) c) ` (rel_interior S) = rel_interior (((*R) c) ` S)" using rel_interior_injective_linear_image[of "((*R) c)" S]
linear_conv_bounded_linear[of "(*R) c"] linear_scaleR injective_scaleR[of c] assms by auto
lemma rel_interior_convex_scaleR: fixes S :: "'n::euclidean_space set" assumes"convex S" shows"((*R) c) ` (rel_interior S) = rel_interior (((*R) c) ` S)" by (metis assms linear_scaleR rel_interior_convex_linear_image)
lemma convex_rel_open_scaleR: fixes S :: "'n::euclidean_space set" assumes"convex S" and"rel_open S" shows"convex (((*R) c) ` S) ∧ rel_open (((*R) c) ` S)" by (metis assms convex_scaling rel_interior_convex_scaleR rel_open_def)
lemma convex_rel_open_finite_Inter: fixesF :: "'n::euclidean_space set set" assumes"∧S. S ∈F==> convex S ∧ rel_open S" and"finite F" shows"convex (∩F) ∧ rel_open (∩F)" proof (cases "∩{rel_interior S |S. S ∈F} = {}") case True thenhave"∩F = {}" using assms unfolding rel_open_def by auto thenshow ?thesis unfolding rel_open_def by auto next case False thenhave"rel_open (∩F)" using assms convex_rel_interior_finite_Inter[of F] by (force simp: rel_open_def) thenshow ?thesis using convex_Inter assms by auto qed
lemma convex_rel_open_linear_preimage: fixes f :: "'m::euclidean_space → 'n::euclidean_space" assumes"linear f" and"convex S" and"rel_open S" shows"convex (f -` S) ∧ rel_open (f -` S)" proof (cases "f -` (rel_interior S) = {}") case True thenhave"f -` S = {}" using assms unfolding rel_open_def by auto thenshow ?thesis unfolding rel_open_def by auto next case False thenhave"rel_open (f -` S)" using assms unfolding rel_open_def using rel_interior_convex_linear_preimage[of f S] by auto thenshow ?thesis using convex_linear_vimage assms by auto qed
lemma rel_interior_projection: fixes S :: "('m::euclidean_space × 'n::euclidean_space) set" and f :: "'m::euclidean_space → 'n::euclidean_space set" assumes"convex S" and"f = (λy. {z. (y, z) ∈ S})" shows"(y, z) ∈ rel_interior S ⟷ (y ∈ rel_interior {y. (f y ≠ {})} ∧ z ∈ rel_interior (f y))" proof -
{ fix y assume"y ∈ {y. f y ≠ {}}" thenobtain z where"(y, z) ∈ S" using assms by auto thenhave"∃x. x ∈ S ∧ y = fst x" by auto thenobtain x where"x ∈ S""y = fst x" by blast thenhave"y ∈ fst ` S" unfolding image_def by auto
} thenhave"fst ` S = {y. f y ≠ {}}" unfolding fst_def using assms by auto thenhave h1: "fst ` rel_interior S = rel_interior {y. f y ≠ {}}" using rel_interior_convex_linear_image[of fst S] assms linear_fst by auto
{ fix y assume"y ∈ rel_interior {y. f y ≠ {}}" thenhave"y ∈ fst ` rel_interior S" using h1 by auto thenhave *: "rel_interior S ∩ fst -` {y} ≠ {}" by auto moreoverhave aff: "affine (fst -` {y})" unfolding affine_alt by (simp add: algebra_simps) ultimatelyhave **: "rel_interior (S ∩ fst -` {y}) = rel_interior S ∩ fst -` {y}" using convex_affine_rel_interior_Int[of S "fst -` {y}"] assms by auto have conv: "convex (S ∩ fst -` {y})" using convex_Int assms aff affine_imp_convex by auto
{ fix x assume"x ∈ f y" thenhave"(y, x) ∈ S ∩ (fst -` {y})" using assms by auto moreoverhave"x = snd (y, x)"by auto ultimatelyhave"x ∈ snd ` (S ∩ fst -` {y})" by blast
} thenhave"snd ` (S ∩ fst -` {y}) = f y" using assms by auto thenhave ***: "rel_interior (f y) = snd ` rel_interior (S ∩ fst -` {y})" using rel_interior_convex_linear_image[of snd "S ∩ fst -` {y}"] linear_snd conv by auto
{ fix z assume"z ∈ rel_interior (f y)" thenhave"z ∈ snd ` rel_interior (S ∩ fst -` {y})" using *** by auto moreoverhave"{y} = fst ` rel_interior (S ∩ fst -` {y})" using * ** rel_interior_subset by auto ultimatelyhave"(y, z) ∈ rel_interior (S ∩ fst -` {y})" by force thenhave"(y,z) ∈ rel_interior S" using ** by auto
} moreover
{ fix z assume"(y, z) ∈ rel_interior S" thenhave"(y, z) ∈ rel_interior (S ∩ fst -` {y})" using ** by auto thenhave"z ∈ snd ` rel_interior (S ∩ fst -` {y})" by (metis Range_iff snd_eq_Range) thenhave"z ∈ rel_interior (f y)" using *** by auto
} ultimatelyhave"∧z. (y, z) ∈ rel_interior S ⟷ z ∈ rel_interior (f y)" by auto
} thenhave h2: "∧y z. y ∈ rel_interior {t. f t ≠ {}} ==> (y, z) ∈ rel_interior S ⟷ z ∈ rel_interior (f y)" by auto
{ fix y z assume asm: "(y, z) ∈ rel_interior S" thenhave"y ∈ fst ` rel_interior S" by (metis Domain_iff fst_eq_Domain) thenhave"y ∈ rel_interior {t. f t ≠ {}}" using h1 by auto thenhave"y ∈ rel_interior {t. f t ≠ {}}"and"(z ∈ rel_interior (f y))" using h2 asm by auto
} thenshow ?thesis using h2 by blast qed
lemma rel_frontier_Times: fixes S :: "'n::euclidean_space set" and T :: "'m::euclidean_space set" assumes"convex S" and"convex T" shows"rel_frontier S × rel_frontier T ⊆ rel_frontier (S × T)" by (force simp: rel_frontier_def rel_interior_Times assms closure_Times)
subsubsection✐‹tag unimportant›‹Relative interior of convex cone›
lemma cone_rel_interior: fixes S :: "'m::euclidean_space set" assumes"cone S" shows"cone ({0} ∪ rel_interior S)" proof (cases "S = {}") case True thenshow ?thesis by (simp add: cone_0) next case False thenhave *: "0 ∈ S ∧ (∀c. c > 0 ⟶ (*R) c ` S = S)" using cone_iff[of S] assms by auto thenhave *: "0 ∈ ({0} ∪ rel_interior S)" and"∀c. c > 0 ⟶ (*R) c ` ({0} ∪ rel_interior S) = ({0} ∪ rel_interior S)" by (auto simp add: rel_interior_scaleR) thenshow ?thesis using cone_iff[of "{0} ∪ rel_interior S"] by auto qed
lemma rel_interior_convex_cone_aux: fixes S :: "'m::euclidean_space set" assumes"convex S" shows"(c, x) ∈ rel_interior (cone hull ({(1 :: real)} × S)) ⟷ c > 0 ∧ x ∈ (((*R) c) ` (rel_interior S))" proof (cases "S = {}") case True thenshow ?thesis by (simp add: cone_hull_empty) next case False thenobtain s where"s ∈ S"by auto have conv: "convex ({(1 :: real)} × S)" using convex_Times[of "{(1 :: real)}" S] assms convex_singleton[of "1 :: real"] by auto define f where"f y = {z. (y, z) ∈ cone hull ({1 :: real} × S)}"for y thenhave *: "(c, x) ∈ rel_interior (cone hull ({(1 :: real)} × S)) = (c ∈ rel_interior {y. f y ≠ {}} ∧ x ∈ rel_interior (f c))" using convex_cone_hull[of "{(1 :: real)} × S"] conv by (subst rel_interior_projection) auto
{ fix y :: real assume"y ≥ 0" thenhave"y *R (1,s) ∈ cone hull ({1 :: real} × S)" using cone_hull_expl[of "{(1 :: real)} × S"] ‹s ∈ S›by auto thenhave"f y ≠ {}" using f_def by auto
} thenhave"{y. f y ≠ {}} = {0..}" using f_def cone_hull_expl[of "{1 :: real} × S"] by auto thenhave **: "rel_interior {y. f y ≠ {}} = {0<..}" using rel_interior_real_semiline by auto
{ fix c :: real assume"c > 0" thenhave"f c = ((*R) c ` S)" using f_def cone_hull_expl[of "{1 :: real} × S"] by auto thenhave"rel_interior (f c) = (*R) c ` rel_interior S" using rel_interior_convex_scaleR[of S c] assms by auto
} thenshow ?thesis using * ** by auto qed
lemma rel_interior_convex_cone: fixes S :: "'m::euclidean_space set" assumes"convex S" shows"rel_interior (cone hull ({1 :: real} × S)) = {(c, c *R x) | c x. c > 0 ∧ x ∈ rel_interior S}"
(is"?lhs = ?rhs") proof -
{ fix z assume"z ∈ ?lhs" have *: "z = (fst z, snd z)" by auto thenhave"z ∈ ?rhs" using rel_interior_convex_cone_aux[of S "fst z""snd z"] assms ‹z ∈ ?lhs›by fastforce
} moreover
{ fix z assume"z ∈ ?rhs" thenhave"z ∈ ?lhs" using rel_interior_convex_cone_aux[of S "fst z""snd z"] assms by auto
} ultimatelyshow ?thesis by blast qed
lemma convex_hull_finite_union: assumes"finite I" assumes"∀i∈I. convex (S i) ∧ (S i) ≠ {}" shows"convex hull (∪(S ` I)) = {sum (λi. c i *R s i) I | c s. (∀i∈I. c i ≥ 0) ∧ sum c I = 1 ∧ (∀i∈I. s i ∈ S i)}"
(is"?lhs = ?rhs") proof - have"?lhs ⊇ ?rhs" proof fix x assume"x ∈ ?rhs" thenobtain c s where *: "sum (λi. c i *R s i) I = x""sum c I = 1" "(∀i∈I. c i ≥ 0) ∧ (∀i∈I. s i ∈ S i)"by auto thenhave"∀i∈I. s i ∈ convex hull (∪(S ` I))" using hull_subset[of "∪(S ` I)" convex] by auto thenshow"x ∈ ?lhs" unfolding *(1)[symmetric] using * assms convex_convex_hull by (subst convex_sum) auto qed
{ fix i assume"i ∈ I" with assms have"∃p. p ∈ S i"by auto
} thenobtain p where p: "∀i∈I. p i ∈ S i"by metis
{ fix i assume"i ∈ I"
{ fix x assume"x ∈ S i" define c where"c j = (if j = i then 1::real else 0)"for j thenhave *: "sum c I = 1" using‹finite I›‹i ∈ I› sum.delta[of I i "λj::'a. 1::real"] by auto define s where"s j = (if j = i then x else p j)"for j thenhave"∀j. c j *R s j = (if j = i then x else 0)" using c_def by (auto simp add: algebra_simps) thenhave"x = sum (λi. c i *R s i) I" using s_def c_def ‹finite I›‹i ∈ I› sum.delta[of I i "λj::'a. x"] by auto moreoverhave"(∀i∈I. 0 ≤ c i) ∧ sum c I = 1 ∧ (∀i∈I. s i ∈ S i)" using * c_def s_def p ‹x ∈ S i›by auto ultimatelyhave"x ∈ ?rhs" by force
} thenhave"?rhs ⊇ S i"by auto
} thenhave *: "?rhs ⊇∪(S ` I)"by auto
{ fix u v :: real assume uv: "u ≥ 0 ∧ v ≥ 0 ∧ u + v = 1" fix x y assume xy: "x ∈ ?rhs ∧ y ∈ ?rhs" from xy obtain c s where
xc: "x = sum (λi. c i *R s i) I ∧ (∀i∈I. c i ≥ 0) ∧ sum c I = 1 ∧ (∀i∈I. s i ∈ S i)" by auto from xy obtain d t where
yc: "y = sum (λi. d i *R t i) I ∧ (∀i∈I. d i ≥ 0) ∧ sum d I = 1 ∧ (∀i∈I. t i ∈ S i)" by auto define e where"e i = u * c i + v * d i"for i have ge0: "∀i∈I. e i ≥ 0" using e_def xc yc uv by simp have"sum (λi. u * c i) I = u * sum c I" by (simp add: sum_distrib_left) moreoverhave"sum (λi. v * d i) I = v * sum d I" by (simp add: sum_distrib_left) ultimatelyhave sum1: "sum e I = 1" using e_def xc yc uv by (simp add: sum.distrib) define q where"q i = (if e i = 0 then p i else (u * c i / e i) *R s i + (v * d i / e i) *R t i)" for i
{ fix i assume i: "i ∈ I" have"q i ∈ S i" proof (cases "e i = 0") case True thenshow ?thesis using i p q_def by auto next case False thenshow ?thesis using mem_convex_alt[of "S i""s i""t i""u * (c i)""v * (d i)"]
mult_nonneg_nonneg[of u "c i"] mult_nonneg_nonneg[of v "d i"]
assms q_def e_def i False xc yc uv by (auto simp del: mult_nonneg_nonneg) qed
} thenhave qs: "∀i∈I. q i ∈ S i"by auto
{ fix i assume i: "i ∈ I" have"(u * c i) *R s i + (v * d i) *R t i = e i *R q i" proof (cases "e i = 0") case True have ge: "u * (c i) ≥ 0 ∧ v * d i ≥ 0" using xc yc uv i by simp moreoverfrom ge have"u * c i ≤ 0 ∧ v * d i ≤ 0" using True e_def i by simp ultimatelyhave"u * c i = 0 ∧ v * d i = 0"by auto with True show ?thesis by auto next case False thenhave"(u * (c i)/(e i))*R (s i)+(v * (d i)/(e i))*R (t i) = q i" using q_def by auto thenhave"e i *R ((u * (c i)/(e i))*R (s i)+(v * (d i)/(e i))*R (t i)) = (e i) *R (q i)"by auto with False show ?thesis by (simp add: algebra_simps) qed
} thenhave *: "∀i∈I. (u * c i) *R s i + (v * d i) *R t i = e i *R q i" by auto have"u *R x + v *R y = sum (λi. (u * c i) *R s i + (v * d i) *R t i) I" using xc yc by (simp add: algebra_simps scaleR_right.sum sum.distrib) alsohave"… = sum (λi. e i *R q i) I" using * by auto finallyhave"u *R x + v *R y = sum (λi. (e i) *R (q i)) I" by auto thenhave"u *R x + v *R y ∈ ?rhs" using ge0 sum1 qs by auto
} thenhave"convex ?rhs"unfolding convex_def by auto thenshow ?thesis using‹?lhs ⊇ ?rhs› * hull_minimal[of "∪(S ` I)" ?rhs convex] by blast qed
lemma convex_hull_union_two: fixes S T :: "'m::euclidean_space set" assumes"convex S" and"S ≠ {}" and"convex T" and"T ≠ {}" shows"convex hull (S ∪ T) = {u *R s + v *R t | u v s t. u ≥ 0 ∧ v ≥ 0 ∧ u + v = 1 ∧ s ∈ S ∧ t ∈ T}"
(is"?lhs = ?rhs") proof define I :: "nat set"where"I = {1, 2}" define s where"s i = (if i = (1::nat) then S else T)"for i have"∪(s ` I) = S ∪ T" using s_def I_def by auto thenhave"convex hull (∪(s ` I)) = convex hull (S ∪ T)" by auto moreoverhave"convex hull ∪(s ` I) = {∑ i∈I. c i *R sa i | c sa. (∀i∈I. 0 ≤ c i) ∧ sum c I = 1 ∧ (∀i∈I. sa i ∈ s i)}" using assms s_def I_def by (subst convex_hull_finite_union) auto moreoverhave "{∑i∈I. c i *R sa i | c sa. (∀i∈I. 0 ≤ c i) ∧ sum c I = 1 ∧ (∀i∈I. sa i ∈ s i)} ≤ ?rhs" using s_def I_def by auto ultimatelyshow"?lhs ⊆ ?rhs"by auto
{ fix x assume"x ∈ ?rhs" thenobtain u v s t where *: "x = u *R s + v *R t ∧ u ≥ 0 ∧ v ≥ 0 ∧ u + v = 1 ∧ s ∈ S ∧t ∈ T" by auto thenhave"x ∈ convex hull {s, t}" using convex_hull_2[of s t] by auto thenhave"x ∈ convex hull (S ∪ T)" using * hull_mono[of "{s, t}""S ∪ T"] by auto
} thenshow"?lhs ⊇ ?rhs"by blast qed
proposition ray_to_rel_frontier: fixes a :: "'a::real_inner" assumes"bounded S" and a: "a ∈ rel_interior S" and aff: "(a + l) ∈ affine hull S" and"l ≠ 0" obtains d where"0 < d""(a + d *R l) ∈ rel_frontier S" "∧e. [0 ≤ e; e < d]==> (a + e *R l) ∈ rel_interior S" proof - have aaff: "a ∈ affine hull S" by (meson a hull_subset rel_interior_subset rev_subsetD) let ?D = "{d. 0 < d ∧ a + d *R l ∉ rel_interior S}" obtain B where"B > 0"and B: "S ⊆ ball a B" using bounded_subset_ballD [OF ‹bounded S›] by blast have"a + (B / norm l) *R l ∉ ball a B" by (simp add: dist_norm ‹l ≠ 0›) with B have"a + (B / norm l) *R l ∉ rel_interior S" using rel_interior_subset subsetCE by blast with‹B > 0›‹l ≠ 0›have nonMT: "?D ≠ {}" using divide_pos_pos zero_less_norm_iff by fastforce have bdd: "bdd_below ?D" by (metis (no_types, lifting) bdd_belowI le_less mem_Collect_eq) have relin_Ex: "∧x. x ∈ rel_interior S ==> ∃e>0. ∀x'∈affine hull S. dist x' x < e ⟶ x' ∈ rel_interior S" using openin_rel_interior [of S] by (simp add: openin_euclidean_subtopology_iff) define d where"d = Inf ?D" obtain ε where"0 < ε"and ε: "∧η. [0 ≤ η; η < ε]==> (a + η *R l) ∈ rel_interior S" proof - obtain e where"e>0" and e: "∧x'. x' ∈ affine hull S ==> dist x' a < e ==> x' ∈ rel_interior S" using relin_Ex a by blast show thesis proof (rule_tac ε = "e / norm l"in that) show"0 < e / norm l"by (simp add: ‹0 < e›‹l ≠ 0›) next show"a + η *R l ∈ rel_interior S"if"0 ≤ η""η < e / norm l"for η proof (rule e) show"a + η *R l ∈ affine hull S" by (metis (no_types) add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff) show"dist (a + η *R l) a < e" using that by (simp add: ‹l ≠ 0› dist_norm pos_less_divide_eq) qed qed qed have inint: "∧e. [0 ≤ e; e < d]==> a + e *R l ∈ rel_interior S" unfolding d_def using cInf_lower [OF _ bdd] by (metis (no_types, lifting) a add.right_neutral le_less mem_Collect_eq not_less real_vector.scale_zero_left) have"ε ≤ d" unfolding d_def using ε dual_order.strict_implies_order le_less_linear by (blast intro: cInf_greatest [OF nonMT]) with‹0 < \ε›have"0 < d"by simp have"a + d *R l ∉ rel_interior S" proof assume adl: "a + d *R l ∈ rel_interior S" obtain e where"e > 0" and e: "∧x'. x' ∈ affine hull S ==> dist x' (a + d *R l) < e ==> x' ∈ rel_interior S" using relin_Ex adl by blast have"d + e / norm l ≤ x" if"0 < x"and nonrel: "a + x *R l ∉ rel_interior S"for x proof (cases "x < d") case True with inint nonrel ‹0 < x› show ?thesis by auto next case False thenhave dle: "x < d + e / norm l ==> dist (a + x *R l) (a + d *R l) < e" by (simp add: field_simps ‹l ≠ 0›) have ain: "a + x *R l ∈ affine hull S" by (metis add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff) show ?thesis using e [OF ain] nonrel dle by force qed then have"d + e / norm l ≤ Inf {d. 0 < d ∧ a + d *R l ∉ rel_interior S}" by (force simp add: intro: cInf_greatest [OF nonMT]) thenshow False using‹0 < e›‹l ≠ 0›by (simp add: d_def [symmetric] field_simps) qed moreover have"∃y∈S. dist y (a + d *R l) < η"if"0 < η"for η::real proof - have1: "a + (d - min d (η / 2 / norm l)) *R l ∈ S" proof (rule subsetD [OF rel_interior_subset inint]) show"d - min d (η / 2 / norm l) < d" using‹l ≠ 0›‹0 < d›‹0 < \η›by auto qed auto have"norm l * min d (η / (norm l * 2)) ≤ norm l * (η / (norm l * 2))" by (metis min_def mult_left_mono norm_ge_zero order_refl) alsohave"... < η" using‹l ≠ 0›‹0 < \η›by (simp add: field_simps) finallyhave2: "norm l * min d (η / (norm l * 2)) < η" . show ?thesis using12‹0 < d›‹0 < \η› by (rule_tac x="a + (d - min d (η / 2 / norm l)) *R l"in bexI) (auto simp: algebra_simps) qed thenhave"a + d *R l ∈ closure S" by (auto simp: closure_approachable) ultimatelyhave infront: "a + d *R l ∈ rel_frontier S" by (simp add: rel_frontier_def) show ?thesis by (rule that [OF ‹0 < d› infront inint]) qed
corollary ray_to_frontier: fixes a :: "'a::euclidean_space" assumes"bounded S" and a: "a ∈ interior S" and"l ≠ 0" obtains d where"0 < d""(a + d *R l) ∈ frontier S" "∧e. [0 ≤ e; e < d]==> (a + e *R l) ∈ interior S" proof - have§: "interior S = rel_interior S" using a rel_interior_nonempty_interior by auto thenhave"a ∈ rel_interior S" using a by simp moreoverhave"a + l ∈ affine hull S" using a affine_hull_nonempty_interior by blast ultimatelyshow thesis by (metis §‹bounded S›‹l ≠ 0› frontier_def ray_to_rel_frontier rel_frontier_def that) qed
lemma segment_to_rel_frontier_aux: fixes x :: "'a::euclidean_space" assumes"convex S""bounded S"and x: "x ∈ rel_interior S"and y: "y ∈ S"and xy: "x ≠ y" obtains z where"z ∈ rel_frontier S""y ∈ closed_segment x z" "open_segment x z ⊆ rel_interior S" proof - have"x + (y - x) ∈ affine hull S" using hull_inc [OF y] by auto thenobtain d where"0 < d"and df: "(x + d *R (y-x)) ∈ rel_frontier S" and di: "∧e. [0 ≤ e; e < d]==> (x + e *R (y-x)) ∈ rel_interior S" by (rule ray_to_rel_frontier [OF ‹bounded S› x]) (use xy in auto) show ?thesis proof show"x + d *R (y - x) ∈ rel_frontier S" by (simp add: df) next have"open_segment x y ⊆ rel_interior S" using rel_interior_closure_convex_segment [OF ‹convex S› x] closure_subset y by blast moreoverhave"x + d *R (y - x) ∈ open_segment x y"if"d < 1" using xy ‹0 < d› that by (force simp: in_segment algebra_simps) ultimatelyhave"1 ≤ d" using df rel_frontier_def by fastforce moreoverhave"x = (1 / d) *R x + ((d - 1) / d) *R x" by (metis ‹0 < d› add.commute add_divide_distrib diff_add_cancel divide_self_if less_irrefl scaleR_add_left scaleR_one) ultimatelyshow"y ∈ closed_segment x (x + d *R (y - x))" unfolding in_segment by (rule_tac x="1/d"in exI) (auto simp: algebra_simps) next show"open_segment x (x + d *R (y - x)) ⊆ rel_interior S" proof (rule rel_interior_closure_convex_segment [OF ‹convex S› x]) show"x + d *R (y - x) ∈ closure S" using df rel_frontier_def by auto qed qed qed
lemma segment_to_rel_frontier: fixes x :: "'a::euclidean_space" assumes S: "convex S""bounded S"and x: "x ∈ rel_interior S" and y: "y ∈ S"and xy: "¬(x = y ∧ S = {x})" obtains z where"z ∈ rel_frontier S""y ∈ closed_segment x z" "open_segment x z ⊆ rel_interior S" proof (cases "x=y") case True with xy have"S ≠ {x}" by blast with True show ?thesis by (metis Set.set_insert all_not_in_conv ends_in_segment(1) insert_iff segment_to_rel_frontier_aux[OF S x] that y) next case False thenshow ?thesis using segment_to_rel_frontier_aux [OF S x y] that by blast qed
proposition rel_frontier_not_sing: fixes a :: "'a::euclidean_space" assumes"bounded S" shows"rel_frontier S ≠ {a}" proof (cases "S = {}") case True thenshow ?thesis by simp next case False thenobtain z where"z ∈ S" by blast thenshow ?thesis proof (cases "S = {z}") case True thenshow ?thesis by simp next case False thenobtain w where"w ∈ S""w ≠ z" using‹z ∈ S›by blast show ?thesis proof assume"rel_frontier S = {a}" then consider "w ∉ rel_frontier S" | "z ∉ rel_frontier S" using‹w ≠ z›by auto thenshow False proof cases case1 thenhave w: "w ∈ rel_interior S" using‹w ∈ S› closure_subset rel_frontier_def by fastforce have"w + (w - z) ∈ affine hull S" by (metis ‹w ∈ S›‹z ∈ S› affine_affine_hull hull_inc mem_affine_3_minus scaleR_one) thenobtain e where"0 < e""(w + e *R (w - z)) ∈ rel_frontier S" using‹w ≠ z›‹z ∈ S›by (metis assms ray_to_rel_frontier right_minus_eq w) moreoverobtain d where"0 < d""(w + d *R (z - w)) ∈ rel_frontier S" using ray_to_rel_frontier [OF ‹bounded S› w, of "1 *R (z - w)"] ‹w ≠ z›‹z ∈ S› by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one) ultimatelyhave"d *R (z - w) = e *R (w - z)" using‹rel_frontier S = {a}›by force moreoverhave"e ≠ -d " using‹0 < e›‹0 < d›by force ultimatelyshow False by (metis (no_types, lifting) ‹w ≠ z› eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus) next case2 thenhave z: "z ∈ rel_interior S" using‹z ∈ S› closure_subset rel_frontier_def by fastforce have"z + (z - w) ∈ affine hull S" by (metis ‹z ∈ S›‹w ∈ S› affine_affine_hull hull_inc mem_affine_3_minus scaleR_one) thenobtain e where"0 < e""(z + e *R (z - w)) ∈ rel_frontier S" using‹w ≠ z›‹w ∈ S›by (metis assms ray_to_rel_frontier right_minus_eq z) moreoverobtain d where"0 < d""(z + d *R (w - z)) ∈ rel_frontier S" using ray_to_rel_frontier [OF ‹bounded S› z, of "1 *R (w - z)"] ‹w ≠ z›‹w ∈ S› by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one) ultimatelyhave"d *R (w - z) = e *R (z - w)" using‹rel_frontier S = {a}›by force moreoverhave"e ≠ -d " using‹0 < e›‹0 < d›by force ultimatelyshow False by (metis (no_types, lifting) ‹w ≠ z› eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus) qed qed qed qed
subsection✐‹tag unimportant›‹Convexity on direct sums›
lemma closure_sum: fixes S T :: "'a::real_normed_vector set" shows"closure S + closure T ⊆ closure (S + T)" unfolding set_plus_image closure_Times [symmetric] split_def by (intro closure_bounded_linear_image_subset bounded_linear_add
bounded_linear_fst bounded_linear_snd)
lemma fst_snd_linear: "linear (λ(x,y). x + y)" unfolding linear_iff by (simp add: algebra_simps)
lemma rel_interior_sum: fixes S T :: "'n::euclidean_space set" assumes"convex S" and"convex T" shows"rel_interior (S + T) = rel_interior S + rel_interior T" proof - have"rel_interior S + rel_interior T = (λ(x,y). x + y) ` (rel_interior S × rel_interior T)" by (simp add: set_plus_image) alsohave"… = (λ(x,y). x + y) ` rel_interior (S × T)" using rel_interior_Times assms by auto alsohave"… = rel_interior (S + T)" using fst_snd_linear convex_Times assms
rel_interior_convex_linear_image[of "(λ(x,y). x + y)""S × T"] by (auto simp add: set_plus_image) finallyshow ?thesis .. qed
lemma rel_interior_sum_gen: fixes S :: "'a → 'n::euclidean_space set" assumes"∧i. i∈I ==> convex (S i)" shows"rel_interior (sum S I) = sum (λi. rel_interior (S i)) I" using rel_interior_sum rel_interior_sing[of "0"] assms by (subst sum_set_cond_linear[of convex], auto simp add: convex_set_plus)
lemma convex_rel_open_direct_sum: fixes S T :: "'n::euclidean_space set" assumes"convex S" and"rel_open S" and"convex T" and"rel_open T" shows"convex (S × T) ∧ rel_open (S × T)" by (metis assms convex_Times rel_interior_Times rel_open_def)
lemma convex_rel_open_sum: fixes S T :: "'n::euclidean_space set" assumes"convex S" and"rel_open S" and"convex T" and"rel_open T" shows"convex (S + T) ∧ rel_open (S + T)" by (metis assms convex_set_plus rel_interior_sum rel_open_def)
lemma convex_hull_finite_union_cones: assumes"finite I" and"I ≠ {}" assumes"∧i. i∈I ==> convex (S i) ∧ cone (S i) ∧ S i ≠ {}" shows"convex hull (∪(S ` I)) = sum S I"
(is"?lhs = ?rhs") proof -
{ fix x assume"x ∈ ?lhs" thenobtain c xs where
x: "x = sum (λi. c i *R xs i) I ∧ (∀i∈I. c i ≥ 0) ∧ sum c I = 1 ∧ (∀i∈I. xs i ∈ S i)" using convex_hull_finite_union[of I S] assms by auto define s where"s i = c i *R xs i"for i have"∀i∈I. s i ∈ S i" using s_def x assms by (simp add: mem_cone) moreoverhave"x = sum s I"using x s_def by auto ultimatelyhave"x ∈ ?rhs" using set_sum_alt[of I S] assms by auto
} moreover
{ fix x assume"x ∈ ?rhs" thenobtain s where x: "x = sum s I ∧ (∀i∈I. s i ∈ S i)" using set_sum_alt[of I S] assms by auto define xs where"xs i = of_nat(card I) *R s i"for i thenhave"x = sum (λi. ((1 :: real) / of_nat(card I)) *R xs i) I" using x assms by auto moreoverhave"∀i∈I. xs i ∈ S i" using x xs_def assms by (simp add: cone_def) moreoverhave"∀i∈I. (1 :: real) / of_nat (card I) ≥ 0" by auto moreoverhave"sum (λi. (1 :: real) / of_nat (card I)) I = 1" using assms by auto ultimatelyhave"x ∈ ?lhs" using assms apply (simp add: convex_hull_finite_union[of I S]) by (rule_tac x = "(λi. 1 / (card I))"in exI) auto
} ultimatelyshow ?thesis by auto qed
lemma convex_hull_union_cones_two: fixes S T :: "'m::euclidean_space set" assumes"convex S" and"cone S" and"S ≠ {}" assumes"convex T" and"cone T" and"T ≠ {}" shows"convex hull (S ∪ T) = S + T" proof - define I :: "nat set"where"I = {1, 2}" define A where"A i = (if i = (1::nat) then S else T)"for i have"∪(A ` I) = S ∪ T" using A_def I_def by auto thenhave"convex hull (∪(A ` I)) = convex hull (S ∪ T)" by auto moreoverhave"convex hull ∪(A ` I) = sum A I" using A_def I_def by (metis assms convex_hull_finite_union_cones empty_iff finite.emptyI finite.insertI insertI1) moreoverhave"sum A I = S + T" using A_def I_def by (force simp add: set_plus_def) ultimatelyshow ?thesis by auto qed
lemma rel_interior_convex_hull_union: fixes S :: "'a → 'n::euclidean_space set" assumes"finite I" and"∀i∈I. convex (S i) ∧ S i ≠ {}" shows"rel_interior (convex hull (∪(S ` I))) = {sum (λi. c i *R s i) I | c s. (∀i∈I. c i > 0) ∧ sum c I = 1 ∧ (∀i∈I. s i ∈ rel_interior(S i))}"
(is"?lhs = ?rhs") proof (cases "I = {}") case True thenshow ?thesis using convex_hull_empty by auto next case False define C0 where"C0 = convex hull (∪(S ` I))" have"∀i∈I. C0 ≥ S i" unfolding C0_def using hull_subset[of "∪(S ` I)"] by auto define K0 where"K0 = cone hull ({1 :: real} × C0)" define K where"K i = cone hull ({1 :: real} × S i)"for i have"∀i∈I. K i ≠ {}" unfolding K_def using assms by (simp add: cone_hull_empty_iff[symmetric]) have convK: "∀i∈I. convex (K i)" unfolding K_def by (simp add: assms(2) convex_Times convex_cone_hull) have"K0 ⊇ K i"if"i ∈ I"for i unfolding K0_def K_def by (simp add: Sigma_mono ‹∀i∈I. S i ⊆ C0› hull_mono that) thenhave"K0 ⊇∪(K ` I)"by auto moreoverhave"convex K0" unfolding K0_def by (simp add: C0_def convex_Times convex_cone_hull) ultimatelyhave geq: "K0 ⊇ convex hull (∪(K ` I))" using hull_minimal[of _ "K0""convex"] by blast have"∀i∈I. K i ⊇ {1 :: real} × S i" using K_def by (simp add: hull_subset) thenhave"∪(K ` I) ⊇ {1 :: real} ×∪(S ` I)" by auto thenhave"convex hull ∪(K ` I) ⊇ convex hull ({1 :: real} ×∪(S ` I))" by (simp add: hull_mono) thenhave"convex hull ∪(K ` I) ⊇ {1 :: real} × C0" unfolding C0_def using convex_hull_Times[of "{(1 :: real)}""∪(S ` I)"] convex_hull_singleton by auto moreoverhave"cone (convex hull (∪(K ` I)))" by (simp add: K_def cone_Union cone_cone_hull cone_convex_hull) ultimatelyhave"convex hull (∪(K ` I)) ⊇ K0" unfolding K0_def using hull_minimal[of _ "convex hull (∪(K ` I))""cone"] by blast thenhave"K0 = convex hull (∪(K ` I))" using geq by auto alsohave"… = sum K I" using assms False ‹∀i∈I. K i ≠ {}› cone_hull_eq convK by (intro convex_hull_finite_union_cones; fastforce simp: K_def) finallyhave"K0 = sum K I"by auto thenhave *: "rel_interior K0 = sum (λi. (rel_interior (K i))) I" using rel_interior_sum_gen[of I K] convK by auto
{ fix x assume"x ∈ ?lhs" thenhave"(1::real, x) ∈ rel_interior K0" using K0_def C0_def rel_interior_convex_cone_aux[of C0 "1::real" x] convex_convex_hull by auto thenobtain k where k: "(1::real, x) = sum k I ∧ (∀i∈I. k i ∈ rel_interior (K i))" using‹finite I› * set_sum_alt[of I "λi. rel_interior (K i)"] by auto
{ fix i assume"i ∈ I" thenhave"convex (S i) ∧ k i ∈ rel_interior (cone hull {1} × S i)" using k K_def assms by auto thenhave"∃ci si. k i = (ci, ci *R si) ∧ 0 < ci ∧ si ∈ rel_interior (S i)" using rel_interior_convex_cone[of "S i"] by auto
} thenobtain c s where cs: "∀i∈I. k i = (c i, c i *R s i) ∧ 0 < c i ∧ s i ∈ rel_interior (S i)" by metis thenhave"x = (∑i∈I. c i *R s i) ∧ sum c I = 1" using k by (simp add: sum_prod) thenhave"x ∈ ?rhs" using k cs by auto
} moreover
{ fix x assume"x ∈ ?rhs" thenobtain c s where cs: "x = sum (λi. c i *R s i) I ∧ (∀i∈I. c i > 0) ∧ sum c I = 1 ∧ (∀i∈I. s i ∈ rel_interior (S i))" by auto define k where"k i = (c i, c i *R s i)"for i
{ fix i assume"i ∈ I" thenhave"k i ∈ rel_interior (K i)" using k_def K_def assms cs rel_interior_convex_cone[of "S i"] by auto
} thenhave"(1, x) ∈ rel_interior K0" using * set_sum_alt[of I "(λi. rel_interior (K i))"] assms cs by (simp add: k_def) (metis (mono_tags, lifting) sum_prod) thenhave"x ∈ ?lhs" using K0_def C0_def rel_interior_convex_cone_aux[of C0 1 x] by auto
} ultimatelyshow ?thesis by blast qed
lemma convex_le_Inf_differential: fixes f :: "real → real" assumes"convex_on I f" and"x ∈ interior I" and"y ∈ I" shows"f y ≥ f x + Inf ((λt. (f x - f t) / (x - t)) ` ({x<..} ∩ I)) * (y - x)"
(is"_ ≥ _ + Inf (?F x) * (y - x)") proof (cases rule: linorder_cases) assume"x < y" moreover have"open (interior I)"by auto from openE[OF this ‹x ∈ interior I›] obtain e where e: "0 < e""ball x e ⊆ interior I" . moreoverdefine t where"t = min (x + e / 2) ((x + y) / 2)" ultimatelyhave"x < t""t < y""t ∈ ball x e" by (auto simp: dist_real_def field_simps split: split_min) with‹x ∈ interior I› e interior_subset[of I] have"t ∈ I""x ∈ I"by auto
define K where"K = x - e / 2" with‹0 < e›have"K ∈ ball x e""K < x" by (auto simp: dist_real_def) thenhave"K ∈ I" using‹interior I ⊆ I› e(2) by blast
have"Inf (?F x) ≤ (f x - f y) / (x - y)" proof (intro bdd_belowI cInf_lower2) show"(f x - f t) / (x - t) ∈ ?F x" using‹t ∈ I›‹x < t›by auto show"(f x - f t) / (x - t) ≤ (f x - f y) / (x - y)" using‹convex_on I f›‹x ∈ I›‹y ∈ I›‹x < t›‹t < y› by (rule convex_on_slope_le) next fix y assume"y ∈ ?F x" with order_trans[OF convex_on_slope_le[OF ‹convex_on I f›‹K ∈ I› _ ‹K < x› _]] show"(f K - f x) / (K - x) ≤ y"by auto qed thenshow ?thesis using‹x < y›by (simp add: field_simps) next assume"y < x" moreover have"open (interior I)"by auto from openE[OF this ‹x ∈ interior I›] obtain e where e: "0 < e""ball x e ⊆ interior I" . moreoverdefine t where"t = x + e / 2" ultimatelyhave"x < t""t ∈ ball x e" by (auto simp: dist_real_def field_simps) with‹x ∈ interior I› e interior_subset[of I] have"t ∈ I""x ∈ I"by auto
have"(f x - f y) / (x - y) ≤ Inf (?F x)" proof (rule cInf_greatest) have"(f x - f y) / (x - y) = (f y - f x) / (y - x)" using‹y < x›by (auto simp: field_simps) also fix z assume"z ∈ ?F x" with order_trans[OF convex_on_slope_le[OF ‹convex_on I f›‹y ∈ I› _ ‹y < x›]] have"(f y - f x) / (y - x) ≤ z" by auto finallyshow"(f x - f y) / (x - y) ≤ z" . next have"x + e / 2 ∈ ball x e" using e by (auto simp: dist_real_def) with e interior_subset[of I] have"x + e / 2 ∈ {x<..} ∩ I" by auto thenshow"?F x ≠ {}" by blast qed thenshow ?thesis using‹y < x›by (simp add: field_simps) qed simp
subsection✐‹tag unimportant›\<open>Explicit formulas for interior and relative interior of convex hull›
lemma at_within_cbox_finite: assumes"x ∈ box a b""x ∉ S""finite S" shows"(at x within cbox a b - S) = at x" proof - have"interior (cbox a b - S) = box a b - S" using‹finite S› by (simp add: interior_diff finite_imp_closed) thenshow?thesis usingat_within_interiorassmsbyfastforce qed
lemmadiffs_affine_hull_span: assumes"a\<in>S" shows"(\<lambda>x.x-a)`(affinehullS)=span((\<lambda>x.x-a)`S)" proof- have*:"((\<lambda>x.x-a)`(S-{a}))=((\<lambda>x.x-a)`S)-{0}" by(autosimp:algebra_simps) show?thesis
by (auto simp add: algebra_simps affine_hull_span2 [OF assms] *) qed
lemma aff_dim_dim_affine_diffs: fixes S :: "'a :: euclidean_space set" assumes"affine S""a ∈ S" shows"aff_dim S = dim ((λx. x - a) ` S)" proof - obtain B where aff: "affine hull B = affine hull S" and ind: "¬ affine_dependent B" and card: "of_nat (card B) = aff_dim S + 1" using aff_dim_basis_exists by blast thenhave"B ≠ {}"using assms by (metis affine_hull_eq_empty ex_in_conv) thenobtain c where"c ∈ B"by auto thenhave"c ∈ S" by (metis aff affine_hull_eq ‹affine S› hull_inc) have xy: "x - c = y - a ⟷ y = x + 1 *R (a - c)"for x y c and a::'a by (auto simp: algebra_simps) have *: "(λx. x - c) ` S = (λx. x - a) ` S" using assms ‹c ∈ S› by (auto simp: image_iff xy; metis mem_affine_3_minus pth_1) have affS: "affine hull S = S" by (simp add: ‹affine S›) have"aff_dim S = of_nat (card B) - 1" using card by simp alsohave"... = dim ((λx. x - c) ` B)" using affine_independent_card_dim_diffs [OF ind ‹c ∈ B›] by (simp add: affine_independent_card_dim_diffs [OF ind ‹c ∈ B›]) alsohave"... = dim ((λx. x - c) ` (affine hull B))" by (simp add: diffs_affine_hull_span ‹c ∈ B›) alsohave"... = dim ((λx. x - a) ` S)" by (simp add: affS aff *) finallyshow ?thesis . qed
lemma aff_dim_linear_image_le: assumes"linear f" shows"aff_dim(f ` S) ≤ aff_dim S" proof - have"aff_dim (f ` T) ≤ aff_dim T"if"affine T"for T proof (cases "T = {}") case True thenshow ?thesis by (simp add: aff_dim_geq) next case False thenobtain a where"a ∈ T"by auto have1: "((λx. x - f a) ` f ` T) = {x - f a |x. x ∈ f ` T}" by auto have2: "{x - f a| x. x ∈ f ` T} = f ` ((λx. x - a) ` T)" by (force simp: linear_diff [OF assms]) have"aff_dim (f ` T) = int (dim {x - f a |x. x ∈ f ` T})" by (simp add: ‹a ∈ T› hull_inc aff_dim_eq_dim [of "f a"] 1 cong: image_cong_simp) alsohave"... = int (dim (f ` ((λx. x - a) ` T)))" by (force simp: linear_diff [OF assms] 2) alsohave"... ≤ int (dim ((λx. x - a) ` T))" by (simp add: dim_image_le [OF assms]) alsohave"... ≤ aff_dim T" by (simp add: aff_dim_dim_affine_diffs [symmetric] ‹a ∈ T›‹affine T›) finallyshow ?thesis . qed then have"aff_dim (f ` (affine hull S)) ≤ aff_dim (affine hull S)" using affine_affine_hull [of S] by blast thenshow ?thesis using affine_hull_linear_image assms linear_conv_bounded_linear by fastforce qed
lemma aff_dim_injective_linear_image [simp]: assumes"linear f""inj f" shows"aff_dim (f ` S) = aff_dim S" proof (rule antisym) show"aff_dim (f ` S) ≤ aff_dim S" by (simp add: aff_dim_linear_image_le assms(1)) next obtain g where"linear g""g ∘ f = id" using assms(1) assms(2) linear_injective_left_inverse by blast thenhave"aff_dim S ≤ aff_dim(g ` f ` S)" by (simp add: image_comp) alsohave"... ≤ aff_dim (f ` S)" by (simp add: ‹linear g› aff_dim_linear_image_le) finallyshow"aff_dim S ≤ aff_dim (f ` S)" . qed
lemma choose_affine_subset: assumes"affine S""-1 ≤ d"and dle: "d ≤ aff_dim S" obtains T where"affine T""T ⊆ S""aff_dim T = d" proof (cases "d = -1 ∨ S={}") case True with assms show ?thesis by (metis aff_dim_empty affine_empty bot.extremum that eq_iff) next case False with assms obtain a where"a ∈ S""0 ≤ d"by auto with assms have ss: "subspace ((+) (- a) ` S)" by (simp add: affine_diffs_subspace_subtract cong: image_cong_simp) have"nat d ≤ dim ((+) (- a) ` S)" by (metis aff_dim_subspace aff_dim_translation_eq dle nat_int nat_mono ss) thenobtain T where"subspace T"and Tsb: "T ⊆ span ((+) (- a) ` S)" and Tdim: "dim T = nat d" using choose_subspace_of_subspace [of "nat d""(+) (- a) ` S"] by blast thenhave"affine T" using subspace_affine by blast thenhave"affine ((+) a ` T)" by (metis affine_hull_eq affine_hull_translation) moreoverhave"(+) a ` T ⊆ S" proof - have"T ⊆ (+) (- a) ` S" by (metis (no_types) span_eq_iff Tsb ss) thenshow"(+) a ` T ⊆ S" using add_ac by auto qed moreoverhave"aff_dim ((+) a ` T) = d" by (simp add: aff_dim_subspace Tdim ‹0 ≤ d›‹subspace T› aff_dim_translation_eq) ultimatelyshow ?thesis by (rule that) qed
subsection‹Paracompactness›
proposition paracompact: fixes S :: "'a :: {metric_space,second_countable_topology} set" assumes"S ⊆∪C"and opC: "∧T. T ∈C==> open T" obtainsC' where"S ⊆∪C'" and"∧U. U ∈C' ==> open U ∧ (∃T. T ∈C∧ U ⊆ T)" and"∧x. x ∈ S ==>∃V. open V ∧ x ∈ V ∧ finite {U. U ∈C' ∧ (U ∩ V ≠ {})}" proof (cases "S = {}") case True with that show ?thesis by blast next case False have"∃T U. x ∈ U ∧ open U ∧ closure U ⊆ T ∧ T ∈C"if"x ∈ S"for x proof - obtain T where"x ∈ T""T ∈C""open T" using assms ‹x ∈ S›by blast thenobtain e where"e > 0""cball x e ⊆ T" by (force simp: open_contains_cball) thenshow ?thesis by (meson open_ball ‹T ∈C› ball_subset_cball centre_in_ball closed_cball closure_minimal dual_order.trans) qed thenobtain F G where Gin: "x ∈ G x"and oG: "open (G x)" and clos: "closure (G x) ⊆ F x"and Fin: "F x ∈C" if"x ∈ S"for x by metis thenobtainFwhere"F⊆ G ` S""countable F""∪F = ∪(G ` S)" using Lindelof [of "G ` S"] by (metis image_iff) thenobtain K where K: "K ⊆ S""countable K"and eq: "∪(G ` K) = ∪(G ` S)" by (metis countable_subset_image) with False Gin have"K ≠ {}"by force thenobtain a :: "nat → 'a"where"range a = K" by (metis range_from_nat_into ‹countable K›) thenhave odif: "∧n. open (F (a n) - ∪{closure (G (a m)) |m. m < n})" using‹K ⊆ S› Fin opC by (fastforce simp add:) let ?C = "range (λn. F(a n) - ∪{closure(G(a m)) |m. m < n})" have enum_S: "∃n. x ∈ F(a n) ∧ x ∈ G(a n)"if"x ∈ S"for x proof - have"∃y ∈ K. x ∈ G y"using eq that Gin by fastforce thenshow ?thesis using clos K ‹range a = K› closure_subset by blast qed show ?thesis proof show"S ⊆ Union ?C" proof fix x assume"x ∈ S" define n where"n ≡ LEAST n. x ∈ F(a n)" have n: "x ∈ F(a n)" using enum_S [OF ‹x ∈ S›] by (force simp: n_def intro: LeastI) have notn: "x ∉ F(a m)"if"m < n"for m using that not_less_Least by (force simp: n_def) thenhave"x ∉∪{closure (G (a m)) |m. m < n}" using n ‹K ⊆ S›‹range a = K› clos notn by fastforce with n show"x ∈ Union ?C" by blast qed show"∧U. U ∈ ?C ==> open U ∧ (∃T. T ∈C∧ U ⊆ T)" using Fin ‹K ⊆ S›‹range a = K›by (auto simp: odif) show"∃V. open V ∧ x ∈ V ∧ finite {U. U ∈ ?C ∧ (U ∩ V ≠ {})}"if"x ∈ S"for x proof - obtain n where n: "x ∈ F(a n)""x ∈ G(a n)" using‹x ∈ S› enum_S by auto have"{U ∈ ?C. U ∩ G (a n) ≠ {}} ⊆ (λn. F(a n) - ∪{closure(G(a m)) |m. m < n}) ` atMost n" proof clarsimp fix k assume"(F (a k) - ∪{closure (G (a m)) |m. m < k}) ∩ G (a n) ≠ {}" thenhave"k ≤ n" by auto (metis closure_subset not_le subsetCE) thenshow"F (a k) - ∪{closure (G (a m)) |m. m < k} ∈ (λn. F (a n) - ∪{closure (G (a m)) |m. m < n}) ` {..n}" by force qed moreoverhave"finite ((λn. F(a n) - ∪{closure(G(a m)) |m. m < n}) ` atMost n)" by force ultimatelyhave *: "finite {U ∈ ?C. U ∩ G (a n) ≠ {}}" using finite_subset by blast have"a n ∈ S" using‹K ⊆ S›‹range a = K›by blast thenshow ?thesis by (blast intro: oG n *) qed qed qed
corollary paracompact_closedin: fixes S :: "'a :: {metric_space,second_countable_topology} set" assumes cin: "closedin (top_of_set U) S" and oin: "∧T. T ∈C==> openin (top_of_set U) T" and"S ⊆∪C" obtainsC' where"S ⊆∪C'" and"∧V. V ∈C' ==> openin (top_of_set U) V ∧ (∃T. T ∈C∧ V ⊆ T)" and"∧x. x ∈ U ==>∃V. openin (top_of_set U) V ∧ x ∈ V ∧ finite {X. X ∈C' ∧ (X ∩ V ≠ {})}" proof - have"∃Z. open Z ∧ (T = U ∩ Z)"if"T ∈C"for T using oin [OF that] by (auto simp: openin_open) thenobtain F where opF: "open (F T)"and intF: "U ∩ F T = T"if"T ∈C"for T by metis obtain K where K: "closed K""U ∩ K = S" using cin by (auto simp: closedin_closed) have1: "U ⊆∪(insert (- K) (F ` C))" by clarsimp (metis Int_iff Union_iff ‹U ∩ K = S›‹S ⊆∪C› subsetD intF) have2: "∧T. T ∈ insert (- K) (F ` C) ==> open T" using‹closed K›by (auto simp: opF) obtainDwhere"U ⊆∪D" and D1: "∧U. U ∈D==> open U ∧ (∃T. T ∈ insert (- K) (F ` C) ∧ U ⊆ T)" and D2: "∧x. x ∈ U ==>∃V. open V ∧ x ∈ V ∧ finite {U ∈D. U ∩ V ≠ {}}" by (blast intro: paracompact [OF 12]) let ?C = "{U ∩ V |V. V ∈D∧ (V ∩ K ≠ {})}" show ?thesis proof (rule_tac C' = "{U ∩ V |V. V ∈D∧ (V ∩ K ≠ {})}"in that) show"S ⊆∪?C" using‹U ∩ K = S›‹U ⊆∪D› K by (blast dest!: subsetD) show"∧V. V ∈ ?C ==> openin (top_of_set U) V ∧ (∃T. T ∈C∧ V ⊆ T)" using D1 intF by fastforce have *: "{X. (∃V. X = U ∩ V ∧ V ∈D∧ V ∩ K ≠ {}) ∧ X ∩ (U ∩ V) ≠ {}} ⊆ (λx. U ∩ x) ` {U ∈D. U ∩ V ≠ {}}"for V by blast show"∃V. openin (top_of_set U) V ∧ x ∈ V ∧ finite {X ∈ ?C. X ∩ V ≠ {}}" if"x ∈ U"for x proof - from D2 [OF that] obtain V where"open V""x ∈ V""finite {U ∈D. U ∩ V ≠ {}}" by auto with * show ?thesis by (rule_tac x="U ∩ V"in exI) (auto intro: that finite_subset [OF *]) qed qed qed
corollary✐‹tag unimportant› paracompact_closed: fixes S :: "'a :: {metric_space,second_countable_topology} set" assumes"closed S" and opC: "∧T. T ∈C==> open T" and"S ⊆∪C" obtainsC' where"S ⊆∪C'" and"∧U. U ∈C' ==> open U ∧ (∃T. T ∈C∧ U ⊆ T)" and"∧x. ∃V. open V ∧ x ∈ V ∧ finite {U. U ∈C' ∧ (U ∩ V ≠ {})}" by (rule paracompact_closedin [of UNIV S C]) (auto simp: assms)
subsection✐‹tag unimportant›\<open>Closed-graph characterization of continuity›
lemma continuous_closed_graph_gen: fixes T :: "'b::real_normed_vector set" assumes contf: "continuous_on S f"and fim: "f ` S ⊆ T" shows"closedin (top_of_set (S × T)) ((λx. Pair x (f x)) ` S)" proof - have eq: "((λx. Pair x (f x)) ` S) = (S × T ∩ (λz. (f ∘ fst)z - snd z) -` {0})" using fim by auto show ?thesis unfolding eq by (intro continuous_intros continuous_closedin_preimage continuous_on_subset [OF contf]) auto qed
lemma continuous_closed_graph_eq: fixes f :: "'a::euclidean_space → 'b::euclidean_space" assumes"compact T"and fim: "f ∈ S → T" shows"continuous_on S f ⟷ closedin (top_of_set (S × T)) ((λx. Pair x (f x)) ` S)"
(is"?lhs = ?rhs") proof - have"?lhs"if ?rhs proof (clarsimp simp add: continuous_on_closed_gen [OF fim]) fix U assume U: "closedin (top_of_set T) U" have eq: "(S ∩ f -` U) = fst ` (((λx. Pair x (f x)) ` S) ∩ (S × U))" by (force simp: image_iff) show"closedin (top_of_set S) (S ∩ f -` U)" by (simp add: U closedin_Int closedin_Times closed_map_fst [OF ‹compact T›] that eq) qed withcontinuous_closed_graph_genassmsshow?thesisbyblast qed
propositionsubspace_sum_orthogonal_comp: fixesU::"'a::euclidean_spaceset" assumes"subspaceU" shows"U+U\<^sup>\<bottom>=UNIV" proof- obtainBwhere"B\<subseteq>U" andortho:"pairwiseorthogonalB""\<And>x.x\<in>B\<Longrightarrow>normx=1" and"independentB""cardB=dimU""spanB=U" usingorthonormal_basis_subspace[OFassms]bymetis thenhave"finiteB" by(simpadd:indep_card_eq_dim_span) have*:"\<forall>x\<in>B.\<forall>y\<in>B.x\<bullet>y=(ifx=ythen1else0)" usingorthonorm_eq_1by(autosimp:orthogonal_defpairwise_def) {fixv let?u="\<Sum>b\<in>B.(v\<bullet>b)*\<^sub>Rb" have"v=?u+(v-?u)" bysimp moreoverhave"?u\<in>U" by(metis(no_types,lifting)\<open>spanB=U\<close>assmssubspace_sumspan_basespan_mul) moreoverhave"(v-?u)\<in>U\<^sup>\<bottom>" unfoldingorthogonal_comp_deforthogonal_defmem_Collect_eq proof fixy assume"y\<in>U" with\<open>spanB=U\<close>span_finite[OF\<open>finiteB\<close>] obtainuwhereu:"y=(\<Sum>b\<in>B.ub*\<^sub>Rb)" byauto have"b\<bullet>(v-?u)=0"if"b\<in>B"forb usingthat\<open>finiteB\<close>
by (simp add: * algebra_simps inner_sum_right if_distrib [of "(*)v" for v] inner_commute cong: if_cong) then show "y ∙ (v - ?u) = 0" by (simp add: u inner_sum_left) qed ultimately have "v ∈ U + U\<bottom>" using set_plus_intro by fastforce } then show ?thesis by auto qed
lemma orthogonal_Int_0: assumes "subspace U" shows "U ∩ U\<bottom> = {0}" using orthogonal_comp_def orthogonal_self by (force simp: assms subspace_0 subspace_orthogonal_comp)
lemma orthogonal_comp_self: fixes U :: "'a :: euclidean_space set" assumes "subspace U" shows "U\<bottom>\<bottom> = U" proof have ssU': "subspace (U\<bottom>)" by (simp add: subspace_orthogonal_comp) have "u ∈ U" if "u ∈ U\<bottom>\<bottom>" for u proof - obtain v w where "u = v+w" "v ∈ U" "w ∈ U\<bottom>" using subspace_sum_orthogonal_comp [OF assms] set_plus_elim by blast then have "u-v ∈ U\<bottom>" by simp moreover have "v ∈ U\<bottom>\<bottom>" using ‹v ∈ U› orthogonal_comp_subset by blast then have "u-v ∈ U\<bottom>\<bottom>" by (simp add: subspace_diff subspace_orthogonal_comp that) ultimately have "u-v = 0" using orthogonal_Int_0 ssU' by blast with ‹v ∈ U› show ?thesis by auto qed then show "U\<bottom>\<bottom> ⊆ U" by auto qed (use orthogonal_comp_subset in auto)
lemma ker_orthogonal_comp_adjoint: fixes f :: "'m::euclidean_space → 'n::euclidean_space" assumes "linear f" shows "f -` {0} = (range (adjoint f))\<bottom>" proof - have "∧x. [∀y. y ∙ f x = 0]==> f x = 0" using assms inner_commute all_zero_iff by metis then show ?thesis using assms by (auto simp: orthogonal_comp_def orthogonal_def adjoint_works inner_commute) qed
subsection✐‹tag unimportant›‹A non-injective linear function maps into a hyperplane.›
lemma linear_surj_adj_imp_inj: fixes f :: "'m::euclidean_space → 'n::euclidean_space" assumes "linear f" "surj (adjoint f)" shows "inj f" proof - have "∃x. y = adjoint f x" for y using assms by (simp add: surjD) then show "inj f" using assms unfolding inj_on_def image_def by (metis (no_types) adjoint_works euclidean_eqI) qed
\<comment> ‹🌐‹https://mathonline.wikidot.com/injectivity-and-surjectivity-of-the-adjoint-of-a-linear-map›› lemma surj_adjoint_iff_inj [simp]: fixes f :: "'m::euclidean_space → 'n::euclidean_space" assumes "linear f" shows "surj (adjoint f) ⟷ inj f" proof assume "surj (adjoint f)" then show "inj f" by (simp add: assms linear_surj_adj_imp_inj) next assume "inj f" have "f -` {0} = {0}" using assms ‹inj f› linear_0 linear_injective_0 by fastforce moreover have "f -` {0} = range (adjoint f)\<bottom>" by (intro ker_orthogonal_comp_adjoint assms) ultimately have "range (adjoint f)\<bottom>\<bottom> = UNIV" by (metis orthogonal_comp_null) then show "surj (adjoint f)" using adjoint_linear ‹linear f› by (metis linear_subspace_image orthogonal_comp_self subspace_UNIV) qed
lemma inj_adjoint_iff_surj [simp]: fixes f :: "'m::euclidean_space → 'n::euclidean_space" assumes "linear f" shows "inj (adjoint f) ⟷ surj f" proof assume "inj (adjoint f)" have "(adjoint f) -` {0} = {0}" by (metis ‹inj (adjoint f)› adjoint_linear assms surj_adjoint_iff_inj ker_orthogonal_comp_adjoint orthogonal_comp_UNIV) then have "(range(f))\<bottom> = {0}" by (metis (no_types, opaque_lifting) adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint set_zero) then show "surj f" by (metis ‹inj (adjoint f)› adjoint_adjoint adjoint_linear assms surj_adjoint_iff_inj) next assume "surj f" then have "range f = (adjoint f -` {0})\<bottom>" by (simp add: adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint) then have "{0} = adjoint f -` {0}" using ‹surj f› adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint by force then show "inj (adjoint f)" by (simp add: ‹surj f› adjoint_adjoint adjoint_linear assms linear_surj_adj_imp_inj) qed
lemma linear_singular_into_hyperplane: fixes f :: "'n::euclidean_space → 'n" assumes "linear f" shows "¬ inj f ⟷ (∃a. a ≠0∧ (∀x. a ∙ f x = 0))" (is "_ = ?rhs") proof assume "¬inj f" then show ?rhs using all_zero_iff by (metis (no_types, opaque_lifting) adjoint_clauses(2) adjoint_linear assms linear_injective_0 linear_injective_imp_surjective linear_surj_adj_imp_inj) next assume ?rhs then show "¬inj f" by (metis assms linear_injective_isomorphism all_zero_iff) qed
lemma linear_singular_image_hyperplane: fixes f :: "'n::euclidean_space → 'n" assumes "linear f" "¬inj f" obtains a where "a ≠0" "∧S. f ` S ⊆ {x. a ∙ x = 0}" using assms by (fastforce simp add: linear_singular_into_hyperplane)
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 1.267 Sekunden
(vorverarbeitet am 2026-06-30)
¤
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 und die Messung sind noch experimentell.