src/HOL/Analysis/Convex_Euclidean_Space.thy

 imports
   Convex
   Topology_Euclidean_Space
 begin
 
-subsection%unimportant \<open>Topological Properties of Convex Sets and Functions\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological Properties of Convex Sets and Functions\<close>
 
 lemma convex_supp_sum:
   assumes "convex S" and 1: "supp_sum u I = 1"
       and "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> u i \<and> (u i = 0 \<or> f i \<in> S)"
     shows "supp_sum (\<lambda>i. u i *\<^sub>R f i) I \<in> S"

 by (metis low_dim_interior)
 
 
 subsection \<open>Relative interior of a set\<close>
 
-definition%important "rel_interior S =
+definition\<^marker>\<open>tag important\<close> "rel_interior S =
   {x. \<exists>T. openin (top_of_set (affine hull S)) T \<and> x \<in> T \<and> T \<subseteq> S}"
 
 lemma rel_interior_mono:
    "\<lbrakk>S \<subseteq> T; affine hull S = affine hull T\<rbrakk>
    \<Longrightarrow> (rel_interior S) \<subseteq> (rel_interior T)"

     by (auto split: if_split_asm)
 qed
 
 subsubsection \<open>Relative open sets\<close>
 
-definition%important "rel_open S \<longleftrightarrow> rel_interior S = S"
+definition\<^marker>\<open>tag important\<close> "rel_open S \<longleftrightarrow> rel_interior S = S"
 
 lemma rel_open: "rel_open S \<longleftrightarrow> openin (top_of_set (affine hull S)) S"
   unfolding rel_open_def rel_interior_def
   apply auto
   using openin_subopen[of "top_of_set (affine hull S)" S]

       by (simp add: rel_interior_affine affine_closed)
   qed
 qed
 
 
-subsubsection%unimportant\<open>Relative interior preserves under linear transformations\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close>\<open>Relative interior preserves under linear transformations\<close>
 
 lemma rel_interior_translation_aux:
   fixes a :: "'n::euclidean_space"
   shows "((\<lambda>x. a + x) ` rel_interior S) \<subseteq> rel_interior ((\<lambda>x. a + x) ` S)"
 proof -

   using assms rel_interior_injective_on_span_linear_image[of f S]
     subset_inj_on[of f "UNIV" "span S"]
   by auto
 
 
-subsection%unimportant \<open>Openness and compactness are preserved by convex hull operation\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Openness and compactness are preserved by convex hull operation\<close>
 
 lemma open_convex_hull[intro]:
   fixes S :: "'a::real_normed_vector set"
   assumes "open S"
   shows "open (convex hull S)"

     qed
   qed
 qed
 
 
-subsection%unimportant \<open>Extremal points of a simplex are some vertices\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Extremal points of a simplex are some vertices\<close>
 
 lemma dist_increases_online:
   fixes a b d :: "'a::real_inner"
   assumes "d \<noteq> 0"
   shows "dist a (b + d) > dist a b \<or> dist a (b - d) > dist a b"

   by(cases "S = {}") auto
 
 
 subsection \<open>Closest point of a convex set is unique, with a continuous projection\<close>
 
-definition%important closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a"
+definition\<^marker>\<open>tag important\<close> closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a"
   where "closest_point S a = (SOME x. x \<in> S \<and> (\<forall>y\<in>S. dist a x \<le> dist a y))"
 
 lemma closest_point_exists:
   assumes "closed S"
     and "S \<noteq> {}"

     using rel_interior_subset False by blast
   ultimately show ?thesis by blast
 qed
 
 
-subsubsection%unimportant \<open>Various point-to-set separating/supporting hyperplane theorems\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Various point-to-set separating/supporting hyperplane theorems\<close>
 
 lemma supporting_hyperplane_closed_point:
   fixes z :: "'a::{real_inner,heine_borel}"
   assumes "convex S"
     and "closed S"

     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%unimportant \<open>Now set-to-set for closed/compact sets\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Now set-to-set for closed/compact sets\<close>
 
 lemma separating_hyperplane_closed_compact:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S"
     and "closed S"

     apply (rule_tac x="-b" in exI, auto)
     done
 qed
 
 
-subsubsection%unimportant \<open>General case without assuming closure and getting non-strict separation\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>General case without assuming closure and getting non-strict separation\<close>
 
 lemma separating_hyperplane_set_0:
   assumes "convex S" "(0::'a::euclidean_space) \<notin> S"
   shows "\<exists>a. a \<noteq> 0 \<and> (\<forall>x\<in>S. 0 \<le> inner a x)"
 proof -

     by (intro exI[of _ a] exI[of _ "SUP x\<in>S. a \<bullet> x"])
        (auto intro!: cSUP_upper bdd cSUP_least \<open>a \<noteq> 0\<close> \<open>S \<noteq> {}\<close> *)
 qed
 
 
