equal
deleted
inserted
replaced
8 imports |
8 imports |
9 Topology_Euclidean_Space |
9 Topology_Euclidean_Space |
10 "~~/src/HOL/Library/Convex" |
10 "~~/src/HOL/Library/Convex" |
11 "~~/src/HOL/Library/Set_Algebras" |
11 "~~/src/HOL/Library/Set_Algebras" |
12 begin |
12 begin |
|
13 |
|
14 (*FIXME move up e.g. to Library/Convex.thy, but requires the "support" primitive*) |
|
15 lemma convex_supp_setsum: |
|
16 assumes "convex S" and 1: "supp_setsum u I = 1" |
|
17 and "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> u i \<and> (u i = 0 \<or> f i \<in> S)" |
|
18 shows "supp_setsum (\<lambda>i. u i *\<^sub>R f i) I \<in> S" |
|
19 proof - |
|
20 have fin: "finite {i \<in> I. u i \<noteq> 0}" |
|
21 using 1 setsum.infinite by (force simp: supp_setsum_def support_def) |
|
22 then have eq: "supp_setsum(\<lambda>i. u i *\<^sub>R f i) I = |
|
23 setsum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}" |
|
24 by (force intro: setsum.mono_neutral_left simp: supp_setsum_def support_def) |
|
25 show ?thesis |
|
26 apply (simp add: eq) |
|
27 apply (rule convex_setsum [OF fin \<open>convex S\<close>]) |
|
28 using 1 assms apply (auto simp: supp_setsum_def support_def) |
|
29 done |
|
30 qed |
|
31 |
13 |
32 |
14 lemma dim_image_eq: |
33 lemma dim_image_eq: |
15 fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space" |
34 fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space" |
16 assumes lf: "linear f" |
35 assumes lf: "linear f" |
17 and fi: "inj_on f (span S)" |
36 and fi: "inj_on f (span S)" |