# HG changeset patch
# User huffman
# Date 1314202080 25200
# Node ID 13e72da170fc21f642265243d0cca566d9427554
# Parent  0e5c27f0752995f0cf3d0d1a712ccbc0b0149e24
change some subsection headings to subsubsection

diff -r 0e5c27f07529 -r 13e72da170fc src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Aug 23 16:47:48 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Aug 24 09:08:00 2011 -0700
@@ -327,8 +327,7 @@
   unfolding norm_eq_sqrt_inner by simp
 
 
-
-subsection {* Affine set and affine hull.*}
+subsection {* Affine set and affine hull *}
 
 definition
   affine :: "'a::real_vector set \<Rightarrow> bool" where
@@ -359,7 +358,7 @@
 lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
 by (metis affine_affine_hull hull_same)
 
-subsection {* Some explicit formulations (from Lars Schewe). *}
+subsubsection {* Some explicit formulations (from Lars Schewe) *}
 
 lemma affine: fixes V::"'a::real_vector set"
   shows "affine V \<longleftrightarrow> (\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (setsum (\<lambda>x. (u x) *\<^sub>R x)) s \<in> V)"
@@ -459,7 +458,7 @@
   thus "\<exists>u. setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
     unfolding if_smult scaleR_zero_left and setsum_restrict_set[OF assms, THEN sym] and * by auto qed
 
-subsection {* Stepping theorems and hence small special cases. *}
+subsubsection {* Stepping theorems and hence small special cases *}
 
 lemma affine_hull_empty[simp]: "affine hull {} = {}"
   apply(rule hull_unique) by auto
@@ -553,7 +552,7 @@
 using mem_affine_3[of S x y z 1 v "-v"] assms by (simp add: algebra_simps)
 
 
-subsection {* Some relations between affine hull and subspaces. *}
+subsubsection {* Some relations between affine hull and subspaces *}
 
 lemma affine_hull_insert_subset_span:
   shows "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
@@ -596,7 +595,7 @@
   shows "affine hull s = {a + v | v. v \<in> span {x - a | x. x \<in> s - {a}}}"
   using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
 
-subsection{* Parallel Affine Sets *}
+subsubsection {* Parallel affine sets *}
 
 definition affine_parallel :: "'a::real_vector set => 'a::real_vector set => bool"
 where "affine_parallel S T = (? a. T = ((%x. a + x) ` S))"
@@ -670,7 +669,7 @@
 lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s"
   unfolding subspace_def affine_def by auto
 
-subsection{* Subspace Parallel to an Affine Set *}
+subsubsection {* Subspace parallel to an affine set *}
 
 lemma subspace_affine:
   shows "subspace S <-> (affine S & 0 : S)"
@@ -746,7 +745,7 @@
 } from this show ?thesis using ex by auto
 qed
 
-subsection {* Cones. *}
+subsection {* Cones *}
 
 definition
   cone :: "'a::real_vector set \<Rightarrow> bool" where
@@ -761,7 +760,7 @@
 lemma cone_Inter[intro]: "(\<forall>s\<in>f. cone s) \<Longrightarrow> cone(\<Inter> f)"
   unfolding cone_def by auto
 
-subsection {* Conic hull. *}
+subsubsection {* Conic hull *}
 
 lemma cone_cone_hull: "cone (cone hull s)"
   unfolding hull_def by auto
@@ -874,7 +873,7 @@
 ultimately show ?thesis by blast
 qed
 
-subsection {* Affine dependence and consequential theorems (from Lars Schewe). *}
+subsection {* Affine dependence and consequential theorems (from Lars Schewe) *}
 
 definition
   affine_dependent :: "'a::real_vector set \<Rightarrow> bool" where
@@ -1016,12 +1015,12 @@
   thus ?thesis unfolding connected_def by auto
 qed
 
-subsection {* One rather trivial consequence. *}
+text {* One rather trivial consequence. *}
 
 lemma connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
   by(simp add: convex_connected convex_UNIV)
 
-subsection {* Balls, being convex, are connected. *}
+text {* Balls, being convex, are connected. *}
 
 lemma convex_box: fixes a::"'a::euclidean_space"
   assumes "\<And>i. i<DIM('a) \<Longrightarrow> convex {x. P i x}"
@@ -1085,7 +1084,7 @@
   shows "connected(cball x e)"
   using convex_connected convex_cball by auto
 
-subsection {* Convex hull. *}
+subsection {* Convex hull *}
 
 lemma convex_convex_hull: "convex(convex hull s)"
   unfolding hull_def using convex_Inter[of "{t. convex t \<and> s \<subseteq> t}"]
