# HG changeset patch # User paulson # Date 1524667008 -3600 # Node ID 67b39890158c617e3187afa7125e1bed87f6f6c8 # Parent 6d7cc6723978c2e4e51bcb2a583cc2a117c45f78# Parent 20b713cff87afcd1f1177f1d123bd54b92373988 merged diff -r 6d7cc6723978 -r 67b39890158c src/HOL/Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Apr 25 13:29:21 2018 +0000 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Apr 25 15:36:48 2018 +0100 @@ -1,3 +1,7 @@ +(* Title: HOL/Analysis/Cartesian_Euclidean_Space.thy + Some material by Tim Makarios and L C Paulson +*) + section \Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space\ theory Cartesian_Euclidean_Space @@ -526,6 +530,12 @@ definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\ i. ((A$i)$j))" definition "rows(A::'a^'n^'m) = { row i A | i. i \ (UNIV :: 'm set)}" definition "columns(A::'a^'n^'m) = { column i A | i. i \ (UNIV :: 'n set)}" + +lemma times0_left [simp]: "(0::'a::semiring_1^'n^'m) ** (A::'a ^'p^'n) = 0" + by (simp add: matrix_matrix_mult_def zero_vec_def) + +lemma times0_right [simp]: "(A::'a::semiring_1^'n^'m) ** (0::'a ^'p^'n) = 0" + by (simp add: matrix_matrix_mult_def zero_vec_def) lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def) lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)" @@ -562,6 +572,16 @@ apply simp done +lemma scalar_matrix_assoc: + fixes A :: "real^'m^'n" + shows "k *\<^sub>R (A ** B) = (k *\<^sub>R A) ** B" + by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff) + +lemma matrix_scalar_ac: + fixes A :: "real^'m^'n" + shows "A ** (k *\<^sub>R B) = k *\<^sub>R A ** B" + by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff) + lemma matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)" apply (vector matrix_vector_mult_def mat_def) apply (simp add: if_distrib cond_application_beta sum.delta' cong del: if_weak_cong) @@ -615,6 +635,13 @@ lemma columns_transpose [simp]: "columns(transpose (A::'a::semiring_1^_^_)) = rows A" by (metis transpose_transpose rows_transpose) +lemma transpose_scalar: "transpose (k *\<^sub>R A) = k *\<^sub>R transpose A" + unfolding transpose_def + by (simp add: vec_eq_iff) + +lemma transpose_iff [iff]: "transpose A = transpose B \ A = B" + by (metis transpose_transpose) + lemma matrix_mult_transpose_dot_column: fixes A :: "real^'n^'n" shows "transpose A ** A = (\ i j. (column i A) \ (column j A))" @@ -762,6 +789,62 @@ shows "inj (( *v) A)" by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid) +lemma scalar_invertible: + fixes A :: "real^'m^'n" + assumes "k \ 0" and "invertible A" + shows "invertible (k *\<^sub>R A)" +proof - + obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1" + using assms unfolding invertible_def by auto + with `k \ 0` + have "(k *\<^sub>R A) ** ((1/k) *\<^sub>R A') = mat 1" "((1/k) *\<^sub>R A') ** (k *\<^sub>R A) = mat 1" + by (simp_all add: assms matrix_scalar_ac) + thus "invertible (k *\<^sub>R A)" + unfolding invertible_def by auto +qed + +lemma scalar_invertible_iff: + fixes A :: "real^'m^'n" + assumes "k \ 0" and "invertible A" + shows "invertible (k *\<^sub>R A) \ k \ 0 \ invertible A" + by (simp add: assms scalar_invertible) + +lemma vector_transpose_matrix [simp]: "x v* transpose A = A *v x" + unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def + by simp + +lemma transpose_matrix_vector [simp]: "transpose A *v x = x v* A" + unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def + by simp + +lemma vector_matrix_mul_rid: + fixes v :: "('a::semiring_1)^'n" + shows "v v* mat 1 = v" + by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix) + +lemma scalar_vector_matrix_assoc: + fixes k :: real and x :: "real^'n" and A :: "real^'m^'n" + shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)" + by (metis matrix_vector_mult_scaleR transpose_matrix_vector) + +lemma vector_scalar_matrix_ac: + fixes k :: real and x :: "real^'n" and A :: "real^'m^'n" + shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)" +proof - + have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A" + unfolding vector_matrix_mult_def + by (simp add: algebra_simps) + with scalar_vector_matrix_assoc + show "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)" + by auto +qed + +lemma vector_matrix_left_distrib: + fixes x y :: "real^'n" and A :: "real^'m^'n" + shows "(x + y) v* A = x v* A + y v* A" + unfolding vector_matrix_mult_def + by (simp add: algebra_simps sum.distrib vec_eq_iff) + subsection\Some bounds on components etc. relative to operator norm\ @@ -1075,11 +1158,7 @@ { fix A A' :: "real ^'n^'n" assume AA': "A ** A' = mat 1" have sA: "surj (( *v) A)" - unfolding surj_def - apply clarify - apply (rule_tac x="(A' *v y)" in exI) - apply (simp add: matrix_vector_mul_assoc AA' matrix_vector_mul_lid) - done + using AA' matrix_right_invertible_surjective by auto from linear_surjective_isomorphism[OF matrix_vector_mul_linear sA] obtain f' :: "real ^'n \ real ^'n" where f': "linear f'" "\x. f' (A *v x) = x" "\x. A *v f' x = x" by blast @@ -1095,6 +1174,18 @@ then show ?thesis by blast qed +lemma invertible_mult: + fixes A B :: "real^'n^'n" + assumes "invertible A" and "invertible B" + shows "invertible (A ** B)" + by (metis (no_types, hide_lams) assms invertible_def matrix_left_right_inverse matrix_mul_assoc matrix_mul_lid) + +lemma transpose_invertible: + fixes A :: "real^'n^'n" + assumes "invertible A" + shows "invertible (transpose A)" + by (meson assms invertible_def matrix_left_right_inverse right_invertible_transpose) + text \Considering an n-element vector as an n-by-1 or 1-by-n matrix.\ definition "rowvector v = (\ i j. (v$j))"