src/HOL/Analysis/Linear_Algebra.thy
changeset 69675 880ab0f27ddf
parent 69674 fc252acb7100
child 69683 8b3458ca0762
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 16 16:50:35 2019 -0500
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 16 18:14:02 2019 -0500
     1.3 @@ -30,6 +30,79 @@
     1.4  lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x \<in> (UNIV::'a::finite set)}"
     1.5    using finite finite_image_set by blast
     1.6  
     1.7 +lemma substdbasis_expansion_unique:
     1.8 +  includes inner_syntax
     1.9 +  assumes d: "d \<subseteq> Basis"
    1.10 +  shows "(\<Sum>i\<in>d. f i *\<^sub>R i) = (x::'a::euclidean_space) \<longleftrightarrow>
    1.11 +    (\<forall>i\<in>Basis. (i \<in> d \<longrightarrow> f i = x \<bullet> i) \<and> (i \<notin> d \<longrightarrow> x \<bullet> i = 0))"
    1.12 +proof -
    1.13 +  have *: "\<And>x a b P. x * (if P then a else b) = (if P then x * a else x * b)"
    1.14 +    by auto
    1.15 +  have **: "finite d"
    1.16 +    by (auto intro: finite_subset[OF assms])
    1.17 +  have ***: "\<And>i. i \<in> Basis \<Longrightarrow> (\<Sum>i\<in>d. f i *\<^sub>R i) \<bullet> i = (\<Sum>x\<in>d. if x = i then f x else 0)"
    1.18 +    using d
    1.19 +    by (auto intro!: sum.cong simp: inner_Basis inner_sum_left)
    1.20 +  show ?thesis
    1.21 +    unfolding euclidean_eq_iff[where 'a='a] by (auto simp: sum.delta[OF **] ***)
    1.22 +qed
    1.23 +
    1.24 +lemma independent_substdbasis: "d \<subseteq> Basis \<Longrightarrow> independent d"
    1.25 +  by (rule independent_mono[OF independent_Basis])
    1.26 +
    1.27 +lemma sum_not_0: "sum f A \<noteq> 0 \<Longrightarrow> \<exists>a \<in> A. f a \<noteq> 0"
    1.28 +  by (rule ccontr) auto
    1.29 +
    1.30 +lemma subset_translation_eq [simp]:
    1.31 +    fixes a :: "'a::real_vector" shows "(+) a ` s \<subseteq> (+) a ` t \<longleftrightarrow> s \<subseteq> t"
    1.32 +  by auto
    1.33 +
    1.34 +lemma translate_inj_on:
    1.35 +  fixes A :: "'a::ab_group_add set"
    1.36 +  shows "inj_on (\<lambda>x. a + x) A"
    1.37 +  unfolding inj_on_def by auto
    1.38 +
    1.39 +lemma translation_assoc:
    1.40 +  fixes a b :: "'a::ab_group_add"
    1.41 +  shows "(\<lambda>x. b + x) ` ((\<lambda>x. a + x) ` S) = (\<lambda>x. (a + b) + x) ` S"
    1.42 +  by auto
    1.43 +
    1.44 +lemma translation_invert:
    1.45 +  fixes a :: "'a::ab_group_add"
    1.46 +  assumes "(\<lambda>x. a + x) ` A = (\<lambda>x. a + x) ` B"
    1.47 +  shows "A = B"
    1.48 +proof -
    1.49 +  have "(\<lambda>x. -a + x) ` ((\<lambda>x. a + x) ` A) = (\<lambda>x. - a + x) ` ((\<lambda>x. a + x) ` B)"
    1.50 +    using assms by auto
    1.51 +  then show ?thesis
    1.52 +    using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto
    1.53 +qed
    1.54 +
    1.55 +lemma translation_galois:
    1.56 +  fixes a :: "'a::ab_group_add"
    1.57 +  shows "T = ((\<lambda>x. a + x) ` S) \<longleftrightarrow> S = ((\<lambda>x. (- a) + x) ` T)"
    1.58 +  using translation_assoc[of "-a" a S]
    1.59 +  apply auto
    1.60 +  using translation_assoc[of a "-a" T]
    1.61 +  apply auto
    1.62 +  done
    1.63 +
    1.64 +lemma translation_inverse_subset:
    1.65 +  assumes "((\<lambda>x. - a + x) ` V) \<le> (S :: 'n::ab_group_add set)"
    1.66 +  shows "V \<le> ((\<lambda>x. a + x) ` S)"
    1.67 +proof -
    1.68 +  {
    1.69 +    fix x
    1.70 +    assume "x \<in> V"
    1.71 +    then have "x-a \<in> S" using assms by auto
    1.72 +    then have "x \<in> {a + v |v. v \<in> S}"
    1.73 +      apply auto
    1.74 +      apply (rule exI[of _ "x-a"], simp)
    1.75 +      done
    1.76 +    then have "x \<in> ((\<lambda>x. a+x) ` S)" by auto
    1.77 +  }
    1.78 +  then show ?thesis by auto
    1.79 +qed
    1.80  
    1.81  subsection%unimportant \<open>More interesting properties of the norm\<close>
    1.82  
    1.83 @@ -224,6 +297,66 @@
    1.84  qed
    1.85  
    1.86  
    1.87 +subsection%important  \<open>Orthogonality of a transformation\<close>
    1.88 +
    1.89 +definition%important  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
    1.90 +
    1.91 +lemma%unimportant  orthogonal_transformation:
    1.92 +  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v. norm (f v) = norm v)"
    1.93 +  unfolding orthogonal_transformation_def
    1.94 +  apply auto
    1.95 +  apply (erule_tac x=v in allE)+
    1.96 +  apply (simp add: norm_eq_sqrt_inner)
    1.97 +  apply (simp add: dot_norm linear_add[symmetric])
    1.98 +  done
    1.99 +
   1.100 +lemma%unimportant  orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
   1.101 +  by (simp add: linear_iff orthogonal_transformation_def)
   1.102 +
   1.103 +lemma%unimportant  orthogonal_orthogonal_transformation:
   1.104 +    "orthogonal_transformation f \<Longrightarrow> orthogonal (f x) (f y) \<longleftrightarrow> orthogonal x y"
   1.105 +  by (simp add: orthogonal_def orthogonal_transformation_def)
   1.106 +
   1.107 +lemma%unimportant  orthogonal_transformation_compose:
   1.108 +   "\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)"
   1.109 +  by (auto simp: orthogonal_transformation_def linear_compose)
   1.110 +
   1.111 +lemma%unimportant  orthogonal_transformation_neg:
   1.112 +  "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
   1.113 +  by (auto simp: orthogonal_transformation_def dest: linear_compose_neg)
   1.114 +
   1.115 +lemma%unimportant  orthogonal_transformation_scaleR: "orthogonal_transformation f \<Longrightarrow> f (c *\<^sub>R v) = c *\<^sub>R f v"
   1.116 +  by (simp add: linear_iff orthogonal_transformation_def)
   1.117 +
   1.118 +lemma%unimportant  orthogonal_transformation_linear:
   1.119 +   "orthogonal_transformation f \<Longrightarrow> linear f"
   1.120 +  by (simp add: orthogonal_transformation_def)
   1.121 +
   1.122 +lemma%unimportant  orthogonal_transformation_inj:
   1.123 +  "orthogonal_transformation f \<Longrightarrow> inj f"
   1.124 +  unfolding orthogonal_transformation_def inj_on_def
   1.125 +  by (metis vector_eq)
   1.126 +
   1.127 +lemma%unimportant  orthogonal_transformation_surj:
   1.128 +  "orthogonal_transformation f \<Longrightarrow> surj f"
   1.129 +  for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   1.130 +  by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear)
   1.131 +
   1.132 +lemma%unimportant  orthogonal_transformation_bij:
   1.133 +  "orthogonal_transformation f \<Longrightarrow> bij f"
   1.134 +  for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   1.135 +  by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj)
   1.136 +
   1.137 +lemma%unimportant  orthogonal_transformation_inv:
   1.138 +  "orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)"
   1.139 +  for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   1.140 +  by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj)
   1.141 +
   1.142 +lemma%unimportant  orthogonal_transformation_norm:
   1.143 +  "orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x"
   1.144 +  by (metis orthogonal_transformation)
   1.145 +
   1.146 +
   1.147  subsection \<open>Bilinear functions\<close>
   1.148  
   1.149  definition%important
   1.150 @@ -1210,4 +1343,540 @@
   1.151    qed
   1.152  qed
   1.153  
   1.154 +
   1.155 +subsection\<open>Properties of special hyperplanes\<close>
   1.156 +
   1.157 +lemma subspace_hyperplane: "subspace {x. a \<bullet> x = 0}"
   1.158 +  by (simp add: subspace_def inner_right_distrib)
   1.159 +
   1.160 +lemma subspace_hyperplane2: "subspace {x. x \<bullet> a = 0}"
   1.161 +  by (simp add: inner_commute inner_right_distrib subspace_def)
   1.162 +
   1.163 +lemma special_hyperplane_span:
   1.164 +  fixes S :: "'n::euclidean_space set"
   1.165 +  assumes "k \<in> Basis"
   1.166 +  shows "{x. k \<bullet> x = 0} = span (Basis - {k})"
   1.167 +proof -
   1.168 +  have *: "x \<in> span (Basis - {k})" if "k \<bullet> x = 0" for x
   1.169 +  proof -
   1.170 +    have "x = (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b)"
   1.171 +      by (simp add: euclidean_representation)
   1.172 +    also have "... = (\<Sum>b \<in> Basis - {k}. (x \<bullet> b) *\<^sub>R b)"
   1.173 +      by (auto simp: sum.remove [of _ k] inner_commute assms that)
   1.174 +    finally have "x = (\<Sum>b\<in>Basis - {k}. (x \<bullet> b) *\<^sub>R b)" .
   1.175 +    then show ?thesis
   1.176 +      by (simp add: span_finite)
   1.177 +  qed
   1.178 +  show ?thesis
   1.179 +    apply (rule span_subspace [symmetric])
   1.180 +    using assms
   1.181 +    apply (auto simp: inner_not_same_Basis intro: * subspace_hyperplane)
   1.182 +    done
   1.183 +qed
   1.184 +
   1.185 +lemma dim_special_hyperplane:
   1.186 +  fixes k :: "'n::euclidean_space"
   1.187 +  shows "k \<in> Basis \<Longrightarrow> dim {x. k \<bullet> x = 0} = DIM('n) - 1"
   1.188 +apply (simp add: special_hyperplane_span)
   1.189 +apply (rule dim_unique [OF subset_refl])
   1.190 +apply (auto simp: independent_substdbasis)
   1.191 +apply (metis member_remove remove_def span_base)
   1.192 +done
   1.193 +
   1.194 +proposition dim_hyperplane:
   1.195 +  fixes a :: "'a::euclidean_space"
   1.196 +  assumes "a \<noteq> 0"
   1.197 +    shows "dim {x. a \<bullet> x = 0} = DIM('a) - 1"
   1.198 +proof -
   1.199 +  have span0: "span {x. a \<bullet> x = 0} = {x. a \<bullet> x = 0}"
   1.200 +    by (rule span_unique) (auto simp: subspace_hyperplane)
   1.201 +  then obtain B where "independent B"
   1.202 +              and Bsub: "B \<subseteq> {x. a \<bullet> x = 0}"
   1.203 +              and subspB: "{x. a \<bullet> x = 0} \<subseteq> span B"
   1.204 +              and card0: "(card B = dim {x. a \<bullet> x = 0})"
   1.205 +              and ortho: "pairwise orthogonal B"
   1.206 +    using orthogonal_basis_exists by metis
   1.207 +  with assms have "a \<notin> span B"
   1.208 +    by (metis (mono_tags, lifting) span_eq inner_eq_zero_iff mem_Collect_eq span0)
   1.209 +  then have ind: "independent (insert a B)"
   1.210 +    by (simp add: \<open>independent B\<close> independent_insert)
   1.211 +  have "finite B"
   1.212 +    using \<open>independent B\<close> independent_bound by blast
   1.213 +  have "UNIV \<subseteq> span (insert a B)"
   1.214 +  proof fix y::'a
   1.215 +    obtain r z where z: "y = r *\<^sub>R a + z" "a \<bullet> z = 0"
   1.216 +      apply (rule_tac r="(a \<bullet> y) / (a \<bullet> a)" and z = "y - ((a \<bullet> y) / (a \<bullet> a)) *\<^sub>R a" in that)
   1.217 +      using assms
   1.218 +      by (auto simp: algebra_simps)
   1.219 +    show "y \<in> span (insert a B)"
   1.220 +      by (metis (mono_tags, lifting) z Bsub span_eq_iff
   1.221 +         add_diff_cancel_left' mem_Collect_eq span0 span_breakdown_eq span_subspace subspB)
   1.222 +  qed
   1.223 +  then have dima: "DIM('a) = dim(insert a B)"
   1.224 +    by (metis independent_Basis span_Basis dim_eq_card top.extremum_uniqueI)
   1.225 +  then show ?thesis
   1.226 +    by (metis (mono_tags, lifting) Bsub Diff_insert_absorb \<open>a \<notin> span B\<close> ind card0
   1.227 +        card_Diff_singleton dim_span indep_card_eq_dim_span insertI1 subsetCE
   1.228 +        subspB)
   1.229 +qed
   1.230 +
   1.231 +lemma lowdim_eq_hyperplane:
   1.232 +  fixes S :: "'a::euclidean_space set"
   1.233 +  assumes "dim S = DIM('a) - 1"
   1.234 +  obtains a where "a \<noteq> 0" and "span S = {x. a \<bullet> x = 0}"
   1.235 +proof -
   1.236 +  have dimS: "dim S < DIM('a)"
   1.237 +    by (simp add: assms)
   1.238 +  then obtain b where b: "b \<noteq> 0" "span S \<subseteq> {a. b \<bullet> a = 0}"
   1.239 +    using lowdim_subset_hyperplane [of S] by fastforce
   1.240 +  show ?thesis
   1.241 +    apply (rule that[OF b(1)])
   1.242 +    apply (rule subspace_dim_equal)
   1.243 +    by (auto simp: assms b dim_hyperplane dim_span subspace_hyperplane
   1.244 +        subspace_span)
   1.245 +qed
   1.246 +
   1.247 +lemma dim_eq_hyperplane:
   1.248 +  fixes S :: "'n::euclidean_space set"
   1.249 +  shows "dim S = DIM('n) - 1 \<longleftrightarrow> (\<exists>a. a \<noteq> 0 \<and> span S = {x. a \<bullet> x = 0})"
   1.250 +by (metis One_nat_def dim_hyperplane dim_span lowdim_eq_hyperplane)
   1.251 +
   1.252 +
   1.253 +subsection\<open> Orthogonal bases, Gram-Schmidt process, and related theorems\<close>
   1.254 +
   1.255 +lemma pairwise_orthogonal_independent:
   1.256 +  assumes "pairwise orthogonal S" and "0 \<notin> S"
   1.257 +    shows "independent S"
   1.258 +proof -
   1.259 +  have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   1.260 +    using assms by (simp add: pairwise_def orthogonal_def)
   1.261 +  have "False" if "a \<in> S" and a: "a \<in> span (S - {a})" for a
   1.262 +  proof -
   1.263 +    obtain T U where "T \<subseteq> S - {a}" "a = (\<Sum>v\<in>T. U v *\<^sub>R v)"
   1.264 +      using a by (force simp: span_explicit)
   1.265 +    then have "a \<bullet> a = a \<bullet> (\<Sum>v\<in>T. U v *\<^sub>R v)"
   1.266 +      by simp
   1.267 +    also have "... = 0"
   1.268 +      apply (simp add: inner_sum_right)
   1.269 +      apply (rule comm_monoid_add_class.sum.neutral)
   1.270 +      by (metis "0" DiffE \<open>T \<subseteq> S - {a}\<close> mult_not_zero singletonI subsetCE \<open>a \<in> S\<close>)
   1.271 +    finally show ?thesis
   1.272 +      using \<open>0 \<notin> S\<close> \<open>a \<in> S\<close> by auto
   1.273 +  qed
   1.274 +  then show ?thesis
   1.275 +    by (force simp: dependent_def)
   1.276 +qed
   1.277 +
   1.278 +lemma pairwise_orthogonal_imp_finite:
   1.279 +  fixes S :: "'a::euclidean_space set"
   1.280 +  assumes "pairwise orthogonal S"
   1.281 +    shows "finite S"
   1.282 +proof -
   1.283 +  have "independent (S - {0})"
   1.284 +    apply (rule pairwise_orthogonal_independent)
   1.285 +     apply (metis Diff_iff assms pairwise_def)
   1.286 +    by blast
   1.287 +  then show ?thesis
   1.288 +    by (meson independent_imp_finite infinite_remove)
   1.289 +qed
   1.290 +
   1.291 +lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}"
   1.292 +  by (simp add: subspace_def orthogonal_clauses)
   1.293 +
   1.294 +lemma subspace_orthogonal_to_vectors: "subspace {y. \<forall>x \<in> S. orthogonal x y}"
   1.295 +  by (simp add: subspace_def orthogonal_clauses)
   1.296 +
   1.297 +lemma orthogonal_to_span:
   1.298 +  assumes a: "a \<in> span S" and x: "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
   1.299 +    shows "orthogonal x a"
   1.300 +  by (metis a orthogonal_clauses(1,2,4)
   1.301 +      span_induct_alt x)
   1.302 +
   1.303 +proposition Gram_Schmidt_step:
   1.304 +  fixes S :: "'a::euclidean_space set"
   1.305 +  assumes S: "pairwise orthogonal S" and x: "x \<in> span S"
   1.306 +    shows "orthogonal x (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b))"
   1.307 +proof -
   1.308 +  have "finite S"
   1.309 +    by (simp add: S pairwise_orthogonal_imp_finite)
   1.310 +  have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)) x"
   1.311 +       if "x \<in> S" for x
   1.312 +  proof -
   1.313 +    have "a \<bullet> x = (\<Sum>y\<in>S. if y = x then y \<bullet> a else 0)"
   1.314 +      by (simp add: \<open>finite S\<close> inner_commute sum.delta that)
   1.315 +    also have "... =  (\<Sum>b\<in>S. b \<bullet> a * (b \<bullet> x) / (b \<bullet> b))"
   1.316 +      apply (rule sum.cong [OF refl], simp)
   1.317 +      by (meson S orthogonal_def pairwise_def that)
   1.318 +   finally show ?thesis
   1.319 +     by (simp add: orthogonal_def algebra_simps inner_sum_left)
   1.320 +  qed
   1.321 +  then show ?thesis
   1.322 +    using orthogonal_to_span orthogonal_commute x by blast
   1.323 +qed
   1.324 +
   1.325 +
   1.326 +lemma orthogonal_extension_aux:
   1.327 +  fixes S :: "'a::euclidean_space set"
   1.328 +  assumes "finite T" "finite S" "pairwise orthogonal S"
   1.329 +    shows "\<exists>U. pairwise orthogonal (S \<union> U) \<and> span (S \<union> U) = span (S \<union> T)"
   1.330 +using assms
   1.331 +proof (induction arbitrary: S)
   1.332 +  case empty then show ?case
   1.333 +    by simp (metis sup_bot_right)
   1.334 +next
   1.335 +  case (insert a T)
   1.336 +  have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   1.337 +    using insert by (simp add: pairwise_def orthogonal_def)
   1.338 +  define a' where "a' = a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)"
   1.339 +  obtain U where orthU: "pairwise orthogonal (S \<union> insert a' U)"
   1.340 +             and spanU: "span (insert a' S \<union> U) = span (insert a' S \<union> T)"
   1.341 +    by (rule exE [OF insert.IH [of "insert a' S"]])
   1.342 +      (auto simp: Gram_Schmidt_step a'_def insert.prems orthogonal_commute
   1.343 +        pairwise_orthogonal_insert span_clauses)
   1.344 +  have orthS: "\<And>x. x \<in> S \<Longrightarrow> a' \<bullet> x = 0"
   1.345 +    apply (simp add: a'_def)
   1.346 +    using Gram_Schmidt_step [OF \<open>pairwise orthogonal S\<close>]
   1.347 +    apply (force simp: orthogonal_def inner_commute span_superset [THEN subsetD])
   1.348 +    done
   1.349 +  have "span (S \<union> insert a' U) = span (insert a' (S \<union> T))"
   1.350 +    using spanU by simp
   1.351 +  also have "... = span (insert a (S \<union> T))"
   1.352 +    apply (rule eq_span_insert_eq)
   1.353 +    apply (simp add: a'_def span_neg span_sum span_base span_mul)
   1.354 +    done
   1.355 +  also have "... = span (S \<union> insert a T)"
   1.356 +    by simp
   1.357 +  finally show ?case
   1.358 +    by (rule_tac x="insert a' U" in exI) (use orthU in auto)
   1.359 +qed
   1.360 +
   1.361 +
   1.362 +proposition orthogonal_extension:
   1.363 +  fixes S :: "'a::euclidean_space set"
   1.364 +  assumes S: "pairwise orthogonal S"
   1.365 +  obtains U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
   1.366 +proof -
   1.367 +  obtain B where "finite B" "span B = span T"
   1.368 +    using basis_subspace_exists [of "span T"] subspace_span by metis
   1.369 +  with orthogonal_extension_aux [of B S]
   1.370 +  obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> B)"
   1.371 +    using assms pairwise_orthogonal_imp_finite by auto
   1.372 +  with \<open>span B = span T\<close> show ?thesis
   1.373 +    by (rule_tac U=U in that) (auto simp: span_Un)
   1.374 +qed
   1.375 +
   1.376 +corollary%unimportant orthogonal_extension_strong:
   1.377 +  fixes S :: "'a::euclidean_space set"
   1.378 +  assumes S: "pairwise orthogonal S"
   1.379 +  obtains U where "U \<inter> (insert 0 S) = {}" "pairwise orthogonal (S \<union> U)"
   1.380 +                  "span (S \<union> U) = span (S \<union> T)"
   1.381 +proof -
   1.382 +  obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
   1.383 +    using orthogonal_extension assms by blast
   1.384 +  then show ?thesis
   1.385 +    apply (rule_tac U = "U - (insert 0 S)" in that)
   1.386 +      apply blast
   1.387 +     apply (force simp: pairwise_def)
   1.388 +    apply (metis Un_Diff_cancel Un_insert_left span_redundant span_zero)
   1.389 +    done
   1.390 +qed
   1.391 +
   1.392 +subsection\<open>Decomposing a vector into parts in orthogonal subspaces\<close>
   1.393 +
   1.394 +text\<open>existence of orthonormal basis for a subspace.\<close>
   1.395 +
   1.396 +lemma orthogonal_spanningset_subspace:
   1.397 +  fixes S :: "'a :: euclidean_space set"
   1.398 +  assumes "subspace S"
   1.399 +  obtains B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S"
   1.400 +proof -
   1.401 +  obtain B where "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S"
   1.402 +    using basis_exists by blast
   1.403 +  with orthogonal_extension [of "{}" B]
   1.404 +  show ?thesis
   1.405 +    by (metis Un_empty_left assms pairwise_empty span_superset span_subspace that)
   1.406 +qed
   1.407 +
   1.408 +lemma orthogonal_basis_subspace:
   1.409 +  fixes S :: "'a :: euclidean_space set"
   1.410 +  assumes "subspace S"
   1.411 +  obtains B where "0 \<notin> B" "B \<subseteq> S" "pairwise orthogonal B" "independent B"
   1.412 +                  "card B = dim S" "span B = S"
   1.413 +proof -
   1.414 +  obtain B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S"
   1.415 +    using assms orthogonal_spanningset_subspace by blast
   1.416 +  then show ?thesis
   1.417 +    apply (rule_tac B = "B - {0}" in that)
   1.418 +    apply (auto simp: indep_card_eq_dim_span pairwise_subset pairwise_orthogonal_independent elim: pairwise_subset)
   1.419 +    done
   1.420 +qed
   1.421 +
   1.422 +proposition orthonormal_basis_subspace:
   1.423 +  fixes S :: "'a :: euclidean_space set"
   1.424 +  assumes "subspace S"
   1.425 +  obtains B where "B \<subseteq> S" "pairwise orthogonal B"
   1.426 +              and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
   1.427 +              and "independent B" "card B = dim S" "span B = S"
   1.428 +proof -
   1.429 +  obtain B where "0 \<notin> B" "B \<subseteq> S"
   1.430 +             and orth: "pairwise orthogonal B"
   1.431 +             and "independent B" "card B = dim S" "span B = S"
   1.432 +    by (blast intro: orthogonal_basis_subspace [OF assms])
   1.433 +  have 1: "(\<lambda>x. x /\<^sub>R norm x) ` B \<subseteq> S"
   1.434 +    using \<open>span B = S\<close> span_superset span_mul by fastforce
   1.435 +  have 2: "pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` B)"
   1.436 +    using orth by (force simp: pairwise_def orthogonal_clauses)
   1.437 +  have 3: "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` B \<Longrightarrow> norm x = 1"
   1.438 +    by (metis (no_types, lifting) \<open>0 \<notin> B\<close> image_iff norm_sgn sgn_div_norm)
   1.439 +  have 4: "independent ((\<lambda>x. x /\<^sub>R norm x) ` B)"
   1.440 +    by (metis "2" "3" norm_zero pairwise_orthogonal_independent zero_neq_one)
   1.441 +  have "inj_on (\<lambda>x. x /\<^sub>R norm x) B"
   1.442 +  proof
   1.443 +    fix x y
   1.444 +    assume "x \<in> B" "y \<in> B" "x /\<^sub>R norm x = y /\<^sub>R norm y"
   1.445 +    moreover have "\<And>i. i \<in> B \<Longrightarrow> norm (i /\<^sub>R norm i) = 1"
   1.446 +      using 3 by blast
   1.447 +    ultimately show "x = y"
   1.448 +      by (metis norm_eq_1 orth orthogonal_clauses(7) orthogonal_commute orthogonal_def pairwise_def zero_neq_one)
   1.449 +  qed
   1.450 +  then have 5: "card ((\<lambda>x. x /\<^sub>R norm x) ` B) = dim S"
   1.451 +    by (metis \<open>card B = dim S\<close> card_image)
   1.452 +  have 6: "span ((\<lambda>x. x /\<^sub>R norm x) ` B) = S"
   1.453 +    by (metis "1" "4" "5" assms card_eq_dim independent_imp_finite span_subspace)
   1.454 +  show ?thesis
   1.455 +    by (rule that [OF 1 2 3 4 5 6])
   1.456 +qed
   1.457 +
   1.458 +
   1.459 +proposition%unimportant orthogonal_to_subspace_exists_gen:
   1.460 +  fixes S :: "'a :: euclidean_space set"
   1.461 +  assumes "span S \<subset> span T"
   1.462 +  obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
   1.463 +proof -
   1.464 +  obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
   1.465 +             and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
   1.466 +             and "independent B" "card B = dim S" "span B = span S"
   1.467 +    by (rule orthonormal_basis_subspace [of "span S", OF subspace_span])
   1.468 +      (auto simp: dim_span)
   1.469 +  with assms obtain u where spanBT: "span B \<subseteq> span T" and "u \<notin> span B" "u \<in> span T"
   1.470 +    by auto
   1.471 +  obtain C where orthBC: "pairwise orthogonal (B \<union> C)" and spanBC: "span (B \<union> C) = span (B \<union> {u})"
   1.472 +    by (blast intro: orthogonal_extension [OF orthB])
   1.473 +  show thesis
   1.474 +  proof (cases "C \<subseteq> insert 0 B")
   1.475 +    case True
   1.476 +    then have "C \<subseteq> span B"
   1.477 +      using span_eq
   1.478 +      by (metis span_insert_0 subset_trans)
   1.479 +    moreover have "u \<in> span (B \<union> C)"
   1.480 +      using \<open>span (B \<union> C) = span (B \<union> {u})\<close> span_superset by force
   1.481 +    ultimately show ?thesis
   1.482 +      using True \<open>u \<notin> span B\<close>
   1.483 +      by (metis Un_insert_left span_insert_0 sup.orderE)
   1.484 +  next
   1.485 +    case False
   1.486 +    then obtain x where "x \<in> C" "x \<noteq> 0" "x \<notin> B"
   1.487 +      by blast
   1.488 +    then have "x \<in> span T"
   1.489 +      by (metis (no_types, lifting) Un_insert_right Un_upper2 \<open>u \<in> span T\<close> spanBT spanBC
   1.490 +          \<open>u \<in> span T\<close> insert_subset span_superset span_mono
   1.491 +          span_span subsetCE subset_trans sup_bot.comm_neutral)
   1.492 +    moreover have "orthogonal x y" if "y \<in> span B" for y
   1.493 +      using that
   1.494 +    proof (rule span_induct)
   1.495 +      show "subspace {a. orthogonal x a}"
   1.496 +        by (simp add: subspace_orthogonal_to_vector)
   1.497 +      show "\<And>b. b \<in> B \<Longrightarrow> orthogonal x b"
   1.498 +        by (metis Un_iff \<open>x \<in> C\<close> \<open>x \<notin> B\<close> orthBC pairwise_def)
   1.499 +    qed
   1.500 +    ultimately show ?thesis
   1.501 +      using \<open>x \<noteq> 0\<close> that \<open>span B = span S\<close> by auto
   1.502 +  qed
   1.503 +qed
   1.504 +
   1.505 +corollary%unimportant orthogonal_to_subspace_exists:
   1.506 +  fixes S :: "'a :: euclidean_space set"
   1.507 +  assumes "dim S < DIM('a)"
   1.508 +  obtains x where "x \<noteq> 0" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
   1.509 +proof -
   1.510 +have "span S \<subset> UNIV"
   1.511 +  by (metis (mono_tags) UNIV_I assms inner_eq_zero_iff less_le lowdim_subset_hyperplane
   1.512 +      mem_Collect_eq top.extremum_strict top.not_eq_extremum)
   1.513 +  with orthogonal_to_subspace_exists_gen [of S UNIV] that show ?thesis
   1.514 +    by (auto simp: span_UNIV)
   1.515 +qed
   1.516 +
   1.517 +corollary%unimportant orthogonal_to_vector_exists:
   1.518 +  fixes x :: "'a :: euclidean_space"
   1.519 +  assumes "2 \<le> DIM('a)"
   1.520 +  obtains y where "y \<noteq> 0" "orthogonal x y"
   1.521 +proof -
   1.522 +  have "dim {x} < DIM('a)"
   1.523 +    using assms by auto
   1.524 +  then show thesis
   1.525 +    by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that)
   1.526 +qed
   1.527 +
   1.528 +proposition%unimportant orthogonal_subspace_decomp_exists:
   1.529 +  fixes S :: "'a :: euclidean_space set"
   1.530 +  obtains y z
   1.531 +  where "y \<in> span S"
   1.532 +    and "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w"
   1.533 +    and "x = y + z"
   1.534 +proof -
   1.535 +  obtain T where "0 \<notin> T" "T \<subseteq> span S" "pairwise orthogonal T" "independent T"
   1.536 +    "card T = dim (span S)" "span T = span S"
   1.537 +    using orthogonal_basis_subspace subspace_span by blast
   1.538 +  let ?a = "\<Sum>b\<in>T. (b \<bullet> x / (b \<bullet> b)) *\<^sub>R b"
   1.539 +  have orth: "orthogonal (x - ?a) w" if "w \<in> span S" for w
   1.540 +    by (simp add: Gram_Schmidt_step \<open>pairwise orthogonal T\<close> \<open>span T = span S\<close>
   1.541 +        orthogonal_commute that)
   1.542 +  show ?thesis
   1.543 +    apply (rule_tac y = "?a" and z = "x - ?a" in that)
   1.544 +      apply (meson \<open>T \<subseteq> span S\<close> span_scale span_sum subsetCE)
   1.545 +     apply (fact orth, simp)
   1.546 +    done
   1.547 +qed
   1.548 +
   1.549 +lemma orthogonal_subspace_decomp_unique:
   1.550 +  fixes S :: "'a :: euclidean_space set"
   1.551 +  assumes "x + y = x' + y'"
   1.552 +      and ST: "x \<in> span S" "x' \<in> span S" "y \<in> span T" "y' \<in> span T"
   1.553 +      and orth: "\<And>a b. \<lbrakk>a \<in> S; b \<in> T\<rbrakk> \<Longrightarrow> orthogonal a b"
   1.554 +  shows "x = x' \<and> y = y'"
   1.555 +proof -
   1.556 +  have "x + y - y' = x'"
   1.557 +    by (simp add: assms)
   1.558 +  moreover have "\<And>a b. \<lbrakk>a \<in> span S; b \<in> span T\<rbrakk> \<Longrightarrow> orthogonal a b"
   1.559 +    by (meson orth orthogonal_commute orthogonal_to_span)
   1.560 +  ultimately have "0 = x' - x"
   1.561 +    by (metis (full_types) add_diff_cancel_left' ST diff_right_commute orthogonal_clauses(10) orthogonal_clauses(5) orthogonal_self)
   1.562 +  with assms show ?thesis by auto
   1.563 +qed
   1.564 +
   1.565 +lemma vector_in_orthogonal_spanningset:
   1.566 +  fixes a :: "'a::euclidean_space"
   1.567 +  obtains S where "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
   1.568 +  by (metis UNIV_I Un_iff empty_iff insert_subset orthogonal_extension pairwise_def
   1.569 +      pairwise_orthogonal_insert span_UNIV subsetI subset_antisym)
   1.570 +
   1.571 +lemma vector_in_orthogonal_basis:
   1.572 +  fixes a :: "'a::euclidean_space"
   1.573 +  assumes "a \<noteq> 0"
   1.574 +  obtains S where "a \<in> S" "0 \<notin> S" "pairwise orthogonal S" "independent S" "finite S"
   1.575 +                  "span S = UNIV" "card S = DIM('a)"
   1.576 +proof -
   1.577 +  obtain S where S: "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
   1.578 +    using vector_in_orthogonal_spanningset .
   1.579 +  show thesis
   1.580 +  proof
   1.581 +    show "pairwise orthogonal (S - {0})"
   1.582 +      using pairwise_mono S(2) by blast
   1.583 +    show "independent (S - {0})"
   1.584 +      by (simp add: \<open>pairwise orthogonal (S - {0})\<close> pairwise_orthogonal_independent)
   1.585 +    show "finite (S - {0})"
   1.586 +      using \<open>independent (S - {0})\<close> independent_imp_finite by blast
   1.587 +    show "card (S - {0}) = DIM('a)"
   1.588 +      using span_delete_0 [of S] S
   1.589 +      by (simp add: \<open>independent (S - {0})\<close> indep_card_eq_dim_span dim_UNIV)
   1.590 +  qed (use S \<open>a \<noteq> 0\<close> in auto)
   1.591 +qed
   1.592 +
   1.593 +lemma vector_in_orthonormal_basis:
   1.594 +  fixes a :: "'a::euclidean_space"
   1.595 +  assumes "norm a = 1"
   1.596 +  obtains S where "a \<in> S" "pairwise orthogonal S" "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
   1.597 +    "independent S" "card S = DIM('a)" "span S = UNIV"
   1.598 +proof -
   1.599 +  have "a \<noteq> 0"
   1.600 +    using assms by auto
   1.601 +  then obtain S where "a \<in> S" "0 \<notin> S" "finite S"
   1.602 +          and S: "pairwise orthogonal S" "independent S" "span S = UNIV" "card S = DIM('a)"
   1.603 +    by (metis vector_in_orthogonal_basis)
   1.604 +  let ?S = "(\<lambda>x. x /\<^sub>R norm x) ` S"
   1.605 +  show thesis
   1.606 +  proof
   1.607 +    show "a \<in> ?S"
   1.608 +      using \<open>a \<in> S\<close> assms image_iff by fastforce
   1.609 +  next
   1.610 +    show "pairwise orthogonal ?S"
   1.611 +      using \<open>pairwise orthogonal S\<close> by (auto simp: pairwise_def orthogonal_def)
   1.612 +    show "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` S \<Longrightarrow> norm x = 1"
   1.613 +      using \<open>0 \<notin> S\<close> by (auto simp: divide_simps)
   1.614 +    then show "independent ?S"
   1.615 +      by (metis \<open>pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` S)\<close> norm_zero pairwise_orthogonal_independent zero_neq_one)
   1.616 +    have "inj_on (\<lambda>x. x /\<^sub>R norm x) S"
   1.617 +      unfolding inj_on_def
   1.618 +      by (metis (full_types) S(1) \<open>0 \<notin> S\<close> inverse_nonzero_iff_nonzero norm_eq_zero orthogonal_scaleR orthogonal_self pairwise_def)
   1.619 +    then show "card ?S = DIM('a)"
   1.620 +      by (simp add: card_image S)
   1.621 +    show "span ?S = UNIV"
   1.622 +      by (metis (no_types) \<open>0 \<notin> S\<close> \<open>finite S\<close> \<open>span S = UNIV\<close>
   1.623 +          field_class.field_inverse_zero inverse_inverse_eq less_irrefl span_image_scale
   1.624 +          zero_less_norm_iff)
   1.625 +  qed
   1.626 +qed
   1.627 +
   1.628 +proposition dim_orthogonal_sum:
   1.629 +  fixes A :: "'a::euclidean_space set"
   1.630 +  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   1.631 +    shows "dim(A \<union> B) = dim A + dim B"
   1.632 +proof -
   1.633 +  have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   1.634 +    by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms)
   1.635 +  have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   1.636 +    using 1 by (simp add: span_induct [OF _ subspace_hyperplane])
   1.637 +  then have 0: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   1.638 +    by simp
   1.639 +  have "dim(A \<union> B) = dim (span (A \<union> B))"
   1.640 +    by (simp add: dim_span)
   1.641 +  also have "span (A \<union> B) = ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
   1.642 +    by (auto simp add: span_Un image_def)
   1.643 +  also have "dim \<dots> = dim {x + y |x y. x \<in> span A \<and> y \<in> span B}"
   1.644 +    by (auto intro!: arg_cong [where f=dim])
   1.645 +  also have "... = dim {x + y |x y. x \<in> span A \<and> y \<in> span B} + dim(span A \<inter> span B)"
   1.646 +    by (auto simp: dest: 0)
   1.647 +  also have "... = dim (span A) + dim (span B)"
   1.648 +    by (rule dim_sums_Int) (auto simp: subspace_span)
   1.649 +  also have "... = dim A + dim B"
   1.650 +    by (simp add: dim_span)
   1.651 +  finally show ?thesis .
   1.652 +qed
   1.653 +
   1.654 +lemma dim_subspace_orthogonal_to_vectors:
   1.655 +  fixes A :: "'a::euclidean_space set"
   1.656 +  assumes "subspace A" "subspace B" "A \<subseteq> B"
   1.657 +    shows "dim {y \<in> B. \<forall>x \<in> A. orthogonal x y} + dim A = dim B"
   1.658 +proof -
   1.659 +  have "dim (span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)) = dim (span B)"
   1.660 +  proof (rule arg_cong [where f=dim, OF subset_antisym])
   1.661 +    show "span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A) \<subseteq> span B"
   1.662 +      by (simp add: \<open>A \<subseteq> B\<close> Collect_restrict span_mono)
   1.663 +  next
   1.664 +    have *: "x \<in> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)"
   1.665 +         if "x \<in> B" for x
   1.666 +    proof -
   1.667 +      obtain y z where "x = y + z" "y \<in> span A" and orth: "\<And>w. w \<in> span A \<Longrightarrow> orthogonal z w"
   1.668 +        using orthogonal_subspace_decomp_exists [of A x] that by auto
   1.669 +      have "y \<in> span B"
   1.670 +        using \<open>y \<in> span A\<close> assms(3) span_mono by blast
   1.671 +      then have "z \<in> {a \<in> B. \<forall>x. x \<in> A \<longrightarrow> orthogonal x a}"
   1.672 +        apply simp
   1.673 +        using \<open>x = y + z\<close> assms(1) assms(2) orth orthogonal_commute span_add_eq
   1.674 +          span_eq_iff that by blast
   1.675 +      then have z: "z \<in> span {y \<in> B. \<forall>x\<in>A. orthogonal x y}"
   1.676 +        by (meson span_superset subset_iff)
   1.677 +      then show ?thesis
   1.678 +        apply (auto simp: span_Un image_def  \<open>x = y + z\<close> \<open>y \<in> span A\<close>)
   1.679 +        using \<open>y \<in> span A\<close> add.commute by blast
   1.680 +    qed
   1.681 +    show "span B \<subseteq> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)"
   1.682 +      by (rule span_minimal)
   1.683 +        (auto intro: * span_minimal simp: subspace_span)
   1.684 +  qed
   1.685 +  then show ?thesis
   1.686 +    by (metis (no_types, lifting) dim_orthogonal_sum dim_span mem_Collect_eq
   1.687 +        orthogonal_commute orthogonal_def)
   1.688 +qed
   1.689 +
   1.690  end