@@ -1107,7 +1106,7 @@
   shows "finite s \<Longrightarrow> bounded(convex hull s)"
   using bounded_convex_hull finite_imp_bounded by auto
 
-subsection {* Convex hull is "preserved" by a linear function. *}
+subsubsection {* Convex hull is "preserved" by a linear function *}
 
 lemma convex_hull_linear_image:
   assumes "bounded_linear f"
@@ -1129,7 +1128,7 @@
   shows "(f x) \<in> convex hull (f ` s)"
 using convex_hull_linear_image[OF assms(1)] assms(2) by auto
 
-subsection {* Stepping theorems for convex hulls of finite sets. *}
+subsubsection {* Stepping theorems for convex hulls of finite sets *}
 
 lemma convex_hull_empty[simp]: "convex hull {} = {}"
   apply(rule hull_unique) by auto
@@ -1192,7 +1191,7 @@
 qed
 
 
-subsection {* Explicit expression for convex hull. *}
+subsubsection {* Explicit expression for convex hull *}
 
 lemma convex_hull_indexed:
   fixes s :: "'a::real_vector set"
@@ -1263,7 +1262,7 @@
     using assms and t(1) by auto
 qed
 
-subsection {* Another formulation from Lars Schewe. *}
+subsubsection {* Another formulation from Lars Schewe *}
 
 lemma setsum_constant_scaleR:
   fixes y :: "'a::real_vector"
@@ -1327,7 +1326,7 @@
   ultimately show ?thesis unfolding set_eq_iff by blast
 qed
 
-subsection {* A stepping theorem for that expansion. *}
+subsubsection {* A stepping theorem for that expansion *}
 
 lemma convex_hull_finite_step:
   fixes s :: "'a::real_vector set" assumes "finite s"
@@ -1353,7 +1352,7 @@
   ultimately show ?lhs apply(rule_tac x="\<lambda>x. if a = x then v else u x" in exI)  unfolding setsum_clauses(2)[OF assms] by auto
 qed
 
-subsection {* Hence some special cases. *}
+subsubsection {* Hence some special cases *}
 
 lemma convex_hull_2:
   "convex hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b | u v. 0 \<le> u \<and> 0 \<le> v \<and> u + v = 1}"
@@ -1385,7 +1384,7 @@
   show ?thesis unfolding convex_hull_3 apply (auto simp add: *) apply(rule_tac x=v in exI) apply(rule_tac x=w in exI) apply (simp add: algebra_simps)
     apply(rule_tac x=u in exI) apply(rule_tac x=v in exI) by (simp add: algebra_simps) qed
 
-subsection {* Relations among closure notions and corresponding hulls. *}
+subsection {* Relations among closure notions and corresponding hulls *}
 
 lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
   unfolding affine_def convex_def by auto
@@ -2107,7 +2106,7 @@
 from this show ?thesis using aff_dim_open[of "interior S"] aff_dim_subset_univ[of S] assms by auto   
 qed
 
-subsection{* Relative Interior of a Set *}
+subsection {* Relative interior of a set *}
 
 definition "rel_interior S = {x. ? T. openin (subtopology euclidean (affine hull S)) T & x : T & T <= S}"
 
@@ -2276,7 +2275,7 @@
      by (auto split: split_if_asm)
 qed
 
-subsection "Relative open"
+subsubsection {* Relative open sets *}
 
 definition "rel_open S <-> (rel_interior S) = S"
 
@@ -2383,7 +2382,7 @@
   thus ?thesis using * by auto 
 qed
 
-subsection{* Relative interior preserves under linear transformations *}
+subsubsection{* Relative interior preserves under linear transformations *}
 
 lemma rel_interior_translation_aux:
 fixes a :: "'n::euclidean_space"
@@ -2891,7 +2890,7 @@
   shows "continuous_on t (closest_point s)"
 by(metis continuous_at_imp_continuous_on continuous_at_closest_point[OF assms])
 
-subsection {* Various point-to-set separating/supporting hyperplane theorems. *}
+subsubsection {* Various point-to-set separating/supporting hyperplane theorems. *}
 
 lemma supporting_hyperplane_closed_point:
   fixes z :: "'a::{real_inner,heine_borel}"
@@ -2950,7 +2949,7 @@
 next case False thus ?thesis using False using separating_hyperplane_closed_point[OF assms]
     apply - apply(erule exE)+ unfolding inner_zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
 
-subsection {* Now set-to-set for closed/compact sets. *}
+subsubsection {* Now set-to-set for closed/compact sets *}
 
 lemma separating_hyperplane_closed_compact:
   assumes "convex (s::('a::euclidean_space) set)" "closed s" "convex t" "compact t" "t \<noteq> {}" "s \<inter> t = {}"
