Reorg, in particular Determinants as well as some linear algebra from Starlike and Change_Of_Vars
authorimmler
Wed Jan 16 18:14:02 2019 -0500 (4 months ago)
changeset 69675880ab0f27ddf
parent 69674 fc252acb7100
child 69676 56acd449da41
Reorg, in particular Determinants as well as some linear algebra from Starlike and Change_Of_Vars
src/HOL/Analysis/Cartesian_Space.thy
src/HOL/Analysis/Change_Of_Vars.thy
src/HOL/Analysis/Convex.thy
src/HOL/Analysis/Cross3.thy
src/HOL/Analysis/Determinants.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Starlike.thy
     1.1 --- a/src/HOL/Analysis/Cartesian_Space.thy	Wed Jan 16 16:50:35 2019 -0500
     1.2 +++ b/src/HOL/Analysis/Cartesian_Space.thy	Wed Jan 16 18:14:02 2019 -0500
     1.3 @@ -930,4 +930,492 @@
     1.4  lemma%unimportant const_vector_cart:"((\<chi> i. d)::real^'n) = (\<Sum>i\<in>Basis. d *\<^sub>R i)"
     1.5    by (rule vector_cart)
     1.6  
     1.7 +subsection%unimportant \<open>Explicit formulas for low dimensions\<close>
     1.8 +
     1.9 +lemma%unimportant  prod_neutral_const: "prod f {(1::nat)..1} = f 1"
    1.10 +  by simp
    1.11 +
    1.12 +lemma%unimportant  prod_2: "prod f {(1::nat)..2} = f 1 * f 2"
    1.13 +  by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
    1.14 +
    1.15 +lemma%unimportant  prod_3: "prod f {(1::nat)..3} = f 1 * f 2 * f 3"
    1.16 +  by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
    1.17 +
    1.18 +
    1.19 +subsection%important  \<open>Orthogonality of a matrix\<close>
    1.20 +
    1.21 +definition%important  "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
    1.22 +  transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
    1.23 +
    1.24 +lemma%unimportant  orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1"
    1.25 +  by (metis matrix_left_right_inverse orthogonal_matrix_def)
    1.26 +
    1.27 +lemma%unimportant  orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)"
    1.28 +  by (simp add: orthogonal_matrix_def)
    1.29 +
    1.30 +lemma%unimportant  orthogonal_matrix_mul:
    1.31 +  fixes A :: "real ^'n^'n"
    1.32 +  assumes  "orthogonal_matrix A" "orthogonal_matrix B"
    1.33 +  shows "orthogonal_matrix(A ** B)"
    1.34 +  using assms
    1.35 +  by (simp add: orthogonal_matrix matrix_transpose_mul matrix_left_right_inverse matrix_mul_assoc)
    1.36 +
    1.37 +lemma%important  orthogonal_transformation_matrix:
    1.38 +  fixes f:: "real^'n \<Rightarrow> real^'n"
    1.39 +  shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)"
    1.40 +  (is "?lhs \<longleftrightarrow> ?rhs")
    1.41 +proof%unimportant -
    1.42 +  let ?mf = "matrix f"
    1.43 +  let ?ot = "orthogonal_transformation f"
    1.44 +  let ?U = "UNIV :: 'n set"
    1.45 +  have fU: "finite ?U" by simp
    1.46 +  let ?m1 = "mat 1 :: real ^'n^'n"
    1.47 +  {
    1.48 +    assume ot: ?ot
    1.49 +    from ot have lf: "Vector_Spaces.linear (*s) (*s) f" and fd: "\<And>v w. f v \<bullet> f w = v \<bullet> w"
    1.50 +      unfolding orthogonal_transformation_def orthogonal_matrix linear_def scalar_mult_eq_scaleR
    1.51 +      by blast+
    1.52 +    {
    1.53 +      fix i j
    1.54 +      let ?A = "transpose ?mf ** ?mf"
    1.55 +      have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)"
    1.56 +        "\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)"
    1.57 +        by simp_all
    1.58 +      from fd[of "axis i 1" "axis j 1",
    1.59 +        simplified matrix_works[OF lf, symmetric] dot_matrix_vector_mul]
    1.60 +      have "?A$i$j = ?m1 $ i $ j"
    1.61 +        by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def
    1.62 +            th0 sum.delta[OF fU] mat_def axis_def)
    1.63 +    }
    1.64 +    then have "orthogonal_matrix ?mf"
    1.65 +      unfolding orthogonal_matrix
    1.66 +      by vector
    1.67 +    with lf have ?rhs
    1.68 +      unfolding linear_def scalar_mult_eq_scaleR
    1.69 +      by blast
    1.70 +  }
    1.71 +  moreover
    1.72 +  {
    1.73 +    assume lf: "Vector_Spaces.linear (*s) (*s) f" and om: "orthogonal_matrix ?mf"
    1.74 +    from lf om have ?lhs
    1.75 +      unfolding orthogonal_matrix_def norm_eq orthogonal_transformation
    1.76 +      apply (simp only: matrix_works[OF lf, symmetric] dot_matrix_vector_mul)
    1.77 +      apply (simp add: dot_matrix_product linear_def scalar_mult_eq_scaleR)
    1.78 +      done
    1.79 +  }
    1.80 +  ultimately show ?thesis
    1.81 +    by (auto simp: linear_def scalar_mult_eq_scaleR)
    1.82 +qed
    1.83 +
    1.84 +
    1.85 +subsection%important \<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
    1.86 +
    1.87 +lemma%unimportant  orthogonal_matrix_transpose [simp]:
    1.88 +     "orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
    1.89 +  by (auto simp: orthogonal_matrix_def)
    1.90 +
    1.91 +lemma%unimportant  orthogonal_matrix_orthonormal_columns:
    1.92 +  fixes A :: "real^'n^'n"
    1.93 +  shows "orthogonal_matrix A \<longleftrightarrow>
    1.94 +          (\<forall>i. norm(column i A) = 1) \<and>
    1.95 +          (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (column i A) (column j A))"
    1.96 +  by (auto simp: orthogonal_matrix matrix_mult_transpose_dot_column vec_eq_iff mat_def norm_eq_1 orthogonal_def)
    1.97 +
    1.98 +lemma%unimportant  orthogonal_matrix_orthonormal_rows:
    1.99 +  fixes A :: "real^'n^'n"
   1.100 +  shows "orthogonal_matrix A \<longleftrightarrow>
   1.101 +          (\<forall>i. norm(row i A) = 1) \<and>
   1.102 +          (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (row i A) (row j A))"
   1.103 +  using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp
   1.104 +
   1.105 +lemma%important  orthogonal_matrix_exists_basis:
   1.106 +  fixes a :: "real^'n"
   1.107 +  assumes "norm a = 1"
   1.108 +  obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a"
   1.109 +proof%unimportant -
   1.110 +  obtain S where "a \<in> S" "pairwise orthogonal S" and noS: "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
   1.111 +   and "independent S" "card S = CARD('n)" "span S = UNIV"
   1.112 +    using vector_in_orthonormal_basis assms by force
   1.113 +  then obtain f0 where "bij_betw f0 (UNIV::'n set) S"
   1.114 +    by (metis finite_class.finite_UNIV finite_same_card_bij finiteI_independent)
   1.115 +  then obtain f where f: "bij_betw f (UNIV::'n set) S" and a: "a = f k"
   1.116 +    using bij_swap_iff [of k "inv f0 a" f0]
   1.117 +    by (metis UNIV_I \<open>a \<in> S\<close> bij_betw_inv_into_right bij_betw_swap_iff swap_apply(1))
   1.118 +  show thesis
   1.119 +  proof
   1.120 +    have [simp]: "\<And>i. norm (f i) = 1"
   1.121 +      using bij_betwE [OF \<open>bij_betw f UNIV S\<close>] by (blast intro: noS)
   1.122 +    have [simp]: "\<And>i j. i \<noteq> j \<Longrightarrow> orthogonal (f i) (f j)"
   1.123 +      using \<open>pairwise orthogonal S\<close> \<open>bij_betw f UNIV S\<close>
   1.124 +      by (auto simp: pairwise_def bij_betw_def inj_on_def)
   1.125 +    show "orthogonal_matrix (\<chi> i j. f j $ i)"
   1.126 +      by (simp add: orthogonal_matrix_orthonormal_columns column_def)
   1.127 +    show "(\<chi> i j. f j $ i) *v axis k 1 = a"
   1.128 +      by (simp add: matrix_vector_mult_def axis_def a if_distrib cong: if_cong)
   1.129 +  qed
   1.130 +qed
   1.131 +
   1.132 +lemma%unimportant  orthogonal_transformation_exists_1:
   1.133 +  fixes a b :: "real^'n"
   1.134 +  assumes "norm a = 1" "norm b = 1"
   1.135 +  obtains f where "orthogonal_transformation f" "f a = b"
   1.136 +proof%unimportant -
   1.137 +  obtain k::'n where True
   1.138 +    by simp
   1.139 +  obtain A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
   1.140 +    using orthogonal_matrix_exists_basis assms by metis
   1.141 +  let ?f = "\<lambda>x. (B ** transpose A) *v x"
   1.142 +  show thesis
   1.143 +  proof
   1.144 +    show "orthogonal_transformation ?f"
   1.145 +      by (subst orthogonal_transformation_matrix)
   1.146 +        (auto simp: AB orthogonal_matrix_mul)
   1.147 +  next
   1.148 +    show "?f a = b"
   1.149 +      using \<open>orthogonal_matrix A\<close> unfolding orthogonal_matrix_def
   1.150 +      by (metis eq matrix_mul_rid matrix_vector_mul_assoc)
   1.151 +  qed
   1.152 +qed
   1.153 +
   1.154 +lemma%important  orthogonal_transformation_exists:
   1.155 +  fixes a b :: "real^'n"
   1.156 +  assumes "norm a = norm b"
   1.157 +  obtains f where "orthogonal_transformation f" "f a = b"
   1.158 +proof%unimportant (cases "a = 0 \<or> b = 0")
   1.159 +  case True
   1.160 +  with assms show ?thesis
   1.161 +    using that by force
   1.162 +next
   1.163 +  case False
   1.164 +  then obtain f where f: "orthogonal_transformation f" and eq: "f (a /\<^sub>R norm a) = (b /\<^sub>R norm b)"
   1.165 +    by (auto intro: orthogonal_transformation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b"])
   1.166 +  show ?thesis
   1.167 +  proof
   1.168 +    interpret linear f
   1.169 +      using f by (simp add: orthogonal_transformation_linear)
   1.170 +    have "f a /\<^sub>R norm a = f (a /\<^sub>R norm a)"
   1.171 +      by (simp add: scale)
   1.172 +    also have "\<dots> = b /\<^sub>R norm a"
   1.173 +      by (simp add: eq assms [symmetric])
   1.174 +    finally show "f a = b"
   1.175 +      using False by auto
   1.176 +  qed (use f in auto)
   1.177 +qed
   1.178 +
   1.179 +
   1.180 +subsection%important  \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
   1.181 +
   1.182 +lemma%important  scaling_linear:
   1.183 +  fixes f :: "'a::real_inner \<Rightarrow> 'a::real_inner"
   1.184 +  assumes f0: "f 0 = 0"
   1.185 +    and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y"
   1.186 +  shows "linear f"
   1.187 +proof%unimportant -
   1.188 +  {
   1.189 +    fix v w
   1.190 +    have "norm (f x) = c * norm x" for x
   1.191 +      by (metis dist_0_norm f0 fd)
   1.192 +    then have "f v \<bullet> f w = c\<^sup>2 * (v \<bullet> w)"
   1.193 +      unfolding dot_norm_neg dist_norm[symmetric]
   1.194 +      by (simp add: fd power2_eq_square field_simps)
   1.195 +  }
   1.196 +  then show ?thesis
   1.197 +    unfolding linear_iff vector_eq[where 'a="'a"] scalar_mult_eq_scaleR
   1.198 +    by (simp add: inner_add field_simps)
   1.199 +qed
   1.200 +
   1.201 +lemma%unimportant  isometry_linear:
   1.202 +  "f (0::'a::real_inner) = (0::'a) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y \<Longrightarrow> linear f"
   1.203 +  by (rule scaling_linear[where c=1]) simp_all
   1.204 +
   1.205 +text \<open>Hence another formulation of orthogonal transformation\<close>
   1.206 +
   1.207 +lemma%important  orthogonal_transformation_isometry:
   1.208 +  "orthogonal_transformation f \<longleftrightarrow> f(0::'a::real_inner) = (0::'a) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
   1.209 +  unfolding orthogonal_transformation
   1.210 +  apply (auto simp: linear_0 isometry_linear)
   1.211 +   apply (metis (no_types, hide_lams) dist_norm linear_diff)
   1.212 +  by (metis dist_0_norm)
   1.213 +
   1.214 +
   1.215 +subsection%important  \<open>Can extend an isometry from unit sphere\<close>
   1.216 +
   1.217 +lemma%important  isometry_sphere_extend:
   1.218 +  fixes f:: "'a::real_inner \<Rightarrow> 'a"
   1.219 +  assumes f1: "\<And>x. norm x = 1 \<Longrightarrow> norm (f x) = 1"
   1.220 +    and fd1: "\<And>x y. \<lbrakk>norm x = 1; norm y = 1\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y"
   1.221 +  shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)"
   1.222 +proof%unimportant -
   1.223 +  {
   1.224 +    fix x y x' y' u v u' v' :: "'a"
   1.225 +    assume H: "x = norm x *\<^sub>R u" "y = norm y *\<^sub>R v"
   1.226 +              "x' = norm x *\<^sub>R u'" "y' = norm y *\<^sub>R v'"
   1.227 +      and J: "norm u = 1" "norm u' = 1" "norm v = 1" "norm v' = 1" "norm(u' - v') = norm(u - v)"
   1.228 +    then have *: "u \<bullet> v = u' \<bullet> v' + v' \<bullet> u' - v \<bullet> u "
   1.229 +      by (simp add: norm_eq norm_eq_1 inner_add inner_diff)
   1.230 +    have "norm (norm x *\<^sub>R u' - norm y *\<^sub>R v') = norm (norm x *\<^sub>R u - norm y *\<^sub>R v)"
   1.231 +      using J by (simp add: norm_eq norm_eq_1 inner_diff * field_simps)
   1.232 +    then have "norm(x' - y') = norm(x - y)"
   1.233 +      using H by metis
   1.234 +  }
   1.235 +  note norm_eq = this
   1.236 +  let ?g = "\<lambda>x. if x = 0 then 0 else norm x *\<^sub>R f (x /\<^sub>R norm x)"
   1.237 +  have thfg: "?g x = f x" if "norm x = 1" for x
   1.238 +    using that by auto
   1.239 +  have thd: "dist (?g x) (?g y) = dist x y" for x y
   1.240 +  proof (cases "x=0 \<or> y=0")
   1.241 +    case False
   1.242 +    show "dist (?g x) (?g y) = dist x y"
   1.243 +      unfolding dist_norm
   1.244 +    proof (rule norm_eq)
   1.245 +      show "x = norm x *\<^sub>R (x /\<^sub>R norm x)" "y = norm y *\<^sub>R (y /\<^sub>R norm y)"
   1.246 +           "norm (f (x /\<^sub>R norm x)) = 1" "norm (f (y /\<^sub>R norm y)) = 1"
   1.247 +        using False f1 by auto
   1.248 +    qed (use False in \<open>auto simp: field_simps intro: f1 fd1[unfolded dist_norm]\<close>)
   1.249 +  qed (auto simp: f1)
   1.250 +  show ?thesis
   1.251 +    unfolding orthogonal_transformation_isometry
   1.252 +    by (rule exI[where x= ?g]) (metis thfg thd)
   1.253 +qed
   1.254 +
   1.255 +subsection%important\<open>Induction on matrix row operations\<close>
   1.256 +
   1.257 +lemma%unimportant induct_matrix_row_operations:
   1.258 +  fixes P :: "real^'n^'n \<Rightarrow> bool"
   1.259 +  assumes zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
   1.260 +    and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
   1.261 +    and swap_cols: "\<And>A m n. \<lbrakk>P A; m \<noteq> n\<rbrakk> \<Longrightarrow> P(\<chi> i j. A $ i $ Fun.swap m n id j)"
   1.262 +    and row_op: "\<And>A m n c. \<lbrakk>P A; m \<noteq> n\<rbrakk>
   1.263 +                   \<Longrightarrow> P(\<chi> i. if i = m then row m A + c *\<^sub>R row n A else row i A)"
   1.264 +  shows "P A"
   1.265 +proof -
   1.266 +  have "P A" if "(\<And>i j. \<lbrakk>j \<in> -K;  i \<noteq> j\<rbrakk> \<Longrightarrow> A$i$j = 0)" for A K
   1.267 +  proof -
   1.268 +    have "finite K"
   1.269 +      by simp
   1.270 +    then show ?thesis using that
   1.271 +    proof (induction arbitrary: A rule: finite_induct)
   1.272 +      case empty
   1.273 +      with diagonal show ?case
   1.274 +        by simp
   1.275 +    next
   1.276 +      case (insert k K)
   1.277 +      note insertK = insert
   1.278 +      have "P A" if kk: "A$k$k \<noteq> 0"
   1.279 +        and 0: "\<And>i j. \<lbrakk>j \<in> - insert k K; i \<noteq> j\<rbrakk> \<Longrightarrow> A$i$j = 0"
   1.280 +               "\<And>i. \<lbrakk>i \<in> -L; i \<noteq> k\<rbrakk> \<Longrightarrow> A$i$k = 0" for A L
   1.281 +      proof -
   1.282 +        have "finite L"
   1.283 +          by simp
   1.284 +        then show ?thesis using 0 kk
   1.285 +        proof (induction arbitrary: A rule: finite_induct)
   1.286 +          case (empty B)
   1.287 +          show ?case
   1.288 +          proof (rule insertK)
   1.289 +            fix i j
   1.290 +            assume "i \<in> - K" "j \<noteq> i"
   1.291 +            show "B $ j $ i = 0"
   1.292 +              using \<open>j \<noteq> i\<close> \<open>i \<in> - K\<close> empty
   1.293 +              by (metis ComplD ComplI Compl_eq_Diff_UNIV Diff_empty UNIV_I insert_iff)
   1.294 +          qed
   1.295 +        next
   1.296 +          case (insert l L B)
   1.297 +          show ?case
   1.298 +          proof (cases "k = l")
   1.299 +            case True
   1.300 +            with insert show ?thesis
   1.301 +              by auto
   1.302 +          next
   1.303 +            case False
   1.304 +            let ?C = "\<chi> i. if i = l then row l B - (B $ l $ k / B $ k $ k) *\<^sub>R row k B else row i B"
   1.305 +            have 1: "\<lbrakk>j \<in> - insert k K; i \<noteq> j\<rbrakk> \<Longrightarrow> ?C $ i $ j = 0" for j i
   1.306 +              by (auto simp: insert.prems(1) row_def)
   1.307 +            have 2: "?C $ i $ k = 0"
   1.308 +              if "i \<in> - L" "i \<noteq> k" for i
   1.309 +            proof (cases "i=l")
   1.310 +              case True
   1.311 +              with that insert.prems show ?thesis
   1.312 +                by (simp add: row_def)
   1.313 +            next
   1.314 +              case False
   1.315 +              with that show ?thesis
   1.316 +                by (simp add: insert.prems(2) row_def)
   1.317 +            qed
   1.318 +            have 3: "?C $ k $ k \<noteq> 0"
   1.319 +              by (auto simp: insert.prems row_def \<open>k \<noteq> l\<close>)
   1.320 +            have PC: "P ?C"
   1.321 +              using insert.IH [OF 1 2 3] by auto
   1.322 +            have eqB: "(\<chi> i. if i = l then row l ?C + (B $ l $ k / B $ k $ k) *\<^sub>R row k ?C else row i ?C) = B"
   1.323 +              using \<open>k \<noteq> l\<close> by (simp add: vec_eq_iff row_def)
   1.324 +            show ?thesis
   1.325 +              using row_op [OF PC, of l k, where c = "B$l$k / B$k$k"] eqB \<open>k \<noteq> l\<close>
   1.326 +              by (simp add: cong: if_cong)
   1.327 +          qed
   1.328 +        qed
   1.329 +      qed
   1.330 +      then have nonzero_hyp: "P A"
   1.331 +        if kk: "A$k$k \<noteq> 0" and zeroes: "\<And>i j. j \<in> - insert k K \<and> i\<noteq>j \<Longrightarrow> A$i$j = 0" for A
   1.332 +        by (auto simp: intro!: kk zeroes)
   1.333 +      show ?case
   1.334 +      proof (cases "row k A = 0")
   1.335 +        case True
   1.336 +        with zero_row show ?thesis by auto
   1.337 +      next
   1.338 +        case False
   1.339 +        then obtain l where l: "A$k$l \<noteq> 0"
   1.340 +          by (auto simp: row_def zero_vec_def vec_eq_iff)
   1.341 +        show ?thesis
   1.342 +        proof (cases "k = l")
   1.343 +          case True
   1.344 +          with l nonzero_hyp insert.prems show ?thesis
   1.345 +            by blast
   1.346 +        next
   1.347 +          case False
   1.348 +          have *: "A $ i $ Fun.swap k l id j = 0" if "j \<noteq> k" "j \<notin> K" "i \<noteq> j" for i j
   1.349 +            using False l insert.prems that
   1.350 +            by (auto simp: swap_def insert split: if_split_asm)
   1.351 +          have "P (\<chi> i j. (\<chi> i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j)"
   1.352 +            by (rule swap_cols [OF nonzero_hyp False]) (auto simp: l *)
   1.353 +          moreover
   1.354 +          have "(\<chi> i j. (\<chi> i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j) = A"
   1.355 +            by (vector Fun.swap_def)
   1.356 +          ultimately show ?thesis
   1.357 +            by simp
   1.358 +        qed
   1.359 +      qed
   1.360 +    qed
   1.361 +  qed
   1.362 +  then show ?thesis
   1.363 +    by blast
   1.364 +qed
   1.365 +
   1.366 +lemma%unimportant induct_matrix_elementary:
   1.367 +  fixes P :: "real^'n^'n \<Rightarrow> bool"
   1.368 +  assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
   1.369 +    and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
   1.370 +    and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
   1.371 +    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)"
   1.372 +    and idplus: "\<And>m n c. m \<noteq> n \<Longrightarrow> P(\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j))"
   1.373 +  shows "P A"
   1.374 +proof -
   1.375 +  have swap: "P (\<chi> i j. A $ i $ Fun.swap m n id j)"  (is "P ?C")
   1.376 +    if "P A" "m \<noteq> n" for A m n
   1.377 +  proof -
   1.378 +    have "A ** (\<chi> i j. mat 1 $ i $ Fun.swap m n id j) = ?C"
   1.379 +      by (simp add: matrix_matrix_mult_def mat_def vec_eq_iff if_distrib sum.delta_remove)
   1.380 +    then show ?thesis
   1.381 +      using mult swap1 that by metis
   1.382 +  qed
   1.383 +  have row: "P (\<chi> i. if i = m then row m A + c *\<^sub>R row n A else row i A)"  (is "P ?C")
   1.384 +    if "P A" "m \<noteq> n" for A m n c
   1.385 +  proof -
   1.386 +    let ?B = "\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j)"
   1.387 +    have "?B ** A = ?C"
   1.388 +      using \<open>m \<noteq> n\<close> unfolding matrix_matrix_mult_def row_def of_bool_def
   1.389 +      by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
   1.390 +    then show ?thesis
   1.391 +      by (rule subst) (auto simp: that mult idplus)
   1.392 +  qed
   1.393 +  show ?thesis
   1.394 +    by (rule induct_matrix_row_operations [OF zero_row diagonal swap row])
   1.395 +qed
   1.396 +
   1.397 +lemma%unimportant induct_matrix_elementary_alt:
   1.398 +  fixes P :: "real^'n^'n \<Rightarrow> bool"
   1.399 +  assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
   1.400 +    and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
   1.401 +    and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
   1.402 +    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)"
   1.403 +    and idplus: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j))"
   1.404 +  shows "P A"
   1.405 +proof -
   1.406 +  have *: "P (\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j))"
   1.407 +    if "m \<noteq> n" for m n c
   1.408 +  proof (cases "c = 0")
   1.409 +    case True
   1.410 +    with diagonal show ?thesis by auto
   1.411 +  next
   1.412 +    case False
   1.413 +    then have eq: "(\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j)) =
   1.414 +                      (\<chi> i j. if i = j then (if j = n then inverse c else 1) else 0) **
   1.415 +                      (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)) **
   1.416 +                      (\<chi> i j. if i = j then if j = n then c else 1 else 0)"
   1.417 +      using \<open>m \<noteq> n\<close>
   1.418 +      apply (simp add: matrix_matrix_mult_def vec_eq_iff of_bool_def if_distrib [of "\<lambda>x. y * x" for y] cong: if_cong)
   1.419 +      apply (simp add: if_if_eq_conj sum.neutral conj_commute cong: conj_cong)
   1.420 +      done
   1.421 +    show ?thesis
   1.422 +      apply (subst eq)
   1.423 +      apply (intro mult idplus that)
   1.424 +       apply (auto intro: diagonal)
   1.425 +      done
   1.426 +  qed
   1.427 +  show ?thesis
   1.428 +    by (rule induct_matrix_elementary) (auto intro: assms *)
   1.429 +qed
   1.430 +
   1.431 +lemma%unimportant matrix_vector_mult_matrix_matrix_mult_compose:
   1.432 +  "(*v) (A ** B) = (*v) A \<circ> (*v) B"
   1.433 +  by (auto simp: matrix_vector_mul_assoc)
   1.434 +
   1.435 +lemma%unimportant induct_linear_elementary:
   1.436 +  fixes f :: "real^'n \<Rightarrow> real^'n"
   1.437 +  assumes "linear f"
   1.438 +    and comp: "\<And>f g. \<lbrakk>linear f; linear g; P f; P g\<rbrakk> \<Longrightarrow> P(f \<circ> g)"
   1.439 +    and zeroes: "\<And>f i. \<lbrakk>linear f; \<And>x. (f x) $ i = 0\<rbrakk> \<Longrightarrow> P f"
   1.440 +    and const: "\<And>c. P(\<lambda>x. \<chi> i. c i * x$i)"
   1.441 +    and swap: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. x $ Fun.swap m n id i)"
   1.442 +    and idplus: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. if i = m then x$m + x$n else x$i)"
   1.443 +  shows "P f"
   1.444 +proof -
   1.445 +  have "P ((*v) A)" for A
   1.446 +  proof (rule induct_matrix_elementary_alt)
   1.447 +    fix A B
   1.448 +    assume "P ((*v) A)" and "P ((*v) B)"
   1.449 +    then show "P ((*v) (A ** B))"
   1.450 +      by (auto simp add: matrix_vector_mult_matrix_matrix_mult_compose matrix_vector_mul_linear
   1.451 +          intro!: comp)
   1.452 +  next
   1.453 +    fix A :: "real^'n^'n" and i
   1.454 +    assume "row i A = 0"
   1.455 +    show "P ((*v) A)"
   1.456 +      using matrix_vector_mul_linear
   1.457 +      by (rule zeroes[where i=i])
   1.458 +        (metis \<open>row i A = 0\<close> inner_zero_left matrix_vector_mul_component row_def vec_lambda_eta)
   1.459 +  next
   1.460 +    fix A :: "real^'n^'n"
   1.461 +    assume 0: "\<And>i j. i \<noteq> j \<Longrightarrow> A $ i $ j = 0"
   1.462 +    have "A $ i $ i * x $ i = (\<Sum>j\<in>UNIV. A $ i $ j * x $ j)" for x and i :: "'n"
   1.463 +      by (simp add: 0 comm_monoid_add_class.sum.remove [where x=i])
   1.464 +    then have "(\<lambda>x. \<chi> i. A $ i $ i * x $ i) = ((*v) A)"
   1.465 +      by (auto simp: 0 matrix_vector_mult_def)
   1.466 +    then show "P ((*v) A)"
   1.467 +      using const [of "\<lambda>i. A $ i $ i"] by simp
   1.468 +  next
   1.469 +    fix m n :: "'n"
   1.470 +    assume "m \<noteq> n"
   1.471 +    have eq: "(\<Sum>j\<in>UNIV. if i = Fun.swap m n id j then x $ j else 0) =
   1.472 +              (\<Sum>j\<in>UNIV. if j = Fun.swap m n id i then x $ j else 0)"
   1.473 +      for i and x :: "real^'n"
   1.474 +      unfolding swap_def by (rule sum.cong) auto
   1.475 +    have "(\<lambda>x::real^'n. \<chi> i. x $ Fun.swap m n id i) = ((*v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))"
   1.476 +      by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
   1.477 +    with swap [OF \<open>m \<noteq> n\<close>] show "P ((*v) (\<chi> i j. mat 1 $ i $ Fun.swap m n id j))"
   1.478 +      by (simp add: mat_def matrix_vector_mult_def)
   1.479 +  next
   1.480 +    fix m n :: "'n"
   1.481 +    assume "m \<noteq> n"
   1.482 +    then have "x $ m + x $ n = (\<Sum>j\<in>UNIV. of_bool (j = n \<or> m = j) * x $ j)" for x :: "real^'n"
   1.483 +      by (auto simp: of_bool_def if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
   1.484 +    then have "(\<lambda>x::real^'n. \<chi> i. if i = m then x $ m + x $ n else x $ i) =
   1.485 +               ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
   1.486 +      unfolding matrix_vector_mult_def of_bool_def
   1.487 +      by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
   1.488 +    then show "P ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
   1.489 +      using idplus [OF \<open>m \<noteq> n\<close>] by simp
   1.490 +  qed
   1.491 +  then show ?thesis
   1.492 +    by (metis \<open>linear f\<close> matrix_vector_mul)
   1.493 +qed
   1.494 +
   1.495  end
   1.496 \ No newline at end of file
     2.1 --- a/src/HOL/Analysis/Change_Of_Vars.thy	Wed Jan 16 16:50:35 2019 -0500
     2.2 +++ b/src/HOL/Analysis/Change_Of_Vars.thy	Wed Jan 16 18:14:02 2019 -0500
     2.3 @@ -9,246 +9,42 @@
     2.4  
     2.5  begin
     2.6  
     2.7 -subsection%important\<open>Induction on matrix row operations\<close>
     2.8 +subsection%unimportant \<open>Orthogonal Transformation of Balls\<close>
     2.9  
    2.10 -lemma%unimportant induct_matrix_row_operations:
    2.11 -  fixes P :: "real^'n^'n \<Rightarrow> bool"
    2.12 -  assumes zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
    2.13 -    and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
    2.14 -    and swap_cols: "\<And>A m n. \<lbrakk>P A; m \<noteq> n\<rbrakk> \<Longrightarrow> P(\<chi> i j. A $ i $ Fun.swap m n id j)"
    2.15 -    and row_op: "\<And>A m n c. \<lbrakk>P A; m \<noteq> n\<rbrakk>
    2.16 -                   \<Longrightarrow> P(\<chi> i. if i = m then row m A + c *\<^sub>R row n A else row i A)"
    2.17 -  shows "P A"
    2.18 -proof -
    2.19 -  have "P A" if "(\<And>i j. \<lbrakk>j \<in> -K;  i \<noteq> j\<rbrakk> \<Longrightarrow> A$i$j = 0)" for A K
    2.20 -  proof -
    2.21 -    have "finite K"
    2.22 -      by simp
    2.23 -    then show ?thesis using that
    2.24 -    proof (induction arbitrary: A rule: finite_induct)
    2.25 -      case empty
    2.26 -      with diagonal show ?case
    2.27 -        by simp
    2.28 -    next
    2.29 -      case (insert k K)
    2.30 -      note insertK = insert
    2.31 -      have "P A" if kk: "A$k$k \<noteq> 0"
    2.32 -        and 0: "\<And>i j. \<lbrakk>j \<in> - insert k K; i \<noteq> j\<rbrakk> \<Longrightarrow> A$i$j = 0"
    2.33 -               "\<And>i. \<lbrakk>i \<in> -L; i \<noteq> k\<rbrakk> \<Longrightarrow> A$i$k = 0" for A L
    2.34 -      proof -
    2.35 -        have "finite L"
    2.36 -          by simp
    2.37 -        then show ?thesis using 0 kk
    2.38 -        proof (induction arbitrary: A rule: finite_induct)
    2.39 -          case (empty B)
    2.40 -          show ?case
    2.41 -          proof (rule insertK)
    2.42 -            fix i j
    2.43 -            assume "i \<in> - K" "j \<noteq> i"
    2.44 -            show "B $ j $ i = 0"
    2.45 -              using \<open>j \<noteq> i\<close> \<open>i \<in> - K\<close> empty
    2.46 -              by (metis ComplD ComplI Compl_eq_Diff_UNIV Diff_empty UNIV_I insert_iff)
    2.47 -          qed
    2.48 -        next
    2.49 -          case (insert l L B)
    2.50 -          show ?case
    2.51 -          proof (cases "k = l")
    2.52 -            case True
    2.53 -            with insert show ?thesis
    2.54 -              by auto
    2.55 -          next
    2.56 -            case False
    2.57 -            let ?C = "\<chi> i. if i = l then row l B - (B $ l $ k / B $ k $ k) *\<^sub>R row k B else row i B"
    2.58 -            have 1: "\<lbrakk>j \<in> - insert k K; i \<noteq> j\<rbrakk> \<Longrightarrow> ?C $ i $ j = 0" for j i
    2.59 -              by (auto simp: insert.prems(1) row_def)
    2.60 -            have 2: "?C $ i $ k = 0"
    2.61 -              if "i \<in> - L" "i \<noteq> k" for i
    2.62 -            proof (cases "i=l")
    2.63 -              case True
    2.64 -              with that insert.prems show ?thesis
    2.65 -                by (simp add: row_def)
    2.66 -            next
    2.67 -              case False
    2.68 -              with that show ?thesis
    2.69 -                by (simp add: insert.prems(2) row_def)
    2.70 -            qed
    2.71 -            have 3: "?C $ k $ k \<noteq> 0"
    2.72 -              by (auto simp: insert.prems row_def \<open>k \<noteq> l\<close>)
    2.73 -            have PC: "P ?C"
    2.74 -              using insert.IH [OF 1 2 3] by auto
    2.75 -            have eqB: "(\<chi> i. if i = l then row l ?C + (B $ l $ k / B $ k $ k) *\<^sub>R row k ?C else row i ?C) = B"
    2.76 -              using \<open>k \<noteq> l\<close> by (simp add: vec_eq_iff row_def)
    2.77 -            show ?thesis
    2.78 -              using row_op [OF PC, of l k, where c = "B$l$k / B$k$k"] eqB \<open>k \<noteq> l\<close>
    2.79 -              by (simp add: cong: if_cong)
    2.80 -          qed
    2.81 -        qed
    2.82 -      qed
    2.83 -      then have nonzero_hyp: "P A"
    2.84 -        if kk: "A$k$k \<noteq> 0" and zeroes: "\<And>i j. j \<in> - insert k K \<and> i\<noteq>j \<Longrightarrow> A$i$j = 0" for A
    2.85 -        by (auto simp: intro!: kk zeroes)
    2.86 -      show ?case
    2.87 -      proof (cases "row k A = 0")
    2.88 -        case True
    2.89 -        with zero_row show ?thesis by auto
    2.90 -      next
    2.91 -        case False
    2.92 -        then obtain l where l: "A$k$l \<noteq> 0"
    2.93 -          by (auto simp: row_def zero_vec_def vec_eq_iff)
    2.94 -        show ?thesis
    2.95 -        proof (cases "k = l")
    2.96 -          case True
    2.97 -          with l nonzero_hyp insert.prems show ?thesis
    2.98 -            by blast
    2.99 -        next
   2.100 -          case False
   2.101 -          have *: "A $ i $ Fun.swap k l id j = 0" if "j \<noteq> k" "j \<notin> K" "i \<noteq> j" for i j
   2.102 -            using False l insert.prems that
   2.103 -            by (auto simp: swap_def insert split: if_split_asm)
   2.104 -          have "P (\<chi> i j. (\<chi> i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j)"
   2.105 -            by (rule swap_cols [OF nonzero_hyp False]) (auto simp: l *)
   2.106 -          moreover
   2.107 -          have "(\<chi> i j. (\<chi> i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j) = A"
   2.108 -            by (metis (no_types, lifting) id_apply o_apply swap_id_idempotent vec_lambda_unique vec_lambda_unique)
   2.109 -          ultimately show ?thesis
   2.110 -            by simp
   2.111 -        qed
   2.112 -      qed
   2.113 -    qed
   2.114 -  qed
   2.115 -  then show ?thesis
   2.116 -    by blast
   2.117 +lemma%unimportant image_orthogonal_transformation_ball:
   2.118 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
   2.119 +  assumes "orthogonal_transformation f"
   2.120 +  shows "f ` ball x r = ball (f x) r"
   2.121 +proof (intro equalityI subsetI)
   2.122 +  fix y assume "y \<in> f ` ball x r"
   2.123 +  with assms show "y \<in> ball (f x) r"
   2.124 +    by (auto simp: orthogonal_transformation_isometry)
   2.125 +next
   2.126 +  fix y assume y: "y \<in> ball (f x) r"
   2.127 +  then obtain z where z: "y = f z"
   2.128 +    using assms orthogonal_transformation_surj by blast
   2.129 +  with y assms show "y \<in> f ` ball x r"
   2.130 +    by (auto simp: orthogonal_transformation_isometry)
   2.131  qed
   2.132  
   2.133 -lemma%unimportant induct_matrix_elementary:
   2.134 -  fixes P :: "real^'n^'n \<Rightarrow> bool"
   2.135 -  assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
   2.136 -    and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
   2.137 -    and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
   2.138 -    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)"
   2.139 -    and idplus: "\<And>m n c. m \<noteq> n \<Longrightarrow> P(\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j))"
   2.140 -  shows "P A"
   2.141 -proof -
   2.142 -  have swap: "P (\<chi> i j. A $ i $ Fun.swap m n id j)"  (is "P ?C")
   2.143 -    if "P A" "m \<noteq> n" for A m n
   2.144 -  proof -
   2.145 -    have "A ** (\<chi> i j. mat 1 $ i $ Fun.swap m n id j) = ?C"
   2.146 -      by (simp add: matrix_matrix_mult_def mat_def vec_eq_iff if_distrib sum.delta_remove)
   2.147 -    then show ?thesis
   2.148 -      using mult swap1 that by metis
   2.149 -  qed
   2.150 -  have row: "P (\<chi> i. if i = m then row m A + c *\<^sub>R row n A else row i A)"  (is "P ?C")
   2.151 -    if "P A" "m \<noteq> n" for A m n c
   2.152 -  proof -
   2.153 -    let ?B = "\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j)"
   2.154 -    have "?B ** A = ?C"
   2.155 -      using \<open>m \<noteq> n\<close> unfolding matrix_matrix_mult_def row_def of_bool_def
   2.156 -      by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
   2.157 -    then show ?thesis
   2.158 -      by (rule subst) (auto simp: that mult idplus)
   2.159 -  qed
   2.160 -  show ?thesis
   2.161 -    by (rule induct_matrix_row_operations [OF zero_row diagonal swap row])
   2.162 -qed
   2.163 -
   2.164 -lemma%unimportant induct_matrix_elementary_alt:
   2.165 -  fixes P :: "real^'n^'n \<Rightarrow> bool"
   2.166 -  assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
   2.167 -    and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
   2.168 -    and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
   2.169 -    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)"
   2.170 -    and idplus: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j))"
   2.171 -  shows "P A"
   2.172 -proof -
   2.173 -  have *: "P (\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j))"
   2.174 -    if "m \<noteq> n" for m n c
   2.175 -  proof (cases "c = 0")
   2.176 -    case True
   2.177 -    with diagonal show ?thesis by auto
   2.178 -  next
   2.179 -    case False
   2.180 -    then have eq: "(\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j)) =
   2.181 -                      (\<chi> i j. if i = j then (if j = n then inverse c else 1) else 0) **
   2.182 -                      (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)) **
   2.183 -                      (\<chi> i j. if i = j then if j = n then c else 1 else 0)"
   2.184 -      using \<open>m \<noteq> n\<close>
   2.185 -      apply (simp add: matrix_matrix_mult_def vec_eq_iff of_bool_def if_distrib [of "\<lambda>x. y * x" for y] cong: if_cong)
   2.186 -      apply (simp add: if_if_eq_conj sum.neutral conj_commute cong: conj_cong)
   2.187 -      done
   2.188 -    show ?thesis
   2.189 -      apply (subst eq)
   2.190 -      apply (intro mult idplus that)
   2.191 -       apply (auto intro: diagonal)
   2.192 -      done
   2.193 -  qed
   2.194 -  show ?thesis
   2.195 -    by (rule induct_matrix_elementary) (auto intro: assms *)
   2.196 +lemma%unimportant  image_orthogonal_transformation_cball:
   2.197 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
   2.198 +  assumes "orthogonal_transformation f"
   2.199 +  shows "f ` cball x r = cball (f x) r"
   2.200 +proof (intro equalityI subsetI)
   2.201 +  fix y assume "y \<in> f ` cball x r"
   2.202 +  with assms show "y \<in> cball (f x) r"
   2.203 +    by (auto simp: orthogonal_transformation_isometry)
   2.204 +next
   2.205 +  fix y assume y: "y \<in> cball (f x) r"
   2.206 +  then obtain z where z: "y = f z"
   2.207 +    using assms orthogonal_transformation_surj by blast
   2.208 +  with y assms show "y \<in> f ` cball x r"
   2.209 +    by (auto simp: orthogonal_transformation_isometry)
   2.210  qed
   2.211  
   2.212 -lemma%unimportant matrix_vector_mult_matrix_matrix_mult_compose:
   2.213 -  "(*v) (A ** B) = (*v) A \<circ> (*v) B"
   2.214 -  by (auto simp: matrix_vector_mul_assoc)
   2.215  
   2.216 -lemma%unimportant induct_linear_elementary:
   2.217 -  fixes f :: "real^'n \<Rightarrow> real^'n"
   2.218 -  assumes "linear f"
   2.219 -    and comp: "\<And>f g. \<lbrakk>linear f; linear g; P f; P g\<rbrakk> \<Longrightarrow> P(f \<circ> g)"
   2.220 -    and zeroes: "\<And>f i. \<lbrakk>linear f; \<And>x. (f x) $ i = 0\<rbrakk> \<Longrightarrow> P f"
   2.221 -    and const: "\<And>c. P(\<lambda>x. \<chi> i. c i * x$i)"
   2.222 -    and swap: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. x $ Fun.swap m n id i)"
   2.223 -    and idplus: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. if i = m then x$m + x$n else x$i)"
   2.224 -  shows "P f"
   2.225 -proof -
   2.226 -  have "P ((*v) A)" for A
   2.227 -  proof (rule induct_matrix_elementary_alt)
   2.228 -    fix A B
   2.229 -    assume "P ((*v) A)" and "P ((*v) B)"
   2.230 -    then show "P ((*v) (A ** B))"
   2.231 -      by (auto simp add: matrix_vector_mult_matrix_matrix_mult_compose matrix_vector_mul_linear
   2.232 -          intro!: comp)
   2.233 -  next
   2.234 -    fix A :: "real^'n^'n" and i
   2.235 -    assume "row i A = 0"
   2.236 -    show "P ((*v) A)"
   2.237 -      using matrix_vector_mul_linear
   2.238 -      by (rule zeroes[where i=i])
   2.239 -        (metis \<open>row i A = 0\<close> inner_zero_left matrix_vector_mul_component row_def vec_lambda_eta)
   2.240 -  next
   2.241 -    fix A :: "real^'n^'n"
   2.242 -    assume 0: "\<And>i j. i \<noteq> j \<Longrightarrow> A $ i $ j = 0"
   2.243 -    have "A $ i $ i * x $ i = (\<Sum>j\<in>UNIV. A $ i $ j * x $ j)" for x and i :: "'n"
   2.244 -      by (simp add: 0 comm_monoid_add_class.sum.remove [where x=i])
   2.245 -    then have "(\<lambda>x. \<chi> i. A $ i $ i * x $ i) = ((*v) A)"
   2.246 -      by (auto simp: 0 matrix_vector_mult_def)
   2.247 -    then show "P ((*v) A)"
   2.248 -      using const [of "\<lambda>i. A $ i $ i"] by simp
   2.249 -  next
   2.250 -    fix m n :: "'n"
   2.251 -    assume "m \<noteq> n"
   2.252 -    have eq: "(\<Sum>j\<in>UNIV. if i = Fun.swap m n id j then x $ j else 0) =
   2.253 -              (\<Sum>j\<in>UNIV. if j = Fun.swap m n id i then x $ j else 0)"
   2.254 -      for i and x :: "real^'n"
   2.255 -      unfolding swap_def by (rule sum.cong) auto
   2.256 -    have "(\<lambda>x::real^'n. \<chi> i. x $ Fun.swap m n id i) = ((*v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))"
   2.257 -      by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
   2.258 -    with swap [OF \<open>m \<noteq> n\<close>] show "P ((*v) (\<chi> i j. mat 1 $ i $ Fun.swap m n id j))"
   2.259 -      by (simp add: mat_def matrix_vector_mult_def)
   2.260 -  next
   2.261 -    fix m n :: "'n"
   2.262 -    assume "m \<noteq> n"
   2.263 -    then have "x $ m + x $ n = (\<Sum>j\<in>UNIV. of_bool (j = n \<or> m = j) * x $ j)" for x :: "real^'n"
   2.264 -      by (auto simp: of_bool_def if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
   2.265 -    then have "(\<lambda>x::real^'n. \<chi> i. if i = m then x $ m + x $ n else x $ i) =
   2.266 -               ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
   2.267 -      unfolding matrix_vector_mult_def of_bool_def
   2.268 -      by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
   2.269 -    then show "P ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
   2.270 -      using idplus [OF \<open>m \<noteq> n\<close>] by simp
   2.271 -  qed
   2.272 -  then show ?thesis
   2.273 -    by (metis \<open>linear f\<close> matrix_vector_mul)
   2.274 -qed
   2.275 -
   2.276 +subsection \<open>Measurable Shear and Stretch\<close>
   2.277  
   2.278  proposition%important
   2.279    fixes a :: "real^'n"
     3.1 --- a/src/HOL/Analysis/Convex.thy	Wed Jan 16 16:50:35 2019 -0500
     3.2 +++ b/src/HOL/Analysis/Convex.thy	Wed Jan 16 18:14:02 2019 -0500
     3.3 @@ -14,79 +14,6 @@
     3.4    "HOL-Library.Set_Algebras"
     3.5  begin
     3.6  
     3.7 -lemma substdbasis_expansion_unique:
     3.8 -  assumes d: "d \<subseteq> Basis"
     3.9 -  shows "(\<Sum>i\<in>d. f i *\<^sub>R i) = (x::'a::euclidean_space) \<longleftrightarrow>
    3.10 -    (\<forall>i\<in>Basis. (i \<in> d \<longrightarrow> f i = x \<bullet> i) \<and> (i \<notin> d \<longrightarrow> x \<bullet> i = 0))"
    3.11 -proof -
    3.12 -  have *: "\<And>x a b P. x * (if P then a else b) = (if P then x * a else x * b)"
    3.13 -    by auto
    3.14 -  have **: "finite d"
    3.15 -    by (auto intro: finite_subset[OF assms])
    3.16 -  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)"
    3.17 -    using d
    3.18 -    by (auto intro!: sum.cong simp: inner_Basis inner_sum_left)
    3.19 -  show ?thesis
    3.20 -    unfolding euclidean_eq_iff[where 'a='a] by (auto simp: sum.delta[OF **] ***)
    3.21 -qed
    3.22 -
    3.23 -lemma independent_substdbasis: "d \<subseteq> Basis \<Longrightarrow> independent d"
    3.24 -  by (rule independent_mono[OF independent_Basis])
    3.25 -
    3.26 -lemma sum_not_0: "sum f A \<noteq> 0 \<Longrightarrow> \<exists>a \<in> A. f a \<noteq> 0"
    3.27 -  by (rule ccontr) auto
    3.28 -
    3.29 -lemma subset_translation_eq [simp]:
    3.30 -    fixes a :: "'a::real_vector" shows "(+) a ` s \<subseteq> (+) a ` t \<longleftrightarrow> s \<subseteq> t"
    3.31 -  by auto
    3.32 -
    3.33 -lemma translate_inj_on:
    3.34 -  fixes A :: "'a::ab_group_add set"
    3.35 -  shows "inj_on (\<lambda>x. a + x) A"
    3.36 -  unfolding inj_on_def by auto
    3.37 -
    3.38 -lemma translation_assoc:
    3.39 -  fixes a b :: "'a::ab_group_add"
    3.40 -  shows "(\<lambda>x. b + x) ` ((\<lambda>x. a + x) ` S) = (\<lambda>x. (a + b) + x) ` S"
    3.41 -  by auto
    3.42 -
    3.43 -lemma translation_invert:
    3.44 -  fixes a :: "'a::ab_group_add"
    3.45 -  assumes "(\<lambda>x. a + x) ` A = (\<lambda>x. a + x) ` B"
    3.46 -  shows "A = B"
    3.47 -proof -
    3.48 -  have "(\<lambda>x. -a + x) ` ((\<lambda>x. a + x) ` A) = (\<lambda>x. - a + x) ` ((\<lambda>x. a + x) ` B)"
    3.49 -    using assms by auto
    3.50 -  then show ?thesis
    3.51 -    using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto
    3.52 -qed
    3.53 -
    3.54 -lemma translation_galois:
    3.55 -  fixes a :: "'a::ab_group_add"
    3.56 -  shows "T = ((\<lambda>x. a + x) ` S) \<longleftrightarrow> S = ((\<lambda>x. (- a) + x) ` T)"
    3.57 -  using translation_assoc[of "-a" a S]
    3.58 -  apply auto
    3.59 -  using translation_assoc[of a "-a" T]
    3.60 -  apply auto
    3.61 -  done
    3.62 -
    3.63 -lemma translation_inverse_subset:
    3.64 -  assumes "((\<lambda>x. - a + x) ` V) \<le> (S :: 'n::ab_group_add set)"
    3.65 -  shows "V \<le> ((\<lambda>x. a + x) ` S)"
    3.66 -proof -
    3.67 -  {
    3.68 -    fix x
    3.69 -    assume "x \<in> V"
    3.70 -    then have "x-a \<in> S" using assms by auto
    3.71 -    then have "x \<in> {a + v |v. v \<in> S}"
    3.72 -      apply auto
    3.73 -      apply (rule exI[of _ "x-a"], simp)
    3.74 -      done
    3.75 -    then have "x \<in> ((\<lambda>x. a+x) ` S)" by auto
    3.76 -  }
    3.77 -  then show ?thesis by auto
    3.78 -qed
    3.79 -
    3.80  subsection \<open>Convexity\<close>
    3.81  
    3.82  definition%important convex :: "'a::real_vector set \<Rightarrow> bool"
     4.1 --- a/src/HOL/Analysis/Cross3.thy	Wed Jan 16 16:50:35 2019 -0500
     4.2 +++ b/src/HOL/Analysis/Cross3.thy	Wed Jan 16 18:14:02 2019 -0500
     4.3 @@ -7,7 +7,7 @@
     4.4  section\<open>Vector Cross Products in 3 Dimensions\<close>
     4.5  
     4.6  theory "Cross3"
     4.7 -  imports Determinants
     4.8 +  imports Determinants Cartesian_Euclidean_Space
     4.9  begin
    4.10  
    4.11  context includes no_Set_Product_syntax 
     5.1 --- a/src/HOL/Analysis/Determinants.thy	Wed Jan 16 16:50:35 2019 -0500
     5.2 +++ b/src/HOL/Analysis/Determinants.thy	Wed Jan 16 18:14:02 2019 -0500
     5.3 @@ -6,7 +6,7 @@
     5.4  
     5.5  theory Determinants
     5.6  imports
     5.7 -  Cartesian_Euclidean_Space
     5.8 +  Cartesian_Space
     5.9    "HOL-Library.Permutations"
    5.10  begin
    5.11  
    5.12 @@ -941,372 +941,6 @@
    5.13      by auto
    5.14  qed
    5.15  
    5.16 -subsection%important  \<open>Orthogonality of a transformation and matrix\<close>
    5.17 -
    5.18 -definition%important  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
    5.19 -
    5.20 -definition%important  "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
    5.21 -  transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
    5.22 -
    5.23 -lemma%unimportant  orthogonal_transformation:
    5.24 -  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v. norm (f v) = norm v)"
    5.25 -  unfolding orthogonal_transformation_def
    5.26 -  apply auto
    5.27 -  apply (erule_tac x=v in allE)+
    5.28 -  apply (simp add: norm_eq_sqrt_inner)
    5.29 -  apply (simp add: dot_norm linear_add[symmetric])
    5.30 -  done
    5.31 -
    5.32 -lemma%unimportant  orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
    5.33 -  by (simp add: linear_iff orthogonal_transformation_def)
    5.34 -
    5.35 -lemma%unimportant  orthogonal_orthogonal_transformation:
    5.36 -    "orthogonal_transformation f \<Longrightarrow> orthogonal (f x) (f y) \<longleftrightarrow> orthogonal x y"
    5.37 -  by (simp add: orthogonal_def orthogonal_transformation_def)
    5.38 -
    5.39 -lemma%unimportant  orthogonal_transformation_compose:
    5.40 -   "\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)"
    5.41 -  by (auto simp: orthogonal_transformation_def linear_compose)
    5.42 -
    5.43 -lemma%unimportant  orthogonal_transformation_neg:
    5.44 -  "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
    5.45 -  by (auto simp: orthogonal_transformation_def dest: linear_compose_neg)
    5.46 -
    5.47 -lemma%unimportant  orthogonal_transformation_scaleR: "orthogonal_transformation f \<Longrightarrow> f (c *\<^sub>R v) = c *\<^sub>R f v"
    5.48 -  by (simp add: linear_iff orthogonal_transformation_def)
    5.49 -
    5.50 -lemma%unimportant  orthogonal_transformation_linear:
    5.51 -   "orthogonal_transformation f \<Longrightarrow> linear f"
    5.52 -  by (simp add: orthogonal_transformation_def)
    5.53 -
    5.54 -lemma%unimportant  orthogonal_transformation_inj:
    5.55 -  "orthogonal_transformation f \<Longrightarrow> inj f"
    5.56 -  unfolding orthogonal_transformation_def inj_on_def
    5.57 -  by (metis vector_eq)
    5.58 -
    5.59 -lemma%unimportant  orthogonal_transformation_surj:
    5.60 -  "orthogonal_transformation f \<Longrightarrow> surj f"
    5.61 -  for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
    5.62 -  by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear)
    5.63 -
    5.64 -lemma%unimportant  orthogonal_transformation_bij:
    5.65 -  "orthogonal_transformation f \<Longrightarrow> bij f"
    5.66 -  for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
    5.67 -  by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj)
    5.68 -
    5.69 -lemma%unimportant  orthogonal_transformation_inv:
    5.70 -  "orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)"
    5.71 -  for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
    5.72 -  by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj)
    5.73 -
    5.74 -lemma%unimportant  orthogonal_transformation_norm:
    5.75 -  "orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x"
    5.76 -  by (metis orthogonal_transformation)
    5.77 -
    5.78 -lemma%unimportant  orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1"
    5.79 -  by (metis matrix_left_right_inverse orthogonal_matrix_def)
    5.80 -
    5.81 -lemma%unimportant  orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)"
    5.82 -  by (simp add: orthogonal_matrix_def)
    5.83 -
    5.84 -lemma%unimportant  orthogonal_matrix_mul:
    5.85 -  fixes A :: "real ^'n^'n"
    5.86 -  assumes  "orthogonal_matrix A" "orthogonal_matrix B"
    5.87 -  shows "orthogonal_matrix(A ** B)"
    5.88 -  using assms
    5.89 -  by (simp add: orthogonal_matrix matrix_transpose_mul matrix_left_right_inverse matrix_mul_assoc)
    5.90 -
    5.91 -lemma%important  orthogonal_transformation_matrix:
    5.92 -  fixes f:: "real^'n \<Rightarrow> real^'n"
    5.93 -  shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)"
    5.94 -  (is "?lhs \<longleftrightarrow> ?rhs")
    5.95 -proof%unimportant -
    5.96 -  let ?mf = "matrix f"
    5.97 -  let ?ot = "orthogonal_transformation f"
    5.98 -  let ?U = "UNIV :: 'n set"
    5.99 -  have fU: "finite ?U" by simp
   5.100 -  let ?m1 = "mat 1 :: real ^'n^'n"
   5.101 -  {
   5.102 -    assume ot: ?ot
   5.103 -    from ot have lf: "Vector_Spaces.linear (*s) (*s) f" and fd: "\<And>v w. f v \<bullet> f w = v \<bullet> w"
   5.104 -      unfolding orthogonal_transformation_def orthogonal_matrix linear_def scalar_mult_eq_scaleR
   5.105 -      by blast+
   5.106 -    {
   5.107 -      fix i j
   5.108 -      let ?A = "transpose ?mf ** ?mf"
   5.109 -      have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)"
   5.110 -        "\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)"
   5.111 -        by simp_all
   5.112 -      from fd[of "axis i 1" "axis j 1",
   5.113 -        simplified matrix_works[OF lf, symmetric] dot_matrix_vector_mul]
   5.114 -      have "?A$i$j = ?m1 $ i $ j"
   5.115 -        by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def
   5.116 -            th0 sum.delta[OF fU] mat_def axis_def)
   5.117 -    }
   5.118 -    then have "orthogonal_matrix ?mf"
   5.119 -      unfolding orthogonal_matrix
   5.120 -      by vector
   5.121 -    with lf have ?rhs
   5.122 -      unfolding linear_def scalar_mult_eq_scaleR
   5.123 -      by blast
   5.124 -  }
   5.125 -  moreover
   5.126 -  {
   5.127 -    assume lf: "Vector_Spaces.linear (*s) (*s) f" and om: "orthogonal_matrix ?mf"
   5.128 -    from lf om have ?lhs
   5.129 -      unfolding orthogonal_matrix_def norm_eq orthogonal_transformation
   5.130 -      apply (simp only: matrix_works[OF lf, symmetric] dot_matrix_vector_mul)
   5.131 -      apply (simp add: dot_matrix_product linear_def scalar_mult_eq_scaleR)
   5.132 -      done
   5.133 -  }
   5.134 -  ultimately show ?thesis
   5.135 -    by (auto simp: linear_def scalar_mult_eq_scaleR)
   5.136 -qed
   5.137 -
   5.138 -lemma%important  det_orthogonal_matrix:
   5.139 -  fixes Q:: "'a::linordered_idom^'n^'n"
   5.140 -  assumes oQ: "orthogonal_matrix Q"
   5.141 -  shows "det Q = 1 \<or> det Q = - 1"
   5.142 -proof%unimportant -
   5.143 -  have "Q ** transpose Q = mat 1"
   5.144 -    by (metis oQ orthogonal_matrix_def)
   5.145 -  then have "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)"
   5.146 -    by simp
   5.147 -  then have "det Q * det Q = 1"
   5.148 -    by (simp add: det_mul)
   5.149 -  then show ?thesis
   5.150 -    by (simp add: square_eq_1_iff)
   5.151 -qed
   5.152 -
   5.153 -lemma%important  orthogonal_transformation_det [simp]:
   5.154 -  fixes f :: "real^'n \<Rightarrow> real^'n"
   5.155 -  shows "orthogonal_transformation f \<Longrightarrow> \<bar>det (matrix f)\<bar> = 1"
   5.156 -  using%unimportant det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
   5.157 -
   5.158 -
   5.159 -subsection%important  \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
   5.160 -
   5.161 -lemma%important  scaling_linear:
   5.162 -  fixes f :: "'a::real_inner \<Rightarrow> 'a::real_inner"
   5.163 -  assumes f0: "f 0 = 0"
   5.164 -    and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y"
   5.165 -  shows "linear f"
   5.166 -proof%unimportant -
   5.167 -  {
   5.168 -    fix v w
   5.169 -    have "norm (f x) = c * norm x" for x
   5.170 -      by (metis dist_0_norm f0 fd)
   5.171 -    then have "f v \<bullet> f w = c\<^sup>2 * (v \<bullet> w)"
   5.172 -      unfolding dot_norm_neg dist_norm[symmetric]
   5.173 -      by (simp add: fd power2_eq_square field_simps)
   5.174 -  }
   5.175 -  then show ?thesis
   5.176 -    unfolding linear_iff vector_eq[where 'a="'a"] scalar_mult_eq_scaleR
   5.177 -    by (simp add: inner_add field_simps)
   5.178 -qed
   5.179 -
   5.180 -lemma%unimportant  isometry_linear:
   5.181 -  "f (0::'a::real_inner) = (0::'a) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y \<Longrightarrow> linear f"
   5.182 -  by (rule scaling_linear[where c=1]) simp_all
   5.183 -
   5.184 -text \<open>Hence another formulation of orthogonal transformation\<close>
   5.185 -
   5.186 -lemma%important  orthogonal_transformation_isometry:
   5.187 -  "orthogonal_transformation f \<longleftrightarrow> f(0::'a::real_inner) = (0::'a) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
   5.188 -  unfolding orthogonal_transformation
   5.189 -  apply (auto simp: linear_0 isometry_linear)
   5.190 -   apply (metis (no_types, hide_lams) dist_norm linear_diff)
   5.191 -  by (metis dist_0_norm)
   5.192 -
   5.193 -
   5.194 -lemma%unimportant  image_orthogonal_transformation_ball:
   5.195 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
   5.196 -  assumes "orthogonal_transformation f"
   5.197 -  shows "f ` ball x r = ball (f x) r"
   5.198 -proof (intro equalityI subsetI)
   5.199 -  fix y assume "y \<in> f ` ball x r"
   5.200 -  with assms show "y \<in> ball (f x) r"
   5.201 -    by (auto simp: orthogonal_transformation_isometry)
   5.202 -next
   5.203 -  fix y assume y: "y \<in> ball (f x) r"
   5.204 -  then obtain z where z: "y = f z"
   5.205 -    using assms orthogonal_transformation_surj by blast
   5.206 -  with y assms show "y \<in> f ` ball x r"
   5.207 -    by (auto simp: orthogonal_transformation_isometry)
   5.208 -qed
   5.209 -
   5.210 -lemma%unimportant  image_orthogonal_transformation_cball:
   5.211 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
   5.212 -  assumes "orthogonal_transformation f"
   5.213 -  shows "f ` cball x r = cball (f x) r"
   5.214 -proof (intro equalityI subsetI)
   5.215 -  fix y assume "y \<in> f ` cball x r"
   5.216 -  with assms show "y \<in> cball (f x) r"
   5.217 -    by (auto simp: orthogonal_transformation_isometry)
   5.218 -next
   5.219 -  fix y assume y: "y \<in> cball (f x) r"
   5.220 -  then obtain z where z: "y = f z"
   5.221 -    using assms orthogonal_transformation_surj by blast
   5.222 -  with y assms show "y \<in> f ` cball x r"
   5.223 -    by (auto simp: orthogonal_transformation_isometry)
   5.224 -qed
   5.225 -
   5.226 -subsection%important \<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
   5.227 -
   5.228 -lemma%unimportant  orthogonal_matrix_transpose [simp]:
   5.229 -     "orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
   5.230 -  by (auto simp: orthogonal_matrix_def)
   5.231 -
   5.232 -lemma%unimportant  orthogonal_matrix_orthonormal_columns:
   5.233 -  fixes A :: "real^'n^'n"
   5.234 -  shows "orthogonal_matrix A \<longleftrightarrow>
   5.235 -          (\<forall>i. norm(column i A) = 1) \<and>
   5.236 -          (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (column i A) (column j A))"
   5.237 -  by (auto simp: orthogonal_matrix matrix_mult_transpose_dot_column vec_eq_iff mat_def norm_eq_1 orthogonal_def)
   5.238 -
   5.239 -lemma%unimportant  orthogonal_matrix_orthonormal_rows:
   5.240 -  fixes A :: "real^'n^'n"
   5.241 -  shows "orthogonal_matrix A \<longleftrightarrow>
   5.242 -          (\<forall>i. norm(row i A) = 1) \<and>
   5.243 -          (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (row i A) (row j A))"
   5.244 -  using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp
   5.245 -
   5.246 -lemma%important  orthogonal_matrix_exists_basis:
   5.247 -  fixes a :: "real^'n"
   5.248 -  assumes "norm a = 1"
   5.249 -  obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a"
   5.250 -proof%unimportant -
   5.251 -  obtain S where "a \<in> S" "pairwise orthogonal S" and noS: "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
   5.252 -   and "independent S" "card S = CARD('n)" "span S = UNIV"
   5.253 -    using vector_in_orthonormal_basis assms by force
   5.254 -  then obtain f0 where "bij_betw f0 (UNIV::'n set) S"
   5.255 -    by (metis finite_class.finite_UNIV finite_same_card_bij finiteI_independent)
   5.256 -  then obtain f where f: "bij_betw f (UNIV::'n set) S" and a: "a = f k"
   5.257 -    using bij_swap_iff [of k "inv f0 a" f0]
   5.258 -    by (metis UNIV_I \<open>a \<in> S\<close> bij_betw_inv_into_right bij_betw_swap_iff swap_apply1)
   5.259 -  show thesis
   5.260 -  proof
   5.261 -    have [simp]: "\<And>i. norm (f i) = 1"
   5.262 -      using bij_betwE [OF \<open>bij_betw f UNIV S\<close>] by (blast intro: noS)
   5.263 -    have [simp]: "\<And>i j. i \<noteq> j \<Longrightarrow> orthogonal (f i) (f j)"
   5.264 -      using \<open>pairwise orthogonal S\<close> \<open>bij_betw f UNIV S\<close>
   5.265 -      by (auto simp: pairwise_def bij_betw_def inj_on_def)
   5.266 -    show "orthogonal_matrix (\<chi> i j. f j $ i)"
   5.267 -      by (simp add: orthogonal_matrix_orthonormal_columns column_def)
   5.268 -    show "(\<chi> i j. f j $ i) *v axis k 1 = a"
   5.269 -      by (simp add: matrix_vector_mult_def axis_def a if_distrib cong: if_cong)
   5.270 -  qed
   5.271 -qed
   5.272 -
   5.273 -lemma%unimportant  orthogonal_transformation_exists_1:
   5.274 -  fixes a b :: "real^'n"
   5.275 -  assumes "norm a = 1" "norm b = 1"
   5.276 -  obtains f where "orthogonal_transformation f" "f a = b"
   5.277 -proof%unimportant -
   5.278 -  obtain k::'n where True
   5.279 -    by simp
   5.280 -  obtain A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
   5.281 -    using orthogonal_matrix_exists_basis assms by metis
   5.282 -  let ?f = "\<lambda>x. (B ** transpose A) *v x"
   5.283 -  show thesis
   5.284 -  proof
   5.285 -    show "orthogonal_transformation ?f"
   5.286 -      by (subst orthogonal_transformation_matrix)
   5.287 -        (auto simp: AB orthogonal_matrix_mul)
   5.288 -  next
   5.289 -    show "?f a = b"
   5.290 -      using \<open>orthogonal_matrix A\<close> unfolding orthogonal_matrix_def
   5.291 -      by (metis eq matrix_mul_rid matrix_vector_mul_assoc)
   5.292 -  qed
   5.293 -qed
   5.294 -
   5.295 -lemma%important  orthogonal_transformation_exists:
   5.296 -  fixes a b :: "real^'n"
   5.297 -  assumes "norm a = norm b"
   5.298 -  obtains f where "orthogonal_transformation f" "f a = b"
   5.299 -proof%unimportant (cases "a = 0 \<or> b = 0")
   5.300 -  case True
   5.301 -  with assms show ?thesis
   5.302 -    using that by force
   5.303 -next
   5.304 -  case False
   5.305 -  then obtain f where f: "orthogonal_transformation f" and eq: "f (a /\<^sub>R norm a) = (b /\<^sub>R norm b)"
   5.306 -    by (auto intro: orthogonal_transformation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b"])
   5.307 -  show ?thesis
   5.308 -  proof
   5.309 -    interpret linear f
   5.310 -      using f by (simp add: orthogonal_transformation_linear)
   5.311 -    have "f a /\<^sub>R norm a = f (a /\<^sub>R norm a)"
   5.312 -      by (simp add: scale)
   5.313 -    also have "\<dots> = b /\<^sub>R norm a"
   5.314 -      by (simp add: eq assms [symmetric])
   5.315 -    finally show "f a = b"
   5.316 -      using False by auto
   5.317 -  qed (use f in auto)
   5.318 -qed
   5.319 -
   5.320 -
   5.321 -subsection%important  \<open>Can extend an isometry from unit sphere\<close>
   5.322 -
   5.323 -lemma%important  isometry_sphere_extend:
   5.324 -  fixes f:: "'a::real_inner \<Rightarrow> 'a"
   5.325 -  assumes f1: "\<And>x. norm x = 1 \<Longrightarrow> norm (f x) = 1"
   5.326 -    and fd1: "\<And>x y. \<lbrakk>norm x = 1; norm y = 1\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y"
   5.327 -  shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)"
   5.328 -proof%unimportant -
   5.329 -  {
   5.330 -    fix x y x' y' u v u' v' :: "'a"
   5.331 -    assume H: "x = norm x *\<^sub>R u" "y = norm y *\<^sub>R v"
   5.332 -              "x' = norm x *\<^sub>R u'" "y' = norm y *\<^sub>R v'"
   5.333 -      and J: "norm u = 1" "norm u' = 1" "norm v = 1" "norm v' = 1" "norm(u' - v') = norm(u - v)"
   5.334 -    then have *: "u \<bullet> v = u' \<bullet> v' + v' \<bullet> u' - v \<bullet> u "
   5.335 -      by (simp add: norm_eq norm_eq_1 inner_add inner_diff)
   5.336 -    have "norm (norm x *\<^sub>R u' - norm y *\<^sub>R v') = norm (norm x *\<^sub>R u - norm y *\<^sub>R v)"
   5.337 -      using J by (simp add: norm_eq norm_eq_1 inner_diff * field_simps)
   5.338 -    then have "norm(x' - y') = norm(x - y)"
   5.339 -      using H by metis
   5.340 -  }
   5.341 -  note norm_eq = this
   5.342 -  let ?g = "\<lambda>x. if x = 0 then 0 else norm x *\<^sub>R f (x /\<^sub>R norm x)"
   5.343 -  have thfg: "?g x = f x" if "norm x = 1" for x
   5.344 -    using that by auto
   5.345 -  have thd: "dist (?g x) (?g y) = dist x y" for x y
   5.346 -  proof (cases "x=0 \<or> y=0")
   5.347 -    case False
   5.348 -    show "dist (?g x) (?g y) = dist x y"
   5.349 -      unfolding dist_norm
   5.350 -    proof (rule norm_eq)
   5.351 -      show "x = norm x *\<^sub>R (x /\<^sub>R norm x)" "y = norm y *\<^sub>R (y /\<^sub>R norm y)"
   5.352 -           "norm (f (x /\<^sub>R norm x)) = 1" "norm (f (y /\<^sub>R norm y)) = 1"
   5.353 -        using False f1 by auto
   5.354 -    qed (use False in \<open>auto simp: field_simps intro: f1 fd1[unfolded dist_norm]\<close>)
   5.355 -  qed (auto simp: f1)
   5.356 -  show ?thesis
   5.357 -    unfolding orthogonal_transformation_isometry
   5.358 -    by (rule exI[where x= ?g]) (metis thfg thd)
   5.359 -qed
   5.360 -
   5.361 -subsection%important  \<open>Rotation, reflection, rotoinversion\<close>
   5.362 -
   5.363 -definition%important  "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
   5.364 -definition%important  "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
   5.365 -
   5.366 -lemma%important  orthogonal_rotation_or_rotoinversion:
   5.367 -  fixes Q :: "'a::linordered_idom^'n^'n"
   5.368 -  shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q"
   5.369 -  by%unimportant (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix)
   5.370 -
   5.371 -text \<open>Explicit formulas for low dimensions\<close>
   5.372 -
   5.373 -lemma%unimportant  prod_neutral_const: "prod f {(1::nat)..1} = f 1"
   5.374 -  by simp
   5.375 -
   5.376 -lemma%unimportant  prod_2: "prod f {(1::nat)..2} = f 1 * f 2"
   5.377 -  by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
   5.378 -
   5.379 -lemma%unimportant  prod_3: "prod f {(1::nat)..3} = f 1 * f 2 * f 3"
   5.380 -  by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
   5.381 -
   5.382  lemma%unimportant  det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
   5.383    by (simp add: det_def sign_id)
   5.384  
   5.385 @@ -1342,6 +976,36 @@
   5.386      by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)
   5.387  qed
   5.388  
   5.389 +lemma%important  det_orthogonal_matrix:
   5.390 +  fixes Q:: "'a::linordered_idom^'n^'n"
   5.391 +  assumes oQ: "orthogonal_matrix Q"
   5.392 +  shows "det Q = 1 \<or> det Q = - 1"
   5.393 +proof%unimportant -
   5.394 +  have "Q ** transpose Q = mat 1"
   5.395 +    by (metis oQ orthogonal_matrix_def)
   5.396 +  then have "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)"
   5.397 +    by simp
   5.398 +  then have "det Q * det Q = 1"
   5.399 +    by (simp add: det_mul)
   5.400 +  then show ?thesis
   5.401 +    by (simp add: square_eq_1_iff)
   5.402 +qed
   5.403 +
   5.404 +lemma%important  orthogonal_transformation_det [simp]:
   5.405 +  fixes f :: "real^'n \<Rightarrow> real^'n"
   5.406 +  shows "orthogonal_transformation f \<Longrightarrow> \<bar>det (matrix f)\<bar> = 1"
   5.407 +  using%unimportant det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
   5.408 +
   5.409 +subsection%important  \<open>Rotation, reflection, rotoinversion\<close>
   5.410 +
   5.411 +definition%important  "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
   5.412 +definition%important  "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
   5.413 +
   5.414 +lemma%important  orthogonal_rotation_or_rotoinversion:
   5.415 +  fixes Q :: "'a::linordered_idom^'n^'n"
   5.416 +  shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q"
   5.417 +  by%unimportant (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix)
   5.418 +
   5.419  text\<open> Slightly stronger results giving rotation, but only in two or more dimensions\<close>
   5.420  
   5.421  lemma%unimportant  rotation_matrix_exists_basis:
   5.422 @@ -1360,8 +1024,10 @@
   5.423      then show ?thesis
   5.424        using \<open>A *v axis k 1 = a\<close> that by auto
   5.425    next
   5.426 -    obtain j where "j \<noteq> k"
   5.427 -      by (metis (full_types) 2 card_2_exists ex_card)
   5.428 +    from ex_card[OF 2] obtain h i::'n where "h \<noteq> i"
   5.429 +      by (auto simp add: eval_nat_numeral card_Suc_eq)
   5.430 +    then obtain j where "j \<noteq> k"
   5.431 +      by (metis (full_types))
   5.432      let ?TA = "transpose A"
   5.433      let ?A = "\<chi> i. if i = j then - 1 *\<^sub>R (?TA $ i) else ?TA $i"
   5.434      assume "rotoinversion_matrix A"
     6.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 16 16:50:35 2019 -0500
     6.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 16 18:14:02 2019 -0500
     6.3 @@ -30,6 +30,79 @@
     6.4  lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x \<in> (UNIV::'a::finite set)}"
     6.5    using finite finite_image_set by blast
     6.6  
     6.7 +lemma substdbasis_expansion_unique:
     6.8 +  includes inner_syntax
     6.9 +  assumes d: "d \<subseteq> Basis"
    6.10 +  shows "(\<Sum>i\<in>d. f i *\<^sub>R i) = (x::'a::euclidean_space) \<longleftrightarrow>
    6.11 +    (\<forall>i\<in>Basis. (i \<in> d \<longrightarrow> f i = x \<bullet> i) \<and> (i \<notin> d \<longrightarrow> x \<bullet> i = 0))"
    6.12 +proof -
    6.13 +  have *: "\<And>x a b P. x * (if P then a else b) = (if P then x * a else x * b)"
    6.14 +    by auto
    6.15 +  have **: "finite d"
    6.16 +    by (auto intro: finite_subset[OF assms])
    6.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)"
    6.18 +    using d
    6.19 +    by (auto intro!: sum.cong simp: inner_Basis inner_sum_left)
    6.20 +  show ?thesis
    6.21 +    unfolding euclidean_eq_iff[where 'a='a] by (auto simp: sum.delta[OF **] ***)
    6.22 +qed
    6.23 +
    6.24 +lemma independent_substdbasis: "d \<subseteq> Basis \<Longrightarrow> independent d"
    6.25 +  by (rule independent_mono[OF independent_Basis])
    6.26 +
    6.27 +lemma sum_not_0: "sum f A \<noteq> 0 \<Longrightarrow> \<exists>a \<in> A. f a \<noteq> 0"
    6.28 +  by (rule ccontr) auto
    6.29 +
    6.30 +lemma subset_translation_eq [simp]:
    6.31 +    fixes a :: "'a::real_vector" shows "(+) a ` s \<subseteq> (+) a ` t \<longleftrightarrow> s \<subseteq> t"
    6.32 +  by auto
    6.33 +
    6.34 +lemma translate_inj_on:
    6.35 +  fixes A :: "'a::ab_group_add set"
    6.36 +  shows "inj_on (\<lambda>x. a + x) A"
    6.37 +  unfolding inj_on_def by auto
    6.38 +
    6.39 +lemma translation_assoc:
    6.40 +  fixes a b :: "'a::ab_group_add"
    6.41 +  shows "(\<lambda>x. b + x) ` ((\<lambda>x. a + x) ` S) = (\<lambda>x. (a + b) + x) ` S"
    6.42 +  by auto
    6.43 +
    6.44 +lemma translation_invert:
    6.45 +  fixes a :: "'a::ab_group_add"
    6.46 +  assumes "(\<lambda>x. a + x) ` A = (\<lambda>x. a + x) ` B"
    6.47 +  shows "A = B"
    6.48 +proof -
    6.49 +  have "(\<lambda>x. -a + x) ` ((\<lambda>x. a + x) ` A) = (\<lambda>x. - a + x) ` ((\<lambda>x. a + x) ` B)"
    6.50 +    using assms by auto
    6.51 +  then show ?thesis
    6.52 +    using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto
    6.53 +qed
    6.54 +
    6.55 +lemma translation_galois:
    6.56 +  fixes a :: "'a::ab_group_add"
    6.57 +  shows "T = ((\<lambda>x. a + x) ` S) \<longleftrightarrow> S = ((\<lambda>x. (- a) + x) ` T)"
    6.58 +  using translation_assoc[of "-a" a S]
    6.59 +  apply auto
    6.60 +  using translation_assoc[of a "-a" T]
    6.61 +  apply auto
    6.62 +  done
    6.63 +
    6.64 +lemma translation_inverse_subset:
    6.65 +  assumes "((\<lambda>x. - a + x) ` V) \<le> (S :: 'n::ab_group_add set)"
    6.66 +  shows "V \<le> ((\<lambda>x. a + x) ` S)"
    6.67 +proof -
    6.68 +  {
    6.69 +    fix x
    6.70 +    assume "x \<in> V"
    6.71 +    then have "x-a \<in> S" using assms by auto
    6.72 +    then have "x \<in> {a + v |v. v \<in> S}"
    6.73 +      apply auto
    6.74 +      apply (rule exI[of _ "x-a"], simp)
    6.75 +      done
    6.76 +    then have "x \<in> ((\<lambda>x. a+x) ` S)" by auto
    6.77 +  }
    6.78 +  then show ?thesis by auto
    6.79 +qed
    6.80  
    6.81  subsection%unimportant \<open>More interesting properties of the norm\<close>
    6.82  
    6.83 @@ -224,6 +297,66 @@
    6.84  qed
    6.85  
    6.86  
    6.87 +subsection%important  \<open>Orthogonality of a transformation\<close>
    6.88 +
    6.89 +definition%important  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
    6.90 +
    6.91 +lemma%unimportant  orthogonal_transformation:
    6.92 +  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v. norm (f v) = norm v)"
    6.93 +  unfolding orthogonal_transformation_def
    6.94 +  apply auto
    6.95 +  apply (erule_tac x=v in allE)+
    6.96 +  apply (simp add: norm_eq_sqrt_inner)
    6.97 +  apply (simp add: dot_norm linear_add[symmetric])
    6.98 +  done
    6.99 +
   6.100 +lemma%unimportant  orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
   6.101 +  by (simp add: linear_iff orthogonal_transformation_def)
   6.102 +
   6.103 +lemma%unimportant  orthogonal_orthogonal_transformation:
   6.104 +    "orthogonal_transformation f \<Longrightarrow> orthogonal (f x) (f y) \<longleftrightarrow> orthogonal x y"
   6.105 +  by (simp add: orthogonal_def orthogonal_transformation_def)
   6.106 +
   6.107 +lemma%unimportant  orthogonal_transformation_compose:
   6.108 +   "\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)"
   6.109 +  by (auto simp: orthogonal_transformation_def linear_compose)
   6.110 +
   6.111 +lemma%unimportant  orthogonal_transformation_neg:
   6.112 +  "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
   6.113 +  by (auto simp: orthogonal_transformation_def dest: linear_compose_neg)
   6.114 +
   6.115 +lemma%unimportant  orthogonal_transformation_scaleR: "orthogonal_transformation f \<Longrightarrow> f (c *\<^sub>R v) = c *\<^sub>R f v"
   6.116 +  by (simp add: linear_iff orthogonal_transformation_def)
   6.117 +
   6.118 +lemma%unimportant  orthogonal_transformation_linear:
   6.119 +   "orthogonal_transformation f \<Longrightarrow> linear f"
   6.120 +  by (simp add: orthogonal_transformation_def)
   6.121 +
   6.122 +lemma%unimportant  orthogonal_transformation_inj:
   6.123 +  "orthogonal_transformation f \<Longrightarrow> inj f"
   6.124 +  unfolding orthogonal_transformation_def inj_on_def
   6.125 +  by (metis vector_eq)
   6.126 +
   6.127 +lemma%unimportant  orthogonal_transformation_surj:
   6.128 +  "orthogonal_transformation f \<Longrightarrow> surj f"
   6.129 +  for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   6.130 +  by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear)
   6.131 +
   6.132 +lemma%unimportant  orthogonal_transformation_bij:
   6.133 +  "orthogonal_transformation f \<Longrightarrow> bij f"
   6.134 +  for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   6.135 +  by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj)
   6.136 +
   6.137 +lemma%unimportant  orthogonal_transformation_inv:
   6.138 +  "orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)"
   6.139 +  for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   6.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)
   6.141 +
   6.142 +lemma%unimportant  orthogonal_transformation_norm:
   6.143 +  "orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x"
   6.144 +  by (metis orthogonal_transformation)
   6.145 +
   6.146 +
   6.147  subsection \<open>Bilinear functions\<close>
   6.148  
   6.149  definition%important
   6.150 @@ -1210,4 +1343,540 @@
   6.151    qed
   6.152  qed
   6.153  
   6.154 +
   6.155 +subsection\<open>Properties of special hyperplanes\<close>
   6.156 +
   6.157 +lemma subspace_hyperplane: "subspace {x. a \<bullet> x = 0}"
   6.158 +  by (simp add: subspace_def inner_right_distrib)
   6.159 +
   6.160 +lemma subspace_hyperplane2: "subspace {x. x \<bullet> a = 0}"
   6.161 +  by (simp add: inner_commute inner_right_distrib subspace_def)
   6.162 +
   6.163 +lemma special_hyperplane_span:
   6.164 +  fixes S :: "'n::euclidean_space set"
   6.165 +  assumes "k \<in> Basis"
   6.166 +  shows "{x. k \<bullet> x = 0} = span (Basis - {k})"
   6.167 +proof -
   6.168 +  have *: "x \<in> span (Basis - {k})" if "k \<bullet> x = 0" for x
   6.169 +  proof -
   6.170 +    have "x = (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b)"
   6.171 +      by (simp add: euclidean_representation)
   6.172 +    also have "... = (\<Sum>b \<in> Basis - {k}. (x \<bullet> b) *\<^sub>R b)"
   6.173 +      by (auto simp: sum.remove [of _ k] inner_commute assms that)
   6.174 +    finally have "x = (\<Sum>b\<in>Basis - {k}. (x \<bullet> b) *\<^sub>R b)" .
   6.175 +    then show ?thesis
   6.176 +      by (simp add: span_finite)
   6.177 +  qed
   6.178 +  show ?thesis
   6.179 +    apply (rule span_subspace [symmetric])
   6.180 +    using assms
   6.181 +    apply (auto simp: inner_not_same_Basis intro: * subspace_hyperplane)
   6.182 +    done
   6.183 +qed
   6.184 +
   6.185 +lemma dim_special_hyperplane:
   6.186 +  fixes k :: "'n::euclidean_space"
   6.187 +  shows "k \<in> Basis \<Longrightarrow> dim {x. k \<bullet> x = 0} = DIM('n) - 1"
   6.188 +apply (simp add: special_hyperplane_span)
   6.189 +apply (rule dim_unique [OF subset_refl])
   6.190 +apply (auto simp: independent_substdbasis)
   6.191 +apply (metis member_remove remove_def span_base)
   6.192 +done
   6.193 +
   6.194 +proposition dim_hyperplane:
   6.195 +  fixes a :: "'a::euclidean_space"
   6.196 +  assumes "a \<noteq> 0"
   6.197 +    shows "dim {x. a \<bullet> x = 0} = DIM('a) - 1"
   6.198 +proof -
   6.199 +  have span0: "span {x. a \<bullet> x = 0} = {x. a \<bullet> x = 0}"
   6.200 +    by (rule span_unique) (auto simp: subspace_hyperplane)
   6.201 +  then obtain B where "independent B"
   6.202 +              and Bsub: "B \<subseteq> {x. a \<bullet> x = 0}"
   6.203 +              and subspB: "{x. a \<bullet> x = 0} \<subseteq> span B"
   6.204 +              and card0: "(card B = dim {x. a \<bullet> x = 0})"
   6.205 +              and ortho: "pairwise orthogonal B"
   6.206 +    using orthogonal_basis_exists by metis
   6.207 +  with assms have "a \<notin> span B"
   6.208 +    by (metis (mono_tags, lifting) span_eq inner_eq_zero_iff mem_Collect_eq span0)
   6.209 +  then have ind: "independent (insert a B)"
   6.210 +    by (simp add: \<open>independent B\<close> independent_insert)
   6.211 +  have "finite B"
   6.212 +    using \<open>independent B\<close> independent_bound by blast
   6.213 +  have "UNIV \<subseteq> span (insert a B)"
   6.214 +  proof fix y::'a
   6.215 +    obtain r z where z: "y = r *\<^sub>R a + z" "a \<bullet> z = 0"
   6.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)
   6.217 +      using assms
   6.218 +      by (auto simp: algebra_simps)
   6.219 +    show "y \<in> span (insert a B)"
   6.220 +      by (metis (mono_tags, lifting) z Bsub span_eq_iff
   6.221 +         add_diff_cancel_left' mem_Collect_eq span0 span_breakdown_eq span_subspace subspB)
   6.222 +  qed
   6.223 +  then have dima: "DIM('a) = dim(insert a B)"
   6.224 +    by (metis independent_Basis span_Basis dim_eq_card top.extremum_uniqueI)
   6.225 +  then show ?thesis
   6.226 +    by (metis (mono_tags, lifting) Bsub Diff_insert_absorb \<open>a \<notin> span B\<close> ind card0
   6.227 +        card_Diff_singleton dim_span indep_card_eq_dim_span insertI1 subsetCE
   6.228 +        subspB)
   6.229 +qed
   6.230 +
   6.231 +lemma lowdim_eq_hyperplane:
   6.232 +  fixes S :: "'a::euclidean_space set"
   6.233 +  assumes "dim S = DIM('a) - 1"
   6.234 +  obtains a where "a \<noteq> 0" and "span S = {x. a \<bullet> x = 0}"
   6.235 +proof -
   6.236 +  have dimS: "dim S < DIM('a)"
   6.237 +    by (simp add: assms)
   6.238 +  then obtain b where b: "b \<noteq> 0" "span S \<subseteq> {a. b \<bullet> a = 0}"
   6.239 +    using lowdim_subset_hyperplane [of S] by fastforce
   6.240 +  show ?thesis
   6.241 +    apply (rule that[OF b(1)])
   6.242 +    apply (rule subspace_dim_equal)
   6.243 +    by (auto simp: assms b dim_hyperplane dim_span subspace_hyperplane
   6.244 +        subspace_span)
   6.245 +qed
   6.246 +
   6.247 +lemma dim_eq_hyperplane:
   6.248 +  fixes S :: "'n::euclidean_space set"
   6.249 +  shows "dim S = DIM('n) - 1 \<longleftrightarrow> (\<exists>a. a \<noteq> 0 \<and> span S = {x. a \<bullet> x = 0})"
   6.250 +by (metis One_nat_def dim_hyperplane dim_span lowdim_eq_hyperplane)
   6.251 +
   6.252 +
   6.253 +subsection\<open> Orthogonal bases, Gram-Schmidt process, and related theorems\<close>
   6.254 +
   6.255 +lemma pairwise_orthogonal_independent:
   6.256 +  assumes "pairwise orthogonal S" and "0 \<notin> S"
   6.257 +    shows "independent S"
   6.258 +proof -
   6.259 +  have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   6.260 +    using assms by (simp add: pairwise_def orthogonal_def)
   6.261 +  have "False" if "a \<in> S" and a: "a \<in> span (S - {a})" for a
   6.262 +  proof -
   6.263 +    obtain T U where "T \<subseteq> S - {a}" "a = (\<Sum>v\<in>T. U v *\<^sub>R v)"
   6.264 +      using a by (force simp: span_explicit)
   6.265 +    then have "a \<bullet> a = a \<bullet> (\<Sum>v\<in>T. U v *\<^sub>R v)"
   6.266 +      by simp
   6.267 +    also have "... = 0"
   6.268 +      apply (simp add: inner_sum_right)
   6.269 +      apply (rule comm_monoid_add_class.sum.neutral)
   6.270 +      by (metis "0" DiffE \<open>T \<subseteq> S - {a}\<close> mult_not_zero singletonI subsetCE \<open>a \<in> S\<close>)
   6.271 +    finally show ?thesis
   6.272 +      using \<open>0 \<notin> S\<close> \<open>a \<in> S\<close> by auto
   6.273 +  qed
   6.274 +  then show ?thesis
   6.275 +    by (force simp: dependent_def)
   6.276 +qed
   6.277 +
   6.278 +lemma pairwise_orthogonal_imp_finite:
   6.279 +  fixes S :: "'a::euclidean_space set"
   6.280 +  assumes "pairwise orthogonal S"
   6.281 +    shows "finite S"
   6.282 +proof -
   6.283 +  have "independent (S - {0})"
   6.284 +    apply (rule pairwise_orthogonal_independent)
   6.285 +     apply (metis Diff_iff assms pairwise_def)
   6.286 +    by blast
   6.287 +  then show ?thesis
   6.288 +    by (meson independent_imp_finite infinite_remove)
   6.289 +qed
   6.290 +
   6.291 +lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}"
   6.292 +  by (simp add: subspace_def orthogonal_clauses)
   6.293 +
   6.294 +lemma subspace_orthogonal_to_vectors: "subspace {y. \<forall>x \<in> S. orthogonal x y}"
   6.295 +  by (simp add: subspace_def orthogonal_clauses)
   6.296 +
   6.297 +lemma orthogonal_to_span:
   6.298 +  assumes a: "a \<in> span S" and x: "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
   6.299 +    shows "orthogonal x a"
   6.300 +  by (metis a orthogonal_clauses(1,2,4)
   6.301 +      span_induct_alt x)
   6.302 +
   6.303 +proposition Gram_Schmidt_step:
   6.304 +  fixes S :: "'a::euclidean_space set"
   6.305 +  assumes S: "pairwise orthogonal S" and x: "x \<in> span S"
   6.306 +    shows "orthogonal x (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b))"
   6.307 +proof -
   6.308 +  have "finite S"
   6.309 +    by (simp add: S pairwise_orthogonal_imp_finite)
   6.310 +  have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)) x"
   6.311 +       if "x \<in> S" for x
   6.312 +  proof -
   6.313 +    have "a \<bullet> x = (\<Sum>y\<in>S. if y = x then y \<bullet> a else 0)"
   6.314 +      by (simp add: \<open>finite S\<close> inner_commute sum.delta that)
   6.315 +    also have "... =  (\<Sum>b\<in>S. b \<bullet> a * (b \<bullet> x) / (b \<bullet> b))"
   6.316 +      apply (rule sum.cong [OF refl], simp)
   6.317 +      by (meson S orthogonal_def pairwise_def that)
   6.318 +   finally show ?thesis
   6.319 +     by (simp add: orthogonal_def algebra_simps inner_sum_left)
   6.320 +  qed
   6.321 +  then show ?thesis
   6.322 +    using orthogonal_to_span orthogonal_commute x by blast
   6.323 +qed
   6.324 +
   6.325 +
   6.326 +lemma orthogonal_extension_aux:
   6.327 +  fixes S :: "'a::euclidean_space set"
   6.328 +  assumes "finite T" "finite S" "pairwise orthogonal S"
   6.329 +    shows "\<exists>U. pairwise orthogonal (S \<union> U) \<and> span (S \<union> U) = span (S \<union> T)"
   6.330 +using assms
   6.331 +proof (induction arbitrary: S)
   6.332 +  case empty then show ?case
   6.333 +    by simp (metis sup_bot_right)
   6.334 +next
   6.335 +  case (insert a T)
   6.336 +  have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   6.337 +    using insert by (simp add: pairwise_def orthogonal_def)
   6.338 +  define a' where "a' = a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)"
   6.339 +  obtain U where orthU: "pairwise orthogonal (S \<union> insert a' U)"
   6.340 +             and spanU: "span (insert a' S \<union> U) = span (insert a' S \<union> T)"
   6.341 +    by (rule exE [OF insert.IH [of "insert a' S"]])
   6.342 +      (auto simp: Gram_Schmidt_step a'_def insert.prems orthogonal_commute
   6.343 +        pairwise_orthogonal_insert span_clauses)
   6.344 +  have orthS: "\<And>x. x \<in> S \<Longrightarrow> a' \<bullet> x = 0"
   6.345 +    apply (simp add: a'_def)
   6.346 +    using Gram_Schmidt_step [OF \<open>pairwise orthogonal S\<close>]
   6.347 +    apply (force simp: orthogonal_def inner_commute span_superset [THEN subsetD])
   6.348 +    done
   6.349 +  have "span (S \<union> insert a' U) = span (insert a' (S \<union> T))"
   6.350 +    using spanU by simp
   6.351 +  also have "... = span (insert a (S \<union> T))"
   6.352 +    apply (rule eq_span_insert_eq)
   6.353 +    apply (simp add: a'_def span_neg span_sum span_base span_mul)
   6.354 +    done
   6.355 +  also have "... = span (S \<union> insert a T)"
   6.356 +    by simp
   6.357 +  finally show ?case
   6.358 +    by (rule_tac x="insert a' U" in exI) (use orthU in auto)
   6.359 +qed
   6.360 +
   6.361 +
   6.362 +proposition orthogonal_extension:
   6.363 +  fixes S :: "'a::euclidean_space set"
   6.364 +  assumes S: "pairwise orthogonal S"
   6.365 +  obtains U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
   6.366 +proof -
   6.367 +  obtain B where "finite B" "span B = span T"
   6.368 +    using basis_subspace_exists [of "span T"] subspace_span by metis
   6.369 +  with orthogonal_extension_aux [of B S]
   6.370 +  obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> B)"
   6.371 +    using assms pairwise_orthogonal_imp_finite by auto
   6.372 +  with \<open>span B = span T\<close> show ?thesis
   6.373 +    by (rule_tac U=U in that) (auto simp: span_Un)
   6.374 +qed
   6.375 +
   6.376 +corollary%unimportant orthogonal_extension_strong:
   6.377 +  fixes S :: "'a::euclidean_space set"
   6.378 +  assumes S: "pairwise orthogonal S"
   6.379 +  obtains U where "U \<inter> (insert 0 S) = {}" "pairwise orthogonal (S \<union> U)"
   6.380 +                  "span (S \<union> U) = span (S \<union> T)"
   6.381 +proof -
   6.382 +  obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
   6.383 +    using orthogonal_extension assms by blast
   6.384 +  then show ?thesis
   6.385 +    apply (rule_tac U = "U - (insert 0 S)" in that)
   6.386 +      apply blast
   6.387 +     apply (force simp: pairwise_def)
   6.388 +    apply (metis Un_Diff_cancel Un_insert_left span_redundant span_zero)
   6.389 +    done
   6.390 +qed
   6.391 +
   6.392 +subsection\<open>Decomposing a vector into parts in orthogonal subspaces\<close>
   6.393 +
   6.394 +text\<open>existence of orthonormal basis for a subspace.\<close>
   6.395 +
   6.396 +lemma orthogonal_spanningset_subspace:
   6.397 +  fixes S :: "'a :: euclidean_space set"
   6.398 +  assumes "subspace S"
   6.399 +  obtains B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S"
   6.400 +proof -
   6.401 +  obtain B where "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S"
   6.402 +    using basis_exists by blast
   6.403 +  with orthogonal_extension [of "{}" B]
   6.404 +  show ?thesis
   6.405 +    by (metis Un_empty_left assms pairwise_empty span_superset span_subspace that)
   6.406 +qed
   6.407 +
   6.408 +lemma orthogonal_basis_subspace:
   6.409 +  fixes S :: "'a :: euclidean_space set"
   6.410 +  assumes "subspace S"
   6.411 +  obtains B where "0 \<notin> B" "B \<subseteq> S" "pairwise orthogonal B" "independent B"
   6.412 +                  "card B = dim S" "span B = S"
   6.413 +proof -
   6.414 +  obtain B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S"
   6.415 +    using assms orthogonal_spanningset_subspace by blast
   6.416 +  then show ?thesis
   6.417 +    apply (rule_tac B = "B - {0}" in that)
   6.418 +    apply (auto simp: indep_card_eq_dim_span pairwise_subset pairwise_orthogonal_independent elim: pairwise_subset)
   6.419 +    done
   6.420 +qed
   6.421 +
   6.422 +proposition orthonormal_basis_subspace:
   6.423 +  fixes S :: "'a :: euclidean_space set"
   6.424 +  assumes "subspace S"
   6.425 +  obtains B where "B \<subseteq> S" "pairwise orthogonal B"
   6.426 +              and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
   6.427 +              and "independent B" "card B = dim S" "span B = S"
   6.428 +proof -
   6.429 +  obtain B where "0 \<notin> B" "B \<subseteq> S"
   6.430 +             and orth: "pairwise orthogonal B"
   6.431 +             and "independent B" "card B = dim S" "span B = S"
   6.432 +    by (blast intro: orthogonal_basis_subspace [OF assms])
   6.433 +  have 1: "(\<lambda>x. x /\<^sub>R norm x) ` B \<subseteq> S"
   6.434 +    using \<open>span B = S\<close> span_superset span_mul by fastforce
   6.435 +  have 2: "pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` B)"
   6.436 +    using orth by (force simp: pairwise_def orthogonal_clauses)
   6.437 +  have 3: "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` B \<Longrightarrow> norm x = 1"
   6.438 +    by (metis (no_types, lifting) \<open>0 \<notin> B\<close> image_iff norm_sgn sgn_div_norm)
   6.439 +  have 4: "independent ((\<lambda>x. x /\<^sub>R norm x) ` B)"
   6.440 +    by (metis "2" "3" norm_zero pairwise_orthogonal_independent zero_neq_one)
   6.441 +  have "inj_on (\<lambda>x. x /\<^sub>R norm x) B"
   6.442 +  proof
   6.443 +    fix x y
   6.444 +    assume "x \<in> B" "y \<in> B" "x /\<^sub>R norm x = y /\<^sub>R norm y"
   6.445 +    moreover have "\<And>i. i \<in> B \<Longrightarrow> norm (i /\<^sub>R norm i) = 1"
   6.446 +      using 3 by blast
   6.447 +    ultimately show "x = y"
   6.448 +      by (metis norm_eq_1 orth orthogonal_clauses(7) orthogonal_commute orthogonal_def pairwise_def zero_neq_one)
   6.449 +  qed
   6.450 +  then have 5: "card ((\<lambda>x. x /\<^sub>R norm x) ` B) = dim S"
   6.451 +    by (metis \<open>card B = dim S\<close> card_image)
   6.452 +  have 6: "span ((\<lambda>x. x /\<^sub>R norm x) ` B) = S"
   6.453 +    by (metis "1" "4" "5" assms card_eq_dim independent_imp_finite span_subspace)
   6.454 +  show ?thesis
   6.455 +    by (rule that [OF 1 2 3 4 5 6])
   6.456 +qed
   6.457 +
   6.458 +
   6.459 +proposition%unimportant orthogonal_to_subspace_exists_gen:
   6.460 +  fixes S :: "'a :: euclidean_space set"
   6.461 +  assumes "span S \<subset> span T"
   6.462 +  obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
   6.463 +proof -
   6.464 +  obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
   6.465 +             and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
   6.466 +             and "independent B" "card B = dim S" "span B = span S"
   6.467 +    by (rule orthonormal_basis_subspace [of "span S", OF subspace_span])
   6.468 +      (auto simp: dim_span)
   6.469 +  with assms obtain u where spanBT: "span B \<subseteq> span T" and "u \<notin> span B" "u \<in> span T"
   6.470 +    by auto
   6.471 +  obtain C where orthBC: "pairwise orthogonal (B \<union> C)" and spanBC: "span (B \<union> C) = span (B \<union> {u})"
   6.472 +    by (blast intro: orthogonal_extension [OF orthB])
   6.473 +  show thesis
   6.474 +  proof (cases "C \<subseteq> insert 0 B")
   6.475 +    case True
   6.476 +    then have "C \<subseteq> span B"
   6.477 +      using span_eq
   6.478 +      by (metis span_insert_0 subset_trans)
   6.479 +    moreover have "u \<in> span (B \<union> C)"
   6.480 +      using \<open>span (B \<union> C) = span (B \<union> {u})\<close> span_superset by force
   6.481 +    ultimately show ?thesis
   6.482 +      using True \<open>u \<notin> span B\<close>
   6.483 +      by (metis Un_insert_left span_insert_0 sup.orderE)
   6.484 +  next
   6.485 +    case False
   6.486 +    then obtain x where "x \<in> C" "x \<noteq> 0" "x \<notin> B"
   6.487 +      by blast
   6.488 +    then have "x \<in> span T"
   6.489 +      by (metis (no_types, lifting) Un_insert_right Un_upper2 \<open>u \<in> span T\<close> spanBT spanBC
   6.490 +          \<open>u \<in> span T\<close> insert_subset span_superset span_mono
   6.491 +          span_span subsetCE subset_trans sup_bot.comm_neutral)
   6.492 +    moreover have "orthogonal x y" if "y \<in> span B" for y
   6.493 +      using that
   6.494 +    proof (rule span_induct)
   6.495 +      show "subspace {a. orthogonal x a}"
   6.496 +        by (simp add: subspace_orthogonal_to_vector)
   6.497 +      show "\<And>b. b \<in> B \<Longrightarrow> orthogonal x b"
   6.498 +        by (metis Un_iff \<open>x \<in> C\<close> \<open>x \<notin> B\<close> orthBC pairwise_def)
   6.499 +    qed
   6.500 +    ultimately show ?thesis
   6.501 +      using \<open>x \<noteq> 0\<close> that \<open>span B = span S\<close> by auto
   6.502 +  qed
   6.503 +qed
   6.504 +
   6.505 +corollary%unimportant orthogonal_to_subspace_exists:
   6.506 +  fixes S :: "'a :: euclidean_space set"
   6.507 +  assumes "dim S < DIM('a)"
   6.508 +  obtains x where "x \<noteq> 0" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
   6.509 +proof -
   6.510 +have "span S \<subset> UNIV"
   6.511 +  by (metis (mono_tags) UNIV_I assms inner_eq_zero_iff less_le lowdim_subset_hyperplane
   6.512 +      mem_Collect_eq top.extremum_strict top.not_eq_extremum)
   6.513 +  with orthogonal_to_subspace_exists_gen [of S UNIV] that show ?thesis
   6.514 +    by (auto simp: span_UNIV)
   6.515 +qed
   6.516 +
   6.517 +corollary%unimportant orthogonal_to_vector_exists:
   6.518 +  fixes x :: "'a :: euclidean_space"
   6.519 +  assumes "2 \<le> DIM('a)"
   6.520 +  obtains y where "y \<noteq> 0" "orthogonal x y"
   6.521 +proof -
   6.522 +  have "dim {x} < DIM('a)"
   6.523 +    using assms by auto
   6.524 +  then show thesis
   6.525 +    by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that)
   6.526 +qed
   6.527 +
   6.528 +proposition%unimportant orthogonal_subspace_decomp_exists:
   6.529 +  fixes S :: "'a :: euclidean_space set"
   6.530 +  obtains y z
   6.531 +  where "y \<in> span S"
   6.532 +    and "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w"
   6.533 +    and "x = y + z"
   6.534 +proof -
   6.535 +  obtain T where "0 \<notin> T" "T \<subseteq> span S" "pairwise orthogonal T" "independent T"
   6.536 +    "card T = dim (span S)" "span T = span S"
   6.537 +    using orthogonal_basis_subspace subspace_span by blast
   6.538 +  let ?a = "\<Sum>b\<in>T. (b \<bullet> x / (b \<bullet> b)) *\<^sub>R b"
   6.539 +  have orth: "orthogonal (x - ?a) w" if "w \<in> span S" for w
   6.540 +    by (simp add: Gram_Schmidt_step \<open>pairwise orthogonal T\<close> \<open>span T = span S\<close>
   6.541 +        orthogonal_commute that)
   6.542 +  show ?thesis
   6.543 +    apply (rule_tac y = "?a" and z = "x - ?a" in that)
   6.544 +      apply (meson \<open>T \<subseteq> span S\<close> span_scale span_sum subsetCE)
   6.545 +     apply (fact orth, simp)
   6.546 +    done
   6.547 +qed
   6.548 +
   6.549 +lemma orthogonal_subspace_decomp_unique:
   6.550 +  fixes S :: "'a :: euclidean_space set"
   6.551 +  assumes "x + y = x' + y'"
   6.552 +      and ST: "x \<in> span S" "x' \<in> span S" "y \<in> span T" "y' \<in> span T"
   6.553 +      and orth: "\<And>a b. \<lbrakk>a \<in> S; b \<in> T\<rbrakk> \<Longrightarrow> orthogonal a b"
   6.554 +  shows "x = x' \<and> y = y'"
   6.555 +proof -
   6.556 +  have "x + y - y' = x'"
   6.557 +    by (simp add: assms)
   6.558 +  moreover have "\<And>a b. \<lbrakk>a \<in> span S; b \<in> span T\<rbrakk> \<Longrightarrow> orthogonal a b"
   6.559 +    by (meson orth orthogonal_commute orthogonal_to_span)
   6.560 +  ultimately have "0 = x' - x"
   6.561 +    by (metis (full_types) add_diff_cancel_left' ST diff_right_commute orthogonal_clauses(10) orthogonal_clauses(5) orthogonal_self)
   6.562 +  with assms show ?thesis by auto
   6.563 +qed
   6.564 +
   6.565 +lemma vector_in_orthogonal_spanningset:
   6.566 +  fixes a :: "'a::euclidean_space"
   6.567 +  obtains S where "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
   6.568 +  by (metis UNIV_I Un_iff empty_iff insert_subset orthogonal_extension pairwise_def
   6.569 +      pairwise_orthogonal_insert span_UNIV subsetI subset_antisym)
   6.570 +
   6.571 +lemma vector_in_orthogonal_basis:
   6.572 +  fixes a :: "'a::euclidean_space"
   6.573 +  assumes "a \<noteq> 0"
   6.574 +  obtains S where "a \<in> S" "0 \<notin> S" "pairwise orthogonal S" "independent S" "finite S"
   6.575 +                  "span S = UNIV" "card S = DIM('a)"
   6.576 +proof -
   6.577 +  obtain S where S: "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
   6.578 +    using vector_in_orthogonal_spanningset .
   6.579 +  show thesis
   6.580 +  proof
   6.581 +    show "pairwise orthogonal (S - {0})"
   6.582 +      using pairwise_mono S(2) by blast
   6.583 +    show "independent (S - {0})"
   6.584 +      by (simp add: \<open>pairwise orthogonal (S - {0})\<close> pairwise_orthogonal_independent)
   6.585 +    show "finite (S - {0})"
   6.586 +      using \<open>independent (S - {0})\<close> independent_imp_finite by blast
   6.587 +    show "card (S - {0}) = DIM('a)"
   6.588 +      using span_delete_0 [of S] S
   6.589 +      by (simp add: \<open>independent (S - {0})\<close> indep_card_eq_dim_span dim_UNIV)
   6.590 +  qed (use S \<open>a \<noteq> 0\<close> in auto)
   6.591 +qed
   6.592 +
   6.593 +lemma vector_in_orthonormal_basis:
   6.594 +  fixes a :: "'a::euclidean_space"
   6.595 +  assumes "norm a = 1"
   6.596 +  obtains S where "a \<in> S" "pairwise orthogonal S" "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
   6.597 +    "independent S" "card S = DIM('a)" "span S = UNIV"
   6.598 +proof -
   6.599 +  have "a \<noteq> 0"
   6.600 +    using assms by auto
   6.601 +  then obtain S where "a \<in> S" "0 \<notin> S" "finite S"
   6.602 +          and S: "pairwise orthogonal S" "independent S" "span S = UNIV" "card S = DIM('a)"
   6.603 +    by (metis vector_in_orthogonal_basis)
   6.604 +  let ?S = "(\<lambda>x. x /\<^sub>R norm x) ` S"
   6.605 +  show thesis
   6.606 +  proof
   6.607 +    show "a \<in> ?S"
   6.608 +      using \<open>a \<in> S\<close> assms image_iff by fastforce
   6.609 +  next
   6.610 +    show "pairwise orthogonal ?S"
   6.611 +      using \<open>pairwise orthogonal S\<close> by (auto simp: pairwise_def orthogonal_def)
   6.612 +    show "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` S \<Longrightarrow> norm x = 1"
   6.613 +      using \<open>0 \<notin> S\<close> by (auto simp: divide_simps)
   6.614 +    then show "independent ?S"
   6.615 +      by (metis \<open>pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` S)\<close> norm_zero pairwise_orthogonal_independent zero_neq_one)
   6.616 +    have "inj_on (\<lambda>x. x /\<^sub>R norm x) S"
   6.617 +      unfolding inj_on_def
   6.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)
   6.619 +    then show "card ?S = DIM('a)"
   6.620 +      by (simp add: card_image S)
   6.621 +    show "span ?S = UNIV"
   6.622 +      by (metis (no_types) \<open>0 \<notin> S\<close> \<open>finite S\<close> \<open>span S = UNIV\<close>
   6.623 +          field_class.field_inverse_zero inverse_inverse_eq less_irrefl span_image_scale
   6.624 +          zero_less_norm_iff)
   6.625 +  qed
   6.626 +qed
   6.627 +
   6.628 +proposition dim_orthogonal_sum:
   6.629 +  fixes A :: "'a::euclidean_space set"
   6.630 +  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   6.631 +    shows "dim(A \<union> B) = dim A + dim B"
   6.632 +proof -
   6.633 +  have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   6.634 +    by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms)
   6.635 +  have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   6.636 +    using 1 by (simp add: span_induct [OF _ subspace_hyperplane])
   6.637 +  then have 0: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   6.638 +    by simp
   6.639 +  have "dim(A \<union> B) = dim (span (A \<union> B))"
   6.640 +    by (simp add: dim_span)
   6.641 +  also have "span (A \<union> B) = ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
   6.642 +    by (auto simp add: span_Un image_def)
   6.643 +  also have "dim \<dots> = dim {x + y |x y. x \<in> span A \<and> y \<in> span B}"
   6.644 +    by (auto intro!: arg_cong [where f=dim])
   6.645 +  also have "... = dim {x + y |x y. x \<in> span A \<and> y \<in> span B} + dim(span A \<inter> span B)"
   6.646 +    by (auto simp: dest: 0)
   6.647 +  also have "... = dim (span A) + dim (span B)"
   6.648 +    by (rule dim_sums_Int) (auto simp: subspace_span)
   6.649 +  also have "... = dim A + dim B"
   6.650 +    by (simp add: dim_span)
   6.651 +  finally show ?thesis .
   6.652 +qed
   6.653 +
   6.654 +lemma dim_subspace_orthogonal_to_vectors:
   6.655 +  fixes A :: "'a::euclidean_space set"
   6.656 +  assumes "subspace A" "subspace B" "A \<subseteq> B"
   6.657 +    shows "dim {y \<in> B. \<forall>x \<in> A. orthogonal x y} + dim A = dim B"
   6.658 +proof -
   6.659 +  have "dim (span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)) = dim (span B)"
   6.660 +  proof (rule arg_cong [where f=dim, OF subset_antisym])
   6.661 +    show "span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A) \<subseteq> span B"
   6.662 +      by (simp add: \<open>A \<subseteq> B\<close> Collect_restrict span_mono)
   6.663 +  next
   6.664 +    have *: "x \<in> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)"
   6.665 +         if "x \<in> B" for x
   6.666 +    proof -
   6.667 +      obtain y z where "x = y + z" "y \<in> span A" and orth: "\<And>w. w \<in> span A \<Longrightarrow> orthogonal z w"
   6.668 +        using orthogonal_subspace_decomp_exists [of A x] that by auto
   6.669 +      have "y \<in> span B"
   6.670 +        using \<open>y \<in> span A\<close> assms(3) span_mono by blast
   6.671 +      then have "z \<in> {a \<in> B. \<forall>x. x \<in> A \<longrightarrow> orthogonal x a}"
   6.672 +        apply simp
   6.673 +        using \<open>x = y + z\<close> assms(1) assms(2) orth orthogonal_commute span_add_eq
   6.674 +          span_eq_iff that by blast
   6.675 +      then have z: "z \<in> span {y \<in> B. \<forall>x\<in>A. orthogonal x y}"
   6.676 +        by (meson span_superset subset_iff)
   6.677 +      then show ?thesis
   6.678 +        apply (auto simp: span_Un image_def  \<open>x = y + z\<close> \<open>y \<in> span A\<close>)
   6.679 +        using \<open>y \<in> span A\<close> add.commute by blast
   6.680 +    qed
   6.681 +    show "span B \<subseteq> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)"
   6.682 +      by (rule span_minimal)
   6.683 +        (auto intro: * span_minimal simp: subspace_span)
   6.684 +  qed
   6.685 +  then show ?thesis
   6.686 +    by (metis (no_types, lifting) dim_orthogonal_sum dim_span mem_Collect_eq
   6.687 +        orthogonal_commute orthogonal_def)
   6.688 +qed
   6.689 +
   6.690  end
     7.1 --- a/src/HOL/Analysis/Starlike.thy	Wed Jan 16 16:50:35 2019 -0500
     7.2 +++ b/src/HOL/Analysis/Starlike.thy	Wed Jan 16 18:14:02 2019 -0500
     7.3 @@ -5469,103 +5469,6 @@
     7.4          (if a = 0 \<and> r > 0 then -1 else DIM('a))"
     7.5  using aff_dim_halfspace_le [of "-a" "-r"] by simp
     7.6  
     7.7 -subsection\<open>Properties of special hyperplanes\<close>
     7.8 -
     7.9 -lemma subspace_hyperplane: "subspace {x. a \<bullet> x = 0}"
    7.10 -  by (simp add: subspace_def inner_right_distrib)
    7.11 -
    7.12 -lemma subspace_hyperplane2: "subspace {x. x \<bullet> a = 0}"
    7.13 -  by (simp add: inner_commute inner_right_distrib subspace_def)
    7.14 -
    7.15 -lemma special_hyperplane_span:
    7.16 -  fixes S :: "'n::euclidean_space set"
    7.17 -  assumes "k \<in> Basis"
    7.18 -  shows "{x. k \<bullet> x = 0} = span (Basis - {k})"
    7.19 -proof -
    7.20 -  have *: "x \<in> span (Basis - {k})" if "k \<bullet> x = 0" for x
    7.21 -  proof -
    7.22 -    have "x = (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b)"
    7.23 -      by (simp add: euclidean_representation)
    7.24 -    also have "... = (\<Sum>b \<in> Basis - {k}. (x \<bullet> b) *\<^sub>R b)"
    7.25 -      by (auto simp: sum.remove [of _ k] inner_commute assms that)
    7.26 -    finally have "x = (\<Sum>b\<in>Basis - {k}. (x \<bullet> b) *\<^sub>R b)" .
    7.27 -    then show ?thesis
    7.28 -      by (simp add: span_finite)
    7.29 -  qed
    7.30 -  show ?thesis
    7.31 -    apply (rule span_subspace [symmetric])
    7.32 -    using assms
    7.33 -    apply (auto simp: inner_not_same_Basis intro: * subspace_hyperplane)
    7.34 -    done
    7.35 -qed
    7.36 -
    7.37 -lemma dim_special_hyperplane:
    7.38 -  fixes k :: "'n::euclidean_space"
    7.39 -  shows "k \<in> Basis \<Longrightarrow> dim {x. k \<bullet> x = 0} = DIM('n) - 1"
    7.40 -apply (simp add: special_hyperplane_span)
    7.41 -apply (rule dim_unique [OF subset_refl])
    7.42 -apply (auto simp: independent_substdbasis)
    7.43 -apply (metis member_remove remove_def span_base)
    7.44 -done
    7.45 -
    7.46 -proposition dim_hyperplane:
    7.47 -  fixes a :: "'a::euclidean_space"
    7.48 -  assumes "a \<noteq> 0"
    7.49 -    shows "dim {x. a \<bullet> x = 0} = DIM('a) - 1"
    7.50 -proof -
    7.51 -  have span0: "span {x. a \<bullet> x = 0} = {x. a \<bullet> x = 0}"
    7.52 -    by (rule span_unique) (auto simp: subspace_hyperplane)
    7.53 -  then obtain B where "independent B"
    7.54 -              and Bsub: "B \<subseteq> {x. a \<bullet> x = 0}"
    7.55 -              and subspB: "{x. a \<bullet> x = 0} \<subseteq> span B"
    7.56 -              and card0: "(card B = dim {x. a \<bullet> x = 0})"
    7.57 -              and ortho: "pairwise orthogonal B"
    7.58 -    using orthogonal_basis_exists by metis
    7.59 -  with assms have "a \<notin> span B"
    7.60 -    by (metis (mono_tags, lifting) span_eq inner_eq_zero_iff mem_Collect_eq span0)
    7.61 -  then have ind: "independent (insert a B)"
    7.62 -    by (simp add: \<open>independent B\<close> independent_insert)
    7.63 -  have "finite B"
    7.64 -    using \<open>independent B\<close> independent_bound by blast
    7.65 -  have "UNIV \<subseteq> span (insert a B)"
    7.66 -  proof fix y::'a
    7.67 -    obtain r z where z: "y = r *\<^sub>R a + z" "a \<bullet> z = 0"
    7.68 -      apply (rule_tac r="(a \<bullet> y) / (a \<bullet> a)" and z = "y - ((a \<bullet> y) / (a \<bullet> a)) *\<^sub>R a" in that)
    7.69 -      using assms
    7.70 -      by (auto simp: algebra_simps)
    7.71 -    show "y \<in> span (insert a B)"
    7.72 -      by (metis (mono_tags, lifting) z Bsub span_eq_iff
    7.73 -         add_diff_cancel_left' mem_Collect_eq span0 span_breakdown_eq span_subspace subspB)
    7.74 -  qed
    7.75 -  then have dima: "DIM('a) = dim(insert a B)"
    7.76 -    by (metis independent_Basis span_Basis dim_eq_card top.extremum_uniqueI)
    7.77 -  then show ?thesis
    7.78 -    by (metis (mono_tags, lifting) Bsub Diff_insert_absorb \<open>a \<notin> span B\<close> ind card0
    7.79 -        card_Diff_singleton dim_span indep_card_eq_dim_span insertI1 subsetCE
    7.80 -        subspB)
    7.81 -qed
    7.82 -
    7.83 -lemma lowdim_eq_hyperplane:
    7.84 -  fixes S :: "'a::euclidean_space set"
    7.85 -  assumes "dim S = DIM('a) - 1"
    7.86 -  obtains a where "a \<noteq> 0" and "span S = {x. a \<bullet> x = 0}"
    7.87 -proof -
    7.88 -  have dimS: "dim S < DIM('a)"
    7.89 -    by (simp add: assms)
    7.90 -  then obtain b where b: "b \<noteq> 0" "span S \<subseteq> {a. b \<bullet> a = 0}"
    7.91 -    using lowdim_subset_hyperplane [of S] by fastforce
    7.92 -  show ?thesis
    7.93 -    apply (rule that[OF b(1)])
    7.94 -    apply (rule subspace_dim_equal)
    7.95 -    by (auto simp: assms b dim_hyperplane dim_span subspace_hyperplane
    7.96 -        subspace_span)
    7.97 -qed
    7.98 -
    7.99 -lemma dim_eq_hyperplane:
   7.100 -  fixes S :: "'n::euclidean_space set"
   7.101 -  shows "dim S = DIM('n) - 1 \<longleftrightarrow> (\<exists>a. a \<noteq> 0 \<and> span S = {x. a \<bullet> x = 0})"
   7.102 -by (metis One_nat_def dim_hyperplane dim_span lowdim_eq_hyperplane)
   7.103 -
   7.104  proposition aff_dim_eq_hyperplane:
   7.105    fixes S :: "'a::euclidean_space set"
   7.106    shows "aff_dim S = DIM('a) - 1 \<longleftrightarrow> (\<exists>a b. a \<noteq> 0 \<and> affine hull S = {x. a \<bullet> x = b})"
   7.107 @@ -6436,444 +6339,6 @@
   7.108    shows "aff_dim S < DIM('a) \<longleftrightarrow> (affine hull S \<noteq> UNIV)"
   7.109  by (metis (no_types) aff_dim_affine_hull aff_dim_le_DIM aff_dim_UNIV affine_hull_UNIV less_le)
   7.110  
   7.111 -
   7.112 -subsection\<open> Orthogonal bases, Gram-Schmidt process, and related theorems\<close>
   7.113 -
   7.114 -lemma pairwise_orthogonal_independent:
   7.115 -  assumes "pairwise orthogonal S" and "0 \<notin> S"
   7.116 -    shows "independent S"
   7.117 -proof -
   7.118 -  have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   7.119 -    using assms by (simp add: pairwise_def orthogonal_def)
   7.120 -  have "False" if "a \<in> S" and a: "a \<in> span (S - {a})" for a
   7.121 -  proof -
   7.122 -    obtain T U where "T \<subseteq> S - {a}" "a = (\<Sum>v\<in>T. U v *\<^sub>R v)"
   7.123 -      using a by (force simp: span_explicit)
   7.124 -    then have "a \<bullet> a = a \<bullet> (\<Sum>v\<in>T. U v *\<^sub>R v)"
   7.125 -      by simp
   7.126 -    also have "... = 0"
   7.127 -      apply (simp add: inner_sum_right)
   7.128 -      apply (rule comm_monoid_add_class.sum.neutral)
   7.129 -      by (metis "0" DiffE \<open>T \<subseteq> S - {a}\<close> mult_not_zero singletonI subsetCE \<open>a \<in> S\<close>)
   7.130 -    finally show ?thesis
   7.131 -      using \<open>0 \<notin> S\<close> \<open>a \<in> S\<close> by auto
   7.132 -  qed
   7.133 -  then show ?thesis
   7.134 -    by (force simp: dependent_def)
   7.135 -qed
   7.136 -
   7.137 -lemma pairwise_orthogonal_imp_finite:
   7.138 -  fixes S :: "'a::euclidean_space set"
   7.139 -  assumes "pairwise orthogonal S"
   7.140 -    shows "finite S"
   7.141 -proof -
   7.142 -  have "independent (S - {0})"
   7.143 -    apply (rule pairwise_orthogonal_independent)
   7.144 -     apply (metis Diff_iff assms pairwise_def)
   7.145 -    by blast
   7.146 -  then show ?thesis
   7.147 -    by (meson independent_imp_finite infinite_remove)
   7.148 -qed
   7.149 -
   7.150 -lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}"
   7.151 -  by (simp add: subspace_def orthogonal_clauses)
   7.152 -
   7.153 -lemma subspace_orthogonal_to_vectors: "subspace {y. \<forall>x \<in> S. orthogonal x y}"
   7.154 -  by (simp add: subspace_def orthogonal_clauses)
   7.155 -
   7.156 -lemma orthogonal_to_span:
   7.157 -  assumes a: "a \<in> span S" and x: "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
   7.158 -    shows "orthogonal x a"
   7.159 -  by (metis a orthogonal_clauses(1,2,4)
   7.160 -      span_induct_alt x)
   7.161 -
   7.162 -proposition Gram_Schmidt_step:
   7.163 -  fixes S :: "'a::euclidean_space set"
   7.164 -  assumes S: "pairwise orthogonal S" and x: "x \<in> span S"
   7.165 -    shows "orthogonal x (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b))"
   7.166 -proof -
   7.167 -  have "finite S"
   7.168 -    by (simp add: S pairwise_orthogonal_imp_finite)
   7.169 -  have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)) x"
   7.170 -       if "x \<in> S" for x
   7.171 -  proof -
   7.172 -    have "a \<bullet> x = (\<Sum>y\<in>S. if y = x then y \<bullet> a else 0)"
   7.173 -      by (simp add: \<open>finite S\<close> inner_commute sum.delta that)
   7.174 -    also have "... =  (\<Sum>b\<in>S. b \<bullet> a * (b \<bullet> x) / (b \<bullet> b))"
   7.175 -      apply (rule sum.cong [OF refl], simp)
   7.176 -      by (meson S orthogonal_def pairwise_def that)
   7.177 -   finally show ?thesis
   7.178 -     by (simp add: orthogonal_def algebra_simps inner_sum_left)
   7.179 -  qed
   7.180 -  then show ?thesis
   7.181 -    using orthogonal_to_span orthogonal_commute x by blast
   7.182 -qed
   7.183 -
   7.184 -
   7.185 -lemma orthogonal_extension_aux:
   7.186 -  fixes S :: "'a::euclidean_space set"
   7.187 -  assumes "finite T" "finite S" "pairwise orthogonal S"
   7.188 -    shows "\<exists>U. pairwise orthogonal (S \<union> U) \<and> span (S \<union> U) = span (S \<union> T)"
   7.189 -using assms
   7.190 -proof (induction arbitrary: S)
   7.191 -  case empty then show ?case
   7.192 -    by simp (metis sup_bot_right)
   7.193 -next
   7.194 -  case (insert a T)
   7.195 -  have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   7.196 -    using insert by (simp add: pairwise_def orthogonal_def)
   7.197 -  define a' where "a' = a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)"
   7.198 -  obtain U where orthU: "pairwise orthogonal (S \<union> insert a' U)"
   7.199 -             and spanU: "span (insert a' S \<union> U) = span (insert a' S \<union> T)"
   7.200 -    by (rule exE [OF insert.IH [of "insert a' S"]])
   7.201 -      (auto simp: Gram_Schmidt_step a'_def insert.prems orthogonal_commute
   7.202 -        pairwise_orthogonal_insert span_clauses)
   7.203 -  have orthS: "\<And>x. x \<in> S \<Longrightarrow> a' \<bullet> x = 0"
   7.204 -    apply (simp add: a'_def)
   7.205 -    using Gram_Schmidt_step [OF \<open>pairwise orthogonal S\<close>]
   7.206 -    apply (force simp: orthogonal_def inner_commute span_superset [THEN subsetD])
   7.207 -    done
   7.208 -  have "span (S \<union> insert a' U) = span (insert a' (S \<union> T))"
   7.209 -    using spanU by simp
   7.210 -  also have "... = span (insert a (S \<union> T))"
   7.211 -    apply (rule eq_span_insert_eq)
   7.212 -    apply (simp add: a'_def span_neg span_sum span_base span_mul)
   7.213 -    done
   7.214 -  also have "... = span (S \<union> insert a T)"
   7.215 -    by simp
   7.216 -  finally show ?case
   7.217 -    by (rule_tac x="insert a' U" in exI) (use orthU in auto)
   7.218 -qed
   7.219 -
   7.220 -
   7.221 -proposition orthogonal_extension:
   7.222 -  fixes S :: "'a::euclidean_space set"
   7.223 -  assumes S: "pairwise orthogonal S"
   7.224 -  obtains U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
   7.225 -proof -
   7.226 -  obtain B where "finite B" "span B = span T"
   7.227 -    using basis_subspace_exists [of "span T"] subspace_span by metis
   7.228 -  with orthogonal_extension_aux [of B S]
   7.229 -  obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> B)"
   7.230 -    using assms pairwise_orthogonal_imp_finite by auto
   7.231 -  with \<open>span B = span T\<close> show ?thesis
   7.232 -    by (rule_tac U=U in that) (auto simp: span_Un)
   7.233 -qed
   7.234 -
   7.235 -corollary%unimportant orthogonal_extension_strong:
   7.236 -  fixes S :: "'a::euclidean_space set"
   7.237 -  assumes S: "pairwise orthogonal S"
   7.238 -  obtains U where "U \<inter> (insert 0 S) = {}" "pairwise orthogonal (S \<union> U)"
   7.239 -                  "span (S \<union> U) = span (S \<union> T)"
   7.240 -proof -
   7.241 -  obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
   7.242 -    using orthogonal_extension assms by blast
   7.243 -  then show ?thesis
   7.244 -    apply (rule_tac U = "U - (insert 0 S)" in that)
   7.245 -      apply blast
   7.246 -     apply (force simp: pairwise_def)
   7.247 -    apply (metis Un_Diff_cancel Un_insert_left span_redundant span_zero)
   7.248 -    done
   7.249 -qed
   7.250 -
   7.251 -subsection\<open>Decomposing a vector into parts in orthogonal subspaces\<close>
   7.252 -
   7.253 -text\<open>existence of orthonormal basis for a subspace.\<close>
   7.254 -
   7.255 -lemma orthogonal_spanningset_subspace:
   7.256 -  fixes S :: "'a :: euclidean_space set"
   7.257 -  assumes "subspace S"
   7.258 -  obtains B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S"
   7.259 -proof -
   7.260 -  obtain B where "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S"
   7.261 -    using basis_exists by blast
   7.262 -  with orthogonal_extension [of "{}" B]
   7.263 -  show ?thesis
   7.264 -    by (metis Un_empty_left assms pairwise_empty span_superset span_subspace that)
   7.265 -qed
   7.266 -
   7.267 -lemma orthogonal_basis_subspace:
   7.268 -  fixes S :: "'a :: euclidean_space set"
   7.269 -  assumes "subspace S"
   7.270 -  obtains B where "0 \<notin> B" "B \<subseteq> S" "pairwise orthogonal B" "independent B"
   7.271 -                  "card B = dim S" "span B = S"
   7.272 -proof -
   7.273 -  obtain B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S"
   7.274 -    using assms orthogonal_spanningset_subspace by blast
   7.275 -  then show ?thesis
   7.276 -    apply (rule_tac B = "B - {0}" in that)
   7.277 -    apply (auto simp: indep_card_eq_dim_span pairwise_subset pairwise_orthogonal_independent elim: pairwise_subset)
   7.278 -    done
   7.279 -qed
   7.280 -
   7.281 -proposition orthonormal_basis_subspace:
   7.282 -  fixes S :: "'a :: euclidean_space set"
   7.283 -  assumes "subspace S"
   7.284 -  obtains B where "B \<subseteq> S" "pairwise orthogonal B"
   7.285 -              and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
   7.286 -              and "independent B" "card B = dim S" "span B = S"
   7.287 -proof -
   7.288 -  obtain B where "0 \<notin> B" "B \<subseteq> S"
   7.289 -             and orth: "pairwise orthogonal B"
   7.290 -             and "independent B" "card B = dim S" "span B = S"
   7.291 -    by (blast intro: orthogonal_basis_subspace [OF assms])
   7.292 -  have 1: "(\<lambda>x. x /\<^sub>R norm x) ` B \<subseteq> S"
   7.293 -    using \<open>span B = S\<close> span_superset span_mul by fastforce
   7.294 -  have 2: "pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` B)"
   7.295 -    using orth by (force simp: pairwise_def orthogonal_clauses)
   7.296 -  have 3: "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` B \<Longrightarrow> norm x = 1"
   7.297 -    by (metis (no_types, lifting) \<open>0 \<notin> B\<close> image_iff norm_sgn sgn_div_norm)
   7.298 -  have 4: "independent ((\<lambda>x. x /\<^sub>R norm x) ` B)"
   7.299 -    by (metis "2" "3" norm_zero pairwise_orthogonal_independent zero_neq_one)
   7.300 -  have "inj_on (\<lambda>x. x /\<^sub>R norm x) B"
   7.301 -  proof
   7.302 -    fix x y
   7.303 -    assume "x \<in> B" "y \<in> B" "x /\<^sub>R norm x = y /\<^sub>R norm y"
   7.304 -    moreover have "\<And>i. i \<in> B \<Longrightarrow> norm (i /\<^sub>R norm i) = 1"
   7.305 -      using 3 by blast
   7.306 -    ultimately show "x = y"
   7.307 -      by (metis norm_eq_1 orth orthogonal_clauses(7) orthogonal_commute orthogonal_def pairwise_def zero_neq_one)
   7.308 -  qed
   7.309 -  then have 5: "card ((\<lambda>x. x /\<^sub>R norm x) ` B) = dim S"
   7.310 -    by (metis \<open>card B = dim S\<close> card_image)
   7.311 -  have 6: "span ((\<lambda>x. x /\<^sub>R norm x) ` B) = S"
   7.312 -    by (metis "1" "4" "5" assms card_eq_dim independent_finite span_subspace)
   7.313 -  show ?thesis
   7.314 -    by (rule that [OF 1 2 3 4 5 6])
   7.315 -qed
   7.316 -
   7.317 -
   7.318 -proposition%unimportant orthogonal_to_subspace_exists_gen:
   7.319 -  fixes S :: "'a :: euclidean_space set"
   7.320 -  assumes "span S \<subset> span T"
   7.321 -  obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
   7.322 -proof -
   7.323 -  obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
   7.324 -             and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
   7.325 -             and "independent B" "card B = dim S" "span B = span S"
   7.326 -    by (rule orthonormal_basis_subspace [of "span S", OF subspace_span])
   7.327 -      (auto simp: dim_span)
   7.328 -  with assms obtain u where spanBT: "span B \<subseteq> span T" and "u \<notin> span B" "u \<in> span T"
   7.329 -    by auto
   7.330 -  obtain C where orthBC: "pairwise orthogonal (B \<union> C)" and spanBC: "span (B \<union> C) = span (B \<union> {u})"
   7.331 -    by (blast intro: orthogonal_extension [OF orthB])
   7.332 -  show thesis
   7.333 -  proof (cases "C \<subseteq> insert 0 B")
   7.334 -    case True
   7.335 -    then have "C \<subseteq> span B"
   7.336 -      using span_eq
   7.337 -      by (metis span_insert_0 subset_trans)
   7.338 -    moreover have "u \<in> span (B \<union> C)"
   7.339 -      using \<open>span (B \<union> C) = span (B \<union> {u})\<close> span_superset by force
   7.340 -    ultimately show ?thesis
   7.341 -      using True \<open>u \<notin> span B\<close>
   7.342 -      by (metis Un_insert_left span_insert_0 sup.orderE)
   7.343 -  next
   7.344 -    case False
   7.345 -    then obtain x where "x \<in> C" "x \<noteq> 0" "x \<notin> B"
   7.346 -      by blast
   7.347 -    then have "x \<in> span T"
   7.348 -      by (metis (no_types, lifting) Un_insert_right Un_upper2 \<open>u \<in> span T\<close> spanBT spanBC
   7.349 -          \<open>u \<in> span T\<close> insert_subset span_superset span_mono
   7.350 -          span_span subsetCE subset_trans sup_bot.comm_neutral)
   7.351 -    moreover have "orthogonal x y" if "y \<in> span B" for y
   7.352 -      using that
   7.353 -    proof (rule span_induct)
   7.354 -      show "subspace {a. orthogonal x a}"
   7.355 -        by (simp add: subspace_orthogonal_to_vector)
   7.356 -      show "\<And>b. b \<in> B \<Longrightarrow> orthogonal x b"
   7.357 -        by (metis Un_iff \<open>x \<in> C\<close> \<open>x \<notin> B\<close> orthBC pairwise_def)
   7.358 -    qed
   7.359 -    ultimately show ?thesis
   7.360 -      using \<open>x \<noteq> 0\<close> that \<open>span B = span S\<close> by auto
   7.361 -  qed
   7.362 -qed
   7.363 -
   7.364 -corollary%unimportant orthogonal_to_subspace_exists:
   7.365 -  fixes S :: "'a :: euclidean_space set"
   7.366 -  assumes "dim S < DIM('a)"
   7.367 -  obtains x where "x \<noteq> 0" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
   7.368 -proof -
   7.369 -have "span S \<subset> UNIV"
   7.370 -  by (metis (mono_tags) UNIV_I assms inner_eq_zero_iff less_le lowdim_subset_hyperplane
   7.371 -      mem_Collect_eq top.extremum_strict top.not_eq_extremum)
   7.372 -  with orthogonal_to_subspace_exists_gen [of S UNIV] that show ?thesis
   7.373 -    by (auto simp: span_UNIV)
   7.374 -qed
   7.375 -
   7.376 -corollary%unimportant orthogonal_to_vector_exists:
   7.377 -  fixes x :: "'a :: euclidean_space"
   7.378 -  assumes "2 \<le> DIM('a)"
   7.379 -  obtains y where "y \<noteq> 0" "orthogonal x y"
   7.380 -proof -
   7.381 -  have "dim {x} < DIM('a)"
   7.382 -    using assms by auto
   7.383 -  then show thesis
   7.384 -    by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that)
   7.385 -qed
   7.386 -
   7.387 -proposition%unimportant orthogonal_subspace_decomp_exists:
   7.388 -  fixes S :: "'a :: euclidean_space set"
   7.389 -  obtains y z
   7.390 -  where "y \<in> span S"
   7.391 -    and "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w"
   7.392 -    and "x = y + z"
   7.393 -proof -
   7.394 -  obtain T where "0 \<notin> T" "T \<subseteq> span S" "pairwise orthogonal T" "independent T"
   7.395 -    "card T = dim (span S)" "span T = span S"
   7.396 -    using orthogonal_basis_subspace subspace_span by blast
   7.397 -  let ?a = "\<Sum>b\<in>T. (b \<bullet> x / (b \<bullet> b)) *\<^sub>R b"
   7.398 -  have orth: "orthogonal (x - ?a) w" if "w \<in> span S" for w
   7.399 -    by (simp add: Gram_Schmidt_step \<open>pairwise orthogonal T\<close> \<open>span T = span S\<close>
   7.400 -        orthogonal_commute that)
   7.401 -  show ?thesis
   7.402 -    apply (rule_tac y = "?a" and z = "x - ?a" in that)
   7.403 -      apply (meson \<open>T \<subseteq> span S\<close> span_scale span_sum subsetCE)
   7.404 -     apply (fact orth, simp)
   7.405 -    done
   7.406 -qed
   7.407 -
   7.408 -lemma orthogonal_subspace_decomp_unique:
   7.409 -  fixes S :: "'a :: euclidean_space set"
   7.410 -  assumes "x + y = x' + y'"
   7.411 -      and ST: "x \<in> span S" "x' \<in> span S" "y \<in> span T" "y' \<in> span T"
   7.412 -      and orth: "\<And>a b. \<lbrakk>a \<in> S; b \<in> T\<rbrakk> \<Longrightarrow> orthogonal a b"
   7.413 -  shows "x = x' \<and> y = y'"
   7.414 -proof -
   7.415 -  have "x + y - y' = x'"
   7.416 -    by (simp add: assms)
   7.417 -  moreover have "\<And>a b. \<lbrakk>a \<in> span S; b \<in> span T\<rbrakk> \<Longrightarrow> orthogonal a b"
   7.418 -    by (meson orth orthogonal_commute orthogonal_to_span)
   7.419 -  ultimately have "0 = x' - x"
   7.420 -    by (metis (full_types) add_diff_cancel_left' ST diff_right_commute orthogonal_clauses(10) orthogonal_clauses(5) orthogonal_self)
   7.421 -  with assms show ?thesis by auto
   7.422 -qed
   7.423 -
   7.424 -lemma vector_in_orthogonal_spanningset:
   7.425 -  fixes a :: "'a::euclidean_space"
   7.426 -  obtains S where "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
   7.427 -  by (metis UNIV_I Un_iff empty_iff insert_subset orthogonal_extension pairwise_def
   7.428 -      pairwise_orthogonal_insert span_UNIV subsetI subset_antisym)
   7.429 -
   7.430 -lemma vector_in_orthogonal_basis:
   7.431 -  fixes a :: "'a::euclidean_space"
   7.432 -  assumes "a \<noteq> 0"
   7.433 -  obtains S where "a \<in> S" "0 \<notin> S" "pairwise orthogonal S" "independent S" "finite S"
   7.434 -                  "span S = UNIV" "card S = DIM('a)"
   7.435 -proof -
   7.436 -  obtain S where S: "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
   7.437 -    using vector_in_orthogonal_spanningset .
   7.438 -  show thesis
   7.439 -  proof
   7.440 -    show "pairwise orthogonal (S - {0})"
   7.441 -      using pairwise_mono S(2) by blast
   7.442 -    show "independent (S - {0})"
   7.443 -      by (simp add: \<open>pairwise orthogonal (S - {0})\<close> pairwise_orthogonal_independent)
   7.444 -    show "finite (S - {0})"
   7.445 -      using \<open>independent (S - {0})\<close> independent_finite by blast
   7.446 -    show "card (S - {0}) = DIM('a)"
   7.447 -      using span_delete_0 [of S] S
   7.448 -      by (simp add: \<open>independent (S - {0})\<close> indep_card_eq_dim_span dim_UNIV)
   7.449 -  qed (use S \<open>a \<noteq> 0\<close> in auto)
   7.450 -qed
   7.451 -
   7.452 -lemma vector_in_orthonormal_basis:
   7.453 -  fixes a :: "'a::euclidean_space"
   7.454 -  assumes "norm a = 1"
   7.455 -  obtains S where "a \<in> S" "pairwise orthogonal S" "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
   7.456 -    "independent S" "card S = DIM('a)" "span S = UNIV"
   7.457 -proof -
   7.458 -  have "a \<noteq> 0"
   7.459 -    using assms by auto
   7.460 -  then obtain S where "a \<in> S" "0 \<notin> S" "finite S"
   7.461 -          and S: "pairwise orthogonal S" "independent S" "span S = UNIV" "card S = DIM('a)"
   7.462 -    by (metis vector_in_orthogonal_basis)
   7.463 -  let ?S = "(\<lambda>x. x /\<^sub>R norm x) ` S"
   7.464 -  show thesis
   7.465 -  proof
   7.466 -    show "a \<in> ?S"
   7.467 -      using \<open>a \<in> S\<close> assms image_iff by fastforce
   7.468 -  next
   7.469 -    show "pairwise orthogonal ?S"
   7.470 -      using \<open>pairwise orthogonal S\<close> by (auto simp: pairwise_def orthogonal_def)
   7.471 -    show "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` S \<Longrightarrow> norm x = 1"
   7.472 -      using \<open>0 \<notin> S\<close> by (auto simp: divide_simps)
   7.473 -    then show "independent ?S"
   7.474 -      by (metis \<open>pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` S)\<close> norm_zero pairwise_orthogonal_independent zero_neq_one)
   7.475 -    have "inj_on (\<lambda>x. x /\<^sub>R norm x) S"
   7.476 -      unfolding inj_on_def
   7.477 -      by (metis (full_types) S(1) \<open>0 \<notin> S\<close> inverse_nonzero_iff_nonzero norm_eq_zero orthogonal_scaleR orthogonal_self pairwise_def)
   7.478 -    then show "card ?S = DIM('a)"
   7.479 -      by (simp add: card_image S)
   7.480 -    show "span ?S = UNIV"
   7.481 -      by (metis (no_types) \<open>0 \<notin> S\<close> \<open>finite S\<close> \<open>span S = UNIV\<close>
   7.482 -          field_class.field_inverse_zero inverse_inverse_eq less_irrefl span_image_scale
   7.483 -          zero_less_norm_iff)
   7.484 -  qed
   7.485 -qed
   7.486 -
   7.487 -proposition dim_orthogonal_sum:
   7.488 -  fixes A :: "'a::euclidean_space set"
   7.489 -  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   7.490 -    shows "dim(A \<union> B) = dim A + dim B"
   7.491 -proof -
   7.492 -  have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   7.493 -    by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms)
   7.494 -  have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   7.495 -    using 1 by (simp add: span_induct [OF _ subspace_hyperplane])
   7.496 -  then have 0: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   7.497 -    by simp
   7.498 -  have "dim(A \<union> B) = dim (span (A \<union> B))"
   7.499 -    by (simp add: dim_span)
   7.500 -  also have "span (A \<union> B) = ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
   7.501 -    by (auto simp add: span_Un image_def)
   7.502 -  also have "dim \<dots> = dim {x + y |x y. x \<in> span A \<and> y \<in> span B}"
   7.503 -    by (auto intro!: arg_cong [where f=dim])
   7.504 -  also have "... = dim {x + y |x y. x \<in> span A \<and> y \<in> span B} + dim(span A \<inter> span B)"
   7.505 -    by (auto simp: dest: 0)
   7.506 -  also have "... = dim (span A) + dim (span B)"
   7.507 -    by (rule dim_sums_Int) (auto simp: subspace_span)
   7.508 -  also have "... = dim A + dim B"
   7.509 -    by (simp add: dim_span)
   7.510 -  finally show ?thesis .
   7.511 -qed
   7.512 -
   7.513 -lemma dim_subspace_orthogonal_to_vectors:
   7.514 -  fixes A :: "'a::euclidean_space set"
   7.515 -  assumes "subspace A" "subspace B" "A \<subseteq> B"
   7.516 -    shows "dim {y \<in> B. \<forall>x \<in> A. orthogonal x y} + dim A = dim B"
   7.517 -proof -
   7.518 -  have "dim (span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)) = dim (span B)"
   7.519 -  proof (rule arg_cong [where f=dim, OF subset_antisym])
   7.520 -    show "span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A) \<subseteq> span B"
   7.521 -      by (simp add: \<open>A \<subseteq> B\<close> Collect_restrict span_mono)
   7.522 -  next
   7.523 -    have *: "x \<in> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)"
   7.524 -         if "x \<in> B" for x
   7.525 -    proof -
   7.526 -      obtain y z where "x = y + z" "y \<in> span A" and orth: "\<And>w. w \<in> span A \<Longrightarrow> orthogonal z w"
   7.527 -        using orthogonal_subspace_decomp_exists [of A x] that by auto
   7.528 -      have "y \<in> span B"
   7.529 -        using \<open>y \<in> span A\<close> assms(3) span_mono by blast
   7.530 -      then have "z \<in> {a \<in> B. \<forall>x. x \<in> A \<longrightarrow> orthogonal x a}"
   7.531 -        apply simp
   7.532 -        using \<open>x = y + z\<close> assms(1) assms(2) orth orthogonal_commute span_add_eq
   7.533 -          span_eq_iff that by blast
   7.534 -      then have z: "z \<in> span {y \<in> B. \<forall>x\<in>A. orthogonal x y}"
   7.535 -        by (meson span_superset subset_iff)
   7.536 -      then show ?thesis
   7.537 -        apply (auto simp: span_Un image_def  \<open>x = y + z\<close> \<open>y \<in> span A\<close>)
   7.538 -        using \<open>y \<in> span A\<close> add.commute by blast
   7.539 -    qed
   7.540 -    show "span B \<subseteq> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)"
   7.541 -      by (rule span_minimal)
   7.542 -        (auto intro: * span_minimal simp: subspace_span)
   7.543 -  qed
   7.544 -  then show ?thesis
   7.545 -    by (metis (no_types, lifting) dim_orthogonal_sum dim_span mem_Collect_eq
   7.546 -        orthogonal_commute orthogonal_def)
   7.547 -qed
   7.548 -
   7.549  lemma aff_dim_openin:
   7.550    fixes S :: "'a::euclidean_space set"
   7.551    assumes ope: "openin (subtopology euclidean T) S" and "affine T" "S \<noteq> {}"