author immler Wed Jan 16 18:14:02 2019 -0500 (18 months ago) changeset 69675 880ab0f27ddf 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 file | annotate | diff | revisions src/HOL/Analysis/Change_Of_Vars.thy file | annotate | diff | revisions src/HOL/Analysis/Convex.thy file | annotate | diff | revisions src/HOL/Analysis/Cross3.thy file | annotate | diff | revisions src/HOL/Analysis/Determinants.thy file | annotate | diff | revisions src/HOL/Analysis/Linear_Algebra.thy file | annotate | diff | revisions src/HOL/Analysis/Starlike.thy file | annotate | diff | revisions
```     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.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.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.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.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.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.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.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.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.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.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.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.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> {}"
```