--- a/src/HOL/Analysis/Convex.thy Wed Jan 16 16:50:35 2019 -0500
+++ b/src/HOL/Analysis/Convex.thy Wed Jan 16 18:14:02 2019 -0500
@@ -14,79 +14,6 @@
"HOL-Library.Set_Algebras"
begin
-lemma substdbasis_expansion_unique:
- assumes d: "d \<subseteq> Basis"
- shows "(\<Sum>i\<in>d. f i *\<^sub>R i) = (x::'a::euclidean_space) \<longleftrightarrow>
- (\<forall>i\<in>Basis. (i \<in> d \<longrightarrow> f i = x \<bullet> i) \<and> (i \<notin> d \<longrightarrow> x \<bullet> i = 0))"
-proof -
- have *: "\<And>x a b P. x * (if P then a else b) = (if P then x * a else x * b)"
- by auto
- have **: "finite d"
- by (auto intro: finite_subset[OF assms])
- have ***: "\<And>i. i \<in> Basis \<Longrightarrow> (\<Sum>i\<in>d. f i *\<^sub>R i) \<bullet> i = (\<Sum>x\<in>d. if x = i then f x else 0)"
- using d
- by (auto intro!: sum.cong simp: inner_Basis inner_sum_left)
- show ?thesis
- unfolding euclidean_eq_iff[where 'a='a] by (auto simp: sum.delta[OF **] ***)
-qed
-
-lemma independent_substdbasis: "d \<subseteq> Basis \<Longrightarrow> independent d"
- by (rule independent_mono[OF independent_Basis])
-
-lemma sum_not_0: "sum f A \<noteq> 0 \<Longrightarrow> \<exists>a \<in> A. f a \<noteq> 0"
- by (rule ccontr) auto
-
-lemma subset_translation_eq [simp]:
- fixes a :: "'a::real_vector" shows "(+) a ` s \<subseteq> (+) a ` t \<longleftrightarrow> s \<subseteq> t"
- by auto
-
-lemma translate_inj_on:
- fixes A :: "'a::ab_group_add set"
- shows "inj_on (\<lambda>x. a + x) A"
- unfolding inj_on_def by auto
-
-lemma translation_assoc:
- fixes a b :: "'a::ab_group_add"
- shows "(\<lambda>x. b + x) ` ((\<lambda>x. a + x) ` S) = (\<lambda>x. (a + b) + x) ` S"
- by auto
-
-lemma translation_invert:
- fixes a :: "'a::ab_group_add"
- assumes "(\<lambda>x. a + x) ` A = (\<lambda>x. a + x) ` B"
- shows "A = B"
-proof -
- have "(\<lambda>x. -a + x) ` ((\<lambda>x. a + x) ` A) = (\<lambda>x. - a + x) ` ((\<lambda>x. a + x) ` B)"
- using assms by auto
- then show ?thesis
- using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto
-qed
-
-lemma translation_galois:
- fixes a :: "'a::ab_group_add"
- shows "T = ((\<lambda>x. a + x) ` S) \<longleftrightarrow> S = ((\<lambda>x. (- a) + x) ` T)"
- using translation_assoc[of "-a" a S]
- apply auto
- using translation_assoc[of a "-a" T]
- apply auto
- done
-
-lemma translation_inverse_subset:
- assumes "((\<lambda>x. - a + x) ` V) \<le> (S :: 'n::ab_group_add set)"
- shows "V \<le> ((\<lambda>x. a + x) ` S)"
-proof -
- {
- fix x
- assume "x \<in> V"
- then have "x-a \<in> S" using assms by auto
- then have "x \<in> {a + v |v. v \<in> S}"
- apply auto
- apply (rule exI[of _ "x-a"], simp)
- done
- then have "x \<in> ((\<lambda>x. a+x) ` S)" by auto
- }
- then show ?thesis by auto
-qed
-
subsection \<open>Convexity\<close>
definition%important convex :: "'a::real_vector set \<Rightarrow> bool"