(* Title: HOL/Analysis/Starlike.thy Author: L C Paulson, University of Cambridge Author: Robert Himmelmann, TU Muenchen Author: Bogdan Grechuk, University of Edinburgh Author: Armin Heller, TU Muenchen Author: Johannes Hoelzl, TU Muenchen *) section ‹Line segments, Starlike Sets, etc› theory Starlike imports Convex_Euclidean_Space begin subsection ‹Midpoint› definition%important midpoint :: "'a::real_vector ⇒ 'a ⇒ 'a" where "midpoint a b = (inverse (2::real)) *⇩_{R}(a + b)" lemma midpoint_idem [simp]: "midpoint x x = x" unfolding midpoint_def by simp lemma midpoint_sym: "midpoint a b = midpoint b a" unfolding midpoint_def by (auto simp add: scaleR_right_distrib) lemma midpoint_eq_iff: "midpoint a b = c ⟷ a + b = c + c" proof - have "midpoint a b = c ⟷ scaleR 2 (midpoint a b) = scaleR 2 c" by simp then show ?thesis unfolding midpoint_def scaleR_2 [symmetric] by simp qed lemma fixes a::real assumes "a ≤ b" shows ge_midpoint_1: "a ≤ midpoint a b" and le_midpoint_1: "midpoint a b ≤ b" by (simp_all add: midpoint_def assms) lemma dist_midpoint: fixes a b :: "'a::real_normed_vector" shows "dist a (midpoint a b) = (dist a b) / 2" (is ?t1) "dist b (midpoint a b) = (dist a b) / 2" (is ?t2) "dist (midpoint a b) a = (dist a b) / 2" (is ?t3) "dist (midpoint a b) b = (dist a b) / 2" (is ?t4) proof - have *: "⋀x y::'a. 2 *⇩_{R}x = - y ⟹ norm x = (norm y) / 2" unfolding equation_minus_iff by auto have **: "⋀x y::'a. 2 *⇩_{R}x = y ⟹ norm x = (norm y) / 2" by auto note scaleR_right_distrib [simp] show ?t1 unfolding midpoint_def dist_norm apply (rule **) apply (simp add: scaleR_right_diff_distrib) apply (simp add: scaleR_2) done show ?t2 unfolding midpoint_def dist_norm apply (rule *) apply (simp add: scaleR_right_diff_distrib) apply (simp add: scaleR_2) done show ?t3 unfolding midpoint_def dist_norm apply (rule *) apply (simp add: scaleR_right_diff_distrib) apply (simp add: scaleR_2) done show ?t4 unfolding midpoint_def dist_norm apply (rule **) apply (simp add: scaleR_right_diff_distrib) apply (simp add: scaleR_2) done qed lemma midpoint_eq_endpoint [simp]: "midpoint a b = a ⟷ a = b" "midpoint a b = b ⟷ a = b" unfolding midpoint_eq_iff by auto lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b" using midpoint_eq_iff by metis lemma midpoint_linear_image: "linear f ⟹ midpoint(f a)(f b) = f(midpoint a b)" by (simp add: linear_iff midpoint_def) subsection ‹Line segments› definition%important closed_segment :: "'a::real_vector ⇒ 'a ⇒ 'a set" where "closed_segment a b = {(1 - u) *⇩_{R}a + u *⇩_{R}b | u::real. 0 ≤ u ∧ u ≤ 1}" definition%important open_segment :: "'a::real_vector ⇒ 'a ⇒ 'a set" where "open_segment a b ≡ closed_segment a b - {a,b}" lemmas segment = open_segment_def closed_segment_def lemma in_segment: "x ∈ closed_segment a b ⟷ (∃u. 0 ≤ u ∧ u ≤ 1 ∧ x = (1 - u) *⇩_{R}a + u *⇩_{R}b)" "x ∈ open_segment a b ⟷ a ≠ b ∧ (∃u. 0 < u ∧ u < 1 ∧ x = (1 - u) *⇩_{R}a + u *⇩_{R}b)" using less_eq_real_def by (auto simp: segment algebra_simps) lemma closed_segment_linear_image: "closed_segment (f a) (f b) = f ` (closed_segment a b)" if "linear f" proof - interpret linear f by fact show ?thesis by (force simp add: in_segment add scale) qed lemma open_segment_linear_image: "⟦linear f; inj f⟧ ⟹ open_segment (f a) (f b) = f ` (open_segment a b)" by (force simp: open_segment_def closed_segment_linear_image inj_on_def) lemma closed_segment_translation: "closed_segment (c + a) (c + b) = image (λx. c + x) (closed_segment a b)" apply safe apply (rule_tac x="x-c" in image_eqI) apply (auto simp: in_segment algebra_simps) done lemma open_segment_translation: "open_segment (c + a) (c + b) = image (λx. c + x) (open_segment a b)" by (simp add: open_segment_def closed_segment_translation translation_diff) lemma closed_segment_of_real: "closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y" apply (auto simp: image_iff in_segment scaleR_conv_of_real) apply (rule_tac x="(1-u)*x + u*y" in bexI) apply (auto simp: in_segment) done lemma open_segment_of_real: "open_segment (of_real x) (of_real y) = of_real ` open_segment x y" apply (auto simp: image_iff in_segment scaleR_conv_of_real) apply (rule_tac x="(1-u)*x + u*y" in bexI) apply (auto simp: in_segment) done lemma closed_segment_Reals: "⟦x ∈ Reals; y ∈ Reals⟧ ⟹ closed_segment x y = of_real ` closed_segment (Re x) (Re y)" by (metis closed_segment_of_real of_real_Re) lemma open_segment_Reals: "⟦x ∈ Reals; y ∈ Reals⟧ ⟹ open_segment x y = of_real ` open_segment (Re x) (Re y)" by (metis open_segment_of_real of_real_Re) lemma open_segment_PairD: "(x, x') ∈ open_segment (a, a') (b, b') ⟹ (x ∈ open_segment a b ∨ a = b) ∧ (x' ∈ open_segment a' b' ∨ a' = b')" by (auto simp: in_segment) lemma closed_segment_PairD: "(x, x') ∈ closed_segment (a, a') (b, b') ⟹ x ∈ closed_segment a b ∧ x' ∈ closed_segment a' b'" by (auto simp: closed_segment_def) lemma closed_segment_translation_eq [simp]: "d + x ∈ closed_segment (d + a) (d + b) ⟷ x ∈ closed_segment a b" proof - have *: "⋀d x a b. x ∈ closed_segment a b ⟹ d + x ∈ closed_segment (d + a) (d + b)" apply (simp add: closed_segment_def) apply (erule ex_forward) apply (simp add: algebra_simps) done show ?thesis using * [where d = "-d"] * by (fastforce simp add:) qed lemma open_segment_translation_eq [simp]: "d + x ∈ open_segment (d + a) (d + b) ⟷ x ∈ open_segment a b" by (simp add: open_segment_def) lemma of_real_closed_segment [simp]: "of_real x ∈ closed_segment (of_real a) (of_real b) ⟷ x ∈ closed_segment a b" apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward) using of_real_eq_iff by fastforce lemma of_real_open_segment [simp]: "of_real x ∈ open_segment (of_real a) (of_real b) ⟷ x ∈ open_segment a b" apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE) using of_real_eq_iff by fastforce lemma convex_contains_segment: "convex S ⟷ (∀a∈S. ∀b∈S. closed_segment a b ⊆ S)" unfolding convex_alt closed_segment_def by auto lemma closed_segment_in_Reals: "⟦x ∈ closed_segment a b; a ∈ Reals; b ∈ Reals⟧ ⟹ x ∈ Reals" by (meson subsetD convex_Reals convex_contains_segment) lemma open_segment_in_Reals: "⟦x ∈ open_segment a b; a ∈ Reals; b ∈ Reals⟧ ⟹ x ∈ Reals" by (metis Diff_iff closed_segment_in_Reals open_segment_def) lemma closed_segment_subset: "⟦x ∈ S; y ∈ S; convex S⟧ ⟹ closed_segment x y ⊆ S" by (simp add: convex_contains_segment) lemma closed_segment_subset_convex_hull: "⟦x ∈ convex hull S; y ∈ convex hull S⟧ ⟹ closed_segment x y ⊆ convex hull S" using convex_contains_segment by blast lemma segment_convex_hull: "closed_segment a b = convex hull {a,b}" proof - have *: "⋀x. {x} ≠ {}" by auto show ?thesis unfolding segment convex_hull_insert[OF *] convex_hull_singleton by (safe; rule_tac x="1 - u" in exI; force) qed lemma open_closed_segment: "u ∈ open_segment w z ⟹ u ∈ closed_segment w z" by (auto simp add: closed_segment_def open_segment_def) lemma segment_open_subset_closed: "open_segment a b ⊆ closed_segment a b" by (auto simp: closed_segment_def open_segment_def) lemma bounded_closed_segment: fixes a :: "'a::euclidean_space" shows "bounded (closed_segment a b)" by (simp add: segment_convex_hull compact_convex_hull compact_imp_bounded) lemma bounded_open_segment: fixes a :: "'a::euclidean_space" shows "bounded (open_segment a b)" by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed]) lemmas bounded_segment = bounded_closed_segment open_closed_segment lemma ends_in_segment [iff]: "a ∈ closed_segment a b" "b ∈ closed_segment a b" unfolding segment_convex_hull by (auto intro!: hull_subset[unfolded subset_eq, rule_format]) lemma eventually_closed_segment: fixes x0::"'a::real_normed_vector" assumes "open X0" "x0 ∈ X0" shows "∀⇩_{F}x in at x0 within U. closed_segment x0 x ⊆ X0" proof - from openE[OF assms] obtain e where e: "0 < e" "ball x0 e ⊆ X0" . then have "∀⇩_{F}x in at x0 within U. x ∈ ball x0 e" by (auto simp: dist_commute eventually_at) then show ?thesis proof eventually_elim case (elim x) have "x0 ∈ ball x0 e" using ‹e > 0› by simp from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim] have "closed_segment x0 x ⊆ ball x0 e" . also note ‹… ⊆ X0› finally show ?case . qed qed lemma segment_furthest_le: fixes a b x y :: "'a::euclidean_space" assumes "x ∈ closed_segment a b" shows "norm (y - x) ≤ norm (y - a) ∨ norm (y - x) ≤ norm (y - b)" proof - obtain z where "z ∈ {a, b}" "norm (x - y) ≤ norm (z - y)" using simplex_furthest_le[of "{a, b}" y] using assms[unfolded segment_convex_hull] by auto then show ?thesis by (auto simp add:norm_minus_commute) qed lemma closed_segment_commute: "closed_segment a b = closed_segment b a" proof - have "{a, b} = {b, a}" by auto thus ?thesis by (simp add: segment_convex_hull) qed lemma segment_bound1: assumes "x ∈ closed_segment a b" shows "norm (x - a) ≤ norm (b - a)" proof - obtain u where "x = (1 - u) *⇩_{R}a + u *⇩_{R}b" "0 ≤ u" "u ≤ 1" using assms by (auto simp add: closed_segment_def) then show "norm (x - a) ≤ norm (b - a)" apply clarify apply (auto simp: algebra_simps) apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le) done qed lemma segment_bound: assumes "x ∈ closed_segment a b" shows "norm (x - a) ≤ norm (b - a)" "norm (x - b) ≤ norm (b - a)" apply (simp add: assms segment_bound1) by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1) lemma open_segment_commute: "open_segment a b = open_segment b a" proof - have "{a, b} = {b, a}" by auto thus ?thesis by (simp add: closed_segment_commute open_segment_def) qed lemma closed_segment_idem [simp]: "closed_segment a a = {a}" unfolding segment by (auto simp add: algebra_simps) lemma open_segment_idem [simp]: "open_segment a a = {}" by (simp add: open_segment_def) lemma closed_segment_eq_open: "closed_segment a b = open_segment a b ∪ {a,b}" using open_segment_def by auto lemma convex_contains_open_segment: "convex s ⟷ (∀a∈s. ∀b∈s. open_segment a b ⊆ s)" by (simp add: convex_contains_segment closed_segment_eq_open) lemma closed_segment_eq_real_ivl: fixes a b::real shows "closed_segment a b = (if a ≤ b then {a .. b} else {b .. a})" proof - have "b ≤ a ⟹ closed_segment b a = {b .. a}" and "a ≤ b ⟹ closed_segment a b = {a .. b}" by (auto simp: convex_hull_eq_real_cbox segment_convex_hull) thus ?thesis by (auto simp: closed_segment_commute) qed lemma open_segment_eq_real_ivl: fixes a b::real shows "open_segment a b = (if a ≤ b then {a<..<b} else {b<..<a})" by (auto simp: closed_segment_eq_real_ivl open_segment_def split: if_split_asm) lemma closed_segment_real_eq: fixes u::real shows "closed_segment u v = (λx. (v - u) * x + u) ` {0..1}" by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl) lemma dist_in_closed_segment: fixes a :: "'a :: euclidean_space" assumes "x ∈ closed_segment a b" shows "dist x a ≤ dist a b ∧ dist x b ≤ dist a b" proof (intro conjI) obtain u where u: "0 ≤ u" "u ≤ 1" and x: "x = (1 - u) *⇩_{R}a + u *⇩_{R}b" using assms by (force simp: in_segment algebra_simps) have "dist x a = u * dist a b" apply (simp add: dist_norm algebra_simps x) by (metis ‹0 ≤ u› abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib) also have "... ≤ dist a b" by (simp add: mult_left_le_one_le u) finally show "dist x a ≤ dist a b" . have "dist x b = norm ((1-u) *⇩_{R}a - (1-u) *⇩_{R}b)" by (simp add: dist_norm algebra_simps x) also have "... = (1-u) * dist a b" proof - have "norm ((1 - 1 * u) *⇩_{R}(a - b)) = (1 - 1 * u) * norm (a - b)" using ‹u ≤ 1› by force then show ?thesis by (simp add: dist_norm real_vector.scale_right_diff_distrib) qed also have "... ≤ dist a b" by (simp add: mult_left_le_one_le u) finally show "dist x b ≤ dist a b" . qed lemma dist_in_open_segment: fixes a :: "'a :: euclidean_space" assumes "x ∈ open_segment a b" shows "dist x a < dist a b ∧ dist x b < dist a b" proof (intro conjI) obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *⇩_{R}a + u *⇩_{R}b" using assms by (force simp: in_segment algebra_simps) have "dist x a = u * dist a b" apply (simp add: dist_norm algebra_simps x) by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib ‹0 < u›) also have *: "... < dist a b" by (metis (no_types) assms dist_eq_0_iff dist_not_less_zero in_segment(2) linorder_neqE_linordered_idom mult.left_neutral real_mult_less_iff1 ‹u < 1›) finally show "dist x a < dist a b" . have ab_ne0: "dist a b ≠ 0" using * by fastforce have "dist x b = norm ((1-u) *⇩_{R}a - (1-u) *⇩_{R}b)" by (simp add: dist_norm algebra_simps x) also have "... = (1-u) * dist a b" proof - have "norm ((1 - 1 * u) *⇩_{R}(a - b)) = (1 - 1 * u) * norm (a - b)" using ‹u < 1› by force then show ?thesis by (simp add: dist_norm real_vector.scale_right_diff_distrib) qed also have "... < dist a b" using ab_ne0 ‹0 < u› by simp finally show "dist x b < dist a b" . qed lemma dist_decreases_open_segment_0: fixes x :: "'a :: euclidean_space" assumes "x ∈ open_segment 0 b" shows "dist c x < dist c 0 ∨ dist c x < dist c b" proof (rule ccontr, clarsimp simp: not_less) obtain u where u: "0 ≠ b" "0 < u" "u < 1" and x: "x = u *⇩_{R}b" using assms by (auto simp: in_segment) have xb: "x ∙ b < b ∙ b" using u x by auto assume "norm c ≤ dist c x" then have "c ∙ c ≤ (c - x) ∙ (c - x)" by (simp add: dist_norm norm_le) moreover have "0 < x ∙ b" using u x by auto ultimately have less: "c ∙ b < x ∙ b" by (simp add: x algebra_simps inner_commute u) assume "dist c b ≤ dist c x" then have "(c - b) ∙ (c - b) ≤ (c - x) ∙ (c - x)" by (simp add: dist_norm norm_le) then have "(b ∙ b) * (1 - u*u) ≤ 2 * (b ∙ c) * (1-u)" by (simp add: x algebra_simps inner_commute) then have "(1+u) * (b ∙ b) * (1-u) ≤ 2 * (b ∙ c) * (1-u)" by (simp add: algebra_simps) then have "(1+u) * (b ∙ b) ≤ 2 * (b ∙ c)" using ‹u < 1› by auto with xb have "c ∙ b ≥ x ∙ b" by (auto simp: x algebra_simps inner_commute) with less show False by auto qed proposition dist_decreases_open_segment: fixes a :: "'a :: euclidean_space" assumes "x ∈ open_segment a b" shows "dist c x < dist c a ∨ dist c x < dist c b" proof - have *: "x - a ∈ open_segment 0 (b - a)" using assms by (metis diff_self open_segment_translation_eq uminus_add_conv_diff) show ?thesis using dist_decreases_open_segment_0 [OF *, of "c-a"] assms by (simp add: dist_norm) qed corollary open_segment_furthest_le: fixes a b x y :: "'a::euclidean_space" assumes "x ∈ open_segment a b" shows "norm (y - x) < norm (y - a) ∨ norm (y - x) < norm (y - b)" by (metis assms dist_decreases_open_segment dist_norm) corollary dist_decreases_closed_segment: fixes a :: "'a :: euclidean_space" assumes "x ∈ closed_segment a b" shows "dist c x ≤ dist c a ∨ dist c x ≤ dist c b" apply (cases "x ∈ open_segment a b") using dist_decreases_open_segment less_eq_real_def apply blast by (metis DiffI assms empty_iff insertE open_segment_def order_refl) lemma convex_intermediate_ball: fixes a :: "'a :: euclidean_space" shows "⟦ball a r ⊆ T; T ⊆ cball a r⟧ ⟹ convex T" apply (simp add: convex_contains_open_segment, clarify) by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment) lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b ⊆ closed_segment a b" apply (clarsimp simp: midpoint_def in_segment) apply (rule_tac x="(1 + u) / 2" in exI) apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib) by (metis field_sum_of_halves scaleR_left.add) lemma notin_segment_midpoint: fixes a :: "'a :: euclidean_space" shows "a ≠ b ⟹ a ∉ closed_segment (midpoint a b) b" by (auto simp: dist_midpoint dest!: dist_in_closed_segment) lemma segment_to_closest_point: fixes S :: "'a :: euclidean_space set" shows "⟦closed S; S ≠ {}⟧ ⟹ open_segment a (closest_point S a) ∩ S = {}" apply (subst disjoint_iff_not_equal) apply (clarify dest!: dist_in_open_segment) by (metis closest_point_le dist_commute le_less_trans less_irrefl) lemma segment_to_point_exists: fixes S :: "'a :: euclidean_space set" assumes "closed S" "S ≠ {}" obtains b where "b ∈ S" "open_segment a b ∩ S = {}" by (metis assms segment_to_closest_point closest_point_exists that) subsubsection‹More lemmas, especially for working with the underlying formula› lemma segment_eq_compose: fixes a :: "'a :: real_vector" shows "(λu. (1 - u) *⇩_{R}a + u *⇩_{R}b) = (λx. a + x) o (λu. u *⇩_{R}(b - a))" by (simp add: o_def algebra_simps) lemma segment_degen_1: fixes a :: "'a :: real_vector" shows "(1 - u) *⇩_{R}a + u *⇩_{R}b = b ⟷ a=b ∨ u=1" proof - { assume "(1 - u) *⇩_{R}a + u *⇩_{R}b = b" then have "(1 - u) *⇩_{R}a = (1 - u) *⇩_{R}b" by (simp add: algebra_simps) then have "a=b ∨ u=1" by simp } then show ?thesis by (auto simp: algebra_simps) qed lemma segment_degen_0: fixes a :: "'a :: real_vector" shows "(1 - u) *⇩_{R}a + u *⇩_{R}b = a ⟷ a=b ∨ u=0" using segment_degen_1 [of "1-u" b a] by (auto simp: algebra_simps) lemma add_scaleR_degen: fixes a b ::"'a::real_vector" assumes "(u *⇩_{R}b + v *⇩_{R}a) = (u *⇩_{R}a + v *⇩_{R}b)" "u ≠ v" shows "a=b" by (metis (no_types, hide_lams) add.commute add_diff_eq diff_add_cancel real_vector.scale_cancel_left real_vector.scale_left_diff_distrib assms) lemma closed_segment_image_interval: "closed_segment a b = (λu. (1 - u) *⇩_{R}a + u *⇩_{R}b) ` {0..1}" by (auto simp: set_eq_iff image_iff closed_segment_def) lemma open_segment_image_interval: "open_segment a b = (if a=b then {} else (λu. (1 - u) *⇩_{R}a + u *⇩_{R}b) ` {0<..<1})" by (auto simp: open_segment_def closed_segment_def segment_degen_0 segment_degen_1) lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval lemma open_segment_bound1: assumes "x ∈ open_segment a b" shows "norm (x - a) < norm (b - a)" proof - obtain u where "x = (1 - u) *⇩_{R}a + u *⇩_{R}b" "0 < u" "u < 1" "a ≠ b" using assms by (auto simp add: open_segment_image_interval split: if_split_asm) then show "norm (x - a) < norm (b - a)" apply clarify apply (auto simp: algebra_simps) apply (simp add: scaleR_diff_right [symmetric]) done qed lemma compact_segment [simp]: fixes a :: "'a::real_normed_vector" shows "compact (closed_segment a b)" by (auto simp: segment_image_interval intro!: compact_continuous_image continuous_intros) lemma closed_segment [simp]: fixes a :: "'a::real_normed_vector" shows "closed (closed_segment a b)" by (simp add: compact_imp_closed) lemma closure_closed_segment [simp]: fixes a :: "'a::real_normed_vector" shows "closure(closed_segment a b) = closed_segment a b" by simp lemma open_segment_bound: assumes "x ∈ open_segment a b" shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)" apply (simp add: assms open_segment_bound1) by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute) lemma closure_open_segment [simp]: fixes a :: "'a::euclidean_space" shows "closure(open_segment a b) = (if a = b then {} else closed_segment a b)" proof - have "closure ((λu. u *⇩_{R}(b - a)) ` {0<..<1}) = (λu. u *⇩_{R}(b - a)) ` closure {0<..<1}" if "a ≠ b" apply (rule closure_injective_linear_image [symmetric]) apply (simp add:) using that by (simp add: inj_on_def) then show ?thesis by (simp add: segment_image_interval segment_eq_compose closure_greaterThanLessThan [symmetric] closure_translation image_comp [symmetric] del: closure_greaterThanLessThan) qed lemma closed_open_segment_iff [simp]: fixes a :: "'a::euclidean_space" shows "closed(open_segment a b) ⟷ a = b" by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2)) lemma compact_open_segment_iff [simp]: fixes a :: "'a::euclidean_space" shows "compact(open_segment a b) ⟷ a = b" by (simp add: bounded_open_segment compact_eq_bounded_closed) lemma convex_closed_segment [iff]: "convex (closed_segment a b)" unfolding segment_convex_hull by(rule convex_convex_hull) lemma convex_open_segment [iff]: "convex(open_segment a b)" proof - have "convex ((λu. u *⇩_{R}(b-a)) ` {0<..<1})" by (rule convex_linear_image) auto then show ?thesis apply (simp add: open_segment_image_interval segment_eq_compose) by (metis image_comp convex_translation) qed lemmas convex_segment = convex_closed_segment convex_open_segment lemma connected_segment [iff]: fixes x :: "'a :: real_normed_vector" shows "connected (closed_segment x y)" by (simp add: convex_connected) lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real by (auto simp: is_interval_convex_1) lemma IVT'_closed_segment_real: fixes f :: "real ⇒ real" assumes "y ∈ closed_segment (f a) (f b)" assumes "continuous_on (closed_segment a b) f" shows "∃x ∈ closed_segment a b. f x = y" using IVT'[of f a y b] IVT'[of "-f" a "-y" b] IVT'[of f b y a] IVT'[of "-f" b "-y" a] assms by (cases "a ≤ b"; cases "f b ≥ f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus) subsection‹Starlike sets› definition%important "starlike S ⟷ (∃a∈S. ∀x∈S. closed_segment a x ⊆ S)" lemma starlike_UNIV [simp]: "starlike UNIV" by (simp add: starlike_def) lemma convex_imp_starlike: "convex S ⟹ S ≠ {} ⟹ starlike S" unfolding convex_contains_segment starlike_def by auto 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" then show "x ∈ rel_interior S" unfolding closed_segment_def open_segment_def using assms by (auto intro: rel_interior_closure_convex_shrink) qed lemma convex_hull_insert_segments: "convex hull (insert a S) = (if S = {} then {a} else ⋃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) then show "?lhs ⊆ ?rhs" proof (clarsimp simp add: convex_hull_insert_segments) fix x y assume "x ∈ S" and y: "y ∈ convex hull T" and "x ∈ closed_segment z y" have "y ∈ closure C" by (metis y ‹convex C› ‹T ⊆ C› closure_subset contra_subsetD convex_hull_eq hull_mono) moreover have "x ∉ rel_interior C" by (meson ‹x ∈ S› dis disjnt_iff) moreover have "x ∈ open_segment z y ∪ {z, y}" using ‹x ∈ closed_segment z y› closed_segment_eq_open by blast ultimately show "x ∈ convex hull T" using rel_interior_closure_convex_segment [OF ‹convex C› z] using y z by blast qed show "?rhs ⊆ ?lhs" by (meson hull_mono inf_mono subset_insertI subset_refl) qed subsection%unimportant‹More results about segments› lemma dist_half_times2: fixes a :: "'a :: real_normed_vector" shows "dist ((1 / 2) *⇩_{R}(a + b)) x * 2 = dist (a+b) (2 *⇩_{R}x)" proof - have "norm ((1 / 2) *⇩_{R}(a + b) - x) * 2 = norm (2 *⇩_{R}((1 / 2) *⇩_{R}(a + b) - x))" by simp also have "... = norm ((a + b) - 2 *⇩_{R}x)" by (simp add: real_vector.scale_right_diff_distrib) finally show ?thesis by (simp only: dist_norm) qed lemma closed_segment_as_ball: "closed_segment a b = affine hull {a,b} ∩ cball(inverse 2 *⇩_{R}(a + b))(norm(b - a) / 2)" proof (cases "b = a") case True then show ?thesis by (auto simp: hull_inc) next case False then have *: "((∃u v. x = u *⇩_{R}a + v *⇩_{R}b ∧ u + v = 1) ∧ dist ((1 / 2) *⇩_{R}(a + b)) x * 2 ≤ norm (b - a)) = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ 0 ≤ u ∧ u ≤ 1)" for x proof - have "((∃u v. x = u *⇩_{R}a + v *⇩_{R}b ∧ u + v = 1) ∧ dist ((1 / 2) *⇩_{R}(a + b)) x * 2 ≤ norm (b - a)) = ((∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b) ∧ dist ((1 / 2) *⇩_{R}(a + b)) x * 2 ≤ norm (b - a))" unfolding eq_diff_eq [symmetric] by simp also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ norm ((a+b) - (2 *⇩_{R}x)) ≤ norm (b - a))" by (simp add: dist_half_times2) (simp add: dist_norm) also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ norm ((a+b) - (2 *⇩_{R}((1 - u) *⇩_{R}a + u *⇩_{R}b))) ≤ norm (b - a))" by auto also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ norm ((1 - u * 2) *⇩_{R}(b - a)) ≤ norm (b - a))" by (simp add: algebra_simps scaleR_2) also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ ¦1 - u * 2¦ * norm (b - a) ≤ norm (b - a))" by simp also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ ¦1 - u * 2¦ ≤ 1)" by (simp add: mult_le_cancel_right2 False) also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ 0 ≤ u ∧ u ≤ 1)" by auto finally show ?thesis . qed show ?thesis by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *) qed lemma open_segment_as_ball: "open_segment a b = affine hull {a,b} ∩ ball(inverse 2 *⇩_{R}(a + b))(norm(b - a) / 2)" proof (cases "b = a") case True then show ?thesis by (auto simp: hull_inc) next case False then have *: "((∃u v. x = u *⇩_{R}a + v *⇩_{R}b ∧ u + v = 1) ∧ dist ((1 / 2) *⇩_{R}(a + b)) x * 2 < norm (b - a)) = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ 0 < u ∧ u < 1)" for x proof - have "((∃u v. x = u *⇩_{R}a + v *⇩_{R}b ∧ u + v = 1) ∧ dist ((1 / 2) *⇩_{R}(a + b)) x * 2 < norm (b - a)) = ((∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b) ∧ dist ((1 / 2) *⇩_{R}(a + b)) x * 2 < norm (b - a))" unfolding eq_diff_eq [symmetric] by simp also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ norm ((a+b) - (2 *⇩_{R}x)) < norm (b - a))" by (simp add: dist_half_times2) (simp add: dist_norm) also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ norm ((a+b) - (2 *⇩_{R}((1 - u) *⇩_{R}a + u *⇩_{R}b))) < norm (b - a))" by auto also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ norm ((1 - u * 2) *⇩_{R}(b - a)) < norm (b - a))" by (simp add: algebra_simps scaleR_2) also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ ¦1 - u * 2¦ * norm (b - a) < norm (b - a))" by simp also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ ¦1 - u * 2¦ < 1)" by (simp add: mult_le_cancel_right2 False) also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ 0 < u ∧ u < 1)" by auto finally show ?thesis . qed show ?thesis using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *) qed lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball lemma closed_segment_neq_empty [simp]: "closed_segment a b ≠ {}" by auto lemma open_segment_eq_empty [simp]: "open_segment a b = {} ⟷ a = b" proof - { assume a1: "open_segment a b = {}" have "{} ≠ {0::real<..<1}" by simp then have "a = b" using a1 open_segment_image_interval by fastforce } then show ?thesis by auto qed lemma open_segment_eq_empty' [simp]: "{} = open_segment a b ⟷ a = b" using open_segment_eq_empty by blast lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty lemma inj_segment: fixes a :: "'a :: real_vector" assumes "a ≠ b" shows "inj_on (λu. (1 - u) *⇩_{R}a + u *⇩_{R}b) I" proof fix x y assume "(1 - x) *⇩_{R}a + x *⇩_{R}b = (1 - y) *⇩_{R}a + y *⇩_{R}b" then have "x *⇩_{R}(b - a) = y *⇩_{R}(b - a)" by (simp add: algebra_simps) with assms show "x = y" by (simp add: real_vector.scale_right_imp_eq) qed lemma finite_closed_segment [simp]: "finite(closed_segment a b) ⟷ a = b" apply auto apply (rule ccontr) apply (simp add: segment_image_interval) using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast done lemma finite_open_segment [simp]: "finite(open_segment a b) ⟷ a = b" by (auto simp: open_segment_def) lemmas finite_segment = finite_closed_segment finite_open_segment lemma closed_segment_eq_sing: "closed_segment a b = {c} ⟷ a = c ∧ b = c" by auto lemma open_segment_eq_sing: "open_segment a b ≠ {c}" by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval) lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing lemma subset_closed_segment: "closed_segment a b ⊆ closed_segment c d ⟷ a ∈ closed_segment c d ∧ b ∈ closed_segment c d" by auto (meson contra_subsetD convex_closed_segment convex_contains_segment) lemma subset_co_segment: "closed_segment a b ⊆ open_segment c d ⟷ a ∈ open_segment c d ∧ b ∈ open_segment c d" using closed_segment_subset by blast lemma subset_open_segment: fixes a :: "'a::euclidean_space" shows "open_segment a b ⊆ open_segment c d ⟷ a = b ∨ a ∈ closed_segment c d ∧ b ∈ closed_segment c d" (is "?lhs = ?rhs") proof (cases "a = b") case True then show ?thesis by simp next case False show ?thesis proof assume rhs: ?rhs with ‹a ≠ b› have "c ≠ d" using closed_segment_idem singleton_iff by auto have "∃uc. (1 - u) *⇩_{R}((1 - ua) *⇩_{R}c + ua *⇩_{R}d) + u *⇩_{R}((1 - ub) *⇩_{R}c + ub *⇩_{R}d) = (1 - uc) *⇩_{R}c + uc *⇩_{R}d ∧ 0 < uc ∧ uc < 1" if neq: "(1 - ua) *⇩_{R}c + ua *⇩_{R}d ≠ (1 - ub) *⇩_{R}c + ub *⇩_{R}d" "c ≠ d" and "a = (1 - ua) *⇩_{R}c + ua *⇩_{R}d" "b = (1 - ub) *⇩_{R}c + ub *⇩_{R}d" and u: "0 < u" "u < 1" and uab: "0 ≤ ua" "ua ≤ 1" "0 ≤ ub" "ub ≤ 1" for u ua ub proof - have "ua ≠ ub" using neq by auto moreover have "(u - 1) * ua ≤ 0" using u uab by (simp add: mult_nonpos_nonneg) ultimately have lt: "(u - 1) * ua < u * ub" using u uab by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less) have "p * ua + q * ub < p+q" if p: "0 < p" and q: "0 < q" for p q proof - have "¬ p ≤ 0" "¬ q ≤ 0" using p q not_less by blast+ then show ?thesis by (metis ‹ua ≠ ub› add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5) less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4)) qed then have "(1 - u) * ua + u * ub < 1" using u ‹ua ≠ ub› by (metis diff_add_cancel diff_gt_0_iff_gt) with lt show ?thesis by (rule_tac x="ua + u*(ub-ua)" in exI) (simp add: algebra_simps) qed with rhs ‹a ≠ b› ‹c ≠ d› show ?lhs unfolding open_segment_image_interval closed_segment_def by (fastforce simp add:) next assume lhs: ?lhs with ‹a ≠ b› have "c ≠ d" by (meson finite_open_segment rev_finite_subset) have "closure (open_segment a b) ⊆ closure (open_segment c d)" using lhs closure_mono by blast then have "closed_segment a b ⊆ closed_segment c d" by (simp add: ‹a ≠ b› ‹c ≠ d›) then show ?rhs by (force simp: ‹a ≠ b›) qed qed lemma subset_oc_segment: fixes a :: "'a::euclidean_space" shows "open_segment a b ⊆ closed_segment c d ⟷ a = b ∨ a ∈ closed_segment c d ∧ b ∈ closed_segment c d" apply (simp add: subset_open_segment [symmetric]) apply (rule iffI) apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment) apply (meson dual_order.trans segment_open_subset_closed) done lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment subsection‹Betweenness› definition%important "between = (λ(a,b) x. x ∈ closed_segment a b)" lemma betweenI: assumes "0 ≤ u" "u ≤ 1" "x = (1 - u) *⇩_{R}a + u *⇩_{R}b" shows "between (a, b) x" using assms unfolding between_def closed_segment_def by auto lemma betweenE: assumes "between (a, b) x" obtains u where "0 ≤ u" "u ≤ 1" "x = (1 - u) *⇩_{R}a + u *⇩_{R}b" using assms unfolding between_def closed_segment_def by auto lemma between_implies_scaled_diff: assumes "between (S, T) X" "between (S, T) Y" "S ≠ Y" obtains c where "(X - Y) = c *⇩_{R}(S - Y)" proof - from ‹between (S, T) X› obtain u⇩_{X}where X: "X = u⇩_{X}*⇩_{R}S + (1 - u⇩_{X}) *⇩_{R}T" by (metis add.commute betweenE eq_diff_eq) from ‹between (S, T) Y› obtain u⇩_{Y}where Y: "Y = u⇩_{Y}*⇩_{R}S + (1 - u⇩_{Y}) *⇩_{R}T" by (metis add.commute betweenE eq_diff_eq) have "X - Y = (u⇩_{X}- u⇩_{Y}) *⇩_{R}(S - T)" proof - from X Y have "X - Y = u⇩_{X}*⇩_{R}S - u⇩_{Y}*⇩_{R}S + ((1 - u⇩_{X}) *⇩_{R}T - (1 - u⇩_{Y}) *⇩_{R}T)" by simp also have "… = (u⇩_{X}- u⇩_{Y}) *⇩_{R}S - (u⇩_{X}- u⇩_{Y}) *⇩_{R}T" by (simp add: scaleR_left.diff) finally show ?thesis by (simp add: real_vector.scale_right_diff_distrib) qed moreover from Y have "S - Y = (1 - u⇩_{Y}) *⇩_{R}(S - T)" by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib) moreover note ‹S ≠ Y› ultimately have "(X - Y) = ((u⇩_{X}- u⇩_{Y}) / (1 - u⇩_{Y})) *⇩_{R}(S - Y)" by auto from this that show thesis by blast qed lemma between_mem_segment: "between (a,b) x ⟷ x ∈ closed_segment a b" unfolding between_def by auto lemma between: "between (a, b) (x::'a::euclidean_space) ⟷ dist a b = (dist a x) + (dist x b)" proof (cases "a = b") case True then show ?thesis by (auto simp add: between_def dist_commute) next case False then have Fal: "norm (a - b) ≠ 0" and Fal2: "norm (a - b) > 0" by auto have *: "⋀u. a - ((1 - u) *⇩_{R}a + u *⇩_{R}b) = u *⇩_{R}(a - b)" by (auto simp add: algebra_simps) have "norm (a - x) *⇩_{R}(x - b) = norm (x - b) *⇩_{R}(a - x)" if "x = (1 - u) *⇩_{R}a + u *⇩_{R}b" "0 ≤ u" "u ≤ 1" for u proof - have *: "a - x = u *⇩_{R}(a - b)" "x - b = (1 - u) *⇩_{R}(a - b)" unfolding that(1) by (auto simp add:algebra_simps) show "norm (a - x) *⇩_{R}(x - b) = norm (x - b) *⇩_{R}(a - x)" unfolding norm_minus_commute[of x a] * using ‹0 ≤ u› ‹u ≤ 1› by (auto simp add: field_simps) qed moreover have "∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ 0 ≤ u ∧ u ≤ 1" if "dist a b = dist a x + dist x b" proof - let ?β = "norm (a - x) / norm (a - b)" show "∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ 0 ≤ u ∧ u ≤ 1" proof (intro exI conjI) show "?β ≤ 1" using Fal2 unfolding that[unfolded dist_norm] norm_ge_zero by auto show "x = (1 - ?β) *⇩_{R}a + (?β) *⇩_{R}b" proof (subst euclidean_eq_iff; intro ballI) fix i :: 'a assume i: "i ∈ Basis" have "((1 - ?β) *⇩_{R}a + (?β) *⇩_{R}b) ∙ i = ((norm (a - b) - norm (a - x)) * (a ∙ i) + norm (a - x) * (b ∙ i)) / norm (a - b)" using Fal by (auto simp add: field_simps inner_simps) also have "… = x∙i" apply (rule divide_eq_imp[OF Fal]) unfolding that[unfolded dist_norm] using that[unfolded dist_triangle_eq] i apply (subst (asm) euclidean_eq_iff) apply (auto simp add: field_simps inner_simps) done finally show "x ∙ i = ((1 - ?β) *⇩_{R}a + (?β) *⇩_{R}b) ∙ i" by auto qed qed (use Fal2 in auto) qed ultimately show ?thesis by (force simp add: between_def closed_segment_def dist_triangle_eq) qed lemma between_midpoint: fixes a :: "'a::euclidean_space" shows "between (a,b) (midpoint a b)" (is ?t1) and "between (b,a) (midpoint a b)" (is ?t2) proof - have *: "⋀x y z. x = (1/2::real) *⇩_{R}z ⟹ y = (1/2) *⇩_{R}z ⟹ norm z = norm x + norm y" by auto show ?t1 ?t2 unfolding between midpoint_def dist_norm by (auto simp add: field_simps inner_simps euclidean_eq_iff[where 'a='a] intro!: *) qed lemma between_mem_convex_hull: "between (a,b) x ⟷ x ∈ convex hull {a,b}" unfolding between_mem_segment segment_convex_hull .. lemma between_triv_iff [simp]: "between (a,a) b ⟷ a=b" by (auto simp: between_def) lemma between_triv1 [simp]: "between (a,b) a" by (auto simp: between_def) lemma between_triv2 [simp]: "between (a,b) b" by (auto simp: between_def) lemma between_commute: "between (a,b) = between (b,a)" by (auto simp: between_def closed_segment_commute) lemma between_antisym: fixes a :: "'a :: euclidean_space" shows "⟦between (b,c) a; between (a,c) b⟧ ⟹ a = b" by (auto simp: between dist_commute) lemma between_trans: fixes a :: "'a :: euclidean_space" shows "⟦between (b,c) a; between (a,c) d⟧ ⟹ between (b,c) d" using dist_triangle2 [of b c d] dist_triangle3 [of b d a] by (auto simp: between dist_commute) lemma between_norm: fixes a :: "'a :: euclidean_space" shows "between (a,b) x ⟷ norm(x - a) *⇩_{R}(b - x) = norm(b - x) *⇩_{R}(x - a)" by (auto simp: between dist_triangle_eq norm_minus_commute algebra_simps) lemma between_swap: fixes A B X Y :: "'a::euclidean_space" assumes "between (A, B) X" assumes "between (A, B) Y" shows "between (X, B) Y ⟷ between (A, Y) X" using assms by (auto simp add: between) lemma between_translation [simp]: "between (a + y,a + z) (a + x) ⟷ between (y,z) x" by (auto simp: between_def) lemma between_trans_2: fixes a :: "'a :: euclidean_space" shows "⟦between (b,c) a; between (a,b) d⟧ ⟹ between (c,d) a" by (metis between_commute between_swap between_trans) lemma between_scaleR_lift [simp]: fixes v :: "'a::euclidean_space" shows "between (a *⇩_{R}v, b *⇩_{R}v) (c *⇩_{R}v) ⟷ v = 0 ∨ between (a, b) c" by (simp add: between dist_norm scaleR_left_diff_distrib [symmetric] distrib_right [symmetric]) lemma between_1: fixes x::real shows "between (a,b) x ⟷ (a ≤ x ∧ x ≤ b) ∨ (b ≤ x ∧ x ≤ a)" by (auto simp: between_mem_segment closed_segment_eq_real_ivl) subsection%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)" then have 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 "dist c ((1 / e) *⇩_{R}y - ((1 - e) / e) *⇩_{R}x) = ¦1/e¦ * norm (e *⇩_{R}c - y + (1 - e) *⇩_{R}x)" unfolding dist_norm unfolding norm_scaleR[symmetric] apply (rule arg_cong[where f=norm]) using ‹e > 0› by (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps) also have "… = ¦1/e¦ * norm (x - e *⇩_{R}(x - c) - y)" by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps) also have "… < d" using as[unfolded dist_norm] and ‹e > 0› by (auto simp add:pos_divide_less_eq[OF ‹e > 0›] mult.commute) finally show "y ∈ S" apply (subst *) apply (rule assms(1)[unfolded convex_alt,rule_format]) apply (rule d[unfolded subset_eq,rule_format]) unfolding mem_ball using assms(3-5) apply auto done qed (insert ‹e>0› ‹d>0›, 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 then show ?thesis using ‹e > 0› ‹d > 0› apply (rule_tac bexI[where x=x]) apply (auto) done next case False then have x: "x islimpt S" using assms(3)[unfolded closure_def] by auto show ?thesis proof (cases "e = 1") case True obtain y where "y ∈ S" "y ≠ x" "dist y x < 1" using x[unfolded islimpt_approachable,THEN spec[where x=1]] by auto then show ?thesis apply (rule_tac x=y in bexI) unfolding True using ‹d > 0› apply auto done next case False then have "0 < e * d / (1 - e)" and *: "1 - e > 0" using ‹e ≤ 1› ‹e > 0› ‹d > 0› by auto then obtain y where "y ∈ S" "y ≠ x" "dist y x < e * d / (1 - e)" using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto then show ?thesis apply (rule_tac x=y in bexI) unfolding dist_norm using pos_less_divide_eq[OF *] apply auto done qed qed then obtain y where "y ∈ S" and y: "norm (y - x) * (1 - e) < e * d" by auto define z where "z = c + ((1 - e) / e) *⇩_{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 "z ∈ interior S" apply (rule interior_mono[OF d,unfolded subset_eq,rule_format]) unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5) apply (auto simp add:field_simps norm_minus_commute) done then show ?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 (clarsimp simp: in_segment) 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) also have "... ∈ interior S" using mem_interior_closure_convex_shrink [OF assms] u by simp finally show "(1 - u) *⇩_{R}a + u *⇩_{R}b ∈ interior S" . qed lemma closure_open_Int_superset: assumes "open S" "S ⊆ closure T" shows "closure(S ∩ T) = closure S" proof - have "closure S ⊆ closure(S ∩ T)" by (metis assms closed_closure closure_minimal inf.orderE open_Int_closure_subset) then show ?thesis by (simp add: closure_mono dual_order.antisym) qed lemma convex_closure_interior: fixes S :: "'a::euclidean_space set" assumes "convex S" and int: "interior S ≠ {}" shows "closure(interior S) = closure S" proof - obtain a where a: "a ∈ interior S" using int by auto have "closure S ⊆ closure(interior S)" proof fix x assume x: "x ∈ closure S" show "x ∈ closure (interior S)" proof (cases "x=a") case True then show ?thesis using ‹a ∈ interior S› closure_subset by blast next case False show ?thesis proof (clarsimp simp add: closure_def islimpt_approachable) fix e::real assume xnotS: "x ∉ interior S" and "0 < e" show "∃x'∈interior S. x' ≠ x ∧ dist x' x < e" proof (intro bexI conjI) show "x - min (e/2 / norm (x - a)) 1 *⇩_{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" apply (clarsimp simp add: min_def a) apply (rule mem_interior_closure_convex_shrink [OF ‹convex S› a x]) using ‹0 < e› False apply (auto simp: divide_simps) done qed qed qed qed then show ?thesis by (simp add: closure_mono interior_subset subset_antisym) qed lemma closure_convex_Int_superset: fixes S :: "'a::euclidean_space set" assumes "convex S" "interior S ≠ {}" "interior S ⊆ closure T" shows "closure(S ∩ T) = closure S" proof - have "closure S ⊆ closure(interior S)" by (simp add: convex_closure_interior assms) also have "... ⊆ closure (S ∩ T)" using interior_subset [of S] assms by (metis (no_types, lifting) Int_assoc Int_lower2 closure_mono closure_open_Int_superset inf.orderE open_interior) finally show ?thesis by (simp add: closure_mono dual_order.antisym) qed subsection%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 (simp add: convex_hull_finite set_eq_iff assms, safe) fix x and u :: "'a ⇒ real" assume "0 ≤ u 0" "∀x∈S. 0 ≤ u x" "u 0 + sum u S = 1" then show "∃v. (∀x∈S. 0 ≤ v x) ∧ sum v S ≤ 1 ∧ (∑x∈S. v x *⇩_{R}x) = (∑x∈S. u x *⇩_{R}x)" by force next fix x and u :: "'a ⇒ real" assume "∀x∈S. 0 ≤ u x" "sum u S ≤ 1" then show "∃v. 0 ≤ v 0 ∧ (∀x∈S. 0 ≤ v x) ∧ v 0 + sum v S = 1 ∧ (∑x∈S. v x *⇩_{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) 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+ then have **: "sum u ?D = sum ((∙) ?x) ?D" using assms by (auto intro!: sum.cong) show "0 ≤ ?x ∙ i" if "i ∈ Basis" for i using as(1) ind notind that by fastforce show "sum ((∙) ?x) ?D ≤ 1" using "**" as(2) by linarith show "?x ∙ i = 0" if "i ∈ Basis" "i ∉ d" for i using notind that by blast next fix x assume "∀i∈Basis. 0 ≤ x ∙ i" "sum ((∙) x) ?D ≤ 1" "(∀i∈Basis. i ∉ d ⟶ x ∙ i = 0)" with d show "∃u. (∀x∈?D. 0 ≤ u x) ∧ sum u ?D ≤ 1 ∧ (∑x∈?D. u x *⇩_{R}x) = x" unfolding substdbasis_expansion_unique[OF assms] by (rule_tac x="inner x" in exI) auto qed qed lemma std_simplex: "convex hull (insert 0 Basis) = {x::'a::euclidean_space. (∀i∈Basis. 0 ≤ x∙i) ∧ sum (λi. x∙i) Basis ≤ 1}" using substd_simplex[of Basis] by auto lemma interior_std_simplex: "interior (convex hull (insert 0 Basis)) = {x::'a::euclidean_space. (∀i∈Basis. 0 < x∙i) ∧ sum (λi. x∙i) Basis < 1}" unfolding set_eq_iff mem_interior std_simplex proof (intro allI iffI CollectI; clarify) fix x :: 'a fix e assume "e > 0" and as: "ball x e ⊆ {x. (∀i∈Basis. 0 ≤ x ∙ i) ∧ sum ((∙) x) Basis ≤ 1}" show "(∀i∈Basis. 0 < x ∙ i) ∧ sum ((∙) x) Basis < 1" proof safe fix i :: 'a assume i: "i ∈ Basis" then show "0 < x ∙ i" using as[THEN subsetD[where c="x - (e / 2) *⇩_{R}i"]] and ‹e > 0› by (force simp add: inner_simps) next have **: "dist x (x + (e / 2) *⇩_{R}(SOME i. i∈Basis)) < e" using ‹e > 0› unfolding dist_norm by (auto intro!: mult_strict_left_mono simp: SOME_Basis) have "⋀i. i ∈ Basis ⟹ (x + (e / 2) *⇩_{R}(SOME i. i∈Basis)) ∙ i = x∙i + (if i = (SOME i. i∈Basis) then e/2 else 0)" by (auto simp: SOME_Basis inner_Basis inner_simps) then have *: "sum ((∙) (x + (e / 2) *⇩_{R}(SOME i. i∈Basis))) Basis = sum (λi. x∙i + (if (SOME i. i∈Basis) = i then e/2 else 0)) Basis" by (auto simp: intro!: sum.cong) have "sum ((∙) x) Basis < sum ((∙) (x + (e / 2) *⇩_{R}(SOME i. i∈Basis))) Basis" using ‹e > 0› DIM_positive by (auto simp: SOME_Basis sum.distrib *) also have "… ≤ 1" using ** as by force finally show "sum ((∙) x) Basis < 1" by auto qed next fix x :: 'a assume as: "∀i∈Basis. 0 < x ∙ i" "sum ((∙) x) Basis < 1" obtain a :: 'b where "a ∈ UNIV" using UNIV_witness .. let ?d = "(1 - sum ((∙) x) Basis) / real (DIM('a))" show "∃e>0. ball x e ⊆ {x. (∀i∈Basis. 0 ≤ x ∙ i) ∧ sum ((∙) x) Basis ≤ 1}" proof (rule_tac x="min (Min (((∙) x) ` Basis)) D" for D in exI, intro conjI subsetI CollectI) fix y assume y: "y ∈ ball x (min (Min ((∙) x ` Basis)) ?d)" have "sum ((∙) y) Basis ≤ sum (λi. x∙i + ?d) Basis" proof (rule sum_mono) fix i :: 'a assume i: "i ∈ Basis" have "¦y∙i - x∙i¦ ≤ norm (y - x)" by (metis Basis_le_norm i inner_commute inner_diff_right) also have "... < ?d" using y by (simp add: dist_norm norm_minus_commute) finally have "¦y∙i - x∙i¦ < ?d" . then show "y ∙ i ≤ x ∙ i + ?d" by auto qed also have "… ≤ 1" unfolding sum.distrib sum_constant by (auto simp add: Suc_le_eq) finally show "sum ((∙) y) Basis ≤ 1" . show "(∀i∈Basis. 0 ≤ y ∙ i)" proof safe fix i :: 'a assume i: "i ∈ Basis" have "norm (x - y) < MINIMUM Basis ((∙) x)" using y by (auto simp: dist_norm less_eq_real_def) also have "... ≤ x∙i" using i by auto finally have "norm (x - y) < x∙i" . then show "0 ≤ y∙i" using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format, OF i] by (auto simp: inner_simps) qed next have "Min (((∙) x) ` Basis) > 0" using as by simp moreover have "?d > 0" using as by (auto simp: Suc_le_eq) ultimately show "0 < min (Min ((∙) x ` Basis)) ((1 - sum ((∙) x) Basis) / real DIM('a))" by linarith qed qed lemma interior_std_simplex_nonempty: obtains a :: "'a::euclidean_space" where "a ∈ interior(convex hull (insert 0 Basis))" proof - let ?D = "Basis :: 'a set" let ?a = "sum (λb::'a. inverse (2 * real DIM('a)) *⇩_{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 apply (rule that[of ?a]) 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 DIM_positive) next have "sum ((∙) ?a) ?D = sum (λi. inverse (2 * real DIM('a))) ?D" apply (rule sum.cong) apply rule apply auto done also have "… < 1" unfolding sum_constant divide_inverse[symmetric] by (auto simp add: field_simps) finally show "sum ((∙) ?a) ?D < 1" by auto qed qed 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 "rel_interior (convex hull (insert 0 ?p)) = ?s") proof - have "finite D" using D finite_Basis finite_subset by blast show ?thesis proof (cases "D = {}") case True then show ?thesis using rel_interior_sing using euclidean_eq_iff[of _ 0] by auto next case False have h0: "affine hull (convex hull (insert 0 ?p)) = {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 ?p))" then obtain e where "e > 0" and "ball x e ∩ {xa. (∀i∈Basis. i ∉ D ⟶ xa∙i = 0)} ⊆ convex hull (insert 0 ?p)" using mem_rel_interior_ball[of x "convex hull (insert 0 ?p)"] h0 by auto then have as [rule_format]: "⋀y. dist x y < e ∧ (∀i∈Basis. i ∉ D ⟶ y∙i = 0) ⟶ (∀i∈D. 0 ≤ y ∙ i) ∧ sum ((∙) y) D ≤ 1" unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto have x0: "(∀i∈Basis. i ∉ D ⟶ x∙i = 0)" using x rel_interior_subset substd_simplex[OF assms] by auto have "(∀i∈D. 0 < x ∙ i) ∧ sum ((∙) x) D < 1 ∧ (∀i∈Basis. i ∉ D ⟶ x∙i = 0)" proof (intro conjI ballI) fix i :: 'a assume "i ∈ D" then have "∀j∈D. 0 ≤ (x - (e / 2) *⇩_{R}i) ∙ j" apply - apply (rule as[THEN conjunct1]) using D ‹e > 0› x0 apply (auto simp: dist_norm inner_simps inner_Basis) done then show "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 then have **: "dist x (x + (e / 2) *⇩_{R}a) < e" using ‹e > 0› norm_Basis[of a] D unfolding dist_norm by auto 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) then have *: "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 then have 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) also have "… ≤ 1" using ** h1 as[rule_format, of "x + (e / 2) *⇩_{R}a"] by auto finally show "sum ((∙) x) D < 1" "⋀i. i∈Basis ⟹ i ∉ D ⟶ x∙i = 0" using x0 by auto qed } moreover { fix x :: "'a::euclidean_space" assume as: "x ∈ ?s" have "∀i. 0 < x∙i ∨ 0 = x∙i ⟶ 0 ≤ x∙i" by auto moreover have "∀i. i ∈ D ∨ i ∉ D" by auto ultimately have "∀i. (∀i∈D. 0 < x∙i) ∧ (∀i. i ∉ D ⟶ x∙i = 0) ⟶ 0 ≤ x∙i" by metis then have h2: "x ∈ convex hull (insert 0 ?p)" using as assms unfolding substd_simplex[OF assms] by fastforce obtain a where a: "a ∈ D" using ‹D ≠ {}› by auto let ?d = "(1 - sum ((∙) x) D) / real (card D)" 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 add: Min_gr_iff) moreover have "?d > 0" using as using ‹0 < card D› by auto ultimately have h3: "min (Min (((∙) x) ` D)) ?d > 0" by auto have "x ∈ rel_interior (convex hull (insert 0 ?p))" unfolding rel_interior_ball mem_Collect_eq h0 apply (rule,rule h2) unfolding substd_simplex[OF assms] apply (rule_tac x="min (Min (((∙) x) ` D)) ?d" in exI) apply (rule, rule h3) apply safe unfolding mem_ball proof - fix y :: 'a assume y: "dist x y < min (Min ((∙) x ` D)) ?d" assume y2: "∀i∈Basis. i ∉ D ⟶ y∙i = 0" have "sum ((∙) y) D ≤ sum (λi. x∙i + ?d) D" proof (rule sum_mono) fix i assume "i ∈ D" with D have i: "i ∈ Basis" by auto have "¦y∙i - x∙i¦ ≤ norm (y - x)" by (metis i inner_commute inner_diff_right norm_bound_Basis_le order_refl) also have "... < ?d" by (metis dist_norm min_less_iff_conj norm_minus_commute y) finally have "¦y∙i - x∙i¦ < ?d" . then show "y ∙ i ≤ x ∙ i + ?d" by auto qed also have "… ≤ 1" unfolding sum.distrib sum_constant using ‹0 < card D› by auto finally show "sum ((∙) y) D ≤ 1" . fix i :: 'a assume i: "i ∈ Basis" then show "0 ≤ y∙i" proof (cases "i∈D") case True have "norm (x - y) < x∙i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1] using Min_gr_iff[of "(∙) x ` D" "norm (x - y)"] ‹0 < card D› ‹i ∈ D› by (simp add: card_gt_0_iff) then show "0 ≤ y∙i" using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format] by (auto simp: inner_simps) qed (insert y2, auto) qed } ultimately have "⋀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 then show ?thesis by (rule set_eqI) qed qed lemma rel_interior_substd_simplex_nonempty: assumes "D ≠ {}" and "D ⊆ Basis" obtains a :: "'a::euclidean_space" where "a ∈ rel_interior (convex hull (insert 0 D))" proof - let ?D = D let ?a = "sum (λb::'a::euclidean_space. inverse (2 * real (card D)) *⇩_{R}b) ?D" have "finite D" apply (rule finite_subset) using assms(2) apply auto done then have d1: "0 < real (card D)" using ‹D ≠ {}› by auto { fix i assume "i ∈ D" have "?a ∙ i = inverse (2 * real (card D))" apply (rule trans[of _ "sum (λj. if i = j then inverse (2 * real (card D)) else 0) ?D"]) unfolding inner_sum_left apply (rule sum.cong) using ‹i ∈ D› ‹finite D› sum.delta'[of D i "(λk. inverse (2 * real (card D)))"] d1 assms(2) by (auto simp: inner_Basis set_rev_mp[OF _ assms(2)]) } note ** = this show ?thesis apply (rule that[of ?a]) unfolding rel_interior_substd_simplex[OF assms(2)] mem_Collect_eq proof safe fix i assume "i ∈ D" have "0 < inverse (2 * real (card D))" using d1 by auto also have "… = ?a ∙ i" using **[of i] ‹i ∈ D› by auto finally show "0 < ?a ∙ i" by auto next have "sum ((∙) ?a) ?D = sum (λi. inverse (2 * real (card D))) ?D" by (rule sum.cong) (rule refl, rule **) also have "… < 1" unfolding sum_constant divide_real_def[symmetric] by (auto simp add: field_simps) finally show "sum ((∙) ?a) ?D < 1" by auto next fix i assume "i ∈ Basis" and "i ∉ D" have "?a ∈ span D" proof (rule span_sum[of D "(λb. b /⇩_{R}(2 * real (card D)))" D]) { fix x :: "'a::euclidean_space" assume "x ∈ D" then have "x ∈ span D" using span_base[of _ "D"] by auto then have "x /⇩_{R}(2 * real (card D)) ∈ span D" using span_mul[of x "D" "(inverse (real (card D)) / 2)"] by auto } then show "⋀x. x∈D ⟹ x /⇩_{R}(2 * real (card D)) ∈ span D" by auto qed then show "?a ∙ i = 0 " using ‹i ∉ D› unfolding span_substd_basis[OF assms(2)] using ‹i ∈ Basis› by auto qed qed subsection%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 then show ?thesis using rel_interior_sing by auto next case False obtain B where B: "independent B ∧ B ≤ S ∧ S ≤ span B ∧ card B = dim S" using basis_exists[of S] by metis then have "B ≠ {}" using B assms ‹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 then have "span (insert 0 B) ≤ span B" using span_span[of B] span_mono[of "insert 0 B" "span B"] by blast then have "convex hull insert 0 B ≤ span B" using convex_hull_subset_span[of "insert 0 B"] by auto then have "span (convex hull insert 0 B) ≤ span B" using span_span[of B] span_mono[of "convex hull insert 0 B" "span B"] by blast then have *: "span (convex hull insert 0 B) = span B" using span_mono[of B "convex hull insert 0 B"] hull_subset[of "insert 0 B"] by auto then have "span (convex hull insert 0 B) = span S" using B span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto moreover have "0 ∈ affine hull (convex hull insert 0 B)" using hull_subset[of "convex hull insert 0 B"] hull_subset[of "insert 0 B"] by auto ultimately have **: "affine hull (convex hull insert 0 B) = affine hull S" using affine_hull_span_0[of "convex hull insert 0 B"] affine_hull_span_0[of "S"] assms hull_subset[of S] by auto obtain d and f :: "'n ⇒ 'n" where fd: "card d = card B" "linear f" "f ` B = d" "f ` span B = {x. ∀i∈Basis. i ∉ d ⟶ x ∙ i = (0::real)} ∧ inj_on f (span B)" and d: "d ⊆ Basis" using basis_to_substdbasis_subspace_isomorphism[of B,OF _ ] B by auto then have "bounded_linear f" using linear_conv_bounded_linear by auto have "d ≠ {}" using fd B ‹B ≠ {}› by auto have "insert 0 d = f ` (insert 0 B)" using fd linear_0 by auto then have "(convex hull (insert 0 d)) = f ` (convex hull (insert 0 B))" using convex_hull_linear_image[of f "(insert 0 d)"] convex_hull_linear_image[of f "(insert 0 B)"] ‹linear f› by auto moreover have "rel_interior (f ` (convex hull insert 0 B)) = f ` rel_interior (convex hull insert 0 B)" apply (rule rel_interior_injective_on_span_linear_image[of f "(convex hull insert 0 B)"]) using ‹bounded_linear f› fd * apply auto done ultimately have "rel_interior (convex hull insert 0 B) ≠ {}" using rel_interior_substd_simplex_nonempty[OF ‹d ≠ {}› d] apply auto apply blast done moreover have "convex hull (insert 0 B) ⊆ S" using B assms hull_mono[of "insert 0 B" "S" "convex"] convex_hull_eq by auto ultimately show ?thesis using subset_rel_interior[of "convex hull insert 0 B" S] ** by auto qed lemma rel_interior_eq_empty: fixes S :: "'n::euclidean_space set" assumes "convex S" shows "rel_interior S = {} ⟷ S = {}" proof - { assume "S ≠ {}" then obtain a where "a ∈ S" by auto then have "0 ∈ (+) (-a) ` S" using assms exI[of "(λx. x ∈ S ∧ - a + x = 0)" a] by auto then have "rel_interior ((+) (-a) ` S) ≠ {}" using rel_interior_convex_nonempty_aux[of "(+) (-a) ` S"] convex_translation[of S "-a"] assms by auto then have "rel_interior S ≠ {}" using rel_interior_translation by auto } then show ?thesis using rel_interior_empty by auto qed lemma interior_simplex_nonempty: fixes S :: "'N :: euclidean_space set" assumes "independent S" "finite S" "card S = DIM('N)" obtains a where "a ∈ interior (convex hull (insert 0 S))" proof - have "affine hull (insert 0 S) = UNIV" by (simp add: hull_inc affine_hull_span_0 dim_eq_full[symmetric] assms(1) assms(3) dim_eq_card_independent) moreover have "rel_interior (convex hull insert 0 S) ≠ {}" using rel_interior_eq_empty [of "convex hull (insert 0 S)"] by auto ultimately have "interior (convex hull insert 0 S) ≠ {}" by (simp add: rel_interior_interior) with that show ?thesis by auto qed lemma convex_rel_interior: fixes S :: "'n::euclidean_space set" assumes "convex S" shows "convex (rel_interior S)" proof - { fix x y and u :: real assume assm: "x ∈ rel_interior S" "y ∈ rel_interior S" "0 ≤ u" "u ≤ 1" then have "x ∈ S" using rel_interior_subset by auto have "x - u *⇩_{R}(x-y) ∈ rel_interior S" proof (cases "0 = u") case False then have "0 < u" using assm by auto then show ?thesis using assm rel_interior_convex_shrink[of S y x u] assms ‹x ∈ S› by auto next case True then show ?thesis using assm by auto qed then have "(1 - u) *⇩_{R}x + u *⇩_{R}y ∈ rel_interior S" by (simp add: algebra_simps) } then show ?thesis unfolding convex_alt by auto qed lemma convex_closure_rel_interior: fixes S :: "'n::euclidean_space set" assumes "convex S" shows "closure (rel_interior S) = closure S" proof - have h1: "closure (rel_interior S) ≤ closure S" using closure_mono[of "rel_interior S" S] rel_interior_subset[of S] by auto show ?thesis proof (cases "S = {}") case False then obtain a where a: "a ∈ rel_interior S" using rel_interior_eq_empty assms by auto { fix x assume x: "x ∈ closure S" { assume "x = a" then have "x ∈ closure (rel_interior S)" using a unfolding closure_def by auto } moreover { assume "x ≠ a" { fix e :: real assume "e > 0" define e1 where "e1 = min 1 (e/norm (x - a))" then have e1: "e1 > 0" "e1 ≤ 1" "e1 * norm (x - a) ≤ e" using ‹x ≠ a› ‹e > 0› le_divide_eq[of e1 e "norm (x - a)"] by simp_all then have *: "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" apply (rule_tac x="x - e1 *⇩_{R}(x - a)" in exI) using * e1 dist_norm[of "x - e1 *⇩_{R}(x - a)" x] ‹x ≠ a› apply simp done } then have "x islimpt rel_interior S" unfolding islimpt_approachable_le by auto then have "x ∈ closure(rel_interior S)" unfolding closure_def by auto } ultimately have "x ∈ closure(rel_interior S)" by auto } then show ?thesis using h1 by auto next case True then have "rel_interior S = {}" using rel_interior_empty by auto then have "closure (rel_interior S) = {}" using closure_empty by auto with True show ?thesis by auto qed qed lemma rel_interior_same_affine_hull: fixes S :: "'n::euclidean_space set" assumes "convex S" shows "affine hull (rel_interior S) = affine hull S" by (metis assms closure_same_affine_hull convex_closure_rel_interior) lemma rel_interior_aff_dim: fixes S :: "'n::euclidean_space set" assumes "convex S" shows "aff_dim (rel_interior S) = aff_dim S" by (metis aff_dim_affine_hull2 assms rel_interior_same_affine_hull) lemma rel_interior_rel_interior: fixes S :: "'n::euclidean_space set" assumes "convex S" shows "rel_interior (rel_interior S) = rel_interior S" proof - have "openin (subtopology euclidean (affine hull (rel_interior S))) (rel_interior S)" using openin_rel_interior[of S] rel_interior_same_affine_hull[of S] assms by auto then show ?thesis using rel_interior_def by auto qed lemma rel_interior_rel_open: fixes S :: "'n::euclidean_space set" assumes "convex S" shows "rel_open (rel_interior S)" unfolding rel_open_def using rel_interior_rel_interior assms by auto lemma convex_rel_interior_closure_aux: fixes x y z :: "'n::euclidean_space" assumes "0 < a" "0 < b" "(a + b) *⇩_{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) also have "… = (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 also have "… = y - e *⇩_{R}(y-x)" using e_def apply (simp add: algebra_simps) using scaleR_left_distrib[of "a/(a+b)" "b/(a+b)" y] assms add_divide_distrib[of a b "a+b"] apply auto done finally have "z = y - e *⇩_{R}(y-x)" by auto moreover have "e > 0" using e_def assms by auto moreover have "e ≤ 1" using e_def assms by auto ultimately show ?thesis using that[of e] by auto qed lemma convex_rel_interior_closure: fixes S :: "'n::euclidean_space set" assumes "convex S" shows "rel_interior (closure S) = rel_interior S" proof (cases "S = {}") case True then show ?thesis using assms rel_interior_eq_empty by auto next case False have "rel_interior (closure S) ⊇ rel_interior S" using subset_rel_interior[of S "closure S"] closure_same_affine_hull closure_subset by auto moreover { fix z assume z: "z ∈ rel_interior (closure S)" obtain x where x: "x ∈ rel_interior S" using ‹S ≠ {}› assms rel_interior_eq_empty by auto have "z ∈ rel_interior S" proof (cases "x = z") case True then show ?thesis using x by auto next case False obtain e where e: "e > 0" "cball z e ∩ affine hull closure S ≤ closure S" using z rel_interior_cball[of "closure S"] by auto hence *: "0 < e/norm(z-x)" using e False by auto define y where "y = z + (e/norm(z-x)) *⇩_{R}(z-x)" have yball: "y ∈ cball z e" using mem_cball y_def dist_norm[of z y] e by auto have "x ∈ affine hull closure S" using x rel_interior_subset_closure hull_inc[of x "closure S"] by blast moreover have "z ∈ affine hull closure S" using z rel_interior_subset hull_subset[of "closure S"] by blast ultimately have "y ∈ affine hull closure S" using y_def affine_affine_hull[of "closure S"] mem_affine_3_minus [of "affine hull closure S" z z x "e/norm(z-x)"] by auto then have "y ∈ closure S" using e yball by auto have "(1 + (e/norm(z-x))) *⇩_{R}z = (e/norm(z-x)) *⇩_{R}x + y" using y_def by (simp add: algebra_simps) then obtain 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) then show ?thesis using rel_interior_closure_convex_shrink assms x ‹y ∈ closure S› by auto qed } ultimately show ?thesis by auto qed lemma convex_interior_closure: fixes S :: "'n::euclidean_space set" assumes "convex S" shows "interior (closure S) = interior S" using closure_aff_dim[of S] interior_rel_interior_gen[of S] interior_rel_interior_gen[of "closure S"] convex_rel_interior_closure[of S] assms by auto lemma closure_eq_rel_interior_eq: fixes S1 S2 :: "'n::euclidean_space set" assumes "convex S1" and "convex S2" shows "closure S1 = closure S2 ⟷ rel_interior S1 = rel_interior S2" by (metis convex_rel_interior_closure convex_closure_rel_interior assms) lemma closure_eq_between: fixes S1 S2 :: "'n::euclidean_space set" assumes "convex S1" and "convex S2" shows "closure S1 = closure S2 ⟷ rel_interior S1 ≤ S2 ∧ S2 ⊆ closure S1" (is "?A ⟷ ?B") proof assume ?A then show ?B by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset) next assume ?B then have "closure S1 ⊆ closure S2" by (metis assms(1) convex_closure_rel_interior closure_mono) moreover from ‹?B› have "closure S1 ⊇ closure S2" by (metis closed_closure closure_minimal) ultimately show ?A .. qed lemma open_inter_closure_rel_interior: fixes S A :: "'n::euclidean_space set" assumes "convex S" and "open A" shows "A ∩ closure S = {} ⟷ A ∩ rel_interior S = {}" by (metis assms convex_closure_rel_interior open_Int_closure_eq_empty) lemma rel_interior_open_segment: fixes a :: "'a :: euclidean_space" shows "rel_interior(open_segment a b) = open_segment a b" proof (cases "a = b") case True then show ?thesis by auto next case False then show ?thesis apply (simp add: rel_interior_eq openin_open) apply (rule_tac x="ball (inverse 2 *⇩_{R}(a + b)) (norm(b - a) / 2)" in exI) apply (simp add: open_segment_as_ball) done qed lemma rel_interior_closed_segment: fixes a :: "'a :: euclidean_space" shows "rel_interior(closed_segment a b) = (if a = b then {a} else open_segment a b)" proof (cases "a = b") case True then show ?thesis by auto next case False then show ?thesis by simp (metis closure_open_segment convex_open_segment convex_rel_interior_closure rel_interior_open_segment) qed lemmas rel_interior_segment = rel_interior_closed_segment rel_interior_open_segment lemma starlike_convex_tweak_boundary_points: fixes S :: "'a::euclidean_space set" assumes "convex S" "S ≠ {}" and ST: "rel_interior S ⊆ T" and TS: "T ⊆ closure S" shows "starlike T" proof - have "rel_interior S ≠ {}" by (simp add: assms rel_interior_eq_empty) then obtain a where a: "a ∈ rel_interior S" by blast with ST have "a ∈ T" by blast have *: "⋀x. x ∈ T ⟹ open_segment a x ⊆ rel_interior S" apply (rule rel_interior_closure_convex_segment [OF ‹convex S› a]) using assms by blast show ?thesis unfolding starlike_def apply (rule bexI [OF _ ‹a ∈ T›]) apply (simp add: closed_segment_eq_open) apply (intro conjI ballI a ‹a ∈ T› rel_interior_closure_convex_segment [OF ‹convex S› a]) apply (simp add: order_trans [OF * ST]) done qed subsection‹The relative frontier of a set› definition%important "rel_frontier S = closure S - rel_interior S" lemma rel_frontier_empty [simp]: "rel_frontier {} = {}" by (simp add: rel_frontier_def) lemma rel_frontier_eq_empty: fixes S :: "'n::euclidean_space set" shows "rel_frontier S = {} ⟷ affine S" unfolding rel_frontier_def using rel_interior_subset_closure by (auto simp add: rel_interior_eq_closure [symmetric]) lemma rel_frontier_sing [simp]: fixes a :: "'n::euclidean_space" shows "rel_frontier {a} = {}" by (simp add: rel_frontier_def) lemma rel_frontier_affine_hull: fixes S :: "'a::euclidean_space set" shows "rel_frontier S ⊆ affine hull S" using closure_affine_hull rel_frontier_def by fastforce lemma rel_frontier_cball [simp]: fixes a :: "'n::euclidean_space" shows "rel_frontier(cball a r) = (if r = 0 then {} else sphere a r)" proof (cases rule: linorder_cases [of r 0]) case less then show ?thesis by (force simp: sphere_def) next case equal then show ?thesis by simp next case greater then show ?thesis apply simp by (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 closed_affine_hull [iff]: fixes S :: "'n::euclidean_space set" shows "closed (affine hull S)" by (metis affine_affine_hull affine_closed) 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 (subtopology euclidean (affine hull S)) (closure S - rel_interior S)" by (simp add: closed_subset closedin_diff closure_affine_hull openin_rel_interior) show ?thesis apply (rule closedin_closed_trans[of "affine hull S" "rel_frontier S"]) unfolding rel_frontier_def using * closed_affine_hull apply auto done 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 then have *: "affine hull S1 ⊆ affine hull S2" using hull_mono[of "S1" "closure S2"] closure_same_affine_hull[of S2] by blast then have "aff_dim S1 ≤ aff_dim S2" using * aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2] aff_dim_subset[of "affine hull S1" "affine hull S2"] by auto moreover { assume eq: "aff_dim S1 = aff_dim S2" then have "S1 ≠ {}" using aff_dim_empty[of S1] aff_dim_empty[of S2] ‹S2 ≠ {}› by auto have **: "affine hull S1 = affine hull S2" apply (rule affine_dim_equal) using * affine_affine_hull apply auto using ‹S1 ≠ {}› hull_subset[of S1] apply auto using eq aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2] apply auto done 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 then have "a ∈ T ∩ closure S2" using a assms unfolding rel_frontier_def by auto then obtain b where b: "b ∈ T ∩ rel_interior S2" using open_inter_closure_rel_interior[of S2 T] assms T by auto then have "b ∈ affine hull S1" using rel_interior_subset hull_subset[of S2] ** by auto then have "b ∈ S1" using T b by auto then have False using b assms unfolding rel_frontier_def by auto } ultimately show ?thesis using less_le by auto qed lemma convex_rel_interior_if: fixes S :: "'n::euclidean_space set" assumes "convex S" and "z ∈ rel_interior S" shows "∀x∈affine hull S. ∃m. m > 1 ∧ (∀e. e > 1 ∧ e ≤ m ⟶ (1 - e) *⇩_{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 then have *: "(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) also have "… = (e - 1) * norm (x-z)" using norm_scaleR e by auto also have "… ≤ (m - 1) * norm (x - z)" using e mult_right_mono[of _ _ "norm(x-z)"] by auto also have "… = (e1 / norm (x - z)) * norm (x - z)" using m_def by auto also have "… = e1" using ‹x ≠ z› e1 by simp finally have **: "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) then have "(1 - e) *⇩_{R}x+ e *⇩_{R}z ∈ S" using e * e1 by auto } then have "∃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" then have "m > 1" using e1 by auto { fix e assume e: "e > 1 ∧ e ≤ m" then have "(1 - e) *⇩_{R}x + e *⇩_{R}z ∈ S" using e1 x ‹x = z› by (auto simp add: algebra_simps) then have "(1 - e) *⇩_{R}x + e *⇩_{R}z ∈ S" using e by auto } then have "∃m. m > 1 ∧ (∀e. e > 1 ∧ e ≤ m ⟶ (1 - e) *⇩_{R}x + e *⇩_{R}z ∈ S)" using ‹m > 1› by auto } ultimately have "∃m. m > 1 ∧ (∀e. e > 1 ∧ e ≤ m ⟶ (1 - e) *⇩_{R}x + e *⇩_{R}z ∈ S )" by blast } then show ?thesis by auto qed lemma convex_rel_interior_if2: fixes S :: "'n::euclidean_space set" assumes "convex S" assumes "z ∈ rel_interior S" shows "∀x∈affine hull S. ∃e. e > 1 ∧ (1 - e)*⇩_{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 then have "x ∈ S" using rel_interior_subset by auto then obtain 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" then have "y ∈ S" using e by auto define e1 where "e1 = 1/e" then have "0 < e1 ∧ e1 < 1" using e by auto then have "z =y - (1 - e1) *⇩_{R}(y - x)" using e1_def y_def by (auto simp add: algebra_simps) then show ?thesis using rel_interior_convex_shrink[of S x y "1-e1"] ‹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" then have 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)" then have x1: "x1 ∈ affine hull S" using e1 hull_subset[of S] by auto define x2 where [abs_def]: "x2 = z + e2 *⇩_{R}(z - x)" then have x2: "x2 ∈ affine hull S" using e2 hull_subset[of S] by auto have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using add_divide_distrib[of e1 e2 "e1+e2"] e1 e2 by simp then have "z = (e2/(e1+e2)) *⇩_{R}x1 + (e1/(e1+e2)) *⇩_{R}x2" using x1_def x2_def apply (auto simp add: algebra_simps) using scaleR_left_distrib[of "e1/(e1+e2)" "e2/(e1+e2)" z] apply auto done then have z: "z ∈ affine hull S" using mem_affine[of "affine hull S" x1 x2 "e2/(e1+e2)" "e1/(e1+e2)"] x1 x2 affine_affine_hull[of S] * by auto have "x1 - x2 = (e1 + e2) *⇩_{R}(x - z)" using x1_def x2_def by (auto simp add: algebra_simps) then have "x = z+(1/(e1+e2)) *⇩_{R}(x1-x2)" using e1 e2 by simp then have "x ∈ affine hull S" using mem_affine_3_minus[of "affine hull S" z x1 x2 "1/(e1+e2)"] x1 x2 z affine_affine_hull[of S] by auto } then have "affine hull S = UNIV" by auto then have "aff_dim S = int DIM('n)" using aff_dim_affine_hull[of S] by (simp add: aff_dim_UNIV) then have False using False by auto } ultimately show ?thesis by auto next case True then have "S ≠ {}" using aff_dim_empty[of S] by auto have *: "affine hull S = UNIV" using True affine_hull_UNIV by auto { assume "z ∈ interior S" then have "z ∈ rel_interior S" using True interior_rel_interior_gen[of S] by auto then have **: "∀x. ∃e. e > 1 ∧ (1 - e) *⇩_{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" then have "(1 - e1) *⇩_{R}(z - x) + e1 *⇩_{R}z = z + e *⇩_{R}x" by (simp add: algebra_simps) then have "e > 0" "z + e *⇩_{R}x ∈ S" using e1 e_def by auto then have "∃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" then have "z + e1 *⇩_{R}(z - x) = (1 - e) *⇩_{R}x + e *⇩_{R}z" by (simp add: algebra_simps) then have "e > 1" "(1 - e)*⇩_{R}x + e *⇩_{R}z ∈ S" using e1 e_def by auto then have "∃e. e > 1 ∧ (1 - e) *⇩_{R}x + e *⇩_{R}z ∈ S" by auto } then have "z ∈ rel_interior S" using convex_rel_interior_iff2[of S z] assms ‹S ≠ {}› by auto then have "z ∈ interior S" using True interior_rel_interior_gen[of S] by auto } ultimately show ?thesis by auto qed subsubsection%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}" then have y: "∀S ∈ I. y ∈ rel_interior S" by auto { fix S assume "S ∈ I" then have "y ∈ S" using rel_interior_subset y by auto } then have "y ∈ ⋂I" by auto } then show ?thesis by auto qed lemma closure_Int: "closure (⋂I) ≤ ⋂{closure S |S. S ∈ I}" proof - { fix y assume "y ∈ ⋂I" then have y: "∀S ∈ I. y ∈ S" by auto { fix S assume "S ∈ I" then have "y ∈ closure S" using closure_subset y by auto } then have "y ∈ ⋂{closure S |S. S ∈ I}" by auto } then have "⋂I ⊆ ⋂{closure S |S. S ∈ I}" by auto moreover have "closed (⋂{closure S |S. S ∈ I})" unfolding closed_Inter closed_closure by auto ultimately show ?thesis using closure_hull[of "⋂I"] hull_minimal[of "⋂I" "⋂{closure S |S. S ∈ I}" "closed"] by auto qed lemma convex_closure_rel_interior_inter: assumes "∀S∈I. convex (S :: 'n::euclidean_space set)" and "⋂{rel_interior S |S. S ∈ I} ≠ {}" shows "⋂{closure S |S. S ∈ I} ≤ closure (⋂{rel_interior S |S. S ∈ I})" proof - obtain x where x: "∀S∈I. x ∈ rel_interior S" using assms by auto { fix y assume "y ∈ ⋂{closure S |S. S ∈ I}" then have y: "∀S ∈ I. y ∈ closure S" by auto { assume "y = x" then have "y ∈ closure (⋂{rel_interior S |S. S ∈ I})" using x closure_subset[of "⋂{rel_interior S |S. S ∈ I}"] by auto } moreover { assume "y ≠ x" { fix e :: real assume e: "e > 0" define e1 where "e1 = min 1 (e/norm (y - x))" then have e1: "e1 > 0" "e1 ≤ 1" "e1 * norm (y - x) ≤ e" using ‹y ≠ x› ‹e > 0› le_divide_eq[of e1 e "norm (y - x)"] by simp_all define z where "z = y - e1 *⇩_{R}(y - x)" { fix S assume "S ∈ I" then have "z ∈ rel_interior S" using rel_interior_closure_convex_shrink[of S x y e1] assms x y e1 z_def by auto } then have *: "z ∈ ⋂{rel_interior S |S. S ∈ I}" by auto have "∃z. z ∈ ⋂{rel_interior S |S. S ∈ I} ∧ z ≠ y ∧ dist z y ≤ e" apply (rule_tac x="z" in exI) using ‹y ≠ x› z_def * e1 e dist_norm[of z y] apply simp done } then have "y islimpt ⋂{rel_interior S |S. S ∈ I}" unfolding islimpt_approachable_le by blast then have "y ∈ closure (⋂{rel_interior S |S. S ∈ I})" unfolding closure_def by auto } ultimately have "y ∈ closure (⋂{rel_interior S |S. S ∈ I})" by auto } then show ?thesis by auto qed lemma convex_closure_inter: assumes "∀S∈I. convex (S :: 'n::euclidean_space set)" and "⋂{rel_interior S |S. S ∈ I} ≠ {}" shows "closure (⋂I) = ⋂{closure S |S. S ∈ I}" proof - have "⋂{closure S |S. S ∈ I} ≤ closure (⋂{rel_interior S |S. S ∈ I})" using convex_closure_rel_interior_inter assms by auto moreover have "closure (⋂{rel_interior S |S. S ∈ I}) ≤ closure (⋂I)" using rel_interior_inter_aux closure_mono[of "⋂{rel_interior S |S. S ∈ I}" "⋂I"] by auto ultimately show ?thesis using closure_Int[of I] by auto qed lemma convex_inter_rel_interior_same_closure: assumes "∀S∈I. convex (S :: 'n::euclidean_space set)" and "⋂{rel_interior S |S. S ∈ I} ≠ {}" shows "closure (⋂{rel_interior S |S. S ∈ I}) = closure (⋂I)" proof - have "⋂{closure S |S. S ∈ I} ≤ closure (⋂{rel_interior S |S. S ∈ I})" using convex_closure_rel_interior_inter assms by auto moreover have "closure (⋂{rel_interior S |S. S ∈ I}) ≤ closure (⋂I)" using rel_interior_inter_aux closure_mono[of "⋂{rel_interior S |S. S ∈ I}" "⋂I"] by auto ultimately show ?thesis using closure_Int[of I] by auto qed lemma convex_rel_interior_inter: assumes "∀S∈I. convex (S :: 'n::euclidean_space set)" and "⋂{rel_interior S |S. S ∈ I} ≠ {}" shows "rel_interior (⋂I) ⊆ ⋂{rel_interior S |S. S ∈ I}" proof - have "convex (⋂I)" using assms convex_Inter by auto moreover have "convex (⋂{rel_interior S |S. S ∈ I})" apply (rule convex_Inter) using assms convex_rel_interior apply auto done ultimately have "rel_interior (⋂{rel_interior S |S. S ∈ I}) = rel_interior (⋂I)" using convex_inter_rel_interior_same_closure assms closure_eq_rel_interior_eq[of "⋂{rel_interior S |S. S ∈ I}" "⋂I"] by blast then show ?thesis using rel_interior_subset[of "⋂{rel_interior S |S. S ∈ I}"] by auto qed lemma convex_rel_interior_finite_inter: assumes "∀S∈I. convex (S :: 'n::euclidean_space set)" and "⋂{rel_interior S |S. S ∈ I} ≠ {}" and "finite I" shows "rel_interior (⋂I) = ⋂{rel_interior S |S. S ∈ I}" proof - have "⋂I ≠ {}" using assms rel_interior_inter_aux[of I] by auto have "convex (⋂I)" using convex_Inter assms by auto show ?thesis proof (cases "I = {}") case True then show ?thesis using Inter_empty rel_interior_UNIV by auto next case False { fix z assume z: "z ∈ ⋂{rel_interior S |S. S ∈ I}" { fix x assume x: "x ∈ ⋂I" { fix S assume S: "S ∈ I" then have "z ∈ rel_interior S" "x ∈ S" using z x by auto then have "∃m. m > 1 ∧ (∀e. e > 1 ∧ e ≤ m ⟶ (1 - e)*⇩_{R}x + e *⇩_{R}z ∈ S)" using convex_rel_interior_if[of S z] S assms hull_subset[of S] by auto } then obtain mS where mS: "∀S∈I. mS S > 1 ∧ (∀e. e > 1 ∧ e ≤ mS S ⟶ (1 - e) *⇩_{R}x + e *⇩_{R}z ∈ S)" by metis define e where "e = Min (mS ` I)" then have "e ∈ mS ` I" using assms ‹I ≠ {}› by simp then have "e > 1" using mS by auto moreover have "∀S∈I. e ≤ mS S" using e_def assms by auto ultimately have "∃e > 1. (1 - e) *⇩_{R}x + e *⇩_{R}z ∈ ⋂I" using mS by auto } then have "z ∈ rel_interior (⋂I)" using convex_rel_interior_iff[of "⋂I" z] ‹⋂I ≠ {}› ‹convex (⋂I)› by auto } then show ?thesis using convex_rel_interior_inter[of I] assms by auto qed qed lemma convex_closure_inter_two: fixes S T :: "'n::euclidean_space set" assumes "convex S" and "convex T" assumes "rel_interior S ∩ rel_interior T ≠ {}" shows "closure (S ∩ T) = closure S ∩ closure T" using convex_closure_inter[of "{S,T}"] assms by auto lemma convex_rel_interior_inter_two: fixes S T :: "'n::euclidean_space set" assumes "convex S" and "convex T" and "rel_interior S ∩ rel_interior T ≠ {}" shows "rel_interior (S ∩ T) = rel_interior S ∩ rel_interior T" using convex_rel_interior_finite_inter[of "{S,T}"] assms by auto lemma convex_affine_closure_Int: fixes S T :: "'n::euclidean_space set" assumes "convex S" and "affine T" and "rel_interior S ∩ T ≠ {}" shows "closure (S ∩ T) = closure S ∩ T" proof - have "affine hull T = T" using assms by auto then have "rel_interior T = T" using rel_interior_affine_hull[of T] by metis moreover have "closure T = T" using assms affine_closed[of T] by auto ultimately show ?thesis using convex_closure_inter_two[of S T] assms affine_imp_convex by auto qed lemma connected_component_1_gen: fixes S :: "'a :: euclidean_space set" assumes "DIM('a) = 1" shows "connected_component S a b ⟷ closed_segment a b ⊆ S" unfolding connected_component_def by (metis (no_types, lifting) assms subsetD subsetI convex_contains_segment convex_segment(1) ends_in_segment connected_convex_1_gen) lemma connected_component_1: fixes S :: "real set" shows "connected_component S a b ⟷ closed_segment a b ⊆ S" by (simp add: connected_component_1_gen) lemma convex_affine_rel_interior_Int: fixes S T :: "'n::euclidean_space set" assumes "convex S" and "affine T" and "rel_interior S ∩ T ≠ {}" shows "rel_interior (S ∩ T) = rel_interior S ∩ T" proof - have "affine hull T = T" using assms by auto then have "rel_interior T = T" using rel_interior_affine_hull[of T] by metis moreover have "closure T = T" using assms affine_closed[of T] by auto ultimately show ?thesis using convex_rel_interior_inter_two[of S T] assms affine_imp_convex by auto qed lemma convex_affine_rel_frontier_Int: fixes S T :: "'n::euclidean_space set" assumes "convex S" and "affine T" and "interior S ∩ T ≠ {}" shows "rel_frontier(S ∩ T) = frontier S ∩ T" using assms apply (simp add: rel_frontier_def convex_affine_closure_Int frontier_def) by (metis Diff_Int_distrib2 Int_emptyI convex_affine_closure_Int convex_affine_rel_interior_Int empty_iff interior_rel_interior_gen) 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" proof - obtain a where aS: "a ∈ interior S" and aT:"a ∈ T" using assms by force have "rel_interior S = interior S" by (metis (no_types) aS affine_hull_nonempty_interior equals0D rel_interior_interior) then show ?thesis by (metis (no_types) affine_imp_convex assms convex_rel_interior_inter_two hull_same rel_interior_affine_hull) qed lemma closure_convex_Int_affine: fixes S :: "'a::euclidean_space set" assumes "convex S" "affine T" "rel_interior S ∩ T ≠ {}" shows "closure(S ∩ T) = closure S ∩ T" proof have "closure (S ∩ T) ⊆ closure T" by (simp add: closure_mono) also have "... ⊆ T" by (simp add: affine_closed assms) finally show "closure(S ∩ T) ⊆ closure S ∩ T" by (simp add: closure_mono) next obtain a where "a ∈ rel_interior S" "a ∈ T" using assms by auto then have ssT: "subspace ((λx. (-a)+x) ` T)" and "a ∈ S" using affine_diffs_subspace rel_interior_subset assms by blast+ show "closure S ∩ T ⊆ closure (S ∩ T)" proof fix x assume "x ∈ closure S ∩ T" show "x ∈ closure (S ∩ T)" proof (cases "x = a") case True then show ?thesis using ‹a ∈ S› ‹a ∈ T› closure_subset by fastforce next case False then have "x ∈ closure(open_segment a x)" by auto then show ?thesis using ‹x ∈ closure S ∩ T› assms convex_affine_closure_Int by blast qed qed qed 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 then have "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 then have "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 also have "… = rel_interior S" using * by auto finally show ?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 then show ?thesis using assms rel_interior_empty rel_interior_eq_empty 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 also have "… = f ` (closure (rel_interior S))" using convex_closure_rel_interior assms by auto also have "… ⊆ closure (f ` (rel_interior S))" using closure_linear_image_subset assms by auto finally have "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 then have "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 then have "rel_interior (f ` S) ⊆ f ` rel_interior S" using rel_interior_subset by auto moreover { fix z assume "z ∈ f ` rel_interior S" then obtain z1 where z1: "z1 ∈ rel_interior S" "f z1 = z" by auto { fix x assume "x ∈ f ` S" then obtain x1 where x1: "x1 ∈ S" "f x1 = x" by auto then obtain 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 moreover have "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›) ultimately have "(1 - e) *⇩_{R}x + e *⇩_{R}z ∈ f ` S" using imageI[of "(1 - e) *⇩_{R}x1 + e *⇩_{R}z1" S f] by auto then have "∃e. e > 1 ∧ (1 - e) *⇩_{R}x + e *⇩_{R}z ∈ f ` S" using e by auto } then have "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 } ultimately show ?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 rel_interior_empty by auto have nonemp: "f -` S ≠ {}" by (metis assms(3) rel_interior_subset subset_empty vimage_mono) then have "S ∩ (range f) ≠ {}" by auto have conv: "convex (f -` S)" using convex_linear_vimage assms by auto then have "convex (S ∩ range f)" by (simp add: assms(2) convex_Int convex_linear_image linear_axioms) { fix z assume "z ∈ f -` (rel_interior S)" then have z: "f z ∈ rel_interior S" by auto { fix x assume "x ∈ f -` S" then have "f x ∈ S" by auto then obtain 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 moreover have "(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) ultimately have "∃e. e > 1 ∧ (1 - e) *⇩_{R}x + e *⇩_{R}z ∈ f -` S" using e by auto } then have "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" then obtain y where y: "f y = x" "y ∈ f -` S" by auto then obtain 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 moreover have "(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) ultimately have "∃e. e > 1 ∧ (1 - e) *⇩_{R}x + e *⇩_{R}f z ∈ S ∩ range f" using e by auto } then have "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 moreover have "affine (range f)" by (simp add: linear_axioms linear_subspace_image subspace_imp_affine) ultimately have "f z ∈ rel_interior S" using convex_affine_rel_interior_Int[of S "range f"] assms by auto then have "z ∈ f -` (rel_interior S)" by auto } ultimately show ?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 - { assume "S = {}" then have ?thesis by auto } moreover { assume "T = {}" then have ?thesis by auto } moreover { assume "S ≠ {}" "T ≠ {}" then have ri: "rel_interior S ≠ {}" "rel_interior T ≠ {}" using rel_interior_eq_empty assms by auto then have "fst -` rel_interior S ≠ {}" using fst_vimage_eq_Times[of "rel_interior S"] by auto then have "rel_interior ((fst :: 'n * 'm ⇒ 'n) -` S) = fst -` rel_interior S" using fst_linear ‹convex S› rel_interior_convex_linear_preimage[of fst S] by auto then have 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 then have "rel_interior ((snd :: 'n * 'm ⇒ 'm) -` T) = snd -` rel_interior T" using snd_linear ‹convex T› rel_interior_convex_linear_preimage[of snd T] by auto then have 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 then have "rel_interior (S × T) = rel_interior ((S × (UNIV :: 'm set)) ∩ ((UNIV :: 'n set) × T))" by auto also have "… = rel_interior (S × (UNIV :: 'm set)) ∩ rel_interior ((UNIV :: 'n set) × T)" apply (subst convex_rel_interior_inter_two[of "S × (UNIV :: 'm set)" "(UNIV :: 'n set) × T"]) using * ri assms convex_Times apply auto done finally have ?thesis using * by auto } ultimately show ?thesis by blast 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: assumes "∀S∈I. convex (S :: 'n::euclidean_space set) ∧ rel_open S" and "finite I" shows "convex (⋂I) ∧ rel_open (⋂I)" proof (cases "⋂{rel_interior S |S. S ∈ I} = {}") case True then have "⋂I = {}" using assms unfolding rel_open_def by auto then show ?thesis unfolding rel_open_def using rel_interior_empty by auto next case False then have "rel_open (⋂I)" using assms unfolding rel_open_def using convex_rel_interior_finite_inter[of I] by auto then show ?thesis using convex_Inter assms by auto qed lemma convex_rel_open_linear_image: 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)" by (metis assms convex_linear_image rel_interior_convex_linear_image rel_open_def) 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 then have "f -` S = {}" using assms unfolding rel_open_def by auto then show ?thesis unfolding rel_open_def using rel_interior_empty by auto next case False then have "rel_open (f -` S)" using assms unfolding rel_open_def using rel_interior_convex_linear_preimage[of f S] by auto then show ?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 ≠ {}}" then obtain z where "(y, z) ∈ S" using assms by auto then have "∃x. x ∈ S ∧ y = fst x" apply (rule_tac x="(y, z)" in exI) apply auto done then obtain x where "x ∈ S" "y = fst x" by blast then have "y ∈ fst ` S" unfolding image_def by auto } then have "fst ` S = {y. f y ≠ {}}" unfolding fst_def using assms by auto then have h1: "fst ` rel_interior S = rel_interior {y. f y ≠ {}}" using rel_interior_convex_linear_image[of fst S] assms fst_linear by auto { fix y assume "y ∈ rel_interior {y. f y ≠ {}}" then have "y ∈ fst ` rel_interior S" using h1 by auto then have *: "rel_interior S ∩ fst -` {y} ≠ {}" by auto moreover have aff: "affine (fst -` {y})" unfolding affine_alt by (simp add: algebra_simps) ultimately have **: "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" then have "(y, x) ∈ S ∩ (fst -` {y})" using assms by auto moreover have "x = snd (y, x)" by auto ultimately have "x ∈ snd ` (S ∩ fst -` {y})" by blast } then have "snd ` (S ∩ fst -` {y}) = f y" using assms by auto then have ***: "rel_interior (f y) = snd ` rel_interior (S ∩ fst -` {y})" using rel_interior_convex_linear_image[of snd "S ∩ fst -` {y}"] snd_linear conv by auto { fix z assume "z ∈ rel_interior (f y)" then have "z ∈ snd ` rel_interior (S ∩ fst -` {y})" using *** by auto moreover have "{y} = fst ` rel_interior (S ∩ fst -` {y})" using * ** rel_interior_subset by auto ultimately have "(y, z) ∈ rel_interior (S ∩ fst -` {y})" by force then have "(y,z) ∈ rel_interior S" using ** by auto } moreover { fix z assume "(y, z) ∈ rel_interior S" then have "(y, z) ∈ rel_interior (S ∩ fst -` {y})" using ** by auto then have "z ∈ snd ` rel_interior (S ∩ fst -` {y})" by (metis Range_iff snd_eq_Range) then have "z ∈ rel_interior (f y)" using *** by auto } ultimately have "⋀z. (y, z) ∈ rel_interior S ⟷ z ∈ rel_interior (f y)" by auto } then have 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" then have "y ∈ fst ` rel_interior S" by (metis Domain_iff fst_eq_Domain) then have "y ∈ rel_interior {t. f t ≠ {}}" using h1 by auto then have "y ∈ rel_interior {t. f t ≠ {}}" and "(z ∈ rel_interior (f y))" using h2 asm by auto } then show ?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%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 then show ?thesis by (simp add: rel_interior_empty cone_0) next case False then have *: "0 ∈ S ∧ (∀c. c > 0 ⟶ ( *⇩_{R}) c ` S = S)" using cone_iff[of S] assms by auto then have *: "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) then show ?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 then show ?thesis by (simp add: rel_interior_empty cone_hull_empty) next case False then obtain 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 then have *: "(c, x) ∈ rel_interior (cone hull ({(1 :: real)} × S)) = (c ∈ rel_interior {y. f y ≠ {}} ∧ x ∈ rel_interior (f c))" apply (subst rel_interior_projection[of "cone hull ({(1 :: real)} × S)" f c x]) using convex_cone_hull[of "{(1 :: real)} × S"] conv apply auto done { fix y :: real assume "y ≥ 0" then have "y *⇩_{R}(1,s) ∈ cone hull ({1 :: real} × S)" using cone_hull_expl[of "{(1 :: real)} × S"] ‹s ∈ S› by auto then have "f y ≠ {}" using f_def by auto } then have "{y. f y ≠ {}} = {0..}" using f_def cone_hull_expl[of "{1 :: real} × S"] by auto then have **: "rel_interior {y. f y ≠ {}} = {0<..}" using rel_interior_real_semiline by auto { fix c :: real assume "c > 0" then have "f c = (( *⇩_{R}) c ` S)" using f_def cone_hull_expl[of "{1 :: real} × S"] by auto then have "rel_interior (f c) = ( *⇩_{R}) c ` rel_interior S" using rel_interior_convex_scaleR[of S c] assms by auto } then show ?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 have "z ∈ ?rhs" using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms ‹z ∈ ?lhs› apply auto apply (rule_tac x = "fst z" in exI) apply (rule_tac x = x in exI) using * apply auto done } moreover { fix z assume "z ∈ ?rhs" then have "z ∈ ?lhs" using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms by auto } ultimately show ?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" then obtain 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 then have "∀i∈I. s i ∈ convex hull (⋃(S ` I))" using hull_subset[of "⋃(S ` I)" convex] by auto then show "x ∈ ?lhs" unfolding *(1)[symmetric] apply (subst convex_sum[of I "convex hull ⋃(S ` I)" c s]) using * assms convex_convex_hull apply auto done qed { fix i assume "i ∈ I" with assms have "∃p. p ∈ S i" by auto } then obtain 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 then have *: "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 then have "∀j. c j *⇩_{R}s j = (if j = i then x else 0)" using c_def by (auto simp add: algebra_simps) then have "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 then have "x ∈ ?rhs" apply auto apply (rule_tac x = c in exI) apply (rule_tac x = s in exI) using * c_def s_def p ‹x ∈ S i› apply auto done } then have "?rhs ⊇ S i" by auto } then have *: "?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) moreover have "sum (λi. v * d i) I = v * sum d I" by (simp add: sum_distrib_left) ultimately have 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 then show ?thesis using i p q_def by auto next case False then show ?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 } then have 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 moreover from ge have "u * c i ≤ 0 ∧ v * d i ≤ 0" using True e_def i by simp ultimately have "u * c i = 0 ∧ v * d i = 0" by auto with True show ?thesis by auto next case False then have "(u * (c i)/(e i))*⇩_{R}(s i)+(v * (d i)/(e i))*⇩_{R}(t i) = q i" using q_def by auto then have "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 } then have *: "∀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) also have "… = sum (λi. e i *⇩_{R}q i) I" using * by auto finally have "u *⇩_{R}x + v *⇩_{R}y = sum (λi. (e i) *⇩_{R}(q i)) I" by auto then have "u *⇩_{R}x + v *⇩_{R}y ∈ ?rhs" using ge0 sum1 qs by auto } then have "convex ?rhs" unfolding convex_def by auto then show ?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 then have "convex hull (⋃(s ` I)) = convex hull (S ∪ T)" by auto moreover have "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)}" apply (subst convex_hull_finite_union[of I s]) using assms s_def I_def apply auto done moreover have "{∑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 ultimately show "?lhs ⊆ ?rhs" by auto { fix x assume "x ∈ ?rhs" then obtain 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 then have "x ∈ convex hull {s, t}" using convex_hull_2[of s t] by auto then have "x ∈ convex hull (S ∪ T)" using * hull_mono[of "{s, t}" "S ∪ T"] by auto } then show "?lhs ⊇ ?rhs" by blast qed subsection%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 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) also have "… = (λ(x,y). x + y) ` rel_interior (S × T)" using rel_interior_Times assms by auto also have "… = 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) finally show ?thesis .. qed lemma rel_interior_sum_gen: fixes S :: "'a ⇒ 'n::euclidean_space set" assumes "∀i∈I. convex (S i)" shows "rel_interior (sum S I) = sum (λi. rel_interior (S i)) I" apply (subst sum_set_cond_linear[of convex]) using rel_interior_sum rel_interior_sing[of "0"] assms apply (auto simp add: convex_set_plus) done 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. 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" then obtain 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 { fix i assume "i ∈ I" then have "s i ∈ S i" using s_def x assms mem_cone[of "S i" "xs i" "c i"] by auto } then have "∀i∈I. s i ∈ S i" by auto moreover have "x = sum s I" using x s_def by auto ultimately have "x ∈ ?rhs" using set_sum_alt[of I S] assms by auto } moreover { fix x assume "x ∈ ?rhs" then obtain 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 then have "x = sum (λi. ((1 :: real) / of_nat(card I)) *⇩_{R}xs i) I" using x assms by auto moreover have "∀i∈I. xs i ∈ S i" using x xs_def assms by (simp add: cone_def) moreover have "∀i∈I. (1 :: real) / of_nat (card I) ≥ 0" by auto moreover have "sum (λi. (1 :: real) / of_nat (card I)) I = 1" using assms by auto ultimately have "x ∈ ?lhs" apply (subst convex_hull_finite_union[of I S]) using assms apply blast using assms apply blast apply rule apply (rule_tac x = "(λi. (1 :: real) / of_nat (card I))" in exI) apply auto done } ultimately show ?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 then have "convex hull (⋃(A ` I)) = convex hull (S ∪ T)" by auto moreover have "convex hull ⋃(A ` I) = sum A I" apply (subst convex_hull_finite_union_cones[of I A]) using assms A_def I_def apply auto done moreover have "sum A I = S + T" using A_def I_def unfolding set_plus_def apply auto unfolding set_plus_def apply auto done ultimately show ?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 then show ?thesis using convex_hull_empty rel_interior_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]) { fix i assume "i ∈ I" then have "convex (K i)" unfolding K_def apply (subst convex_cone_hull) apply (subst convex_Times) using assms apply auto done } then have convK: "∀i∈I. convex (K i)" by auto { fix i assume "i ∈ I" then have "K0 ⊇ K i" unfolding K0_def K_def apply (subst hull_mono) using ‹∀i∈I. C0 ≥ S i› apply auto done } then have "K0 ⊇ ⋃(K ` I)" by auto moreover have "convex K0" unfolding K0_def apply (subst convex_cone_hull) apply (subst convex_Times) unfolding C0_def using convex_convex_hull apply auto done ultimately have 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) then have "⋃(K ` I) ⊇ {1 :: real} × ⋃(S ` I)" by auto then have "convex hull ⋃(K ` I) ⊇ convex hull ({1 :: real} × ⋃(S ` I))" by (simp add: hull_mono) then have "convex hull ⋃(K ` I) ⊇ {1 :: real} × C0" unfolding C0_def using convex_hull_Times[of "{(1 :: real)}" "⋃(S ` I)"] convex_hull_singleton by auto moreover have "cone (convex hull (⋃(K ` I)))" apply (subst cone_convex_hull) using cone_Union[of "K ` I"] apply auto unfolding K_def using cone_cone_hull apply auto done ultimately have "convex hull (⋃(K ` I)) ⊇ K0" unfolding K0_def using hull_minimal[of _ "convex hull (⋃(K ` I))" "cone"] by blast then have "K0 = convex hull (⋃(K ` I))" using geq by auto also have "… = sum K I" apply (subst convex_hull_finite_union_cones[of I K]) using assms apply blast using False apply blast unfolding K_def apply rule apply (subst convex_cone_hull) apply (subst convex_Times) using assms cone_cone_hull ‹∀i∈I. K i ≠ {}› K_def apply auto done finally have "K0 = sum K I" by auto then have *: "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" then have "(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 then obtain 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" then have "convex (S i) ∧ k i ∈ rel_interior (cone hull {1} × S i)" using k K_def assms by auto then have "∃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 } then obtain 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 then have "x = (∑i∈I. c i *⇩_{R}s i) ∧ sum c I = 1" using k by (simp add: sum_prod) then have "x ∈ ?rhs" using k cs by auto } moreover { fix x assume "x ∈ ?rhs" then obtain 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" then have "k i ∈ rel_interior (K i)" using k_def K_def assms cs rel_interior_convex_cone[of "S i"] by auto } then have "(1::real, x) ∈ rel_interior K0" using K0_def * set_sum_alt[of I "(λi. rel_interior (K i))"] assms k_def cs apply auto apply (rule_tac x = k in exI) apply (simp add: sum_prod) done then have "x ∈ ?lhs" using K0_def C0_def rel_interior_convex_cone_aux[of C0 1 x] by auto } ultimately show ?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" . moreover define t where "t = min (x + e / 2) ((x + y) / 2)" ultimately have "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 have "open (interior I)" by auto from openE[OF this ‹x ∈ interior I›] obtain e where "0 < e" "ball x e ⊆ interior I" . moreover define K where "K = x - e / 2" with ‹0 < e› have "K ∈ ball x e" "K < x" by (auto simp: dist_real_def) ultimately have "K ∈ I" "K < x" "x ∈ I" using interior_subset[of I] ‹x ∈ interior I› by auto 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_diff) next fix y assume "y ∈ ?F x" with order_trans[OF convex_on_diff[OF ‹convex_on I f› ‹K ∈ I› _ ‹K < x› _]] show "(f K - f x) / (K - x) ≤ y" by auto qed then show ?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" . moreover define t where "t = x + e / 2" ultimately have "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_diff[OF ‹convex_on I f› ‹y ∈ I› _ ‹y < x›]] have "(f y - f x) / (y - x) ≤ z" by auto finally show "(f x - f y) / (x - y) ≤ z" . next have "open (interior I)" by auto from openE[OF this ‹x ∈ interior I›] obtain e where e: "0 < e" "ball x e ⊆ interior I" . then have "x + e / 2 ∈ ball x e" by (auto simp: dist_real_def) with e interior_subset[of I] have "x + e / 2 ∈ {x<..} ∩ I" by auto then show "?F x ≠ {}" by blast qed then show ?thesis using ‹y < x› by (simp add: field_simps) qed simp subsection%unimportant‹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) then show ?thesis using at_within_interior assms by fastforce qed lemma affine_independent_convex_affine_hull: fixes s :: "'a::euclidean_space set" assumes "~affine_dependent s" "t ⊆ s" shows "convex hull t = affine hull t ∩ convex hull s" proof - have fin: "finite s" "finite t" using assms aff_independent_finite finite_subset by auto { fix u v x assume uv: "sum u t = 1" "∀x∈s. 0 ≤ v x" "sum v s = 1" "(∑x∈s. v x *⇩_{R}x) = (∑v∈t. u v *⇩_{R}v)" "x ∈ t" then have s: "s = (s - t) ∪ t" ― ‹split into separate cases› using assms by auto have [simp]: "(∑x∈t. v x *⇩_{R}x) + (∑x∈s - t. v x *⇩_{R}x) = (∑x∈t. u x *⇩_{R}x)" "sum v t + sum v (s - t) = 1" using uv fin s by (auto simp: sum.union_disjoint [symmetric] Un_commute) have "(∑x∈s. if x ∈ t then v x - u x else v x) = 0" "(∑x∈s. (if x ∈ t then v x - u x else v x) *⇩_{R}x) = 0" using uv fin by (subst s, subst sum.union_disjoint, auto simp: algebra_simps sum_subtractf)+ } note [simp] = this have "convex hull t ⊆ affine hull t" using convex_hull_subset_affine_hull by blast moreover have "convex hull t ⊆ convex hull s" using assms hull_mono by blast moreover have "affine hull t ∩ convex hull s ⊆ convex hull t" using assms apply (simp add: convex_hull_finite affine_hull_finite fin affine_dependent_explicit) apply (drule_tac x=s in spec) apply (auto simp: fin) apply (rule_tac x=u in exI) apply (rename_tac v) apply (drule_tac x="λx. if x ∈ t then v x - u x else v x" in spec) apply (force)+ done ultimately show ?thesis by blast qed lemma affine_independent_span_eq: fixes s :: "'a::euclidean_space set" assumes "~affine_dependent s" "card s = Suc (DIM ('a))" shows "affine hull s = UNIV" proof (cases "s = {}") case True then show ?thesis using assms by simp next case False then obtain a t where t: "a ∉ t" "s = insert a t" by blast then have fin: "finite t" using assms by (metis finite_insert aff_independent_finite) show ?thesis using assms t fin apply (simp add: affine_dependent_iff_dependent affine_hull_insert_span_gen) apply (rule subset_antisym) apply force apply (rule Fun.vimage_subsetD) apply (metis add.commute diff_add_cancel surj_def) apply (rule card_ge_dim_independent) apply (auto simp: card_image inj_on_def dim_subset_UNIV) done qed lemma affine_independent_span_gt: fixes s :: "'a::euclidean_space set" assumes ind: "~ affine_dependent s" and dim: "DIM ('a) < card s" shows "affine hull s = UNIV" apply (rule affine_independent_span_eq [OF ind]) apply (rule antisym) using assms apply auto apply (metis add_2_eq_Suc' not_less_eq_eq affine_dependent_biggerset aff_independent_finite) done lemma empty_interior_affine_hull: fixes s :: "'a::euclidean_space set" assumes "finite s" and dim: "card s ≤ DIM ('a)" shows "interior(affine hull s) = {}" using assms apply (induct s rule: finite_induct) apply (simp_all add: affine_dependent_iff_dependent affine_hull_insert_span_gen interior_translation) apply (rule empty_interior_lowdim) by (auto simp: Suc_le_lessD card_image_le dual_order.trans intro!: dim_le_card'[THEN le_less_trans]) lemma empty_interior_convex_hull: fixes s :: "'a::euclidean_space set" assumes "finite s" and dim: "card s ≤ DIM ('a)" shows "interior(convex hull s) = {}" by (metis Diff_empty Diff_eq_empty_iff convex_hull_subset_affine_hull interior_mono empty_interior_affine_hull [OF assms]) lemma explicit_subset_rel_interior_convex_hull: fixes s :: "'a::euclidean_space set" shows "finite s ⟹ {y. ∃u. (∀x ∈ s. 0 < u x ∧ u x < 1) ∧ sum u s = 1 ∧ sum (λx. u x *⇩_{R}x) s = y} ⊆ rel_interior (convex hull s)" by (force simp add: rel_interior_convex_hull_union [where S="λx. {x}" and I=s, simplified]) lemma explicit_subset_rel_interior_convex_hull_minimal: fixes s :: "'a::euclidean_space set" shows "finite s ⟹ {y. ∃u. (∀x ∈ s. 0 < u x) ∧ sum u s = 1 ∧ sum (λx. u x *⇩_{R}x) s = y} ⊆ rel_interior (convex hull s)" by (force simp add: rel_interior_convex_hull_union [where S="λx. {x}" and I=s, simplified]) lemma rel_interior_convex_hull_explicit: fixes s :: "'a::euclidean_space set" assumes "~ affine_dependent s" shows "rel_interior(convex hull s) = {y. ∃u. (∀x ∈ s. 0 < u x) ∧ sum u s = 1 ∧ sum (λx. u x *⇩_{R}x) s = y}" (is "?lhs = ?rhs") proof show "?rhs ≤ ?lhs" by (simp add: aff_independent_finite explicit_subset_rel_interior_convex_hull_minimal assms) next show "?lhs ≤ ?rhs" proof (cases "∃a. s = {a}") case True then show "?lhs ≤ ?rhs" by force next case False have fs: "finite s" using assms by (simp add: aff_independent_finite) { fix a b and d::real assume ab: "a ∈ s" "b ∈ s" "a ≠ b" then have s: "s = (s - {a,b}) ∪ {a,b}" ― ‹split into separate cases› by auto have "(∑x∈s. if x = a then - d else if x = b then d else 0) = 0" "(∑x∈s. (if x = a then - d else if x = b then d else 0) *⇩_{R}x) = d *⇩_{R}b - d *⇩_{R}a" using ab fs by (subst s, subst sum.union_disjoint, auto)+ } note [simp] = this { fix y assume y: "y ∈ convex hull s" "y ∉ ?rhs" { fix u T a assume ua: "∀x∈s. 0 ≤ u x" "sum u s = 1" "¬ 0 < u a" "a ∈ s" and yT: "y = (∑x∈s. u x *⇩_{R}x)" "y ∈ T" "open T" and sb: "T ∩ affine hull s ⊆ {w. ∃u. (∀x∈s. 0 ≤ u x) ∧ sum u s = 1 ∧ (∑x∈s. u x *⇩_{R}x) = w}" have ua0: "u a = 0" using ua by auto obtain b where b: "b∈s" "a ≠ b" using ua False by auto obtain e where e: "0 < e" "ball (∑x∈s. u x *⇩_{R}x) e ⊆ T" using yT by (auto elim: openE) with b obtain d where d: "0 < d" "norm(d *⇩_{R}(a-b)) < e" by (auto intro: that [of "e / 2 / norm(a-b)"]) have "(∑x∈s. u x *⇩_{R}x) ∈ affine hull s" using yT y by (metis affine_hull_convex_hull hull_redundant_eq) then have "(∑x∈s. u x *⇩_{R}x) - d *⇩_{R}(a - b) ∈ affine hull s" using ua b by (auto simp: hull_inc intro: mem_affine_3_minus2) then have "y - d *⇩_{R}(a - b) ∈ T ∩ affine hull s" using d e yT by auto then obtain v where "∀x∈s. 0 ≤ v x" "sum v s = 1" "(∑x∈s. v x *⇩_{R}x) = (∑x∈s. u x *⇩_{R}x) - d *⇩_{R}(a - b)" using subsetD [OF sb] yT by auto then have False using assms apply (simp add: affine_dependent_explicit_finite fs) apply (drule_tac x="λx. (v x - u x) - (if x = a then -d else if x = b then d else 0)" in spec) using ua b d apply (auto simp: algebra_simps sum_subtractf sum.distrib) done } note * = this have "y ∉ rel_interior (convex hull s)" using y apply (simp add: mem_rel_interior affine_hull_convex_hull) apply (auto simp: convex_hull_finite [OF fs]) apply (drule_tac x=u in spec) apply (auto intro: *) done } with rel_interior_subset show "?lhs ≤ ?rhs" by blast qed qed lemma interior_convex_hull_explicit_minimal: fixes s :: "'a::euclidean_space set" shows "~ affine_dependent s ==> interior(convex hull s) = (if card(s) ≤ DIM('a) then {} else {y. ∃u. (∀x ∈ s. 0 < u x) ∧ sum u s = 1 ∧ (∑x∈s. u x *⇩_{R}x) = y})" apply (simp add: aff_independent_finite empty_interior_convex_hull, clarify) apply (rule trans [of _ "rel_interior(convex hull s)"]) apply (simp add: affine_hull_convex_hull affine_independent_span_gt rel_interior_interior) by (simp add: rel_interior_convex_hull_explicit) lemma interior_convex_hull_explicit: fixes s :: "'a::euclidean_space set" assumes "~ affine_dependent s" shows "interior(convex hull s) = (if card(s) ≤ DIM('a) then {} else {y. ∃u. (∀x ∈ s. 0 < u x ∧ u x < 1) ∧ sum u s = 1 ∧ (∑x∈s. u x *⇩_{R}x) = y})" proof - { fix u :: "'a ⇒ real" and a assume "card Basis < card s" and u: "⋀x. x∈s ⟹ 0 < u x" "sum u s = 1" and a: "a ∈ s" then have cs: "Suc 0 < card s" by (metis DIM_positive less_trans_Suc) obtain b where b: "b ∈ s" "a ≠ b" proof (cases "s ≤ {a}") case True then show thesis using cs subset_singletonD by fastforce next case False then show thesis by (blast intro: that) qed have "u a + u b ≤ sum u {a,b}" using a b by simp also have "... ≤ sum u s" apply (rule Groups_Big.sum_mono2) using a b u apply (auto simp: less_imp_le aff_independent_finite assms) done finally have "u a < 1" using ‹b ∈ s› u by fastforce } note [simp] = this show ?thesis using assms apply (auto simp: interior_convex_hull_explicit_minimal) apply (rule_tac x=u in exI) apply (auto simp: not_le) done qed lemma interior_closed_segment_ge2: fixes a :: "'a::euclidean_space" assumes "2 ≤ DIM('a)" shows "interior(closed_segment a b) = {}" using assms unfolding segment_convex_hull proof - have "card {a, b} ≤ DIM('a)" using assms by (simp add: card_insert_if linear not_less_eq_eq numeral_2_eq_2) then show "interior (convex hull {a, b}) = {}" by (metis empty_interior_convex_hull finite.insertI finite.emptyI) qed lemma interior_open_segment: fixes a :: "'a::euclidean_space" shows "interior(open_segment a b) = (if 2 ≤ DIM('a) then {} else open_segment a b)" proof (simp add: not_le, intro conjI impI) assume "2 ≤ DIM('a)" then show "interior (open_segment a b) = {}" apply (simp add: segment_convex_hull open_segment_def) apply (metis Diff_subset interior_mono segment_convex_hull subset_empty interior_closed_segment_ge2) done next assume le2: "DIM('a) < 2" show "interior (open_segment a b) = open_segment a b" proof (cases "a = b") case True then show ?thesis by auto next case False with le2 have "affine hull (open_segment a b) = UNIV" apply simp apply (rule affine_independent_span_gt) apply (simp_all add: affine_dependent_def insert_Diff_if) done then show "interior (open_segment a b) = open_segment a b" using rel_interior_interior rel_interior_open_segment by blast qed qed lemma interior_closed_segment: fixes a :: "'a::euclidean_space" shows "interior(closed_segment a b) = (if 2 ≤ DIM('a) then {} else open_segment a b)" proof (cases "a = b") case True then show ?thesis by simp next case False then have "closure (open_segment a b) = closed_segment a b" by simp then show ?thesis by (metis (no_types) convex_interior_closure convex_open_segment interior_open_segment) qed lemmas interior_segment = interior_closed_segment interior_open_segment lemma closed_segment_eq [simp]: fixes a :: "'a::euclidean_space" shows "closed_segment a b = closed_segment c d ⟷ {a,b} = {c,d}" proof assume abcd: "closed_segment a b = closed_segment c d" show "{a,b} = {c,d}"