Theory HOL-Analysis.Convex_Euclidean_Space
section ‹Convex Sets and Functions on (Normed) Euclidean Spaces›
theory Convex_Euclidean_Space
imports
Convex Topology_Euclidean_Space Line_Segment
begin
subsection ‹Topological Properties of Convex Sets and Functions›
lemma aff_dim_cball:
fixes a :: "'n::euclidean_space"
assumes "e > 0"
shows "aff_dim (cball a e) = int (DIM('n))"
proof -
have "(λx. a + x) ` (cball 0 e) ⊆ cball a e"
unfolding cball_def dist_norm by auto
then have "aff_dim (cball (0 :: 'n::euclidean_space) e) ≤ aff_dim (cball a e)"
using aff_dim_translation_eq[of a "cball 0 e"]
aff_dim_subset[of "(+) a ` cball 0 e" "cball a e"]
by auto
moreover have "aff_dim (cball (0 :: 'n::euclidean_space) e) = int (DIM('n))"
using hull_inc[of "(0 :: 'n::euclidean_space)" "cball 0 e"]
centre_in_cball[of "(0 :: 'n::euclidean_space)"] assms
by (simp add: dim_cball[of e] aff_dim_zero[of "cball 0 e"])
ultimately show ?thesis
using aff_dim_le_DIM[of "cball a e"] by auto
qed
lemma aff_dim_open:
fixes S :: "'n::euclidean_space set"
assumes "open S"
and "S ≠ {}"
shows "aff_dim S = int (DIM('n))"
proof -
obtain x where "x ∈ S"
using assms by auto
then obtain e where e: "e > 0" "cball x e ⊆ S"
using open_contains_cball[of S] assms by auto
then have "aff_dim (cball x e) ≤ aff_dim S"
using aff_dim_subset by auto
with e show ?thesis
using aff_dim_cball[of e x] aff_dim_le_DIM[of S] by auto
qed
lemma low_dim_interior:
fixes S :: "'n::euclidean_space set"
assumes "¬ aff_dim S = int (DIM('n))"
shows "interior S = {}"
proof -
have "aff_dim(interior S) ≤ aff_dim S"
using interior_subset aff_dim_subset[of "interior S" S] by auto
then show ?thesis
using aff_dim_open[of "interior S"] aff_dim_le_DIM[of S] assms by auto
qed
corollary empty_interior_lowdim:
fixes S :: "'n::euclidean_space set"
shows "dim S < DIM ('n) ⟹ interior S = {}"
by (metis low_dim_interior affine_hull_UNIV dim_affine_hull less_not_refl dim_UNIV)
corollary aff_dim_nonempty_interior:
fixes S :: "'a::euclidean_space set"
shows "interior S ≠ {} ⟹ aff_dim S = DIM('a)"
by (metis low_dim_interior)
subsection ‹Relative interior of a set›
definition "rel_interior S =
{x. ∃T. openin (top_of_set (affine hull S)) T ∧ x ∈ T ∧ T ⊆ S}"
lemma rel_interior_mono:
"⟦S ⊆ T; affine hull S = affine hull T⟧
⟹ (rel_interior S) ⊆ (rel_interior T)"
by (auto simp: rel_interior_def)
lemma rel_interior_maximal:
"⟦T ⊆ S; openin(top_of_set (affine hull S)) T⟧ ⟹ T ⊆ (rel_interior S)"
by (auto simp: rel_interior_def)
lemma rel_interior: "rel_interior S = {x ∈ S. ∃T. open T ∧ x ∈ T ∧ T ∩ affine hull S ⊆ S}"
(is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs"
by (force simp add: rel_interior_def openin_open)
{ fix x T
assume *: "x ∈ S" "open T" "x ∈ T" "T ∩ affine hull S ⊆ S"
then have **: "x ∈ T ∩ affine hull S"
using hull_inc by auto
with * have "∃Tb. (∃Ta. open Ta ∧ Tb = affine hull S ∩ Ta) ∧ x ∈ Tb ∧ Tb ⊆ S"
by (rule_tac x = "T ∩ (affine hull S)" in exI) auto
}
then show "?rhs ⊆ ?lhs"
by (force simp add: rel_interior_def openin_open)
qed
lemma mem_rel_interior: "x ∈ rel_interior S ⟷ (∃T. open T ∧ x ∈ T ∩ S ∧ T ∩ affine hull S ⊆ S)"
by (auto simp: rel_interior)
lemma mem_rel_interior_ball:
"x ∈ rel_interior S ⟷ x ∈ S ∧ (∃e. e > 0 ∧ ball x e ∩ affine hull S ⊆ S)"
(is "?lhs = ?rhs")
proof
assume ?rhs then show ?lhs
by (simp add: rel_interior) (meson Elementary_Metric_Spaces.open_ball centre_in_ball)
qed (force simp: rel_interior open_contains_ball)
lemma rel_interior_ball:
"rel_interior S = {x ∈ S. ∃e. e > 0 ∧ ball x e ∩ affine hull S ⊆ S}"
using mem_rel_interior_ball [of _ S] by auto
lemma mem_rel_interior_cball:
"x ∈ rel_interior S ⟷ x ∈ S ∧ (∃e. e > 0 ∧ cball x e ∩ affine hull S ⊆ S)"
(is "?lhs = ?rhs")
proof
assume ?rhs then obtain e where "x ∈ S" "e > 0" "cball x e ∩ affine hull S ⊆ S"
by (auto simp: rel_interior)
then have "ball x e ∩ affine hull S ⊆ S"
by auto
then show ?lhs
using ‹0 < e› ‹x ∈ S› rel_interior_ball by auto
qed (force simp: rel_interior open_contains_cball)
lemma rel_interior_cball:
"rel_interior S = {x ∈ S. ∃e. e > 0 ∧ cball x e ∩ affine hull S ⊆ S}"
using mem_rel_interior_cball [of _ S] by auto
lemma rel_interior_empty [simp]: "rel_interior {} = {}"
by (auto simp: rel_interior_def)
lemma affine_hull_sing [simp]: "affine hull {a :: 'n::euclidean_space} = {a}"
by (metis affine_hull_eq affine_sing)
lemma rel_interior_sing [simp]:
fixes a :: "'n::euclidean_space" shows "rel_interior {a} = {a}"
proof -
have "∃x::real. 0 < x"
using zero_less_one by blast
then show ?thesis
by (auto simp: rel_interior_ball)
qed
lemma subset_rel_interior:
fixes S T :: "'n::euclidean_space set"
assumes "S ⊆ T"
and "affine hull S = affine hull T"
shows "rel_interior S ⊆ rel_interior T"
using assms by (auto simp: rel_interior_def)
lemma rel_interior_subset: "rel_interior S ⊆ S"
by (auto simp: rel_interior_def)
lemma rel_interior_subset_closure: "rel_interior S ⊆ closure S"
using rel_interior_subset by (auto simp: closure_def)
lemma interior_subset_rel_interior: "interior S ⊆ rel_interior S"
by (auto simp: rel_interior interior_def)
lemma interior_rel_interior:
fixes S :: "'n::euclidean_space set"
assumes "aff_dim S = int(DIM('n))"
shows "rel_interior S = interior S"
proof -
have "affine hull S = UNIV"
using assms affine_hull_UNIV[of S] by auto
then show ?thesis
unfolding rel_interior interior_def by auto
qed
lemma rel_interior_interior:
fixes S :: "'n::euclidean_space set"
assumes "affine hull S = UNIV"
shows "rel_interior S = interior S"
using assms unfolding rel_interior interior_def by auto
lemma rel_interior_open:
fixes S :: "'n::euclidean_space set"
assumes "open S"
shows "rel_interior S = S"
by (metis assms interior_eq interior_subset_rel_interior rel_interior_subset set_eq_subset)
lemma interior_rel_interior_gen:
fixes S :: "'n::euclidean_space set"
shows "interior S = (if aff_dim S = int(DIM('n)) then rel_interior S else {})"
by (metis interior_rel_interior low_dim_interior)
lemma rel_interior_nonempty_interior:
fixes S :: "'n::euclidean_space set"
shows "interior S ≠ {} ⟹ rel_interior S = interior S"
by (metis interior_rel_interior_gen)
lemma affine_hull_nonempty_interior:
fixes S :: "'n::euclidean_space set"
shows "interior S ≠ {} ⟹ affine hull S = UNIV"
by (metis affine_hull_UNIV interior_rel_interior_gen)
lemma rel_interior_affine_hull [simp]:
fixes S :: "'n::euclidean_space set"
shows "rel_interior (affine hull S) = affine hull S"
proof -
have *: "rel_interior (affine hull S) ⊆ affine hull S"
using rel_interior_subset by auto
{
fix x
assume x: "x ∈ affine hull S"
define e :: real where "e = 1"
then have "e > 0" "ball x e ∩ affine hull (affine hull S) ⊆ affine hull S"
using hull_hull[of _ S] by auto
then have "x ∈ rel_interior (affine hull S)"
using x rel_interior_ball[of "affine hull S"] by auto
}
then show ?thesis using * by auto
qed
lemma rel_interior_UNIV [simp]: "rel_interior (UNIV :: ('n::euclidean_space) set) = UNIV"
by (metis open_UNIV rel_interior_open)
lemma rel_interior_convex_shrink:
fixes S :: "'a::euclidean_space set"
assumes "convex S"
and "c ∈ rel_interior S"
and "x ∈ S"
and "0 < e"
and "e ≤ 1"
shows "x - e *⇩R (x - c) ∈ rel_interior S"
proof -
obtain d where "d > 0" and d: "ball c d ∩ affine hull S ⊆ S"
using assms(2) unfolding mem_rel_interior_ball by auto
{
fix y
assume as: "dist (x - e *⇩R (x - c)) y < e * d" "y ∈ affine hull S"
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: scaleR_left_diff_distrib scaleR_right_diff_distrib)
have "x ∈ affine hull S"
using assms hull_subset[of S] by auto
moreover have "1 / e + - ((1 - e) / e) = 1"
using ‹e > 0› left_diff_distrib[of "1" "(1-e)" "1/e"] by auto
ultimately have **: "(1 / e) *⇩R y - ((1 - e) / e) *⇩R x ∈ affine hull S"
using as affine_affine_hull[of S] mem_affine[of "affine hull S" y x "(1 / e)" "-((1 - e) / e)"]
by (simp add: algebra_simps)
have "c - ((1 / e) *⇩R y - ((1 - e) / e) *⇩R x) = (1 / e) *⇩R (e *⇩R c - y + (1 - e) *⇩R x)"
using ‹e > 0›
by (auto simp: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
then 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 norm_scaleR[symmetric] by auto
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:pos_divide_less_eq[OF ‹e > 0›] mult.commute)
finally have "(1 / e) *⇩R y - ((1 - e) / e) *⇩R x ∈ S"
using "**" d by auto
then have "y ∈ S"
using * convexD [OF ‹convex S›] assms(3-5)
by (metis diff_add_cancel diff_ge_0_iff_ge le_add_same_cancel1 less_eq_real_def)
}
then have "ball (x - e *⇩R (x - c)) (e*d) ∩ affine hull S ⊆ S"
by auto
moreover have "e * d > 0"
using ‹e > 0› ‹d > 0› by simp
moreover have c: "c ∈ S"
using assms rel_interior_subset by auto
moreover from c have "x - e *⇩R (x - c) ∈ S"
using convexD_alt[of S x c e] assms
by (metis diff_add_eq diff_diff_eq2 less_eq_real_def scaleR_diff_left scaleR_one scale_right_diff_distrib)
ultimately show ?thesis
using mem_rel_interior_ball[of "x - e *⇩R (x - c)" S] ‹e > 0› by auto
qed
lemma interior_real_atLeast [simp]:
fixes a :: real
shows "interior {a..} = {a<..}"
proof -
{
fix y
have "ball y (y - a) ⊆ {a..}"
by (auto simp: dist_norm)
moreover assume "a < y"
ultimately have "y ∈ interior {a..}"
by (force simp add: mem_interior)
}
moreover
{
fix y
assume "y ∈ interior {a..}"
then obtain e where e: "e > 0" "cball y e ⊆ {a..}"
using mem_interior_cball[of y "{a..}"] by auto
moreover from e have "y - e ∈ cball y e"
by (auto simp: cball_def dist_norm)
ultimately have "a ≤ y - e" by blast
then have "a < y" using e by auto
}
ultimately show ?thesis by auto
qed
lemma continuous_ge_on_Ioo:
assumes "continuous_on {c..d} g" "⋀x. x ∈ {c<..<d} ⟹ g x ≥ a" "c < d" "x ∈ {c..d}"
shows "g (x::real) ≥ (a::real)"
proof-
from assms(3) have "{c..d} = closure {c<..<d}" by (rule closure_greaterThanLessThan[symmetric])
also from assms(2) have "{c<..<d} ⊆ (g -` {a..} ∩ {c..d})" by auto
hence "closure {c<..<d} ⊆ closure (g -` {a..} ∩ {c..d})" by (rule closure_mono)
also from assms(1) have "closed (g -` {a..} ∩ {c..d})"
by (auto simp: continuous_on_closed_vimage)
hence "closure (g -` {a..} ∩ {c..d}) = g -` {a..} ∩ {c..d}" by simp
finally show ?thesis using ‹x ∈ {c..d}› by auto
qed
lemma interior_real_atMost [simp]:
fixes a :: real
shows "interior {..a} = {..<a}"
proof -
{
fix y
have "ball y (a - y) ⊆ {..a}"
by (auto simp: dist_norm)
moreover assume "a > y"
ultimately have "y ∈ interior {..a}"
by (force simp add: mem_interior)
}
moreover
{
fix y
assume "y ∈ interior {..a}"
then obtain e where e: "e > 0" "cball y e ⊆ {..a}"
using mem_interior_cball[of y "{..a}"] by auto
moreover from e have "y + e ∈ cball y e"
by (auto simp: cball_def dist_norm)
ultimately have "a ≥ y + e" by auto
then have "a > y" using e by auto
}
ultimately show ?thesis by auto
qed
lemma interior_atLeastAtMost_real [simp]: "interior {a..b} = {a<..<b :: real}"
proof-
have "{a..b} = {a..} ∩ {..b}" by auto
also have "interior … = {a<..} ∩ {..<b}"
by (simp)
also have "… = {a<..<b}" by auto
finally show ?thesis .
qed
lemma interior_atLeastLessThan [simp]:
fixes a::real shows "interior {a..<b} = {a<..<b}"
by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost_real interior_Int interior_interior interior_real_atLeast)
lemma interior_lessThanAtMost [simp]:
fixes a::real shows "interior {a<..b} = {a<..<b}"
by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost_real interior_Int
interior_interior interior_real_atLeast)
lemma interior_greaterThanLessThan_real [simp]: "interior {a<..<b} = {a<..<b :: real}"
by (metis interior_atLeastAtMost_real interior_interior)
lemma frontier_real_atMost [simp]:
fixes a :: real
shows "frontier {..a} = {a}"
unfolding frontier_def by auto
lemma frontier_real_atLeast [simp]: "frontier {a..} = {a::real}"
by (auto simp: frontier_def)
lemma frontier_real_greaterThan [simp]: "frontier {a<..} = {a::real}"
by (auto simp: interior_open frontier_def)
lemma frontier_real_lessThan [simp]: "frontier {..<a} = {a::real}"
by (auto simp: interior_open frontier_def)
lemma rel_interior_real_box [simp]:
fixes a b :: real
assumes "a < b"
shows "rel_interior {a .. b} = {a <..< b}"
proof -
have "box a b ≠ {}"
using assms
unfolding set_eq_iff
by (auto intro!: exI[of _ "(a + b) / 2"] simp: box_def)
then show ?thesis
using interior_rel_interior_gen[of "cbox a b", symmetric]
by (simp split: if_split_asm del: box_real add: box_real[symmetric])
qed
lemma rel_interior_real_semiline [simp]:
fixes a :: real
shows "rel_interior {a..} = {a<..}"
proof -
have *: "{a<..} ≠ {}"
unfolding set_eq_iff by (auto intro!: exI[of _ "a + 1"])
then show ?thesis using interior_real_atLeast interior_rel_interior_gen[of "{a..}"]
by (auto split: if_split_asm)
qed
subsubsection ‹Relative open sets›
definition "rel_open S ⟷ rel_interior S = S"
lemma rel_open: "rel_open S ⟷ openin (top_of_set (affine hull S)) S" (is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
unfolding rel_open_def rel_interior_def
using openin_subopen[of "top_of_set (affine hull S)" S] by auto
qed (auto simp: rel_open_def rel_interior_def)
lemma openin_rel_interior: "openin (top_of_set (affine hull S)) (rel_interior S)"
using openin_subopen by (fastforce simp add: rel_interior_def)
lemma openin_set_rel_interior:
"openin (top_of_set S) (rel_interior S)"
by (rule openin_subset_trans [OF openin_rel_interior rel_interior_subset hull_subset])
lemma affine_rel_open:
fixes S :: "'n::euclidean_space set"
assumes "affine S"
shows "rel_open S"
unfolding rel_open_def
using assms rel_interior_affine_hull[of S] affine_hull_eq[of S]
by metis
lemma affine_closed:
fixes S :: "'n::euclidean_space set"
assumes "affine S"
shows "closed S"
proof -
{
assume "S ≠ {}"
then obtain L where L: "subspace L" "affine_parallel S L"
using assms affine_parallel_subspace[of S] by auto
then obtain a where a: "S = ((+) a ` L)"
using affine_parallel_def[of L S] affine_parallel_commute by auto
from L have "closed L" using closed_subspace by auto
then have "closed S"
using closed_translation a by auto
}
then show ?thesis by auto
qed
lemma closure_affine_hull:
fixes S :: "'n::euclidean_space set"
shows "closure S ⊆ affine hull S"
by (intro closure_minimal hull_subset affine_closed affine_affine_hull)
lemma closed_affine_hull [iff]:
fixes S :: "'n::euclidean_space set"
shows "closed (affine hull S)"
by (metis affine_affine_hull affine_closed)
lemma closure_same_affine_hull [simp]:
fixes S :: "'n::euclidean_space set"
shows "affine hull (closure S) = affine hull S"
proof -
have "affine hull (closure S) ⊆ affine hull S"
using hull_mono[of "closure S" "affine hull S" "affine"]
closure_affine_hull[of S] hull_hull[of "affine" S]
by auto
moreover have "affine hull (closure S) ⊇ affine hull S"
using hull_mono[of "S" "closure S" "affine"] closure_subset by auto
ultimately show ?thesis by auto
qed
lemma closure_aff_dim [simp]:
fixes S :: "'n::euclidean_space set"
shows "aff_dim (closure S) = aff_dim S"
proof -
have "aff_dim S ≤ aff_dim (closure S)"
using aff_dim_subset closure_subset by auto
moreover have "aff_dim (closure S) ≤ aff_dim (affine hull S)"
using aff_dim_subset closure_affine_hull by blast
moreover have "aff_dim (affine hull S) = aff_dim S"
using aff_dim_affine_hull by auto
ultimately show ?thesis by auto
qed
lemma rel_interior_closure_convex_shrink:
fixes S :: "_::euclidean_space set"
assumes "convex S"
and "c ∈ rel_interior S"
and "x ∈ closure S"
and "e > 0"
and "e ≤ 1"
shows "x - e *⇩R (x - c) ∈ rel_interior S"
proof -
obtain d where "d > 0" and d: "ball c d ∩ affine hull S ⊆ S"
using assms(2) unfolding mem_rel_interior_ball 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› by force
next
case False
then have x: "x islimpt S"
using assms(3)[unfolded closure_def] by auto
show ?thesis
proof (cases "e = 1")
case True
obtain y where "y ∈ S" "y ≠ x" "dist y x < 1"
using x[unfolded islimpt_approachable,THEN spec[where x=1]] by auto
then show ?thesis
unfolding True using ‹d > 0› by (force simp add: )
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
unfolding dist_norm using pos_less_divide_eq[OF *] by force
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: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
have zball: "z ∈ ball c d"
using mem_ball z_def dist_norm[of c]
using y and assms(4,5)
by (simp add: norm_minus_commute) (simp add: field_simps)
have "x ∈ affine hull S"
using closure_affine_hull assms by auto
moreover have "y ∈ affine hull S"
using ‹y ∈ S› hull_subset[of S] by auto
moreover have "c ∈ affine hull S"
using assms rel_interior_subset hull_subset[of S] by auto
ultimately have "z ∈ affine hull S"
using z_def affine_affine_hull[of S]
mem_affine_3_minus [of "affine hull S" c x y "(1 - e) / e"]
assms
by simp
then have "z ∈ S" using d zball by auto
obtain d1 where "d1 > 0" and d1: "ball z d1 ≤ ball c d"
using zball open_ball[of c d] openE[of "ball c d" z] by auto
then have "ball z d1 ∩ affine hull S ⊆ ball c d ∩ affine hull S"
by auto
then have "ball z d1 ∩ affine hull S ⊆ S"
using d by auto
then have "z ∈ rel_interior S"
using mem_rel_interior_ball using ‹d1 > 0› ‹z ∈ S› by auto
then have "y - e *⇩R (y - z) ∈ rel_interior S"
using rel_interior_convex_shrink[of S z y e] assms ‹y ∈ S› by auto
then show ?thesis using * by auto
qed
lemma rel_interior_eq:
"rel_interior s = s ⟷ openin(top_of_set (affine hull s)) s"
using rel_open rel_open_def by blast
lemma rel_interior_openin:
"openin(top_of_set (affine hull s)) s ⟹ rel_interior s = s"
by (simp add: rel_interior_eq)
lemma rel_interior_affine:
fixes S :: "'n::euclidean_space set"
shows "affine S ⟹ rel_interior S = S"
using affine_rel_open rel_open_def by auto
lemma rel_interior_eq_closure:
fixes S :: "'n::euclidean_space set"
shows "rel_interior S = closure S ⟷ affine S"
proof (cases "S = {}")
case True
then show ?thesis
by auto
next
case False show ?thesis
proof
assume eq: "rel_interior S = closure S"
have "openin (top_of_set (affine hull S)) S"
by (metis eq closure_subset openin_rel_interior rel_interior_subset subset_antisym)
moreover have "closedin (top_of_set (affine hull S)) S"
by (metis closed_subset closure_subset_eq eq hull_subset rel_interior_subset)
ultimately have "S = {} ∨ S = affine hull S"
using convex_connected connected_clopen convex_affine_hull by metis
with False have "affine hull S = S"
by auto
then show "affine S"
by (metis affine_hull_eq)
next
assume "affine S"
then show "rel_interior S = closure S"
by (simp add: rel_interior_affine affine_closed)
qed
qed
subsubsection‹Relative interior preserves under linear transformations›
lemma rel_interior_translation_aux:
fixes a :: "'n::euclidean_space"
shows "((λx. a + x) ` rel_interior S) ⊆ rel_interior ((λx. a + x) ` S)"
proof -
{
fix x
assume x: "x ∈ rel_interior S"
then obtain T where "open T" "x ∈ T ∩ S" "T ∩ affine hull S ⊆ S"
using mem_rel_interior[of x S] by auto
then have "open ((λx. a + x) ` T)"
and "a + x ∈ ((λx. a + x) ` T) ∩ ((λx. a + x) ` S)"
and "((λx. a + x) ` T) ∩ affine hull ((λx. a + x) ` S) ⊆ (λx. a + x) ` S"
using affine_hull_translation[of a S] open_translation[of T a] x by auto
then have "a + x ∈ rel_interior ((λx. a + x) ` S)"
using mem_rel_interior[of "a+x" "((λx. a + x) ` S)"] by auto
}
then show ?thesis by auto
qed
lemma rel_interior_translation:
fixes a :: "'n::euclidean_space"
shows "rel_interior ((λx. a + x) ` S) = (λx. a + x) ` rel_interior S"
proof -
have "(λx. (-a) + x) ` rel_interior ((λx. a + x) ` S) ⊆ rel_interior S"
using rel_interior_translation_aux[of "-a" "(λx. a + x) ` S"]
translation_assoc[of "-a" "a"]
by auto
then have "((λx. a + x) ` rel_interior S) ⊇ rel_interior ((λx. a + x) ` S)"
using translation_inverse_subset[of a "rel_interior ((+) a ` S)" "rel_interior S"]
by auto
then show ?thesis
using rel_interior_translation_aux[of a S] by auto
qed
lemma affine_hull_linear_image:
assumes "bounded_linear f"
shows "f ` (affine hull s) = affine hull f ` s"
proof -
interpret f: bounded_linear f by fact
have "affine {x. f x ∈ affine hull f ` s}"
unfolding affine_def
by (auto simp: f.scaleR f.add affine_affine_hull[unfolded affine_def, rule_format])
moreover have "affine {x. x ∈ f ` (affine hull s)}"
using affine_affine_hull[unfolded affine_def, of s]
unfolding affine_def by (auto simp: f.scaleR [symmetric] f.add [symmetric])
ultimately show ?thesis
by (auto simp: hull_inc elim!: hull_induct)
qed
lemma rel_interior_injective_on_span_linear_image:
fixes f :: "'m::euclidean_space ⇒ 'n::euclidean_space"
and S :: "'m::euclidean_space set"
assumes "bounded_linear f"
and "inj_on f (span S)"
shows "rel_interior (f ` S) = f ` (rel_interior S)"
proof -
{
fix z
assume z: "z ∈ rel_interior (f ` S)"
then have "z ∈ f ` S"
using rel_interior_subset[of "f ` S"] by auto
then obtain x where x: "x ∈ S" "f x = z" by auto
obtain e2 where e2: "e2 > 0" "cball z e2 ∩ affine hull (f ` S) ⊆ (f ` S)"
using z rel_interior_cball[of "f ` S"] by auto
obtain K where K: "K > 0" "⋀x. norm (f x) ≤ norm x * K"
using assms Real_Vector_Spaces.bounded_linear.pos_bounded[of f] by auto
define e1 where "e1 = 1 / K"
then have e1: "e1 > 0" "⋀x. e1 * norm (f x) ≤ norm x"
using K pos_le_divide_eq[of e1] by auto
define e where "e = e1 * e2"
then have "e > 0" using e1 e2 by auto
{
fix y
assume y: "y ∈ cball x e ∩ affine hull S"
then have h1: "f y ∈ affine hull (f ` S)"
using affine_hull_linear_image[of f S] assms by auto
from y have "norm (x-y) ≤ e1 * e2"
using cball_def[of x e] dist_norm[of x y] e_def by auto
moreover have "f x - f y = f (x - y)"
using assms linear_diff[of f x y] linear_conv_bounded_linear[of f] by auto
moreover have "e1 * norm (f (x-y)) ≤ norm (x - y)"
using e1 by auto
ultimately have "e1 * norm ((f x)-(f y)) ≤ e1 * e2"
by auto
then have "f y ∈ cball z e2"
using cball_def[of "f x" e2] dist_norm[of "f x" "f y"] e1 x by auto
then have "f y ∈ f ` S"
using y e2 h1 by auto
then have "y ∈ S"
using assms y hull_subset[of S] affine_hull_subset_span
inj_on_image_mem_iff [OF ‹inj_on f (span S)›]
by (metis Int_iff span_superset subsetCE)
}
then have "z ∈ f ` (rel_interior S)"
using mem_rel_interior_cball[of x S] ‹e > 0› x by auto
}
moreover
{
fix x
assume x: "x ∈ rel_interior S"
then obtain e2 where e2: "e2 > 0" "cball x e2 ∩ affine hull S ⊆ S"
using rel_interior_cball[of S] by auto
have "x ∈ S" using x rel_interior_subset by auto
then have *: "f x ∈ f ` S" by auto
have "∀x∈span S. f x = 0 ⟶ x = 0"
using assms subspace_span linear_conv_bounded_linear[of f]
linear_injective_on_subspace_0[of f "span S"]
by auto
then obtain e1 where e1: "e1 > 0" "∀x ∈ span S. e1 * norm x ≤ norm (f x)"
using assms injective_imp_isometric[of "span S" f]
subspace_span[of S] closed_subspace[of "span S"]
by auto
define e where "e = e1 * e2"
hence "e > 0" using e1 e2 by auto
{
fix y
assume y: "y ∈ cball (f x) e ∩ affine hull (f ` S)"
then have "y ∈ f ` (affine hull S)"
using affine_hull_linear_image[of f S] assms by auto
then obtain xy where xy: "xy ∈ affine hull S" "f xy = y" by auto
with y have "norm (f x - f xy) ≤ e1 * e2"
using cball_def[of "f x" e] dist_norm[of "f x" y] e_def by auto
moreover have "f x - f xy = f (x - xy)"
using assms linear_diff[of f x xy] linear_conv_bounded_linear[of f] by auto
moreover have *: "x - xy ∈ span S"
using subspace_diff[of "span S" x xy] subspace_span ‹x ∈ S› xy
affine_hull_subset_span[of S] span_superset
by auto
moreover from * have "e1 * norm (x - xy) ≤ norm (f (x - xy))"
using e1 by auto
ultimately have "e1 * norm (x - xy) ≤ e1 * e2"
by auto
then have "xy ∈ cball x e2"
using cball_def[of x e2] dist_norm[of x xy] e1 by auto
then have "y ∈ f ` S"
using xy e2 by auto
}
then have "f x ∈ rel_interior (f ` S)"
using mem_rel_interior_cball[of "(f x)" "(f ` S)"] * ‹e > 0› by auto
}
ultimately show ?thesis by auto
qed
lemma rel_interior_injective_linear_image:
fixes f :: "'m::euclidean_space ⇒ 'n::euclidean_space"
assumes "bounded_linear f"
and "inj f"
shows "rel_interior (f ` S) = f ` (rel_interior S)"
using assms rel_interior_injective_on_span_linear_image[of f S]
subset_inj_on[of f "UNIV" "span S"]
by auto
subsection ‹Openness and compactness are preserved by convex hull operation›
lemma open_convex_hull[intro]:
fixes S :: "'a::real_normed_vector set"
assumes "open S"
shows "open (convex hull S)"
proof (clarsimp simp: open_contains_cball convex_hull_explicit)
fix T and u :: "'a⇒real"
assume obt: "finite T" "T⊆S" "∀x∈T. 0 ≤ u x" "sum u T = 1"
from assms[unfolded open_contains_cball] obtain b
where b: "⋀x. x∈S ⟹ 0 < b x ∧ cball x (b x) ⊆ S" by metis
have "b ` T ≠ {}"
using obt by auto
define i where "i = b ` T"
let ?Φ = "λy. ∃F. finite F ∧ F ⊆ S ∧ (∃u. (∀x∈F. 0 ≤ u x) ∧ sum u F = 1 ∧ (∑v∈F. u v *⇩R v) = y)"
let ?a = "∑v∈T. u v *⇩R v"
show "∃e > 0. cball ?a e ⊆ {y. ?Φ y}"
proof (intro exI subsetI conjI)
show "0 < Min i"
unfolding i_def and Min_gr_iff[OF finite_imageI[OF obt(1)] ‹b ` T≠{}›]
using b ‹T⊆S› by auto
next
fix y
assume "y ∈ cball ?a (Min i)"
then have y: "norm (?a - y) ≤ Min i"
unfolding dist_norm[symmetric] by auto
{ fix x
assume "x ∈ T"
then have "Min i ≤ b x"
by (simp add: i_def obt(1))
then have "x + (y - ?a) ∈ cball x (b x)"
using y unfolding mem_cball dist_norm by auto
moreover have "x ∈ S"
using ‹x∈T› ‹T⊆S› by auto
ultimately have "x + (y - ?a) ∈ S"
using y b by blast
}
moreover
have *: "inj_on (λv. v + (y - ?a)) T"
unfolding inj_on_def by auto
have "(∑v∈(λv. v + (y - ?a)) ` T. u (v - (y - ?a)) *⇩R v) = y"
unfolding sum.reindex[OF *] o_def using obt(4)
by (simp add: sum.distrib sum_subtractf scaleR_left.sum[symmetric] scaleR_right_distrib)
ultimately show "y ∈ {y. ?Φ y}"
proof (intro CollectI exI conjI)
show "finite ((λv. v + (y - ?a)) ` T)"
by (simp add: obt(1))
show "sum (λv. u (v - (y - ?a))) ((λv. v + (y - ?a)) ` T) = 1"
unfolding sum.reindex[OF *] o_def using obt(4) by auto
qed (use obt(1, 3) in auto)
qed
qed
lemma compact_convex_combinations:
fixes S T :: "'a::real_normed_vector set"
assumes "compact S" "compact T"
shows "compact { (1 - u) *⇩R x + u *⇩R y | x y u. 0 ≤ u ∧ u ≤ 1 ∧ x ∈ S ∧ y ∈ T}"
proof -
let ?X = "{0..1} × S × T"
let ?h = "(λz. (1 - fst z) *⇩R fst (snd z) + fst z *⇩R snd (snd z))"
have *: "{ (1 - u) *⇩R x + u *⇩R y | x y u. 0 ≤ u ∧ u ≤ 1 ∧ x ∈ S ∧ y ∈ T} = ?h ` ?X"
by force
have "continuous_on ?X (λz. (1 - fst z) *⇩R fst (snd z) + fst z *⇩R snd (snd z))"
unfolding continuous_on by (rule ballI) (intro tendsto_intros)
with assms show ?thesis
by (simp add: * compact_Times compact_continuous_image)
qed
lemma finite_imp_compact_convex_hull:
fixes S :: "'a::real_normed_vector set"
assumes "finite S"
shows "compact (convex hull S)"
proof (cases "S = {}")
case True
then show ?thesis by simp
next
case False
with assms show ?thesis
proof (induct rule: finite_ne_induct)
case (singleton x)
show ?case by simp
next
case (insert x A)
let ?f = "λ(u, y::'a). u *⇩R x + (1 - u) *⇩R y"
let ?T = "{0..1::real} × (convex hull A)"
have "continuous_on ?T ?f"
unfolding split_def continuous_on by (intro ballI tendsto_intros)
moreover have "compact ?T"
by (intro compact_Times compact_Icc insert)
ultimately have "compact (?f ` ?T)"
by (rule compact_continuous_image)
also have "?f ` ?T = convex hull (insert x A)"
unfolding convex_hull_insert [OF ‹A ≠ {}›]
apply safe
apply (rule_tac x=a in exI, simp)
apply (rule_tac x="1 - a" in exI, simp, fast)
apply (rule_tac x="(u, b)" in image_eqI, simp_all)
done
finally show "compact (convex hull (insert x A))" .
qed
qed
lemma compact_convex_hull:
fixes S :: "'a::euclidean_space set"
assumes "compact S"
shows "compact (convex hull S)"
proof (cases "S = {}")
case True
then show ?thesis using compact_empty by simp
next
case False
then obtain w where "w ∈ S" by auto
show ?thesis
unfolding caratheodory[of S]
proof (induct ("DIM('a) + 1"))
case 0
have *: "{x.∃sa. finite sa ∧ sa ⊆ S ∧ card sa ≤ 0 ∧ x ∈ convex hull sa} = {}"
using compact_empty by auto
from 0 show ?case unfolding * by simp
next
case (Suc n)
show ?case
proof (cases "n = 0")
case True
have "{x. ∃T. finite T ∧ T ⊆ S ∧ card T ≤ Suc n ∧ x ∈ convex hull T} = S"
unfolding set_eq_iff and mem_Collect_eq
proof (rule, rule)
fix x
assume "∃T. finite T ∧ T ⊆ S ∧ card T ≤ Suc n ∧ x ∈ convex hull T"
then obtain T where T: "finite T" "T ⊆ S" "card T ≤ Suc n" "x ∈ convex hull T"
by auto
show "x ∈ S"
proof (cases "card T = 0")
case True
then show ?thesis
using T(4) unfolding card_0_eq[OF T(1)] by simp
next
case False
then have "card T = Suc 0" using T(3) ‹n=0› by auto
then obtain a where "T = {a}" unfolding card_Suc_eq by auto
then show ?thesis using T(2,4) by simp
qed
next
fix x assume "x∈S"
then show "∃T. finite T ∧ T ⊆ S ∧ card T ≤ Suc n ∧ x ∈ convex hull T"
by (rule_tac x="{x}" in exI) (use convex_hull_singleton in auto)
qed
then show ?thesis using assms by simp
next
case False
have "{x. ∃T. finite T ∧ T ⊆ S ∧ card T ≤ Suc n ∧ x ∈ convex hull T} =
{(1 - u) *⇩R x + u *⇩R y | x y u.
0 ≤ u ∧ u ≤ 1 ∧ x ∈ S ∧ y ∈ {x. ∃T. finite T ∧ T ⊆ S ∧ card T ≤ n ∧ x ∈ convex hull T}}"
unfolding set_eq_iff and mem_Collect_eq
proof (rule, rule)
fix x
assume "∃u v c. x = (1 - c) *⇩R u + c *⇩R v ∧
0 ≤ c ∧ c ≤ 1 ∧ u ∈ S ∧ (∃T. finite T ∧ T ⊆ S ∧ card T ≤ n ∧ v ∈ convex hull T)"
then obtain u v c T where obt: "x = (1 - c) *⇩R u + c *⇩R v"
"0 ≤ c ∧ c ≤ 1" "u ∈ S" "finite T" "T ⊆ S" "card T ≤ n" "v ∈ convex hull T"
by auto
moreover have "(1 - c) *⇩R u + c *⇩R v ∈ convex hull insert u T"
by (meson convexD_alt convex_convex_hull hull_inc hull_mono in_mono insertCI obt(2) obt(7) subset_insertI)
ultimately show "∃T. finite T ∧ T ⊆ S ∧ card T ≤ Suc n ∧ x ∈ convex hull T"
by (rule_tac x="insert u T" in exI) (auto simp: card_insert_if)
next
fix x
assume "∃T. finite T ∧ T ⊆ S ∧ card T ≤ Suc n ∧ x ∈ convex hull T"
then obtain T where T: "finite T" "T ⊆ S" "card T ≤ Suc n" "x ∈ convex hull T"
by auto
show "∃u v c. x = (1 - c) *⇩R u + c *⇩R v ∧
0 ≤ c ∧ c ≤ 1 ∧ u ∈ S ∧ (∃T. finite T ∧ T ⊆ S ∧ card T ≤ n ∧ v ∈ convex hull T)"
proof (cases "card T = Suc n")
case False
then have "card T ≤ n" using T(3) by auto
then show ?thesis
using ‹w∈S› and T
by (rule_tac x=w in exI, rule_tac x=x in exI, rule_tac x=1 in exI) auto
next
case True
then obtain a u where au: "T = insert a u" "a∉u"
by (metis card_le_Suc_iff order_refl)
show ?thesis
proof (cases "u = {}")
case True
then have "x = a" using T(4)[unfolded au] by auto
show ?thesis unfolding ‹x = a›
using T ‹n ≠ 0› unfolding au
by (rule_tac x=a in exI, rule_tac x=a in exI, rule_tac x=1 in exI) force
next
case False
obtain ux vx b where obt: "ux≥0" "vx≥0" "ux + vx = 1"
"b ∈ convex hull u" "x = ux *⇩R a + vx *⇩R b"
using T(4)[unfolded au convex_hull_insert[OF False]]
by auto
have *: "1 - vx = ux" using obt(3) by auto
show ?thesis
using obt T(1-3) card_insert_disjoint[OF _ au(2)] unfolding au *
by (rule_tac x=a in exI, rule_tac x=b in exI, rule_tac x=vx in exI) force
qed
qed
qed
then show ?thesis
using compact_convex_combinations[OF assms Suc] by simp
qed
qed
qed
subsection ‹Extremal points of a simplex are some vertices›
lemma dist_increases_online:
fixes a b d :: "'a::real_inner"
assumes "d ≠ 0"
shows "dist a (b + d) > dist a b ∨ dist a (b - d) > dist a b"
proof (cases "inner a d - inner b d > 0")
case True
then have "0 < inner d d + (inner a d * 2 - inner b d * 2)"
using assms
by (intro add_pos_pos) auto
then show ?thesis
unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff
by (simp add: algebra_simps inner_commute)
next
case False
then have "0 < inner d d + (inner b d * 2 - inner a d * 2)"
using assms
by (intro add_pos_nonneg) auto
then show ?thesis
unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff
by (simp add: algebra_simps inner_commute)
qed
lemma norm_increases_online:
fixes d :: "'a::real_inner"
shows "d ≠ 0 ⟹ norm (a + d) > norm a ∨ norm(a - d) > norm a"
using dist_increases_online[of d a 0] unfolding dist_norm by auto
lemma simplex_furthest_lt:
fixes S :: "'a::real_inner set"
assumes "finite S"
shows "∀x ∈ convex hull S. x ∉ S ⟶ (∃y ∈ convex hull S. norm (x - a) < norm(y - a))"
using assms
proof induct
fix x S
assume as: "finite S" "x∉S" "∀x∈convex hull S. x ∉ S ⟶ (∃y∈convex hull S. norm (x - a) < norm (y - a))"
show "∀xa∈convex hull insert x S. xa ∉ insert x S ⟶
(∃y∈convex hull insert x S. norm (xa - a) < norm (y - a))"
proof (intro impI ballI, cases "S = {}")
case False
fix y
assume y: "y ∈ convex hull insert x S" "y ∉ insert x S"
obtain u v b where obt: "u≥0" "v≥0" "u + v = 1" "b ∈ convex hull S" "y = u *⇩R x + v *⇩R b"
using y(1)[unfolded convex_hull_insert[OF False]] by auto
show "∃z∈convex hull insert x S. norm (y - a) < norm (z - a)"
proof (cases "y ∈ convex hull S")
case True
then obtain z where "z ∈ convex hull S" "norm (y - a) < norm (z - a)"
using as(3)[THEN bspec[where x=y]] and y(2) by auto
then show ?thesis
by (meson hull_mono subsetD subset_insertI)
next
case False
show ?thesis
proof (cases "u = 0 ∨ v = 0")
case True
with False show ?thesis
using obt y by auto
next
case False
then obtain w where w: "w>0" "w<u" "w<v"
using field_lbound_gt_zero[of u v] and obt(1,2) by auto
have "x ≠ b"
proof
assume "x = b"
then have "y = b" unfolding obt(5)
using obt(3) by (auto simp: scaleR_left_distrib[symmetric])
then show False using obt(4) and False
using ‹x = b› y(2) by blast
qed
then have *: "w *⇩R (x - b) ≠ 0" using w(1) by auto
show ?thesis
using dist_increases_online[OF *, of a y]
proof (elim disjE)
assume "dist a y < dist a (y + w *⇩R (x - b))"
then have "norm (y - a) < norm ((u + w) *⇩R x + (v - w) *⇩R b - a)"
unfolding dist_commute[of a]
unfolding dist_norm obt(5)
by (simp add: algebra_simps)
moreover have "(u + w) *⇩R x + (v - w) *⇩R b ∈ convex hull insert x S"
unfolding convex_hull_insert[OF ‹S≠{}›]
proof (intro CollectI conjI exI)
show "u + w ≥ 0" "v - w ≥ 0"
using obt(1) w by auto
qed (use obt in auto)
ultimately show ?thesis by auto
next
assume "dist a y < dist a (y - w *⇩R (x - b))"
then have "norm (y - a) < norm ((u - w) *⇩R x + (v + w) *⇩R b - a)"
unfolding dist_commute[of a]
unfolding dist_norm obt(5)
by (simp add: algebra_simps)
moreover have "(u - w) *⇩R x + (v + w) *⇩R b ∈ convex hull insert x S"
unfolding convex_hull_insert[OF ‹S≠{}›]
proof (intro CollectI conjI exI)
show "u - w ≥ 0" "v + w ≥ 0"
using obt(1) w by auto
qed (use obt in auto)
ultimately show ?thesis by auto
qed
qed
qed
qed auto
qed (auto simp: assms)
lemma simplex_furthest_le:
fixes S :: "'a::real_inner set"
assumes "finite S"
and "S ≠ {}"
shows "∃y∈S. ∀x∈ convex hull S. norm (x - a) ≤ norm (y - a)"
proof -
have "convex hull S ≠ {}"
using hull_subset[of S convex] and assms(2) by auto
then obtain x where x: "x ∈ convex hull S" "∀y∈convex hull S. norm (y - a) ≤ norm (x - a)"
using distance_attains_sup[OF finite_imp_compact_convex_hull[OF ‹finite S›], of a]
unfolding dist_commute[of a]
unfolding dist_norm
by auto
show ?thesis
proof (cases "x ∈ S")
case False
then obtain y where "y ∈ convex hull S" "norm (x - a) < norm (y - a)"
using simplex_furthest_lt[OF assms(1), THEN bspec[where x=x]] and x(1)
by auto
then show ?thesis
using x(2)[THEN bspec[where x=y]] by auto
next
case True
with x show ?thesis by auto
qed
qed
lemma simplex_furthest_le_exists:
fixes S :: "('a::real_inner) set"
shows "finite S ⟹ ∀x∈(convex hull S). ∃y∈S. norm (x - a) ≤ norm (y - a)"
using simplex_furthest_le[of S] by (cases "S = {}") auto
lemma simplex_extremal_le:
fixes S :: "'a::real_inner set"
assumes "finite S"
and "S ≠ {}"
shows "∃u∈S. ∃v∈S. ∀x∈convex hull S. ∀y ∈ convex hull S. norm (x - y) ≤ norm (u - v)"
proof -
have "convex hull S ≠ {}"
using hull_subset[of S convex] and assms(2) by auto
then obtain u v where obt: "u ∈ convex hull S" "v ∈ convex hull S"
"∀x∈convex hull S. ∀y∈convex hull S. norm (x - y) ≤ norm (u - v)"
using compact_sup_maxdistance[OF finite_imp_compact_convex_hull[OF assms(1)]]
by (auto simp: dist_norm)
then show ?thesis
proof (cases "u∉S ∨ v∉S", elim disjE)
assume "u ∉ S"
then obtain y where "y ∈ convex hull S" "norm (u - v) < norm (y - v)"
using simplex_furthest_lt[OF assms(1), THEN bspec[where x=u]] and obt(1)
by auto
then show ?thesis
using obt(3)[THEN bspec[where x=y], THEN bspec[where x=v]] and obt(2)
by auto
next
assume "v ∉ S"
then obtain y where "y ∈ convex hull S" "norm (v - u) < norm (y - u)"
using simplex_furthest_lt[OF assms(1), THEN bspec[where x=v]] and obt(2)
by auto
then show ?thesis
using obt(3)[THEN bspec[where x=u], THEN bspec[where x=y]] and obt(1)
by (auto simp: norm_minus_commute)
qed auto
qed
lemma simplex_extremal_le_exists:
fixes S :: "'a::real_inner set"
shows "finite S ⟹ x ∈ convex hull S ⟹ y ∈ convex hull S ⟹
∃u∈S. ∃v∈S. norm (x - y) ≤ norm (u - v)"
using convex_hull_empty simplex_extremal_le[of S]
by(cases "S = {}") auto
subsection ‹Closest point of a convex set is unique, with a continuous projection›
definition closest_point :: "'a::{real_inner,heine_borel} set ⇒ 'a ⇒ 'a"
where "closest_point S a = (SOME x. x ∈ S ∧ (∀y∈S. dist a x ≤ dist a y))"
lemma closest_point_exists:
assumes "closed S"
and "S ≠ {}"
shows closest_point_in_set: "closest_point S a ∈ S"
and "∀y∈S. dist a (closest_point S a) ≤ dist a y"
unfolding closest_point_def
by (rule_tac someI2_ex, auto intro: distance_attains_inf[OF assms(1,2), of a])+
lemma closest_point_le: "closed S ⟹ x ∈ S ⟹ dist a (closest_point S a) ≤ dist a x"
using closest_point_exists[of S] by auto
lemma closest_point_self:
assumes "x ∈ S"
shows "closest_point S x = x"
unfolding closest_point_def
by (rule some1_equality, rule ex1I[of _ x]) (use assms in auto)
lemma closest_point_refl: "closed S ⟹ S ≠ {} ⟹ closest_point S x = x ⟷ x ∈ S"
using closest_point_in_set[of S x] closest_point_self[of x S]
by auto
lemma closer_points_lemma:
assumes "inner y z > 0"
shows "∃u>0. ∀v>0. v ≤ u ⟶ norm(v *⇩R z - y) < norm y"
proof -
have z: "inner z z > 0"
unfolding inner_gt_zero_iff using assms by auto
have "norm (v *⇩R z - y) < norm y"
if "0 < v" and "v ≤ inner y z / inner z z" for v
unfolding norm_lt using z assms that
by (simp add: field_simps inner_diff inner_commute mult_strict_left_mono[OF _ ‹0<v›])
then show ?thesis
using assms z
by (rule_tac x = "inner y z / inner z z" in exI) auto
qed
lemma closer_point_lemma:
assumes "inner (y - x) (z - x) > 0"
shows "∃u>0. u ≤ 1 ∧ dist (x + u *⇩R (z - x)) y < dist x y"
proof -
obtain u where "u > 0"
and u: "⋀v. ⟦0<v; v ≤ u⟧ ⟹ norm (v *⇩R (z - x) - (y - x)) < norm (y - x)"
using closer_points_lemma[OF assms] by auto
show ?thesis
using u[of "min u 1"] and ‹u > 0›
by (metis diff_diff_add dist_commute dist_norm less_eq_real_def not_less u zero_less_one)
qed
lemma any_closest_point_dot:
assumes "convex S" "closed S" "x ∈ S" "y ∈ S" "∀z∈S. dist a x ≤ dist a z"
shows "inner (a - x) (y - x) ≤ 0"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain u where u: "u>0" "u≤1" "dist (x + u *⇩R (y - x)) a < dist x a"
using closer_point_lemma[of a x y] by auto
let ?z = "(1 - u) *⇩R x + u *⇩R y"
have "?z ∈ S"
using convexD_alt[OF assms(1,3,4), of u] using u by auto
then show False
using assms(5)[THEN bspec[where x="?z"]] and u(3)
by (auto simp: dist_commute algebra_simps)
qed
lemma any_closest_point_unique:
fixes x :: "'a::real_inner"
assumes "convex S" "closed S" "x ∈ S" "y ∈ S"
"∀z∈S. dist a x ≤ dist a z" "∀z∈S. dist a y ≤ dist a z"
shows "x = y"
using any_closest_point_dot[OF assms(1-4,5)] and any_closest_point_dot[OF assms(1-2,4,3,6)]
unfolding norm_pths(1) and norm_le_square
by (auto simp: algebra_simps)
lemma closest_point_unique:
assumes "convex S" "closed S" "x ∈ S" "∀z∈S. dist a x ≤ dist a z"
shows "x = closest_point S a"
using any_closest_point_unique[OF assms(1-3) _ assms(4), of "closest_point S a"]
using closest_point_exists[OF assms(2)] and assms(3) by auto
lemma closest_point_dot:
assumes "convex S" "closed S" "x ∈ S"
shows "inner (a - closest_point S a) (x - closest_point S a) ≤ 0"
using any_closest_point_dot[OF assms(1,2) _ assms(3)]
by (metis assms(2) assms(3) closest_point_in_set closest_point_le empty_iff)
lemma closest_point_lt:
assumes "convex S" "closed S" "x ∈ S" "x ≠ closest_point S a"
shows "dist a (closest_point S a) < dist a x"
using closest_point_unique[where a=a] closest_point_le[where a=a] assms by fastforce
lemma setdist_closest_point:
"⟦closed S; S ≠ {}⟧ ⟹ setdist {a} S = dist a (closest_point S a)"
by (metis closest_point_exists(2) closest_point_in_set emptyE insert_iff setdist_unique)
lemma closest_point_lipschitz:
assumes "convex S"
and "closed S" "S ≠ {}"
shows "dist (closest_point S x) (closest_point S y) ≤ dist x y"
proof -
have "inner (x - closest_point S x) (closest_point S y - closest_point S x) ≤ 0"
and "inner (y - closest_point S y) (closest_point S x - closest_point S y) ≤ 0"
by (simp_all add: assms closest_point_dot closest_point_in_set)
then show ?thesis unfolding dist_norm and norm_le
using inner_ge_zero[of "(x - closest_point S x) - (y - closest_point S y)"]
by (simp add: inner_add inner_diff inner_commute)
qed
lemma continuous_at_closest_point:
assumes "convex S"
and "closed S"
and "S ≠ {}"
shows "continuous (at x) (closest_point S)"
unfolding continuous_at_eps_delta
using le_less_trans[OF closest_point_lipschitz[OF assms]] by auto
lemma continuous_on_closest_point:
assumes "convex S"
and "closed S"
and "S ≠ {}"
shows "continuous_on t (closest_point S)"
by (metis continuous_at_imp_continuous_on continuous_at_closest_point[OF assms])
proposition closest_point_in_rel_interior:
assumes "closed S" "S ≠ {}" and x: "x ∈ affine hull S"
shows "closest_point S x ∈ rel_interior S ⟷ x ∈ rel_interior S"
proof (cases "x ∈ S")
case True
then show ?thesis
by (simp add: closest_point_self)
next
case False
then have "False" if asm: "closest_point S x ∈ rel_interior S"
proof -
obtain e where "e > 0" and clox: "closest_point S x ∈ S"
and e: "cball (closest_point S x) e ∩ affine hull S ⊆ S"
using asm mem_rel_interior_cball by blast
then have clo_notx: "closest_point S x ≠ x"
using ‹x ∉ S› by auto
define y where "y ≡ closest_point S x -
(min 1 (e / norm(closest_point S x - x))) *⇩R (closest_point S x - x)"
have "x - y = (1 - min 1 (e / norm (closest_point S x - x))) *⇩R (x - closest_point S x)"
by (simp add: y_def algebra_simps)
then have "norm (x - y) = abs ((1 - min 1 (e / norm (closest_point S x - x)))) * norm(x - closest_point S x)"
by simp
also have "… < norm(x - closest_point S x)"
using clo_notx ‹e > 0›
by (auto simp: mult_less_cancel_right2 field_split_simps)
finally have no_less: "norm (x - y) < norm (x - closest_point S x)" .
have "y ∈ affine hull S"
unfolding y_def
by (meson affine_affine_hull clox hull_subset mem_affine_3_minus2 subsetD x)
moreover have "dist (closest_point S x) y ≤ e"
using ‹e > 0› by (auto simp: y_def min_mult_distrib_right)
ultimately have "y ∈ S"
using subsetD [OF e] by simp
then have "dist x (closest_point S x) ≤ dist x y"
by (simp add: closest_point_le ‹closed S›)
with no_less show False
by (simp add: dist_norm)
qed
moreover have "x ∉ rel_interior S"
using rel_interior_subset False by blast
ultimately show ?thesis by blast
qed
subsubsection ‹Various point-to-set separating/supporting hyperplane theorems›
lemma supporting_hyperplane_closed_point:
fixes z :: "'a::{real_inner,heine_borel}"
assumes "convex S"
and "closed S"
and "S ≠ {}"
and "z ∉ S"
shows "∃a b. ∃y∈S. inner a z < b ∧ inner a y = b ∧ (∀x∈S. inner a x ≥ b)"
proof -
obtain y where "y ∈ S" and y: "∀x∈S. dist z y ≤ dist z x"
by (metis distance_attains_inf[OF assms(2-3)])
show ?thesis
proof (intro exI bexI conjI ballI)
show "(y - z) ∙ z < (y - z) ∙ y"
by (metis ‹y ∈ S› assms(4) diff_gt_0_iff_gt inner_commute inner_diff_left inner_gt_zero_iff right_minus_eq)
show "(y - z) ∙ y ≤ (y - z) ∙ x" if "x ∈ S" for x
proof (rule ccontr)
have *: "⋀u. 0 ≤ u ∧ u ≤ 1 ⟶ dist z y ≤ dist z ((1 - u) *⇩R y + u *⇩R x)"
using assms(1)[unfolded convex_alt] and y and ‹x∈S› and ‹y∈S› by auto
assume "¬ (y - z) ∙ y ≤ (y - z) ∙ x"
then obtain v where "v > 0" "v ≤ 1" "dist (y + v *⇩R (x - y)) z < dist y z"
using closer_point_lemma[of z y x] by (auto simp: inner_diff)
then show False
using *[of v] by (auto simp: dist_commute algebra_simps)
qed
qed (use ‹y ∈ S› in auto)
qed
lemma separating_hyperplane_closed_point:
fixes z :: "'a::{real_inner,heine_borel}"
assumes "convex S"
and "closed S"
and "z ∉ S"
shows "∃a b. inner a z < b ∧ (∀x∈S. inner a x > b)"
proof (cases "S = {}")
case True
then show ?thesis
by (simp add: gt_ex)
next
case False
obtain y where "y ∈ S" and y: "⋀x. x ∈ S ⟹ dist z y ≤ dist z x"
by (metis distance_attains_inf[OF assms(2) False])
show ?thesis
proof (intro exI conjI ballI)
show "(y - z) ∙ z < inner (y - z) z + (norm (y - z))⇧2 / 2"
using ‹y∈S› ‹z∉S› by auto
next
fix x
assume "x ∈ S"
have "False" if *: "0 < inner (z - y) (x - y)"
proof -
obtain u where "u > 0" "u ≤ 1" "dist (y + u *⇩R (x - y)) z < dist y z"
using * closer_point_lemma by blast
then show False using y[of "y + u *⇩R (x - y)"] convexD_alt [OF ‹convex S›]
using ‹x∈S› ‹y∈S› by (auto simp: dist_commute algebra_simps)
qed
moreover have "0 < (norm (y - z))⇧2"
using ‹y∈S› ‹z∉S› by auto
then have "0 < inner (y - z) (y - z)"
unfolding power2_norm_eq_inner by simp
ultimately show "(y - z) ∙ z + (norm (y - z))⇧2 / 2 < (y - z) ∙ x"
by (force simp: field_simps power2_norm_eq_inner inner_commute inner_diff)
qed
qed
lemma separating_hyperplane_closed_0:
assumes "convex (S::('a::euclidean_space) set)"
and "closed S"
and "0 ∉ S"
shows "∃a b. a ≠ 0 ∧ 0 < b ∧ (∀x∈S. inner a x > b)"
proof (cases "S = {}")
case True
have "(SOME i. i∈Basis) ≠ (0::'a)"
by (metis Basis_zero SOME_Basis)
then show ?thesis
using True zero_less_one by blast
next
case False
then show ?thesis
using False using separating_hyperplane_closed_point[OF assms]
by (metis all_not_in_conv inner_zero_left inner_zero_right less_eq_real_def not_le)
qed
subsubsection ‹Now set-to-set for closed/compact sets›
lemma separating_hyperplane_closed_compact:
fixes S :: "'a::euclidean_space set"
assumes "convex S"
and "closed S"
and "convex T"
and "compact T"
and "T ≠ {}"
and "S ∩ T = {}"
shows "∃a b. (∀x∈S. inner a x < b) ∧ (∀x∈T. inner a x > b)"
proof (cases "S = {}")
case True
obtain b where b: "b > 0" "∀x∈T. norm x ≤ b"
using compact_imp_bounded[OF assms(4)] unfolding bounded_pos by auto
obtain z :: 'a where z: "norm z = b + 1"
using vector_choose_size[of "b + 1"] and b(1) by auto
then have "z ∉ T" using b(2)[THEN bspec[where x=z]] by auto
then obtain a b where ab: "inner a z < b" "∀x∈T. b < inner a x"
using separating_hyperplane_closed_point[OF assms(3) compact_imp_closed[OF assms(4)], of z]
by auto
then show ?thesis
using True by auto
next
case False
then obtain y where "y ∈ S" by auto
obtain a b where "0 < b" and §: "⋀x. x ∈ (⋃x∈ S. ⋃y ∈ T. {x - y}) ⟹ b < inner a x"
using separating_hyperplane_closed_point[OF convex_differences[OF assms(1,3)], of 0]
using closed_compact_differences assms by fastforce
have ab: "b + inner a y < inner a x" if "x∈S" "y∈T" for x y
using § [of "x-y"] that by (auto simp add: inner_diff_right less_diff_eq)
define k where "k = (SUP x∈T. a ∙ x)"
have "k + b / 2 < a ∙ x" if "x ∈ S" for x
proof -
have "k ≤ inner a x - b"
unfolding k_def
using ‹T ≠ {}› ab that by (fastforce intro: cSUP_least)
then show ?thesis
using ‹0 < b› by auto
qed
moreover
have "- (k + b / 2) < - a ∙ x" if "x ∈ T" for x
proof -
have "inner a x - b / 2 < k"
unfolding k_def
proof (subst less_cSUP_iff)
show "T ≠ {}" by fact
show "bdd_above ((∙) a ` T)"
using ab[rule_format, of y] ‹y ∈ S›
by (intro bdd_aboveI2[where M="inner a y - b"]) (auto simp: field_simps intro: less_imp_le)
show "∃y∈T. a ∙ x - b / 2 < a ∙ y"
using ‹0 < b› that by force
qed
then show ?thesis
by auto
qed
ultimately show ?thesis
by (metis inner_minus_left neg_less_iff_less)
qed
lemma separating_hyperplane_compact_closed:
fixes S :: "'a::euclidean_space set"
assumes "convex S"
and "compact S"
and "S ≠ {}"
and "convex T"
and "closed T"
and "S ∩ T = {}"
shows "∃a b. (∀x∈S. inner a x < b) ∧ (∀x∈T. inner a x > b)"
proof -
obtain a b where "(∀x∈T. inner a x < b) ∧ (∀x∈S. b < inner a x)"
by (metis disjoint_iff_not_equal separating_hyperplane_closed_compact assms)
then show ?thesis
by (metis inner_minus_left neg_less_iff_less)
qed
subsubsection ‹General case without assuming closure and getting non-strict separation›
lemma separating_hyperplane_set_0:
assumes "convex S" "(0::'a::euclidean_space) ∉ S"
shows "∃a. a ≠ 0 ∧ (∀x∈S. 0 ≤ inner a x)"
proof -
let ?k = "λc. {x::'a. 0 ≤ inner c x}"
have *: "frontier (cball 0 1) ∩ ⋂f ≠ {}" if as: "f ⊆ ?k ` S" "finite f" for f
proof -
obtain c where c: "f = ?k ` c" "c ⊆ S" "finite c"
using finite_subset_image[OF as(2,1)] by auto
then obtain a b where ab: "a ≠ 0" "0 < b" "∀x∈convex hull c. b < inner a x"
using separating_hyperplane_closed_0[OF convex_convex_hull, of c]
using finite_imp_compact_convex_hull[OF c(3), THEN compact_imp_closed] and assms(2)
using subset_hull[of convex, OF assms(1), symmetric, of c]
by force
have "norm (a /⇩R norm a) = 1"
by (simp add: ab(1))
moreover have "(∀y∈c. 0 ≤ y ∙ (a /⇩R norm a))"
using hull_subset[of c convex] ab by (force simp: inner_commute)
ultimately have "∃x. norm x = 1 ∧ (∀y∈c. 0 ≤ inner y x)"
by blast
then show "frontier (cball 0 1) ∩ ⋂f ≠ {}"
unfolding c(1) frontier_cball sphere_def dist_norm by auto
qed
have "frontier (cball 0 1) ∩ (⋂(?k ` S)) ≠ {}"
by (rule compact_imp_fip) (use * closed_halfspace_ge in auto)
then obtain x where "norm x = 1" "∀y∈S. x∈?k y"
unfolding frontier_cball dist_norm sphere_def by auto
then show ?thesis
by (metis inner_commute mem_Collect_eq norm_eq_zero zero_neq_one)
qed
lemma separating_hyperplane_sets:
fixes S T :: "'a::euclidean_space set"
assumes "convex S"
and "convex T"
and "S ≠ {}"
and "T ≠ {}"
and "S ∩ T = {}"
shows "∃a b. a ≠ 0 ∧ (∀x∈S. inner a x ≤ b) ∧ (∀x∈T. inner a x ≥ b)"
proof -
from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
obtain a where "a ≠ 0" "∀x∈{x - y |x y. x ∈ T ∧ y ∈ S}. 0 ≤ inner a x"
using assms(3-5) by force
then have *: "⋀x y. x ∈ T ⟹ y ∈ S ⟹ inner a y ≤ inner a x"
by (force simp: inner_diff)
then have bdd: "bdd_above (((∙) a)`S)"
using ‹T ≠ {}› by (auto intro: bdd_aboveI2[OF *])
show ?thesis
using ‹a≠0›
by (intro exI[of _ a] exI[of _ "SUP x∈S. a ∙ x"])
(auto intro!: cSUP_upper bdd cSUP_least ‹a ≠ 0› ‹S ≠ {}› *)
qed
subsection ‹More convexity generalities›
lemma convex_closure [intro,simp]:
fixes S :: "'a::real_normed_vector set"
assumes "convex S"
shows "convex (closure S)"
apply (rule convexI)
unfolding closure_sequential
apply (elim exE)
subgoal for x y u v f g
by (rule_tac x="λn. u *⇩R f n + v *⇩R g n" in exI) (force intro: tendsto_intros dest: convexD [OF assms])
done
lemma convex_interior [intro,simp]:
fixes S :: "'a::real_normed_vector set"
assumes "convex S"
shows "convex (interior S)"
unfolding convex_alt Ball_def mem_interior
proof clarify
fix x y u
assume u: "0 ≤ u" "u ≤ (1::real)"
fix e d
assume ed: "ball x e ⊆ S" "ball y d ⊆ S" "0<d" "0<e"
show "∃e>0. ball ((1 - u) *⇩R x + u *⇩R y) e ⊆ S"
proof (intro exI conjI subsetI)
fix z
assume z: "z ∈ ball ((1 - u) *⇩R x + u *⇩R y) (min d e)"
have "(1- u) *⇩R (z - u *⇩R (y - x)) + u *⇩R (z + (1 - u) *⇩R (y - x)) ∈ S"
proof (rule_tac assms[unfolded convex_alt, rule_format])
show "z - u *⇩R (y - x) ∈ S" "z + (1 - u) *⇩R (y - x) ∈ S"
using ed z u by (auto simp add: algebra_simps dist_norm)
qed (use u in auto)
then show "z ∈ S"
using u by (auto simp: algebra_simps)
qed(use u ed in auto)
qed
lemma convex_hull_eq_empty[simp]: "convex hull S = {} ⟷ S = {}"
using hull_subset[of S convex] convex_hull_empty by auto
subsection ‹Convex set as intersection of halfspaces›
lemma convex_halfspace_intersection:
fixes S :: "('a::euclidean_space) set"
assumes "closed S" "convex S"
shows "S = ⋂{h. S ⊆ h ∧ (∃a b. h = {x. inner a x ≤ b})}"
proof -
{ fix z
assume "∀T. S ⊆ T ∧ (∃a b. T = {x. inner a x ≤ b}) ⟶ z ∈ T" "z ∉ S"
then have §: "⋀a b. S ⊆ {x. inner a x ≤ b} ⟹ z ∈ {x. inner a x ≤ b}"
by blast
obtain a b where "inner a z < b" "(∀x∈S. inner a x > b)"
using ‹z ∉ S› assms separating_hyperplane_closed_point by blast
then have False
using § [of "-a" "-b"] by fastforce
}
then show ?thesis
by force
qed
subsection ‹Convexity of general and special intervals›
lemma is_interval_convex:
fixes S :: "'a::euclidean_space set"
assumes "is_interval S"
shows "convex S"
proof (rule convexI)
fix x y and u v :: real
assume "x ∈ S" "y ∈ S" and uv: "0 ≤ u" "0 ≤ v" "u + v = 1"
then have *: "u = 1 - v" "1 - v ≥ 0" and **: "v = 1 - u" "1 - u ≥ 0"
by auto
{
fix a b
assume "¬ b ≤ u * a + v * b"
then have "u * a < (1 - v) * b"
unfolding not_le using ‹0 ≤ v›by (auto simp: field_simps)
then have "a < b"
using "*"(1) less_eq_real_def uv(1) by auto
then have "a ≤ u * a + v * b"
unfolding * using ‹0 ≤ v›
by (auto simp: field_simps intro!:mult_right_mono)
}
moreover
{
fix a b
assume "¬ u * a + v * b ≤ a"
then have "v * b > (1 - u) * a"
unfolding not_le using ‹0 ≤ v› by (auto simp: field_simps)
then have "a < b"
unfolding * using ‹0 ≤ v›
by (rule_tac mult_left_less_imp_less) (auto simp: field_simps)
then have "u * a + v * b ≤ b"
unfolding **
using **(2) ‹0 ≤ u› by (auto simp: algebra_simps mult_right_mono)
}
ultimately show "u *⇩R x + v *⇩R y ∈ S"
using DIM_positive[where 'a='a]
by (intro mem_is_intervalI [OF assms ‹x ∈ S› ‹y ∈ S›]) (auto simp: inner_simps)
qed
lemma is_interval_connected:
fixes S :: "'a::euclidean_space set"
shows "is_interval S ⟹ connected S"
using is_interval_convex convex_connected by auto
lemma convex_box [simp]: "convex (cbox a b)" "convex (box a (b::'a::euclidean_space))"
by (auto simp add: is_interval_convex)
text‹A non-singleton connected set is perfect (i.e. has no isolated points). ›
lemma connected_imp_perfect:
fixes a :: "'a::metric_space"
assumes "connected S" "a ∈ S" and S: "⋀x. S ≠ {x}"
shows "a islimpt S"
proof -
have False if "a ∈ T" "open T" "⋀y. ⟦y ∈ S; y ∈ T⟧ ⟹ y = a" for T
proof -
obtain e where "e > 0" and e: "cball a e ⊆ T"
using ‹open T› ‹a ∈ T› by (auto simp: open_contains_cball)
have "openin (top_of_set S) {a}"
unfolding openin_open using that ‹a ∈ S› by blast
moreover have "closedin (top_of_set S) {a}"
by (simp add: assms)
ultimately show "False"
using ‹connected S› connected_clopen S by blast
qed
then show ?thesis
unfolding islimpt_def by blast
qed
lemma islimpt_Ioc [simp]:
fixes a :: real
assumes "a<b"
shows "x islimpt {a<..b} ⟷ x ∈ {a..b}" (is "?lhs = ?rhs")
proof
show "?lhs ⟹ ?rhs"
by (metis assms closed_atLeastAtMost closed_limpt closure_greaterThanAtMost closure_subset islimpt_subset)
next
assume ?rhs
then have "x ∈ closure {a<..<b}"
using assms closure_greaterThanLessThan by blast
then show ?lhs
by (metis (no_types) Diff_empty Diff_insert0 interior_lessThanAtMost interior_limit_point interior_subset islimpt_in_closure islimpt_subset)
qed
lemma islimpt_Ico [simp]:
fixes a :: real
assumes "a<b" shows "x islimpt {a..<b} ⟷ x ∈ {a..b}"
by (metis assms closure_atLeastLessThan closure_greaterThanAtMost islimpt_Ioc limpt_of_closure)
lemma islimpt_Icc [simp]:
fixes a :: real
assumes "a<b" shows "x islimpt {a..b} ⟷ x ∈ {a..b}"
by (metis assms closure_atLeastLessThan islimpt_Ico limpt_of_closure)
lemma connected_imp_perfect_aff_dim:
"⟦connected S; aff_dim S ≠ 0; a ∈ S⟧ ⟹ a islimpt S"
using aff_dim_sing connected_imp_perfect by blast
subsection ‹On ‹real›, ‹is_interval›, ‹convex› and ‹connected› are all equivalent›
lemma mem_is_interval_1_I:
fixes a b c::real
assumes "is_interval S"
assumes "a ∈ S" "c ∈ S"
assumes "a ≤ b" "b ≤ c"
shows "b ∈ S"
using assms is_interval_1 by blast
lemma is_interval_connected_1:
fixes S :: "real set"
shows "is_interval S ⟷ connected S"
by (meson connected_iff_interval is_interval_1)
lemma is_interval_convex_1:
fixes S :: "real set"
shows "is_interval S ⟷ convex S"
by (metis is_interval_convex convex_connected is_interval_connected_1)
lemma connected_compact_interval_1:
"connected S ∧ compact S ⟷ (∃a b. S = {a..b::real})"
by (auto simp: is_interval_connected_1 [symmetric] is_interval_compact)
lemma connected_convex_1:
fixes S :: "real set"
shows "connected S ⟷ convex S"
by (metis is_interval_convex convex_connected is_interval_connected_1)
lemma connected_space_iff_is_interval_1 [iff]:
fixes S :: "real set"
shows "connected_space (top_of_set S) ⟷ is_interval S"
using connectedin_topspace is_interval_connected_1 by force
lemma connected_convex_1_gen:
fixes S :: "'a :: euclidean_space set"
assumes "DIM('a) = 1"
shows "connected S ⟷ convex S"
proof -
obtain f:: "'a ⇒ real" where linf: "linear f" and "inj f"
using subspace_isomorphism[OF subspace_UNIV subspace_UNIV,
where 'a='a and 'b=real]
unfolding Euclidean_Space.dim_UNIV
by (auto simp: assms)
then have "f -` (f ` S) = S"
by (simp add: inj_vimage_image_eq)
then show ?thesis
by (metis connected_convex_1 convex_linear_vimage linf convex_connected connected_linear_image)
qed
lemma [simp]:
fixes r s::real
shows is_interval_io: "is_interval {..<r}"
and is_interval_oi: "is_interval {r<..}"
and is_interval_oo: "is_interval {r<..<s}"
and is_interval_oc: "is_interval {r<..s}"
and is_interval_co: "is_interval {r..<s}"
by (simp_all add: is_interval_convex_1)
subsection ‹Another intermediate value theorem formulation›
lemma ivt_increasing_component_on_1:
fixes f :: "real ⇒ 'a::euclidean_space"
assumes "a ≤ b"
and "continuous_on {a..b} f"
and "(f a)∙k ≤ y" "y ≤ (f b)∙k"
shows "∃x∈{a..b}. (f x)∙k = y"
proof -
have "f a ∈ f ` cbox a b" "f b ∈ f ` cbox a b"
using ‹a ≤ b› by auto
then show ?thesis
using connected_ivt_component[of "f ` cbox a b" "f a" "f b" k y]
by (simp add: connected_continuous_image assms)
qed
lemma ivt_increasing_component_1:
fixes f :: "real ⇒ 'a::euclidean_space"
shows "a ≤ b ⟹ ∀x∈{a..b}. continuous (at x) f ⟹
f a∙k ≤ y ⟹ y ≤ f b∙k ⟹ ∃x∈{a..b}. (f x)∙k = y"
by (rule ivt_increasing_component_on_1) (auto simp: continuous_at_imp_continuous_on)
lemma ivt_decreasing_component_on_1:
fixes f :: "real ⇒ 'a::euclidean_space"
assumes "a ≤ b"
and "continuous_on {a..b} f"
and "(f b)∙k ≤ y"
and "y ≤ (f a)∙k"
shows "∃x∈{a..b}. (f x)∙k = y"
using ivt_increasing_component_on_1[of a b "λx. - f x" k "- y"] neg_equal_iff_equal
using assms continuous_on_minus by force
lemma ivt_decreasing_component_1:
fixes f :: "real ⇒ 'a::euclidean_space"
shows "a ≤ b ⟹ ∀x∈{a..b}. continuous (at x) f ⟹
f b∙k ≤ y ⟹ y ≤ f a∙k ⟹ ∃x∈{a..b}. (f x)∙k = y"
by (rule ivt_decreasing_component_on_1) (auto simp: continuous_at_imp_continuous_on)
subsection ‹A bound within an interval›
lemma convex_hull_eq_real_cbox:
fixes x y :: real assumes "x ≤ y"
shows "convex hull {x, y} = cbox x y"
proof (rule hull_unique)
show "{x, y} ⊆ cbox x y" using ‹x ≤ y› by auto
show "convex (cbox x y)"
by (rule convex_box)
next
fix S assume "{x, y} ⊆ S" and "convex S"
then show "cbox x y ⊆ S"
unfolding is_interval_convex_1 [symmetric] is_interval_def Basis_real_def
by - (clarify, simp (no_asm_use), fast)
qed
lemma unit_interval_convex_hull:
"cbox (0::'a::euclidean_space) One = convex hull {x. ∀i∈Basis. (x∙i = 0) ∨ (x∙i = 1)}"
(is "?int = convex hull ?points")
proof -
have One[simp]: "⋀i. i ∈ Basis ⟹ One ∙ i = 1"
by (simp add: inner_sum_left sum.If_cases inner_Basis)
have "?int = {x. ∀i∈Basis. x ∙ i ∈ cbox 0 1}"
by (auto simp: cbox_def)
also have "… = (∑i∈Basis. (λx. x *⇩R i) ` cbox 0 1)"
by (simp only: box_eq_set_sum_Basis)
also have "… = (∑i∈Basis. (λx. x *⇩R i) ` (convex hull {0, 1}))"
by (simp only: convex_hull_eq_real_cbox zero_le_one)
also have "… = (∑i∈Basis. convex hull ((λx. x *⇩R i) ` {0, 1}))"
by (simp add: convex_hull_linear_image)
also have "… = convex hull (∑i∈Basis. (λx. x *⇩R i) ` {0, 1})"
by (simp only: convex_hull_set_sum)
also have "… = convex hull {x. ∀i∈Basis. x∙i ∈ {0, 1}}"
by (simp only: box_eq_set_sum_Basis)
also have "convex hull {x. ∀i∈Basis. x∙i ∈ {0, 1}} = convex hull ?points"
by simp
finally show ?thesis .
qed
text ‹And this is a finite set of vertices.›
lemma unit_cube_convex_hull:
obtains S :: "'a::euclidean_space set"
where "finite S" and "cbox 0 (∑Basis) = convex hull S"
proof
show "finite {x::'a. ∀i∈Basis. x ∙ i = 0 ∨ x ∙ i = 1}"
proof (rule finite_subset, clarify)
show "finite ((λS. ∑i∈Basis. (if i ∈ S then 1 else 0) *⇩R i) ` Pow Basis)"
using finite_Basis by blast
fix x :: 'a
assume x: "∀i∈Basis. x ∙ i = 0 ∨ x ∙ i = 1"
show "x ∈ (λS. ∑i∈Basis. (if i∈S then 1 else 0) *⇩R i) ` Pow Basis"
apply (rule image_eqI[where x="{i. i ∈ Basis ∧ x∙i = 1}"])
using x
by (subst euclidean_eq_iff, auto)
qed
show "cbox 0 One = convex hull {x. ∀i∈Basis. x ∙ i = 0 ∨ x ∙ i = 1}"
using unit_interval_convex_hull by blast
qed
text ‹Hence any cube (could do any nonempty interval).›
lemma cube_convex_hull:
assumes "d > 0"
obtains S :: "'a::euclidean_space set" where
"finite S" and "cbox (x - (∑i∈Basis. d*⇩Ri)) (x + (∑i∈Basis. d*⇩Ri)) = convex hull S"
proof -
let ?d = "(∑i∈Basis. d *⇩R i)::'a"
have *: "cbox (x - ?d) (x + ?d) = (λy. x - ?d + (2 * d) *⇩R y) ` cbox 0 (∑Basis)"
proof (intro set_eqI iffI)
fix y
assume "y ∈ cbox (x - ?d) (x + ?d)"
then have "inverse (2 * d) *⇩R (y - (x - ?d)) ∈ cbox 0 (∑Basis)"
using assms by (simp add: mem_box inner_simps) (simp add: field_simps)
with ‹0 < d› show "y ∈ (λy. x - sum ((*⇩R) d) Basis + (2 * d) *⇩R y) ` cbox 0 One"
by (auto intro: image_eqI[where x= "inverse (2 * d) *⇩R (y - (x - ?d))"])
next
fix y
assume "y ∈ (λy. x - ?d + (2 * d) *⇩R y) ` cbox 0 One"
then obtain z where z: "z ∈ cbox 0 One" "y = x - ?d + (2*d) *⇩R z"
by auto
then show "y ∈ cbox (x - ?d) (x + ?d)"
using z assms by (auto simp: mem_box inner_simps)
qed
obtain S where "finite S" "cbox 0 (∑Basis::'a) = convex hull S"
using unit_cube_convex_hull by auto
then show ?thesis
by (rule_tac that[of "(λy. x - ?d + (2 * d) *⇩R y)` S"]) (auto simp: convex_hull_affinity *)
qed
subsection‹Representation of any interval as a finite convex hull›
lemma image_stretch_interval:
"(λx. ∑k∈Basis. (m k * (x∙k)) *⇩R k) ` cbox a (b::'a::euclidean_space) =
(if (cbox a b) = {} then {} else
cbox (∑k∈Basis. (min (m k * (a∙k)) (m k * (b∙k))) *⇩R k::'a)
(∑k∈Basis. (max (m k * (a∙k)) (m k * (b∙k))) *⇩R k))"
proof cases
assume *: "cbox a b ≠ {}"
show ?thesis
unfolding box_ne_empty if_not_P[OF *]
apply (simp add: cbox_def image_Collect set_eq_iff euclidean_eq_iff[where 'a='a] ball_conj_distrib[symmetric])
apply (subst choice_Basis_iff[symmetric])
proof (intro allI ball_cong refl)
fix x i :: 'a assume "i ∈ Basis"
with * have a_le_b: "a ∙ i ≤ b ∙ i"
unfolding box_ne_empty by auto
show "(∃xa. x ∙ i = m i * xa ∧ a ∙ i ≤ xa ∧ xa ≤ b ∙ i) ⟷
min (m i * (a ∙ i)) (m i * (b ∙ i)) ≤ x ∙ i ∧ x ∙ i ≤ max (m i * (a ∙ i)) (m i * (b ∙ i))"
proof (cases "m i = 0")
case True
with a_le_b show ?thesis by auto
next
case False
then have *: "⋀a b. a = m i * b ⟷ b = a / m i"
by (auto simp: field_simps)
from False have
"min (m i * (a ∙ i)) (m i * (b ∙ i)) = (if 0 < m i then m i * (a ∙ i) else m i * (b ∙ i))"
"max (m i * (a ∙ i)) (m i * (b ∙ i)) = (if 0 < m i then m i * (b ∙ i) else m i * (a ∙ i))"
using a_le_b by (auto simp: min_def max_def mult_le_cancel_left)
with False show ?thesis using a_le_b *
by (simp add: le_divide_eq divide_le_eq) (simp add: ac_simps)
qed
qed
qed simp
lemma interval_image_stretch_interval:
"∃u v. (λx. ∑k∈Basis. (m k * (x∙k))*⇩R k) ` cbox a (b::'a::euclidean_space) = cbox u (v::'a::euclidean_space)"
unfolding image_stretch_interval by auto
lemma cbox_translation: "cbox (c + a) (c + b) = image (λx. c + x) (cbox a b)"
using image_affinity_cbox [of 1 c a b]
using box_ne_empty [of "a+c" "b+c"] box_ne_empty [of a b]
by (auto simp: inner_left_distrib add.commute)
lemma cbox_image_unit_interval:
fixes a :: "'a::euclidean_space"
assumes "cbox a b ≠ {}"
shows "cbox a b =
(+) a ` (λx. ∑k∈Basis. ((b ∙ k - a ∙ k) * (x ∙ k)) *⇩R k) ` cbox 0 One"
using assms
apply (simp add: box_ne_empty image_stretch_interval cbox_translation [symmetric])
apply (simp add: min_def max_def algebra_simps sum_subtractf euclidean_representation)
done
lemma closed_interval_as_convex_hull:
fixes a :: "'a::euclidean_space"
obtains S where "finite S" "cbox a b = convex hull S"
proof (cases "cbox a b = {}")
case True with convex_hull_empty that show ?thesis
by blast
next
case False
obtain S::"'a set" where "finite S" and eq: "cbox 0 One = convex hull S"
by (blast intro: unit_cube_convex_hull)
let ?S = "((+) a ` (λx. ∑k∈Basis. ((b ∙ k - a ∙ k) * (x ∙ k)) *⇩R k) ` S)"
show thesis
proof
show "finite ?S"
by (simp add: ‹finite S›)
have lin: "linear (λx. ∑k∈Basis. ((b ∙ k - a ∙ k) * (x ∙ k)) *⇩R k)"
by (rule linear_compose_sum) (auto simp: algebra_simps linearI)
show "cbox a b = convex hull ?S"
using convex_hull_linear_image [OF lin]
by (simp add: convex_hull_translation eq cbox_image_unit_interval [OF False])
qed
qed
subsection ‹Bounded convex function on open set is continuous›
lemma convex_on_bounded_continuous:
fixes S :: "('a::real_normed_vector) set"
assumes "open S"
and f: "convex_on S f"
and "∀x∈S. ¦f x¦ ≤ b"
shows "continuous_on S f"
proof -
have "∃d>0. ∀x'. norm (x' - x) < d ⟶ ¦f x' - f x¦ < e" if "x ∈ S" "e > 0" for x and e :: real
proof -
define B where "B = ¦b¦ + 1"
then have B: "0 < B""⋀x. x∈S ⟹ ¦f x¦ ≤ B"
using assms(3) by auto
obtain k where "k > 0" and k: "cball x k ⊆ S"
using ‹x ∈ S› assms(1) open_contains_cball_eq by blast
show "∃d>0. ∀x'. norm (x' - x) < d ⟶ ¦f x' - f x¦ < e"
proof (intro exI conjI allI impI)
fix y
assume as: "norm (y - x) < min (k / 2) (e / (2 * B) * k)"
show "¦f y - f x¦ < e"
proof (cases "y = x")
case False
define t where "t = k / norm (y - x)"
have "2 < t" "0<t"
unfolding t_def using as False and ‹k>0›
by (auto simp:field_simps)
have "y ∈ S"
apply (rule k[THEN subsetD])
unfolding mem_cball dist_norm
apply (rule order_trans[of _ "2 * norm (x - y)"])
using as
by (auto simp: field_simps norm_minus_commute)
{
define w where "w = x + t *⇩R (y - x)"
have "w ∈ S"
using ‹k>0› by (auto simp: dist_norm t_def w_def k[THEN subsetD])
have "(1 / t) *⇩R x + - x + ((t - 1) / t) *⇩R x = (1 / t - 1 + (t - 1) / t) *⇩R x"
by (auto simp: algebra_simps)
also have "… = 0"
using ‹t > 0› by (auto simp:field_simps)
finally have w: "(1 / t) *⇩R w + ((t - 1) / t) *⇩R x = y"
unfolding w_def using False and ‹t > 0›
by (auto simp: algebra_simps)
have 2: "2 * B < e * t"
unfolding t_def using ‹0 < e› ‹0 < k› ‹B > 0› and as and False
by (auto simp:field_simps)
have "f y - f x ≤ (f w - f x) / t"
using convex_onD [OF f, of "(t - 1)/t" w x] ‹0 < t› ‹2 < t› ‹x ∈ S› ‹w ∈ S›
by (simp add: w field_simps)
also have "... < e"
using B(2)[OF ‹w∈S›] and B(2)[OF ‹x∈S›] 2 ‹t > 0› by (auto simp: field_simps)
finally have th1: "f y - f x < e" .
}
moreover
{
define w where "w = x - t *⇩R (y - x)"
have "w ∈ S"
using ‹k > 0› by (auto simp: dist_norm t_def w_def k[THEN subsetD])
have "(1 / (1 + t)) *⇩R x + (t / (1 + t)) *⇩R x = (1 / (1 + t) + t / (1 + t)) *⇩R x"
by (auto simp: algebra_simps)
also have "… = x"
using ‹t > 0› by (auto simp:field_simps)
finally have w: "(1 / (1+t)) *⇩R w + (t / (1 + t)) *⇩R y = x"
unfolding w_def using False and ‹t > 0›
by (auto simp: algebra_simps)
have "2 * B < e * t"
unfolding t_def
using ‹0 < e› ‹0 < k› ‹B > 0› and as and False
by (auto simp:field_simps)
then have *: "(f w - f y) / t < e"
using B(2)[OF ‹w∈S›] and B(2)[OF ‹y∈S›]
using ‹t > 0›
by (auto simp:field_simps)
have "f x ≤ 1 / (1 + t) * f w + (t / (1 + t)) * f y"
using convex_onD [OF f, of "t / (1+t)" w y] ‹0 < t› ‹2 < t› ‹y ∈ S› ‹w ∈ S›
by (simp add: w field_simps)
also have "… = (f w + t * f y) / (1 + t)"
using ‹t > 0› by (simp add: add_divide_distrib)
also have "… < e + f y"
using ‹t > 0› * ‹e > 0› by (auto simp: field_simps)
finally have "f x - f y < e" by auto
}
ultimately show ?thesis by auto
qed (use ‹0<e› in auto)
qed (use ‹0<e› ‹0<k› ‹0<B› in ‹auto simp: field_simps›)
qed
then show ?thesis
by (metis continuous_on_iff dist_norm real_norm_def)
qed
subsection ‹Upper bound on a ball implies upper and lower bounds›
lemma convex_bounds_lemma:
fixes x :: "'a::real_normed_vector"
assumes f: "convex_on (cball x e) f"
and b: "⋀y. y ∈ cball x e ⟹ f y ≤ b" and y: "y ∈ cball x e"
shows "¦f y¦ ≤ b + 2 * ¦f x¦"
proof (cases "0 ≤ e")
case True
define z where "z = 2 *⇩R x - y"
have *: "x - (2 *⇩R x - y) = y - x"
by (simp add: scaleR_2)
have z: "z ∈ cball x e"
using y unfolding z_def mem_cball dist_norm * by (auto simp: norm_minus_commute)
have "(1 / 2) *⇩R y + (1 / 2) *⇩R z = x"
unfolding z_def by (auto simp: algebra_simps)
then show "¦f y¦ ≤ b + 2 * ¦f x¦"
using convex_onD [OF f, of "1/2" y z] b[OF y] b y z
by (fastforce simp add: field_simps)
next
case False
have "dist x y < 0"
using False y unfolding mem_cball not_le by (auto simp del: dist_not_less_zero)
then show "¦f y¦ ≤ b + 2 * ¦f x¦"
using zero_le_dist[of x y] by auto
qed
subsubsection ‹Hence a convex function on an open set is continuous›
lemma real_of_nat_ge_one_iff: "1 ≤ real (n::nat) ⟷ 1 ≤ n"
by auto
lemma convex_on_continuous:
fixes S :: "'a::euclidean_space set"
assumes "open S" "convex_on S f"
shows "continuous_on S f"
unfolding continuous_on_eq_continuous_at[OF ‹open S›]
proof
note dimge1 = DIM_positive[where 'a='a]
fix x
assume "x ∈ S"
then obtain e where e: "cball x e ⊆ S" "e > 0"
using assms(1) unfolding open_contains_cball by auto
define d where "d = e / real DIM('a)"
have "0 < d"
unfolding d_def using ‹e > 0› dimge1 by auto
let ?d = "(∑i∈Basis. d *⇩R i)::'a"
obtain c
where c: "finite c" and c1: "convex hull c ⊆ cball x e" and c2: "cball x d ⊆ convex hull c"
proof
define c where "c = (∑i∈Basis. (λa. a *⇩R i) ` {x∙i - d, x∙i + d})"
show "finite c"
unfolding c_def by (simp add: finite_set_sum)
have "⋀i. i ∈ Basis ⟹ convex hull {x ∙ i - d, x ∙ i + d} = cbox (x ∙ i - d) (x ∙ i + d)"
using ‹0 < d› convex_hull_eq_real_cbox by auto
then have 1: "convex hull c = {a. ∀i∈Basis. a ∙ i ∈ cbox (x ∙ i - d) (x ∙ i + d)}"
unfolding box_eq_set_sum_Basis c_def convex_hull_set_sum
apply (subst convex_hull_linear_image [symmetric])
by (force simp add: linear_iff scaleR_add_left)+
then have 2: "convex hull c = {a. ∀i∈Basis. a ∙ i ∈ cball (x ∙ i) d}"
by (simp add: dist_norm abs_le_iff algebra_simps)
show "cball x d ⊆ convex hull c"
unfolding 2
by (clarsimp simp: dist_norm) (metis inner_commute inner_diff_right norm_bound_Basis_le)
have e': "e = (∑(i::'a)∈Basis. d)"
by (simp add: d_def)
show "convex hull c ⊆ cball x e"
unfolding 2
proof clarsimp
show "dist x y ≤ e" if "∀i∈Basis. dist (x ∙ i) (y ∙ i) ≤ d" for y
proof -
have "⋀i. i ∈ Basis ⟹ 0 ≤ dist (x ∙ i) (y ∙ i)"
by simp
have "(∑i∈Basis. dist (x ∙ i) (y ∙ i)) ≤ e"
using e' sum_mono that by fastforce
then show ?thesis
by (metis (mono_tags) euclidean_dist_l2 order_trans [OF L2_set_le_sum] zero_le_dist)
qed
qed
qed
define k where "k = Max (f ` c)"
have "convex_on (convex hull c) f"
using assms(2) c1 convex_on_subset e(1) by blast
then have k: "∀y∈convex hull c. f y ≤ k"
using c convex_on_convex_hull_bound k_def by fastforce
have "e ≤ e * real DIM('a)"
using e(2) real_of_nat_ge_one_iff by auto
then have "d ≤ e"
by (simp add: d_def field_split_simps)
then have dsube: "cball x d ⊆ cball x e"
by (rule subset_cball)
have conv: "convex_on (cball x d) f"
using ‹convex_on (convex hull c) f› c2 convex_on_subset by blast
then have "⋀y. y∈cball x d ⟹ ¦f y¦ ≤ k + 2 * ¦f x¦"
by (rule convex_bounds_lemma) (use c2 k in blast)
moreover have "convex_on (ball x d) f"
using conv convex_on_subset by fastforce
ultimately
have "continuous_on (ball x d) f"
by (metis convex_on_bounded_continuous Elementary_Metric_Spaces.open_ball mem_ball_imp_mem_cball)
then show "continuous (at x) f"
unfolding continuous_on_eq_continuous_at[OF open_ball]
using ‹d > 0› by auto
qed
end