Loads of new material related to porting the Euler Polyhedron Formula from HOL Light
--- a/src/HOL/Analysis/Convex.thy Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Analysis/Convex.thy Sat Sep 09 19:26:08 2023 +0100
@@ -1773,6 +1773,368 @@
shows "cone (convex hull S)"
by (metis (no_types, lifting) affine_hull_convex_hull affine_hull_eq_empty assms cone_iff convex_hull_scaling hull_inc)
+section \<open>Conic sets and conic hull\<close>
+
+definition conic :: "'a::real_vector set \<Rightarrow> bool"
+ where "conic S \<equiv> \<forall>x c. x \<in> S \<longrightarrow> 0 \<le> c \<longrightarrow> (c *\<^sub>R x) \<in> S"
+
+lemma conicD: "\<lbrakk>conic S; x \<in> S; 0 \<le> c\<rbrakk> \<Longrightarrow> (c *\<^sub>R x) \<in> S"
+ by (meson conic_def)
+
+lemma subspace_imp_conic: "subspace S \<Longrightarrow> conic S"
+ by (simp add: conic_def subspace_def)
+
+lemma conic_empty [simp]: "conic {}"
+ using conic_def by blast
+
+lemma conic_UNIV: "conic UNIV"
+ by (simp add: conic_def)
+
+lemma conic_Inter: "(\<And>S. S \<in> \<F> \<Longrightarrow> conic S) \<Longrightarrow> conic(\<Inter>\<F>)"
+ by (simp add: conic_def)
+
+lemma conic_linear_image:
+ "\<lbrakk>conic S; linear f\<rbrakk> \<Longrightarrow> conic(f ` S)"
+ by (smt (verit) conic_def image_iff linear.scaleR)
+
+lemma conic_linear_image_eq:
+ "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> conic (f ` S) \<longleftrightarrow> conic S"
+ by (smt (verit) conic_def conic_linear_image inj_image_mem_iff linear_cmul)
+
+lemma conic_mul: "\<lbrakk>conic S; x \<in> S; 0 \<le> c\<rbrakk> \<Longrightarrow> (c *\<^sub>R x) \<in> S"
+ using conic_def by blast
+
+lemma conic_conic_hull: "conic(conic hull S)"
+ by (metis (no_types, lifting) conic_Inter hull_def mem_Collect_eq)
+
+lemma conic_hull_eq: "(conic hull S = S) \<longleftrightarrow> conic S"
+ by (metis conic_conic_hull hull_same)
+
+lemma conic_hull_UNIV [simp]: "conic hull UNIV = UNIV"
+ by simp
+
+lemma conic_negations: "conic S \<Longrightarrow> conic (image uminus S)"
+ by (auto simp: conic_def image_iff)
+
+lemma conic_span [iff]: "conic(span S)"
+ by (simp add: subspace_imp_conic)
+
+lemma conic_hull_explicit:
+ "conic hull S = {c *\<^sub>R x| c x. 0 \<le> c \<and> x \<in> S}"
+ proof (rule hull_unique)
+ show "S \<subseteq> {c *\<^sub>R x |c x. 0 \<le> c \<and> x \<in> S}"
+ by (metis (no_types) cone_hull_expl hull_subset)
+ show "conic {c *\<^sub>R x |c x. 0 \<le> c \<and> x \<in> S}"
+ using mult_nonneg_nonneg by (force simp: conic_def)
+qed (auto simp: conic_def)
+
+lemma conic_hull_as_image:
+ "conic hull S = (\<lambda>z. fst z *\<^sub>R snd z) ` ({0..} \<times> S)"
+ by (force simp: conic_hull_explicit)
+
+lemma conic_hull_linear_image:
+ "linear f \<Longrightarrow> conic hull f ` S = f ` (conic hull S)"
+ by (force simp: conic_hull_explicit image_iff set_eq_iff linear_scale)
+
+lemma conic_hull_image_scale:
+ assumes "\<And>x. x \<in> S \<Longrightarrow> 0 < c x"
+ shows "conic hull (\<lambda>x. c x *\<^sub>R x) ` S = conic hull S"
+proof
+ show "conic hull (\<lambda>x. c x *\<^sub>R x) ` S \<subseteq> conic hull S"
+ proof (rule hull_minimal)
+ show "(\<lambda>x. c x *\<^sub>R x) ` S \<subseteq> conic hull S"
+ using assms conic_hull_explicit by fastforce
+ qed (simp add: conic_conic_hull)
+ show "conic hull S \<subseteq> conic hull (\<lambda>x. c x *\<^sub>R x) ` S"
+ proof (rule hull_minimal)
+ show "S \<subseteq> conic hull (\<lambda>x. c x *\<^sub>R x) ` S"
+ proof clarsimp
+ fix x
+ assume "x \<in> S"
+ then have "x = inverse(c x) *\<^sub>R c x *\<^sub>R x"
+ using assms by fastforce
+ then show "x \<in> conic hull (\<lambda>x. c x *\<^sub>R x) ` S"
+ by (smt (verit, best) \<open>x \<in> S\<close> assms conic_conic_hull conic_mul hull_inc image_eqI inverse_nonpositive_iff_nonpositive)
+ qed
+ qed (simp add: conic_conic_hull)
+qed
+
+lemma convex_conic_hull:
+ assumes "convex S"
+ shows "convex (conic hull S)"
+proof (clarsimp simp add: conic_hull_explicit convex_alt)
+ fix c x d y and u :: real
+ assume \<section>: "(0::real) \<le> c" "x \<in> S" "(0::real) \<le> d" "y \<in> S" "0 \<le> u" "u \<le> 1"
+ show "\<exists>c'' x''. ((1 - u) * c) *\<^sub>R x + (u * d) *\<^sub>R y = c'' *\<^sub>R x'' \<and> 0 \<le> c'' \<and> x'' \<in> S"
+ proof (cases "(1 - u) * c = 0")
+ case True
+ with \<open>0 \<le> d\<close> \<open>y \<in> S\<close>\<open>0 \<le> u\<close>
+ show ?thesis by force
+ next
+ case False
+ define \<xi> where "\<xi> \<equiv> (1 - u) * c + u * d"
+ have *: "c * u \<le> c"
+ by (simp add: "\<section>" mult_left_le)
+ have "\<xi> > 0"
+ using False \<section> by (smt (verit, best) \<xi>_def split_mult_pos_le)
+ then have **: "c + d * u = \<xi> + c * u"
+ by (simp add: \<xi>_def mult.commute right_diff_distrib')
+ show ?thesis
+ proof (intro exI conjI)
+ show "0 \<le> \<xi>"
+ using \<open>0 < \<xi>\<close> by auto
+ show "((1 - u) * c) *\<^sub>R x + (u * d) *\<^sub>R y = \<xi> *\<^sub>R (((1 - u) * c / \<xi>) *\<^sub>R x + (u * d / \<xi>) *\<^sub>R y)"
+ using \<open>\<xi> > 0\<close> by (simp add: algebra_simps diff_divide_distrib)
+ show "((1 - u) * c / \<xi>) *\<^sub>R x + (u * d / \<xi>) *\<^sub>R y \<in> S"
+ using \<open>0 < \<xi>\<close>
+ by (intro convexD [OF assms]) (auto simp: \<section> field_split_simps * **)
+ qed
+ qed
+qed
+
+lemma conic_halfspace_le: "conic {x. a \<bullet> x \<le> 0}"
+ by (auto simp: conic_def mult_le_0_iff)
+
+lemma conic_halfspace_ge: "conic {x. a \<bullet> x \<ge> 0}"
+ by (auto simp: conic_def mult_le_0_iff)
+
+lemma conic_hull_empty [simp]: "conic hull {} = {}"
+ by (simp add: conic_hull_eq)
+
+lemma conic_contains_0: "conic S \<Longrightarrow> (0 \<in> S \<longleftrightarrow> S \<noteq> {})"
+ by (simp add: Convex.cone_def cone_contains_0 conic_def)
+
+lemma conic_hull_eq_empty: "conic hull S = {} \<longleftrightarrow> (S = {})"
+ using conic_hull_explicit by fastforce
+
+lemma conic_sums: "\<lbrakk>conic S; conic T\<rbrakk> \<Longrightarrow> conic (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})"
+ by (simp add: conic_def) (metis scaleR_right_distrib)
+
+lemma conic_Times: "\<lbrakk>conic S; conic T\<rbrakk> \<Longrightarrow> conic(S \<times> T)"
+ by (auto simp: conic_def)
+
+lemma conic_Times_eq:
+ "conic(S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> conic S \<and> conic T" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ by (force simp: conic_def)
+ show "?rhs \<Longrightarrow> ?lhs"
+ by (force simp: conic_Times)
+qed
+
+lemma conic_hull_0 [simp]: "conic hull {0} = {0}"
+ by (simp add: conic_hull_eq subspace_imp_conic)
+
+lemma conic_hull_contains_0 [simp]: "0 \<in> conic hull S \<longleftrightarrow> (S \<noteq> {})"
+ by (simp add: conic_conic_hull conic_contains_0 conic_hull_eq_empty)
+
+lemma conic_hull_eq_sing:
+ "conic hull S = {x} \<longleftrightarrow> S = {0} \<and> x = 0"
+proof
+ show "conic hull S = {x} \<Longrightarrow> S = {0} \<and> x = 0"
+ by (metis conic_conic_hull conic_contains_0 conic_def conic_hull_eq hull_inc insert_not_empty singleton_iff)
+qed simp
+
+lemma conic_hull_Int_affine_hull:
+ assumes "T \<subseteq> S" "0 \<notin> affine hull S"
+ shows "(conic hull T) \<inter> (affine hull S) = T"
+proof -
+ have TaffS: "T \<subseteq> affine hull S"
+ using \<open>T \<subseteq> S\<close> hull_subset by fastforce
+ moreover
+ have "conic hull T \<inter> affine hull S \<subseteq> T"
+ proof (clarsimp simp: conic_hull_explicit)
+ fix c x
+ assume "c *\<^sub>R x \<in> affine hull S"
+ and "0 \<le> c"
+ and "x \<in> T"
+ show "c *\<^sub>R x \<in> T"
+ proof (cases "c=1")
+ case True
+ then show ?thesis
+ by (simp add: \<open>x \<in> T\<close>)
+ next
+ case False
+ then have "x /\<^sub>R (1 - c) = x + (c * inverse (1 - c)) *\<^sub>R x"
+ by (smt (verit, ccfv_SIG) diff_add_cancel mult.commute real_vector_affinity_eq scaleR_collapse scaleR_scaleR)
+ then have "0 = inverse(1 - c) *\<^sub>R c *\<^sub>R x + (1 - inverse(1 - c)) *\<^sub>R x"
+ by (simp add: algebra_simps)
+ then have "0 \<in> affine hull S"
+ by (smt (verit) \<open>c *\<^sub>R x \<in> affine hull S\<close> \<open>x \<in> T\<close> affine_affine_hull TaffS in_mono mem_affine)
+ then show ?thesis
+ using assms by auto
+ qed
+ qed
+ ultimately show ?thesis
+ by (auto simp: hull_inc)
+qed
+
+
+section \<open>Convex cones and corresponding hulls\<close>
+
+definition convex_cone :: "'a::real_vector set \<Rightarrow> bool"
+ where "convex_cone \<equiv> \<lambda>S. S \<noteq> {} \<and> convex S \<and> conic S"
+
+lemma convex_cone_iff:
+ "convex_cone S \<longleftrightarrow>
+ 0 \<in> S \<and> (\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S) \<and> (\<forall>x \<in> S. \<forall>c\<ge>0. c *\<^sub>R x \<in> S)"
+ by (metis cone_def conic_contains_0 conic_def convex_cone convex_cone_def)
+
+lemma convex_cone_add: "\<lbrakk>convex_cone S; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x+y \<in> S"
+ by (simp add: convex_cone_iff)
+
+lemma convex_cone_scaleR: "\<lbrakk>convex_cone S; 0 \<le> c; x \<in> S\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> S"
+ by (simp add: convex_cone_iff)
+
+lemma convex_cone_nonempty: "convex_cone S \<Longrightarrow> S \<noteq> {}"
+ by (simp add: convex_cone_def)
+
+lemma convex_cone_linear_image:
+ "convex_cone S \<and> linear f \<Longrightarrow> convex_cone(f ` S)"
+ by (simp add: conic_linear_image convex_cone_def convex_linear_image)
+
+lemma convex_cone_linear_image_eq:
+ "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> (convex_cone(f ` S) \<longleftrightarrow> convex_cone S)"
+ by (simp add: conic_linear_image_eq convex_cone_def)
+
+lemma convex_cone_halfspace_ge: "convex_cone {x. a \<bullet> x \<ge> 0}"
+ by (simp add: convex_cone_iff inner_simps(2))
+
+lemma convex_cone_halfspace_le: "convex_cone {x. a \<bullet> x \<le> 0}"
+ by (simp add: convex_cone_iff inner_right_distrib mult_nonneg_nonpos)
+
+lemma convex_cone_contains_0: "convex_cone S \<Longrightarrow> 0 \<in> S"
+ using convex_cone_iff by blast
+
+lemma convex_cone_Inter:
+ "(\<And>S. S \<in> f \<Longrightarrow> convex_cone S) \<Longrightarrow> convex_cone(\<Inter> f)"
+ by (simp add: convex_cone_iff)
+
+lemma convex_cone_convex_cone_hull: "convex_cone(convex_cone hull S)"
+ by (metis (no_types, lifting) convex_cone_Inter hull_def mem_Collect_eq)
+
+lemma convex_convex_cone_hull: "convex(convex_cone hull S)"
+ by (meson convex_cone_convex_cone_hull convex_cone_def)
+
+lemma conic_convex_cone_hull: "conic(convex_cone hull S)"
+ by (metis convex_cone_convex_cone_hull convex_cone_def)
+
+lemma convex_cone_hull_nonempty: "convex_cone hull S \<noteq> {}"
+ by (simp add: convex_cone_convex_cone_hull convex_cone_nonempty)
+
+lemma convex_cone_hull_contains_0: "0 \<in> convex_cone hull S"
+ by (simp add: convex_cone_contains_0 convex_cone_convex_cone_hull)
+
+lemma convex_cone_hull_add:
+ "\<lbrakk>x \<in> convex_cone hull S; y \<in> convex_cone hull S\<rbrakk> \<Longrightarrow> x + y \<in> convex_cone hull S"
+ by (simp add: convex_cone_add convex_cone_convex_cone_hull)
+
+lemma convex_cone_hull_mul:
+ "\<lbrakk>x \<in> convex_cone hull S; 0 \<le> c\<rbrakk> \<Longrightarrow> (c *\<^sub>R x) \<in> convex_cone hull S"
+ by (simp add: conic_convex_cone_hull conic_mul)
+
+thm convex_sums
+lemma convex_cone_sums:
+ "\<lbrakk>convex_cone S; convex_cone T\<rbrakk> \<Longrightarrow> convex_cone (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})"
+ by (simp add: convex_cone_def conic_sums convex_sums)
+
+lemma convex_cone_Times:
+ "\<lbrakk>convex_cone S; convex_cone T\<rbrakk> \<Longrightarrow> convex_cone(S \<times> T)"
+ by (simp add: conic_Times convex_Times convex_cone_def)
+
+lemma convex_cone_Times_D1: "convex_cone (S \<times> T) \<Longrightarrow> convex_cone S"
+ by (metis Times_empty conic_Times_eq convex_cone_def convex_convex_hull convex_hull_Times hull_same times_eq_iff)
+
+lemma convex_cone_Times_eq:
+ "convex_cone(S \<times> T) \<longleftrightarrow> convex_cone S \<and> convex_cone T"
+proof (cases "S={} \<or> T={}")
+ case True
+ then show ?thesis
+ by (auto dest: convex_cone_nonempty)
+next
+ case False
+ then have "convex_cone (S \<times> T) \<Longrightarrow> convex_cone T"
+ by (metis conic_Times_eq convex_cone_def convex_convex_hull convex_hull_Times hull_same times_eq_iff)
+ then show ?thesis
+ using convex_cone_Times convex_cone_Times_D1 by blast
+qed
+
+
+lemma convex_cone_hull_Un:
+ "convex_cone hull(S \<union> T) = (\<Union>x \<in> convex_cone hull S. \<Union>y \<in> convex_cone hull T. {x + y})"
+ (is "?lhs = ?rhs")
+proof
+ show "?lhs \<subseteq> ?rhs"
+ proof (rule hull_minimal)
+ show "S \<union> T \<subseteq> (\<Union>x\<in>convex_cone hull S. \<Union>y\<in>convex_cone hull T. {x + y})"
+ apply (clarsimp simp: subset_iff)
+ by (metis add_0 convex_cone_hull_contains_0 group_cancel.rule0 hull_inc)
+ show "convex_cone (\<Union>x\<in>convex_cone hull S. \<Union>y\<in>convex_cone hull T. {x + y})"
+ by (simp add: convex_cone_convex_cone_hull convex_cone_sums)
+ qed
+next
+ show "?rhs \<subseteq> ?lhs"
+ by clarify (metis convex_cone_hull_add hull_mono le_sup_iff subsetD subsetI)
+qed
+
+lemma convex_cone_singleton [iff]: "convex_cone {0}"
+ by (simp add: convex_cone_iff)
+
+lemma convex_hull_subset_convex_cone_hull:
+ "convex hull S \<subseteq> convex_cone hull S"
+ by (simp add: convex_convex_cone_hull hull_minimal hull_subset)
+
+lemma conic_hull_subset_convex_cone_hull:
+ "conic hull S \<subseteq> convex_cone hull S"
+ by (simp add: conic_convex_cone_hull hull_minimal hull_subset)
+
+lemma subspace_imp_convex_cone: "subspace S \<Longrightarrow> convex_cone S"
+ by (simp add: convex_cone_iff subspace_def)
+
+lemma convex_cone_span: "convex_cone(span S)"
+ by (simp add: subspace_imp_convex_cone)
+
+lemma convex_cone_negations:
+ "convex_cone S \<Longrightarrow> convex_cone (image uminus S)"
+ by (simp add: convex_cone_linear_image module_hom_uminus)
+
+lemma subspace_convex_cone_symmetric:
+ "subspace S \<longleftrightarrow> convex_cone S \<and> (\<forall>x \<in> S. -x \<in> S)"
+ by (smt (verit) convex_cone_iff scaleR_left.minus subspace_def subspace_neg)
+
+lemma convex_cone_hull_separate_nonempty:
+ assumes "S \<noteq> {}"
+ shows "convex_cone hull S = conic hull (convex hull S)" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<subseteq> ?rhs"
+ by (metis assms conic_conic_hull convex_cone_def convex_conic_hull convex_convex_hull hull_subset subset_empty subset_hull)
+ show "?rhs \<subseteq> ?lhs"
+ by (simp add: conic_convex_cone_hull convex_hull_subset_convex_cone_hull subset_hull)
+qed
+
+lemma convex_cone_hull_empty [simp]: "convex_cone hull {} = {0}"
+ by (metis convex_cone_hull_contains_0 convex_cone_singleton hull_redundant hull_same)
+
+lemma convex_cone_hull_separate:
+ "convex_cone hull S = insert 0 (conic hull (convex hull S))"
+proof(cases "S={}")
+ case False
+ then show ?thesis
+ using convex_cone_hull_contains_0 convex_cone_hull_separate_nonempty by blast
+qed auto
+
+lemma convex_cone_hull_convex_hull_nonempty:
+ "S \<noteq> {} \<Longrightarrow> convex_cone hull S = (\<Union>x \<in> convex hull S. \<Union>c\<in>{0..}. {c *\<^sub>R x})"
+ by (force simp: convex_cone_hull_separate_nonempty conic_hull_as_image)
+
+lemma convex_cone_hull_convex_hull:
+ "convex_cone hull S = insert 0 (\<Union>x \<in> convex hull S. \<Union>c\<in>{0..}. {c *\<^sub>R x})"
+ by (force simp: convex_cone_hull_separate conic_hull_as_image)
+
+lemma convex_cone_hull_linear_image:
+ "linear f \<Longrightarrow> convex_cone hull (f ` S) = image f (convex_cone hull S)"
+ by (metis (no_types, lifting) conic_hull_linear_image convex_cone_hull_separate convex_hull_linear_image image_insert linear_0)
+
subsection \<open>Radon's theorem\<close>
text "Formalized by Lars Schewe."
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Sat Sep 09 19:26:08 2023 +0100
@@ -1092,11 +1092,6 @@
shows "lebesgue = density (distr lebesgue lebesgue (\<lambda>x. c * x)) (\<lambda>x. ennreal \<bar>c\<bar>)"
using assms by (subst lebesgue_affine_euclidean[of "\<lambda>_. c" 0]) simp_all
-lemma divideR_right:
- fixes x y :: "'a::real_normed_vector"
- shows "r \<noteq> 0 \<Longrightarrow> y = x /\<^sub>R r \<longleftrightarrow> r *\<^sub>R y = x"
- using scaleR_cancel_left[of r y "x /\<^sub>R r"] by simp
-
lemma lborel_has_bochner_integral_real_affine_iff:
fixes x :: "'a :: {banach, second_countable_topology}"
shows "c \<noteq> 0 \<Longrightarrow>
--- a/src/HOL/Analysis/Linear_Algebra.thy Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Sat Sep 09 19:26:08 2023 +0100
@@ -704,7 +704,7 @@
text \<open>Low-dimensional subset is in a hyperplane (weak orthogonal complement).\<close>
-lemma span_not_univ_orthogonal:
+lemma span_not_UNIV_orthogonal:
fixes S :: "'a::euclidean_space set"
assumes sU: "span S \<noteq> UNIV"
shows "\<exists>a::'a. a \<noteq> 0 \<and> (\<forall>x \<in> span S. a \<bullet> x = 0)"
@@ -754,7 +754,7 @@
fixes S :: "'a::euclidean_space set"
assumes SU: "span S \<noteq> UNIV"
shows "\<exists> a. a \<noteq>0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"
- using span_not_univ_orthogonal[OF SU] by auto
+ using span_not_UNIV_orthogonal[OF SU] by auto
lemma lowdim_subset_hyperplane:
fixes S :: "'a::euclidean_space set"
--- a/src/HOL/Analysis/Polytope.thy Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Analysis/Polytope.thy Sat Sep 09 19:26:08 2023 +0100
@@ -28,8 +28,12 @@
lemma face_of_linear_image:
assumes "linear f" "inj f"
- shows "(f ` c face_of f ` S) \<longleftrightarrow> c face_of S"
-by (simp add: face_of_def inj_image_subset_iff inj_image_mem_iff open_segment_linear_image assms)
+ shows "(f ` c face_of f ` S) \<longleftrightarrow> c face_of S"
+ by (simp add: face_of_def inj_image_subset_iff inj_image_mem_iff open_segment_linear_image assms)
+
+lemma faces_of_linear_image:
+ "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> {T. T face_of (f ` S)} = (image f) ` {T. T face_of S}"
+ by (smt (verit) Collect_cong face_of_def face_of_linear_image setcompr_eq_image subset_imageE)
lemma face_of_refl: "convex S \<Longrightarrow> S face_of S"
by (auto simp: face_of_def)
@@ -269,6 +273,39 @@
using \<open>affine S\<close> xy by (auto simp: affine_alt)
qed
+proposition face_of_conic:
+ assumes "conic S" "f face_of S"
+ shows "conic f"
+ unfolding conic_def
+proof (intro strip)
+ fix x and c::real
+ assume "x \<in> f" and "0 \<le> c"
+ have f: "\<And>a b x. \<lbrakk>a \<in> S; b \<in> S; x \<in> f; x \<in> open_segment a b\<rbrakk> \<Longrightarrow> a \<in> f \<and> b \<in> f"
+ using \<open>f face_of S\<close> face_ofD by blast
+ show "c *\<^sub>R x \<in> f"
+ proof (cases "x=0 \<or> c=1")
+ case True
+ then show ?thesis
+ using \<open>x \<in> f\<close> by auto
+ next
+ case False
+ with \<open>0 \<le> c\<close> obtain d e where de: "0 \<le> d" "0 \<le> e" "d < 1" "1 < e" "d < e" "(d = c \<or> e = c)"
+ apply (simp add: neq_iff)
+ by (metis gt_ex less_eq_real_def order_less_le_trans zero_less_one)
+ then obtain [simp]: "c *\<^sub>R x \<in> S" "e *\<^sub>R x \<in> S" \<open>x \<in> S\<close>
+ using \<open>x \<in> f\<close> assms conic_mul face_of_imp_subset by blast
+ have "x \<in> open_segment (d *\<^sub>R x) (e *\<^sub>R x)" if "c *\<^sub>R x \<notin> f"
+ using de False that
+ apply (simp add: in_segment)
+ apply (rule_tac x="(1 - d) / (e - d)" in exI)
+ apply (simp add: field_simps)
+ by (smt (verit, del_insts) add_divide_distrib divide_self scaleR_collapse)
+ then show ?thesis
+ using \<open>conic S\<close> f [of "d *\<^sub>R x" "e *\<^sub>R x" x] de \<open>x \<in> f\<close>
+ by (force simp: conic_def in_segment)
+ qed
+qed
+
proposition face_of_convex_hulls:
assumes S: "finite S" "T \<subseteq> S" and disj: "affine hull T \<inter> convex hull (S - T) = {}"
shows "(convex hull T) face_of (convex hull S)"
@@ -927,6 +964,18 @@
by (auto simp: face_of_singleton hull_same)
qed (use assms in \<open>simp add: hull_inc\<close>)
+lemma extreme_point_of_conic:
+ assumes "conic S" and x: "x extreme_point_of S"
+ shows "x = 0"
+proof -
+ have "{x} face_of S"
+ by (simp add: face_of_singleton x)
+ then have "conic{x}"
+ using assms(1) face_of_conic by blast
+ then show ?thesis
+ by (force simp: conic_def)
+qed
+
subsection\<open>Facets\<close>
definition\<^marker>\<open>tag important\<close> facet_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
@@ -3826,5 +3875,135 @@
using that by (auto simp: in\<T>)
qed
qed
+section \<open>Finitely generated cone is polyhedral, and hence closed\<close>
+
+proposition polyhedron_convex_cone_hull:
+ fixes S :: "'a::euclidean_space set"
+ assumes "finite S"
+ shows "polyhedron(convex_cone hull S)"
+proof (cases "S = {}")
+ case True
+ then show ?thesis
+ by (simp add: affine_imp_polyhedron)
+next
+ case False
+ then have "polyhedron(convex hull (insert 0 S))"
+ by (simp add: assms polyhedron_convex_hull)
+ then obtain F a b where "finite F"
+ and F: "convex hull (insert 0 S) = \<Inter> F"
+ and ab: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
+ unfolding polyhedron_def by metis
+ then have "F \<noteq> {}"
+ by (metis bounded_convex_hull finite_imp_bounded Inf_empty assms finite_insert not_bounded_UNIV)
+ show ?thesis
+ unfolding polyhedron_def
+ proof (intro exI conjI)
+ show "convex_cone hull S = \<Inter> {h \<in> F. b h = 0}" (is "?lhs = ?rhs")
+ proof
+ show "?lhs \<subseteq> ?rhs"
+ proof (rule hull_minimal)
+ show "S \<subseteq> \<Inter> {h \<in> F. b h = 0}"
+ by (smt (verit, best) F InterE InterI hull_subset insert_subset mem_Collect_eq subset_eq)
+ have "\<And>S. \<lbrakk>S \<in> F; b S = 0\<rbrakk> \<Longrightarrow> convex_cone S"
+ by (metis ab convex_cone_halfspace_le)
+ then show "convex_cone (\<Inter> {h \<in> F. b h = 0})"
+ by (force intro: convex_cone_Inter)
+ qed
+ have "x \<in> convex_cone hull S"
+ if x: "\<And>h. \<lbrakk>h \<in> F; b h = 0\<rbrakk> \<Longrightarrow> x \<in> h" for x
+ proof -
+ have "\<exists>t. 0 < t \<and> (t *\<^sub>R x) \<in> h" if "h \<in> F" for h
+ proof (cases "b h = 0")
+ case True
+ then show ?thesis
+ by (metis x linordered_field_no_ub mult_1 scaleR_one that zero_less_mult_iff)
+ next
+ case False
+ then have "b h > 0"
+ by (smt (verit, del_insts) F InterE ab hull_subset inner_zero_right insert_subset mem_Collect_eq that)
+ then have "0 \<in> interior {x. a h \<bullet> x \<le> b h}"
+ by (simp add: ab that)
+ then have "0 \<in> interior h"
+ using ab that by auto
+ then obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball 0 \<epsilon> \<subseteq> h"
+ using mem_interior by blast
+ show ?thesis
+ proof (cases "x=0")
+ case True
+ then show ?thesis
+ using \<epsilon> \<open>0 < \<epsilon>\<close> by auto
+ next
+ case False
+ with \<epsilon> \<open>0 < \<epsilon>\<close> show ?thesis
+ by (rule_tac x="\<epsilon> / (2 * norm x)" in exI) (auto simp: divide_simps)
+ qed
+ qed
+ then obtain t where t: "\<And>h. h \<in> F \<Longrightarrow> 0 < t h \<and> (t h *\<^sub>R x) \<in> h"
+ by metis
+ then have "Inf (t ` F) *\<^sub>R x /\<^sub>R Inf (t ` F) = x"
+ by (smt (verit) \<open>F \<noteq> {}\<close> \<open>finite F\<close> divideR_right finite_imageI finite_less_Inf_iff image_iff image_is_empty)
+ moreover have "Inf (t ` F) *\<^sub>R x /\<^sub>R Inf (t ` F) \<in> convex_cone hull S"
+ proof (rule conicD [OF conic_convex_cone_hull])
+ have "Inf (t ` F) *\<^sub>R x \<in> \<Inter> F"
+ proof clarify
+ fix h
+ assume "h \<in> F"
+ have eq: "Inf (t ` F) *\<^sub>R x = (1 - Inf(t ` F) / t h) *\<^sub>R 0 + (Inf(t ` F) / t h) *\<^sub>R t h *\<^sub>R x"
+ using \<open>h \<in> F\<close> t by force
+ show "Inf (t ` F) *\<^sub>R x \<in> h"
+ unfolding eq
+ proof (rule convexD_alt)
+ have "h = {x. a h \<bullet> x \<le> b h}"
+ by (simp add: \<open>h \<in> F\<close> ab)
+ then show "convex h"
+ by (metis convex_halfspace_le)
+ show "0 \<in> h"
+ by (metis F InterE \<open>h \<in> F\<close> hull_subset insertCI subsetD)
+ show "t h *\<^sub>R x \<in> h"
+ by (simp add: \<open>h \<in> F\<close> t)
+ show "0 \<le> Inf (t ` F) / t h"
+ by (metis \<open>F \<noteq> {}\<close> \<open>h \<in> F\<close> cINF_greatest divide_nonneg_pos less_eq_real_def t)
+ show "Inf (t ` F) / t h \<le> 1"
+ by (simp add: \<open>finite F\<close> \<open>h \<in> F\<close> cInf_le_finite t)
+ qed
+ qed
+ moreover have "convex hull (insert 0 S) \<subseteq> convex_cone hull S"
+ by (simp add: convex_cone_hull_contains_0 convex_convex_cone_hull hull_minimal hull_subset)
+ ultimately show "Inf (t ` F) *\<^sub>R x \<in> convex_cone hull S"
+ using F by blast
+ show "0 \<le> inverse (Inf (t ` F))"
+ using t by (simp add: \<open>F \<noteq> {}\<close> \<open>finite F\<close> finite_less_Inf_iff less_eq_real_def)
+ qed
+ ultimately show ?thesis
+ by auto
+ qed
+ then show "?rhs \<subseteq> ?lhs"
+ by auto
+ qed
+ show "\<forall>h\<in>{h \<in> F. b h = 0}. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
+ using ab by blast
+ qed (auto simp: \<open>finite F\<close>)
+qed
+
+
+lemma closed_convex_cone_hull:
+ fixes S :: "'a::euclidean_space set"
+ shows "finite S \<Longrightarrow> closed(convex_cone hull S)"
+ by (simp add: polyhedron_convex_cone_hull polyhedron_imp_closed)
+
+lemma polyhedron_convex_cone_hull_polytope:
+ fixes S :: "'a::euclidean_space set"
+ shows "polytope S \<Longrightarrow> polyhedron(convex_cone hull S)"
+ by (metis convex_cone_hull_separate hull_hull polyhedron_convex_cone_hull polytope_def)
+
+lemma polyhedron_conic_hull_polytope:
+ fixes S :: "'a::euclidean_space set"
+ shows "polytope S \<Longrightarrow> polyhedron(conic hull S)"
+ by (metis conic_hull_eq_empty convex_cone_hull_separate_nonempty hull_hull polyhedron_convex_cone_hull_polytope polyhedron_empty polytope_def)
+
+lemma closed_conic_hull_strong:
+ fixes S :: "'a::euclidean_space set"
+ shows "0 \<in> rel_interior S \<or> polytope S \<or> compact S \<and> ~(0 \<in> S) \<Longrightarrow> closed(conic hull S)"
+ using closed_conic_hull polyhedron_conic_hull_polytope polyhedron_imp_closed by blast
end
--- a/src/HOL/Analysis/Starlike.thy Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Analysis/Starlike.thy Sat Sep 09 19:26:08 2023 +0100
@@ -214,6 +214,84 @@
by (simp add: closure_mono interior_subset subset_antisym)
qed
+lemma openin_subset_relative_interior:
+ fixes S :: "'a::euclidean_space set"
+ shows "openin (top_of_set (affine hull T)) S \<Longrightarrow> (S \<subseteq> rel_interior T) = (S \<subseteq> T)"
+ by (meson order.trans rel_interior_maximal rel_interior_subset)
+
+lemma conic_hull_eq_span_affine_hull:
+ fixes S :: "'a::euclidean_space set"
+ assumes "0 \<in> rel_interior S"
+ shows "conic hull S = span S \<and> conic hull S = affine hull S"
+proof -
+ obtain \<epsilon> where "\<epsilon>>0" and \<epsilon>: "cball 0 \<epsilon> \<inter> affine hull S \<subseteq> S"
+ using assms mem_rel_interior_cball by blast
+ have *: "affine hull S = span S"
+ by (meson affine_hull_span_0 assms hull_inc mem_rel_interior_cball)
+ moreover
+ have "conic hull S \<subseteq> span S"
+ by (simp add: hull_minimal span_superset)
+ moreover
+ have "affine hull S \<subseteq> conic hull S"
+ proof clarsimp
+ fix x
+ assume "x \<in> affine hull S"
+ show "x \<in> conic hull S"
+ proof (cases "x=0")
+ case True
+ then show ?thesis
+ using \<open>x \<in> affine hull S\<close> by auto
+ next
+ case False
+ then have "(\<epsilon> / norm x) *\<^sub>R x \<in> cball 0 \<epsilon> \<inter> affine hull S"
+ using \<open>0 < \<epsilon>\<close> \<open>x \<in> affine hull S\<close> * span_mul by fastforce
+ then have "(\<epsilon> / norm x) *\<^sub>R x \<in> S"
+ by (meson \<epsilon> subsetD)
+ then have "\<exists>c xa. x = c *\<^sub>R xa \<and> 0 \<le> c \<and> xa \<in> S"
+ by (smt (verit, del_insts) \<open>0 < \<epsilon>\<close> divide_nonneg_nonneg eq_vector_fraction_iff norm_eq_zero norm_ge_zero)
+ then show ?thesis
+ by (simp add: conic_hull_explicit)
+ qed
+ qed
+ ultimately show ?thesis
+ by blast
+qed
+
+lemma conic_hull_eq_span:
+ fixes S :: "'a::euclidean_space set"
+ assumes "0 \<in> rel_interior S"
+ shows "conic hull S = span S"
+ by (simp add: assms conic_hull_eq_span_affine_hull)
+
+lemma conic_hull_eq_affine_hull:
+ fixes S :: "'a::euclidean_space set"
+ assumes "0 \<in> rel_interior S"
+ shows "conic hull S = affine hull S"
+ using assms conic_hull_eq_span_affine_hull by blast
+
+lemma conic_hull_eq_span_eq:
+ fixes S :: "'a::euclidean_space set"
+ shows "0 \<in> rel_interior(conic hull S) \<longleftrightarrow> conic hull S = span S" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ by (metis conic_hull_eq_span conic_span hull_hull hull_minimal hull_subset span_eq)
+ show "?rhs \<Longrightarrow> ?lhs"
+ by (metis rel_interior_affine subspace_affine subspace_span)
+qed
+
+lemma aff_dim_psubset:
+ "(affine hull S) \<subset> (affine hull T) \<Longrightarrow> aff_dim S < aff_dim T"
+ by (metis aff_dim_affine_hull aff_dim_empty aff_dim_subset affine_affine_hull affine_dim_equal order_less_le)
+
+lemma aff_dim_eq_full_gen:
+ "S \<subseteq> T \<Longrightarrow> (aff_dim S = aff_dim T \<longleftrightarrow> affine hull S = affine hull T)"
+ by (smt (verit, del_insts) aff_dim_affine_hull2 aff_dim_psubset hull_mono psubsetI)
+
+lemma aff_dim_eq_full:
+ fixes S :: "'n::euclidean_space set"
+ shows "aff_dim S = (DIM('n)) \<longleftrightarrow> affine hull S = UNIV"
+ by (metis aff_dim_UNIV aff_dim_affine_hull affine_hull_UNIV)
+
lemma closure_convex_Int_superset:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "interior S \<noteq> {}" "interior S \<subseteq> closure T"
@@ -772,6 +850,61 @@
qed auto
qed
+lemma empty_interior_subset_hyperplane_aux:
+ fixes S :: "'a::euclidean_space set"
+ assumes "convex S" "0 \<in> S" and empty_int: "interior S = {}"
+ shows "\<exists>a b. a\<noteq>0 \<and> S \<subseteq> {x. a \<bullet> x = b}"
+proof -
+ have False if "\<And>a. a = 0 \<or> (\<forall>b. \<exists>T \<in> S. a \<bullet> T \<noteq> b)"
+ proof -
+ have rel_int: "rel_interior S \<noteq> {}"
+ using assms rel_interior_eq_empty by auto
+ moreover
+ have "dim S \<noteq> dim (UNIV::'a set)"
+ by (metis aff_dim_zero affine_hull_UNIV \<open>0 \<in> S\<close> dim_UNIV empty_int hull_inc rel_int rel_interior_interior)
+ then obtain a where "a \<noteq> 0" and a: "span S \<subseteq> {x. a \<bullet> x = 0}"
+ using lowdim_subset_hyperplane
+ by (metis dim_UNIV dim_subset_UNIV order_less_le)
+ have "span UNIV = span S"
+ by (metis span_base span_not_UNIV_orthogonal that)
+ then have "UNIV \<subseteq> affine hull S"
+ by (simp add: \<open>0 \<in> S\<close> hull_inc affine_hull_span_0)
+ ultimately show False
+ using \<open>rel_interior S \<noteq> {}\<close> empty_int rel_interior_interior by blast
+ qed
+ then show ?thesis
+ by blast
+qed
+
+lemma empty_interior_subset_hyperplane:
+ fixes S :: "'a::euclidean_space set"
+ assumes "convex S" and int: "interior S = {}"
+ obtains a b where "a \<noteq> 0" "S \<subseteq> {x. a \<bullet> x = b}"
+proof (cases "S = {}")
+ case True
+ then show ?thesis
+ using that by blast
+next
+ case False
+ then obtain u where "u \<in> S"
+ by blast
+ have "\<exists>a b. a \<noteq> 0 \<and> (\<lambda>x. x - u) ` S \<subseteq> {x. a \<bullet> x = b}"
+ proof (rule empty_interior_subset_hyperplane_aux)
+ show "convex ((\<lambda>x. x - u) ` S)"
+ using \<open>convex S\<close> by force
+ show "0 \<in> (\<lambda>x. x - u) ` S"
+ by (simp add: \<open>u \<in> S\<close>)
+ show "interior ((\<lambda>x. x - u) ` S) = {}"
+ by (simp add: int interior_translation_subtract)
+ qed
+ then obtain a b where "a \<noteq> 0" and ab: "(\<lambda>x. x - u) ` S \<subseteq> {x. a \<bullet> x = b}"
+ by metis
+ then have "S \<subseteq> {x. a \<bullet> x = b + (a \<bullet> u)}"
+ using ab by (auto simp: algebra_simps)
+ then show ?thesis
+ using \<open>a \<noteq> 0\<close> that by auto
+qed
+
lemma rel_interior_same_affine_hull:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
@@ -1327,118 +1460,119 @@
then show ?thesis by auto
qed
-lemma convex_closure_rel_interior_inter:
- assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
- and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
- shows "\<Inter>{closure S |S. S \<in> I} \<le> closure (\<Inter>{rel_interior S |S. S \<in> I})"
+lemma convex_closure_rel_interior_Int:
+ assumes "\<And>S. S\<in>\<F> \<Longrightarrow> convex (S :: 'n::euclidean_space set)"
+ and "\<Inter>(rel_interior ` \<F>) \<noteq> {}"
+ shows "\<Inter>(closure ` \<F>) \<subseteq> closure (\<Inter>(rel_interior ` \<F>))"
proof -
- obtain x where x: "\<forall>S\<in>I. x \<in> rel_interior S"
+ obtain x where x: "\<forall>S\<in>\<F>. x \<in> rel_interior S"
using assms by auto
- {
+ show ?thesis
+ proof
fix y
- assume "y \<in> \<Inter>{closure S |S. S \<in> I}"
- then have y: "\<forall>S \<in> I. y \<in> closure S"
- by auto
- {
- assume "y = x"
- then have "y \<in> closure (\<Inter>{rel_interior S |S. S \<in> I})"
- using x closure_subset[of "\<Inter>{rel_interior S |S. S \<in> I}"] by auto
- }
- moreover
- {
- assume "y \<noteq> x"
- { fix e :: real
- assume e: "e > 0"
- define e1 where "e1 = min 1 (e/norm (y - x))"
- then have e1: "e1 > 0" "e1 \<le> 1" "e1 * norm (y - x) \<le> e"
- using \<open>y \<noteq> x\<close> \<open>e > 0\<close> le_divide_eq[of e1 e "norm (y - x)"]
+ assume y: "y \<in> \<Inter> (closure ` \<F>)"
+ show "y \<in> closure (\<Inter>(rel_interior ` \<F>))"
+ proof (cases "y=x")
+ case True
+ with closure_subset x show ?thesis
+ by fastforce
+ next
+ case False
+ show ?thesis
+ proof (clarsimp simp: closure_approachable_le)
+ fix \<epsilon> :: real
+ assume e: "\<epsilon> > 0"
+ define e1 where "e1 = min 1 (\<epsilon>/norm (y - x))"
+ then have e1: "e1 > 0" "e1 \<le> 1" "e1 * norm (y - x) \<le> \<epsilon>"
+ using \<open>y \<noteq> x\<close> \<open>\<epsilon> > 0\<close> le_divide_eq[of e1 \<epsilon> "norm (y - x)"]
by simp_all
define z where "z = y - e1 *\<^sub>R (y - x)"
{
fix S
- assume "S \<in> I"
+ assume "S \<in> \<F>"
then have "z \<in> rel_interior S"
using rel_interior_closure_convex_shrink[of S x y e1] assms x y e1 z_def
by auto
}
- then have *: "z \<in> \<Inter>{rel_interior S |S. S \<in> I}"
+ then have *: "z \<in> \<Inter>(rel_interior ` \<F>)"
by auto
- have "\<exists>z. z \<in> \<Inter>{rel_interior S |S. S \<in> I} \<and> z \<noteq> y \<and> dist z y \<le> e"
+ show "\<exists>x\<in>\<Inter> (rel_interior ` \<F>). dist x y \<le> \<epsilon>"
using \<open>y \<noteq> x\<close> z_def * e1 e dist_norm[of z y]
- by (rule_tac x="z" in exI) auto
- }
- then have "y islimpt \<Inter>{rel_interior S |S. S \<in> I}"
- unfolding islimpt_approachable_le by blast
- then have "y \<in> closure (\<Inter>{rel_interior S |S. S \<in> I})"
- unfolding closure_def by auto
- }
- ultimately have "y \<in> closure (\<Inter>{rel_interior S |S. S \<in> I})"
- by auto
- }
- then show ?thesis by auto
-qed
-
-lemma convex_closure_inter:
- assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
- and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
- shows "closure (\<Inter>I) = \<Inter>{closure S |S. S \<in> I}"
+ by force
+ qed
+ qed
+ qed
+qed
+
+
+lemma closure_Inter_convex:
+ fixes \<F> :: "'n::euclidean_space set set"
+ assumes "\<And>S. S \<in> \<F> \<Longrightarrow> convex S" and "\<Inter>(rel_interior ` \<F>) \<noteq> {}"
+ shows "closure(\<Inter>\<F>) = \<Inter>(closure ` \<F>)"
proof -
- have "\<Inter>{closure S |S. S \<in> I} \<le> closure (\<Inter>{rel_interior S |S. S \<in> I})"
- using convex_closure_rel_interior_inter assms by auto
+ have "\<Inter>(closure ` \<F>) \<le> closure (\<Inter>(rel_interior ` \<F>))"
+ by (meson assms convex_closure_rel_interior_Int)
moreover
- have "closure (\<Inter>{rel_interior S |S. S \<in> I}) \<le> closure (\<Inter>I)"
- using rel_interior_inter_aux closure_mono[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"]
+ have "closure (\<Inter>(rel_interior ` \<F>)) \<subseteq> closure (\<Inter>\<F>)"
+ using rel_interior_inter_aux closure_mono[of "\<Inter>(rel_interior ` \<F>)" "\<Inter>\<F>"]
by auto
ultimately show ?thesis
- using closure_Int[of I] by auto
-qed
-
-lemma convex_inter_rel_interior_same_closure:
- assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
- and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
- shows "closure (\<Inter>{rel_interior S |S. S \<in> I}) = closure (\<Inter>I)"
+ using closure_Int[of \<F>] by blast
+qed
+
+lemma closure_Inter_convex_open:
+ "(\<And>S::'n::euclidean_space set. S \<in> \<F> \<Longrightarrow> convex S \<and> open S)
+ \<Longrightarrow> closure(\<Inter>\<F>) = (if \<Inter>\<F> = {} then {} else \<Inter>(closure ` \<F>))"
+ by (simp add: closure_Inter_convex rel_interior_open)
+
+lemma convex_Inter_rel_interior_same_closure:
+ fixes \<F> :: "'n::euclidean_space set set"
+ assumes "\<And>S. S \<in> \<F> \<Longrightarrow> convex S"
+ and "\<Inter>(rel_interior ` \<F>) \<noteq> {}"
+ shows "closure (\<Inter>(rel_interior ` \<F>)) = closure (\<Inter>\<F>)"
proof -
- have "\<Inter>{closure S |S. S \<in> I} \<le> closure (\<Inter>{rel_interior S |S. S \<in> I})"
- using convex_closure_rel_interior_inter assms by auto
+ have "\<Inter>(closure ` \<F>) \<subseteq> closure (\<Inter>(rel_interior ` \<F>))"
+ by (meson assms convex_closure_rel_interior_Int)
moreover
- have "closure (\<Inter>{rel_interior S |S. S \<in> I}) \<le> closure (\<Inter>I)"
- using rel_interior_inter_aux closure_mono[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"]
- by auto
+ have "closure (\<Inter>(rel_interior ` \<F>)) \<subseteq> closure (\<Inter>\<F>)"
+ by (metis Setcompr_eq_image closure_mono rel_interior_inter_aux)
ultimately show ?thesis
- using closure_Int[of I] by auto
-qed
-
-lemma convex_rel_interior_inter:
- assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
- and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
- shows "rel_interior (\<Inter>I) \<subseteq> \<Inter>{rel_interior S |S. S \<in> I}"
+ by (simp add: assms closure_Inter_convex)
+qed
+
+lemma convex_rel_interior_Inter:
+ fixes \<F> :: "'n::euclidean_space set set"
+ assumes "\<And>S. S \<in> \<F> \<Longrightarrow> convex S"
+ and "\<Inter>(rel_interior ` \<F>) \<noteq> {}"
+ shows "rel_interior (\<Inter>\<F>) \<subseteq> \<Inter>(rel_interior ` \<F>)"
proof -
- have "convex (\<Inter>I)"
+ have "convex (\<Inter>\<F>)"
using assms convex_Inter by auto
moreover
- have "convex (\<Inter>{rel_interior S |S. S \<in> I})"
- using assms convex_rel_interior by (force intro: convex_Inter)
+ have "convex (\<Inter>(rel_interior ` \<F>))"
+ using assms by (metis convex_rel_interior convex_INT)
ultimately
- have "rel_interior (\<Inter>{rel_interior S |S. S \<in> I}) = rel_interior (\<Inter>I)"
- using convex_inter_rel_interior_same_closure assms
- closure_eq_rel_interior_eq[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"]
+ have "rel_interior (\<Inter>(rel_interior ` \<F>)) = rel_interior (\<Inter>\<F>)"
+ using convex_Inter_rel_interior_same_closure assms
+ closure_eq_rel_interior_eq[of "\<Inter>(rel_interior ` \<F>)" "\<Inter>\<F>"]
by blast
then show ?thesis
- using rel_interior_subset[of "\<Inter>{rel_interior S |S. S \<in> I}"] by auto
-qed
-
-lemma convex_rel_interior_finite_inter:
- assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
- and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
- and "finite I"
- shows "rel_interior (\<Inter>I) = \<Inter>{rel_interior S |S. S \<in> I}"
+ using rel_interior_subset[of "\<Inter>(rel_interior ` \<F>)"] by auto
+qed
+
+lemma convex_rel_interior_finite_Inter:
+ fixes \<F> :: "'n::euclidean_space set set"
+ assumes "\<And>S. S \<in> \<F> \<Longrightarrow> convex S"
+ and "\<Inter>(rel_interior ` \<F>) \<noteq> {}"
+ and "finite \<F>"
+ shows "rel_interior (\<Inter>\<F>) = \<Inter>(rel_interior ` \<F>)"
proof -
- have "\<Inter>I \<noteq> {}"
- using assms rel_interior_inter_aux[of I] by auto
- have "convex (\<Inter>I)"
+ have "\<Inter>\<F> \<noteq> {}"
+ using assms rel_interior_inter_aux[of \<F>] by auto
+ have "convex (\<Inter>\<F>)"
using convex_Inter assms by auto
show ?thesis
- proof (cases "I = {}")
+ proof (cases "\<F> = {}")
case True
then show ?thesis
using Inter_empty rel_interior_UNIV by auto
@@ -1446,43 +1580,43 @@
case False
{
fix z
- assume z: "z \<in> \<Inter>{rel_interior S |S. S \<in> I}"
+ assume z: "z \<in> \<Inter>(rel_interior ` \<F>)"
{
fix x
- assume x: "x \<in> \<Inter>I"
+ assume x: "x \<in> \<Inter>\<F>"
{
fix S
- assume S: "S \<in> I"
+ assume S: "S \<in> \<F>"
then have "z \<in> rel_interior S" "x \<in> S"
using z x by auto
then have "\<exists>m. m > 1 \<and> (\<forall>e. e > 1 \<and> e \<le> m \<longrightarrow> (1 - e)*\<^sub>R x + e *\<^sub>R z \<in> S)"
using convex_rel_interior_if[of S z] S assms hull_subset[of S] by auto
}
then obtain mS where
- mS: "\<forall>S\<in>I. mS S > 1 \<and> (\<forall>e. e > 1 \<and> e \<le> mS S \<longrightarrow> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S)" by metis
- define e where "e = Min (mS ` I)"
- then have "e \<in> mS ` I" using assms \<open>I \<noteq> {}\<close> by simp
+ mS: "\<forall>S\<in>\<F>. mS S > 1 \<and> (\<forall>e. e > 1 \<and> e \<le> mS S \<longrightarrow> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S)" by metis
+ define e where "e = Min (mS ` \<F>)"
+ then have "e \<in> mS ` \<F>" using assms \<open>\<F> \<noteq> {}\<close> by simp
then have "e > 1" using mS by auto
- moreover have "\<forall>S\<in>I. e \<le> mS S"
+ moreover have "\<forall>S\<in>\<F>. e \<le> mS S"
using e_def assms by auto
- ultimately have "\<exists>e > 1. (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> \<Inter>I"
+ ultimately have "\<exists>e > 1. (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> \<Inter>\<F>"
using mS by auto
}
- then have "z \<in> rel_interior (\<Inter>I)"
- using convex_rel_interior_iff[of "\<Inter>I" z] \<open>\<Inter>I \<noteq> {}\<close> \<open>convex (\<Inter>I)\<close> by auto
+ then have "z \<in> rel_interior (\<Inter>\<F>)"
+ using convex_rel_interior_iff[of "\<Inter>\<F>" z] \<open>\<Inter>\<F> \<noteq> {}\<close> \<open>convex (\<Inter>\<F>)\<close> by auto
}
then show ?thesis
- using convex_rel_interior_inter[of I] assms by auto
+ using convex_rel_interior_Inter[of \<F>] assms by auto
qed
qed
-lemma convex_closure_inter_two:
+lemma closure_Int_convex:
fixes S T :: "'n::euclidean_space set"
assumes "convex S"
and "convex T"
assumes "rel_interior S \<inter> rel_interior T \<noteq> {}"
shows "closure (S \<inter> T) = closure S \<inter> closure T"
- using convex_closure_inter[of "{S,T}"] assms by auto
+ using closure_Inter_convex[of "{S,T}"] assms by auto
lemma convex_rel_interior_inter_two:
fixes S T :: "'n::euclidean_space set"
@@ -1490,7 +1624,7 @@
and "convex T"
and "rel_interior S \<inter> rel_interior T \<noteq> {}"
shows "rel_interior (S \<inter> T) = rel_interior S \<inter> rel_interior T"
- using convex_rel_interior_finite_inter[of "{S,T}"] assms by auto
+ using convex_rel_interior_finite_Inter[of "{S,T}"] assms by auto
lemma convex_affine_closure_Int:
fixes S T :: "'n::euclidean_space set"
@@ -1498,7 +1632,7 @@
and "affine T"
and "rel_interior S \<inter> T \<noteq> {}"
shows "closure (S \<inter> T) = closure S \<inter> T"
- by (metis affine_imp_convex assms convex_closure_inter_two rel_interior_affine rel_interior_eq_closure)
+ by (metis affine_imp_convex assms closure_Int_convex rel_interior_affine rel_interior_eq_closure)
lemma connected_component_1_gen:
fixes S :: "'a :: euclidean_space set"
@@ -1749,22 +1883,21 @@
shows "convex (((*\<^sub>R) c) ` S) \<and> rel_open (((*\<^sub>R) c) ` S)"
by (metis assms convex_scaling rel_interior_convex_scaleR rel_open_def)
-lemma convex_rel_open_finite_inter:
- assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set) \<and> rel_open S"
- and "finite I"
- shows "convex (\<Inter>I) \<and> rel_open (\<Inter>I)"
-proof (cases "\<Inter>{rel_interior S |S. S \<in> I} = {}")
+lemma convex_rel_open_finite_Inter:
+ fixes \<F> :: "'n::euclidean_space set set"
+ assumes "\<And>S. S \<in> \<F> \<Longrightarrow> convex S \<and> rel_open S"
+ and "finite \<F>"
+ shows "convex (\<Inter>\<F>) \<and> rel_open (\<Inter>\<F>)"
+proof (cases "\<Inter>{rel_interior S |S. S \<in> \<F>} = {}")
case True
- then have "\<Inter>I = {}"
+ then have "\<Inter>\<F> = {}"
using assms unfolding rel_open_def by auto
then show ?thesis
unfolding rel_open_def by auto
next
case False
- then have "rel_open (\<Inter>I)"
- using assms unfolding rel_open_def
- using convex_rel_interior_finite_inter[of I]
- by auto
+ then have "rel_open (\<Inter>\<F>)"
+ using assms convex_rel_interior_finite_Inter[of \<F>] by (force simp: rel_open_def)
then show ?thesis
using convex_Inter assms by auto
qed
@@ -2880,12 +3013,9 @@
by (auto simp: algebra_simps sum_subtractf sum.distrib)
qed
have "y \<notin> rel_interior (convex hull S)"
- using y
- apply (simp add: mem_rel_interior)
- apply (auto simp: convex_hull_finite [OF fs])
- apply (drule_tac x=u in spec)
- apply (auto intro: *)
- done
+ using y convex_hull_finite [OF fs] *
+ apply simp
+ by (metis (no_types, lifting) IntD1 affine_hull_convex_hull mem_rel_interior)
} with rel_interior_subset show "?lhs \<le> ?rhs"
by blast
qed
@@ -4022,6 +4152,133 @@
by (force simp: closedin_limpt)
qed
+subsection \<open>Closure of conic hulls\<close>
+proposition closedin_conic_hull:
+ fixes S :: "'a::euclidean_space set"
+ assumes "compact T" "0 \<notin> T" "T \<subseteq> S"
+ shows "closedin (top_of_set (conic hull S)) (conic hull T)"
+proof -
+ have **: "compact ({0..} \<times> T \<inter> (\<lambda>z. fst z *\<^sub>R snd z) -` K)" (is "compact ?L")
+ if "K \<subseteq> (\<lambda>z. (fst z) *\<^sub>R snd z) ` ({0..} \<times> S)" "compact K" for K
+ proof -
+ obtain r where "r > 0" and r: "\<And>x. x \<in> K \<Longrightarrow> norm x \<le> r"
+ by (metis \<open>compact K\<close> bounded_normE compact_imp_bounded)
+ show ?thesis
+ unfolding compact_eq_bounded_closed
+ proof
+ have "bounded ({0..r / setdist{0}T} \<times> T)"
+ by (simp add: assms(1) bounded_Times compact_imp_bounded)
+ moreover have "?L \<subseteq> ({0..r / setdist{0}T} \<times> T)"
+ proof clarsimp
+ fix a b
+ assume "a *\<^sub>R b \<in> K" and "b \<in> T" and "0 \<le> a"
+ have "setdist {0} T \<noteq> 0"
+ using \<open>b \<in> T\<close> assms compact_imp_closed setdist_eq_0_closed by auto
+ then have T0: "setdist {0} T > 0"
+ using less_eq_real_def by fastforce
+ then have "a * setdist {0} T \<le> r"
+ by (smt (verit, ccfv_SIG) \<open>0 \<le> a\<close> \<open>a *\<^sub>R b \<in> K\<close> \<open>b \<in> T\<close> dist_0_norm mult_mono' norm_scaleR r setdist_le_dist singletonI)
+ with T0 \<open>r>0\<close> show "a \<le> r / setdist {0} T"
+ by (simp add: divide_simps)
+ qed
+ ultimately show "bounded ?L"
+ by (meson bounded_subset)
+ show "closed ?L"
+ proof (rule continuous_closed_preimage)
+ show "continuous_on ({0..} \<times> T) (\<lambda>z. fst z *\<^sub>R snd z)"
+ by (intro continuous_intros)
+ show "closed ({0::real..} \<times> T)"
+ by (simp add: assms(1) closed_Times compact_imp_closed)
+ show "closed K"
+ by (simp add: compact_imp_closed that(2))
+ qed
+ qed
+ qed
+ show ?thesis
+ unfolding conic_hull_as_image
+ proof (rule proper_map)
+ show "compact ({0..} \<times> T \<inter> (\<lambda>z. fst z *\<^sub>R snd z) -` K)" (is "compact ?L")
+ if "K \<subseteq> (\<lambda>z. (fst z) *\<^sub>R snd z) ` ({0..} \<times> S)" "compact K" for K
+ proof -
+ obtain r where "r > 0" and r: "\<And>x. x \<in> K \<Longrightarrow> norm x \<le> r"
+ by (metis \<open>compact K\<close> bounded_normE compact_imp_bounded)
+ show ?thesis
+ unfolding compact_eq_bounded_closed
+ proof
+ have "bounded ({0..r / setdist{0}T} \<times> T)"
+ by (simp add: assms(1) bounded_Times compact_imp_bounded)
+ moreover have "?L \<subseteq> ({0..r / setdist{0}T} \<times> T)"
+ proof clarsimp
+ fix a b
+ assume "a *\<^sub>R b \<in> K" and "b \<in> T" and "0 \<le> a"
+ have "setdist {0} T \<noteq> 0"
+ using \<open>b \<in> T\<close> assms compact_imp_closed setdist_eq_0_closed by auto
+ then have T0: "setdist {0} T > 0"
+ using less_eq_real_def by fastforce
+ then have "a * setdist {0} T \<le> r"
+ by (smt (verit, ccfv_SIG) \<open>0 \<le> a\<close> \<open>a *\<^sub>R b \<in> K\<close> \<open>b \<in> T\<close> dist_0_norm mult_mono' norm_scaleR r setdist_le_dist singletonI)
+ with T0 \<open>r>0\<close> show "a \<le> r / setdist {0} T"
+ by (simp add: divide_simps)
+ qed
+ ultimately show "bounded ?L"
+ by (meson bounded_subset)
+ show "closed ?L"
+ proof (rule continuous_closed_preimage)
+ show "continuous_on ({0..} \<times> T) (\<lambda>z. fst z *\<^sub>R snd z)"
+ by (intro continuous_intros)
+ show "closed ({0::real..} \<times> T)"
+ by (simp add: assms(1) closed_Times compact_imp_closed)
+ show "closed K"
+ by (simp add: compact_imp_closed that(2))
+ qed
+ qed
+ qed
+ show "(\<lambda>z. fst z *\<^sub>R snd z) ` ({0::real..} \<times> T) \<subseteq> (\<lambda>z. fst z *\<^sub>R snd z) ` ({0..} \<times> S)"
+ using \<open>T \<subseteq> S\<close> by force
+ qed auto
+qed
+
+lemma closed_conic_hull:
+ fixes S :: "'a::euclidean_space set"
+ assumes "0 \<in> rel_interior S \<or> compact S \<and> 0 \<notin> S"
+ shows "closed(conic hull S)"
+ using assms
+proof
+ assume "0 \<in> rel_interior S"
+ then show "closed (conic hull S)"
+ by (simp add: conic_hull_eq_span)
+next
+ assume "compact S \<and> 0 \<notin> S"
+ then have "closedin (top_of_set UNIV) (conic hull S)"
+ using closedin_conic_hull by force
+ then show "closed (conic hull S)"
+ by simp
+qed
+
+lemma conic_closure:
+ fixes S :: "'a::euclidean_space set"
+ shows "conic S \<Longrightarrow> conic(closure S)"
+ by (meson Convex.cone_def cone_closure conic_def)
+
+lemma closure_conic_hull:
+ fixes S :: "'a::euclidean_space set"
+ assumes "0 \<in> rel_interior S \<or> bounded S \<and> ~(0 \<in> closure S)"
+ shows "closure(conic hull S) = conic hull (closure S)"
+ using assms
+proof
+ assume "0 \<in> rel_interior S"
+ then show "closure (conic hull S) = conic hull closure S"
+ by (metis closed_affine_hull closure_closed closure_same_affine_hull closure_subset conic_hull_eq_affine_hull subsetD subset_rel_interior)
+next
+ have "\<And>x. x \<in> conic hull closure S \<Longrightarrow> x \<in> closure (conic hull S)"
+ by (metis (no_types, opaque_lifting) closure_mono conic_closure conic_conic_hull subset_eq subset_hull)
+ moreover
+ assume "bounded S \<and> 0 \<notin> closure S"
+ then have "\<And>x. x \<in> closure (conic hull S) \<Longrightarrow> x \<in> conic hull closure S"
+ by (metis closed_conic_hull closure_Un_frontier closure_closed closure_mono compact_closure hull_Un_subset le_sup_iff subsetD)
+ ultimately show "closure (conic hull S) = conic hull closure S"
+ by blast
+qed
lemma compact_continuous_image_eq:
fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
--- a/src/HOL/Binomial.thy Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Binomial.thy Sat Sep 09 19:26:08 2023 +0100
@@ -115,6 +115,9 @@
lemma binomial_1 [simp]: "n choose Suc 0 = n"
by (induct n) simp_all
+lemma choose_one: "n choose 1 = n" for n :: nat
+ by simp
+
lemma choose_reduce_nat:
"0 < n \<Longrightarrow> 0 < k \<Longrightarrow>
n choose k = ((n - 1) choose (k - 1)) + ((n - 1) choose k)"
@@ -1084,109 +1087,190 @@
qed
-subsection \<open>More on Binomial Coefficients\<close>
+subsection \<open>Inclusion-exclusion principle\<close>
+
+lemma Inter_over_Union:
+ "\<Inter> {\<Union> (\<F> x) |x. x \<in> S} = \<Union> {\<Inter> (G ` S) |G. \<forall>x\<in>S. G x \<in> \<F> x}"
+proof -
+ have "\<And>x. \<forall>s\<in>S. \<exists>X \<in> \<F> s. x \<in> X \<Longrightarrow> \<exists>G. (\<forall>x\<in>S. G x \<in> \<F> x) \<and> (\<forall>s\<in>S. x \<in> G s)"
+ by metis
+ then show ?thesis
+ by (auto simp flip: all_simps ex_simps)
+qed
+
+lemma subset_insert_lemma:
+ "{T. T \<subseteq> (insert a S) \<and> P T} = {T. T \<subseteq> S \<and> P T} \<union> {insert a T |T. T \<subseteq> S \<and> P(insert a T)}" (is "?L=?R")
+proof
+ show "?L \<subseteq> ?R"
+ by (smt (verit) UnI1 UnI2 insert_Diff mem_Collect_eq subsetI subset_insert_iff)
+qed blast
+
+
+text\<open>Versions for additive real functions, where the additivity applies only to some
+ specific subsets (e.g. cardinality of finite sets, measurable sets with bounded measure.
+ (From HOL Light)\<close>
+
+locale Incl_Excl =
+ fixes P :: "'a set \<Rightarrow> bool" and f :: "'a set \<Rightarrow> 'b::ring_1"
+ assumes disj_add: "\<lbrakk>P S; P T; disjnt S T\<rbrakk> \<Longrightarrow> f(S \<union> T) = f S + f T"
+ and empty: "P{}"
+ and Int: "\<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S \<inter> T)"
+ and Un: "\<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S \<union> T)"
+ and Diff: "\<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S - T)"
+
+begin
+
+lemma f_empty [simp]: "f{} = 0"
+ using disj_add empty by fastforce
+
+lemma f_Un_Int: "\<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> f(S \<union> T) + f(S \<inter> T) = f S + f T"
+ by (smt (verit, ccfv_threshold) Groups.add_ac(2) Incl_Excl.Diff Incl_Excl.Int Incl_Excl_axioms Int_Diff_Un Int_Diff_disjoint Int_absorb Un_Diff Un_Int_eq(2) disj_add disjnt_def group_cancel.add2 sup_bot.right_neutral)
-lemma choose_one: "n choose 1 = n" for n :: nat
- by simp
+lemma restricted_indexed:
+ assumes "finite A" and X: "\<And>a. a \<in> A \<Longrightarrow> P(X a)"
+ shows "f(\<Union>(X ` A)) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> (X ` B)))"
+proof -
+ have "\<lbrakk>finite A; card A = n; \<forall>a \<in> A. P (X a)\<rbrakk>
+ \<Longrightarrow> f(\<Union>(X ` A)) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> (X ` B)))" for n X and A :: "'c set"
+ proof (induction n arbitrary: A X rule: less_induct)
+ case (less n0 A0 X)
+ show ?case
+ proof (cases "n0=0")
+ case True
+ with less show ?thesis
+ by fastforce
+ next
+ case False
+ with less.prems obtain A n a where *: "n0 = Suc n" "A0 = insert a A" "a \<notin> A" "card A = n" "finite A"
+ by (metis card_Suc_eq_finite not0_implies_Suc)
+ with less have "P (X a)" by blast
+ have APX: "\<forall>a \<in> A. P (X a)"
+ by (simp add: "*" less.prems)
+ have PUXA: "P (\<Union> (X ` A))"
+ using \<open>finite A\<close> APX
+ by (induction) (auto simp: empty Un)
+ have "f (\<Union> (X ` A0)) = f (X a \<union> \<Union> (X ` A))"
+ by (simp add: *)
+ also have "... = f (X a) + f (\<Union> (X ` A)) - f (X a \<inter> \<Union> (X ` A))"
+ using f_Un_Int add_diff_cancel PUXA \<open>P (X a)\<close> by metis
+ also have "... = f (X a) - (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ card B * f (\<Inter> (X ` B))) +
+ (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ card B * f (X a \<inter> \<Inter> (X ` B)))"
+ proof -
+ have 1: "f (\<Union>i\<in>A. X a \<inter> X i) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter>b\<in>B. X a \<inter> X b))"
+ using less.IH [of n A "\<lambda>i. X a \<inter> X i"] APX Int \<open>P (X a)\<close> by (simp add: *)
+ have 2: "X a \<inter> \<Union> (X ` A) = (\<Union>i\<in>A. X a \<inter> X i)"
+ by auto
+ have 3: "f (\<Union> (X ` A)) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> (X ` B)))"
+ using less.IH [of n A X] APX Int \<open>P (X a)\<close> by (simp add: *)
+ show ?thesis
+ unfolding 3 2 1
+ by (simp add: sum_negf)
+ qed
+ also have "... = (\<Sum>B | B \<subseteq> A0 \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> (X ` B)))"
+ proof -
+ have F: "{insert a B |B. B \<subseteq> A} = insert a ` Pow A \<and> {B. B \<subseteq> A \<and> B \<noteq> {}} = Pow A - {{}}"
+ by auto
+ have G: "(\<Sum>B\<in>Pow A. (- 1) ^ card (insert a B) * f (X a \<inter> \<Inter> (X ` B))) = (\<Sum>B\<in>Pow A. - ((- 1) ^ card B * f (X a \<inter> \<Inter> (X ` B))))"
+ proof (rule sum.cong [OF refl])
+ fix B
+ assume B: "B \<in> Pow A"
+ then have "finite B"
+ using \<open>finite A\<close> finite_subset by auto
+ show "(- 1) ^ card (insert a B) * f (X a \<inter> \<Inter> (X ` B)) = - ((- 1) ^ card B * f (X a \<inter> \<Inter> (X ` B)))"
+ using B * by (auto simp add: card_insert_if \<open>finite B\<close>)
+ qed
+ have disj: "{B. B \<subseteq> A \<and> B \<noteq> {}} \<inter> {insert a B |B. B \<subseteq> A} = {}"
+ using * by blast
+ have inj: "inj_on (insert a) (Pow A)"
+ using "*" inj_on_def by fastforce
+ show ?thesis
+ apply (simp add: * subset_insert_lemma sum.union_disjoint disj sum_negf)
+ apply (simp add: F G sum_negf sum.reindex [OF inj] o_def sum_diff *)
+ done
+ qed
+ finally show ?thesis .
+ qed
+ qed
+ then show ?thesis
+ by (meson assms)
+qed
+
+lemma restricted:
+ assumes "finite A" "\<And>a. a \<in> A \<Longrightarrow> P a"
+ shows "f(\<Union> A) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> B))"
+ using restricted_indexed [of A "\<lambda>x. x"] assms by auto
+
+end
+
+subsection\<open>Versions for unrestrictedly additive functions\<close>
+
+lemma Incl_Excl_UN:
+ fixes f :: "'a set \<Rightarrow> 'b::ring_1"
+ assumes "\<And>S T. disjnt S T \<Longrightarrow> f(S \<union> T) = f S + f T" "finite A"
+ shows "f(\<Union>(G ` A)) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (-1) ^ (card B + 1) * f (\<Inter> (G ` B)))"
+proof -
+ interpret Incl_Excl "\<lambda>x. True" f
+ by (simp add: Incl_Excl.intro assms(1))
+ show ?thesis
+ using restricted_indexed assms by blast
+qed
+
+lemma Incl_Excl_Union:
+ fixes f :: "'a set \<Rightarrow> 'b::ring_1"
+ assumes "\<And>S T. disjnt S T \<Longrightarrow> f(S \<union> T) = f S + f T" "finite A"
+ shows "f(\<Union> A) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> B))"
+ using Incl_Excl_UN[of f A "\<lambda>X. X"] assms by simp
text \<open>The famous inclusion-exclusion formula for the cardinality of a union\<close>
lemma int_card_UNION:
- assumes "finite A"
- and "\<forall>k \<in> A. finite k"
+ assumes "finite A" "\<And>K. K \<in> A \<Longrightarrow> finite K"
shows "int (card (\<Union>A)) = (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
- (is "?lhs = ?rhs")
+proof -
+ interpret Incl_Excl finite "int o card"
+ proof qed (auto simp add: card_Un_disjnt)
+ show ?thesis
+ using restricted assms by auto
+qed
+
+text\<open>A more conventional form\<close>
+lemma inclusion_exclusion:
+ assumes "finite A" "\<And>K. K \<in> A \<Longrightarrow> finite K"
+ shows "int(card(\<Union> A)) =
+ (\<Sum>n=1..card A. (-1) ^ (Suc n) * (\<Sum>B | B \<subseteq> A \<and> card B = n. int (card (\<Inter> B))))" (is "_=?R")
proof -
- have "?rhs = (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))"
- by simp
- also have "\<dots> = (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. (- 1) ^ (card I + 1)))"
- by (subst sum_distrib_left) simp
- also have "\<dots> = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. (- 1) ^ (card I + 1))"
- using assms by (subst sum.Sigma) auto
- also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
- by (rule sum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI)
- also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
- using assms
- by (auto intro!: sum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"])
- also have "\<dots> = (\<Sum>x\<in>\<Union>A. (\<Sum>I|I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I. (- 1) ^ (card I + 1)))"
- using assms by (subst sum.Sigma) auto
- also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "sum ?lhs _ = _")
- proof (rule sum.cong[OF refl])
- fix x
- assume x: "x \<in> \<Union>A"
- define K where "K = {X \<in> A. x \<in> X}"
- with \<open>finite A\<close> have K: "finite K"
- by auto
- let ?I = "\<lambda>i. {I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I}"
- have "inj_on snd (SIGMA i:{1..card A}. ?I i)"
- using assms by (auto intro!: inj_onI)
- moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}"
- using assms
- by (auto intro!: rev_image_eqI[where x="(card a, a)" for a]
- simp add: card_gt_0_iff[folded Suc_le_eq]
- dest: finite_subset intro: card_mono)
- ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). (- 1) ^ (i + 1))"
- by (rule sum.reindex_cong [where l = snd]) fastforce
- also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. (- 1) ^ (i + 1)))"
- using assms by (subst sum.Sigma) auto
- also have "\<dots> = (\<Sum>i=1..card A. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))"
- by (subst sum_distrib_left) simp
- also have "\<dots> = (\<Sum>i=1..card K. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))"
- (is "_ = ?rhs")
- proof (rule sum.mono_neutral_cong_right[rule_format])
- show "finite {1..card A}"
- by simp
- show "{1..card K} \<subseteq> {1..card A}"
- using \<open>finite A\<close> by (auto simp add: K_def intro: card_mono)
- next
- fix i
- assume "i \<in> {1..card A} - {1..card K}"
- then have i: "i \<le> card A" "card K < i"
- by auto
- have "{I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I} = {I. I \<subseteq> K \<and> card I = i}"
- by (auto simp add: K_def)
- also have "\<dots> = {}"
- using \<open>finite A\<close> i by (auto simp add: K_def dest: card_mono[rotated 1])
- finally show "(- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
- by (metis mult_zero_right sum.empty)
- next
- fix i
- have "(\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1) = (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)"
- (is "?lhs = ?rhs")
- by (rule sum.cong) (auto simp add: K_def)
- then show "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs"
- by simp
- qed
- also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}"
- using assms by (auto simp add: card_eq_0_iff K_def dest: finite_subset)
- then have "?rhs = (\<Sum>i = 0..card K. (- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
- by (subst (2) sum.atLeast_Suc_atMost) simp_all
- also have "\<dots> = (\<Sum>i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1"
- using K by (subst n_subsets[symmetric]) simp_all
- also have "\<dots> = - (\<Sum>i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"
- by (subst sum_distrib_left[symmetric]) simp
- also have "\<dots> = - ((-1 + 1) ^ card K) + 1"
- by (subst binomial_ring) (simp add: ac_simps atMost_atLeast0)
- also have "\<dots> = 1"
- using x K by (auto simp add: K_def card_gt_0_iff)
- finally show "?lhs x = 1" .
+ have fin: "finite {I. I \<subseteq> A \<and> I \<noteq> {}}"
+ by (simp add: assms)
+ have "\<And>k. \<lbrakk>Suc 0 \<le> k; k \<le> card A\<rbrakk> \<Longrightarrow> \<exists>B\<subseteq>A. B \<noteq> {} \<and> k = card B"
+ by (metis (mono_tags, lifting) Suc_le_D Zero_neq_Suc card_eq_0_iff obtain_subset_with_card_n)
+ with \<open>finite A\<close> finite_subset
+ have card_eq: "card ` {I. I \<subseteq> A \<and> I \<noteq> {}} = {1..card A}"
+ using not_less_eq_eq card_mono by (fastforce simp: image_iff)
+ have "int(card(\<Union> A))
+ = (\<Sum>y = 1..card A. \<Sum>I\<in>{x. x \<subseteq> A \<and> x \<noteq> {} \<and> card x = y}. - ((- 1) ^ y * int (card (\<Inter> I))))"
+ by (simp add: int_card_UNION assms sum.image_gen [OF fin, where g=card] card_eq)
+ also have "... = ?R"
+ proof -
+ have "{B. B \<subseteq> A \<and> B \<noteq> {} \<and> card B = k} = {B. B \<subseteq> A \<and> card B = k}"
+ if "Suc 0 \<le> k" and "k \<le> card A" for k
+ using that by auto
+ then show ?thesis
+ by (clarsimp simp add: sum_negf simp flip: sum_distrib_left)
qed
- also have "\<dots> = int (card (\<Union>A))"
- by simp
- finally show ?thesis ..
+ finally show ?thesis .
qed
lemma card_UNION:
- assumes "finite A"
- and "\<forall>k \<in> A. finite k"
+ assumes "finite A" and "\<And>K. K \<in> A \<Longrightarrow> finite K"
shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
by (simp only: flip: int_card_UNION [OF assms])
lemma card_UNION_nonneg:
- assumes "finite A"
- and "\<forall>k \<in> A. finite k"
+ assumes "finite A" and "\<And>K. K \<in> A \<Longrightarrow> finite K"
shows "(\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I))) \<ge> 0"
using int_card_UNION [OF assms] by presburger
+subsection \<open>More on Binomial Coefficients\<close>
+
text \<open>The number of nat lists of length \<open>m\<close> summing to \<open>N\<close> is \<^term>\<open>(N + m - 1) choose N\<close>:\<close>
lemma card_length_sum_list_rec:
assumes "m \<ge> 1"
--- a/src/HOL/Real_Vector_Spaces.thy Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Sat Sep 09 19:26:08 2023 +0100
@@ -142,7 +142,7 @@
lemma scaleR_minus1_left [simp]: "scaleR (-1) x = - x"
for x :: "'a::real_vector"
- using scaleR_minus_left [of 1 x] by simp
+ by simp
lemma scaleR_2:
fixes x :: "'a::real_vector"
@@ -786,6 +786,11 @@
class real_normed_div_algebra = real_div_algebra + real_normed_vector +
assumes norm_mult: "norm (x * y) = norm x * norm y"
+lemma divideR_right:
+ fixes x y :: "'a::real_normed_vector"
+ shows "r \<noteq> 0 \<Longrightarrow> y = x /\<^sub>R r \<longleftrightarrow> r *\<^sub>R y = x"
+ by auto
+
class real_normed_field = real_field + real_normed_div_algebra
instance real_normed_div_algebra < real_normed_algebra_1