-subsection%unimportant \<open>More convexity generalities\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>More convexity generalities\<close>
 
 lemma convex_closure [intro,simp]:
   fixes S :: "'a::real_normed_vector set"
   assumes "convex S"
   shows "convex (closure S)"

 
 lemma convex_hull_eq_empty[simp]: "convex hull S = {} \<longleftrightarrow> S = {}"
   using hull_subset[of S convex] convex_hull_empty by auto
 
 
-subsection%unimportant \<open>Convex set as intersection of halfspaces\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Convex set as intersection of halfspaces\<close>
 
 lemma convex_halfspace_intersection:
   fixes s :: "('a::euclidean_space) set"
   assumes "closed s" "convex s"
   shows "s = \<Inter>{h. s \<subseteq> h \<and> (\<exists>a b. h = {x. inner a x \<le> b})}"

     apply (erule_tac x="-b" in allE, auto)
     done
 qed auto
 
 
-subsection%unimportant \<open>Convexity of general and special intervals\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Convexity of general and special intervals\<close>
 
 lemma is_interval_convex:
   fixes S :: "'a::euclidean_space set"
   assumes "is_interval S"
   shows "convex S"

 
 lemma connected_imp_perfect_aff_dim:
      "\<lbrakk>connected S; aff_dim S \<noteq> 0; a \<in> S\<rbrakk> \<Longrightarrow> a islimpt S"
   using aff_dim_sing connected_imp_perfect by blast
 
-subsection%unimportant \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent\<close>
 
 lemma mem_is_interval_1_I:
   fixes a b c::real
   assumes "is_interval S"
   assumes "a \<in> S" "c \<in> S"

     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%unimportant \<open>Another intermediate value theorem formulation\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Another intermediate value theorem formulation\<close>
 
 lemma ivt_increasing_component_on_1:
   fixes f :: "real \<Rightarrow> 'a::euclidean_space"
   assumes "a \<le> b"
     and "continuous_on {a..b} f"

   shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a..b}. continuous (at x) f \<Longrightarrow>
     f b\<bullet>k \<le> y \<Longrightarrow> y \<le> f a\<bullet>k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
   by (rule ivt_decreasing_component_on_1) (auto simp: continuous_at_imp_continuous_on)
 
 
-subsection%unimportant \<open>A bound within an interval\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>A bound within an interval\<close>
 
 lemma convex_hull_eq_real_cbox:
   fixes x y :: real assumes "x \<le> y"
   shows "convex hull {x, y} = cbox x y"
 proof (rule hull_unique)

     using unit_cube_convex_hull by auto
   then show ?thesis
     by (rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` S"]) (auto simp: convex_hull_affinity *)
 qed
 
-subsection%unimportant\<open>Representation of any interval as a finite convex hull\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Representation of any interval as a finite convex hull\<close>
 
 lemma image_stretch_interval:
   "(\<lambda>x. \<Sum>k\<in>Basis. (m k * (x\<bullet>k)) *\<^sub>R k) ` cbox a (b::'a::euclidean_space) =
   (if (cbox a b) = {} then {} else
     cbox (\<Sum>k\<in>Basis. (min (m k * (a\<bullet>k)) (m k * (b\<bullet>k))) *\<^sub>R k::'a)

     apply (simp add: eq [symmetric] cbox_image_unit_interval [OF False])
     done
 qed
 
 
-subsection%unimportant \<open>Bounded convex function on open set is continuous\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Bounded convex function on open set is continuous\<close>
 
 lemma convex_on_bounded_continuous:
   fixes S :: "('a::real_normed_vector) set"
   assumes "open S"
     and "convex_on S f"

     qed (insert \<open>0<e\<close>, auto)
   qed (insert \<open>0<e\<close> \<open>0<k\<close> \<open>0<B\<close>, auto simp: field_simps)
 qed
 
 
-subsection%unimportant \<open>Upper bound on a ball implies upper and lower bounds\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Upper bound on a ball implies upper and lower bounds\<close>
 
 lemma convex_bounds_lemma:
   fixes x :: "'a::real_normed_vector"
   assumes "convex_on (cball x e) f"
     and "\<forall>y \<in> cball x e. f y \<le> b"

   then show "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>"
     using zero_le_dist[of x y] by auto
 qed
 
 
-subsubsection%unimportant \<open>Hence a convex function on an open set is continuous\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Hence a convex function on an open set is continuous\<close>
 
 lemma real_of_nat_ge_one_iff: "1 \<le> real (n::nat) \<longleftrightarrow> 1 \<le> n"
   by auto
 
 lemma convex_on_continuous: