src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
 changeset 63075 60a42a4166af parent 63072 eb5d493a9e03 child 63077 844725394a37
```     1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon May 09 16:02:23 2016 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon May 09 17:23:19 2016 +0100
1.3 @@ -2136,7 +2136,6 @@
1.4  lemma convex_hull_subset_affine_hull: "(convex hull s) \<subseteq> (affine hull s)"
1.5    by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset)
1.6
1.7 -
1.8  lemma affine_dependent_imp_dependent: "affine_dependent s \<Longrightarrow> dependent s"
1.9    unfolding affine_dependent_def dependent_def
1.10    using affine_hull_subset_span by auto
1.11 @@ -2669,6 +2668,13 @@
1.12    shows "\<lbrakk>S \<subseteq> T; dim T \<le> dim S\<rbrakk> \<Longrightarrow> span S = span T"
1.13  by (simp add: span_mono subspace_dim_equal subspace_span)
1.14
1.15 +lemma dim_eq_full:
1.16 +    fixes S :: "'a :: euclidean_space set"
1.17 +    shows "dim S = DIM('a) \<longleftrightarrow> span S = UNIV"
1.18 +apply (rule iffI)
1.19 + apply (metis dim_eq_span dim_subset_UNIV span_Basis span_span subset_UNIV)
1.20 +by (metis dim_UNIV dim_span)
1.21 +
1.22  lemma span_substd_basis:
1.23    assumes d: "d \<subseteq> Basis"
1.24    shows "span d = {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
1.25 @@ -2741,7 +2747,7 @@
1.26  lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1"
1.27    by (simp add: aff_dim_empty [symmetric])
1.28
1.29 -lemma aff_dim_affine_hull: "aff_dim (affine hull S) = aff_dim S"
1.30 +lemma aff_dim_affine_hull [simp]: "aff_dim (affine hull S) = aff_dim S"
1.31    unfolding aff_dim_def using hull_hull[of _ S] by auto
1.32
1.33  lemma aff_dim_affine_hull2:
1.34 @@ -3672,7 +3678,7 @@
1.35    have "aff_dim S \<le> aff_dim (closure S)"
1.36      using aff_dim_subset closure_subset by auto
1.37    moreover have "aff_dim (closure S) \<le> aff_dim (affine hull S)"
1.38 -    using aff_dim_subset closure_affine_hull by auto
1.39 +    using aff_dim_subset closure_affine_hull by blast
1.40    moreover have "aff_dim (affine hull S) = aff_dim S"
1.41      using aff_dim_affine_hull by auto
1.42    ultimately show ?thesis by auto
1.43 @@ -4578,7 +4584,7 @@
1.44    shows "\<exists>a b. \<exists>y\<in>s. inner a z < b \<and> inner a y = b \<and> (\<forall>x\<in>s. inner a x \<ge> b)"
1.45  proof -
1.46    obtain y where "y \<in> s" and y: "\<forall>x\<in>s. dist z y \<le> dist z x"
1.47 -    by (metis distance_attains_inf[OF assms(2-3)])
1.48 +    by (metis distance_attains_inf[OF assms(2-3)])
1.49    show ?thesis
1.50      apply (rule_tac x="y - z" in exI)
1.51      apply (rule_tac x="inner (y - z) y" in exI)
1.52 @@ -6751,7 +6757,11 @@
1.53
1.54  lemma closed_segment_eq_open: "closed_segment a b = open_segment a b \<union> {a,b}"
1.55    using open_segment_def by auto
1.56 -
1.57 +
1.58 +lemma convex_contains_open_segment:
1.59 +  "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. open_segment a b \<subseteq> s)"
1.60 +  by (simp add: convex_contains_segment closed_segment_eq_open)
1.61 +
1.62  lemma closed_segment_eq_real_ivl:
1.63    fixes a b::real
1.64    shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})"
1.65 @@ -7759,7 +7769,7 @@
1.66          then have "x /\<^sub>R (2 * real (card d)) \<in> span d"
1.67            using span_mul[of x "d" "(inverse (real (card d)) / 2)"] by auto
1.68        }
1.69 -      then show "\<forall>x\<in>d. x /\<^sub>R (2 * real (card d)) \<in> span d"
1.70 +      then show "\<And>x. x\<in>d \<Longrightarrow> x /\<^sub>R (2 * real (card d)) \<in> span d"
1.71          by auto
1.72      qed
1.73      then show "?a \<bullet> i = 0 "
1.74 @@ -8124,8 +8134,8 @@
1.75  proof -
1.76    have "rel_interior S \<noteq> {}"
1.77      by (simp add: assms rel_interior_eq_empty)
1.78 -  then obtain a where a: "a \<in> rel_interior S"  by blast
1.79 -  with ST have "a \<in> T"  by blast
1.80 +  then obtain a where a: "a \<in> rel_interior S"  by blast
1.81 +  with ST have "a \<in> T"  by blast
1.82    have *: "\<And>x. x \<in> T \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
1.83      apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
1.84      using assms by blast
1.85 @@ -11013,8 +11023,7 @@
1.86      apply (simp add: aff_dim_eq_dim [of c] affine_hull_span_gen [of c] \<open>c \<in> S\<close> hull_inc dim_eq_hyperplane
1.87                  del: One_nat_def)
1.88      apply (rule ex_cong)
1.89 -    using span_0
1.90 -    apply (force simp: \<open>c = 0\<close>)
1.91 +    apply (metis (mono_tags) span_0 \<open>c = 0\<close> image_add_0 inner_zero_right mem_Collect_eq)
1.92      done
1.93    next
1.94      case False
1.95 @@ -11048,7 +11057,7 @@
1.96    qed
1.97  qed
1.98
1.99 -corollary aff_dim_hyperplane:
1.100 +corollary aff_dim_hyperplane [simp]:
1.101    fixes a :: "'a::euclidean_space"
1.102    shows "a \<noteq> 0 \<Longrightarrow> aff_dim {x. a \<bullet> x = r} = DIM('a) - 1"
1.103  by (metis aff_dim_eq_hyperplane affine_hull_eq affine_hyperplane)
1.104 @@ -11379,17 +11388,17 @@
1.105
1.106  subsection\<open> Some results on decomposing convex hulls, e.g. simplicial subdivision\<close>
1.107
1.108 -lemma
1.109 +lemma
1.110    fixes s :: "'a::euclidean_space set"
1.111 -  assumes "~ (affine_dependent(s \<union> t))"
1.112 +  assumes "~ (affine_dependent(s \<union> t))"
1.113      shows convex_hull_Int_subset: "convex hull s \<inter> convex hull t \<subseteq> convex hull (s \<inter> t)" (is ?C)
1.114        and affine_hull_Int_subset: "affine hull s \<inter> affine hull t \<subseteq> affine hull (s \<inter> t)" (is ?A)
1.115  proof -
1.116    have [simp]: "finite s" "finite t"
1.117      using aff_independent_finite assms by blast+
1.118 -    have "setsum u (s \<inter> t) = 1 \<and>
1.119 -          (\<Sum>v\<in>s \<inter> t. u v *\<^sub>R v) = (\<Sum>v\<in>s. u v *\<^sub>R v)"
1.120 -      if [simp]:  "setsum u s = 1"
1.121 +    have "setsum u (s \<inter> t) = 1 \<and>
1.122 +          (\<Sum>v\<in>s \<inter> t. u v *\<^sub>R v) = (\<Sum>v\<in>s. u v *\<^sub>R v)"
1.123 +      if [simp]:  "setsum u s = 1"
1.124                   "setsum v t = 1"
1.125           and eq: "(\<Sum>x\<in>t. v x *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x)" for u v
1.126      proof -
1.127 @@ -11408,7 +11417,7 @@
1.128      then have u [simp]: "\<And>x. x \<in> s \<Longrightarrow> u x = (if x \<in> t then v x else 0)"
1.129        by (simp add: f_def) presburger
1.130      have "setsum u (s \<inter> t) = setsum u s"
1.131 -      by (simp add: setsum.inter_restrict)
1.132 +      by (simp add: setsum.inter_restrict)
1.133      then have "setsum u (s \<inter> t) = 1"
1.134        using that by linarith
1.135      moreover have "(\<Sum>v\<in>s \<inter> t. u v *\<^sub>R v) = (\<Sum>v\<in>s. u v *\<^sub>R v)"
1.136 @@ -11423,7 +11432,7 @@
1.137
1.138  proposition affine_hull_Int:
1.139    fixes s :: "'a::euclidean_space set"
1.140 -  assumes "~ (affine_dependent(s \<union> t))"
1.141 +  assumes "~ (affine_dependent(s \<union> t))"
1.142      shows "affine hull (s \<inter> t) = affine hull s \<inter> affine hull t"
1.143  apply (rule subset_antisym)
1.145 @@ -11431,20 +11440,20 @@
1.146
1.147  proposition convex_hull_Int:
1.148    fixes s :: "'a::euclidean_space set"
1.149 -  assumes "~ (affine_dependent(s \<union> t))"
1.150 +  assumes "~ (affine_dependent(s \<union> t))"
1.151      shows "convex hull (s \<inter> t) = convex hull s \<inter> convex hull t"
1.152  apply (rule subset_antisym)
1.154  by (simp add: convex_hull_Int_subset assms)
1.155
1.156 -proposition
1.157 +proposition
1.158    fixes s :: "'a::euclidean_space set set"
1.159 -  assumes "~ (affine_dependent (\<Union>s))"
1.160 +  assumes "~ (affine_dependent (\<Union>s))"
1.161      shows affine_hull_Inter: "affine hull (\<Inter>s) = (\<Inter>t\<in>s. affine hull t)" (is "?A")
1.162        and convex_hull_Inter: "convex hull (\<Inter>s) = (\<Inter>t\<in>s. convex hull t)" (is "?C")
1.163  proof -
1.164    have "finite s"
1.165 -    using aff_independent_finite assms finite_UnionD by blast
1.166 +    using aff_independent_finite assms finite_UnionD by blast
1.167    then have "?A \<and> ?C" using assms
1.168    proof (induction s rule: finite_induct)
1.169      case empty then show ?case by auto
1.170 @@ -11515,11 +11524,11 @@
1.171      have ind: "\<not> affine_dependent (\<Union>a\<in>c - b. c - {a})"
1.172        by (rule affine_independent_subset [OF indc]) auto
1.173      have affeq: "affine hull s = (\<Inter>x\<in>(\<lambda>a. c - {a}) ` (c - b). affine hull x)"
1.174 -      using \<open>b \<subseteq> c\<close> False
1.175 +      using \<open>b \<subseteq> c\<close> False
1.176        apply (subst affine_hull_Inter [OF ind, symmetric])
1.177        apply (simp add: eq double_diff)
1.178        done
1.179 -    have *: "1 + aff_dim (c - {t}) = int (DIM('a))"
1.180 +    have *: "1 + aff_dim (c - {t}) = int (DIM('a))"
1.181              if t: "t \<in> c" for t
1.182      proof -
1.183        have "insert t c = c"
1.184 @@ -11537,4 +11546,592 @@
1.185    qed
1.186  qed
1.187
1.189 +
1.190 +lemma eq_span_insert_eq:
1.191 +  assumes "(x - y) \<in> span S"
1.192 +    shows "span(insert x S) = span(insert y S)"
1.193 +proof -
1.194 +  have *: "span(insert x S) \<subseteq> span(insert y S)" if "(x - y) \<in> span S" for x y
1.195 +  proof -
1.196 +    have 1: "(r *\<^sub>R x - r *\<^sub>R y) \<in> span S" for r
1.197 +      by (metis real_vector.scale_right_diff_distrib span_mul that)
1.198 +    have 2: "(z - k *\<^sub>R y) - k *\<^sub>R (x - y) = z - k *\<^sub>R x" for  z k
1.199 +      by (simp add: real_vector.scale_right_diff_distrib)
1.200 +  show ?thesis
1.201 +    apply (clarsimp simp add: span_breakdown_eq)
1.203 +  qed
1.204 +  show ?thesis
1.205 +    apply (intro subset_antisym * assms)
1.206 +    using assms subspace_neg subspace_span minus_diff_eq by force
1.207 +qed
1.208 +
1.209 +lemma dim_psubset:
1.210 +    fixes S :: "'a :: euclidean_space set"
1.211 +    shows "span S \<subset> span T \<Longrightarrow> dim S < dim T"
1.212 +by (metis (no_types, hide_lams) dim_span less_le not_le subspace_dim_equal subspace_span)
1.213 +
1.214 +
1.215 +lemma basis_subspace_exists:
1.216 +  fixes S :: "'a::euclidean_space set"
1.217 +  shows
1.218 +   "subspace S
1.219 +        \<Longrightarrow> \<exists>b. finite b \<and> b \<subseteq> S \<and>
1.220 +                independent b \<and> span b = S \<and> card b = dim S"
1.221 +by (metis span_subspace basis_exists independent_imp_finite)
1.222 +
1.223 +lemma affine_hyperplane_sums_eq_UNIV_0:
1.224 +  fixes S :: "'a :: euclidean_space set"
1.225 +  assumes "affine S"
1.226 +     and "0 \<in> S" and "w \<in> S"
1.227 +     and "a \<bullet> w \<noteq> 0"
1.228 +   shows "{x + y| x y. x \<in> S \<and> a \<bullet> y = 0} = UNIV"
1.229 +proof -
1.230 +  have "subspace S"
1.231 +    by (simp add: assms subspace_affine)
1.232 +  have span1: "span {y. a \<bullet> y = 0} \<subseteq> span {x + y |x y. x \<in> S \<and> a \<bullet> y = 0}"
1.233 +    apply (rule span_mono)
1.234 +    using \<open>0 \<in> S\<close> add.left_neutral by force
1.235 +  have "w \<notin> span {y. a \<bullet> y = 0}"
1.236 +    using \<open>a \<bullet> w \<noteq> 0\<close> span_induct subspace_hyperplane by auto
1.237 +  moreover have "w \<in> span {x + y |x y. x \<in> S \<and> a \<bullet> y = 0}"
1.238 +    using \<open>w \<in> S\<close>
1.239 +    by (metis (mono_tags, lifting) inner_zero_right mem_Collect_eq pth_d span_superset)
1.240 +  ultimately have span2: "span {y. a \<bullet> y = 0} \<noteq> span {x + y |x y. x \<in> S \<and> a \<bullet> y = 0}"
1.241 +    by blast
1.242 +  have "a \<noteq> 0" using assms inner_zero_left by blast
1.243 +  then have "DIM('a) - 1 = dim {y. a \<bullet> y = 0}"
1.244 +    by (simp add: dim_hyperplane)
1.245 +  also have "... < dim {x + y |x y. x \<in> S \<and> a \<bullet> y = 0}"
1.246 +    using span1 span2 by (blast intro: dim_psubset)
1.247 +  finally have DIM_lt: "DIM('a) - 1 < dim {x + y |x y. x \<in> S \<and> a \<bullet> y = 0}" .
1.248 +  have subs: "subspace {x + y| x y. x \<in> S \<and> a \<bullet> y = 0}"
1.249 +    using subspace_sums [OF \<open>subspace S\<close> subspace_hyperplane] by simp
1.250 +  moreover have "span {x + y| x y. x \<in> S \<and> a \<bullet> y = 0} = UNIV"
1.251 +    apply (rule dim_eq_full [THEN iffD1])
1.252 +    apply (rule antisym [OF dim_subset_UNIV])
1.253 +    using DIM_lt apply simp
1.254 +    done
1.255 +  ultimately show ?thesis
1.256 +    by (simp add: subs) (metis (lifting) span_eq subs)
1.257 +qed
1.258 +
1.259 +proposition affine_hyperplane_sums_eq_UNIV:
1.260 +  fixes S :: "'a :: euclidean_space set"
1.261 +  assumes "affine S"
1.262 +      and "S \<inter> {v. a \<bullet> v = b} \<noteq> {}"
1.263 +      and "S - {v. a \<bullet> v = b} \<noteq> {}"
1.264 +    shows "{x + y| x y. x \<in> S \<and> a \<bullet> y = b} = UNIV"
1.265 +proof (cases "a = 0")
1.266 +  case True with assms show ?thesis
1.267 +    by (auto simp: if_splits)
1.268 +next
1.269 +  case False
1.270 +  obtain c where "c \<in> S" and c: "a \<bullet> c = b"
1.271 +    using assms by force
1.272 +  with affine_diffs_subspace [OF \<open>affine S\<close>]
1.273 +  have "subspace (op + (- c) ` S)" by blast
1.274 +  then have aff: "affine (op + (- c) ` S)"
1.275 +    by (simp add: subspace_imp_affine)
1.276 +  have 0: "0 \<in> op + (- c) ` S"
1.277 +    by (simp add: \<open>c \<in> S\<close>)
1.278 +  obtain d where "d \<in> S" and "a \<bullet> d \<noteq> b" and dc: "d-c \<in> op + (- c) ` S"
1.279 +    using assms by auto
1.280 +  then have adc: "a \<bullet> (d - c) \<noteq> 0"
1.281 +    by (simp add: c inner_diff_right)
1.282 +  let ?U = "op + (c+c) ` {x + y |x y. x \<in> op + (- c) ` S \<and> a \<bullet> y = 0}"
1.283 +  have "u + v \<in> op + (c + c) ` {x + v |x v. x \<in> op + (- c) ` S \<and> a \<bullet> v = 0}"
1.284 +              if "u \<in> S" "b = a \<bullet> v" for u v
1.285 +    apply (rule_tac x="u+v-c-c" in image_eqI)
1.286 +    apply (simp_all add: algebra_simps)
1.287 +    apply (rule_tac x="u-c" in exI)
1.288 +    apply (rule_tac x="v-c" in exI)
1.289 +    apply (simp add: algebra_simps that c)
1.290 +    done
1.291 +  moreover have "\<lbrakk>a \<bullet> v = 0; u \<in> S\<rbrakk>
1.292 +       \<Longrightarrow> \<exists>x ya. v + (u + c) = x + ya \<and> x \<in> S \<and> a \<bullet> ya = b" for v u
1.293 +    by (metis add.left_commute c inner_right_distrib pth_d)
1.294 +  ultimately have "{x + y |x y. x \<in> S \<and> a \<bullet> y = b} = ?U"
1.295 +    by (fastforce simp: algebra_simps)
1.296 +  also have "... = op + (c+c) ` UNIV"
1.298 +  also have "... = UNIV"
1.299 +    by (simp add: translation_UNIV)
1.300 +  finally show ?thesis .
1.301 +qed
1.302 +
1.303 +proposition dim_sums_Int:
1.304 +    fixes S :: "'a :: euclidean_space set"
1.305 +  assumes "subspace S" "subspace T"
1.306 +  shows "dim {x + y |x y. x \<in> S \<and> y \<in> T} + dim(S \<inter> T) = dim S + dim T"
1.307 +proof -
1.308 +  obtain B where B: "B \<subseteq> S \<inter> T" "S \<inter> T \<subseteq> span B"
1.309 +             and indB: "independent B"
1.310 +             and cardB: "card B = dim (S \<inter> T)"
1.311 +    using basis_exists by blast
1.312 +  then obtain C D where "B \<subseteq> C" "C \<subseteq> S" "independent C" "S \<subseteq> span C"
1.313 +                    and "B \<subseteq> D" "D \<subseteq> T" "independent D" "T \<subseteq> span D"
1.314 +    using maximal_independent_subset_extend
1.315 +    by (metis Int_subset_iff \<open>B \<subseteq> S \<inter> T\<close> indB)
1.316 +  then have "finite B" "finite C" "finite D"
1.317 +    by (simp_all add: independent_imp_finite indB independent_bound)
1.318 +  have Beq: "B = C \<inter> D"
1.319 +    apply (rule sym)
1.320 +    apply (rule spanning_subset_independent)
1.321 +    using \<open>B \<subseteq> C\<close> \<open>B \<subseteq> D\<close> apply blast
1.322 +    apply (meson \<open>independent C\<close> independent_mono inf.cobounded1)
1.323 +    using B \<open>C \<subseteq> S\<close> \<open>D \<subseteq> T\<close> apply auto
1.324 +    done
1.325 +  then have Deq: "D = B \<union> (D - C)"
1.326 +    by blast
1.327 +  have CUD: "C \<union> D \<subseteq> {x + y |x y. x \<in> S \<and> y \<in> T}"
1.328 +    apply safe
1.329 +    apply (metis add.right_neutral subsetCE \<open>C \<subseteq> S\<close> \<open>subspace T\<close> set_eq_subset span_0 span_minimal)
1.330 +    apply (metis add.left_neutral subsetCE \<open>D \<subseteq> T\<close> \<open>subspace S\<close> set_eq_subset span_0 span_minimal)
1.331 +    done
1.332 +  have "a v = 0" if 0: "(\<Sum>v\<in>C. a v *\<^sub>R v) + (\<Sum>v\<in>D - C. a v *\<^sub>R v) = 0"
1.333 +                 and v: "v \<in> C \<union> (D-C)" for a v
1.334 +  proof -
1.335 +    have eq: "(\<Sum>v\<in>D - C. a v *\<^sub>R v) = - (\<Sum>v\<in>C. a v *\<^sub>R v)"
1.336 +      using that add_eq_0_iff by blast
1.337 +    have "(\<Sum>v\<in>D - C. a v *\<^sub>R v) \<in> S"
1.338 +      apply (subst eq)
1.339 +      apply (rule subspace_neg [OF \<open>subspace S\<close>])
1.340 +      apply (rule subspace_setsum [OF \<open>subspace S\<close>])
1.341 +      by (meson subsetCE subspace_mul \<open>C \<subseteq> S\<close> \<open>subspace S\<close>)
1.342 +    moreover have "(\<Sum>v\<in>D - C. a v *\<^sub>R v) \<in> T"
1.343 +      apply (rule subspace_setsum [OF \<open>subspace T\<close>])
1.344 +      by (meson DiffD1 \<open>D \<subseteq> T\<close> \<open>subspace T\<close> subset_eq subspace_def)
1.345 +    ultimately have "(\<Sum>v \<in> D-C. a v *\<^sub>R v) \<in> span B"
1.346 +      using B by blast
1.347 +    then obtain e where e: "(\<Sum>v\<in>B. e v *\<^sub>R v) = (\<Sum>v \<in> D-C. a v *\<^sub>R v)"
1.348 +      using span_finite [OF \<open>finite B\<close>] by blast
1.349 +    have "\<And>c v. \<lbrakk>(\<Sum>v\<in>C. c v *\<^sub>R v) = 0; v \<in> C\<rbrakk> \<Longrightarrow> c v = 0"
1.350 +      using independent_explicit \<open>independent C\<close> by blast
1.351 +    def cc \<equiv> "(\<lambda>x. if x \<in> B then a x + e x else a x)"
1.352 +    have [simp]: "C \<inter> B = B" "D \<inter> B = B" "C \<inter> - B = C-D" "B \<inter> (D - C) = {}"
1.353 +      using \<open>B \<subseteq> C\<close> \<open>B \<subseteq> D\<close> Beq by blast+
1.354 +    have f2: "(\<Sum>v\<in>C \<inter> D. e v *\<^sub>R v) = (\<Sum>v\<in>D - C. a v *\<^sub>R v)"
1.355 +      using Beq e by presburger
1.356 +    have f3: "(\<Sum>v\<in>C \<union> D. a v *\<^sub>R v) = (\<Sum>v\<in>C - D. a v *\<^sub>R v) + (\<Sum>v\<in>D - C. a v *\<^sub>R v) + (\<Sum>v\<in>C \<inter> D. a v *\<^sub>R v)"
1.357 +      using \<open>finite C\<close> \<open>finite D\<close> setsum.union_diff2 by blast
1.358 +    have f4: "(\<Sum>v\<in>C \<union> (D - C). a v *\<^sub>R v) = (\<Sum>v\<in>C. a v *\<^sub>R v) + (\<Sum>v\<in>D - C. a v *\<^sub>R v)"
1.359 +      by (meson Diff_disjoint \<open>finite C\<close> \<open>finite D\<close> finite_Diff setsum.union_disjoint)
1.360 +    have "(\<Sum>v\<in>C. cc v *\<^sub>R v) = 0"
1.361 +      using 0 f2 f3 f4
1.362 +      apply (simp add: cc_def Beq if_smult \<open>finite C\<close> setsum.If_cases algebra_simps setsum.distrib)
1.364 +      done
1.365 +    then have "\<And>v. v \<in> C \<Longrightarrow> cc v = 0"
1.366 +      using independent_explicit \<open>independent C\<close> by blast
1.367 +    then have C0: "\<And>v. v \<in> C - B \<Longrightarrow> a v = 0"
1.368 +      by (simp add: cc_def Beq) meson
1.369 +    then have [simp]: "(\<Sum>x\<in>C - B. a x *\<^sub>R x) = 0"
1.370 +      by simp
1.371 +    have "(\<Sum>x\<in>C. a x *\<^sub>R x) = (\<Sum>x\<in>B. a x *\<^sub>R x)"
1.372 +    proof -
1.373 +      have "C - D = C - B"
1.374 +        using Beq by blast
1.375 +      then show ?thesis
1.376 +        using Beq \<open>(\<Sum>x\<in>C - B. a x *\<^sub>R x) = 0\<close> f3 f4 by auto
1.377 +    qed
1.378 +    with 0 have Dcc0: "(\<Sum>v\<in>D. a v *\<^sub>R v) = 0"
1.379 +      apply (subst Deq)
1.380 +      by (simp add: \<open>finite B\<close> \<open>finite D\<close> setsum_Un)
1.381 +    then have D0: "\<And>v. v \<in> D \<Longrightarrow> a v = 0"
1.382 +      using independent_explicit \<open>independent D\<close> by blast
1.383 +    show ?thesis
1.384 +      using v C0 D0 Beq by blast
1.385 +  qed
1.386 +  then have "independent (C \<union> (D - C))"
1.387 +    by (simp add: independent_explicit \<open>finite C\<close> \<open>finite D\<close> setsum_Un del: Un_Diff_cancel)
1.388 +  then have indCUD: "independent (C \<union> D)" by simp
1.389 +  have "dim (S \<inter> T) = card B"
1.390 +    by (rule dim_unique [OF B indB refl])
1.391 +  moreover have "dim S = card C"
1.392 +    by (metis \<open>C \<subseteq> S\<close> \<open>independent C\<close> \<open>S \<subseteq> span C\<close> basis_card_eq_dim)
1.393 +  moreover have "dim T = card D"
1.394 +    by (metis \<open>D \<subseteq> T\<close> \<open>independent D\<close> \<open>T \<subseteq> span D\<close> basis_card_eq_dim)
1.395 +  moreover have "dim {x + y |x y. x \<in> S \<and> y \<in> T} = card(C \<union> D)"
1.396 +    apply (rule dim_unique [OF CUD _ indCUD refl], clarify)
1.397 +    apply (meson \<open>S \<subseteq> span C\<close> \<open>T \<subseteq> span D\<close> span_add span_inc span_minimal subsetCE subspace_span sup.bounded_iff)
1.398 +    done
1.399 +  ultimately show ?thesis
1.400 +    using \<open>B = C \<inter> D\<close> [symmetric]
1.401 +    by (simp add:  \<open>independent C\<close> \<open>independent D\<close> card_Un_Int independent_finite)
1.402 +qed
1.403 +
1.404 +
1.405 +lemma aff_dim_sums_Int_0:
1.406 +  assumes "affine S"
1.407 +      and "affine T"
1.408 +      and "0 \<in> S" "0 \<in> T"
1.409 +    shows "aff_dim {x + y| x y. x \<in> S \<and> y \<in> T} = (aff_dim S + aff_dim T) - aff_dim(S \<inter> T)"
1.410 +proof -
1.411 +  have "0 \<in> {x + y |x y. x \<in> S \<and> y \<in> T}"
1.412 +    using assms by force
1.413 +  then have 0: "0 \<in> affine hull {x + y |x y. x \<in> S \<and> y \<in> T}"
1.414 +    by (metis (lifting) hull_inc)
1.415 +  have sub: "subspace S"  "subspace T"
1.416 +    using assms by (auto simp: subspace_affine)
1.417 +  show ?thesis
1.418 +    using dim_sums_Int [OF sub] by (simp add: aff_dim_zero assms 0 hull_inc)
1.419 +qed
1.420 +
1.421 +proposition aff_dim_sums_Int:
1.422 +  assumes "affine S"
1.423 +      and "affine T"
1.424 +      and "S \<inter> T \<noteq> {}"
1.425 +    shows "aff_dim {x + y| x y. x \<in> S \<and> y \<in> T} = (aff_dim S + aff_dim T) - aff_dim(S \<inter> T)"
1.426 +proof -
1.427 +  obtain a where a: "a \<in> S" "a \<in> T" using assms by force
1.428 +  have aff: "affine (op+ (-a) ` S)"  "affine (op+ (-a) ` T)"
1.429 +    using assms by (auto simp: affine_translation [symmetric])
1.430 +  have zero: "0 \<in> (op+ (-a) ` S)"  "0 \<in> (op+ (-a) ` T)"
1.431 +    using a assms by auto
1.432 +  have [simp]: "{x + y |x y. x \<in> op + (- a) ` S \<and> y \<in> op + (- a) ` T} =
1.433 +        op + (- 2 *\<^sub>R a) ` {x + y| x y. x \<in> S \<and> y \<in> T}"
1.434 +    by (force simp: algebra_simps scaleR_2)
1.435 +  have [simp]: "op + (- a) ` S \<inter> op + (- a) ` T = op + (- a) ` (S \<inter> T)"
1.436 +    by auto
1.437 +  show ?thesis
1.438 +    using aff_dim_sums_Int_0 [OF aff zero]
1.439 +    by (auto simp: aff_dim_translation_eq)
1.440 +qed
1.441 +
1.442 +lemma aff_dim_affine_Int_hyperplane:
1.443 +  fixes a :: "'a::euclidean_space"
1.444 +  assumes "affine S"
1.445 +    shows "aff_dim(S \<inter> {x. a \<bullet> x = b}) =
1.446 +             (if S \<inter> {v. a \<bullet> v = b} = {} then - 1
1.447 +              else if S \<subseteq> {v. a \<bullet> v = b} then aff_dim S
1.448 +              else aff_dim S - 1)"
1.449 +proof (cases "a = 0")
1.450 +  case True with assms show ?thesis
1.451 +    by auto
1.452 +next
1.453 +  case False
1.454 +  then have "aff_dim (S \<inter> {x. a \<bullet> x = b}) = aff_dim S - 1"
1.455 +            if "x \<in> S" "a \<bullet> x \<noteq> b" and non: "S \<inter> {v. a \<bullet> v = b} \<noteq> {}" for x
1.456 +  proof -
1.457 +    have [simp]: "{x + y| x y. x \<in> S \<and> a \<bullet> y = b} = UNIV"
1.458 +      using affine_hyperplane_sums_eq_UNIV [OF assms non] that  by blast
1.459 +    show ?thesis
1.460 +      using aff_dim_sums_Int [OF assms affine_hyperplane non]
1.461 +      by (simp add: of_nat_diff False)
1.462 +  qed
1.463 +  then show ?thesis
1.464 +    by (metis (mono_tags, lifting) inf.orderE aff_dim_empty_eq mem_Collect_eq subsetI)
1.465 +qed
1.466 +
1.467 +lemma aff_dim_lt_full:
1.468 +  fixes S :: "'a::euclidean_space set"
1.469 +  shows "aff_dim S < DIM('a) \<longleftrightarrow> (affine hull S \<noteq> UNIV)"
1.470 +by (metis (no_types) aff_dim_affine_hull aff_dim_le_DIM aff_dim_UNIV affine_hull_UNIV less_le)
1.471 +
1.472 +subsection\<open> Orthogonal bases, Gram-Schmidt process, and related theorems\<close>
1.473 +
1.474 +lemma span_delete_0 [simp]: "span(S - {0}) = span S"
1.475 +proof
1.476 +  show "span (S - {0}) \<subseteq> span S"
1.477 +    by (blast intro!: span_mono)
1.478 +next
1.479 +  have "span S \<subseteq> span(insert 0 (S - {0}))"
1.480 +    by (blast intro!: span_mono)
1.481 +  also have "... \<subseteq> span(S - {0})"
1.482 +    using span_insert_0 by blast
1.483 +  finally show "span S \<subseteq> span (S - {0})" .
1.484 +qed
1.485 +
1.486 +lemma span_image_scale:
1.487 +  assumes "finite S" and nz: "\<And>x. x \<in> S \<Longrightarrow> c x \<noteq> 0"
1.488 +    shows "span ((\<lambda>x. c x *\<^sub>R x) ` S) = span S"
1.489 +using assms
1.490 +proof (induction S arbitrary: c)
1.491 +  case (empty c) show ?case by simp
1.492 +next
1.493 +  case (insert x F c)
1.494 +  show ?case
1.495 +  proof (intro set_eqI iffI)
1.496 +    fix y
1.497 +      assume "y \<in> span ((\<lambda>x. c x *\<^sub>R x) ` insert x F)"
1.498 +      then show "y \<in> span (insert x F)"
1.499 +        using insert by (force simp: span_breakdown_eq)
1.500 +  next
1.501 +    fix y
1.502 +      assume "y \<in> span (insert x F)"
1.503 +      then show "y \<in> span ((\<lambda>x. c x *\<^sub>R x) ` insert x F)"
1.504 +        using insert
1.505 +        apply (clarsimp simp: span_breakdown_eq)
1.506 +        apply (rule_tac x="k / c x" in exI)
1.507 +        by simp
1.508 +  qed
1.509 +qed
1.510 +
1.511 +lemma pairwise_orthogonal_independent:
1.512 +  assumes "pairwise orthogonal S" and "0 \<notin> S"
1.513 +    shows "independent S"
1.514 +proof -
1.515 +  have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
1.516 +    using assms by (simp add: pairwise_def orthogonal_def)
1.517 +  have "False" if "a \<in> S" and a: "a \<in> span (S - {a})" for a
1.518 +  proof -
1.519 +    obtain T U where "T \<subseteq> S - {a}" "a = (\<Sum>v\<in>T. U v *\<^sub>R v)"
1.520 +      using a by (force simp: span_explicit)
1.521 +    then have "a \<bullet> a = a \<bullet> (\<Sum>v\<in>T. U v *\<^sub>R v)"
1.522 +      by simp
1.523 +    also have "... = 0"
1.524 +      apply (simp add: inner_setsum_right)
1.526 +      by (metis "0" DiffE \<open>T \<subseteq> S - {a}\<close> mult_not_zero singletonI subsetCE \<open>a \<in> S\<close>)
1.527 +    finally show ?thesis
1.528 +      using \<open>0 \<notin> S\<close> \<open>a \<in> S\<close> by auto
1.529 +  qed
1.530 +  then show ?thesis
1.531 +    by (force simp: dependent_def)
1.532 +qed
1.533 +
1.534 +lemma pairwise_orthogonal_imp_finite:
1.535 +  fixes S :: "'a::euclidean_space set"
1.536 +  assumes "pairwise orthogonal S"
1.537 +    shows "finite S"
1.538 +proof -
1.539 +  have "independent (S - {0})"
1.540 +    apply (rule pairwise_orthogonal_independent)
1.541 +     apply (metis Diff_iff assms pairwise_def)
1.542 +    by blast
1.543 +  then show ?thesis
1.544 +    by (meson independent_imp_finite infinite_remove)
1.545 +qed
1.546 +
1.547 +lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}"
1.548 +  by (simp add: subspace_def orthogonal_clauses)
1.549 +
1.550 +lemma subspace_orthogonal_to_vectors: "subspace {y. \<forall>x \<in> S. orthogonal x y}"
1.551 +  by (simp add: subspace_def orthogonal_clauses)
1.552 +
1.553 +lemma orthogonal_to_span:
1.554 +  assumes a: "a \<in> span S" and x: "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
1.555 +    shows "orthogonal x a"
1.556 +apply (rule CollectD, rule span_induct [OF a subspace_orthogonal_to_vector])
1.558 +done
1.559 +
1.560 +proposition Gram_Schmidt_step:
1.561 +  fixes S :: "'a::euclidean_space set"
1.562 +  assumes S: "pairwise orthogonal S" and x: "x \<in> span S"
1.563 +    shows "orthogonal x (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b))"
1.564 +proof -
1.565 +  have "finite S"
1.566 +    by (simp add: S pairwise_orthogonal_imp_finite)
1.567 +  have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)) x"
1.568 +       if "x \<in> S" for x
1.569 +  proof -
1.570 +    have "a \<bullet> x = (\<Sum>y\<in>S. if y = x then y \<bullet> a else 0)"
1.571 +      by (simp add: \<open>finite S\<close> inner_commute setsum.delta that)
1.572 +    also have "... =  (\<Sum>b\<in>S. b \<bullet> a * (b \<bullet> x) / (b \<bullet> b))"
1.573 +      apply (rule setsum.cong [OF refl], simp)
1.574 +      by (meson S orthogonal_def pairwise_def that)
1.575 +   finally show ?thesis
1.576 +     by (simp add: orthogonal_def algebra_simps inner_setsum_left)
1.577 +  qed
1.578 +  then show ?thesis
1.579 +    using orthogonal_to_span orthogonal_commute x by blast
1.580 +qed
1.581 +
1.582 +
1.583 +lemma orthogonal_extension_aux:
1.584 +  fixes S :: "'a::euclidean_space set"
1.585 +  assumes "finite T" "finite S" "pairwise orthogonal S"
1.586 +    shows "\<exists>U. pairwise orthogonal (S \<union> U) \<and> span (S \<union> U) = span (S \<union> T)"
1.587 +using assms
1.588 +proof (induction arbitrary: S)
1.589 +  case empty then show ?case
1.590 +    by simp (metis sup_bot_right)
1.591 +next
1.592 +  case (insert a T)
1.593 +  have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
1.594 +    using insert by (simp add: pairwise_def orthogonal_def)
1.595 +  def a' \<equiv> "a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)"
1.596 +  obtain U where orthU: "pairwise orthogonal (S \<union> insert a' U)"
1.597 +             and spanU: "span (insert a' S \<union> U) = span (insert a' S \<union> T)"
1.598 +    apply (rule exE [OF insert.IH [of "insert a' S"]])
1.599 +    apply (auto simp: Gram_Schmidt_step a'_def insert.prems orthogonal_commute pairwise_orthogonal_insert span_clauses)
1.600 +    done
1.601 +  have orthS: "\<And>x. x \<in> S \<Longrightarrow> a' \<bullet> x = 0"
1.602 +    apply (simp add: a'_def)
1.603 +    using Gram_Schmidt_step [OF \<open>pairwise orthogonal S\<close>]
1.604 +    apply (force simp: orthogonal_def inner_commute span_inc [THEN subsetD])
1.605 +    done
1.606 +  have "span (S \<union> insert a' U) = span (insert a' (S \<union> T))"
1.607 +    using spanU by simp
1.608 +  also have "... = span (insert a (S \<union> T))"
1.609 +    apply (rule eq_span_insert_eq)
1.610 +    apply (simp add: a'_def span_neg span_setsum span_clauses(1) span_mul)
1.611 +    done
1.612 +  also have "... = span (S \<union> insert a T)"
1.613 +    by simp
1.614 +  finally show ?case
1.615 +    apply (rule_tac x="insert a' U" in exI)
1.616 +    using orthU apply auto
1.617 +    done
1.618 +qed
1.619 +
1.620 +
1.621 +proposition orthogonal_extension:
1.622 +  fixes S :: "'a::euclidean_space set"
1.623 +  assumes S: "pairwise orthogonal S"
1.624 +  obtains U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
1.625 +proof -
1.626 +  obtain B where "finite B" "span B = span T"
1.627 +    using basis_subspace_exists [of "span T"] subspace_span by auto
1.628 +  with orthogonal_extension_aux [of B S]
1.629 +  obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> B)"
1.630 +    using assms pairwise_orthogonal_imp_finite by auto
1.631 +  show ?thesis
1.632 +    apply (rule_tac U=U in that)
1.633 +     apply (simp add: \<open>pairwise orthogonal (S \<union> U)\<close>)
1.634 +    by (metis \<open>span (S \<union> U) = span (S \<union> B)\<close> \<open>span B = span T\<close> span_union)
1.635 +qed
1.636 +
1.637 +corollary orthogonal_extension_strong:
1.638 +  fixes S :: "'a::euclidean_space set"
1.639 +  assumes S: "pairwise orthogonal S"
1.640 +  obtains U where "U \<inter> (insert 0 S) = {}" "pairwise orthogonal (S \<union> U)"
1.641 +                   "span (S \<union> U) = span (S \<union> T)"
1.642 +proof -
1.643 +  obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
1.644 +    using orthogonal_extension assms by blast
1.645 +  then show ?thesis
1.646 +    apply (rule_tac U = "U - (insert 0 S)" in that)
1.647 +      apply blast
1.648 +     apply (force simp: pairwise_def)
1.649 +    apply (metis (no_types, lifting) Un_Diff_cancel span_insert_0 span_union)
1.650 +  done
1.651 +qed
1.652 +
1.653 +subsection\<open>Decomposing a vector into parts in orthogonal subspaces.\<close>
1.654 +
1.655 +text\<open>existence of orthonormal basis for a subspace.\<close>
1.656 +
1.657 +lemma orthogonal_spanningset_subspace:
1.658 +  fixes S :: "'a :: euclidean_space set"
1.659 +  assumes "subspace S"
1.660 +  obtains B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S"
1.661 +proof -
1.662 +  obtain B where "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S"
1.663 +    using basis_exists by blast
1.664 +  with orthogonal_extension [of "{}" B]
1.665 +  show ?thesis
1.666 +    by (metis Un_empty_left assms pairwise_empty span_inc span_subspace that)
1.667 +qed
1.668 +
1.669 +lemma orthogonal_basis_subspace:
1.670 +  fixes S :: "'a :: euclidean_space set"
1.671 +  assumes "subspace S"
1.672 +  obtains B where "0 \<notin> B" "B \<subseteq> S" "pairwise orthogonal B" "independent B"
1.673 +                  "card B = dim S" "span B = S"
1.674 +proof -
1.675 +  obtain B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S"
1.676 +    using assms orthogonal_spanningset_subspace by blast
1.677 +  then show ?thesis
1.678 +    apply (rule_tac B = "B - {0}" in that)
1.679 +    apply (auto simp: indep_card_eq_dim_span pairwise_subset Diff_subset pairwise_orthogonal_independent elim: pairwise_subset)
1.680 +    done
1.681 +qed
1.682 +
1.683 +proposition orthogonal_subspace_decomp_exists:
1.684 +  fixes S :: "'a :: euclidean_space set"
1.685 +  obtains y z where "y \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"
1.686 +proof -
1.687 +  obtain T where "0 \<notin> T" "T \<subseteq> span S" "pairwise orthogonal T" "independent T" "card T = dim (span S)" "span T = span S"
1.688 +    using orthogonal_basis_subspace subspace_span by blast
1.689 +  let ?a = "\<Sum>b\<in>T. (b \<bullet> x / (b \<bullet> b)) *\<^sub>R b"
1.690 +  have orth: "orthogonal (x - ?a) w" if "w \<in> span S" for w
1.691 +    by (simp add: Gram_Schmidt_step \<open>pairwise orthogonal T\<close> \<open>span T = span S\<close> orthogonal_commute that)
1.692 +  show ?thesis
1.693 +    apply (rule_tac y = "?a" and z = "x - ?a" in that)
1.694 +      apply (meson \<open>T \<subseteq> span S\<close> span_mul span_setsum subsetCE)
1.695 +     apply (fact orth, simp)
1.696 +    done
1.697 +qed
1.698 +
1.699 +lemma orthogonal_subspace_decomp_unique:
1.700 +  fixes S :: "'a :: euclidean_space set"
1.701 +  assumes "x + y = x' + y'"
1.702 +      and ST: "x \<in> span S" "x' \<in> span S" "y \<in> span T" "y' \<in> span T"
1.703 +      and orth: "\<And>a b. \<lbrakk>a \<in> S; b \<in> T\<rbrakk> \<Longrightarrow> orthogonal a b"
1.704 +  shows "x = x' \<and> y = y'"
1.705 +proof -
1.706 +  have "x + y - y' = x'"
1.707 +    by (simp add: assms)
1.708 +  moreover have "\<And>a b. \<lbrakk>a \<in> span S; b \<in> span T\<rbrakk> \<Longrightarrow> orthogonal a b"
1.709 +    by (meson orth orthogonal_commute orthogonal_to_span)
1.710 +  ultimately have "0 = x' - x"
1.711 +    by (metis (full_types) add_diff_cancel_left' ST diff_right_commute orthogonal_clauses(10) orthogonal_clauses(5) orthogonal_self)
1.712 +  with assms show ?thesis by auto
1.713 +qed
1.714 +
1.715 +
1.716 +text\<open> If we take a slice out of a set, we can do it perpendicularly,
1.717 +  with the normal vector to the slice parallel to the affine hull.\<close>
1.718 +
1.719 +proposition affine_parallel_slice:
1.720 +  fixes S :: "'a :: euclidean_space set"
1.721 +  assumes "affine S"
1.722 +      and "S \<inter> {x. a \<bullet> x \<le> b} \<noteq> {}"
1.723 +      and "~ (S \<subseteq> {x. a \<bullet> x \<le> b})"
1.724 +  obtains a' b' where "a' \<noteq> 0"
1.725 +                   "S \<inter> {x. a' \<bullet> x \<le> b'} = S \<inter> {x. a \<bullet> x \<le> b}"
1.726 +                   "S \<inter> {x. a' \<bullet> x = b'} = S \<inter> {x. a \<bullet> x = b}"
1.727 +                   "\<And>w. w \<in> S \<Longrightarrow> (w + a') \<in> S"
1.728 +proof (cases "S \<inter> {x. a \<bullet> x = b} = {}")
1.729 +  case True
1.730 +  then obtain u v where "u \<in> S" "v \<in> S" "a \<bullet> u \<le> b" "a \<bullet> v > b"
1.731 +    using assms by (auto simp: not_le)
1.732 +  def \<eta> \<equiv> "u + ((b - a \<bullet> u) / (a \<bullet> v - a \<bullet> u)) *\<^sub>R (v - u)"
1.733 +  have "\<eta> \<in> S"
1.734 +    by (simp add: \<eta>_def \<open>u \<in> S\<close> \<open>v \<in> S\<close> \<open>affine S\<close> mem_affine_3_minus)
1.735 +  moreover have "a \<bullet> \<eta> = b"
1.736 +    using \<open>a \<bullet> u \<le> b\<close> \<open>b < a \<bullet> v\<close>
1.738 +  ultimately have False
1.739 +    using True by force
1.740 +  then show ?thesis ..
1.741 +next
1.742 +  case False
1.743 +  then obtain z where "z \<in> S" and z: "a \<bullet> z = b"
1.744 +    using assms by auto
1.745 +  with affine_diffs_subspace [OF \<open>affine S\<close>]
1.746 +  have sub: "subspace (op + (- z) ` S)" by blast
1.747 +  then have aff: "affine (op + (- z) ` S)" and span: "span (op + (- z) ` S) = (op + (- z) ` S)"
1.748 +    by (auto simp: subspace_imp_affine)
1.749 +  obtain a' a'' where a': "a' \<in> span (op + (- z) ` S)" and a: "a = a' + a''"
1.750 +                  and "\<And>w. w \<in> span (op + (- z) ` S) \<Longrightarrow> orthogonal a'' w"
1.751 +      using orthogonal_subspace_decomp_exists [of "op + (- z) ` S" "a"] by metis
1.752 +  then have "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> (w-z) = 0"
1.753 +    by (simp add: imageI orthogonal_def span)
1.754 +  then have a'': "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> w = (a - a') \<bullet> z"
1.755 +    by (simp add: a inner_diff_right)
1.756 +  then have ba'': "\<And>w. w \<in> S \<Longrightarrow> a'' \<bullet> w = b - a' \<bullet> z"
1.757 +    by (simp add: inner_diff_left z)
1.758 +  have "\<And>w. w \<in> op + (- z) ` S \<Longrightarrow> (w + a') \<in> op + (- z) ` S"
1.759 +    by (metis subspace_add a' span_eq sub)
1.760 +  then have Sclo: "\<And>w. w \<in> S \<Longrightarrow> (w + a') \<in> S"
1.761 +    by fastforce
1.762 +  show ?thesis
1.763 +  proof (cases "a' = 0")
1.764 +    case True
1.765 +    with a assms True a'' diff_zero less_irrefl show ?thesis
1.766 +      by auto
1.767 +  next
1.768 +    case False
1.769 +    show ?thesis
1.770 +      apply (rule_tac a' = "a'" and b' = "a' \<bullet> z" in that)
1.771 +      apply (auto simp: a ba'' inner_left_distrib False Sclo)
1.772 +      done
1.773 +  qed
1.774 +qed
1.775 +
1.776  end
```