@@ -2992,7 +2991,7 @@
     using separating_hyperplane_closed_compact[OF assms(4-5,1-2,3)] and assms(6) by auto
   thus ?thesis apply(rule_tac x="-a" in exI, rule_tac x="-b" in exI) by auto qed
 
-subsection {* General case without assuming closure and getting non-strict separation. *}
+subsubsection {* General case without assuming closure and getting non-strict separation *}
 
 lemma separating_hyperplane_set_0:
   assumes "convex s" "(0::'a::euclidean_space) \<notin> s"
@@ -3035,7 +3034,7 @@
     done
 qed
 
-subsection {* More convexity generalities. *}
+subsection {* More convexity generalities *}
 
 lemma convex_closure:
   fixes s :: "'a::real_normed_vector set"
@@ -3147,7 +3146,7 @@
 ultimately show ?thesis by blast
 qed
 
-subsection {* Convex set as intersection of halfspaces. *}
+subsection {* Convex set as intersection of halfspaces *}
 
 lemma convex_halfspace_intersection:
   fixes s :: "('a::euclidean_space) set"
@@ -3160,7 +3159,7 @@
     apply(erule exE)+ apply(erule_tac x="-a" in allE, erule_tac x="-b" in allE) by auto
 qed auto
 
-subsection {* Radon's theorem (from Lars Schewe). *}
+subsection {* Radon's theorem (from Lars Schewe) *}
 
 lemma radon_ex_lemma:
   assumes "finite c" "affine_dependent c"
@@ -3229,7 +3228,7 @@
   from radon_partition[OF *] guess m .. then guess p ..
   thus ?thesis apply(rule_tac that[of p m]) using s by auto qed
 
-subsection {* Helly's theorem. *}
+subsection {* Helly's theorem *}
 
 lemma helly_induct: fixes f::"('a::euclidean_space) set set"
   assumes "card f = n" "n \<ge> DIM('a) + 1"
@@ -3275,7 +3274,7 @@
   shows "\<Inter> f \<noteq>{}"
   apply(rule helly_induct) using assms by auto
 
-subsection {* Homeomorphism of all convex compact sets with nonempty interior. *}
+subsection {* Homeomorphism of all convex compact sets with nonempty interior *}
 
 lemma compact_frontier_line_lemma:
   fixes s :: "('a::euclidean_space) set"
@@ -3495,7 +3494,7 @@
   shows "s homeomorphic t"
   using assms by(meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
 
-subsection {* Epigraphs of convex functions. *}
+subsection {* Epigraphs of convex functions *}
 
 definition "epigraph s (f::_ \<Rightarrow> real) = {xy. fst xy \<in> s \<and> f (fst xy) \<le> snd xy}"
 
@@ -3519,7 +3518,7 @@
   "convex s \<Longrightarrow> convex_on s f \<longleftrightarrow> convex(epigraph s f)"
 by(simp add: convex_epigraph)
 
-subsection {* Use this to derive general bound property of convex function. *}
+subsubsection {* Use this to derive general bound property of convex function *}
 
 lemma convex_on:
   assumes "convex s"
@@ -3538,7 +3537,7 @@
   apply(rule mult_left_mono)using assms[unfolded convex] by auto
 
 
-subsection {* Convexity of general and special intervals. *}
+subsection {* Convexity of general and special intervals *}
 
 lemma convexI: (* TODO: move to Library/Convex.thy *)
   assumes "\<And>x y u v. \<lbrakk>x \<in> s; y \<in> s; 0 \<le> u; 0 \<le> v; u + v = 1\<rbrakk> \<Longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s"
@@ -3601,7 +3600,7 @@
   "connected s \<longleftrightarrow> convex (s::(real^1) set)" 
 by(metis is_interval_convex convex_connected is_interval_connected_1)
 *)
-subsection {* Another intermediate value theorem formulation. *}
+subsection {* Another intermediate value theorem formulation *}
 
 lemma ivt_increasing_component_on_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
   assumes "a \<le> b" "continuous_on {a .. b} f" "(f a)$$k \<le> y" "y \<le> (f b)$$k"
@@ -3631,7 +3630,7 @@
 by(rule ivt_decreasing_component_on_1)
   (auto simp: continuous_at_imp_continuous_on)
 
-subsection {* A bound within a convex hull, and so an interval. *}
+subsection {* A bound within a convex hull, and so an interval *}
 
 lemma convex_on_convex_hull_bound:
   assumes "convex_on (convex hull s) f" "\<forall>x\<in>s. f x \<le> b"
@@ -3702,7 +3701,7 @@
     unfolding mem_interval apply rule unfolding mem_Collect_eq apply(erule_tac x=i in allE)
     by auto qed
 
-subsection {* And this is a finite set of vertices. *}
+text {* And this is a finite set of vertices. *}
 
 lemma unit_cube_convex_hull: obtains s where "finite s" "{0 .. (\<chi>\<chi> i. 1)::'a::ordered_euclidean_space} = convex hull s"
   apply(rule that[of "{x::'a. \<forall>i<DIM('a). x$$i=0 \<or> x$$i=1}"])
@@ -3713,7 +3712,7 @@
     apply(rule image_eqI[where x="{i. i<DIM('a) \<and> x$$i = 1}"])
     using as apply(subst euclidean_eq) by auto qed auto
 
-subsection {* Hence any cube (could do any nonempty interval). *}
+text {* Hence any cube (could do any nonempty interval). *}
 
 lemma cube_convex_hull:
   assumes "0 < d" obtains s::"('a::ordered_euclidean_space) set" where
@@ -3745,7 +3744,7 @@
   obtain s where "finite s" "{0::'a..\<chi>\<chi> i.1} = convex hull s" using unit_cube_convex_hull by auto
   thus ?thesis apply(rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` s"]) unfolding * and convex_hull_affinity by auto qed
 
-subsection {* Bounded convex function on open set is continuous. *}
+subsection {* Bounded convex function on open set is continuous *}
 
 lemma convex_on_bounded_continuous:
   fixes s :: "('a::real_normed_vector) set"
@@ -3796,7 +3795,7 @@
     qed(insert `0<e`, auto) 
   qed(insert `0<e` `0<k` `0<B`, auto simp add:field_simps intro!:mult_pos_pos) qed
 
-subsection {* Upper bound on a ball implies upper and lower bounds. *}
+subsection {* Upper bound on a ball implies upper and lower bounds *}
 
 lemma convex_bounds_lemma:
   fixes x :: "'a::real_normed_vector"
@@ -3813,7 +3812,7 @@
   hence "dist x y < 0" using False unfolding mem_cball not_le by (auto simp del: dist_not_less_zero)
   thus "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>" using zero_le_dist[of x y] by auto qed
 
-subsection {* Hence a convex function on an open set is continuous. *}
+subsubsection {* Hence a convex function on an open set is continuous *}
 
 lemma convex_on_continuous:
   assumes "open (s::('a::ordered_euclidean_space) set)" "convex_on s f" 
@@ -3856,7 +3855,7 @@
     using `d>0` by auto 
 qed
 
-subsection {* Line segments, Starlike Sets, etc.*}
+subsection {* Line segments, Starlike Sets, etc. *}
 
 (* Use the same overloading tricks as for intervals, so that 
    segment[a,b] is closed and segment(a,b) is open relative to affine hull. *)
@@ -4002,7 +4001,7 @@
   "between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}"
   unfolding between_mem_segment segment_convex_hull ..
 
-subsection {* Shrinking towards the interior of a convex set. *}
+subsection {* Shrinking towards the interior of a convex set *}
 
 lemma mem_interior_convex_shrink:
   fixes s :: "('a::euclidean_space) set"
@@ -4049,7 +4048,7 @@
   thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink) 
     using assms(1,4-5) `y\<in>s` by auto qed
 
-subsection {* Some obvious but surprisingly hard simplex lemmas. *}
+subsection {* Some obvious but surprisingly hard simplex lemmas *}
 
 lemma simplex:
   assumes "finite s" "0 \<notin> s"
@@ -4292,7 +4291,7 @@
   qed
 qed
 
-subsection{* Relative Interior of Convex Set *}
+subsection {* Relative interior of convex set *}
 
 lemma rel_interior_convex_nonempty_aux: 
 fixes S :: "('n::euclidean_space) set" 
@@ -4716,7 +4715,7 @@
 } ultimately show ?thesis by auto
 qed
 
-subsection{* Relative interior and closure under commom operations *}
+subsubsection {* Relative interior and closure under common operations *}
 
 lemma rel_interior_inter_aux: "Inter {rel_interior S |S. S : I} <= Inter I"
 proof- 
@@ -5219,7 +5218,7 @@
 } from this show ?thesis using h2 by blast
 qed
 
-subsection{* Relative interior of convex cone *}
+subsubsection {* Relative interior of convex cone *}
 
 lemma cone_rel_interior:
 fixes S :: "('m::euclidean_space) set"