equal
deleted
inserted
replaced
113 |
113 |
114 lemma substdbasis_expansion_unique: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}" |
114 lemma substdbasis_expansion_unique: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}" |
115 shows "setsum (%i. f i *\<^sub>R basis i) d = (x::'a::euclidean_space) |
115 shows "setsum (%i. f i *\<^sub>R basis i) d = (x::'a::euclidean_space) |
116 <-> (!i<DIM('a). (i:d --> f i = x$$i) & (i ~: d --> x $$ i = 0))" |
116 <-> (!i<DIM('a). (i:d --> f i = x$$i) & (i ~: d --> x $$ i = 0))" |
117 proof- have *:"\<And>x a b P. x * (if P then a else b) = (if P then x*a else x*b)" by auto |
117 proof- have *:"\<And>x a b P. x * (if P then a else b) = (if P then x*a else x*b)" by auto |
118 have **:"finite d" apply(rule finite_subset[OF assms]) by fastsimp |
118 have **:"finite d" apply(rule finite_subset[OF assms]) by fastforce |
119 have ***:"\<And>i. (setsum (%i. f i *\<^sub>R ((basis i)::'a)) d) $$ i = (\<Sum>x\<in>d. if x = i then f x else 0)" |
119 have ***:"\<And>i. (setsum (%i. f i *\<^sub>R ((basis i)::'a)) d) $$ i = (\<Sum>x\<in>d. if x = i then f x else 0)" |
120 unfolding euclidean_component_setsum euclidean_component_scaleR basis_component * |
120 unfolding euclidean_component_setsum euclidean_component_scaleR basis_component * |
121 apply(rule setsum_cong2) using assms by auto |
121 apply(rule setsum_cong2) using assms by auto |
122 show ?thesis unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto |
122 show ?thesis unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto |
123 qed |
123 qed |
1317 unfolding setsum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f] |
1317 unfolding setsum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f] |
1318 unfolding f using setsum_cong2[of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"] |
1318 unfolding f using setsum_cong2[of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"] |
1319 using setsum_cong2 [of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto |
1319 using setsum_cong2 [of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto |
1320 |
1320 |
1321 ultimately have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> setsum u {1..k} = 1 \<and> (\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y" |
1321 ultimately have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> setsum u {1..k} = 1 \<and> (\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y" |
1322 apply(rule_tac x="card s" in exI) apply(rule_tac x="u \<circ> f" in exI) apply(rule_tac x=f in exI) by fastsimp |
1322 apply(rule_tac x="card s" in exI) apply(rule_tac x="u \<circ> f" in exI) apply(rule_tac x=f in exI) by fastforce |
1323 hence "y \<in> ?lhs" unfolding convex_hull_indexed by auto } |
1323 hence "y \<in> ?lhs" unfolding convex_hull_indexed by auto } |
1324 ultimately show ?thesis unfolding set_eq_iff by blast |
1324 ultimately show ?thesis unfolding set_eq_iff by blast |
1325 qed |
1325 qed |
1326 |
1326 |
1327 subsubsection {* A stepping theorem for that expansion *} |
1327 subsubsection {* A stepping theorem for that expansion *} |
2882 lemma closest_point_lt: |
2882 lemma closest_point_lt: |
2883 assumes "convex s" "closed s" "x \<in> s" "x \<noteq> closest_point s a" |
2883 assumes "convex s" "closed s" "x \<in> s" "x \<noteq> closest_point s a" |
2884 shows "dist a (closest_point s a) < dist a x" |
2884 shows "dist a (closest_point s a) < dist a x" |
2885 apply(rule ccontr) apply(rule_tac notE[OF assms(4)]) |
2885 apply(rule ccontr) apply(rule_tac notE[OF assms(4)]) |
2886 apply(rule closest_point_unique[OF assms(1-3), of a]) |
2886 apply(rule closest_point_unique[OF assms(1-3), of a]) |
2887 using closest_point_le[OF assms(2), of _ a] by fastsimp |
2887 using closest_point_le[OF assms(2), of _ a] by fastforce |
2888 |
2888 |
2889 lemma closest_point_lipschitz: |
2889 lemma closest_point_lipschitz: |
2890 assumes "convex s" "closed s" "s \<noteq> {}" |
2890 assumes "convex s" "closed s" "s \<noteq> {}" |
2891 shows "dist (closest_point s x) (closest_point s y) \<le> dist x y" |
2891 shows "dist (closest_point s x) (closest_point s y) \<le> dist x y" |
2892 proof- |
2892 proof- |
4227 have "!i. ((0<x$$i) | (0=x$$i) --> 0<=x$$i)" by auto |
4227 have "!i. ((0<x$$i) | (0=x$$i) --> 0<=x$$i)" by auto |
4228 moreover have "!i. (i:d) | (i ~: d)" by auto |
4228 moreover have "!i. (i:d) | (i ~: d)" by auto |
4229 ultimately |
4229 ultimately |
4230 have "!i. ( (ALL i:d. 0 < x$$i) & (ALL i. i ~: d --> x$$i = 0) ) --> 0 <= x$$i" by metis |
4230 have "!i. ( (ALL i:d. 0 < x$$i) & (ALL i. i ~: d --> x$$i = 0) ) --> 0 <= x$$i" by metis |
4231 hence h2: "x : convex hull (insert 0 ?p)" using as assms |
4231 hence h2: "x : convex hull (insert 0 ?p)" using as assms |
4232 unfolding substd_simplex[OF assms] by fastsimp |
4232 unfolding substd_simplex[OF assms] by fastforce |
4233 obtain a where a:"a:d" using `d ~= {}` by auto |
4233 obtain a where a:"a:d" using `d ~= {}` by auto |
4234 let ?d = "(1 - setsum (op $$ x) d) / real (card d)" |
4234 let ?d = "(1 - setsum (op $$ x) d) / real (card d)" |
4235 have "0 < card d" using `d ~={}` `finite d` by (simp add: card_gt_0_iff) |
4235 have "0 < card d" using `d ~={}` `finite d` by (simp add: card_gt_0_iff) |
4236 have "Min ((op $$ x) ` d) > 0" using as `d \<noteq> {}` `finite d` by (simp add: Min_grI) |
4236 have "Min ((op $$ x) ` d) > 0" using as `d \<noteq> {}` `finite d` by (simp add: Min_grI) |
4237 moreover have "?d > 0" apply(rule divide_pos_pos) using as using `0 < card d` by auto |
4237 moreover have "?d > 0" apply(rule divide_pos_pos) using as using `0 < card d` by auto |