# HG changeset patch # User paulson # Date 1445902921 0 # Node ID df57e4e3c0b702cf6d55cc1f28275c49cd8d5c97 # Parent 6cf5215afe8c8ff678e9caaf1b27093fdc5ae168# Parent ff12606337e94b217a19aebae95f469c326bcbf4 merged diff -r 6cf5215afe8c -r df57e4e3c0b7 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Mon Oct 26 19:00:24 2015 +0100 +++ b/src/HOL/Finite_Set.thy Mon Oct 26 23:42:01 2015 +0000 @@ -1545,6 +1545,10 @@ apply(auto simp add: intro:ccontr) done +lemma card_1_singletonE: + assumes "card A = 1" obtains x where "A = {x}" + using assms by (auto simp: card_Suc_eq) + lemma card_le_Suc_iff: "finite A \ Suc n \ card A = (\a B. A = insert a B \ a \ B \ n \ card B \ finite B)" by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff diff -r 6cf5215afe8c -r df57e4e3c0b7 src/HOL/Library/Convex.thy --- a/src/HOL/Library/Convex.thy Mon Oct 26 19:00:24 2015 +0100 +++ b/src/HOL/Library/Convex.thy Mon Oct 26 23:42:01 2015 +0000 @@ -96,7 +96,7 @@ lemma convex_halfspace_gt: "convex {x. inner a x > b}" using convex_halfspace_lt[of "-a" "-b"] by auto -lemma convex_real_interval: +lemma convex_real_interval [iff]: fixes a b :: "real" shows "convex {a..}" and "convex {..b}" and "convex {a<..}" and "convex {..2 = inner x x" by (simp add: norm_eq_sqrt_inner) +text \Identities involving real multiplication and division.\ + +lemma inner_mult_left: "inner (of_real m * a) b = m * (inner a b)" + by (metis real_inner_class.inner_scaleR_left scaleR_conv_of_real) + +lemma inner_mult_right: "inner a (of_real m * b) = m * (inner a b)" + by (metis real_inner_class.inner_scaleR_right scaleR_conv_of_real) + +lemma inner_mult_left': "inner (a * of_real m) b = m * (inner a b)" + by (simp add: of_real_def) + +lemma inner_mult_right': "inner a (b * of_real m) = (inner a b) * m" + by (simp add: of_real_def real_inner_class.inner_scaleR_right) + lemma Cauchy_Schwarz_ineq: "(inner x y)\<^sup>2 \ inner x x * inner y y" proof (cases) @@ -141,6 +155,16 @@ end +lemma inner_divide_left: + fixes a :: "'a :: {real_inner,real_div_algebra}" + shows "inner (a / of_real m) b = (inner a b) / m" + by (metis (no_types) divide_inverse inner_commute inner_scaleR_right mult.left_neutral mult.right_neutral mult_scaleR_right of_real_inverse scaleR_conv_of_real times_divide_eq_left) + +lemma inner_divide_right: + fixes a :: "'a :: {real_inner,real_div_algebra}" + shows "inner a (b / of_real m) = (inner a b) / m" + by (metis inner_commute inner_divide_left) + text \ Re-enable constraints for @{term "open"}, @{term dist}, and @{term norm}. diff -r 6cf5215afe8c -r df57e4e3c0b7 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Oct 26 19:00:24 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Oct 26 23:42:01 2015 +0000 @@ -2484,7 +2484,7 @@ shows "convex hull {a,b,c} \ s" using s apply (clarsimp simp add: convex_hull_insert [of "{b,c}" a] segment_convex_hull) - apply (meson subs convexD convex_segment ends_in_segment(1) ends_in_segment(2) subsetCE) + apply (meson subs convexD convex_closed_segment ends_in_segment(1) ends_in_segment(2) subsetCE) done lemma triangle_path_integrals_starlike_primitive: @@ -3096,7 +3096,6 @@ using path_integral_nearby [OF assms, where Ends=False] by simp_all - thm has_vector_derivative_polynomial_function corollary differentiable_polynomial_function: fixes p :: "real \ 'a::euclidean_space" shows "polynomial_function p \ p differentiable_on s" @@ -3112,6 +3111,11 @@ shows "polynomial_function p \ valid_path p" by (force simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_polymonial_function C1_differentiable_polynomial_function) +lemma valid_path_subpath_trivial [simp]: + fixes g :: "real \ 'a::euclidean_space" + shows "z \ g x \ valid_path (subpath x x g)" + by (simp add: subpath_def valid_path_polynomial_function) + lemma path_integral_bound_exists: assumes s: "open s" and g: "valid_path g" diff -r 6cf5215afe8c -r df57e4e3c0b7 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Oct 26 19:00:24 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Oct 26 23:42:01 2015 +0000 @@ -1083,7 +1083,7 @@ also have "... \ B * cmod (z - w) ^ n / (fact n) * cmod (w - z)" apply (rule complex_differentiable_bound [where f' = "\w. f (Suc n) w * (z - w)^n / (fact n)" - and s = "closed_segment w z", OF convex_segment]) + and s = "closed_segment w z", OF convex_closed_segment]) apply (auto simp: ends_in_segment real_of_nat_def DERIV_subset [OF sum_deriv wzs] norm_divide norm_mult norm_power divide_le_cancel cmod_bound) done @@ -1096,7 +1096,7 @@ lemma complex_mvt_line: assumes "\u. u \ closed_segment w z \ (f has_field_derivative f'(u)) (at u)" - shows "\u. u \ open_segment w z \ Re(f z) - Re(f w) = Re(f'(u) * (z - w))" + shows "\u. u \ closed_segment w z \ Re(f z) - Re(f w) = Re(f'(u) * (z - w))" proof - have twz: "\t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)" by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib) @@ -1107,11 +1107,10 @@ "\u. Re o (\h. f'((1 - u) *\<^sub>R w + u *\<^sub>R z) * h) o (\t. t *\<^sub>R (z - w))"]) apply auto apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI) - apply (auto simp add: open_segment_def twz) [] - apply (intro derivative_eq_intros has_derivative_at_within) - apply simp_all + apply (auto simp: closed_segment_def twz) [] + apply (intro derivative_eq_intros has_derivative_at_within, simp_all) apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib) - apply (force simp add: twz closed_segment_def) + apply (force simp: twz closed_segment_def) done qed diff -r 6cf5215afe8c -r df57e4e3c0b7 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Oct 26 19:00:24 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Oct 26 23:42:01 2015 +0000 @@ -464,7 +464,7 @@ "norm(exp z - (\k\n. z ^ k / (fact k))) \ exp\Re z\ * (norm z) ^ (Suc n) / (fact n)" proof (rule complex_taylor [of _ n "\k. exp" "exp\Re z\" 0 z, simplified]) show "convex (closed_segment 0 z)" - by (rule convex_segment [of 0 z]) + by (rule convex_closed_segment [of 0 z]) next fix k x assume "x \ closed_segment 0 z" "k \ n" diff -r 6cf5215afe8c -r df57e4e3c0b7 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Oct 26 19:00:24 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Oct 26 23:42:01 2015 +0000 @@ -17,10 +17,10 @@ (* To be moved elsewhere *) (* ------------------------------------------------------------------------- *) -lemma linear_scaleR: "linear (\x. scaleR c x)" +lemma linear_scaleR [simp]: "linear (\x. scaleR c x)" by (simp add: linear_iff scaleR_add_right) -lemma linear_scaleR_left: "linear (\r. scaleR r x)" +lemma linear_scaleR_left [simp]: "linear (\r. scaleR r x)" by (simp add: linear_iff scaleR_add_left) lemma injective_scaleR: "c \ 0 \ inj (\x::'a::real_vector. scaleR c x)" @@ -259,33 +259,62 @@ by blast qed -lemma closure_bounded_linear_image: +lemma closure_bounded_linear_image_subset: assumes f: "bounded_linear f" shows "f ` closure S \ closure (f ` S)" using linear_continuous_on [OF f] closed_closure closure_subset by (rule image_closure_subset) -lemma closure_linear_image: +lemma closure_linear_image_subset: fixes f :: "'m::euclidean_space \ 'n::real_normed_vector" assumes "linear f" - shows "f ` (closure S) \ closure (f ` S)" + shows "f ` (closure S) \ closure (f ` S)" using assms unfolding linear_conv_bounded_linear - by (rule closure_bounded_linear_image) + by (rule closure_bounded_linear_image_subset) + +lemma closed_injective_linear_image: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes S: "closed S" and f: "linear f" "inj f" + shows "closed (f ` S)" +proof - + obtain g where g: "linear g" "g \ f = id" + using linear_injective_left_inverse [OF f] by blast + then have confg: "continuous_on (range f) g" + using linear_continuous_on linear_conv_bounded_linear by blast + have [simp]: "g ` f ` S = S" + using g by (simp add: image_comp) + have cgf: "closed (g ` f ` S)" + by (simp add: `g \ f = id` S image_comp) + have [simp]: "{x \ range f. g x \ S} = f ` S" + using g by (simp add: o_def id_def image_def) metis + show ?thesis + apply (rule closedin_closed_trans [of "range f"]) + apply (rule continuous_closedin_preimage [OF confg cgf, simplified]) + apply (rule closed_injective_image_subspace) + using f + apply (auto simp: linear_linear linear_injective_0) + done +qed + +lemma closed_injective_linear_image_eq: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes f: "linear f" "inj f" + shows "(closed(image f s) \ closed s)" + by (metis closed_injective_linear_image closure_eq closure_linear_image_subset closure_subset_eq f(1) f(2) inj_image_subset_iff) lemma closure_injective_linear_image: - fixes f :: "'n::euclidean_space \ 'n::euclidean_space" - assumes "linear f" "inj f" - shows "f ` (closure S) = closure (f ` S)" -proof - - obtain f' where f': "linear f' \ f \ f' = id \ f' \ f = id" - using assms linear_injective_isomorphism[of f] isomorphism_expand by auto - then have "f' ` closure (f ` S) \ closure (S)" - using closure_linear_image[of f' "f ` S"] image_comp[of f' f] by auto - then have "f ` f' ` closure (f ` S) \ f ` closure S" by auto - then have "closure (f ` S) \ f ` closure S" - using image_comp[of f f' "closure (f ` S)"] f' by auto - then show ?thesis using closure_linear_image[of f S] assms by auto -qed + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + shows "\linear f; inj f\ \ f ` (closure S) = closure (f ` S)" + apply (rule subset_antisym) + apply (simp add: closure_linear_image_subset) + by (simp add: closure_minimal closed_injective_linear_image closure_subset image_mono) + +lemma closure_bounded_linear_image: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + shows "\linear f; bounded S\ \ f ` (closure S) = closure (f ` S)" + apply (rule subset_antisym, simp add: closure_linear_image_subset) + apply (rule closure_minimal, simp add: closure_subset image_mono) + by (meson bounded_closure closed_closure compact_continuous_image compact_eq_bounded_closed linear_continuous_on linear_conv_bounded_linear) lemma closure_scaleR: fixes S :: "'a::real_normed_vector set" @@ -293,7 +322,7 @@ proof show "(op *\<^sub>R c) ` (closure S) \ closure ((op *\<^sub>R c) ` S)" using bounded_linear_scaleR_right - by (rule closure_bounded_linear_image) + by (rule closure_bounded_linear_image_subset) show "closure ((op *\<^sub>R c) ` S) \ (op *\<^sub>R c) ` (closure S)" by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure) qed @@ -1422,12 +1451,12 @@ then show ?thesis by (auto simp add: convex_def Ball_def) qed -lemma connected_ball: +lemma connected_ball [iff]: fixes x :: "'a::real_normed_vector" shows "connected (ball x e)" using convex_connected convex_ball by auto -lemma connected_cball: +lemma connected_cball [iff]: fixes x :: "'a::real_normed_vector" shows "connected (cball x e)" using convex_connected convex_cball by auto @@ -2212,140 +2241,6 @@ qed -subsection \Caratheodory's theorem.\ - -lemma convex_hull_caratheodory: - fixes p :: "('a::euclidean_space) set" - shows "convex hull p = - {y. \s u. finite s \ s \ p \ card s \ DIM('a) + 1 \ - (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\v. u v *\<^sub>R v) s = y}" - unfolding convex_hull_explicit set_eq_iff mem_Collect_eq -proof (rule, rule) - fix y - let ?P = "\n. \s u. finite s \ card s = n \ s \ p \ (\x\s. 0 \ u x) \ - setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = y" - assume "\s u. finite s \ s \ p \ (\x\s. 0 \ u x) \ setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = y" - then obtain N where "?P N" by auto - then have "\n\N. (\k ?P k) \ ?P n" - apply (rule_tac ex_least_nat_le) - apply auto - done - then obtain n where "?P n" and smallest: "\k ?P k" - by blast - then obtain s u where obt: "finite s" "card s = n" "s\p" "\x\s. 0 \ u x" - "setsum u s = 1" "(\v\s. u v *\<^sub>R v) = y" by auto - - have "card s \ DIM('a) + 1" - proof (rule ccontr, simp only: not_le) - assume "DIM('a) + 1 < card s" - then have "affine_dependent s" - using affine_dependent_biggerset[OF obt(1)] by auto - then obtain w v where wv: "setsum w s = 0" "v\s" "w v \ 0" "(\v\s. w v *\<^sub>R v) = 0" - using affine_dependent_explicit_finite[OF obt(1)] by auto - def i \ "(\v. (u v) / (- w v)) ` {v\s. w v < 0}" - def t \ "Min i" - have "\x\s. w x < 0" - proof (rule ccontr, simp add: not_less) - assume as:"\x\s. 0 \ w x" - then have "setsum w (s - {v}) \ 0" - apply (rule_tac setsum_nonneg) - apply auto - done - then have "setsum w s > 0" - unfolding setsum.remove[OF obt(1) \v\s\] - using as[THEN bspec[where x=v]] and \v\s\ - using \w v \ 0\ - by auto - then show False using wv(1) by auto - qed - then have "i \ {}" unfolding i_def by auto - - then have "t \ 0" - using Min_ge_iff[of i 0 ] and obt(1) - unfolding t_def i_def - using obt(4)[unfolded le_less] - by (auto simp: divide_le_0_iff) - have t: "\v\s. u v + t * w v \ 0" - proof - fix v - assume "v \ s" - then have v: "0 \ u v" - using obt(4)[THEN bspec[where x=v]] by auto - show "0 \ u v + t * w v" - proof (cases "w v < 0") - case False - thus ?thesis using v \t\0\ by auto - next - case True - then have "t \ u v / (- w v)" - using \v\s\ - unfolding t_def i_def - apply (rule_tac Min_le) - using obt(1) - apply auto - done - then show ?thesis - unfolding real_0_le_add_iff - using pos_le_divide_eq[OF True[unfolded neg_0_less_iff_less[symmetric]]] - by auto - qed - qed - - obtain a where "a \ s" and "t = (\v. (u v) / (- w v)) a" and "w a < 0" - using Min_in[OF _ \i\{}\] and obt(1) unfolding i_def t_def by auto - then have a: "a \ s" "u a + t * w a = 0" by auto - have *: "\f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)" - unfolding setsum.remove[OF obt(1) \a\s\] by auto - have "(\v\s. u v + t * w v) = 1" - unfolding setsum.distrib wv(1) setsum_right_distrib[symmetric] obt(5) by auto - moreover have "(\v\s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y" - unfolding setsum.distrib obt(6) scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] wv(4) - using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp - ultimately have "?P (n - 1)" - apply (rule_tac x="(s - {a})" in exI) - apply (rule_tac x="\v. u v + t * w v" in exI) - using obt(1-3) and t and a - apply (auto simp add: * scaleR_left_distrib) - done - then show False - using smallest[THEN spec[where x="n - 1"]] by auto - qed - then show "\s u. finite s \ s \ p \ card s \ DIM('a) + 1 \ - (\x\s. 0 \ u x) \ setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = y" - using obt by auto -qed auto - -lemma caratheodory: - "convex hull p = - {x::'a::euclidean_space. \s. finite s \ s \ p \ - card s \ DIM('a) + 1 \ x \ convex hull s}" - unfolding set_eq_iff - apply rule - apply rule - unfolding mem_Collect_eq -proof - - fix x - assume "x \ convex hull p" - then obtain s u where "finite s" "s \ p" "card s \ DIM('a) + 1" - "\x\s. 0 \ u x" "setsum u s = 1" "(\v\s. u v *\<^sub>R v) = x" - unfolding convex_hull_caratheodory by auto - then show "\s. finite s \ s \ p \ card s \ DIM('a) + 1 \ x \ convex hull s" - apply (rule_tac x=s in exI) - using hull_subset[of s convex] - using convex_convex_hull[unfolded convex_explicit, of s, - THEN spec[where x=s], THEN spec[where x=u]] - apply auto - done -next - fix x - assume "\s. finite s \ s \ p \ card s \ DIM('a) + 1 \ x \ convex hull s" - then obtain s where "finite s" "s \ p" "card s \ DIM('a) + 1" "x \ convex hull s" - by auto - then show "x \ convex hull p" - using hull_mono[OF \s\p\] by auto -qed - - subsection \Some Properties of Affine Dependent Sets\ lemma affine_independent_empty: "\ affine_dependent {}" @@ -2572,7 +2467,8 @@ subsection \Affine Dimension of a Set\ -definition "aff_dim V = +definition aff_dim :: "('a::euclidean_space) set \ int" + where "aff_dim V = (SOME d :: int. \B. affine hull B = affine hull V \ \ affine_dependent B \ of_nat (card B) = d + 1)" @@ -2782,6 +2678,9 @@ using aff_independent_finite[of B] card_gt_0_iff[of B] by auto qed +lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1" + by (simp add: aff_dim_empty [symmetric]) + lemma aff_dim_affine_hull: "aff_dim (affine hull S) = aff_dim S" unfolding aff_dim_def using hull_hull[of _ S] by auto @@ -2829,6 +2728,13 @@ shows "of_nat (card B) = aff_dim B + 1" using aff_dim_unique[of B B] assms by auto +lemma affine_independent_iff_card: + fixes s :: "'a::euclidean_space set" + shows "~ affine_dependent s \ finite s \ aff_dim s = int(card s) - 1" + apply (rule iffI) + apply (simp add: aff_dim_affine_independent aff_independent_finite) + by (metis affine_basis_exists [of s] aff_dim_unique card_subset_eq diff_add_cancel of_nat_eq_iff) + lemma aff_dim_sing: fixes a :: "'n::euclidean_space" shows "aff_dim {a} = 0" @@ -3136,6 +3042,165 @@ shows "dim S < DIM ('n) \ interior S = {}" by (metis low_dim_interior affine_hull_univ dim_affine_hull less_not_refl dim_UNIV) +subsection \Caratheodory's theorem.\ + +lemma convex_hull_caratheodory_aff_dim: + fixes p :: "('a::euclidean_space) set" + shows "convex hull p = + {y. \s u. finite s \ s \ p \ card s \ aff_dim p + 1 \ + (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\v. u v *\<^sub>R v) s = y}" + unfolding convex_hull_explicit set_eq_iff mem_Collect_eq +proof (intro allI iffI) + fix y + let ?P = "\n. \s u. finite s \ card s = n \ s \ p \ (\x\s. 0 \ u x) \ + setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = y" + assume "\s u. finite s \ s \ p \ (\x\s. 0 \ u x) \ setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = y" + then obtain N where "?P N" by auto + then have "\n\N. (\k ?P k) \ ?P n" + apply (rule_tac ex_least_nat_le) + apply auto + done + then obtain n where "?P n" and smallest: "\k ?P k" + by blast + then obtain s u where obt: "finite s" "card s = n" "s\p" "\x\s. 0 \ u x" + "setsum u s = 1" "(\v\s. u v *\<^sub>R v) = y" by auto + + have "card s \ aff_dim p + 1" + proof (rule ccontr, simp only: not_le) + assume "aff_dim p + 1 < card s" + then have "affine_dependent s" + using affine_dependent_biggerset[OF obt(1)] independent_card_le_aff_dim not_less obt(3) + by blast + then obtain w v where wv: "setsum w s = 0" "v\s" "w v \ 0" "(\v\s. w v *\<^sub>R v) = 0" + using affine_dependent_explicit_finite[OF obt(1)] by auto + def i \ "(\v. (u v) / (- w v)) ` {v\s. w v < 0}" + def t \ "Min i" + have "\x\s. w x < 0" + proof (rule ccontr, simp add: not_less) + assume as:"\x\s. 0 \ w x" + then have "setsum w (s - {v}) \ 0" + apply (rule_tac setsum_nonneg) + apply auto + done + then have "setsum w s > 0" + unfolding setsum.remove[OF obt(1) \v\s\] + using as[THEN bspec[where x=v]] \v\s\ \w v \ 0\ by auto + then show False using wv(1) by auto + qed + then have "i \ {}" unfolding i_def by auto + then have "t \ 0" + using Min_ge_iff[of i 0 ] and obt(1) + unfolding t_def i_def + using obt(4)[unfolded le_less] + by (auto simp: divide_le_0_iff) + have t: "\v\s. u v + t * w v \ 0" + proof + fix v + assume "v \ s" + then have v: "0 \ u v" + using obt(4)[THEN bspec[where x=v]] by auto + show "0 \ u v + t * w v" + proof (cases "w v < 0") + case False + thus ?thesis using v \t\0\ by auto + next + case True + then have "t \ u v / (- w v)" + using \v\s\ unfolding t_def i_def + apply (rule_tac Min_le) + using obt(1) apply auto + done + then show ?thesis + unfolding real_0_le_add_iff + using pos_le_divide_eq[OF True[unfolded neg_0_less_iff_less[symmetric]]] + by auto + qed + qed + obtain a where "a \ s" and "t = (\v. (u v) / (- w v)) a" and "w a < 0" + using Min_in[OF _ \i\{}\] and obt(1) unfolding i_def t_def by auto + then have a: "a \ s" "u a + t * w a = 0" by auto + have *: "\f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)" + unfolding setsum.remove[OF obt(1) \a\s\] by auto + have "(\v\s. u v + t * w v) = 1" + unfolding setsum.distrib wv(1) setsum_right_distrib[symmetric] obt(5) by auto + moreover have "(\v\s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y" + unfolding setsum.distrib obt(6) scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] wv(4) + using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp + ultimately have "?P (n - 1)" + apply (rule_tac x="(s - {a})" in exI) + apply (rule_tac x="\v. u v + t * w v" in exI) + using obt(1-3) and t and a + apply (auto simp add: * scaleR_left_distrib) + done + then show False + using smallest[THEN spec[where x="n - 1"]] by auto + qed + then show "\s u. finite s \ s \ p \ card s \ aff_dim p + 1 \ + (\x\s. 0 \ u x) \ setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = y" + using obt by auto +qed auto + +lemma caratheodory_aff_dim: + fixes p :: "('a::euclidean_space) set" + shows "convex hull p = {x. \s. finite s \ s \ p \ card s \ aff_dim p + 1 \ x \ convex hull s}" + (is "?lhs = ?rhs") +proof + show "?lhs \ ?rhs" + apply (subst convex_hull_caratheodory_aff_dim) + apply clarify + apply (rule_tac x="s" in exI) + apply (simp add: hull_subset convex_explicit [THEN iffD1, OF convex_convex_hull]) + done +next + show "?rhs \ ?lhs" + using hull_mono by blast +qed + +lemma convex_hull_caratheodory: + fixes p :: "('a::euclidean_space) set" + shows "convex hull p = + {y. \s u. finite s \ s \ p \ card s \ DIM('a) + 1 \ + (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\v. u v *\<^sub>R v) s = y}" + (is "?lhs = ?rhs") +proof (intro set_eqI iffI) + fix x + assume "x \ ?lhs" then show "x \ ?rhs" + apply (simp only: convex_hull_caratheodory_aff_dim Set.mem_Collect_eq) + apply (erule ex_forward)+ + using aff_dim_subset_univ [of p] + apply simp + done +next + fix x + assume "x \ ?rhs" then show "x \ ?lhs" + by (auto simp add: convex_hull_explicit) +qed + +theorem caratheodory: + "convex hull p = + {x::'a::euclidean_space. \s. finite s \ s \ p \ + card s \ DIM('a) + 1 \ x \ convex hull s}" +proof safe + fix x + assume "x \ convex hull p" + then obtain s u where "finite s" "s \ p" "card s \