diff --git a/metadata/entries/Commuting_Hermitian.toml b/metadata/entries/Commuting_Hermitian.toml new file mode 100644 --- /dev/null +++ b/metadata/entries/Commuting_Hermitian.toml @@ -0,0 +1,36 @@ +title = "Simultaneous diagonalization of pairwise commuting Hermitian matrices" +date = 2022-07-18 +topics = [ + "Mathematics/Algebra", +] +abstract = """ +A Hermitian matrix is a square complex matrix that is equal to its +conjugate transpose. The (finite-dimensional) spectral theorem states +that any such matrix can be decomposed into a product of a unitary +matrix and a diagonal matrix containing only real elements. We +formalize the generalization of this result, which states that any +finite set of Hermitian and pairwise commuting matrices can be +decomposed as previously, using the same unitary matrix; in other +words, they are simultaneously diagonalizable. Sets of pairwise +commuting Hermitian matrices are called Complete Sets of +Commuting Observables in Quantum Mechanics, where they represent +physical quantities that can be simultaneously measured to uniquely +distinguish quantum states.""" +license = "bsd" +note = "" + +[authors] + +[authors.echenim] +homepage = "echenim_homepage" + +[contributors] + +[notify] +echenim = "echenim_email" + +[history] + +[extra] + +[related] diff --git a/thys/Commuting_Hermitian/Commuting_Hermitian.thy b/thys/Commuting_Hermitian/Commuting_Hermitian.thy new file mode 100644 --- /dev/null +++ b/thys/Commuting_Hermitian/Commuting_Hermitian.thy @@ -0,0 +1,3721 @@ +(* +Author: + Mnacho Echenim, Université Grenoble Alpes +*) + +theory Commuting_Hermitian imports Spectral_Theory_Complements Commuting_Hermitian_Misc +"Projective_Measurements.Linear_Algebra_Complements" +"Projective_Measurements.Projective_Measurements" begin + +section \Additional results on block decompositions of matrices\ + +subsection \Split block results\ + +lemma split_block_diag_carrier: + assumes "D \ carrier_mat n n" + and "a \ n" + and "split_block D a a = (D1, D2, D3, D4)" +shows "D1\ carrier_mat a a" "D4\ carrier_mat (n-a) (n-a)" +proof - + show "D1\ carrier_mat a a" using assms unfolding split_block_def + by (metis Pair_inject mat_carrier) + show "D4 \ carrier_mat (n-a) (n-a)" using assms unfolding split_block_def + by (metis Pair_inject carrier_matD(1) carrier_matD(2) mat_carrier) +qed + +lemma split_block_diagonal: + assumes "diagonal_mat D" + and "D \ carrier_mat n n" +and "a \ n" +and "split_block D a a = (D1, D2, D3, D4)" +shows "diagonal_mat D1 \ diagonal_mat D4" unfolding diagonal_mat_def +proof (intro allI conjI impI) + have "D1 \ carrier_mat a a" using assms unfolding split_block_def Let_def + by fastforce + fix i j + assume "i < dim_row D1" + and "j < dim_col D1" + and "i \ j" + have "D1 $$ (i,j) = D $$(i,j)" using assms unfolding split_block_def Let_def + using \i < dim_row D1\ \j < dim_col D1\ by fastforce + also have "... = 0" using assms \i \ j\ \D1 \ carrier_mat a a\ + \i < dim_row D1\ \j < dim_col D1\ unfolding diagonal_mat_def by fastforce + finally show "D1 $$(i,j) = 0" . +next + have "D4 \ carrier_mat (n-a) (n-a)" using assms + unfolding split_block_def Let_def by fastforce + fix i j + assume "i < dim_row D4" + and "j < dim_col D4" + and "i \ j" + have "D4 $$ (i,j) = D $$(i + a,j + a)" using assms unfolding split_block_def Let_def + using \i < dim_row D4\ \j < dim_col D4\ by fastforce + also have "... = 0" using assms \i \ j\ \D4 \ carrier_mat (n-a) (n-a)\ + \i < dim_row D4\ \j < dim_col D4\ unfolding diagonal_mat_def by fastforce + finally show "D4 $$(i,j) = 0" . +qed + +lemma split_block_times_diag_index: + fixes B::"'a::comm_ring Matrix.mat" + assumes "diagonal_mat D" + and "D\ carrier_mat n n" + and "B\ carrier_mat n n" + and "a \ n" + and "split_block B a a = (B1, B2, B3, B4)" + and "split_block D a a = (D1, D2, D3, D4)" + and "i < dim_row (D4 * B4)" + and "j < dim_col (D4 * B4)" +shows "(B4 * D4) $$ (i, j) = (B*D) $$ (i+a, j+a)" + "(D4 * B4) $$ (i, j) = (D*B) $$ (i+a, j+a)" +proof - + have d4: "D4 \ carrier_mat (n-a) (n-a)" using assms + split_block(4)[of D] by simp + have b4: "B4 \ carrier_mat (n-a) (n-a)" using assms + split_block(4)[of B] by simp + have "diagonal_mat D4" using assms split_block_diagonal[of D] by blast + have "i < n-a" using \i < dim_row (D4 * B4)\ b4 d4 by simp + have "j < n-a" using \j < dim_col (D4 * B4)\ b4 d4 by simp + have "(B4 * D4) $$ (i, j) = D4 $$ (j,j) * B4 $$ (i,j)" + proof (rule diagonal_mat_mult_index') + show "diagonal_mat D4" using \diagonal_mat D4\ . + show "B4 \ carrier_mat (n-a) (n-a)" using b4 . + show "D4 \ carrier_mat (n - a) (n - a)" using d4 . + show "i < n-a" using \i < n-a\ . + show "j < n-a" using \j < n-a\ . + qed + also have "... = D $$ (j+a, j+a) * B $$ (i+a, j+a)" + using assms \i < n-a\ \j < n-a\ + unfolding split_block_def Let_def by fastforce + also have "... = (B*D) $$ (i+a, j+a)" using diagonal_mat_mult_index' assms + by (metis \i < n - a\ \j < n - a\ less_diff_conv) + finally show "(B4 * D4) $$ (i, j) = (B*D) $$ (i+a, j+a)" . + have "(D4 * B4) $$ (i, j) = D4 $$ (i,i) * B4 $$ (i,j)" + using diagonal_mat_mult_index \diagonal_mat D4\ \i < n - a\ \j < n - a\ b4 d4 + by blast + also have "... = D $$ (i+a, i+a) * B $$ (i+a, j+a)" + using assms \i < n-a\ \j < n-a\ + unfolding split_block_def Let_def by fastforce + also have "... = (D*B) $$ (i+a, j+a)" using diagonal_mat_mult_index assms + by (metis \i < n - a\ \j < n - a\ less_diff_conv) + finally show "(D4 * B4) $$ (i, j) = (D*B) $$ (i+a, j+a)" . +qed + +lemma split_block_commute_subblock: + fixes B::"'a::comm_ring Matrix.mat" + assumes "diagonal_mat D" + and "D\ carrier_mat n n" + and "B\ carrier_mat n n" + and "a \ n" + and "split_block B a a = (B1, B2, B3, B4)" + and "split_block D a a = (D1, D2, D3, D4)" + and "B * D = D * B" +shows "B4 * D4 = D4 * B4" +proof + have d4: "D4 \ carrier_mat (n-a) (n-a)" using assms + split_block(4)[of D] by simp + have b4: "B4 \ carrier_mat (n-a) (n-a)" using assms + split_block(4)[of B] by simp + have "diagonal_mat D4" using assms split_block_diagonal[of D] by blast + show "dim_row (B4 * D4) = dim_row (D4 * B4)" using d4 b4 by simp + show "dim_col (B4 * D4) = dim_col (D4 * B4)" using d4 b4 by simp + fix i j + assume "i < dim_row (D4 * B4)" + and "j < dim_col (D4 * B4)" + have "(B4*D4) $$(i,j) = (B*D) $$(i+a, j+a)" + using split_block_times_diag_index[of D n B a] assms + \i < dim_row (D4 * B4)\ \j < dim_col (D4 * B4)\ by blast + also have "... = (D*B) $$ (i+a, j+a)" using assms by simp + also have "... = (D4*B4) $$ (i, j)" + using split_block_times_diag_index[of D n B a] assms + by (metis \i < dim_row (D4 * B4)\ \j < dim_col (D4 * B4)\) + finally show "(B4*D4) $$(i,j) = (D4*B4) $$ (i, j)" . +qed + +lemma commute_diag_mat_zero_comp: + fixes D::"'a::{field} Matrix.mat" + assumes "diagonal_mat D" + and "D\ carrier_mat n n" + and "B\ carrier_mat n n" + and" B* D = D * B" + and "i < n" + and "j < n" + and "D$$(i,i) \ D$$(j,j)" +shows "B $$(i,j) = 0" +proof - + have "B$$(i,j) * D$$(j,j) = (B*D) $$(i,j)" + using diagonal_mat_mult_index'[of B n D] assms by simp + also have "... = (D*B) $$ (i,j)" using assms by simp + also have "... = B$$(i,j) * D$$(i,i)" + using diagonal_mat_mult_index assms + by (metis Groups.mult_ac(2)) + finally have "B$$(i,j) * D$$(j,j) = B$$(i,j) * D$$(i,i)" . + hence "B$$(i,j) * (D$$(j,j) - D$$(i,i)) = 0" by auto + thus "B$$(i,j) = 0" using assms by simp +qed + +lemma commute_diag_mat_split_block: + fixes D::"'a::{field} Matrix.mat" + assumes "diagonal_mat D" + and "D\ carrier_mat n n" + and "B\ carrier_mat n n" + and" B* D = D * B" + and "k \ n" + and "\i j. (i < k \ k \ j \ j < n) \ D$$(i,i) \ D$$(j,j)" + and "(B1, B2, B3, B4) = split_block B k k" +shows "B2 = 0\<^sub>m k (n-k)" "B3 = 0\<^sub>m (n-k) k" +proof (intro eq_matI) + show "dim_row B2 = dim_row (0\<^sub>m k (n - k))" + using assms unfolding split_block_def Let_def by simp + show "dim_col B2 = dim_col (0\<^sub>m k (n - k))" + using assms unfolding split_block_def Let_def by simp + fix i j + assume "i < dim_row (0\<^sub>m k (n - k))" + and "j < dim_col (0\<^sub>m k (n - k))" note ijprop = this + have "B2 $$ (i, j) = B $$ (i, j+k)" using assms ijprop + unfolding split_block_def Let_def by simp + also have "... = 0" + proof (rule commute_diag_mat_zero_comp[of D n], (auto simp add: assms)) + show "i < n" using ijprop assms by simp + show "j + k < n" using ijprop assms by simp + show "D $$ (i, i) = D $$ (j + k, j + k) \ False" using ijprop assms + by (metis \j + k < n\ index_zero_mat(2) le_add2) + qed + finally show "B2 $$ (i, j) = 0\<^sub>m k (n - k) $$ (i, j)" using ijprop by simp +next + show "B3 = 0\<^sub>m (n-k) k" + proof (intro eq_matI) + show "dim_row B3 = dim_row (0\<^sub>m (n - k) k)" + using assms unfolding split_block_def Let_def by simp + show "dim_col B3 = dim_col (0\<^sub>m (n - k) k)" + using assms unfolding split_block_def Let_def by simp + fix i j + assume "i < dim_row (0\<^sub>m (n - k) k)" + and "j < dim_col (0\<^sub>m (n - k) k)" note ijprop = this + have "B3 $$ (i, j) = B $$ (i+k, j)" using assms ijprop + unfolding split_block_def Let_def by simp + also have "... = 0" + proof (rule commute_diag_mat_zero_comp[of D n], (auto simp add: assms)) + show "i + k < n" using ijprop assms by simp + show "j < n" using ijprop assms by simp + show "D $$ (i+k, i+k) = D $$ (j, j) \ False" using ijprop assms + by (metis \i + k < n\ index_zero_mat(3) le_add2) + qed + finally show "B3 $$ (i, j) = 0\<^sub>m (n - k) k $$ (i, j)" using ijprop by simp + qed +qed + +lemma split_block_hermitian_1: + assumes "hermitian A" + and "n \ dim_row A" +and "(A1, A2, A3, A4) = split_block A n n" +shows "hermitian A1" unfolding hermitian_def +proof (rule eq_matI, auto) + have "dim_row A = dim_col A" using assms + by (metis carrier_matD(2) hermitian_square) + show "dim_col A1 = dim_row A1" using assms unfolding split_block_def Let_def + by simp + thus "dim_row A1 = dim_col A1" by simp + show "\i j. i < dim_row A1 \ j < dim_col A1 \ + Complex_Matrix.adjoint A1 $$ (i, j) = A1 $$ (i, j)" + proof - + fix i j + assume "i < dim_row A1" and "j < dim_col A1" note ij = this + have r: "dim_row A1 = n" using assms unfolding split_block_def Let_def + by simp + have c: "dim_col A1 = n" using assms unfolding split_block_def Let_def + by simp + have "Complex_Matrix.adjoint A1 $$ (i, j) = conjugate (A1 $$ (j,i))" + using ij r c unfolding Complex_Matrix.adjoint_def by simp + also have "... = conjugate (A $$ (j,i))" using assms ij r c + unfolding split_block_def Let_def by simp + also have "... = A $$ (i,j)" using assms ij r c \dim_row A = dim_col A\ + unfolding hermitian_def Complex_Matrix.adjoint_def + by (metis adjoint_eval assms(1) hermitian_def order_less_le_trans) + also have "... = A1 $$(i,j)" using assms ij r c + unfolding split_block_def Let_def by simp + finally show "Complex_Matrix.adjoint A1 $$ (i, j) = A1 $$ (i, j)" . + qed +qed + +lemma split_block_hermitian_4: + assumes "hermitian A" + and "n \ dim_row A" +and "(A1, A2, A3, A4) = split_block A n n" +shows "hermitian A4" unfolding hermitian_def +proof (rule eq_matI, auto) + have arc: "dim_row A = dim_col A" using assms + by (metis carrier_matD(2) hermitian_square) + thus "dim_col A4 = dim_row A4" using assms unfolding split_block_def Let_def + by simp + thus "dim_row A4 = dim_col A4" by simp + show "\i j. i < dim_row A4 \ j < dim_col A4 \ + Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)" + proof - + fix i j + assume "i < dim_row A4" and "j < dim_col A4" note ij = this + have r: "dim_row A4 = dim_row A - n" using assms + unfolding split_block_def Let_def by simp + have c: "dim_col A4 = dim_col A - n" using assms + unfolding split_block_def Let_def by simp + have "Complex_Matrix.adjoint A4 $$ (i, j) = conjugate (A4 $$ (j,i))" + using ij r c arc unfolding Complex_Matrix.adjoint_def by simp + also have "... = conjugate (A $$ (j +n ,i+n))" using assms ij r c arc + unfolding split_block_def Let_def by simp + also have "... = A $$ (i+n,j+n)" using assms ij r c arc + unfolding hermitian_def Complex_Matrix.adjoint_def + by (metis index_mat(1) less_diff_conv split_conv) + also have "... = A4 $$(i,j)" using assms ij r c + unfolding split_block_def Let_def by simp + finally show "Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)" . + qed +qed + +lemma diag_block_split_block: + assumes "B\ carrier_mat n n" + and "k < n" + and "(B1, B2, B3, B4) = split_block B k k" + and "B2 = 0\<^sub>m k (n-k)" + and "B3 = 0\<^sub>m (n-k) k" +shows "B = diag_block_mat [B1,B4]" +proof - + have dr: "dim_row B = k + (n-k)" using assms by simp + have dc: "dim_col B = k + (n-k)" using assms by simp + have c1: "B1 \ carrier_mat k k" using assms + split_block(1)[of B, OF _ dr dc] by metis + have c4: "B4 \ carrier_mat (n-k) (n-k)" using assms + split_block(4)[of B, OF _ dr dc] by metis + have d4: "diag_block_mat [B4] = B4" using diag_block_mat_singleton[of B4] + by simp + have "B = four_block_mat B1 B2 B3 B4" using assms split_block(3)[of B k ] + by (metis carrier_matD(1) carrier_matD(2) diff_is_0_eq + le_add_diff_inverse nat_le_linear semiring_norm(137) + split_block(5) zero_less_diff) + also have "... = four_block_mat B1 (0\<^sub>m k (n-k)) (0\<^sub>m (n-k) k) B4" + using assms by simp + also have "... = four_block_mat B1 (0\<^sub>m k (n-k)) (0\<^sub>m (n-k) k) + (diag_block_mat [B4])" using diag_block_mat_singleton[of B4] by simp + also have "... = diag_block_mat [B1, B4]" + using diag_block_mat.simps(2)[of B1 "[B4]"] c1 c4 + unfolding Let_def by auto + finally show ?thesis . +qed + +subsection \Diagonal block matrices\ + +abbreviation four_block_diag where +"four_block_diag B1 B2 \ + (four_block_mat B1 (0\<^sub>m (dim_row B1) (dim_col B2)) + (0\<^sub>m (dim_row B2) (dim_col B1)) B2)" + +lemma four_block_diag_cong_comp: + assumes "dim_row A1 = dim_row B1" + and "dim_col A1 = dim_col B1" + and "four_block_diag A1 A2 = four_block_diag B1 B2" +shows "A1 = B1" +proof (rule eq_matI, auto simp:assms) + define A where "A = four_block_diag A1 A2" + define B where "B = four_block_diag B1 B2" + fix i j + assume "i < dim_row B1" and "jdim_row A2 = dim_row B2\) + have "j+m < dim_col A" + unfolding A_def n_def m_def four_block_mat_def Let_def + by (simp add: \dim_col A2 = dim_col B2\ ij) + { + have "n \ i+n" by simp + have "m\ j+m" by simp + have "i + n - n = i" by simp + have "j + m - m = j" by simp + } note ijeq = this + have "A2$$(i,j) = A$$(i+n, j+m)" using ijeq + using A_def \i + n < dim_row A\ \j + m < dim_col A\ m_def n_def by force + also have "... = B$$(i+n, j+m)" using assms unfolding A_def B_def by simp + also have "... = B2$$(i,j)" using ijeq + by (metis A_def B_def \i + n < dim_row A\ \j + m < dim_col A\ + add_implies_diff assms(1) assms(2) assms(3) index_mat_four_block(1) + index_mat_four_block(2) index_mat_four_block(3) m_def n_def + not_add_less2) + finally show "A2$$(i,j) = B2$$(i,j)" . +qed + +lemma four_block_mat_real_diag: + assumes "\i < dim_row B1. B1$$(i,i) \ Reals" + and "\i < dim_row B2. B2$$(i,i) \ Reals" + and "dim_row B1 = dim_col B1" + and "dim_row B2 = dim_col B2" + and "i < dim_row (four_block_diag B1 B2)" +shows "(four_block_diag B1 B2) $$ (i,i) \ Reals" +proof (cases "i < dim_row B1") + case True + then show ?thesis using assms by simp +next + case False + then show ?thesis using assms by force +qed + +lemma four_block_diagonal: + assumes "dim_row B1 = dim_col B1" + and "dim_row B2 = dim_col B2" + and "diagonal_mat B1" + and "diagonal_mat B2" +shows "diagonal_mat (four_block_diag B1 B2)" unfolding diagonal_mat_def +proof (intro allI impI) + fix i j + assume "i < dim_row (four_block_diag B1 B2)" + and "j < dim_col (four_block_diag B1 B2)" + and "i \ j" note ijprops = this + show "(four_block_diag B1 B2) $$ (i,j) = 0" + proof (cases "i < dim_row B1") + case True + then show ?thesis + using assms(3) diagonal_mat_def ijprops(2) ijprops(3) + by (metis add_less_imp_less_left + ijprops(1) index_mat_four_block(1) index_mat_four_block(2) + index_mat_four_block(3) index_zero_mat(1) + linordered_semidom_class.add_diff_inverse) + next + case False + then show ?thesis using ijprops + by (metis (no_types, lifting) add_less_cancel_left assms(1) + assms(4) diagonal_mat_def index_mat_four_block(1) + index_mat_four_block(2) index_mat_four_block(3) + index_zero_mat(1) linordered_semidom_class.add_diff_inverse) + qed +qed + +lemma four_block_diag_zero: + assumes "B\ carrier_mat 0 0" + shows "four_block_diag A B = A" +proof (rule eq_matI, auto) + show "dim_row B = 0" using assms by simp + show "dim_col B = 0" using assms by simp +qed + +lemma four_block_diag_zero': + assumes "B\ carrier_mat 0 0" + shows "four_block_diag B A = A" +proof (rule eq_matI) + show "dim_row (four_block_diag B A) = dim_row A" using assms by simp + show "dim_col (four_block_diag B A) = dim_col A" using assms by simp + fix i j + assume "i < dim_row A" and "j < dim_col A" + thus "four_block_diag B A $$ (i, j) = A $$ (i, j)" + using \dim_col (four_block_diag B A) = dim_col A\ + \dim_row (four_block_diag B A) = dim_row A\ + by auto +qed + +lemma mult_four_block_diag: + assumes "A1 \ carrier_mat nr1 n1" "D1 \ carrier_mat nr2 n2" + and "A2 \ carrier_mat n1 nc1" "D2 \ carrier_mat n2 nc2" +shows "four_block_diag A1 D1 * + four_block_diag A2 D2 + = four_block_diag (A1 * A2) (D1 * D2)" +proof - + define fb1 where "fb1 = four_block_mat A1 (0\<^sub>m nr1 n2) (0\<^sub>m nr2 n1) D1" + define fb2 where "fb2 = four_block_mat A2 (0\<^sub>m n1 nc2) (0\<^sub>m n2 nc1) D2" + have "fb1 * fb2 = four_block_mat (A1 * A2 + 0\<^sub>m nr1 n2 * 0\<^sub>m n2 nc1) + (A1 * 0\<^sub>m n1 nc2 + 0\<^sub>m nr1 n2 * D2) (0\<^sub>m nr2 n1 * A2 + D1 * 0\<^sub>m n2 nc1) + (0\<^sub>m nr2 n1 * 0\<^sub>m n1 nc2 + D1 * D2)" unfolding fb1_def fb2_def + proof (rule mult_four_block_mat) + show "A1 \ carrier_mat nr1 n1" using assms by simp + show "D1 \ carrier_mat nr2 n2" using assms by simp + show "A2 \ carrier_mat n1 nc1" "D2 \ carrier_mat n2 nc2" using assms by auto + qed auto + also have "... = four_block_mat (A1 * A2) (0\<^sub>m nr1 nc2) (0\<^sub>m nr2 nc1) (D1 * D2)" + using assms by simp + finally show ?thesis unfolding fb1_def fb2_def + using assms by simp +qed + +lemma four_block_diag_adjoint: + shows "(Complex_Matrix.adjoint (four_block_diag A1 A2)) = + (four_block_diag (Complex_Matrix.adjoint A1) + (Complex_Matrix.adjoint A2))" + by (rule eq_matI, + auto simp: four_block_mat_adjoint zero_adjoint adjoint_eval) + +lemma four_block_diag_unitary: + assumes "unitary U1" + and "unitary U2" +shows "unitary + (four_block_diag U1 U2)" +(is "unitary ?fU") + unfolding unitary_def +proof + show "?fU \ carrier_mat (dim_row ?fU) (dim_row ?fU)" + by (metis Complex_Matrix.unitary_def assms(1) assms(2) + four_block_carrier_mat index_mat_four_block(2)) + define n where "n = dim_row ?fU" + show "inverts_mat ?fU (Complex_Matrix.adjoint ?fU)" + proof - + have "(Complex_Matrix.adjoint ?fU) = + (four_block_mat (Complex_Matrix.adjoint U1) + (0\<^sub>m (dim_col U1) (dim_row U2)) + (0\<^sub>m (dim_col U2) (dim_row U1)) + (Complex_Matrix.adjoint U2))" + by (rule eq_matI, + auto simp: four_block_mat_adjoint zero_adjoint adjoint_eval) + hence "?fU * (Complex_Matrix.adjoint ?fU) = + ?fU * (four_block_diag (Complex_Matrix.adjoint U1) + (Complex_Matrix.adjoint U2))" by simp + also have "... = four_block_diag + (U1 * (Complex_Matrix.adjoint U1)) + (U2 * (Complex_Matrix.adjoint U2))" + by (rule mult_four_block_diag, (auto simp add: assms)) + also have "... = four_block_mat + (1\<^sub>m (dim_row U1)) + (0\<^sub>m (dim_row U1) (dim_row U2)) + (0\<^sub>m (dim_row U2) (dim_row U1)) + (1\<^sub>m (dim_row U2))" using assms + unfolding unitary_def inverts_mat_def + by simp + also have "... = 1\<^sub>m (dim_row U1 + dim_row U2)" by simp + finally show ?thesis unfolding inverts_mat_def by simp + qed +qed + +lemma four_block_diag_similar: + assumes "unitarily_equiv A1 B1 U1" + and "unitarily_equiv A2 B2 U2" + and "dim_row A1 = dim_col A1" + and "dim_row A2 = dim_col A2" +shows "similar_mat_wit + (four_block_diag A1 A2) + (four_block_diag B1 B2) + (four_block_diag U1 U2) + (Complex_Matrix.adjoint (four_block_diag U1 U2))" + unfolding similar_mat_wit_def +proof (simp add: Let_def, intro conjI) + define n where "n = dim_row A1 + dim_row A2" + show "four_block_diag A1 A2 \ carrier_mat n n" unfolding n_def using assms + by auto + show "four_block_diag B1 B2 \ carrier_mat n n" unfolding n_def using assms + by (metis carrier_matI four_block_carrier_mat unitarily_equiv_carrier(1)) + show u: "four_block_diag U1 U2 \ carrier_mat n n" unfolding n_def using assms + by (metis carrier_matI four_block_carrier_mat unitarily_equiv_carrier(2)) + thus cu: "Complex_Matrix.adjoint (four_block_diag U1 U2) \ carrier_mat n n" + unfolding n_def using adjoint_dim' by blast + show "four_block_diag U1 U2*Complex_Matrix.adjoint (four_block_diag U1 U2) = + 1\<^sub>m n" unfolding n_def + using u assms four_block_diag_unitary n_def + unitarily_equiv_def unitary_simps(2) by blast + thus "Complex_Matrix.adjoint (four_block_diag U1 U2)*four_block_diag U1 U2 = + 1\<^sub>m n" + using cu mat_mult_left_right_inverse u by blast + have "four_block_diag A1 A2 = + four_block_diag (U1 * B1 * (Complex_Matrix.adjoint U1)) + (U2 * B2 * (Complex_Matrix.adjoint U2))" + using assms unitarily_equiv_eq by blast + also have "... = (four_block_diag (U1*B1) (U2*B2)) * + (four_block_diag (Complex_Matrix.adjoint U1) + (Complex_Matrix.adjoint U2))" + proof (rule mult_four_block_diag[symmetric]) + show "U1 * B1 \ carrier_mat (dim_row A1) (dim_row A1)" + by (metis assms(1) assms(3) carrier_mat_triv mult_carrier_mat + unitarily_equiv_carrier(1) unitarily_equiv_carrier(2)) + show "U2 * B2 \ carrier_mat (dim_row A2) (dim_row A2)" + by (metis assms(2) assms(4) carrier_mat_triv mult_carrier_mat + unitarily_equiv_carrier(1) unitarily_equiv_carrier(2)) + show "Complex_Matrix.adjoint U1 \ carrier_mat (dim_row A1) (dim_row A1)" + by (metis Complex_Matrix.unitary_def adjoint_dim assms(1) + index_mult_mat(2) unitarily_equivD(1) unitarily_equiv_eq) + show "Complex_Matrix.adjoint U2 \ carrier_mat (dim_row A2) (dim_row A2)" + by (meson assms(2) carrier_mat_triv similar_mat_witD2(7) + unitarily_equiv_def) + qed + also have "... = four_block_diag U1 U2 * four_block_diag B1 B2 * + Complex_Matrix.adjoint (four_block_diag U1 U2)" + proof - + have "four_block_diag (U1*B1) (U2*B2) = + four_block_diag U1 U2 * four_block_diag B1 B2" + proof (rule mult_four_block_diag[symmetric]) + show "U1 \ carrier_mat (dim_row A1) (dim_row A1)" + by (metis assms(1) assms(3) carrier_mat_triv + unitarily_equiv_carrier(2)) + show "B1 \ carrier_mat (dim_row A1) (dim_row A1)" + by (metis assms(1) assms(3) carrier_mat_triv + unitarily_equiv_carrier(1)) + show "U2 \ carrier_mat (dim_row A2) (dim_row A2)" + by (metis assms(2) assms(4) carrier_mat_triv + unitarily_equiv_carrier(2)) + show "B2 \ carrier_mat (dim_row A2) (dim_row A2)" + by (metis assms(2) assms(4) carrier_mat_triv + unitarily_equiv_carrier(1)) + qed + moreover have "four_block_diag (Complex_Matrix.adjoint U1) + (Complex_Matrix.adjoint U2) = + Complex_Matrix.adjoint (four_block_diag U1 U2)" + by (rule four_block_diag_adjoint[symmetric]) + ultimately show ?thesis by simp + qed + finally show "four_block_diag A1 A2 = + four_block_diag U1 U2 * four_block_diag B1 B2 * + Complex_Matrix.adjoint (four_block_diag U1 U2)" . +qed + +lemma four_block_unitarily_equiv: + assumes "unitarily_equiv A1 B1 U1" + and "unitarily_equiv A2 B2 U2" + and "dim_row A1 = dim_col A1" + and "dim_row A2 = dim_col A2" +shows "unitarily_equiv + (four_block_diag A1 A2) + (four_block_diag B1 B2) + (four_block_diag U1 U2)" +(is "unitarily_equiv ?fA ?fB ?fU") + unfolding unitarily_equiv_def +proof + show "unitary ?fU" using four_block_diag_unitary assms unitarily_equivD(1) + by blast + show "similar_mat_wit ?fA ?fB ?fU (Complex_Matrix.adjoint ?fU)" + using assms four_block_diag_similar[of A1] by simp +qed + +lemma four_block_unitary_diag: + assumes "unitary_diag A1 B1 U1" + and "unitary_diag A2 B2 U2" + and "dim_row A1 = dim_col A1" + and "dim_row A2 = dim_col A2" +shows "unitary_diag + (four_block_diag A1 A2) + (four_block_diag B1 B2) + (four_block_diag U1 U2)" +(is "unitary_diag ?fA ?fB ?fU") + unfolding unitary_diag_def +proof + show "unitarily_equiv ?fA ?fB ?fU" + using four_block_unitarily_equiv[of A1] assms by simp + have "dim_row B1 = dim_col B1" unfolding unitary_diag_def + by (metis assms(1) assms(3) carrier_matD(1) carrier_matD(2) + carrier_mat_triv unitary_diag_carrier(1)) + moreover have "dim_row B2 = dim_col B2" unfolding unitary_diag_def + by (metis assms(2) assms(4) carrier_matD(1) carrier_matD(2) + carrier_mat_triv unitary_diag_carrier(1)) + ultimately show "diagonal_mat ?fB" using four_block_diagonal assms + unfolding unitary_diag_def by blast +qed + +lemma four_block_real_diag_decomp: + assumes "real_diag_decomp A1 B1 U1" + and "real_diag_decomp A2 B2 U2" + and "dim_row A1 = dim_col A1" + and "dim_row A2 = dim_col A2" +shows "real_diag_decomp + (four_block_diag A1 A2) + (four_block_diag B1 B2) + (four_block_diag U1 U2)" +(is "real_diag_decomp ?fA ?fB ?fU") + unfolding real_diag_decomp_def +proof (intro conjI allI impI) + show "unitary_diag ?fA ?fB ?fU" using four_block_unitary_diag assms + unfolding real_diag_decomp_def by blast + fix i + assume "i < dim_row ?fB" + show "?fB $$ (i,i) \ Reals" + proof (rule four_block_mat_real_diag) + show "i < dim_row ?fB" using \i < dim_row ?fB\ . + show "\i \" using assms + unfolding real_diag_decomp_def by simp + show "\i \" using assms + unfolding real_diag_decomp_def by simp + show "dim_row B1 = dim_col B1" unfolding unitary_diag_def + by (metis assms(1) assms(3) carrier_matD(1) carrier_matD(2) + carrier_mat_triv real_diag_decompD(1) unitary_diag_carrier(1)) + show "dim_row B2 = dim_col B2" unfolding unitary_diag_def + by (metis assms(2) assms(4) carrier_matD(1) carrier_matD(2) + carrier_mat_triv real_diag_decompD(1) unitary_diag_carrier(1)) + qed +qed + +lemma diag_block_mat_mult: + assumes "length Al = length Bl" + and "\i < length Al. dim_col (Al!i) = dim_row (Bl!i)" +shows "diag_block_mat Al * (diag_block_mat Bl) = + (diag_block_mat (map2 (*) Al Bl))" using assms +proof (induct Al arbitrary: Bl) + case Nil + then show ?case by simp +next + case (Cons a Al) + define A where "A = diag_block_mat Al" + define B where "B = diag_block_mat (tl Bl)" + have "0 < length Bl" using Cons by auto + hence "Bl = hd Bl # (tl Bl)" by simp + have "length (tl Bl) = length Al" using Cons by simp + have dim: "\ii < length Al\ length_Cons less_Suc_eq) + also have "... = dim_row (tl Bl!i)" + by (metis \Bl = hd Bl # tl Bl\ nth_Cons_Suc) + finally show "dim_col (Al ! i) = dim_row (tl Bl!i)" . + qed + define C where "C = map2 (*) (a # Al) Bl" + have "hd C = a * hd Bl" using \Bl = hd Bl # tl Bl\ unfolding C_def + by (metis list.map(2) list.sel(1) prod.simps(2) zip_Cons_Cons) + have "tl C = map2 (*) Al (tl Bl)" + by (metis (no_types, lifting) C_def \Bl = hd Bl # tl Bl\ list.sel(3) + map_tl zip_Cons_Cons) + have "C = hd C # (tl C)" unfolding C_def + by (metis Nil_eq_zip_iff Nil_is_map_conv \Bl = hd Bl # tl Bl\ + list.exhaust_sel list.simps(3)) + have "dim_row B = sum_list (map dim_row (tl Bl))" unfolding B_def + by (simp add: dim_diag_block_mat(1)) + also have "... = sum_list (map dim_col Al)" + proof (rule sum_list_cong) + show "length (map dim_row (tl Bl)) = length (map dim_col Al)" + using \length (tl Bl) = length Al\ by simp + show "\ilength (tl Bl) = length Al\ dim length_map nth_map) + qed + also have "... = dim_col A" unfolding A_def + by (simp add: dim_diag_block_mat(2)) + finally have ba: "dim_row B = dim_col A" . + have "diag_block_mat (a#Al) * (diag_block_mat Bl) = + four_block_diag a A * (four_block_diag (hd Bl) B)" + using diag_block_mat.simps(2) \Bl = hd Bl # (tl Bl)\ + unfolding Let_def A_def B_def by metis + also have "... = four_block_diag (a * hd Bl) (A * B)" + proof (rule mult_four_block_diag) + show "a\ carrier_mat (dim_row a) (dim_col a)" by simp + show "hd Bl \ carrier_mat (dim_col a) (dim_col (hd Bl))" + using Cons + by (metis \0 < length Bl\ \Bl = hd Bl # tl Bl\ carrier_mat_triv nth_Cons_0) + show "A \ carrier_mat (dim_row A) (dim_col A)" by simp + show " B \ carrier_mat (dim_col A) (dim_col B)" using ba by auto + qed + also have "... = four_block_diag (hd C) (diag_block_mat (tl C))" + unfolding A_def B_def + using C_def \hd C = a * hd Bl\ \length (tl Bl) = length Al\ + \tl C = map2 (*) Al (tl Bl)\ dim local.Cons(1) + by presburger + also have "... = diag_block_mat C" + using \C = hd C#(tl C)\ diag_block_mat.simps(2) unfolding Let_def by metis + finally show ?case unfolding C_def . +qed + +lemma real_diag_decomp_block: + fixes Al::"complex Matrix.mat list" + assumes "Al \ []" + and "list_all (\A. 0 < dim_row A \ hermitian A) Al" +shows "\ Bl Ul. length Ul = length Al \ + (\i < length Al. + Ul!i \ carrier_mat (dim_row (Al!i)) (dim_col (Al!i)) \ unitary (Ul!i) \ + Bl!i \ carrier_mat (dim_row (Al!i)) (dim_col (Al!i))) \ + real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) (diag_block_mat Ul)" + using assms +proof (induct Al) + case Nil + then show ?case by simp +next + case (Cons A Al) + hence "hermitian A" "0 < dim_row A" by auto + hence "A \ carrier_mat (dim_row A) (dim_row A)" + by (simp add: hermitian_square) + from this obtain B U where r: "real_diag_decomp A B U" + using hermitian_real_diag_decomp \hermitian A\ \0 < dim_row A\ by blast + have bcar: "B \ carrier_mat (dim_row A) (dim_col A)" + using real_diag_decompD(1) + by (metis \A \ carrier_mat (dim_row A) (dim_row A)\ carrier_matD(2) r + unitary_diag_carrier(1)) + have ucar: "U \ carrier_mat (dim_row A) (dim_col A)" + using real_diag_decompD(1) + by (metis \A \ carrier_mat (dim_row A) (dim_row A)\ carrier_matD(2) r + unitary_diag_carrier(2)) + have unit: "unitary U" + by (meson r real_diag_decompD(1) unitary_diagD(3)) + show ?case + proof (cases "Al = []") + case True + hence "diag_block_mat (Cons A Al) = A" by auto + moreover have "diag_block_mat [B] = B" by auto + moreover have "diag_block_mat [U] = U" by auto + moreover have "unitary U" + using r real_diag_decompD(1) unitary_diagD(3) by blast + ultimately have + "real_diag_decomp (diag_block_mat (Cons A Al)) + (diag_block_mat [B]) (diag_block_mat [U])" + using \real_diag_decomp A B U\ by auto + moreover have "(\i carrier_mat (dim_row ((A # Al) ! i)) (dim_col ((A # Al) ! i)) \ + Complex_Matrix.unitary ([U] ! i) \ [B] ! i \ + carrier_mat (dim_row ((A # Al) ! i)) (dim_col ((A # Al) ! i)))" using True + by (simp add: bcar ucar unit) + ultimately show ?thesis + using True \Complex_Matrix.unitary U\ bcar less_one ucar + by (metis length_list_update list_update_code(2)) + next + case False + have "list_all (\A. 0 < dim_row A \ hermitian A) Al" using Cons by auto + hence "\Bl Ul. length Ul = length Al \ + (\i carrier_mat (dim_row (Al ! i)) (dim_col (Al ! i)) \ + unitary (Ul!i) \ + Bl ! i \ carrier_mat (dim_row (Al ! i)) (dim_col (Al ! i))) \ + real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) (diag_block_mat Ul)" + using Cons False by simp + from this obtain Bl Ul where "length Ul =length Al" and + rl: "real_diag_decomp (diag_block_mat Al) + (diag_block_mat Bl) (diag_block_mat Ul)" + and "\i carrier_mat (dim_row (Al ! i)) (dim_col (Al ! i)) \ + unitary (Ul!i) \ + Bl ! i \ carrier_mat (dim_row (Al ! i)) (dim_col (Al ! i))" + by auto note bu = this + have "real_diag_decomp (diag_block_mat (A # Al)) + (diag_block_mat (B # Bl)) (diag_block_mat (U # Ul))" + using four_block_real_diag_decomp[OF r rl] + by (metis \A \ carrier_mat (dim_row A) (dim_row A)\ + carrier_matD(2) diag_block_mat.simps(2) hermitian_square + real_diag_decomp_hermitian rl) + moreover have "length (U#Ul) = length (A#Al)" using bu by simp + moreover have "\i carrier_mat (dim_row ((A # Al) ! i)) (dim_col ((A # Al) ! i)) \ + unitary ((U#Ul)!i) \ + (B#Bl) ! i \ carrier_mat (dim_row ((A # Al) ! i)) (dim_col ((A # Al) ! i))" + proof (intro allI impI) + fix i + assume "i < length (A#Al)" + show "(U # Ul) ! i \ carrier_mat (dim_row ((A # Al) ! i)) + (dim_col ((A # Al) ! i)) \ unitary ((U#Ul)!i) \ + (B # Bl) ! i \ carrier_mat (dim_row ((A # Al) ! i)) + (dim_col ((A # Al) ! i))" + proof (cases "i = 0") + case True + then show ?thesis by (simp add: bcar ucar unit) + next + case False + hence "\j. i = Suc j" by (simp add: not0_implies_Suc) + from this obtain j where j: "i = Suc j" by auto + hence "j < length Al" using \i < length (A#Al)\ by simp + have "(A#Al)!i = Al!j" "(U # Ul) ! i = Ul!j" "(B#Bl) ! i = Bl!j" + using j by auto + then show ?thesis using Cons \j < length Al\ bu(3) by presburger + qed + qed + ultimately show ?thesis by blast + qed +qed + +lemma diag_block_mat_adjoint: + shows "Complex_Matrix.adjoint (diag_block_mat Al) = + diag_block_mat (map Complex_Matrix.adjoint Al)" +proof (induct Al) + case Nil + then show ?case using zero_adjoint by simp +next + case (Cons a Al) + have "Complex_Matrix.adjoint (diag_block_mat (a # Al)) = + Complex_Matrix.adjoint (four_block_diag a (diag_block_mat Al))" + using diag_block_mat.simps(2)[of a] unfolding Let_def by simp + also have "... = four_block_diag (Complex_Matrix.adjoint a) + (Complex_Matrix.adjoint (diag_block_mat Al))" + using four_block_diag_adjoint[of a] by simp + also have "... = four_block_diag (Complex_Matrix.adjoint a) + (diag_block_mat (map Complex_Matrix.adjoint Al))" using Cons by simp + also have "... = diag_block_mat (map Complex_Matrix.adjoint (a#Al))" + using diag_block_mat.simps(2) unfolding Let_def + by (metis (no_types) diag_block_mat.simps(2) list.map(2)) + finally show ?case . +qed + +lemma diag_block_mat_mat_conj: + assumes "length Al = length Bl" + and "\i < length Al. dim_col (Al!i) = dim_row (Bl!i)" + and "\i < length Al. dim_row (Bl!i) = dim_col (Bl!i)" + shows "mat_conj (diag_block_mat Al) (diag_block_mat Bl) = + diag_block_mat (map2 mat_conj Al Bl)" +proof - + have "mat_conj (diag_block_mat Al) (diag_block_mat Bl) = + diag_block_mat Al * diag_block_mat Bl * + diag_block_mat (map Complex_Matrix.adjoint Al)" + using diag_block_mat_adjoint[of Al] unfolding mat_conj_def by simp + also have "... = diag_block_mat (map2 (*) Al Bl) * + diag_block_mat (map Complex_Matrix.adjoint Al)" + using diag_block_mat_mult[OF assms(1) assms(2)] by simp + also have "... = diag_block_mat (map2 (*) (map2 (*) Al Bl) + (map Complex_Matrix.adjoint Al))" + proof (rule diag_block_mat_mult) + show "length (map2 (*) Al Bl) = length (map Complex_Matrix.adjoint Al)" + by (simp add: assms(1)) + show "\ii < length Al. Al!i * (Bl!i) = Bl!i * (Al!i)" + and "\ii []" using assms by blast + hence "Al = hd Al#(tl Al)" by simp + hence da:"diag_block_mat Al = + four_block_diag (hd Al) (diag_block_mat (tl Al))" + using diag_block_mat.simps(2)[of "hd Al" "tl Al"] unfolding Let_def by simp + have "Bl \ []" using assms by simp + hence "Bl = hd Bl#(tl Bl)" by simp + hence "diag_block_mat Bl = four_block_diag (hd Bl) (diag_block_mat (tl Bl))" + using diag_block_mat.simps(2)[of "hd Bl" "tl Bl"] unfolding Let_def by simp + hence "four_block_diag (hd Al) (diag_block_mat (tl Al)) = + four_block_diag (hd Bl) (diag_block_mat (tl Bl))" using da assms by simp + thus ?thesis using four_block_diag_cong_comp assms by metis +qed + +lemma diag_block_mat_cong_tl: + assumes "0 < length Al" + and "length Al = length Bl" + and "dim_row (hd Al) = dim_row (hd Bl)" + and "dim_col (hd Al) = dim_col (hd Bl)" + and "diag_block_mat Al = diag_block_mat Bl" +shows "diag_block_mat (tl Al) = diag_block_mat (tl Bl)" +proof - + have "Al \ []" using assms by blast + hence "Al = hd Al#(tl Al)" by simp + hence da:"diag_block_mat Al = + four_block_diag (hd Al) (diag_block_mat (tl Al))" + using diag_block_mat.simps(2)[of "hd Al" "tl Al"] unfolding Let_def by simp + have "Bl \ []" using assms by simp + hence "Bl = hd Bl#(tl Bl)" by simp + hence "diag_block_mat Bl = four_block_diag (hd Bl) (diag_block_mat (tl Bl))" + using diag_block_mat.simps(2)[of "hd Bl" "tl Bl"] unfolding Let_def by simp + hence "four_block_diag (hd Al) (diag_block_mat (tl Al)) = + four_block_diag (hd Bl) (diag_block_mat (tl Bl))" using da assms by simp + thus ?thesis using four_block_diag_cong_comp' assms by metis +qed + +lemma diag_block_mat_cong_comp: + assumes "length Al = length Bl" + and "\iij = 0\ + by (metis \Bl = hd Bl # tl Bl\ nth_Cons_0) + have da: "diag_block_mat (a#Al) = four_block_diag a (diag_block_mat Al)" + using diag_block_mat.simps(2)[of a Al] unfolding Let_def by simp + have db: "diag_block_mat (hd Bl#(tl Bl)) = + four_block_diag (hd Bl) (diag_block_mat (tl Bl))" + using diag_block_mat.simps(2)[of "hd Bl" "tl Bl"] + unfolding Let_def by simp + have "hd (a#Al) = hd Bl" + proof (rule diag_block_mat_cong_hd) + show "0 < length (a # Al)" by simp + show "length (a # Al) = length Bl" using Cons by simp + show "diag_block_mat (a # Al) = diag_block_mat Bl" using Cons by simp + show "dim_row (hd (a # Al)) = dim_row (hd Bl)" + by (metis True \0 < length Bl\ \Bl ! j = hd Bl\ list.sel(1) Cons(2) + Cons(3) nth_Cons_0) + show "dim_col (hd (a # Al)) = dim_col (hd Bl)" + by (metis True \0 < length Bl\ \Bl ! j = hd Bl\ list.sel(1) Cons(2) + Cons(4) nth_Cons_0) + qed + thus "(a # Al) ! j = Bl ! j" using \j = 0\ \Bl ! j = hd Bl\ by fastforce + next + case False + hence "\k. j = Suc k" by (simp add: not0_implies_Suc) + from this obtain k where "j = Suc k" by auto + hence "(a#Al)!j = Al!k" by simp + have "Bl!j = (tl Bl)!k" using \j = Suc k\ \Bl = hd Bl#(tl Bl)\ + by (metis nth_Cons_Suc) + have "Al!k = (tl Bl)!k" + proof (rule Cons(1)) + show "length Al = length (tl Bl)" using Cons + by (metis diff_Suc_1 length_Cons length_tl) + show "k < length Al" + by (metis Cons.prems(5) Suc_less_SucD \j = Suc k\ length_Cons) + show "\ilength Al = length (tl Bl)\ length_Cons + local.Cons(3) nth_Cons_Suc nth_tl) + show "\iBl = hd Bl # tl Bl\ length_Cons local.Cons(4) + nth_Cons_Suc) + have "diag_block_mat (tl (a#Al)) = diag_block_mat (tl Bl)" + proof (rule diag_block_mat_cong_tl) + show "length (a # Al) = length Bl" using Cons by simp + show "dim_row (hd (a # Al)) = dim_row (hd Bl)" + by (metis \Bl = hd Bl # tl Bl\ length_Cons list.sel(1) local.Cons(3) + nth_Cons_0 zero_less_Suc) + show "dim_col (hd (a # Al)) = dim_col (hd Bl)" + by (metis \0 < length Bl\ \Bl = hd Bl # tl Bl\ list.sel(1) + local.Cons(2) local.Cons(4) nth_Cons_0) + show "diag_block_mat (a # Al) = diag_block_mat Bl" using Cons by simp + show "0 < length (a#Al)" by simp + qed + thus "diag_block_mat Al = diag_block_mat (tl Bl)" by simp + qed + then show ?thesis + by (simp add: \(a # Al) ! j = Al ! k\ \Bl ! j = tl Bl ! k\) + qed +qed + +lemma diag_block_mat_commute_comp: + assumes "length Al = length Bl" + and "\iiiiii < length Bl. dim_row (Bl!i) = dim_row (Ul!i)" + shows "dim_row (diag_block_mat Ul) = dim_row (diag_block_mat Bl)" +proof - + have "dim_row (diag_block_mat Ul) = sum_list (map dim_row Ul)" + by (simp add: dim_diag_block_mat(1)) + also have "... = sum_list (map dim_row Bl)" using assms + by (metis nth_map_conv) + also have "... = dim_row (diag_block_mat Bl)" + by (simp add: dim_diag_block_mat(1)) + finally show ?thesis . +qed + +lemma diag_block_mat_dim_col_cong: + assumes "length Ul = length Bl" + and "\i < length Bl. dim_col (Bl!i) = dim_col (Ul!i)" + shows "dim_col (diag_block_mat Ul) = dim_col (diag_block_mat Bl)" +proof - + have "dim_col (diag_block_mat Ul) = sum_list (map dim_col Ul)" + by (simp add: dim_diag_block_mat(2)) + also have "... = sum_list (map dim_col Bl)" using assms + by (metis nth_map_conv) + also have "... = dim_col (diag_block_mat Bl)" + by (simp add: dim_diag_block_mat(2)) + finally show ?thesis . +qed + +lemma diag_block_mat_dim_row_col_eq: + assumes "\i < length Al. dim_row (Al!i) = dim_col (Al!i)" + shows "dim_row (diag_block_mat Al) = dim_col (diag_block_mat Al)" +proof - + have "dim_row (diag_block_mat Al) = sum_list (map dim_row Al)" + by (simp add:dim_diag_block_mat(1)) + also have "... = sum_list (map dim_col Al)" using assms + by (metis nth_map_conv) + also have "... = dim_col (diag_block_mat Al)" + by (simp add:dim_diag_block_mat(2)) + finally show ?thesis . +qed + +section \Block matrix decomposition\ + +subsection \Subdiagonal extraction\ +text \\verb+extract_subdiags+ returns a list of diagonal sub-blocks, the sizes of which are +specified by the list of integers provided as parameters.\ + +fun extract_subdiags where + "extract_subdiags B [] = []" +| "extract_subdiags B (x#xs) = + (let (B1, B2, B3, B4) = (split_block B x x) in + B1 # (extract_subdiags B4 xs))" + +lemma extract_subdiags_not_emp: + fixes x::nat and l::"nat list" + assumes "(B1, B2, B3, B4) = (split_block B x x)" + shows "hd (extract_subdiags B (x#l)) = B1" + "tl (extract_subdiags B (x#l)) = extract_subdiags B4 l" +proof - + show "hd (extract_subdiags B (x#l)) = B1" unfolding Let_def + by (metis (no_types) assms extract_subdiags.simps(2) list.sel(1) split_conv) + show "tl (extract_subdiags B (x # l)) = extract_subdiags B4 l" + using assms extract_subdiags.simps(2) unfolding Let_def + by (metis (no_types, lifting) list.sel(3) split_conv) +qed + +lemma extract_subdiags_neq_Nil: + shows "extract_subdiags B (a#l) \ []" + using extract_subdiags.simps(2)[of B] + unfolding Let_def split_block_def by simp + +lemma extract_subdiags_length: + shows "length (extract_subdiags B l) = length l" +proof (induct l arbitrary: B) + case Nil + then show ?case by simp +next + case (Cons a l) + define B1 where "B1 = fst (split_block B a a)" + define B2 where "B2 = fst (snd (split_block B a a))" + define B3 where "B3 = fst (snd (snd (split_block B a a)))" + define B4 where "B4 = snd (snd (snd (split_block B a a)))" + have sp: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv + unfolding B1_def B2_def B3_def B4_def by simp + then show ?case using Cons extract_subdiags.simps(2)[of B a l] + unfolding Let_def by simp +qed + +lemma extract_subdiags_carrier: + assumes "i < length l" + shows "(extract_subdiags B l)!i \ carrier_mat (l!i) (l!i)" using assms +proof (induct i arbitrary: l B) + case 0 + define B1 where "B1 = fst (split_block B (hd l) (hd l))" + define B2 where "B2 = fst (snd (split_block B (hd l) (hd l)))" + define B3 where "B3 = fst (snd (snd (split_block B (hd l) (hd l))))" + define B4 where "B4 = snd (snd (snd (split_block B (hd l) (hd l))))" + have sp: "split_block B (hd l) (hd l) = (B1, B2, B3, B4)" using fst_conv snd_conv + unfolding B1_def B2_def B3_def B4_def by simp + have "l = hd l # (tl l)" using 0 by auto + have "(extract_subdiags B l)!0 = B1" + using extract_subdiags.simps(2)[of B "hd l" "tl l"] \l = hd l # tl l\ sp + unfolding Let_def by auto + also have "... \ carrier_mat (hd l) (hd l)" + unfolding B1_def split_block_def Let_def by simp + finally show ?case + by (metis \l = hd l # tl l\ hd_conv_nth list.sel(2) not_Cons_self) +next + case (Suc i) + define B1 where "B1 = fst (split_block B (hd l) (hd l))" + define B2 where "B2 = fst (snd (split_block B (hd l) (hd l)))" + define B3 where "B3 = fst (snd (snd (split_block B (hd l) (hd l))))" + define B4 where "B4 = snd (snd (snd (split_block B (hd l) (hd l))))" + have sp: "split_block B (hd l) (hd l) = (B1, B2, B3, B4)" using fst_conv snd_conv + unfolding B1_def B2_def B3_def B4_def by simp + have "l = hd l # (tl l)" using Suc + by (metis Cons_nth_drop_Suc drop_Nil list.exhaust_sel not_Cons_self) + hence "l! Suc i = (tl l)!i" by (metis nth_Cons_Suc) + have "tl (extract_subdiags B l) = extract_subdiags B4 (tl l)" + using extract_subdiags_not_emp(2)[OF sp[symmetric]] \l = hd l # (tl l)\ + by metis + hence "extract_subdiags B l = B1 # extract_subdiags B4 (tl l)" + using extract_subdiags_not_emp(1)[OF sp[symmetric]] + by (metis \l = hd l # tl l\ extract_subdiags_neq_Nil list.exhaust_sel) + hence "extract_subdiags B l ! Suc i = (extract_subdiags B4 (tl l))!i" + using nth_Cons_Suc by simp + also have "... \ carrier_mat (tl l!i) (tl l!i)" using Suc + by (metis \l = hd l # tl l\ length_Cons not_less_eq) + also have "... = carrier_mat (l!Suc i) (l! Suc i)" + using nth_Cons_Suc[of "hd l" "tl l" i] \l = hd l # tl l\ by simp + finally show ?case . +qed + +lemma extract_subdiags_diagonal: + assumes "diagonal_mat B" + and "B \ carrier_mat n n" + and "l \ []" + and "sum_list l \ n" + and "i < length l" +shows "diagonal_mat ((extract_subdiags B l)!i)" using assms +proof (induct i arbitrary: l B n) + case 0 + define a where "a = hd l" + have "l = a#(tl l)" unfolding a_def using 0 by simp + have "a \ n" using 0 unfolding a_def + by (metis a_def dual_order.strict_trans2 elem_le_sum_list + hd_conv_nth less_le_not_le nat_le_linear) + define B1 where "B1 = fst (split_block B a a)" + define B2 where "B2 = fst (snd (split_block B a a))" + define B3 where "B3 = fst (snd (snd (split_block B a a)))" + define B4 where "B4 = snd (snd (snd (split_block B a a)))" + have sp: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv + unfolding B1_def B2_def B3_def B4_def by simp + hence "extract_subdiags B l!0 = B1" unfolding a_def + using hd_conv_nth 0 + by (metis \l = a # tl l\ sp extract_subdiags_neq_Nil + extract_subdiags_not_emp(1)) + moreover have "diagonal_mat B1" using sp split_block_diagonal assms \a \ n\ 0 + by blast + ultimately show ?case by simp +next + case (Suc i) + show ?case + proof (cases "length l = 1") + case True + hence "Suc i = 0" using Suc by presburger + then show ?thesis by simp + next + case False + define a where "a = hd l" + have "l = a#(tl l)" unfolding a_def using Suc by simp + have "a \ n" using Suc unfolding a_def + by (metis dual_order.trans elem_le_sum_list hd_conv_nth + length_greater_0_conv) + define B1 where "B1 = fst (split_block B a a)" + define B2 where "B2 = fst (snd (split_block B a a))" + define B3 where "B3 = fst (snd (snd (split_block B a a)))" + define B4 where "B4 = snd (snd (snd (split_block B a a)))" + have sp: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv + unfolding B1_def B2_def B3_def B4_def by simp + have "extract_subdiags B l ! Suc i = + extract_subdiags B4 (tl l)! i" using sp + by (metis Suc(6) Suc_less_SucD \l = a # tl l\ length_Cons nth_tl + extract_subdiags_length extract_subdiags_not_emp(2)) + moreover have "diagonal_mat (extract_subdiags B4 (tl l)! i)" + proof (rule Suc(1)) + show "tl l \ []" using False Suc + by (metis \l = a # tl l\ length_Cons list.size(3) numeral_nat(7)) + show "i < length (tl l)" using False Suc + by (metis Suc_lessD \l = a # tl l\ le_neq_implies_less length_Cons + less_Suc_eq_le) + show "B4 \ carrier_mat (n-a) (n-a)" + using sp split_block_diag_carrier(2) Suc(3) \a \ n\ by blast + show "diagonal_mat B4" + using split_block_diagonal sp Suc \a \ n\ by blast + show "sum_list (tl l) \ n - a" using Suc(5) \a \ n\ sum_list_tl_leq + by (simp add: Suc(4) a_def) + qed + ultimately show ?thesis by simp + qed +qed + +lemma extract_subdiags_diag_elem: + fixes B::"complex Matrix.mat" + assumes "B\ carrier_mat n n" + and "0 < n" + and "l \ []" + and "i < length l" + and "j< l!i" + and "sum_list l \ n" + and "\j < length l. 0 < l!j" + shows "extract_subdiags B l!i $$ (j,j) = + diag_mat B!(n_sum i l + j)" using assms +proof (induct i arbitrary: l B n) + case 0 + define a where "a = hd l" + have "l = a#(tl l)" unfolding a_def using 0 by simp + have "a \ n" using 0 unfolding a_def + by (metis a_def dual_order.strict_trans2 elem_le_sum_list + hd_conv_nth less_le_not_le nat_le_linear) + define B1 where "B1 = fst (split_block B a a)" + define B2 where "B2 = fst (snd (split_block B a a))" + define B3 where "B3 = fst (snd (snd (split_block B a a)))" + define B4 where "B4 = snd (snd (snd (split_block B a a)))" + have sp: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv + unfolding B1_def B2_def B3_def B4_def by simp + hence "extract_subdiags B l!0 = B1" + using hd_conv_nth unfolding Let_def + by (metis \l = a # tl l\ extract_subdiags_neq_Nil + extract_subdiags_not_emp(1)) + hence "extract_subdiags B l!0 $$ (j,j) = B$$ (j,j)" + using sp 0 unfolding split_block_def + by (metis (no_types, lifting) carrier_matD(2) dim_col_mat(1) + index_mat(1) prod.sel(1) extract_subdiags_carrier) + also have "... = diag_mat B!j" + using 0 \a \ n\ hd_conv_nth unfolding diag_mat_def a_def + by fastforce + also have "... = diag_mat B!(n_sum 0 l + j)" by simp + finally show ?case . +next + case (Suc i) + show ?case + proof (cases "length l = 1") + case True + hence "Suc i < 0" using Suc by simp + then show ?thesis by simp + next + case False + hence "1 < length l" using Suc by presburger + define a where "a = hd l" + have "l = a#(tl l)" unfolding a_def using Suc by simp + have "a \ n" using Suc unfolding a_def + by (metis add_le_same_cancel1 elem_le_sum_list hd_conv_nth + le_add2 le_trans verit_comp_simplify1(3)) + define B1 where "B1 = fst (split_block B a a)" + define B2 where "B2 = fst (snd (split_block B a a))" + define B3 where "B3 = fst (snd (snd (split_block B a a)))" + define B4 where "B4 = snd (snd (snd (split_block B a a)))" + have sp: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv + unfolding B1_def B2_def B3_def B4_def by simp + have "B4 \ carrier_mat (n-a) (n-a)" + using sp split_block_diag_carrier(2) Suc \a \ n\ by blast + have "B1 \ carrier_mat a a" + using sp split_block_diag_carrier(1) Suc \a \ n\ by blast + have "n_sum (Suc i) l + j < n_sum (Suc (Suc i)) l" + using Suc n_sum_last_lt by metis + hence "a + n_sum i (tl l) + j < n_sum (Suc (Suc i)) l" + unfolding a_def by simp + also have "... \ sum_list l" + proof (rule n_sum_sum_list) + show "\j l ! j" using Suc by simp + show "Suc (Suc i) \ length l" using Suc by simp + qed + also have "... \ n" using Suc by simp + finally have "a + n_sum i (tl l) + j < n" . + hence "n_sum i (tl l) +j < n - a" by simp + have "extract_subdiags B l!(Suc i) = + extract_subdiags B4 (tl l)!i" + using sp \l = a#(tl l)\ unfolding Let_def + by (metis list.exhaust_sel nth_Cons_Suc extract_subdiags_neq_Nil + extract_subdiags_not_emp(2)) + hence "extract_subdiags B l!(Suc i) $$(j,j) = + extract_subdiags B4 (tl l)!i $$(j,j)" by simp + also have "... = diag_mat B4!(n_sum i (tl l) + j)" + proof (rule Suc(1)) + show "tl l \ []" using False Suc + by (metis \l = a # tl l\ length_Cons list.size(3) numeral_nat(7)) + show "i < length (tl l)" using False Suc + by (metis Suc_lessD \l = a # tl l\ le_neq_implies_less length_Cons + less_Suc_eq_le) + show "B4 \ carrier_mat (n-a) (n-a)" + using \B4 \ carrier_mat (n-a) (n-a)\ . + show "sum_list (tl l) \ n - a" using Suc(5) \a \ n\ sum_list_tl_leq + by (simp add: Suc a_def) + show "0 < n - a" + by (metis Suc.prems(4) Suc.prems(7) \i < length (tl l)\ + \l = a # tl l\ \sum_list (tl l) \ n - a\ bot_nat_0.extremum_uniqueI + elem_le_sum_list gr_zeroI nth_Cons_Suc) + show "\ji < length (tl l)\ nth_tl) + qed + also have "... = B4$$(n_sum i (tl l)+j, n_sum i (tl l)+j)" + proof - + have "n_sum i (tl l) +j < n - a" using \n_sum i (tl l) +j < n - a\ . + thus ?thesis + using \B4 \ carrier_mat (n-a) (n-a)\ + unfolding diag_mat_def by simp + qed + also have "... = B$$(n_sum i (tl l) + j + a, n_sum i (tl l) + j + a)" + using sp \B1 \ carrier_mat a a\ \n_sum i (tl l) +j < n - a\ + \B4 \ carrier_mat (n-a) (n-a)\ carrier_matD(2) dim_col_mat(1) Suc + index_mat(1) prod.sel + unfolding split_block_def Let_def by force + also have "... = diag_mat B!(n_sum i (tl l) + j + a)" + proof - + have "n_sum i (tl l) + j + a < n" using \n_sum i (tl l) +j < n - a\ + by simp + thus ?thesis using Suc unfolding diag_mat_def by simp + qed + also have "... = diag_mat B ! (n_sum (Suc i) l + j)" + proof - + have "n_sum i (tl l) + a = n_sum (Suc i) l" unfolding a_def by simp + thus ?thesis + by (simp add: add.commute add.left_commute) + qed + finally show ?thesis . + qed +qed + +lemma hermitian_extract_subdiags: + assumes "hermitian A" + and "sum_list l \ dim_row A" + and "list_all (\a. 0 < a) l" + shows "list_all (\B. 0 < dim_row B \ hermitian B) (extract_subdiags A l)" + using assms +proof (induct l arbitrary: A) + case Nil + then show ?case by simp +next + case (Cons a l) + define es where "es = extract_subdiags A (a#l)" + define B1 where "B1 = fst (split_block A a a)" + define B2 where "B2 = fst (snd (split_block A a a))" + define B3 where "B3 = fst (snd (snd (split_block A a a)))" + define B4 where "B4 = snd (snd (snd (split_block A a a)))" + have sp: "split_block A a a = (B1, B2, B3, B4)" using fst_conv snd_conv + unfolding B1_def B2_def B3_def B4_def by simp + have "0 < a" using Cons by simp + have "es \ []" using extract_subdiags_neq_Nil[of A] + unfolding es_def by simp + hence "es = hd es # (tl es)" by simp + have "hd es = B1" unfolding es_def + using extract_subdiags_not_emp(1)[OF sp[symmetric]] by simp + have "dim_row B1 = a" unfolding B1_def split_block_def Let_def by simp + have "tl es = extract_subdiags B4 l" unfolding es_def + using extract_subdiags_not_emp(2)[OF sp[symmetric]] by simp + have "list_all (\B. 0 < dim_row B \ hermitian B) (hd es # (tl es))" + proof (rule list_all_simps(1)[THEN iffD2], intro conjI) + show "hermitian (hd es)" + proof (rule split_block_hermitian_1) + show "hermitian A" using Cons by simp + show "(hd es, B2, B3, B4) = split_block A a a" using sp \hd es = B1\ + by simp + show "a \ dim_row A" using Cons by simp + qed + have "list_all (\B. 0 < dim_row B \ hermitian B) (extract_subdiags B4 l)" + proof (rule Cons(1)) + show "hermitian B4" + proof (rule split_block_hermitian_4) + show "hermitian A" using Cons by simp + show "a \ dim_row A" using Cons by simp + show "(B1, B2, B3, B4) = split_block A a a" using sp by simp + qed + show "sum_list l \ dim_row B4" using Cons sp + unfolding split_block_def Let_def by force + show "list_all ((<) 0) l" using Cons(4) by auto + qed + thus "list_all (\B. 0 < dim_row B \ hermitian B) (tl es)" + using \tl es = extract_subdiags B4 l\ by simp + show "0 < dim_row (hd es)" + using \hd es = B1\ \0 < a\ \dim_row B1 = a\ by simp + qed + thus ?case using \es = hd es # (tl es)\ unfolding es_def by metis +qed + +subsection \Predicates on diagonal block matrices\ +text \The predicate \verb+diag_compat+ ensures that the provided matrix, when decomposed +according to the list of integers provided as an input, is indeed a diagonal block matrix.\ + +fun diag_compat where + "diag_compat B [] = (dim_row B = 0 \ dim_col B = 0)" +| "diag_compat B (x#xs) = + (x \ dim_row B \ + (let n = dim_row B; (B1, B2, B3, B4) = (split_block B x x) in + B2 = (0\<^sub>m x (n - x)) \ B3 = (0\<^sub>m (n - x) x) \ diag_compat B4 xs))" + +text \When this is the case, the decomposition of a matrix leaves it unchanged.\ + +lemma diag_compat_extract_subdiag: + assumes "B\ carrier_mat n n" + and "diag_compat B l" + shows "B = diag_block_mat (extract_subdiags B l)" using assms +proof (induct l arbitrary:B n) + case Nil + have "extract_subdiags B Nil = []" by simp + have "B = 0\<^sub>m 0 0" + proof (rule eq_matI, auto simp add: assms) + show "dim_row B = 0" using Nil by simp + show "dim_col B = 0" using Nil by simp + qed + then show ?case using diag_block_mat_singleton[of B] by simp +next + case (Cons a l) + define B1 where "B1 = fst (split_block B a a)" + define B2 where "B2 = fst (snd (split_block B a a))" + define B3 where "B3 = fst (snd (snd (split_block B a a)))" + define B4 where "B4 = snd (snd (snd (split_block B a a)))" + have sp: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv + unfolding B1_def B2_def B3_def B4_def by simp + have "a \ n" using assms Cons by simp + have "diag_compat B4 l" using sp Cons by (simp add: Let_def) + have "B1 \ carrier_mat a a" using sp Cons split_block(1)[OF sp] + by (metis \a \ n\ carrier_matD(1) carrier_matD(2) le_add_diff_inverse) + have "B2 \ carrier_mat a (n-a)" using sp Cons by (simp add: Let_def) + have "B3 \ carrier_mat (n-a) a" using sp Cons by (simp add: Let_def) + have "B4 \ carrier_mat (n-a) (n-a)" using assms \a \ n\ Cons + split_block(4)[OF sp] by simp + have b2: "0\<^sub>m (dim_row B1) (dim_col B4) = B2" + using diag_compat.simps(2)[THEN iffD1, OF \diag_compat B (a#l)\] + \B4 \ carrier_mat (n-a) (n-a)\ \B1 \ carrier_mat a a\ + \B2 \ carrier_mat a (n-a)\ sp unfolding Let_def + Cons(2) by force + have b3: "0\<^sub>m (dim_row B4) (dim_col B1) = B3" + using diag_compat.simps(2)[THEN iffD1, OF \diag_compat B (a#l)\] + \B4 \ carrier_mat (n-a) (n-a)\ \B1 \ carrier_mat a a\ + \B2 \ carrier_mat a (n-a)\ sp unfolding Let_def + Cons(2) by force + have "extract_subdiags B (a#l) = B1 # (extract_subdiags B4 l)" + using fst_conv snd_conv extract_subdiags.simps(2)[of B] + unfolding B1_def B4_def Let_def by (simp add: split_def) + also have "diag_block_mat ... = + (let + C = diag_block_mat (extract_subdiags B4 l) + in four_block_mat B1 (0\<^sub>m (dim_row B1) (dim_col C)) + (0\<^sub>m (dim_row C) (dim_col B1)) C)" by simp + also have "... = four_block_mat B1 (0\<^sub>m (dim_row B1) (dim_col B4)) + (0\<^sub>m (dim_row B4) (dim_col B1)) B4" using Cons \diag_compat B4 l\ + \B4 \ carrier_mat (n-a) (n-a)\ by (simp add:Let_def) + also have "... = four_block_mat B1 B2 B3 B4" using b2 b3 by simp + also have "... = B" using split_block(5)[OF sp, of "n-a" "n-a"] Cons by simp + finally show ?case by simp +qed + +text \Predicate \verb+diag_diff+ holds when the decomposition of the considered +matrix based on the list of integers provided as a parameter, is such that the diagonal +elements of separate components are pairwise distinct.\ + +fun diag_diff where + "diag_diff D [] = (dim_row D = 0 \ dim_col D = 0)" +| "diag_diff D (x#xs) = + (x \ dim_row D \ + (let (D1, D2, D3, D4) = (split_block D x x) in + (\i j. i < dim_row D1 \ j < dim_row D4 \ D1$$(i,i) \ D4 $$ (j,j)) \ + diag_diff D4 xs))" + +lemma diag_diff_hd_diff: + assumes "diag_diff D (a#xs)" + and "D\ carrier_mat n n" + and "i < a" + and "a \ j" + and "j < n" +shows "D$$(i,i) \ D $$ (j,j)" +proof - + define D1 where "D1 = fst (split_block D a a)" + define D2 where "D2 = fst (snd (split_block D a a))" + define D3 where "D3 = fst (snd (snd (split_block D a a)))" + define D4 where "D4 = snd (snd (snd (split_block D a a)))" + have spd: "split_block D a a = (D1, D2, D3, D4)" using fst_conv snd_conv + unfolding D1_def D2_def D3_def D4_def by simp + have c1: "D1 \ carrier_mat a a" using split_block(1)[OF spd, of "n-a" "n-a"] + assms by simp + have c4: "D4 \ carrier_mat (n-a) (n-a)" using assms + split_block(4)[OF spd] by simp + hence "j - a < dim_row D4" using assms by simp + have "D $$ (i,i) = D1 $$ (i,i)" using assms spd + unfolding split_block_def Let_def by force + moreover have "D $$ (j,j) = D4 $$ (j-a, j - a)" using assms spd + unfolding split_block_def Let_def by force + moreover have "D1 $$ (i,i) \ D4 $$ (j-a, j - a)" + using assms \j - a < dim_row D4\ spd c1 c4 + diag_diff.simps(2)[THEN iffD1, OF assms(1)] unfolding Let_def by simp + ultimately show ?thesis by simp +qed + +lemma diag_compat_diagonal: + assumes "B\ carrier_mat (dim_row B) (dim_row B)" + and "diagonal_mat B" + and "dim_row B = sum_list l" +shows "diag_compat B l" using assms +proof (induct l arbitrary: B) + case Nil + then show ?case by simp +next + case (Cons a l) + define B1 where "B1 = fst (split_block B a a)" + define B2 where "B2 = fst (snd (split_block B a a))" + define B3 where "B3 = fst (snd (snd (split_block B a a)))" + define B4 where "B4 = snd (snd (snd (split_block B a a)))" + have sp: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv + unfolding B1_def B2_def B3_def B4_def by simp + have "diagonal_mat B1 \ diagonal_mat B4" + proof (rule split_block_diagonal) + show "split_block B a a = (B1, B2, B3, B4)" using sp . + show "diagonal_mat B" using Cons by simp + show "B\ carrier_mat (dim_row B) (dim_row B)" using Cons by simp + show "a \ dim_row B" using Cons by simp + qed + define n where "n = dim_row B" + have "diag_compat B4 l" + proof (rule Cons(1)) + show "diagonal_mat B4" using \diagonal_mat B1 \ diagonal_mat B4\ by simp + show "B4 \ carrier_mat (dim_row B4) (dim_row B4)" using sp Cons + unfolding split_block_def Let_def by auto + show "dim_row B4 = sum_list l" using Cons sp + unfolding split_block_def Let_def by auto + qed + have "B2 = 0\<^sub>m a (n - a)" + proof (rule eq_matI, auto) + show "dim_row B2 = a" using sp unfolding split_block_def Let_def n_def + by auto + show "dim_col B2 = n-a" using sp Cons + unfolding split_block_def Let_def n_def by auto + fix i j + assume "i < a" and "j < n-a" + thus "B2 $$(i,j) = 0" using sp Cons + unfolding split_block_def Let_def n_def diagonal_mat_def by force + qed + have "B3 = 0\<^sub>m (n - a) a" + proof (rule eq_matI, auto) + show "dim_row B3 = n-a" using sp Cons + unfolding split_block_def Let_def n_def by auto + show "dim_col B3 = a" using sp Cons + unfolding split_block_def Let_def n_def by auto + fix i j + assume "i < n-a" and "j < a" + thus "B3 $$(i,j) = 0" using sp Cons + unfolding split_block_def Let_def n_def diagonal_mat_def by force + qed + show ?case + proof (rule diag_compat.simps(2)[THEN iffD2], intro conjI) + show "a \ dim_row B" using Cons by simp + show "let n = dim_row B; + (B1, B2, B3, B4) = split_block B a a in B2 = 0\<^sub>m a (n - a) \ + B3 = 0\<^sub>m (n - a) a \ diag_compat B4 l" + using sp \B3 = 0\<^sub>m (n - a) a\ \B2 = 0\<^sub>m a (n - a)\ + \diag_compat B4 l\ unfolding Let_def n_def by auto + qed +qed + +text \The following lemma provides a sufficient condition for the \verb+diag_compat+ predicate +to hold.\ + +lemma commute_diag_compat: + fixes D::"'a::{field} Matrix.mat" + assumes "diagonal_mat D" + and "D\ carrier_mat n n" + and "B\ carrier_mat n n" + and "B* D = D * B" + and "diag_diff D l" +shows "diag_compat B l" using assms +proof (induct l arbitrary: B D n) + case Nil + hence "D \ carrier_mat 0 0" using assms by simp + hence "n = 0" using assms using Nil(2) by auto + hence "B \ carrier_mat 0 0" using Nil by simp + then show ?case by simp +next + case (Cons a l) + define B1 where "B1 = fst (split_block B a a)" + define B2 where "B2 = fst (snd (split_block B a a))" + define B3 where "B3 = fst (snd (snd (split_block B a a)))" + define B4 where "B4 = snd (snd (snd (split_block B a a)))" + have spb: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv + unfolding B1_def B2_def B3_def B4_def by simp + define D1 where "D1 = fst (split_block D a a)" + define D2 where "D2 = fst (snd (split_block D a a))" + define D3 where "D3 = fst (snd (snd (split_block D a a)))" + define D4 where "D4 = snd (snd (snd (split_block D a a)))" + have spd: "split_block D a a = (D1, D2, D3, D4)" using fst_conv snd_conv + unfolding D1_def D2_def D3_def D4_def by simp + have "a \ n" using Cons by simp + moreover have "diag_compat B4 l" + proof (rule Cons(1)) + show "diagonal_mat D4" using spd Cons \a \ n\ + split_block_diagonal[of D n a] by blast + show "D4\ carrier_mat (n-a) (n-a)" using spd Cons(3) + unfolding split_block_def Let_def by fastforce + show "diag_diff D4 l" using spd Cons by simp + show "B4 \ carrier_mat (n - a) (n - a)" using spb Cons(4) + unfolding split_block_def Let_def by fastforce + show "B4 * D4 = D4 * B4" using spb Cons \a \ n\ + split_block_commute_subblock[of D] by (meson spd) + qed + moreover have "B2 = 0\<^sub>m a (n - a)" + proof (rule commute_diag_mat_split_block(1)[of D n B a B1 B2 B3 B4], + (auto simp add: spb Cons \a \ n\)) + fix i j + assume "i < a" and "a \ j" and "j < n" + thus "D $$ (i, i) = D $$ (j, j) \ False" + using diag_diff_hd_diff[OF Cons(6) Cons(3), of i j] by simp + qed + moreover have "B3 = 0\<^sub>m (n - a) a" + proof (rule commute_diag_mat_split_block(2)[of D n B a B1 B2 B3 B4], + (auto simp add: spb Cons \a \ n\)) + fix i j + assume "i < a" and "a \ j" and "j < n" + thus "D $$ (i, i) = D $$ (j, j) \ False" + using diag_diff_hd_diff[OF Cons(6) Cons(3), of i j] by simp + qed + ultimately show ?case + using spb diag_compat.simps(2)[THEN iffD2, of a B l] Cons + unfolding Let_def by force +qed + +subsection \Counting similar neighbours in a list\ +text \The function \verb+eq_comps+ takes a list as an input and counts the number of +adjacent elements that are identical.\ + +fun eq_comps where + "eq_comps [] = []" +| "eq_comps [x] = [1]" +| "eq_comps (x#y#l) = (let tmp = (eq_comps (y#l)) in + if x = y then Suc (hd tmp) # (tl tmp) + else 1 # tmp)" + +lemma eq_comps_not_empty: + assumes "l\ []" + shows "eq_comps l \ []" using assms +proof (induct l rule: eq_comps.induct) + case 1 + then show ?case by simp +next + case (2 x) + then show ?case by simp +next + case (3 x y l) + then show ?case by (cases "x = y", (auto simp add: Let_def)) +qed + +lemma eq_comps_empty_if: + assumes "eq_comps l = []" + shows "l = []" +proof (rule ccontr) + assume "l\ []" + hence "eq_comps l \ []" using eq_comps_not_empty[of l] by simp + thus False using assms by simp +qed + +lemma eq_comps_hd_eq_tl: + assumes "x = y" + shows "tl (eq_comps (x#y#l)) = tl (eq_comps (y#l))" using assms by (simp add: Let_def) + +lemma eq_comps_hd_neq_tl: + assumes "x \ y" + shows "tl (eq_comps (x#y#l)) = eq_comps (y#l)" using assms by (simp add:Let_def) + +lemma eq_comps_drop: + assumes "x#xs = eq_comps l" + shows "xs = eq_comps (drop x l)" using assms +proof (induct l arbitrary:x xs rule: eq_comps.induct) +case 1 + then show ?case by simp +next + case (2 u) + hence "x = 1" by simp + hence "drop x [u] = []" by simp + then show ?case using "2" by fastforce +next + case (3 u v l) + define ec where "ec = eq_comps (v#l)" + have "ec = hd ec # (tl ec)" using eq_comps_not_empty[of "v#l"] unfolding ec_def + by simp + show ?case + proof (cases "u = v") + case True + have "xs = tl ec" using 3 eq_comps_hd_eq_tl[OF True] ec_def + by (metis list.sel(3)) + moreover have "x = Suc (hd ec)" using True 3 eq_comps.simps(3)[of u v ] + unfolding ec_def Let_def by simp + hence "drop (hd ec) (v#l) = drop x (u#v#l)" by simp + moreover have "tl ec = eq_comps (drop (hd ec) (v#l))" using 3 ec_def + \ec = hd ec # (tl ec)\ by simp + ultimately show ?thesis using 3 by simp + next + case False + hence "x = 1" using 3 unfolding Let_def by simp + moreover have "xs = ec" using 3 eq_comps_hd_neq_tl[OF False] ec_def + by (metis list.sel(3)) + ultimately show ?thesis unfolding ec_def by simp + qed +qed + +lemma eq_comps_neq_0: + assumes "a#m = eq_comps l" + shows "a \ 0" using assms +proof (induct l rule:eq_comps.induct) + case 1 + then show ?case by simp +next + case (2 x) + then show ?case by simp +next + case (3 x y l) + then show ?case by (cases "x = y", (auto simp add: Let_def)) +qed + +lemma eq_comps_gt_0: + assumes "l \ []" + shows "list_all (\a. 0 < a) (eq_comps l)" +proof (induct l rule:eq_comps.induct) + case 1 + then show ?case by simp +next + case (2 x) + then show ?case by simp +next + case (3 x y l) + then show ?case + proof (cases "x = y") + case True + then show ?thesis + using 3 eq_comps.simps(3)[of x y l] list_all_simps(1) unfolding Let_def + by (metis eq_comps_not_empty hd_Cons_tl list.discI zero_less_Suc) + next + case False + then show ?thesis + using 3 eq_comps.simps(3)[of x y l] list_all_simps(1) unfolding Let_def + by auto + qed +qed + +lemma eq_comps_elem_le_length: + assumes "a#m = eq_comps l" + shows "a \ length l" using assms +proof (induct l arbitrary: a rule:eq_comps.induct) + case 1 + then show ?case by simp +next + case (2 x) + then show ?case by auto +next + case (3 x y l) + then show ?case + proof (cases "x = y") + case True + define ec where "ec = eq_comps (y#l)" + have "ec = hd ec # (tl ec)" using eq_comps_not_empty[of "y#l"] unfolding ec_def + by simp + have "a = Suc (hd ec)" using True 3 eq_comps.simps(3)[of x y] + unfolding ec_def Let_def by simp + then show ?thesis using 3 + by (metis True \ec = hd ec # tl ec\ ec_def eq_comps_hd_eq_tl length_Cons + list.sel(3) not_less_eq_eq) + next + case False + hence "a = 1" using 3 by (simp add: Let_def) + then show ?thesis by simp + qed +qed + +lemma eq_comps_length: + shows "length (eq_comps l) \ length l" +proof (induct l rule:eq_comps.induct) + case 1 + then show ?case by simp +next + case (2 x) + then show ?case by auto +next + case (3 x y l) + define ec where "ec = eq_comps (y#l)" + have ec: "ec = hd ec # (tl ec)" using eq_comps_not_empty[of "y#l"] unfolding ec_def + by simp + then show ?case + proof (cases "x = y") + case True + then show ?thesis using ec 3 eq_comps.simps(3) True unfolding Let_def + by (metis ec_def le_SucI length_Cons) + next + case False + then show ?thesis using ec 3 by simp + qed +qed + +lemma eq_comps_eq: + assumes "a#m = eq_comps l" + and "i < a" +shows "nth l i = hd l" using assms +proof (induct l arbitrary: a m i rule: eq_comps.induct) + case 1 + then show ?case by simp +next + case (2 u) + then show ?case by simp +next + case (3 u v l) + show ?case + proof (cases "u = v") + case False + thus ?thesis using 3 by (simp add: Let_def) + next + case True + define ec where "ec = eq_comps (v#l)" + have "ec = hd ec # (tl ec)" using eq_comps_not_empty[of "v#l"] + unfolding ec_def by simp + have "a = Suc (hd ec)" using True 3 eq_comps.simps(3)[of u v] + unfolding ec_def Let_def by simp + hence "i \ hd ec" using 3 by simp + show ?thesis + proof (cases "i = 0") + case True + thus ?thesis by simp + next + case False + hence "\i'. i = Suc i'" by (simp add: not0_implies_Suc) + from this obtain i' where "i = Suc i'" by auto + hence "i' < hd ec" using \i \ hd ec\ by simp + have "(u # v # l) ! i = (v#l) ! i'" using \i = Suc i'\ by simp + also have "... = v" using 3 \ec = eq_comps (v#l)\ \ec = hd ec # (tl ec)\ + by (metis \i' < hd ec\ list.sel(1)) + also have "... = hd (u#v#l)" using \u = v\ by simp + finally show ?thesis . + qed + qed +qed + +lemma eq_comps_singleton: + assumes "[a] = eq_comps l" + shows "a = length l" using assms +proof (induct l arbitrary: a rule: eq_comps.induct) +case 1 +then show ?case by simp +next + case (2 x) + then show ?case by simp +next + case (3 x y l) + define ec where "ec = eq_comps (y#l)" + have "ec = hd ec # (tl ec)" using eq_comps_not_empty[of "y#l"] + unfolding ec_def by simp + show ?case + proof (cases "x = y") + case True + hence "a = Suc (hd ec)" using 3 eq_comps.simps(3)[of x y] + unfolding ec_def Let_def by simp + have "tl ec = []" using 3 True eq_comps.simps(3)[of x y] + unfolding ec_def Let_def by simp + hence "ec = [hd ec]" using \ec = hd ec # tl ec\ by simp + hence "hd ec = length (y#l)" using 3 ec_def by simp + then show ?thesis using \a = Suc (hd ec)\ by simp + next + case False + then show ?thesis using eq_comps_hd_neq_tl 3 + \ec = hd ec # tl ec\ ec_def by fastforce + qed +qed + +lemma eq_comps_leq: + assumes "a#b#m = eq_comps l" + and "sorted l" +shows "hd l < hd (drop a l)" using assms +proof (induct l arbitrary: a b m rule: eq_comps.induct) +case 1 + then show ?case by simp +next + case (2 x) + then show ?case by simp +next + case (3 x y l) + show ?case + proof (cases "x = y") + case True + hence "hd (x#y#l) = y" by simp + define ec where "ec = eq_comps (y#l)" + have "a = Suc (hd (ec))" using True ec_def 3 + eq_comps.simps(3)[of x y] unfolding Let_def by simp + have "b#m = tl ec" using True ec_def 3 + eq_comps.simps(3)[of x y] unfolding Let_def by simp + hence eceq: "ec = hd ec # (hd (tl ec)) # (tl (tl ec))" unfolding ec_def + by (metis eq_comps_not_empty list.exhaust_sel list.simps(3)) + have dra: "drop a (x#y#l) = drop (hd ec) (y#l)" using \a = Suc (hd (ec))\ + by simp + have "sorted (y#l)" using 3 by simp + hence "y < hd (drop (hd ec) (y#l))" using 3(1) eceq unfolding ec_def + by (metis list.sel(1)) + thus ?thesis using True dra by simp + next + case False + hence "a = 1" using 3 by (simp add: Let_def) + have "hd (x#y#l) = x" by simp + moreover have "hd (drop a (x # y # l)) = y" using \a = 1\ by simp + ultimately show ?thesis using False 3 + by (metis order_le_imp_less_or_eq sorted2_simps(2)) + qed +qed + +lemma eq_comps_compare: + assumes "sorted l" + and "a#m = eq_comps l" + and "i < a" + and "a \ j" + and "j < length l" +shows "nth l i < nth l j" using assms +proof (cases "m =[]") + case True + hence "[a] = eq_comps l" using assms by simp + hence "a = length l" using eq_comps_singleton[of a "l"] by simp + then show ?thesis using assms by simp +next + case False + hence "m = hd m # (tl m)" by simp + have "l!i = hd l" using assms eq_comps_eq by metis + also have "... < hd (drop a l)" using eq_comps_leq assms \m = hd m # (tl m)\ + by metis + also have "... \ l!j" using assms + by (metis hd_drop_conv_nth le_less_trans sorted_nth_mono) + finally show ?thesis . +qed + +lemma eq_comps_singleton_elems: + assumes "eq_comps l = [a]" + shows "\i < length l. l!i = l!0" using eq_comps_eq eq_comps_singleton + by (metis assms bot_nat_0.not_eq_extremum eq_comps_neq_0) + +lemma eq_comp_Re: + assumes "\ z \ set l. z \ Reals" + and "m = eq_comps l" +shows "m = eq_comps (map Re l)" using assms +proof (induct l arbitrary:m rule:eq_comps.induct) + case 1 + then show ?case by simp +next + case (2 x) + then show ?case by simp +next + case (3 x y l) + define ec where "ec = eq_comps (y#l)" + have ecr: "ec = eq_comps (map Re (y # l))" using ec_def 3 by simp + show ?case + proof (cases "x = y") + case True + hence "Re x = Re y" by simp + have "m = Suc (hd ec) # (tl ec)" using ec_def 3 True + by (simp add: Let_def) + also have "... = eq_comps (map Re (x#y # l))" using ecr \Re x = Re y\ + by (simp add: Let_def) + finally show ?thesis . + next + case False + hence "Re x \ Re y" using 3 + by (metis list.set_intros(1) list.set_intros(2) of_real_Re) + have "m = 1#ec" using ec_def 3 False + by (simp add: Let_def) + also have "... = eq_comps (map Re (x#y # l))" using ecr \Re x \ Re y\ + by (simp add: Let_def) + finally show ?thesis using ecr unfolding Let_def by simp + qed +qed + +lemma eq_comps_sum_list: + shows "sum_list (eq_comps l) = length l" +proof (induct l rule: eq_comps.induct) + case 1 + then show ?case unfolding diag_mat_def by simp +next + case (2 x) + have "eq_comps [x] = [1]" using eq_comps.simps(2)[of x] by simp + then show ?case by simp +next + case (3 x y l) + then show ?case + proof (cases "x = y") + case True + then show ?thesis using eq_comps.simps(3)[of x y l] 3 + unfolding Let_def + by (metis eq_comps_not_empty hd_Cons_tl length_Cons list.discI + semiring_norm(164) sum_list.Cons) + next + case False + then show ?thesis using eq_comps.simps(3)[of x y l] 3 + unfolding Let_def by simp + qed +qed + +lemma eq_comps_elem_lt: + assumes "1 < length (eq_comps l)" + shows "hd (eq_comps l) < length l" +proof - + define a where "a = hd (eq_comps l)" + define b where "b = hd (tl (eq_comps l))" + define c where "c = tl (tl (eq_comps l))" + have "eq_comps l = a#b#c" using assms unfolding a_def b_def c_def + by (metis eq_comps.simps(2) eq_comps_singleton length_0_conv + less_irrefl_nat less_nat_zero_code list.exhaust_sel) + hence "b#c = eq_comps (drop a l)" using eq_comps_drop by metis + hence "0 < b" using eq_comps_neq_0 by auto + moreover have "0 < a" using \eq_comps l = a#b#c\ eq_comps_neq_0 + by (metis gr0I) + moreover have "a+b \ length l" using eq_comps_sum_list + by (metis \eq_comps l = a # b # c\ le_add1 nat_add_left_cancel_le + sum_list_simps(2)) + ultimately show ?thesis unfolding a_def by auto +qed + +lemma eq_comp_sum_diag_mat: + shows "sum_list (eq_comps (diag_mat A)) = dim_row A" + using eq_comps_sum_list[of "diag_mat A"] diag_mat_length by simp + +lemma nsum_Suc_elem: + assumes "1 < length (eq_comps l)" + shows "l!(n_sum (Suc i) (eq_comps l)) = + (drop (hd (eq_comps l)) l)!(n_sum i (tl (eq_comps l)))" using assms +proof (induct i arbitrary: l) + case 0 + hence "1 < length l" using eq_comps_length[of l] by presburger + hence "l \ []" by fastforce + hence "l ! n_sum (Suc 0) (eq_comps l) = l ! hd (eq_comps l)" + by (simp add: "0.prems" eq_comps_not_empty hd_conv_nth) + also have "... = hd (drop (hd (eq_comps l)) l)" + by (metis "0.prems" eq_comps_elem_lt hd_drop_conv_nth) + finally show ?case using 0 + by (metis (no_types, opaque_lifting) \l ! hd (eq_comps l) = + hd (drop (hd (eq_comps l)) l)\ \l \ []\ append_Nil2 + eq_comps.simps(1) eq_comps_drop eq_comps_empty_if eq_comps_singleton + hd_conv_nth list.exhaust_sel n_sum.simps(1) nat_arith.rule0 + nth_append_length_plus) +next + case (Suc i) + have "l!(n_sum (Suc (Suc i)) (eq_comps l)) = + l!(hd (eq_comps l) + (n_sum (Suc i) (tl (eq_comps l))))" by simp + also have "... = (drop (hd (eq_comps l)) l)! + (n_sum (Suc i) (tl (eq_comps l)))" + using less_or_eq_imp_le + by (metis Suc.prems eq_comps_elem_lt nth_drop) + finally show ?case . +qed + +lemma eq_comps_elems_eq: + assumes "l\[]" + and "i < length (eq_comps l)" + and "j < (eq_comps l)!i" +shows "l!(n_sum i (eq_comps l)) = l!(n_sum i (eq_comps l) + j)" using assms +proof (induct i arbitrary: l) + case 0 + hence "eq_comps l = hd (eq_comps l)#(tl (eq_comps l))" by simp + have "l ! n_sum 0 (eq_comps l) = hd l" + by (simp add: "0"(1) hd_conv_nth) + also have "... = l!j" using 0 eq_comps_eq + by (metis \eq_comps l = hd (eq_comps l) # tl (eq_comps l)\ nth_Cons_0) + finally show ?case by simp +next + case (Suc i) + show ?case + proof (cases "length (eq_comps l) = 1") + case True + hence "Suc i = 0" using Suc.prems(2) by fastforce + then show ?thesis by simp + next + case False + hence "1 < length (eq_comps l)" using Suc eq_comps_not_empty[of l] + by presburger + hence "l!(n_sum (Suc i) (eq_comps l)) = + (drop (hd (eq_comps l)) l)!(n_sum i (tl (eq_comps l)))" + using nsum_Suc_elem by simp + also have "... = (drop (hd (eq_comps l)) l)! + (n_sum i (eq_comps (drop (hd (eq_comps l)) l)))" + using eq_comps_drop[of "hd (eq_comps l)"] eq_comps_empty_if list.collapse + by fastforce + also have "... = (drop (hd (eq_comps l)) l)! + (n_sum i (eq_comps (drop (hd (eq_comps l)) l)) + j)" + proof (rule Suc(1)) + show "drop (hd (eq_comps l)) l \ []" + by (metis Cons_nth_drop_Suc \1 < length (eq_comps l)\ eq_comps_elem_lt + list.distinct(1)) + show "i < length (eq_comps (drop (hd (eq_comps l)) l))" using Suc + by (metis (no_types, lifting) Suc_lessD eq_comps_drop + eq_comps_not_empty length_Suc_conv list.collapse + not_less_less_Suc_eq) + show "j < eq_comps (drop (hd (eq_comps l)) l) ! i" using Suc + by (metis eq_comps_drop length_Suc_conv less_natE list.exhaust_sel + list.simps(3) nth_Cons_Suc) + qed + also have "... = (drop (hd (eq_comps l)) l)! + (n_sum i (tl (eq_comps l)) + j)" + by (metis Suc(2) eq_comps_drop eq_comps_not_empty hd_Cons_tl) + also have "... = l!(n_sum (Suc i) (eq_comps l) + j)" + by (metis (no_types, opaque_lifting) Groups.add_ac(2) + Groups.add_ac(3) \1 < length (eq_comps l)\ eq_comps_elem_lt + less_or_eq_imp_le n_sum.simps(2) nth_drop) + finally show ?thesis . + qed +qed + +text \When the diagonal block matrices are extracted using \verb+eq_comp+, each extracted +matrix is a multiple of the identity.\ + +lemma extract_subdiags_eq_comp: + fixes A::"complex Matrix.mat" + assumes "diagonal_mat A" + and "A\ carrier_mat n n" + and "0 < n" + and "i < length (eq_comps (diag_mat A))" + shows "\k. (extract_subdiags A (eq_comps (diag_mat A)))!i = + k \\<^sub>m (1\<^sub>m ((eq_comps (diag_mat A))!i))" +proof + define l where "l = diag_mat A" + define k where "k = l!(n_sum i (eq_comps l))" + show "extract_subdiags A (eq_comps (diag_mat A)) ! i = + k \\<^sub>m 1\<^sub>m (eq_comps (diag_mat A) ! i)" + proof (rule eq_matI, auto simp add: assms) + show dr: "dim_row (extract_subdiags A (eq_comps (diag_mat A)) ! i) = + eq_comps (diag_mat A) ! i" + using extract_subdiags_carrier assms carrier_matD(1) by blast + show dc: "dim_col (extract_subdiags A (eq_comps (diag_mat A)) ! i) = + eq_comps (diag_mat A) ! i" + using extract_subdiags_carrier assms carrier_matD by blast + fix m np + assume "m < eq_comps (diag_mat A)!i" and "np < eq_comps (diag_mat A)!i" + and "m\ np" note mnp=this + have "diagonal_mat (extract_subdiags A (eq_comps (diag_mat A)) !i)" + proof (rule extract_subdiags_diagonal) + show "diagonal_mat A" using assms by simp + show "A\ carrier_mat n n" using assms by simp + show "eq_comps (diag_mat A) \ []" using assms unfolding diag_mat_def + by auto + show "sum_list (eq_comps (diag_mat A)) \ n" + using assms eq_comps_sum_list unfolding diag_mat_def + by (metis carrier_matD(1) carrier_matD(2) length_cols_mat_to_cols_list + length_map order.eq_iff) + show "i < length (eq_comps (diag_mat A))" using assms by simp + qed + thus "extract_subdiags A (eq_comps (diag_mat A)) ! i $$ (m, np) = 0" + using mnp dr dc by (metis diagonal_mat_def) + next + fix p + assume "p < eq_comps (diag_mat A) ! i" + have "extract_subdiags A (eq_comps (diag_mat A)) ! i $$ (p, p) = + diag_mat A! (n_sum i (eq_comps (diag_mat A)) + p)" + proof (rule extract_subdiags_diag_elem) + show "A\ carrier_mat n n" "0 < n" "i < length (eq_comps (diag_mat A))" + using assms by auto + show ne: "eq_comps (diag_mat A) \ []" using assms by auto + show "p < eq_comps (diag_mat A) ! i" + using \p < eq_comps (diag_mat A) ! i\ . + show "sum_list (eq_comps (diag_mat A)) \ n" + using assms eq_comps_sum_list[of "diag_mat A"] + unfolding diag_mat_def by simp + show "\j []" using assms unfolding diag_mat_def by simp + show "p < eq_comps (diag_mat A) ! i" + using \p < eq_comps (diag_mat A) ! i\ . + show "i < length (eq_comps (diag_mat A))" using assms by simp + qed + finally show + "extract_subdiags A (eq_comps (diag_mat A)) ! i $$ (p, p) = k" . + qed +qed + +lemma extract_subdiags_comp_commute: + fixes A::"complex Matrix.mat" + assumes "diagonal_mat A" + and "A\ carrier_mat n n" + and "0 < n" + and "i < length (eq_comps (diag_mat A))" + and "B \ carrier_mat ((eq_comps (diag_mat A))!i) ((eq_comps (diag_mat A))!i)" + shows "(extract_subdiags A (eq_comps (diag_mat A)))!i * B = + B * (extract_subdiags A (eq_comps (diag_mat A)))!i" +proof - + define m where "m = (eq_comps (diag_mat A))!i" + have "\k. (extract_subdiags A (eq_comps (diag_mat A)))!i = + k \\<^sub>m (1\<^sub>m ((eq_comps (diag_mat A))!i))" + using assms extract_subdiags_eq_comp by simp + from this obtain k where + "(extract_subdiags A (eq_comps (diag_mat A)))!i = + k \\<^sub>m (1\<^sub>m m)" unfolding m_def by auto note kprop = this + hence "(extract_subdiags A (eq_comps (diag_mat A)))!i * B = + k \\<^sub>m (1\<^sub>m m) * B" by simp + also have "... = B * (k \\<^sub>m (1\<^sub>m m))" using assms m_def + by (metis left_mult_one_mat mult_smult_assoc_mat + mult_smult_distrib one_carrier_mat right_mult_one_mat) + finally show ?thesis using kprop by simp +qed + +text \In particular, extracting the diagonal sub-blocks of a diagonal matrix leaves +it unchanged. \ + +lemma diagonal_extract_eq: + assumes "B\ carrier_mat n n" + and "diagonal_mat B" +shows "B = diag_block_mat (extract_subdiags B (eq_comps (diag_mat B)))" +proof (rule diag_compat_extract_subdiag) + define eqcl where "eqcl= eq_comps (diag_mat B)" + show "B \ carrier_mat n n" using assms by simp + show "diag_compat B eqcl" + proof (rule diag_compat_diagonal) + show "B \ carrier_mat (dim_row B) (dim_row B)" + using assms by simp + show "diagonal_mat B" using assms by simp + have "dim_row B = length (diag_mat B)" unfolding diag_mat_def by simp + also have "... = sum_list eqcl" using eq_comps_sum_list[of "diag_mat B"] + unfolding eqcl_def by simp + finally show "dim_row B = sum_list eqcl". + qed +qed + +fun lst_diff where + "lst_diff l [] = (l = [])" +| "lst_diff l (x#xs) = (x \ length l \ + (\i j. i < x \ x \ j \ j < length l \ nth l i < nth l j) \ + lst_diff (drop x l) xs)" + +lemma sorted_lst_diff: + assumes "sorted l" + and "m = eq_comps l" +shows "lst_diff l m" using assms +proof (induct m arbitrary: l) + case Nil + hence "l = []" using eq_comps_empty_if[of l] by simp + then show ?case by simp +next + case (Cons a m) + have "sorted (drop a l)" using Cons sorted_drop by simp + moreover have "m = eq_comps (drop a l)" using eq_comps_drop Cons by simp + ultimately have "lst_diff (drop a l) m" using Cons by simp + have "a \ length l" using eq_comps_elem_le_length Cons by simp + have "(\i j. i < a \ a \ j \ j < length l \ nth l i < nth l j)" + using Cons eq_comps_compare by blast + then show ?case using \a \ length l\ \lst_diff (drop a l) m\ by fastforce +qed + +lemma lst_diff_imp_diag_diff: + fixes D::"'a::preorder Matrix.mat" + assumes "D\ carrier_mat n n" + and "lst_diff (diag_mat D) m" + shows "diag_diff D m" using assms +proof (induct arbitrary: n rule:diag_diff.induct) + case (1 D) + hence "diag_mat D = []" by simp + hence "dim_row D = 0" unfolding diag_mat_def by simp + hence "n= 0" using 1 by simp + hence "dim_col D = 0" using 1 by simp + then show ?case using \dim_row D = 0\ by simp +next + case (2 D a xs) + define D1 where "D1 = fst (split_block D a a)" + define D2 where "D2 = fst (snd (split_block D a a))" + define D3 where "D3 = fst (snd (snd (split_block D a a)))" + define D4 where "D4 = snd (snd (snd (split_block D a a)))" + have spd: "split_block D a a = (D1, D2, D3, D4)" using fst_conv snd_conv + unfolding D1_def D2_def D3_def D4_def by simp + have "length (diag_mat D) = n" using 2 unfolding diag_mat_def by simp + hence "a \ n" using 2 by simp + hence c1: "D1 \ carrier_mat a a" + using split_block(1)[OF spd, of "n-a" "n-a"] 2 by simp + have c4: "D4 \ carrier_mat (n-a) (n-a)" + using 2 split_block(4)[OF spd] \a \ n\ by simp + have "diag_mat D = diag_mat D1 @ (diag_mat D4)" + using diag_four_block_mat split_block(5) + by (metis "2"(2) \a \ n\ c1 c4 carrier_matD(1) carrier_matD(2) + le_Suc_ex spd) + have "length (diag_mat D1) = a" using c1 unfolding diag_mat_def by simp + hence "diag_mat D4 = drop a (diag_mat D)" + using \diag_mat D = diag_mat D1 @ (diag_mat D4)\ by simp + hence "lst_diff (diag_mat D4) xs" using 2 by simp + hence "diag_diff D4 xs" using 2(1)[OF spd[symmetric]] spd c4 + by blast + have "(\i j. i < dim_row D1 \ j < dim_row D4 \ D1$$(i,i) < D4 $$ (j,j))" + proof (intro allI impI) + fix i j + assume ijp: "i < dim_row D1 \ j < dim_row D4" + hence "i < a" using c1 by simp + have "j+a < n" using c4 ijp by (metis carrier_matD(1) less_diff_conv) + have "D1 $$ (i,i) = D $$ (i,i)" using spd \i < a\ + unfolding split_block_def Let_def by force + also have "... = (diag_mat D)!i" using \i < a\ \a \ n\ 2 + unfolding diag_mat_def by simp + also have "... < (diag_mat D)!(j+a)" using 2 \j+a < n\ + by (metis \i < a\ \length (diag_mat D) = n\ + le_add2 lst_diff.simps(2)) + also have "... = D $$ (j+a, j+a)" using \j+a < n\ 2 + unfolding diag_mat_def by simp + also have "... = D4 $$ (j,j)" using spd ijp 2 + unfolding split_block_def Let_def by force + finally show "D1$$(i,i) < D4 $$ (j,j)" . + qed + hence "(\i j. i < dim_row D1 \ j < dim_row D4 \ D1$$(i,i) \ D4 $$ (j,j))" + by (metis order_less_irrefl) + thus ?case using \diag_diff D4 xs\ \a \ n\ 2 spd by simp +qed + +lemma sorted_diag_diff: + fixes D::"'a::linorder Matrix.mat" + assumes "D\ carrier_mat n n" + and "sorted (diag_mat D)" +shows "diag_diff D (eq_comps (diag_mat D))" +proof (rule lst_diff_imp_diag_diff) + show "D \ carrier_mat n n" using assms by simp + show "lst_diff (diag_mat D) (eq_comps (diag_mat D))" + using sorted_lst_diff[of "diag_mat D"] assms by simp +qed + +lemma Re_sorted_lst_diff: + fixes l::"complex list" + assumes "\ z \ set l. z \ Reals" + and "sorted (map Re l)" + and "m = eq_comps l" +shows "lst_diff l m" using assms +proof (induct m arbitrary: l) + case Nil + hence "l = []" using eq_comps_empty_if[of l] by simp + then show ?case by simp +next + case (Cons a m) + have "sorted (map Re (drop a l))" using Cons sorted_drop + by (metis drop_map) + moreover have "m = eq_comps (drop a l)" using eq_comps_drop Cons by simp + ultimately have "lst_diff (drop a l) m" using Cons + by (metis in_set_dropD) + have "a \ length l" using eq_comps_elem_le_length Cons by simp + have "(\i j. i < a \ a \ j \ j < length l \ nth l i < nth l j)" + proof (intro allI impI) + fix i j + assume asm: "i < a \ a \ j \ j < length l" + hence "Re (l!i) < Re (l!j)" + using Cons eq_comps_compare eq_comp_Re + by (smt (z3) dual_order.strict_trans dual_order.strict_trans1 length_map + nth_map) + moreover have "l!i \ Reals" using asm Cons by simp + moreover have "l!j \ Reals" using asm Cons by simp + ultimately show "nth l i < nth l j" using less_complex_def + by (simp add: complex_is_Real_iff) + qed + then show ?case using \a \ length l\ \lst_diff (drop a l) m\ by fastforce +qed + +text \The following lemma states a sufficient condition for the \verb+diag_diff+ predicate +to hold.\ + +lemma cpx_sorted_diag_diff: + fixes D::"complex Matrix.mat" + assumes "D\ carrier_mat n n" + and "\ i < n. D$$(i,i) \ Reals" + and "sorted (map Re (diag_mat D))" +shows "diag_diff D (eq_comps (diag_mat D))" +proof (rule lst_diff_imp_diag_diff) + show "D \ carrier_mat n n" using assms by simp + have "\z\set (diag_mat D). z \ \" using assms unfolding diag_mat_def by auto + thus "lst_diff (diag_mat D) (eq_comps (diag_mat D))" + using Re_sorted_lst_diff[of "diag_mat D"] assms by simp +qed + +section \Sorted hermitian decomposition\ +text \We prove that any Hermitian matrix $A$ can be decomposed into a product +$U^\dagger \cdot B \cdot U$, where $U$ is a unitary matrix and $B$ is a diagonal matrix +containing only real components which are ordered along the diagonal.\ + +definition per_col where +"per_col A f = Matrix.mat (dim_row A) (dim_col A) (\ (i,j). A $$(i, (f j)))" + +lemma per_col_carrier: + assumes "A \ carrier_mat n m" + shows "per_col A f \ carrier_mat n m" using assms unfolding per_col_def + by simp + +lemma per_col_col: + assumes "A \ carrier_mat n m" + and "j < m" +shows "Matrix.col (per_col A f) j = Matrix.col A (f j)" +proof + show dim: "dim_vec (Matrix.col (per_col A f) j) = + dim_vec (Matrix.col A (f j))" + using per_col_carrier by (metis assms(1) carrier_matD(1) dim_col) + fix i + assume "i < dim_vec (Matrix.col A (f j))" + hence "i < dim_vec (Matrix.col (per_col A f) j)" using dim by simp + hence "vec_index (Matrix.col (per_col A f) j) i = (per_col A f)$$(i,j)" + unfolding Matrix.col_def by simp + also have "... = A $$(i, (f j))" unfolding per_col_def + using \i < dim_vec (Matrix.col A (f j))\ assms by fastforce + also have "... = vec_index (Matrix.col A (f j)) i" unfolding Matrix.col_def + using \i < dim_vec (Matrix.col A (f j))\ by auto + finally show "vec_index (Matrix.col (per_col A f) j) i = + vec_index (Matrix.col A (f j)) i" . +qed + +lemma per_col_adjoint_row: + assumes "A \ carrier_mat n n" + and "i < n" + and "f i < n" +shows "Matrix.row (Complex_Matrix.adjoint (per_col A f)) i = + Matrix.row (Complex_Matrix.adjoint A) (f i)" +proof - + have "per_col A f \ carrier_mat n n" using assms per_col_carrier[of A] + by simp + hence "Matrix.row (Complex_Matrix.adjoint (per_col A f)) i = + conjugate (Matrix.col (per_col A f) i)" + using assms adjoint_row[of i "per_col A f"] by simp + also have "... = conjugate (Matrix.col A (f i))" using assms per_col_col + by simp + also have "... = Matrix.row (Complex_Matrix.adjoint A) (f i)" using assms + adjoint_row[of "f i" A] by simp + finally show ?thesis . +qed + +lemma per_col_mult_adjoint: + assumes "A \ carrier_mat n n" + and "i < n" + and "j < n" + and "f i < n" + and "f j < n" +shows "((Complex_Matrix.adjoint (per_col A f)) * (per_col A f))$$(i,j) = + ((Complex_Matrix.adjoint A) * A)$$(f i, f j)" +proof - + have "((Complex_Matrix.adjoint (per_col A f)) * (per_col A f))$$(i,j) = + Matrix.scalar_prod (Matrix.row (Complex_Matrix.adjoint (per_col A f)) i) + (Matrix.col A (f j))" using assms per_col_col unfolding times_mat_def + by (metis adjoint_dim_row carrier_matD(2) dim_col_mat(1) index_mat(1) + old.prod.case per_col_def) + also have "... = Matrix.scalar_prod + (Matrix.row (Complex_Matrix.adjoint A) (f i)) + (Matrix.col A (f j))" using assms per_col_adjoint_row by metis + also have "... = ((Complex_Matrix.adjoint A) * A)$$(f i, f j)" using assms + unfolding times_mat_def by simp + finally show ?thesis . +qed + +lemma idty_index: + assumes "bij_betw f {..< n} {..< n}" + and "i < n" + and "j < n" +shows "(1\<^sub>m n)$$(i,j) = (1\<^sub>m n)$$(f i, f j)" +proof - + have "f i < n" "f j < n" using assms bij_betwE by auto + show ?thesis + proof (cases "i = j") + case True + then show ?thesis using \f i < n\ assms by simp + next + case False + hence "f i \ f j" using assms + by (metis bij_betw_iff_bijections lessThan_iff) + then show ?thesis + by (metis \f i < n\ \f j < n\ assms(2) assms(3) index_one_mat(1)) + qed +qed + +lemma per_col_unitary: + assumes "A\ carrier_mat n n" + and "unitary A" + and "bij_betw f {..< n} {..< n}" +shows "unitary (per_col A f)" unfolding unitary_def +proof + show pc: "per_col A f \ + carrier_mat (dim_row (per_col A f)) (dim_row (per_col A f))" + using assms per_col_carrier by (metis carrier_matD(1)) + have "dim_row (per_col A f) = n" using assms per_col_carrier + by (metis carrier_matD(1)) + moreover have "(Complex_Matrix.adjoint (per_col A f)) * (per_col A f) = 1\<^sub>m n" + proof (rule eq_matI) + show "dim_row (Complex_Matrix.adjoint (per_col A f) * per_col A f) = + dim_row (1\<^sub>m n)" using pc + by (metis adjoint_dim_row calculation carrier_matD(2) index_mult_mat(2) + index_one_mat(2)) + thus "dim_col (Complex_Matrix.adjoint (per_col A f) * per_col A f) = + dim_col (1\<^sub>m n)" by auto + fix i j + assume "i < dim_row (1\<^sub>m n)" and "j < dim_col (1\<^sub>m n)" note ij = this + have "(Complex_Matrix.adjoint (per_col A f) * per_col A f) $$ (i, j) = + (Complex_Matrix.adjoint A * A) $$ (f i, f j)" + proof (rule per_col_mult_adjoint) + show "A\ carrier_mat n n" using assms by simp + show "i < n" "j < n" using ij by auto + thus "f i < n" using assms by (meson bij_betw_apply lessThan_iff) + show "f j < n" using \j < n\ assms by (meson bij_betw_apply lessThan_iff) + qed + also have "... = (1\<^sub>m n) $$ (f i, f j)" using assms + unfolding Complex_Matrix.unitary_def + by (metis assms(2) unitary_simps(1)) + also have "... = (1\<^sub>m n) $$ (i,j)" using idty_index[of f n i j] assms ij + by auto + finally show "(Complex_Matrix.adjoint (per_col A f) * + per_col A f) $$ (i, j) = 1\<^sub>m n $$ (i, j)" . + qed + ultimately show "inverts_mat (per_col A f) + (Complex_Matrix.adjoint (per_col A f))" + using inverts_mat_symm inverts_mat_def + by (metis (no_types, lifting) adjoint_dim_col adjoint_dim_row + carrier_mat_triv index_mult_mat(3) index_one_mat(3)) +qed + +definition per_diag where +"per_diag A f = Matrix.mat (dim_row A) (dim_col A) (\ (i,j). A $$(f i, (f j)))" + +lemma per_diag_carrier: + shows "per_diag A f \ carrier_mat (dim_row A) (dim_col A)" + unfolding per_diag_def by simp + +lemma per_diag_diagonal: + assumes "D\ carrier_mat n n" + and "diagonal_mat D" + and "bij_betw f {..< n} {..< n}" +shows "diagonal_mat (per_diag D f)" unfolding diagonal_mat_def +proof (intro allI impI) + fix i j + assume "i < dim_row (per_diag D f)" and "j < dim_col (per_diag D f)" + and "i\ j" note asm = this + hence "f i \ f j" using assms + by (metis bij_betw_iff_bijections carrier_matD(1) carrier_matD(2) + lessThan_iff per_diag_carrier) + moreover have "f i < n" using assms asm + by (metis bij_betwE carrier_matD(1) lessThan_iff per_diag_carrier) + moreover have "f j < n" using assms asm + by (metis bij_betwE carrier_matD(2) lessThan_iff per_diag_carrier) + ultimately show "per_diag D f $$ (i, j) = 0" using assms + unfolding per_diag_def diagonal_mat_def + by (metis asm(1) asm(2) carrier_matD(1) carrier_matD(2) + dim_col_mat(1) dim_row_mat(1) index_mat(1) old.prod.case per_diag_def) +qed + +lemma per_diag_diag_mat: + assumes "A \ carrier_mat n n" + and "i < n" + and "f i < n" +shows "diag_mat (per_diag A f)!i = diag_mat A ! (f i)" + using assms unfolding diag_mat_def per_diag_def by auto + +lemma per_diag_diag_mat_Re: + assumes "A \ carrier_mat n n" + and "i < n" + and "f i < n" +shows "map Re (diag_mat (per_diag A f))!i = map Re (diag_mat A) ! (f i)" +proof - + have "map Re (diag_mat (per_diag A f))!i = Re (diag_mat (per_diag A f)!i)" + proof (rule nth_map) + show "i < length (diag_mat (per_diag A f))" + using assms unfolding diag_mat_def + by (metis carrier_matD(1) carrier_matD(2) length_cols_mat_to_cols_list + length_map per_diag_carrier) + qed + also have "... = Re (diag_mat A ! (f i))" using assms per_diag_diag_mat + by metis + also have "... = map Re (diag_mat A) ! (f i)" unfolding diag_mat_def + using assms by auto + finally show ?thesis . +qed + +lemma per_diag_real: + fixes B::"complex Matrix.mat" + assumes "B\ carrier_mat n n" + and "\i< n. B$$(i,i) \ Reals" + and "bij_betw f {..j Reals" +proof (intro allI impI) + fix j + assume "j < n" + hence "per_diag B f $$ (j,j) = B $$ (f j, f j)" + using assms unfolding per_diag_def by simp + also have "... \ Reals" using assms \j < n\ bij_betwE by blast + finally show "per_diag B f $$ (j,j) \ Reals" . +qed + +lemma per_col_mult_unitary: + fixes A::"complex Matrix.mat" + assumes "A \ carrier_mat n n" + and "unitary A" + and "D\ carrier_mat n n" + and "diagonal_mat D" + and "0 < n" + and "bij_betw f {..< n} {..< n}" +shows "A * D * (Complex_Matrix.adjoint A) = + (per_col A f) * (per_diag D f) * (Complex_Matrix.adjoint (per_col A f))" + (is "?L = ?R") +proof - + have row: "dim_row ?L = dim_row ?R" using per_col_carrier assms + by (metis carrier_matD(1) index_mult_mat(2)) + have col: "dim_col ?L = dim_col ?R" using per_col_carrier assms + by (metis adjoint_dim carrier_matD(2) index_mult_mat(3)) + define fc::"complex Matrix.mat set" where "fc = carrier_mat n n" + interpret cpx_sq_mat n n fc + proof + show "0 < n" using assms by simp + qed (auto simp add: fc_def) + define h where + "h = (\i. (if i < n then diag_mat D ! i \\<^sub>m rank_1_proj (Matrix.col A i) + else (0\<^sub>m n n)))" + define g where + "g = (\i. (if i < n + then diag_mat D ! (f i) \\<^sub>m rank_1_proj (Matrix.col A (f i)) + else (0\<^sub>m n n)))" + have "f ` {..i. g i \ fc" unfolding g_def fc_def + by (metis adjoint_dim_col assms(1) carrier_matD(1) carrier_matI + dim_col fc_mats_carrier rank_1_proj_adjoint rank_1_proj_dim + smult_carrier_mat zero_mem) + moreover have h:"\i. h i \ fc" unfolding h_def fc_def + by (metis assms(1) carrier_matD(1) dim_col fc_mats_carrier + rank_1_proj_carrier smult_carrier_mat zero_mem) + moreover have "inj_on f {..x. x \ {.. h (f x) = g x" unfolding h_def g_def + by (meson assms(6) bij_betwE lessThan_iff) + ultimately have "sum_mat g {..f ` {.. by simp + also have "... =sum_mat (\i. diag_mat D ! i \\<^sub>m rank_1_proj (Matrix.col A i)) + {..i. i < n \ diag_mat D ! i \\<^sub>m rank_1_proj (Matrix.col A i) \ fc" + using assms unfolding fc_def by (metis fc_mats_carrier h h_def) + show "\i. i < n \ diag_mat D ! i \\<^sub>m rank_1_proj (Matrix.col A i) \ fc" + using assms unfolding fc_def by (metis fc_mats_carrier h h_def) + qed + also have "... = A * D * (Complex_Matrix.adjoint A)" + using weighted_sum_rank_1_proj_unitary assms unfolding fc_def by simp + finally have sg: "sum_mat g {..i. diag_mat (per_diag D f) ! i \\<^sub>m + rank_1_proj (Matrix.col (per_col A f) i)) {.. fc" using per_col_carrier[of A] assms unfolding fc_def + by simp + show "per_diag D f \ fc" using per_diag_carrier[of D] assms + unfolding fc_def by simp + show "diagonal_mat (per_diag D f)" using assms per_diag_diagonal[of D] + by simp + show "unitary (per_col A f)" using per_col_unitary[of A] assms by simp + qed + also have "... = sum_mat g {..i. i < n \ diag_mat (per_diag D f) ! i \\<^sub>m + rank_1_proj (Matrix.col (per_col A f) i) \ fc" + proof - + fix i + assume "i < n" + have "dim_vec (Matrix.col (per_col A f) i) = n" using assms per_col_col + by (metis carrier_matD(1) dim_col) + hence "rank_1_proj (Matrix.col (per_col A f) i) \ fc" unfolding fc_def + using rank_1_proj_carrier by blast + thus "diag_mat (per_diag D f) ! i \\<^sub>m + rank_1_proj (Matrix.col (per_col A f) i) \ fc" unfolding fc_def by simp + qed + show "\i. i < n \ diag_mat D ! f i \\<^sub>m + rank_1_proj (Matrix.col A (f i)) \ fc" + proof - + fix i + assume "i < n" + hence "f i < n" using \f ` {.. by auto + hence "dim_vec (Matrix.col A (f i)) = n" using assms + by (metis carrier_matD(1) dim_col) + hence "rank_1_proj (Matrix.col A (f i)) \ fc" unfolding fc_def + using rank_1_proj_carrier by blast + thus "diag_mat D ! f i \\<^sub>m rank_1_proj (Matrix.col A (f i)) \ fc" + unfolding fc_def by simp + qed + show "\i. i < n \ + diag_mat (per_diag D f) ! i \\<^sub>m + rank_1_proj (Matrix.col (per_col A f) i) = + diag_mat D ! f i \\<^sub>m rank_1_proj (Matrix.col A (f i))" + proof- + fix i + assume "i < n" + hence "f i < n" using \f ` {.. by auto + have "Matrix.col (per_col A f) i = Matrix.col A (f i)" + using per_col_col assms \i < n\ by simp + hence "rank_1_proj (Matrix.col (per_col A f) i) = + rank_1_proj (Matrix.col A (f i))" by simp + thus "diag_mat (per_diag D f) ! i \\<^sub>m + rank_1_proj (Matrix.col (per_col A f) i) = + diag_mat D ! f i \\<^sub>m rank_1_proj (Matrix.col A (f i))" + using assms per_diag_diag_mat[of D] \i < n\ \f i < n\ by simp + qed + qed + also have "... = A * D * (Complex_Matrix.adjoint A)" using sg by simp + finally have "(per_col A f) * (per_diag D f) * + (Complex_Matrix.adjoint (per_col A f)) = + A * D * (Complex_Matrix.adjoint A)" . + thus ?thesis by simp +qed + +lemma sort_permutation: + assumes "m = sort l" + obtains f where "bij_betw f {.. + (\ilength l = length m\ mset_eq_permutation) note pprop = this + have "bij_betw p {..length l = length m\ + by (simp add: permutes_imp_bij) + moreover have "\ilength l = length m\ permute_list_nth) + ultimately have "\f. bij_betw f {.. + (\i carrier_mat n n" + obtains f where "bij_betw f {..< n} {..< n} \ + map Re (diag_mat (per_diag B f)) = sort (map Re (diag_mat B))" +proof - + define m where "m = sort (map Re (diag_mat B))" + have "length m = length (map Re (diag_mat B))" unfolding m_def by simp + also have "... = length (diag_mat B)" by simp + also have "... = n" using assms unfolding diag_mat_def by simp + finally have "length m = n" . + from this obtain f where "bij_betw f {.. + (\ilength m = n\ unfolding diag_mat_def + by (metis carrier_matD(1) length_map map_nth) + have "map Re (diag_mat (per_diag B f)) = m" + proof (rule list_eq_iff_nth_eq[THEN iffD2], intro conjI) + show "length (map Re (diag_mat (per_diag B f))) = length m" using l by simp + have "\i carrier_mat n n" using assms by simp + show "i < n" using \i < n\ . + thus "f i < n" using fprop bij_betwE by blast + qed + also have "... = m!i" using fprop \i < n\ by simp + finally show "(map Re (diag_mat (per_diag B f)))!i = m!i" . + qed + thus "\ilength m = n\ by simp + qed + thus ?thesis using that fprop unfolding m_def by auto +qed + +lemma bij_unitary_diag: + fixes A::"complex Matrix.mat" + assumes "unitary_diag A B U" + and "A \ carrier_mat n n" + and "bij_betw f {.. carrier_mat n n" using assms by simp + moreover have "per_diag B f \ carrier_mat n n" using assms unitary_diagD(1) + per_diag_carrier[of B] + by (metis carrier_matD(1) carrier_matD(2) similar_mat_witD2(5)) + moreover have "per_col U f \ carrier_mat n n" using assms unitary_diagD(1) + per_col_carrier[of U] + by (metis similar_mat_witD2(6)) + moreover hence "Complex_Matrix.adjoint (per_col U f) \ carrier_mat n n" + by (simp add: adjoint_dim) + ultimately show + "{A, per_diag B f, per_col U f, Complex_Matrix.adjoint (per_col U f)} \ + carrier_mat (dim_row A) (dim_row A)" by auto + show "per_col U f * Complex_Matrix.adjoint (per_col U f) = 1\<^sub>m (dim_row A)" + using \Complex_Matrix.unitary (per_col U f)\ assms(2) + \per_col U f \ carrier_mat n n\ by auto + show "Complex_Matrix.adjoint (per_col U f) * per_col U f = 1\<^sub>m (dim_row A)" + using \Complex_Matrix.unitary (per_col U f)\ assms + \per_col U f \ carrier_mat n n\ by auto + qed (simp add: eq) +qed + +lemma hermitian_real_diag_sorted: + assumes "A \ carrier_mat n n" + and "0 < n" + and "hermitian A" + obtains Bs Us where "real_diag_decomp A Bs Us \ sorted (map Re (diag_mat Bs))" +proof - + obtain U1 B1 where "real_diag_decomp A B1 U1" + using hermitian_real_diag_decomp[of A] assms by auto note ubprop = this + hence "B1 \ carrier_mat n n" using assms unfolding real_diag_decomp_def + by (meson unitary_diag_carrier(1)) + from this obtain f where "bij_betw f {..< n} {..< n} \ + map Re (diag_mat (per_diag B1 f)) = sort (map Re (diag_mat B1))" + using per_diag_sorted_Re by auto note fprop = this + define Bs where "Bs = per_diag B1 f" + define Us where "Us = per_col U1 f" + have "unitary_diag A Bs Us" unfolding Bs_def Us_def + proof (rule bij_unitary_diag) + show "unitary_diag A B1 U1" using ubprop unfolding real_diag_decomp_def + by simp + show "A \ carrier_mat n n" using assms by simp + show "bij_betw f {..unitary_diag A Bs Us\) + show "\i \" unfolding Bs_def + proof (rule per_diag_real) + show br: "B1 \ carrier_mat (dim_row (per_diag B1 f)) + (dim_row (per_diag B1 f))" + by (metis \B1 \ carrier_mat n n\ carrier_matD(1) per_diag_carrier) + thus "\i \" using ubprop by auto + show "bij_betw f {..B1 \ carrier_mat n n\ carrier_matD(1)) + qed + qed + moreover have "sorted (map Re (diag_mat Bs))" using fprop unfolding Bs_def + by simp + ultimately show ?thesis using that by simp +qed + +section \Commuting Hermitian families\ +text \This part is devoted to the proof that a finite family of commuting Hermitian matrices +is simultaneously diagonalizable.\ + +subsection \Intermediate properties\ + +lemma real_diag_decomp_mult_dbm_unit: + assumes "A \ carrier_mat n n" + and "real_diag_decomp A B U" + and "B = diag_block_mat Bl" + and "length Ul = length Bl" + and "\i < length Bl. dim_col (Bl!i) = dim_row (Bl!i)" + and "\i < length Bl. dim_row (Bl!i) = dim_row (Ul!i)" + and "\i < length Bl. dim_col (Bl!i) = dim_col (Ul!i)" + and "unitary (diag_block_mat Ul)" + and "\i carrier_mat n n" + by (meson assms(1) assms(2) real_diag_decompD(1) unitary_diag_carrier(1)) + have "dim_row (diag_block_mat Ul) = dim_row B" + using diag_block_mat_dim_row_cong assms by blast + moreover have "dim_col (diag_block_mat Ul) = dim_col B" + using diag_block_mat_dim_col_cong assms by blast + ultimately have "diag_block_mat Ul \ carrier_mat n n" using assms + by (metis \B \ carrier_mat n n\ carrier_matD(1) carrier_matD(2) + carrier_mat_triv) + define Uf where "Uf = U * (diag_block_mat Ul)" + show "\i. i < dim_row B \ B $$ (i, i) \ \" + using assms real_diag_decompD(2) \B \ carrier_mat n n\ by auto + show "unitary_diag A B Uf" unfolding unitary_diag_def + proof + show "diagonal_mat B" using assms real_diag_decompD(2) + real_diag_decompD(1) unitary_diagD(2) by blast + show "unitarily_equiv A B Uf" unfolding Uf_def + proof (rule conjugate_eq_unitarily_equiv) + show "A\ carrier_mat n n" using assms by simp + show "unitarily_equiv A B U" using assms real_diag_decompD(1) + unfolding unitary_diag_def by simp + show "diag_block_mat Ul \ carrier_mat n n" + using \diag_block_mat Ul \ carrier_mat n n\ . + show "unitary (diag_block_mat Ul)" using assms by simp + have "mat_conj (diag_block_mat Ul) (diag_block_mat Bl) = + diag_block_mat Bl" + proof (rule mat_conj_unit_commute) + show "unitary (diag_block_mat Ul)" using \unitary (diag_block_mat Ul)\ . + show "diag_block_mat Bl \ carrier_mat n n" + using assms \B \ carrier_mat n n\ by simp + show "diag_block_mat Ul \ carrier_mat n n" + using \diag_block_mat Ul \ carrier_mat n n\ . + show "diag_block_mat Ul * diag_block_mat Bl = + diag_block_mat Bl * diag_block_mat Ul" + proof (rule diag_block_mat_commute) + show "length Ul = length Bl" using assms + by simp + show comm: "\iiiB = diag_block_mat Bl\ unfolding mat_conj_def by simp + qed + qed +qed + +lemma real_diag_decomp_block_set: + assumes "Als \ {}" + and "0 < n" + and "\ Al \ Als. length Al = n" + and "\i < n. \ Al \ Als. dim_row (Al!i) = dim_col (Al!i)" + and "\i < n. \U. \ Al \ Als. \B. real_diag_decomp (Al!i) B U" +shows "\Ul. (length Ul = n \ (\i Al \ Als. + (dim_row (Ul!i) = dim_row (Al!i) \ dim_col (Ul!i) = dim_col (Al!i)))\ + (\ Al \ Als. \Bl. (length Bl = n \ + real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) (diag_block_mat Ul))))" + using assms +proof (induct n arbitrary: Als) + case 0 + then show ?case by simp +next + case (Suc n) + hence "\U. \ Al \ Als. \B. real_diag_decomp (Al!0) B U" by simp + from this obtain U0 where "\ Al \ Als. \B. real_diag_decomp (Al!0) B U0" + by auto note u0 = this + have u0_dim: "\Al\Als. + dim_row ([U0] ! 0) = dim_row (Al ! 0) \ + dim_col ([U0] ! 0) = dim_col (Al ! 0)" + proof (intro allI impI ballI) + fix Al + assume "Al \ Als" + have "[U0]!0 = U0" by simp + have "\B. real_diag_decomp (Al!0) B U0" using u0 \Al \ Als\ + by simp + from this obtain B where "real_diag_decomp (Al!0) B U0" by auto + moreover have "dim_row (Al!0) = dim_col (Al!0)" using \Al\ Als\ Suc + by simp + ultimately have "dim_row U0 = dim_row (Al!0)" + using unitary_diag_carrier(2) + by (metis carrier_matD(1) carrier_matI real_diag_decompD(1)) + moreover have "dim_col U0 = dim_col (Al!0)" + using \real_diag_decomp (Al!0) B U0\ \dim_row (Al!0) = dim_col (Al!0)\ + using real_diag_decompD(1) unitary_diag_carrier(2) + by (metis carrier_matD(2) carrier_mat_triv) + ultimately show "dim_row ([U0] ! 0) = dim_row (Al ! 0) \ + dim_col ([U0] ! 0) = dim_col (Al ! 0)" + by simp + qed + show ?case + proof (cases "n = 0") + case True + hence "\ Al \ Als. diag_block_mat Al = Al!0" using Suc + by (simp add: diag_block_mat_length_1) + have "\ Al \ Als. \Bl. (length Bl = 1 \ + real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) + (diag_block_mat [U0]))" + proof + fix Al + assume "Al \ Als" + hence "\B. real_diag_decomp (Al!0) B U0" using u0 by simp + from this obtain B where "real_diag_decomp (Al!0) B U0" by auto + hence "real_diag_decomp (diag_block_mat Al) (diag_block_mat [B]) + (diag_block_mat [U0])" + by (metis \Al \ Als\ \\Al\Als. diag_block_mat Al = Al ! 0\ + diag_block_mat_singleton) + moreover have "length [B] = 1" by simp + ultimately show "\Bl. (length Bl = 1 \ + real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) + (diag_block_mat [U0]))" + by blast + qed + moreover have "length [U0] = 1" by simp + moreover have "\iAl\Als. + dim_row ([U0] ! i) = dim_row (Al ! i) \ + dim_col ([U0] ! i) = dim_col (Al ! i)" + using u0_dim \n = 0\ by simp + ultimately have "length [U0] = Suc 0 \ + (\iAl\Als. dim_row ([U0] ! i) = dim_row (Al ! i) \ + dim_col ([U0] ! i) = dim_col (Al ! i)) \ + (\Al\Als. \Bl. length Bl = Suc n \ real_diag_decomp + (diag_block_mat Al) (diag_block_mat Bl) (diag_block_mat [U0]))" + using \n=0\ One_nat_def by metis + thus ?thesis by (metis True) + next + case False + hence "0 < n" by simp + define tAls where "tAls = tl `Als" + have tex: "\tAl\ tAls. \Al \ Als. tAl = tl Al" unfolding tAls_def by auto + have "\Ul. length Ul = n \ + (\i Al \ tAls. + (dim_row (Ul!i) = dim_row (Al!i) \ dim_col (Ul!i) = dim_col (Al!i)))\ + (\Al\tAls. \Bl. length Bl = n \ + real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) + (diag_block_mat Ul))" + proof (rule Suc(1)) + show "tAls \ {}" "0 < n" unfolding tAls_def by (auto simp add: \0 < n\ Suc) + show "\tAl\tAls. length tAl = n" + using Suc(4) tex by fastforce + show "\iU. \Al\tAls. \B. real_diag_decomp (Al ! i) B U" + proof (intro allI impI) + fix i + assume "i < n" + hence "\U. \Al\Als. \B. real_diag_decomp (Al ! (Suc i)) B U" + using Suc Suc_mono by presburger + from this obtain U where + tu: "\Al\Als. \B. real_diag_decomp (Al ! (Suc i)) B U" by auto + have "\tAl\tAls. \B. real_diag_decomp (tAl ! i) B U" + proof + fix tAl + assume "tAl \ tAls" + hence "\Al \ Als. tAl = tl Al" using tex by simp + from this obtain Al where "Al \ Als" and "tAl = tl Al" by auto + hence "tAl!i = Al!(Suc i)" by (simp add: Suc(4) \i < n\ nth_tl) + moreover have "\B. real_diag_decomp (Al!(Suc i)) B U" + using tu \Al \ Als\ by simp + ultimately show "\B. real_diag_decomp (tAl ! i) B U" by simp + qed + thus "\U. \Al\tAls. \B. real_diag_decomp (Al ! i) B U" by auto + qed + show "\i < n. \Al\tAls. dim_row (Al!i) = dim_col (Al!i)" + by (metis Suc(5) \\tAl\tAls. length tAl = n\ not_less_eq nth_tl tex) + qed + from this obtain Ul where "length Ul = n" and + "\i Al \ tAls. + (dim_row (Ul!i) = dim_row (Al!i) \ dim_col (Ul!i) = dim_col (Al!i))" + "(\Al\tAls. \Bl. length Bl = n \ + real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) + (diag_block_mat Ul))" by auto note ulprop = this + have "\Al\Als. \Bl. length Bl = Suc n \ + real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) + (diag_block_mat (U0#Ul))" + proof + fix Al + assume "Al \ Als" + hence "0 < length Al" using Suc by simp + hence "Al = hd Al # (tl Al)" by simp + have "\B. real_diag_decomp (Al!0) B U0" using u0 \Al\ Als\ by simp + from this obtain B0 where b0: "real_diag_decomp (Al!0) B0 U0" by auto + hence "real_diag_decomp (hd Al) B0 U0" + by (metis \Al = hd Al # tl Al\ nth_Cons_0) + have "tl Al \ tAls" using \Al \ Als\ unfolding tAls_def by simp + hence "\Bl. length Bl = n \ + real_diag_decomp (diag_block_mat (tl Al)) (diag_block_mat Bl) + (diag_block_mat Ul)" using ulprop by simp + from this obtain Bl where "length Bl = n" and + rl: "real_diag_decomp (diag_block_mat (tl Al)) (diag_block_mat Bl) + (diag_block_mat Ul)" by auto + have "dim_row (diag_block_mat (tl Al)) = dim_col (diag_block_mat (tl Al))" + using Suc \Al \ Als\ diag_block_mat_dim_row_col_eq + by (metis (no_types, lifting) \Al = hd Al # tl Al\ length_Cons lessI + less_trans_Suc nth_tl) + moreover have "dim_row (Al ! 0) = dim_col (Al ! 0)" + using Suc \Al \ Als\ by simp + ultimately have "real_diag_decomp (diag_block_mat ((hd Al)#(tl Al))) + (diag_block_mat (B0#Bl)) (diag_block_mat (U0#Ul))" + using four_block_real_diag_decomp[OF rl b0] diag_block_mat.simps(2) + real_diag_decomp_hermitian + by (metis \Al = hd Al # tl Al\ b0 four_block_real_diag_decomp nth_Cons_0 rl) + moreover have "length (B0#Bl) = Suc n" using \length Bl = n\ by simp + ultimately show "\Bl. length Bl = Suc n \ + real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) + (diag_block_mat (U0#Ul))" using \Al = hd Al # tl Al\ by metis + qed + moreover have "length (U0#Ul) = Suc n" using ulprop by simp + moreover have "\iAl\Als. dim_row ((U0#Ul) ! i) = dim_row (Al ! i) \ + dim_col ((U0#Ul) ! i) = dim_col (Al ! i)" + proof (intro allI impI ballI) + fix i Al + assume "i < Suc n" and "Al \ Als" + show "dim_row ((U0 # Ul) ! i) = dim_row (Al ! i) \ + dim_col ((U0 # Ul) ! i) = dim_col (Al ! i)" + proof (cases "i = 0") + case True + then show ?thesis using \Al \ Als\ u0_dim by simp + next + case False + hence "\j. i = Suc j" by (simp add: not0_implies_Suc) + from this obtain j where "i = Suc j" by auto + hence "(U0#Ul)!i = Ul!j" by simp + have "tl Al \ tAls" using \Al \ Als\ unfolding tAls_def by simp + moreover have "Al!i = (tl Al)!j" using \i = Suc j\ + by (metis Suc.prems(3) Zero_not_Suc \Al \ Als\ diag_block_mat.cases + list.sel(3) list.size(3) nth_Cons_Suc) + ultimately show ?thesis using \(U0#Ul)!i = Ul!j\ + by (metis Suc_less_SucD \i < Suc n\ \i = Suc j\ ulprop(2)) + qed + qed + ultimately show ?thesis by blast + qed +qed + +lemma real_diag_decomp_eq_comps_props: + assumes "Ap\ carrier_mat n n" + and "0 < n" + and "real_diag_decomp Ap Bs Us \ sorted (map Re (diag_mat Bs))" +shows "Bs \ carrier_mat n n" "diagonal_mat Bs" "unitary Us" + "Us \ carrier_mat n n" "diag_diff Bs (eq_comps (diag_mat Bs))" + "eq_comps (diag_mat Bs) \ []" "diag_mat Bs \ []" +proof - + show "Bs \ carrier_mat n n" + using assms real_diag_decompD(1) unitary_diag_carrier(1) + by blast + thus "diag_mat Bs \ []" using \0 < n\ unfolding diag_mat_def by simp + show "diagonal_mat Bs" using assms + using real_diag_decompD(1) unitary_diagD(2) by blast + show "unitary Us" + using unitary_diagD(3) assms unfolding real_diag_decomp_def by auto + show "Us \ carrier_mat n n" + using assms real_diag_decompD(1) unitary_diag_carrier(2) + by blast + define eqcl where "eqcl = eq_comps (diag_mat Bs)" + show "diag_diff Bs eqcl" unfolding eqcl_def + proof (rule cpx_sorted_diag_diff) + show "Bs \ carrier_mat n n" using \Bs \ carrier_mat n n\ . + show "sorted (map Re (diag_mat Bs))" using assms by simp + show "\i \" + using assms real_diag_decompD(2) \Bs \ carrier_mat n n\ by auto + qed + show "eqcl \ []" using eq_comps_not_empty[of "diag_mat Bs"] + \Bs \ carrier_mat n n\ assms + unfolding eqcl_def diag_mat_def + by (simp add: assms) +qed + +lemma commuting_conj_mat_set_props: + fixes As::"'a::conjugatable_field Matrix.mat set" + and U::"'a Matrix.mat" + assumes "finite As" + and "card As \ i" + and "\A\ As. hermitian A \ A\ carrier_mat n n" + and "\ A\ As. \ B \ As. A*B = B*A" + and "unitary U" + and "U \ carrier_mat n n" + and "CjA = (\A2. mat_conj (Complex_Matrix.adjoint U) A2)`As" +shows "finite CjA" "card CjA \ i" + "\A\ CjA. A\ carrier_mat n n \ hermitian A" + "\ C1\ CjA. \C2\ CjA. C1*C2 = C2*C1" +proof - + define Cj where "Cj = (\A2. mat_conj (Complex_Matrix.adjoint U) A2)" + have "CjA = Cj`As" using assms unfolding Cj_def by simp + show "finite CjA" using assms by simp + show "card CjA \ i" + using \card As \ i\ \finite As\ card_image_le dual_order.trans assms + by blast + show "\A\ CjA. A\ carrier_mat n n \ hermitian A" + proof(intro ballI conjI) + fix A + assume "A\ CjA" + hence "\nA \ As. A = Cj nA" using assms unfolding Cj_def by auto + from this obtain nA where "nA\ As" and "A = Cj nA" by auto + have "hermitian nA" using assms \nA \ As\ by auto + thus "hermitian A" + using assms \A = Cj nA\ hermitian_mat_conj'[of nA n U] \nA\ As\ Cj_def + mat_conj_adjoint by fastforce + show "A\ carrier_mat n n" using \nA\ As\ \A = Cj nA\ unfolding Cj_def + by (metis \hermitian A\ adjoint_dim_row assms(6) carrier_matD(2) + hermitian_square index_mult_mat(2) mat_conj_adjoint) + qed + show "\ C1\ CjA. \C2\ CjA. C1*C2 = C2*C1" + proof (intro ballI) + fix C1 C2 + assume "C1 \ CjA" and "C2\ CjA" + hence "\ A1\ As. C1 = mat_conj (Complex_Matrix.adjoint U) A1" + using assms unfolding Cj_def by auto + from this obtain A1 where "A1\ As" and + "C1 = mat_conj (Complex_Matrix.adjoint U) A1" + by auto + have "\ A2\ As. C2 = mat_conj (Complex_Matrix.adjoint U) A2" + using \C2\ CjA\ assms unfolding Cj_def by auto + from this obtain A2 where "A2\ As" and + "C2 = mat_conj (Complex_Matrix.adjoint U) A2" + by auto + have "mat_conj (Complex_Matrix.adjoint U) A1 * + mat_conj (Complex_Matrix.adjoint U) A2 = + mat_conj (Complex_Matrix.adjoint U) A2 * + mat_conj (Complex_Matrix.adjoint U) A1" + proof (rule mat_conj_commute) + show "unitary U" using \unitary U\ . + show "A1\ carrier_mat n n" using \A1\ As\ assms by simp + show "A2\ carrier_mat n n" using \A2\ As\ assms by simp + show "U \ carrier_mat n n" using \U \ carrier_mat n n\ . + show "A1 * A2 = A2 * A1" using \A1\ As\ \A2\ As\ assms by simp + qed + thus "C1 * C2 = C2 * C1" + using \C1 = mat_conj (Complex_Matrix.adjoint U) A1\ + \C2 = mat_conj (Complex_Matrix.adjoint U) A2\ + by simp + qed +qed + +lemma commute_extract_diag_block_eq: + fixes Ap::"complex Matrix.mat" + assumes "Ap\ carrier_mat n n" + and "0 < n" + and "real_diag_decomp Ap Bs Us \ sorted (map Re (diag_mat Bs))" + and "finite Afp" + and "card Afp \ i" + and "\A\Afp. hermitian A \ A \ carrier_mat n n" + and "\A\Afp. \B\Afp. A * B = B * A" + and "\A\ Afp. Ap * A = A * Ap" + and "CjA = (\A2. mat_conj (Complex_Matrix.adjoint Us) A2)`Afp" + and "eqcl = eq_comps (diag_mat Bs)" + shows "\C \ CjA. C = diag_block_mat (extract_subdiags C eqcl)" +proof + note ubprops = real_diag_decomp_eq_comps_props[OF assms(1) assms(2) assms(3)] + note cjprops = commuting_conj_mat_set_props[OF assms(4) assms(5) assms(6) + assms(7) ubprops(3) ubprops(4) assms(9)] + fix C + assume "C\ CjA" + hence "\Ac \ Afp. C = mat_conj (Complex_Matrix.adjoint Us) Ac" + using assms by auto + from this obtain Ac where "Ac \ Afp" and + "C = mat_conj (Complex_Matrix.adjoint Us) Ac" by auto + show "C = diag_block_mat (extract_subdiags C eqcl)" + proof (rule diag_compat_extract_subdiag) + show "C \ carrier_mat n n" using cjprops \C\ CjA\ by simp + show "diag_compat C eqcl" + proof (rule commute_diag_compat) + show "Bs \ carrier_mat n n" using \Bs \ carrier_mat n n\ . + show "diag_diff Bs eqcl" using ubprops assms by simp + show "diagonal_mat Bs" using \diagonal_mat Bs\ . + show "C \ carrier_mat n n" using \C \ carrier_mat n n\ . + have "Bs * (Complex_Matrix.adjoint Us * Ac * Us) = + Complex_Matrix.adjoint Us * Ac * Us * Bs" + proof (rule unitarily_equiv_commute) + show "unitarily_equiv Ap Bs Us" using assms real_diag_decompD(1) + by simp + show "Ap * Ac = Ac * Ap" using assms \Ac \ Afp\ by simp + qed + thus "C * Bs = Bs * C" + using \C = mat_conj (Complex_Matrix.adjoint Us) Ac\ + by (metis mat_conj_adjoint) + qed + qed +qed + +lemma extract_dbm_eq_component_commute: + assumes "\C\Cs. C = diag_block_mat (extract_subdiags C l)" + and "\C1\Cs. \C2\Cs. C1 * C2 = C2 * C1" + and "ExC = (\A. extract_subdiags A l)`Cs" + and "j < length l" + and "Exi = (\A. (A!j))` ExC" + and "Al \ Exi" + and "Bl\ Exi" + shows "Al * Bl = Bl * Al" +proof - + define ncl where "ncl = length l" + have "\Al\ExC. length Al = ncl" + by (simp add: assms extract_subdiags_length ncl_def) + have "\Ea \ ExC. Al = Ea!j" using assms by auto + from this obtain Ea where "Ea\ ExC" and "Al = Ea!j" by auto + have "\Eb \ ExC. Bl = Eb!j" using assms by auto + from this obtain Eb where "Eb\ ExC" and "Bl = Eb!j" by auto + have "\jE\ExC. E ! j \ carrier_mat (l ! j) (l ! j)" + by (metis (no_types, lifting) assms(3) extract_subdiags_carrier + imageE ncl_def) + hence "\i < ncl. \Al\ExC. dim_row (Al ! i) = dim_col (Al ! i)" + by (metis carrier_matD(1) carrier_matD(2)) + have "Ea!j * Eb!j = Eb!j * Ea!j" + proof (rule diag_block_mat_commute_comp) + show "length Ea = length Eb" + by (simp add: \Ea \ ExC\ \Eb \ ExC\ \\Al\ExC. length Al = ncl\) + show "j < length Ea" + by (metis \Eb \ ExC\ \\Al\ExC. length Al = ncl\ \j < length l\ + ncl_def \length Ea = length Eb\) + show "\iEa \ ExC\ \\Al\ExC. length Al = ncl\ + \\i < ncl. \Al\ExC. dim_row (Al ! i) = dim_col (Al ! i)\) + show "\iEa \ ExC\ \Eb \ ExC\ \\Al\ExC. length Al = ncl\ + \\jE\ExC. E ! j \ carrier_mat (l ! j) (l ! j)\ + carrier_matD(1)) + show "\iEa \ ExC\ \Eb \ ExC\ \\Al\ExC. length Al = ncl\ + \\i + \\iAl\ExC. dim_row (Al ! i) = dim_col (Al ! i)\ by auto + have "\Cea \ Cs. Ea = extract_subdiags Cea l" + using \Ea \ ExC\ assms by auto + from this obtain Cea where "Cea\ Cs" and + "Ea = extract_subdiags Cea l" by auto + hence cea: "Cea = diag_block_mat Ea" + by (simp add: \\C\Cs. C = + diag_block_mat (extract_subdiags C l)\) + have "\Ceb \ Cs. Eb = extract_subdiags Ceb l" + using \Eb \ ExC\ assms by auto + from this obtain Ceb where "Ceb\ Cs" and + "Eb = extract_subdiags Ceb l" by auto + hence "Ceb = diag_block_mat Eb" + by (simp add: \\C\Cs. C = + diag_block_mat (extract_subdiags C l)\) + moreover have "Cea * Ceb = Ceb * Cea" + by (simp add: \Cea \ Cs\ \Ceb \ Cs\ + \\C1\Cs. \C2\Cs. C1 * C2 = C2 * C1\) + ultimately show "diag_block_mat Ea * diag_block_mat Eb = + diag_block_mat Eb * diag_block_mat Ea" using cea by simp + qed + thus "Al * Bl = Bl * Al" using \Al = Ea!j\ \Bl = Eb!j\ by simp +qed + +lemma extract_comm_real_diag_decomp: + fixes CjA::"complex Matrix.mat set" + assumes "\(Af::complex Matrix.mat set) n . finite Af \ + card Af \ i \ + Af \ {} \ + (\A. A \ Af \ A \ carrier_mat n n) \ + 0 < n \ (\A. A \ Af \ hermitian A) \ + (\A B. A \ Af \ B \ Af \ A * B = B * A) \ + \U. \A\Af. \B. real_diag_decomp A B U" + and "finite CjA" + and "CjA \ {}" + and "card CjA \ i" + and "\C\CjA. C = diag_block_mat (extract_subdiags C eqcl)" + and "\C1\CjA. \C2\CjA. C1 * C2 = C2 * C1" + and "Exc = (\A. extract_subdiags A eqcl)`CjA" + and "\ E\ Exc. list_all (\B. 0 < dim_row B \ hermitian B) E" + and "\i < length eqcl. 0 < eqcl!i" + shows "\iU. \Al\Exc. \B. real_diag_decomp (Al ! i) B U" +proof (intro allI impI) + define ncl where "ncl = length eqcl" + fix j + assume "j < ncl" + define Exi where "Exi = (\l. l!j)`Exc" + have "finite Exi" using assms unfolding Exi_def by simp + have "card Exi \ i" using assms unfolding Exi_def + by (metis card_image_le image_image le_trans) + have exfl: "\Ej \ Exi. \Fj \ CjA. Ej = (extract_subdiags Fj eqcl)!j" + proof + fix Ej + assume "Ej \ Exi" + hence "\El \ Exc. Ej = El!j" unfolding Exi_def by auto + from this obtain El where "El \ Exc" and "Ej = El!j" by auto + hence "\Fl \ CjA. El = extract_subdiags Fl eqcl" + using assms by auto + from this obtain Fl where "Fl \ CjA" and + "El = extract_subdiags Fl eqcl" by auto + thus "\Fj \ CjA. Ej = (extract_subdiags Fj eqcl)!j" using \Ej = El!j\ + by auto + qed + have "\U. \Al\Exi. \B. real_diag_decomp (Al) B U" + proof (rule assms(1)) + show "finite Exi" using \finite Exi\ . + show "card Exi \ i" using \card Exi <= i\ . + show "Exi \ {}" using \CjA \ {}\ using assms unfolding Exi_def by auto + show "0 < eqcl!j" using \j < ncl\ ncl_def assms by simp + show "\Al. Al \ Exi \ Al \ carrier_mat (eqcl ! j) (eqcl ! j)" + proof - + fix Al + assume "Al \ Exi" + hence "\Fl \ CjA. Al = (extract_subdiags Fl eqcl)!j" using exfl + by simp + from this obtain Fl where "Fl \ CjA" and + "Al = (extract_subdiags Fl eqcl)!j" by auto + thus "Al \ carrier_mat (eqcl ! j) (eqcl ! j)" + using extract_subdiags_carrier[of j eqcl] \j < ncl\ + unfolding Exi_def ncl_def by simp + qed + show "\Al. Al \ Exi \ hermitian Al" + proof - + fix Al + assume "Al\ Exi" + hence "\El \ Exc. Al = El!j" unfolding Exi_def by auto + from this obtain El where "El \ Exc" and "Al = El!j" by auto + thus "hermitian Al" using assms \j < ncl\ ncl_def + by (metis (no_types, lifting) extract_subdiags_length image_iff + list_all_length) + qed + show "\Al Bl. Al \ Exi \ Bl \ Exi \ Al * Bl = Bl * Al" + proof - + fix Al Bl + assume "Al \ Exi" and "Bl \ Exi" + show "Al*Bl = Bl * Al" + proof (rule extract_dbm_eq_component_commute[of CjA eqcl]) + show "Al \ Exi" using \Al \ Exi\ . + show "Bl \ Exi" using \Bl \ Exi\ . + show "\C\CjA. C = diag_block_mat (extract_subdiags C eqcl)" + using \\C\CjA. C = diag_block_mat (extract_subdiags C eqcl)\ . + show "\C1\CjA. \C2\CjA. C1 * C2 = C2 * C1" + using \\C1\CjA. \C2\CjA. C1 * C2 = C2 * C1\ . + show "j < length eqcl" using \j < ncl\ ncl_def by simp + show "Exi = (\A. A ! j) ` Exc" using Exi_def by simp + show "Exc = (\A. extract_subdiags A eqcl) ` CjA" + using assms by simp + qed + qed + qed + thus "\U. \Al\Exc. \B. real_diag_decomp (Al ! j) B U" unfolding Exi_def + by simp +qed + +subsection \The main result\ + +theorem commuting_hermitian_family_diag: + fixes Af::"complex Matrix.mat set" + assumes "finite Af" + and "Af \ {}" + and "\A. A\ Af \ A\ carrier_mat n n" + and "0 < n" + and "\A. A \ Af \ hermitian A" + and "\A B. A \ Af \ B\ Af \ A * B = B * A" +shows "\ U. \ A\ Af. \B. real_diag_decomp A B U" using assms +proof - + define i where "i = card Af" + have "card Af \ i" + by (simp add: i_def) + from assms(1) this assms(2-) show ?thesis + proof (induct i arbitrary: Af n) + case 0 + then have "Af = {}" by simp + then show ?case using 0 by simp + next + case (Suc i) + hence "\ A. A\ Af" by blast + from this obtain Ap where "Ap \ Af" by auto + define Afp where "Afp = Af - {Ap}" + have "finite Afp" using Suc unfolding Afp_def by simp + have "card Afp \ i" using \card Af \ Suc i\ \Ap \ Af\ + unfolding Afp_def by simp + have "\A\Afp. hermitian A \ A \ carrier_mat n n" using Suc + by (metis Afp_def Diff_subset subset_iff) + have "\A\Afp. \B\Afp. A * B = B * A" using Suc + by (metis Afp_def Diff_subset subset_iff) + have "\A\ Afp. Ap * A = A * Ap" using Suc + by (simp add: Afp_def \Ap \ Af\) + have "hermitian Ap" "Ap\ carrier_mat n n" "0 < n" using \Ap \ Af\ Suc by auto + from this obtain Bs Us where rd: "real_diag_decomp Ap Bs Us \ + sorted (map Re (diag_mat Bs))" + using hermitian_real_diag_sorted[of Ap] by auto note ub = this + note ubprops = real_diag_decomp_eq_comps_props[OF \Ap \ carrier_mat n n\ \0 < n\ ub] + define eqcl where "eqcl = eq_comps (diag_mat Bs)" + have "diag_diff Bs eqcl" using ubprops unfolding eqcl_def by simp + have "eqcl \ []" using ubprops unfolding eqcl_def by simp + hence "eqcl = hd eqcl # (tl eqcl)" by simp + define esubB where "esubB = extract_subdiags Bs eqcl" + have ebcar: "\i < length esubB. esubB ! i \ carrier_mat (eqcl!i) (eqcl!i)" + using extract_subdiags_carrier[of _ eqcl Bs] + by (simp add: esubB_def extract_subdiags_length) + have "Bs = diag_block_mat esubB" unfolding esubB_def eqcl_def + proof (rule diagonal_extract_eq) + show "Bs \ carrier_mat n n" using \Bs \ carrier_mat n n\ . + show "diagonal_mat Bs" using ubprops real_diag_decompD(2) + real_diag_decompD(1) unitary_diagD(2) by blast + qed + show ?case + proof (cases "Afp = {}") + case True + hence "Af = {Ap}" using \Afp = Af - {Ap}\ + by (simp add: Suc(4) subset_singleton_iff) + then show ?thesis using rd \Af = {Ap}\ by auto + next + case False + define Cj where "Cj = (\A2. mat_conj (Complex_Matrix.adjoint Us) A2)" + define CjA where "CjA = Cj`Afp" + have "CjA = (\A2. (mat_conj (Complex_Matrix.adjoint Us) A2)) ` Afp" + using CjA_def Cj_def by simp + note cjprops = commuting_conj_mat_set_props[OF \finite Afp\ \card Afp \ i\ + \\A\Afp. hermitian A \ A \ carrier_mat n n\ + \\A\Afp. \B\Afp. A * B = B * A\ + \unitary Us\ \Us \ carrier_mat n n\ + \CjA = (\A2. mat_conj (Complex_Matrix.adjoint Us) A2) ` Afp\] + have "\C \ CjA. C = diag_block_mat (extract_subdiags C eqcl)" + proof (rule commute_extract_diag_block_eq[OF \Ap\ carrier_mat n n\ + \0 < n\ rd \finite Afp\ _ + \\A\Afp. hermitian A \ A \ carrier_mat n n\], + auto simp add: eqcl_def CjA_def Cj_def) + show "\A B. A \ Afp \ B \ Afp \ A * B = B * A" + by (simp add: \\A\Afp. \B\Afp. A * B = B * A\) + show "\A. A \ Afp \ Ap * A = A * Ap" + using \\ A \ Afp. Ap * A = A * Ap\ by simp + qed + define Ex where "Ex = (\A. extract_subdiags A eqcl)`CjA" + have "finite Ex" using \finite CjA\ unfolding Ex_def by simp + have "Ex \ {}" using False unfolding Ex_def CjA_def by simp + have "card Ex \ i" using \card CjA \ i\ unfolding Ex_def + by (metis \finite CjA\ basic_trans_rules(23) card_image_le) + have exall: "\ E\ Ex. list_all (\B. 0 < dim_row B \ hermitian B) E" + proof + fix E + assume "E\ Ex" + hence "\nA \ CjA. E = extract_subdiags nA eqcl" unfolding Ex_def by auto + from this obtain nA where "nA\ CjA" and "E = extract_subdiags nA eqcl" + by auto + have "list_all (\B. 0 < dim_row B \ hermitian B) + (extract_subdiags nA eqcl)" + proof (rule hermitian_extract_subdiags) + show "hermitian nA" using \\A\ CjA. A \ carrier_mat n n \ hermitian A\ + \nA\ CjA\ by simp + show "list_all ((<) 0) eqcl" unfolding eqcl_def + by (metis \eqcl \ []\ eq_comps.simps(1) eq_comps_gt_0 eqcl_def) + show "sum_list eqcl \ dim_row nA" + using \\A\ CjA. A \ carrier_mat n n \ hermitian A\ + \nA\ CjA\ unfolding eqcl_def + by (metis \Bs \ carrier_mat n n\ carrier_matD(1) + eq_comp_sum_diag_mat le_refl) + qed + thus "list_all (\B. 0 < dim_row B \ hermitian B) E" + using \E = extract_subdiags nA eqcl\ by simp + qed + define ncl where "ncl = length eqcl" + have "\j < ncl. \E \ Ex. E!j \ carrier_mat (eqcl!j) (eqcl!j)" + proof (intro allI impI ballI) + fix E j + assume "j < ncl" and "E \ Ex" + thus "E ! j \ carrier_mat (eqcl ! j) (eqcl ! j)" unfolding Ex_def + using extract_subdiags_carrier ncl_def by blast + qed + have "\Ul. (length Ul = ncl \ + (\i Al \ Ex. + (dim_row (Ul!i) = dim_row (Al!i) \ dim_col (Ul!i) = dim_col (Al!i)))\ + (\ Al \ Ex. \Bl. (length Bl = ncl \ + real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) + (diag_block_mat Ul))))" + proof (rule real_diag_decomp_block_set) + show "Ex \ {}" using \Afp \ {}\ unfolding Ex_def CjA_def by auto + show "0 < ncl" unfolding ncl_def using \eqcl \[]\ by simp + show "\Al\Ex. length Al = ncl" unfolding ncl_def Ex_def + by (simp add: extract_subdiags_length) + show "\iAl\Ex. dim_row (Al ! i) = dim_col (Al ! i)" + proof (intro allI impI ballI) + fix i Al + assume "i < ncl" and "Al \ Ex" + thus "dim_row (Al ! i) = dim_col (Al ! i)" using exall + by (metis (mono_tags, lifting) \\Al\Ex. length Al = ncl\ + carrier_matD(2) hermitian_square list_all_length) + qed + show " \iU. \Al\Ex. \B. real_diag_decomp (Al ! i) B U" unfolding ncl_def + proof (rule extract_comm_real_diag_decomp[of i CjA, OF Suc(1)], + auto simp add: exall Ex_def) + show "finite CjA" using \finite CjA\ . + show "card CjA \ i" using \card CjA \ i\ . + show "\C. C \ CjA \ C = diag_block_mat (extract_subdiags C eqcl)" + using \\C \ CjA. C = diag_block_mat (extract_subdiags C eqcl)\ by simp + show "\C1 C2. C1 \ CjA \ C2 \ CjA \ C1 * C2 = C2 * C1" + using cjprops by simp + show "\i. i < length eqcl \ 0 < eqcl!i" + proof - + fix il + assume "il < length eqcl" + thus "0 < eqcl!il" using eq_comps_gt_0[OF \diag_mat Bs \ []\] + list_all_length[of "(<) 0" "eq_comps (diag_mat Bs)"] + unfolding eqcl_def by simp + qed + show "CjA = {} \ False" by (simp add: CjA_def False) + qed + qed + from this obtain Ul where "length Ul = ncl" and + dimul: "(\i Al \ Ex. + (dim_row (Ul!i) = dim_row (Al!i) \ dim_col (Ul!i) = dim_col (Al!i)))" and + ul: "\ Al \ Ex. \Bl. (length Bl = ncl \ + real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) + (diag_block_mat Ul))" + by auto + define Uf where "Uf = Us * (diag_block_mat Ul)" + have afp:"\A \ Afp. \Bl. real_diag_decomp A (diag_block_mat Bl) Uf" + proof + fix A + assume "A\ Afp" + define Ca where "Ca = mat_conj (Complex_Matrix.adjoint Us) A" + define Eca where "Eca = extract_subdiags Ca eqcl" + have "Ca \ CjA" using \A\ Afp\ + unfolding Ca_def CjA_def Cj_def by simp + hence "Ca = diag_block_mat Eca" unfolding Eca_def + using \\C\ CjA. C = diag_block_mat (extract_subdiags C eqcl)\ by simp + have "Eca \ Ex" unfolding Ex_def Eca_def using \Ca \ CjA\ by simp + hence "\Bl. (length Bl = ncl \ + real_diag_decomp (diag_block_mat Eca) (diag_block_mat Bl) + (diag_block_mat Ul))" using ul by simp + from this obtain Ecb where "length Ecb = ncl" and + "real_diag_decomp (diag_block_mat Eca) (diag_block_mat Ecb) + (diag_block_mat Ul)" by auto + hence "real_diag_decomp Ca (diag_block_mat Ecb) + (diag_block_mat Ul)" using \Ca = diag_block_mat Eca\ by simp + have "real_diag_decomp A (diag_block_mat Ecb) Uf" unfolding Uf_def + proof (rule unitary_conjugate_real_diag_decomp) + show "A\ carrier_mat n n" using \A\ Afp\ unfolding Afp_def + by (simp add: Suc(5)) + show "Us \ carrier_mat n n" using \Us \ carrier_mat n n\ . + show "unitary Us" using \unitary Us\ . + show "real_diag_decomp (mat_conj (Complex_Matrix.adjoint Us) A) + (diag_block_mat Ecb) (diag_block_mat Ul)" + using \real_diag_decomp Ca (diag_block_mat Ecb) + (diag_block_mat Ul)\ unfolding Ca_def by simp + qed + thus "\Bl. real_diag_decomp A (diag_block_mat Bl) Uf" by blast + qed + have "real_diag_decomp Ap Bs Uf" unfolding Uf_def + proof (rule real_diag_decomp_mult_dbm_unit) + show "Ap\ carrier_mat n n" using \Ap\ carrier_mat n n\ . + show "real_diag_decomp Ap Bs Us" using ub by simp + show "Bs = diag_block_mat esubB" using \Bs = diag_block_mat esubB\ . + show "length Ul = length esubB" using \length Ul = ncl\ + by (simp add: esubB_def extract_subdiags_length ncl_def) + show "\ilength Ul = length esubB\ + \length Ul = ncl\ ncl_def by auto + show roweq:"\ilength esubB = ncl\ \Ex\ {}\ + \\j < ncl. \E \ Ex. E!j \ carrier_mat (eqcl!j) (eqcl!j)\ + by (metis all_not_in_conv carrier_matD(1)) + show coleq:"\ilength esubB = ncl\ \Ex\ {}\ + \\j < ncl. \E \ Ex. E!j \ carrier_mat (eqcl!j) (eqcl!j)\ + by (metis all_not_in_conv carrier_matD(2)) + show "unitary (diag_block_mat Ul)" using ul + by (metis CjA_def False all_not_in_conv image_is_empty Ex_def + real_diag_decompD(1) unitary_diagD(3)) + show "\idiagonal_mat Bs\ . + show "Bs\ carrier_mat n n" using \Bs \ carrier_mat n n\ . + show "0 < n" using \0 < n\ . + show "i < length (eq_comps (diag_mat Bs))" + using \i < length Ul\ \length Ul = length esubB\ + extract_subdiags_length + unfolding esubB_def eqcl_def by metis + show "Ul ! i \ carrier_mat (eq_comps (diag_mat Bs) ! i) + (eq_comps (diag_mat Bs) ! i)" + using dimul \\j < ncl. \E \ Ex. E!j \ carrier_mat (eqcl!j) (eqcl!j)\ + \Ex\ {}\ unfolding ncl_def eqcl_def + by (metis coleq roweq + \\i + \i < length Ul\ \length Ul = length esubB\ carrier_matD(2) + carrier_matI ebcar eqcl_def) + qed + qed + qed + hence "\B. real_diag_decomp Ap B Uf" by blast + hence "\ A\ Af. \B. real_diag_decomp A B Uf" using afp + unfolding Afp_def by auto + thus "\U. \A\Af. \B. real_diag_decomp A B U" by blast + qed + qed +qed + +end \ No newline at end of file diff --git a/thys/Commuting_Hermitian/Commuting_Hermitian_Misc.thy b/thys/Commuting_Hermitian/Commuting_Hermitian_Misc.thy new file mode 100644 --- /dev/null +++ b/thys/Commuting_Hermitian/Commuting_Hermitian_Misc.thy @@ -0,0 +1,190 @@ +(* +Author: + Mnacho Echenim, Université Grenoble Alpes +*) + +theory Commuting_Hermitian_Misc imports "Jordan_Normal_Form.Matrix" + +begin +section \Misc\ + +fun n_sum where + "n_sum 0 l = 0" +| "n_sum (Suc n) l = (hd l) + (n_sum n (tl l))" + +lemma n_sum_last: + fixes l::"'a::{comm_monoid_add} list" + assumes "i < length l" + shows "n_sum (Suc i) l = n_sum i l + l!i" using assms +proof (induct i arbitrary:l) + case 0 + hence "l = hd l # tl l" by simp + then show ?case + using "0.prems" hd_conv_nth by auto +next + case (Suc i) + hence "n_sum (Suc (Suc i)) l = hd l + n_sum (Suc i) (tl l)" by simp + also have "... = hd l + n_sum i (tl l) + tl l!i" using Suc + by (metis Groups.add_ac(1) drop_Suc drop_eq_Nil2 leD leI) + also have "... = n_sum (Suc i) l + tl l!i" by simp + also have "... = n_sum (Suc i) l + l!(Suc i)" + by (metis Suc(2) Suc_lessD hd_Cons_tl list.sel(2) nth_Cons_Suc nth_tl) + finally show ?case . +qed + +lemma n_sum_last_lt: + fixes l::"'a::{comm_monoid_add, ordered_cancel_ab_semigroup_add} list" + assumes "j < l!i" + and "i < length l" + shows "n_sum i l + j < n_sum (Suc i) l" +proof - + have "n_sum i l + j < n_sum i l + l!i" + using assms add_strict_left_mono[of j "l!i"] by simp + also have "... = n_sum (Suc i) l" using n_sum_last[of i l] assms + by simp + finally show ?thesis . +qed + +lemma sum_list_tl_leq: + assumes "sum_list l \ (n::nat)" + and "l\ []" + and "hd l \ n" + shows "sum_list (tl l) \ n - hd l" +proof - + have "hd l + sum_list (tl l) = sum_list l" using assms + by (metis list.exhaust_sel sum_list_simps(2)) + also have "... \ n" using assms by simp + finally have "hd l + sum_list (tl l) \ n" . + thus ?thesis by simp +qed + +lemma diag_mat_length: + shows "length (diag_mat A) = dim_row A" unfolding diag_mat_def by simp + +lemma sum_list_geq_tl: + fixes l::"'a::{comm_monoid_add, ordered_ab_semigroup_add_imp_le} list" + assumes "l\[]" + and "\j < length l. 0 \ l!j" +shows "sum_list (tl l) \ sum_list l" using assms +proof (induct l) + case Nil + then show ?case by simp +next + case (Cons a l) + hence "0 \ a" + by (metis length_greater_0_conv nth_Cons_0) + have "sum_list (tl (a#l)) = sum_list l" by simp + also have "... \ a + sum_list l" using \0 \ a\ + by (metis add_0 add_le_cancel_right) + also have "... = sum_list (a#l)" by simp + finally show ?case . +qed + +lemma sum_list_geq_0: + fixes l::"'a::{comm_monoid_add, ordered_ab_semigroup_add_imp_le} list" + assumes "l\[]" + and "\j < length l. 0 \ l!j" +shows "0 \ sum_list l" using assms +proof (induct l) + case Nil + then show ?case by simp +next + case (Cons a l) + hence "0 \ a" + by (metis length_greater_0_conv nth_Cons_0) + show ?case + proof (cases "l = []") + case True + hence "sum_list (a#l) = a" by simp + then show ?thesis using \0 \ a\ by simp + next + case False + hence "0 \ sum_list l" using Cons by force + also have "... = sum_list (tl (a#l))" by simp + also have "... \ sum_list (a#l)" using sum_list_geq_tl Cons by metis + finally show ?thesis . + qed +qed + +lemma sum_list_cong: + assumes "length l = length m" + and "\i < length l. l!i = m!i" +shows "sum_list l = sum_list m" using assms +proof (induct l arbitrary: m) + case Nil + then show ?case by simp +next + case (Cons a l) + hence "0 < length m" by auto + hence "m = hd m # (tl m)" by simp + have "sum_list (a#l) = a + sum_list l" by simp + also have "... = hd m + sum_list l" using Cons + by (metis \0 < length m\ \m = hd m # tl m\ nth_Cons_0) + also have "... = hd m + sum_list (tl m)" + by (metis Cons.prems(1) Cons.prems(2) \m = hd m # tl m\ + calculation nth_equalityI sum_list.Cons) + also have "... = sum_list m" + by (metis \m = hd m # tl m\ sum_list.Cons) + finally show ?case . +qed + +lemma n_sum_sum_list: + fixes l::"'a::{comm_monoid_add, ordered_ab_semigroup_add_imp_le} list" + assumes "i \ length l" + and "\j < length l. 0 \ l!j" + shows "n_sum i l \ sum_list l" using assms +proof (induct i arbitrary: l) + case 0 + then show ?case + by (metis n_sum.simps(1) order.eq_iff sum_list_geq_0 sum_list_simps(1)) +next + case (Suc i) + hence "1 \ length l" by presburger + hence "l = hd l#(tl l)" + by (metis hd_Cons_tl list.size(3) rel_simps(45)) + have "n_sum (Suc i) l \ hd l + sum_list (tl l)" + proof - + have "n_sum i (tl l) \ sum_list (tl l)" + proof (rule Suc(1)) + show "i \ length (tl l)" using Suc by simp + show "\j tl l ! j" using Suc + by (metis Nitpick.size_list_simp(2) le_simps(3) nth_tl + verit_comp_simplify1(3) zero_less_Suc) + qed + thus ?thesis by simp + qed + also have "... = sum_list l" + by (metis \l = hd l # tl l\ sum_list.Cons) + finally show ?case . +qed + +lemma map2_commute: + assumes "length l = length m" + and "\i < length l. f (l!i) (m!i) = f (m!i) (l!i)" +shows "map2 f l m = map2 f m l" using assms +proof (induct l arbitrary: m) + case Nil + then show ?case by simp +next + case (Cons a l) + hence "0 < length m" by auto + hence "m = hd m#(tl m)" by simp + hence "map2 f (a#l) m = f a (hd m) # (map2 f l (tl m))" + by (metis (no_types, lifting) list.map(2) prod.simps(2) zip_Cons_Cons) + also have "... = f (hd m) a # (map2 f l (tl m))" using Cons + by (metis \0 < length m\ \m = hd m # tl m\ nth_Cons_0) + also have "... = f (hd m) a # (map2 f (tl m) l)" using Cons + by (metis Suc_less_eq \m = hd m # tl m\ length_Cons nat.simps(1) + nth_Cons_Suc) + also have "... = map2 f m (a#l)" + by (metis (no_types, lifting) Cons_eq_map_conv \m = hd m # tl m\ + prod.simps(2) zip_Cons_Cons) + finally show ?case . +qed + +lemma map2_length: + assumes "length Al = length Bl" + shows "length (map2 f Al Bl) = length Al" using assms by simp + + +end \ No newline at end of file diff --git a/thys/Commuting_Hermitian/ROOT b/thys/Commuting_Hermitian/ROOT new file mode 100644 --- /dev/null +++ b/thys/Commuting_Hermitian/ROOT @@ -0,0 +1,11 @@ +chapter AFP + +session Commuting_Hermitian (AFP) = "Projective_Measurements" + + options [timeout = 1800] + theories [document = false] + Commuting_Hermitian_Misc + theories + Spectral_Theory_Complements + Commuting_Hermitian + document_files + "root.tex" diff --git a/thys/Commuting_Hermitian/Spectral_Theory_Complements.thy b/thys/Commuting_Hermitian/Spectral_Theory_Complements.thy new file mode 100644 --- /dev/null +++ b/thys/Commuting_Hermitian/Spectral_Theory_Complements.thy @@ -0,0 +1,2157 @@ +(* +Author: + Mnacho Echenim, Université Grenoble Alpes +*) + +theory Spectral_Theory_Complements imports "HOL-Combinatorics.Permutations" +"Projective_Measurements.Linear_Algebra_Complements" + "Projective_Measurements.Projective_Measurements" + +begin +section \Some preliminary results\ + +subsection \Roots of a polynomial\ + +text \Results on polynomials, the main one being that +the set of roots of a polynomial is uniquely defined.\ + +lemma root_poly_linear: + shows "poly (\a\L. [:- a, 1:]) (c::'a :: field) = 0 \ c\ set L" +proof (induct L) + case Nil + thus ?case using Nil by simp +next + case (Cons a L) + show ?case + proof (cases "poly (\a\L. [:- a, 1:]) c = 0") + case True + then show ?thesis using Cons by auto + next + case False + hence "poly [:- a, 1:] c = 0" using Cons by auto + hence "a = c" by auto + thus ?thesis by auto + qed +qed + +lemma poly_root_set_subseteq: + assumes "(\(a::'a::field)\L. [:- a, 1:]) = (\a\M. [:- a, 1:])" + shows "set L \ set M" +proof + fix x + assume "x\ set L" + hence "poly (\(a::'a::field)\L. [:- a, 1:]) x = 0" using linear_poly_root[of x] by simp + hence "poly (\(a::'a::field)\M. [:- a, 1:]) x = 0" using assms by simp + thus "x\ set M" using root_poly_linear[of M] by simp +qed + +lemma poly_root_set_eq: + assumes "(\(a::'a::field)\L. [:- a, 1:]) = (\a\M. [:- a, 1:])" + shows "set L = set M" using assms poly_root_set_subseteq + by (simp add: poly_root_set_subseteq equalityI) + +subsection \Linear algebra preliminaries\ + +lemma minus_zero_vec_eq: + fixes v::"'a::{ab_group_add} Matrix.vec" + assumes "dim_vec v = n" + and "dim_vec w = n" + and "v - w = 0\<^sub>v n" +shows "v = w" +proof - + have "v = v - w + w" using assms + by (metis carrier_vec_dim_vec comm_add_vec left_zero_vec + minus_add_minus_vec minus_cancel_vec uminus_eq_vec + zero_minus_vec) + also have "... = 0\<^sub>v n + w" using assms by simp + also have "... = w" using assms left_zero_vec[of w n] + by (metis carrier_vec_dim_vec) + finally show ?thesis . +qed + +lemma right_minus_zero_mat: + fixes A::"'a::{group_add} Matrix.mat" + shows "A - 0\<^sub>m (dim_row A) (dim_col A) = A" + by (intro eq_matI, auto) + +lemma smult_zero: + shows "(0::'a::comm_ring) \\<^sub>m A = 0\<^sub>m (dim_row A) (dim_col A)" by auto + +lemma rank_1_proj_col_carrier: + assumes "i < dim_col A" + shows "rank_1_proj (Matrix.col A i) \ carrier_mat (dim_row A) (dim_row A)" +proof - + have "dim_vec (Matrix.col A i) = dim_row A" by simp + thus ?thesis by (metis rank_1_proj_carrier) +qed + +lemma zero_adjoint: + shows "Complex_Matrix.adjoint (0\<^sub>m n m) = ((0\<^sub>m m n):: 'a::conjugatable_field Matrix.mat)" + by (rule eq_matI, (auto simp add: adjoint_eval)) + +lemma assoc_mat_mult_vec': + assumes "A \ carrier_mat n n" + and "B\ carrier_mat n n" + and "C\ carrier_mat n n" +and "v\ carrier_vec n" +shows "A * B * C *\<^sub>v v = A *\<^sub>v (B *\<^sub>v (C *\<^sub>v v))" using assms + by (smt (z3) assoc_mult_mat_vec mult_carrier_mat mult_mat_vec_carrier) + +lemma adjoint_dim': + "A \ carrier_mat n m \ Complex_Matrix.adjoint A \ carrier_mat m n" + using adjoint_dim_col adjoint_dim_row by blast + +definition mat_conj where +"mat_conj U V = U * V * (Complex_Matrix.adjoint U)" + +lemma mat_conj_adjoint: + shows "mat_conj (Complex_Matrix.adjoint U) V = + Complex_Matrix.adjoint U * V * U" unfolding mat_conj_def + by (simp add: Complex_Matrix.adjoint_adjoint) + +lemma map2_mat_conj_exp: + assumes "length A = length B" + shows "map2 (*) (map2 (*) A B) (map Complex_Matrix.adjoint A) = + map2 mat_conj A B" using assms +proof (induct A arbitrary: B) + case Nil + then show ?case by simp +next + case (Cons a A) + hence "0 < length B" by auto + hence "B = hd B # (tl B)" by simp + hence "length (tl B) = length A" using Cons by simp + have "map2 (*) (map2 (*) (a # A) B) (map Complex_Matrix.adjoint (a # A)) = + a * hd B * Complex_Matrix.adjoint a # + map2 (*) (map2 (*) A (tl B)) (map Complex_Matrix.adjoint A)" + by (metis (no_types, lifting) \B = hd B # tl B\ list.map(2) + split_conv zip_Cons_Cons) + also have "... = mat_conj a (hd B) # map2 mat_conj A (tl B)" + using Cons \length (tl B) = length A\ + unfolding mat_conj_def + by presburger + also have "... = map2 mat_conj (a#A) B" using \B = hd B # (tl B)\ + by (metis (no_types, opaque_lifting) list.map(2) prod.simps(2) + zip_Cons_Cons) + finally show ?case . +qed + +lemma mat_conj_unit_commute: + assumes "unitary U" + and "U*A = A*U" + and "A\ carrier_mat n n" + and "U\ carrier_mat n n" +shows "mat_conj U A = A" +proof - + have "mat_conj U A = A*U * Complex_Matrix.adjoint U" using assms + unfolding mat_conj_def by simp + also have "... = A * (U * Complex_Matrix.adjoint U)" + proof (rule assoc_mult_mat, auto simp add: assms) + show "U \ carrier_mat (dim_col A) (dim_col U)" + using assms(3) assms(4) by auto + qed + also have "... = A" using assms by simp + finally show ?thesis . +qed + +lemma hermitian_mat_conj: + assumes "A\ carrier_mat n n" + and "U \ carrier_mat n n" + and "hermitian A" +shows "hermitian (mat_conj U A)" +proof - + have "Complex_Matrix.adjoint (U * A * Complex_Matrix.adjoint U) = + U * Complex_Matrix.adjoint (U * A)" + by (metis (no_types, lifting) Complex_Matrix.adjoint_adjoint adjoint_dim' + adjoint_mult assms(1) assms(2) mult_carrier_mat) + also have "... = U * ((Complex_Matrix.adjoint A) * Complex_Matrix.adjoint U)" + by (metis adjoint_mult assms(1) assms(2)) + also have "... = U * A * Complex_Matrix.adjoint U" + by (metis adjoint_dim' assms assoc_mult_mat hermitian_def) + finally show ?thesis unfolding hermitian_def mat_conj_def . +qed + +lemma hermitian_mat_conj': + assumes "A\ carrier_mat n n" + and "U \ carrier_mat n n" + and "hermitian A" +shows "hermitian (mat_conj (Complex_Matrix.adjoint U) A)" + by (metis Complex_Matrix.adjoint_adjoint adjoint_dim_col assms + carrier_matD(1) carrier_matD(2) carrier_mat_triv hermitian_mat_conj) + +lemma mat_conj_uminus_eq: + assumes "A\ carrier_mat n n" + and "U\ carrier_mat n n" + and "B \ carrier_mat n n" + and "A = mat_conj U B" +shows "-A = mat_conj U (-B)" using assms unfolding mat_conj_def by auto + +lemma mat_conj_smult: + assumes "A\ carrier_mat n n" + and "U\ carrier_mat n n" + and "B \ carrier_mat n n" + and "A = U * B * (Complex_Matrix.adjoint U)" +shows "x \\<^sub>m A = U * (x \\<^sub>m B) * (Complex_Matrix.adjoint U)" using assms mult_smult_distrib + by (smt (z3) adjoint_dim' mult_carrier_mat mult_smult_assoc_mat) + +lemma mult_adjoint_hermitian: + fixes A::"'a::conjugatable_field Matrix.mat" + assumes "A\ carrier_mat n m" + shows "hermitian ((Complex_Matrix.adjoint A) * A)" unfolding hermitian_def +proof - + define C where "C = (Complex_Matrix.adjoint A) * A" + have "Complex_Matrix.adjoint C = + Complex_Matrix.adjoint A * Complex_Matrix.adjoint (Complex_Matrix.adjoint A)" + using adjoint_mult assms C_def by (metis adjoint_dim' assms) + also have "... = Complex_Matrix.adjoint A * A" using assms + by (simp add: Complex_Matrix.adjoint_adjoint) + finally show "Complex_Matrix.adjoint C = C" using C_def by simp +qed + +lemma hermitian_square_hermitian: +fixes A::"'a::conjugatable_field Matrix.mat" + assumes "hermitian A" + shows "hermitian (A * A)" +proof - + have "Complex_Matrix.adjoint (A * A) = Complex_Matrix.adjoint A * (Complex_Matrix.adjoint A)" + using adjoint_mult by (metis assms hermitian_square) + also have "... = A * A" using assms unfolding hermitian_def by simp + finally show ?thesis unfolding hermitian_def . +qed + +section \Properties of the spectrum of a matrix\ + +subsection \Results on diagonal matrices\ + +lemma diagonal_mat_uminus: + fixes A::"'a::{ring} Matrix.mat" + assumes "diagonal_mat A" + shows "diagonal_mat (-A)" using assms unfolding diagonal_mat_def uminus_mat_def by auto + +lemma diagonal_mat_smult: + fixes A::"'a::{ring} Matrix.mat" + assumes "diagonal_mat A" + shows "diagonal_mat (x \\<^sub>mA)" using assms unfolding diagonal_mat_def uminus_mat_def by auto + + +lemma diagonal_imp_upper_triangular: + assumes "diagonal_mat A" + and "A \ carrier_mat n n" + shows "upper_triangular A" unfolding upper_triangular_def +proof (intro allI impI) + fix i j + assume "i < dim_row A" and "j < i" + hence "j < dim_col A" "j \ i" using assms by auto + thus "A $$ (i,j) = 0" using assms \i < dim_row A\ unfolding diagonal_mat_def by simp +qed + +lemma set_diag_mat_uminus: + assumes "A\ carrier_mat n n" + shows "set (diag_mat (-A)) = {-a |a. a\ set (diag_mat A)}" (is "?L = ?R") +proof + show "?L \ ?R" + proof + fix x + assume "x \ set (diag_mat (- A))" + hence "\i < length (diag_mat (-A)). nth (diag_mat (-A)) i = x" + using in_set_conv_nth[of x] by simp + from this obtain i where "i < length (diag_mat (-A))" and "nth (diag_mat (-A)) i = x" + by auto note iprop = this + hence "i < dim_row (-A)" unfolding diag_mat_def by simp + hence "i < n" using assms by simp + have "x = (-A)$$(i,i)" using iprop unfolding diag_mat_def by simp + also have "... = - A$$(i,i)" using \i < n\ assms unfolding uminus_mat_def by auto + also have "... \ ?R" using iprop assms \i < n\ + in_set_conv_nth[of "A$$(i,i)"] by (metis (mono_tags, lifting) carrier_matD(1) + diag_elems_mem diag_elems_set_diag_mat mem_Collect_eq) + finally show "x \ ?R" . + qed +next + show "?R \ ?L" + proof + fix x + assume "x\ ?R" + hence "\i < length (diag_mat A). -(nth (diag_mat A) i) = x" + using in_set_conv_nth[of x] by (smt (z3) in_set_conv_nth mem_Collect_eq) + from this obtain i where "i < length (diag_mat A)" and "-(nth (diag_mat A) i) = x" + by auto note iprop = this + hence "i < dim_row (-A)" unfolding diag_mat_def by simp + hence "i < n" using assms by simp + have "x = -A$$(i,i)" using iprop unfolding diag_mat_def by simp + also have "... = (- A)$$(i,i)" using \i < n\ assms unfolding uminus_mat_def by auto + also have "... \ ?L" using iprop assms \i < n\ + in_set_conv_nth[of "A$$(i,i)"] + by (metis \i < dim_row (- A)\ diag_elems_mem diag_elems_set_diag_mat) + finally show "x \ ?L" . + qed +qed + +lemma set_diag_mat_smult: + assumes "A\ carrier_mat n n" + shows "set (diag_mat (x \\<^sub>m A)) = {x * a |a. a\ set (diag_mat A)}" (is "?L = ?R") +proof + show "?L \ ?R" + proof + fix b + assume "b \ set (diag_mat (x \\<^sub>m A))" + hence "\i < length (diag_mat (x \\<^sub>m A)). nth (diag_mat (x \\<^sub>m A)) i = b" + using in_set_conv_nth[of b] by simp + from this obtain i where "i < length (diag_mat (x \\<^sub>m A))" and "nth (diag_mat (x \\<^sub>m A)) i = b" + by auto note iprop = this + hence "i < dim_row (x \\<^sub>m A)" unfolding diag_mat_def by simp + hence "i < n" using assms by simp + have "b = (x \\<^sub>m A)$$(i,i)" using iprop unfolding diag_mat_def by simp + also have "... = x * A$$(i,i)" using \i < n\ assms unfolding uminus_mat_def by auto + also have "... \ ?R" using iprop assms \i < n\ + in_set_conv_nth[of "A$$(i,i)"] + by (metis (mono_tags, lifting) carrier_matD(1) diag_elems_mem diag_elems_set_diag_mat + mem_Collect_eq) + finally show "b \ ?R" . + qed +next + show "?R \ ?L" + proof + fix b + assume "b\ ?R" + hence "\i < length (diag_mat A). x * (nth (diag_mat A) i) = b" + using in_set_conv_nth[of x] by (smt (z3) in_set_conv_nth mem_Collect_eq) + from this obtain i where "i < length (diag_mat A)" and "x * (nth (diag_mat A) i) = b" + by auto note iprop = this + hence "i < dim_row (x \\<^sub>m A)" unfolding diag_mat_def by simp + hence "i < n" using assms by simp + have "b = x *A$$(i,i)" using iprop unfolding diag_mat_def by simp + also have "... = (x \\<^sub>m A)$$(i,i)" using \i < n\ assms unfolding uminus_mat_def by auto + also have "... \ ?L" using iprop assms \i < n\ + in_set_conv_nth[of "A$$(i,i)"] + by (metis \i < dim_row (x \\<^sub>m A)\ diag_elems_mem diag_elems_set_diag_mat) + finally show "b \ ?L" . + qed +qed + + +lemma diag_mat_diagonal_eq: + assumes "diag_mat A = diag_mat B" +and "diagonal_mat A" +and "diagonal_mat B" +and "dim_col A = dim_col B" +shows "A = B" +proof + show c: "dim_col A = dim_col B" using assms by simp + show r: "dim_row A = dim_row B" using assms unfolding diag_mat_def + proof - + assume "map (\i. A $$ (i, i)) [0..i. B $$ (i, i)) [0..dim_row A = dim_row B\ \i \ j\ \i < dim_row B\ \j < dim_col B\) + next + case True + hence "A $$ (i,j) = A $$ (i,i)" by simp + also have "... = (diag_mat A)!i" using c r \i < dim_row B\ unfolding diag_mat_def by simp + also have "... = (diag_mat B)!i" using assms by simp + also have "... = B $$(i,i)" using c r \i < dim_row B\ unfolding diag_mat_def by simp + also have "... = B $$ (i,j)" using True by simp + finally show "A $$(i,j) = B $$(i,j)" . + qed +qed + + +lemma diag_elems_ne: + assumes "B \ carrier_mat n n" + and "0 < n" +shows "diag_elems B \ {}" +proof - + have "B $$(0,0) \ diag_elems B" using assms by simp + thus ?thesis by auto +qed + +lemma diagonal_mat_mult_vec: + fixes B::"'a::conjugatable_field Matrix.mat" + assumes "diagonal_mat B" + and "B \ carrier_mat n n" + and "v\ carrier_vec n" + and "i < n" +shows "vec_index (B *\<^sub>v v) i = B $$ (i,i) * (vec_index v i)" +proof - + have "vec_index (B *\<^sub>v v) i = Matrix.scalar_prod (Matrix.row B i) v" using mult_mat_vec_def assms + by simp + also have "... = (\ j \ {0 ..< n}. vec_index (Matrix.row B i) j * (vec_index v j))" + using Matrix.scalar_prod_def assms(3) carrier_vecD by blast + also have "... = (\ j \ {0 ..< n}. B $$ (i,j) * (vec_index v j))" + proof - + have "\j. j < n \ vec_index (Matrix.row B i) j = B $$ (i,j)" using assms by auto + thus ?thesis by auto + qed + also have "... = B $$ (i,i) * (vec_index v i)" + proof (rule sum_but_one, (auto simp add: assms)) + show "\j. j < n \ j \ i \ B $$ (i, j) = 0" using assms unfolding diagonal_mat_def + by force + qed + finally show ?thesis . +qed + +lemma diagonal_mat_mult_index: + fixes B::"'a::{ring} Matrix.mat" + assumes "diagonal_mat A" + and "A\ carrier_mat n n" + and "B \ carrier_mat n n" + and "i < n" + and "j < n" + shows "(A * B) $$ (i,j) = A$$(i,i) * B$$(i,j)" unfolding diagonal_mat_def +proof - + have "dim_row (A * B) = n" using assms by simp + have "dim_col (A * B) = n" using assms by simp + have jvec: "\j. j < n \ dim_vec (Matrix.col B j) = n" using assms by simp + have "(A * B) $$ (i,j) = Matrix.scalar_prod (Matrix.row A i) (Matrix.col B j)" + using assms by (metis carrier_matD(1) carrier_matD(2) index_mult_mat(1)) + also have "... = + (\ k \ {0 ..< n}. vec_index (Matrix.row A i) k * + vec_index (Matrix.col B j) k)" + using assms jvec unfolding Matrix.scalar_prod_def by simp + also have "... = vec_index (Matrix.row A i) i * vec_index (Matrix.col B j) i" + proof (rule sum_but_one) + show "i < n" using assms \dim_row (A * B) = n\ by simp + show "\k i \ vec_index (Matrix.row A i) k = 0" using assms \i < n\ + unfolding diagonal_mat_def by auto + qed + also have "... = A$$(i,i) * B$$(i,j)" using assms + by (metis carrier_matD(1) carrier_matD(2) index_col index_row(1)) + finally show ?thesis . +qed + +lemma diagonal_mat_mult_index': + fixes A::"'a::comm_ring Matrix.mat" + assumes "A \ carrier_mat n n" +and "B\ carrier_mat n n" +and "diagonal_mat B" +and "j < n" +and "i < n" +shows "(A*B) $$(i,j) = B$$(j,j) *A $$ (i, j)" + (*"(B*A) $$(i,j) = B$$(i,i) *A $$ (i, j)"*) +proof - + have "(A*B) $$ (i,j) = Matrix.scalar_prod (Matrix.row A i) (Matrix.col B j)" using assms + times_mat_def[of A] by simp + also have "... = Matrix.scalar_prod (Matrix.col B j) (Matrix.row A i)" + using comm_scalar_prod[of "Matrix.row A i" n] assms by auto + also have "... = (Matrix.vec_index (Matrix.col B j) j) * (Matrix.vec_index (Matrix.row A i) j)" + unfolding Matrix.scalar_prod_def + proof (rule sum_but_one) + show "j < dim_vec (Matrix.row A i)" using assms by simp + show "\ia j \ Matrix.vec_index (Matrix.col B j) ia = 0" + using assms + by (metis carrier_matD(1) carrier_matD(2) diagonal_mat_def index_col index_row(2)) + qed + also have "... = B $$(j,j) * A $$(i,j)" using assms by auto + finally show "(A * B) $$ (i, j) = B $$ (j, j) * A $$ (i, j)" . +qed + +lemma diagonal_mat_times_diag: + assumes "A\ carrier_mat n n" + and "B\ carrier_mat n n" + and "diagonal_mat A" +and "diagonal_mat B" +shows "diagonal_mat (A*B)" unfolding diagonal_mat_def +proof (intro allI impI) + fix i j + assume "i < dim_row (A * B)" and "j < dim_col (A * B)" and "i \ j" + thus "(A * B) $$ (i, j) = 0" using assms diag_mat_mult_diag_mat[of A n B] + by simp +qed + +lemma diagonal_mat_commute: + fixes A::"'a::{comm_ring} Matrix.mat" + assumes "A\ carrier_mat n n" + and "B\ carrier_mat n n" + and "diagonal_mat A" +and "diagonal_mat B" +shows "A * B = B * A" +proof (rule eq_matI) + show "dim_row (A * B) = dim_row (B * A)" using assms by simp + show "dim_col (A * B) = dim_col (B * A)" using assms by simp + have bac: "B*A \ carrier_mat n n" using assms by simp + fix i j + assume "i < dim_row (B*A)" and "j < dim_col (B*A)" note ij = this + have "(A * B) $$ (i, j) = A $$ (i, j) * B$$(i,j)" + using ij diagonal_mat_mult_index assms bac + by (metis carrier_matD(1) carrier_matD(2) diagonal_mat_def mult_zero_right) + also have "... = B$$(i,j) * A $$ (i, j)" + by (simp add: Groups.mult_ac(2)) + also have "... = (B*A) $$ (i,j)" using ij diagonal_mat_mult_index assms bac + by (metis carrier_matD(1) carrier_matD(2) diagonal_mat_def mult_not_zero) + finally show "(A * B) $$ (i, j) = (B*A) $$ (i,j)" . +qed + +lemma diagonal_mat_sq_index: + fixes B::"'a::{ring} Matrix.mat" + assumes "diagonal_mat B" + and "B \ carrier_mat n n" + and "i < n" + and "j < n" + shows "(B * B) $$ (i,j) = B$$(i,i) * B$$(j,i)" +proof - + have "(B * B) $$ (i,j) = B$$(i,i) * B$$(i,j)" + using assms diagonal_mat_mult_index[of B] by simp + also have "... = B$$(i,i) * B$$(j,i)" using assms unfolding diagonal_mat_def + by (metis carrier_matD(1) carrier_matD(2)) + finally show ?thesis . +qed + +lemma diagonal_mat_sq_index': + fixes B::"'a::{ring} Matrix.mat" + assumes "diagonal_mat B" + and "B \ carrier_mat n n" + and "i < n" + and "j < n" + shows "(B * B) $$ (i,j) = B$$(i,j) * B$$(i,j)" +proof - + have eq: "(B * B) $$ (i,j) = B$$(i,i) * B$$(j,i)" + using assms diagonal_mat_sq_index by metis + show ?thesis + proof (cases "i = j") + case True + then show ?thesis using eq by simp + next + case False + hence "B$$(i,j) = 0" using assms unfolding diagonal_mat_def by simp + hence "(B * B) $$ (i,j) = 0" using eq + by (metis assms diagonal_mat_mult_index mult_not_zero) + thus ?thesis using eq \B$$(i,j) = 0\ by simp + qed +qed + +lemma diagonal_mat_sq_diag: + fixes B::"'a::{ring} Matrix.mat" + assumes "diagonal_mat B" + and "B \ carrier_mat n n" + shows "diagonal_mat (B * B)" unfolding diagonal_mat_def +proof (intro allI impI) + have "dim_row (B * B) = n" using assms by simp + have "dim_col (B * B) = n" using assms by simp + have jvec: "\j. j < n \ dim_vec (Matrix.col B j) = n" using assms by simp + fix i j + assume "i < dim_row (B * B)" + and "j < dim_col (B * B)" + and "i \ j" note ijprops = this + thus "(B * B) $$ (i,j) = 0" using diagonal_mat_sq_index + by (metis \dim_col (B * B) = n\ \dim_row (B * B) = n\ assms(1) assms(2) carrier_matD(1) + carrier_matD(2) diagonal_mat_def mult_not_zero) +qed + +lemma real_diagonal_hermitian: + fixes B::"complex Matrix.mat" + assumes "B\ carrier_mat n n" + and "diagonal_mat B" + and "\i < dim_row B. B$$(i, i) \ Reals" +shows "hermitian B" unfolding hermitian_def +proof (rule eq_matI) + show "dim_row (Complex_Matrix.adjoint B) = dim_row B" using assms by auto + show "dim_col (Complex_Matrix.adjoint B) = dim_col B" using assms by auto +next + fix i j + assume "i < dim_row B" and "j < dim_col B" note ij = this + show "Complex_Matrix.adjoint B $$ (i, j) = B $$ (i, j)" + proof (cases "i = j") + case True + thus ?thesis using assms ij Reals_cnj_iff + unfolding diagonal_mat_def Complex_Matrix.adjoint_def by simp + next + case False + then show ?thesis using assms ij + unfolding diagonal_mat_def Complex_Matrix.adjoint_def by simp + qed +qed + +subsection \Unitary equivalence\ + +definition unitarily_equiv where +"unitarily_equiv A B U \ (unitary U \ + similar_mat_wit A B U (Complex_Matrix.adjoint U))" + +lemma unitarily_equivD: + assumes "unitarily_equiv A B U" + shows "unitary U" + "similar_mat_wit A B U (Complex_Matrix.adjoint U)" using assms + unfolding unitarily_equiv_def by auto + +lemma unitarily_equivI: + assumes "similar_mat_wit A B U (Complex_Matrix.adjoint U)" + and "unitary U" +shows "unitarily_equiv A B U" using assms + unfolding unitarily_equiv_def by simp + +lemma unitarily_equivI': + assumes "A = mat_conj U B" + and "unitary U" + and "A\ carrier_mat n n" + and "B\ carrier_mat n n" +shows "unitarily_equiv A B U" using assms + unfolding unitarily_equiv_def similar_mat_wit_def + by (metis (mono_tags, opaque_lifting) Complex_Matrix.unitary_def + carrier_matD(1) empty_subsetI index_mult_mat(2) index_one_mat(2) + insert_commute insert_subset unitary_adjoint unitary_simps(1) + unitary_simps(2) mat_conj_def) + +lemma unitarily_equiv_carrier: + assumes "A\ carrier_mat n n" + and "unitarily_equiv A B U" +shows "B \ carrier_mat n n" "U\ carrier_mat n n" +proof - + show "B \ carrier_mat n n" + by (metis assms carrier_matD(1) similar_mat_witD(5) unitarily_equivD(2)) + show "U \ carrier_mat n n" + by (metis assms similar_mat_witD2(6) unitarily_equivD(2)) +qed + +lemma unitarily_equiv_carrier': + assumes "unitarily_equiv A B U" + shows "A \ carrier_mat (dim_row A) (dim_row A)" + "B \ carrier_mat (dim_row A) (dim_row A)" + "U\ carrier_mat (dim_row A) (dim_row A)" +proof - + show "A \ carrier_mat (dim_row A) (dim_row A)" + by (metis assms carrier_mat_triv similar_mat_witD2(4) unitarily_equivD(2)) + thus "U \ carrier_mat (dim_row A) (dim_row A)" + using assms unitarily_equiv_carrier(2) by blast + show "B \ carrier_mat (dim_row A) (dim_row A)" + by (metis assms similar_mat_witD(5) unitarily_equivD(2)) +qed + +lemma unitarily_equiv_eq: + assumes "unitarily_equiv A B U" + shows "A = U * B * (Complex_Matrix.adjoint U)" using assms + unfolding unitarily_equiv_def similar_mat_wit_def by meson + +lemma unitarily_equiv_smult: + assumes "A\ carrier_mat n n" + and "unitarily_equiv A B U" + shows "unitarily_equiv (x \\<^sub>m A) (x \\<^sub>m B) U" +proof (rule unitarily_equivI) + show "similar_mat_wit (x \\<^sub>m A) (x \\<^sub>m B) U (Complex_Matrix.adjoint U)" + using mat_conj_smult assms + by (simp add: similar_mat_wit_smult unitarily_equivD(2)) + show "unitary U" using assms unitarily_equivD(1)[of A] by simp +qed + +lemma unitarily_equiv_uminus: + assumes "A\ carrier_mat n n" + and "unitarily_equiv A B U" + shows "unitarily_equiv (-A) (-B) U" +proof (rule unitarily_equivI) + show "similar_mat_wit (-A) (-B) U (Complex_Matrix.adjoint U)" + using mat_conj_uminus_eq assms + by (smt (z3) adjoint_dim_col adjoint_dim_row carrier_matD(1) + carrier_matD(2) carrier_mat_triv index_uminus_mat(2) + index_uminus_mat(3) similar_mat_witI unitarily_equivD(1) + unitarily_equiv_carrier(1) unitarily_equiv_carrier(2) + unitarily_equiv_eq unitary_simps(1) unitary_simps(2) mat_conj_def) + show "unitary U" using assms unitarily_equivD(1)[of A] by simp +qed + +lemma unitarily_equiv_adjoint: + assumes "unitarily_equiv A B U" + shows "unitarily_equiv B A (Complex_Matrix.adjoint U)" + unfolding unitarily_equiv_def +proof + show "Complex_Matrix.unitary (Complex_Matrix.adjoint U)" + using Complex_Matrix.unitary_def assms unitarily_equiv_def unitary_adjoint + by blast + have "similar_mat_wit B A (Complex_Matrix.adjoint U) U" + unfolding similar_mat_wit_def Let_def + proof (intro conjI) + show car: "{B, A, Complex_Matrix.adjoint U, U} \ + carrier_mat (dim_row B) (dim_row B)" + by (metis assms insert_commute similar_mat_wit_def + similar_mat_wit_dim_row unitarily_equivD(2)) + show "Complex_Matrix.adjoint U * U = 1\<^sub>m (dim_row B)" using car + by (meson assms insert_subset unitarily_equivD(1) unitary_simps(1)) + show "U * Complex_Matrix.adjoint U = 1\<^sub>m (dim_row B)" + by (meson assms similar_mat_wit_def similar_mat_wit_sym + unitarily_equivD(2)) + have "Complex_Matrix.adjoint U * A * U = + Complex_Matrix.adjoint U * (U * B * Complex_Matrix.adjoint U) * U" + using assms unitarily_equiv_eq by auto + also have "... = B" + by (metis assms similar_mat_wit_def similar_mat_wit_sym unitarily_equivD(2)) + finally show "B = Complex_Matrix.adjoint U * A * U" by simp + qed + thus "similar_mat_wit B A (Complex_Matrix.adjoint U) + (Complex_Matrix.adjoint (Complex_Matrix.adjoint U))" + by (simp add: Complex_Matrix.adjoint_adjoint) +qed + +lemma unitary_mult_conjugate: + assumes "A \ carrier_mat n n" + and "V\ carrier_mat n n" + and "U\ carrier_mat n n" + and "B\ carrier_mat n n" + and "unitary V" + and "mat_conj (Complex_Matrix.adjoint V) A = mat_conj U B" + shows "A = V* U * B * Complex_Matrix.adjoint (V * U)" +proof - + have "Complex_Matrix.adjoint V *A * V \ carrier_mat n n" using assms + by (metis adjoint_dim_row carrier_matD(2) carrier_mat_triv + index_mult_mat(2) index_mult_mat(3)) + have "A * V = V * (Complex_Matrix.adjoint V) * (A * V)" using assms by simp + also have "... = V * (Complex_Matrix.adjoint V *(A * V))" + proof (rule assoc_mult_mat, auto simp add: assms) + show "A * V \ carrier_mat (dim_row V) (dim_row V)" using assms by auto + qed + also have "... = V * (Complex_Matrix.adjoint V *A * V)" + by (metis adjoint_dim' assms(1) assms(2) assoc_mult_mat) + also have "... = V * (U * B * (Complex_Matrix.adjoint U))" using assms + by (simp add: Complex_Matrix.adjoint_adjoint mat_conj_def) + also have "... = V * (U * (B * (Complex_Matrix.adjoint U)))" + by (metis adjoint_dim' assms(3) assms(4) assoc_mult_mat) + also have "... = V * U * (B * (Complex_Matrix.adjoint U))" + proof (rule assoc_mult_mat[symmetric], auto simp add: assms) + show "U \ carrier_mat (dim_col V) (dim_row B)" using assms by auto + qed + also have "... = V * U * B * (Complex_Matrix.adjoint U)" + proof (rule assoc_mult_mat[symmetric], auto simp add: assms) + show "B \ carrier_mat (dim_col U) (dim_col U)" using assms by auto + qed + finally have eq: "A * V = V * U * B * (Complex_Matrix.adjoint U)" . + have "A = A * (V * Complex_Matrix.adjoint V)" using assms by simp + also have "... = A * V * Complex_Matrix.adjoint V" + proof (rule assoc_mult_mat[symmetric], auto simp add: assms) + show "V \ carrier_mat (dim_col A) (dim_col V)" using assms by auto + qed + also have "... = V * U * B * (Complex_Matrix.adjoint U) * + (Complex_Matrix.adjoint V)" using eq by simp + also have "... = V * U * B * ((Complex_Matrix.adjoint U) * + (Complex_Matrix.adjoint V))" + proof (rule assoc_mult_mat, auto simp add: assms) + show "Complex_Matrix.adjoint U \ carrier_mat (dim_col B) (dim_col V)" + using adjoint_dim' assms by auto + qed + also have "... = V* U * B * Complex_Matrix.adjoint (V * U)" + by (metis adjoint_mult assms(2) assms(3)) + finally show ?thesis . +qed + +lemma unitarily_equiv_conjugate: + assumes "A\ carrier_mat n n" + and "V\ carrier_mat n n" + and "U \ carrier_mat n n" + and "B\ carrier_mat n n" + and "unitarily_equiv (mat_conj (Complex_Matrix.adjoint V) A) B U" + and "unitary V" + shows "unitarily_equiv A B (V * U)" + unfolding unitarily_equiv_def +proof + show "Complex_Matrix.unitary (V*U)" using assms + by (simp add: unitarily_equivD(1) unitary_times_unitary) + show "similar_mat_wit A B (V*U) (Complex_Matrix.adjoint (V*U))" + unfolding similar_mat_wit_def Let_def + proof (intro conjI) + show "{A, B, V*U, Complex_Matrix.adjoint (V*U)} \ + carrier_mat (dim_row A) (dim_row A)" using assms by auto + show "V*U * Complex_Matrix.adjoint (V*U) = 1\<^sub>m (dim_row A)" + by (metis Complex_Matrix.unitary_def \Complex_Matrix.unitary (V * U)\ + assms(1) assms(2) carrier_matD(1) index_mult_mat(2) inverts_mat_def) + show "Complex_Matrix.adjoint (V * U) * (V * U) = 1\<^sub>m (dim_row A)" + by (metis Complex_Matrix.unitary_def \Complex_Matrix.unitary (V * U)\ + \V * U * Complex_Matrix.adjoint (V * U) = 1\<^sub>m (dim_row A)\ + index_mult_mat(2) index_one_mat(2) unitary_simps(1)) + show "A = V * U * B * Complex_Matrix.adjoint (V * U)" + proof (rule unitary_mult_conjugate[of _ n], auto simp add: assms) + show "mat_conj (Complex_Matrix.adjoint V) A = mat_conj U B" using assms + by (simp add: mat_conj_def unitarily_equiv_eq) + qed + qed +qed + +lemma mat_conj_commute: + assumes "A \ carrier_mat n n" + and "B\ carrier_mat n n" + and "U \ carrier_mat n n" + and "unitary U" + and "A*B = B*A" +shows "(mat_conj (Complex_Matrix.adjoint U) A) * + (mat_conj (Complex_Matrix.adjoint U) B) = + (mat_conj (Complex_Matrix.adjoint U) B) * + (mat_conj (Complex_Matrix.adjoint U) A)" (is "?L*?R = ?R* ?L") +proof - + have u: "Complex_Matrix.adjoint U \ carrier_mat n n" using assms + by (simp add: adjoint_dim') + have ca: "Complex_Matrix.adjoint U * A * U \ carrier_mat n n" + using assms by auto + have cb: "Complex_Matrix.adjoint U * B * U \ carrier_mat n n" + using assms by auto + have "?L * ?R = + ?L * (Complex_Matrix.adjoint U * (B * U))" + proof - + have "Complex_Matrix.adjoint U * B * U = + Complex_Matrix.adjoint U * (B * U)" + using assoc_mult_mat[of _ n n B n U] assms + by (meson adjoint_dim') + thus ?thesis using mat_conj_adjoint by metis + qed + also have "... = ?L * Complex_Matrix.adjoint U * (B*U)" + proof - + have "\na nb. Complex_Matrix.adjoint U \ carrier_mat n na \ + B * U \ carrier_mat na nb" + by (metis (no_types) assms(2) carrier_matD(1) carrier_mat_triv index_mult_mat(2) u) + then show ?thesis using ca + by (metis assoc_mult_mat mat_conj_adjoint) + qed + also have "... = Complex_Matrix.adjoint U * A* + (U * (Complex_Matrix.adjoint U)) * (B * U)" + proof - + have "Complex_Matrix.adjoint U * A * U * Complex_Matrix.adjoint U = + Complex_Matrix.adjoint U * A * (U * Complex_Matrix.adjoint U)" + using assoc_mult_mat[of "Complex_Matrix.adjoint U * A" n n] + by (metis assms(1) assms(3) mult_carrier_mat u) + thus ?thesis by (simp add: mat_conj_adjoint) + qed + also have "... = Complex_Matrix.adjoint U * A* (B * U)" + using assms by auto + also have "... = Complex_Matrix.adjoint U * A * B * U" + proof (rule assoc_mult_mat[symmetric], auto simp add: assms) + show "B \ carrier_mat (dim_col A) (dim_row U)" using assms by simp + qed + also have "... = Complex_Matrix.adjoint U * (A * B) * U" + using assms u by auto + also have "... = Complex_Matrix.adjoint U * (B * A) * U" using assms by simp + also have "... = Complex_Matrix.adjoint U * B * A * U" + using assms u by auto + also have "... = Complex_Matrix.adjoint U * B * (A * U)" + proof (rule assoc_mult_mat, auto simp add: assms) + show "A \ carrier_mat (dim_col B) (dim_row U)" + using assms by simp + qed + also have "... = Complex_Matrix.adjoint U * B* + (U * (Complex_Matrix.adjoint U)) * (A * U)" + using assms by auto + also have "... = Complex_Matrix.adjoint U * B* + U * (Complex_Matrix.adjoint U) * (A * U)" + proof - + have "Complex_Matrix.adjoint U * B * U * Complex_Matrix.adjoint U = + Complex_Matrix.adjoint U * B * (U * Complex_Matrix.adjoint U)" + proof (rule assoc_mult_mat, auto simp add: assms) + show "U \ carrier_mat (dim_col B) (dim_col U)" using assms by simp + qed + thus ?thesis by simp + qed + also have "... = Complex_Matrix.adjoint U * B* + U * ((Complex_Matrix.adjoint U) * (A * U))" + proof (rule assoc_mult_mat, auto simp add: u cb) + show "A * U \ carrier_mat (dim_row U) n" using assms by simp + qed + also have "... = Complex_Matrix.adjoint U * B* + U * ((Complex_Matrix.adjoint U) * A * U)" + proof - + have "(Complex_Matrix.adjoint U) * (A * U) = + (Complex_Matrix.adjoint U) * A * U" + proof (rule assoc_mult_mat[symmetric], auto simp add: assms u) + show "A \ carrier_mat (dim_row U) (dim_row U)" using assms by simp + qed + thus ?thesis by simp + qed + finally show ?thesis by (metis mat_conj_adjoint) +qed + +lemma unitarily_equiv_commute: + assumes "unitarily_equiv A B U" + and "A*C = C*A" +shows "B * (Complex_Matrix.adjoint U * C * U) = +Complex_Matrix.adjoint U * C * U * B" +proof - + note car = unitarily_equiv_carrier'[OF assms(1)] + have cr: "dim_row C = dim_col A" + by (metis assms(2) car(1) carrier_matD(2) index_mult_mat(2)) + have cd: "dim_col C = dim_row A" + by (metis \dim_row C = dim_col A\ assms(2) index_mult_mat(2) + index_mult_mat(3)) + have "Complex_Matrix.adjoint U * A * U = B" + using assms unitarily_equiv_adjoint + by (metis Complex_Matrix.adjoint_adjoint unitarily_equiv_eq) + thus ?thesis using mat_conj_commute assms car + by (metis carrier_matD(2) carrier_matI cd cr mat_conj_adjoint + unitarily_equivD(1)) +qed + +definition unitary_diag where +"unitary_diag A B U \ unitarily_equiv A B U \ diagonal_mat B" + +lemma unitary_diagI: + assumes "similar_mat_wit A B U (Complex_Matrix.adjoint U)" + and "diagonal_mat B" + and "unitary U" +shows "unitary_diag A B U" using assms + unfolding unitary_diag_def unitarily_equiv_def by simp + +lemma unitary_diagI': + assumes "A\ carrier_mat n n" + and "B\ carrier_mat n n" + and "diagonal_mat B" + and "unitary U" + and "A = mat_conj U B" +shows "unitary_diag A B U" unfolding unitary_diag_def +proof + show "diagonal_mat B" using assms by simp + show "unitarily_equiv A B U" using assms unitarily_equivI' by metis +qed + +lemma unitary_diagD: + assumes "unitary_diag A B U" + shows "similar_mat_wit A B U (Complex_Matrix.adjoint U)" + "diagonal_mat B" "unitary U" using assms + unfolding unitary_diag_def unitarily_equiv_def + by simp+ + +lemma unitary_diag_imp_unitarily_equiv[simp]: +assumes "unitary_diag A B U" +shows "unitarily_equiv A B U" using assms unfolding unitary_diag_def by simp + +lemma unitary_diag_diagonal[simp]: + assumes "unitary_diag A B U" + shows "diagonal_mat B" using assms unfolding unitary_diag_def by simp + +lemma unitary_diag_carrier: + assumes "A\ carrier_mat n n" + and "unitary_diag A B U" +shows "B \ carrier_mat n n" "U\ carrier_mat n n" +proof - + show "B \ carrier_mat n n" + using assms unitarily_equiv_carrier(1)[of A n B U] by simp + show "U \ carrier_mat n n" + using assms unitarily_equiv_carrier(2)[of A n B U] by simp +qed + +lemma unitary_mult_square_eq: + assumes "A\ carrier_mat n n" + and "U\ carrier_mat n n" + and "B \ carrier_mat n n" + and "A = mat_conj U B" + and "(Complex_Matrix.adjoint U) * U = 1\<^sub>m n" +shows "A * A = mat_conj U (B*B)" +proof - + have "A * A = U * B * (Complex_Matrix.adjoint U) * (U * B * (Complex_Matrix.adjoint U))" + using assms unfolding mat_conj_def by simp + also have "... = U * B * ((Complex_Matrix.adjoint U) * U) * (B * (Complex_Matrix.adjoint U))" + by (smt (z3) adjoint_dim_col adjoint_dim_row assms(3) assms(5) assoc_mult_mat carrier_matD(2) + carrier_mat_triv index_mult_mat(2) index_mult_mat(3) right_mult_one_mat') + also have "... = U * B * (B * (Complex_Matrix.adjoint U))" using assms by simp + also have "... = U * (B * B) * (Complex_Matrix.adjoint U)" + by (smt (z3) adjoint_dim_row assms(2) assms(3) assoc_mult_mat carrier_matD(2) + carrier_mat_triv index_mult_mat(3)) + finally show ?thesis unfolding mat_conj_def . +qed + +lemma hermitian_square_similar_mat_wit: + fixes A::"complex Matrix.mat" + assumes "hermitian A" + and "A\ carrier_mat n n" +and "unitary_diag A B U" +shows "similar_mat_wit (A * A) (B * B) U (Complex_Matrix.adjoint U)" +proof - + have "B\ carrier_mat n n" using unitary_diag_carrier[of A] assms by metis + hence "B * B\ carrier_mat n n" by simp + have "unitary U" using assms unitary_diagD[of A] by simp + have "A * A= mat_conj U (B*B)" using assms unitary_mult_square_eq[of A n] + by (metis \B \ carrier_mat n n\ \Complex_Matrix.unitary U\ mat_conj_def + unitarily_equiv_carrier(2) unitarily_equiv_eq unitary_diag_def + unitary_simps(1)) + moreover have "{A * A, B * B, U, Complex_Matrix.adjoint U} \ carrier_mat n n" + by (metis \B * B \ carrier_mat n n\ adjoint_dim' assms(2) assms(3) empty_subsetI + insert_subsetI mult_carrier_mat unitary_diag_carrier(2)) + moreover have "U * Complex_Matrix.adjoint U = 1\<^sub>m n \ Complex_Matrix.adjoint U * U = 1\<^sub>m n" + by (meson \Complex_Matrix.unitary U\ calculation(2) insert_subset unitary_simps(1) + unitary_simps(2)) + ultimately show ?thesis unfolding similar_mat_wit_def mat_conj_def by auto +qed + +lemma unitarily_equiv_square: + assumes "A\ carrier_mat n n" + and "unitarily_equiv A B U" + shows "unitarily_equiv (A*A) (B*B) U" +proof (rule unitarily_equivI) + show "unitary U" using assms unitarily_equivD(1)[of A] by simp + show "similar_mat_wit (A * A) (B * B) U (Complex_Matrix.adjoint U)" + by (smt (z3) \Complex_Matrix.unitary U\ assms carrier_matD(1) + carrier_matD(2) carrier_mat_triv index_mult_mat(2) + index_mult_mat(3) similar_mat_witI unitarily_equiv_carrier(1) + unitarily_equiv_carrier(2) unitarily_equiv_eq unitary_mult_square_eq + unitary_simps(1) unitary_simps(2) mat_conj_def) +qed + +lemma conjugate_eq_unitarily_equiv: + assumes "A\ carrier_mat n n" + and "V\ carrier_mat n n" + and "unitarily_equiv A B U" + and "unitary V" + and "V * B * (Complex_Matrix.adjoint V) = B" +shows "unitarily_equiv A B (U*V)" + unfolding unitarily_equiv_def similar_mat_wit_def Let_def +proof (intro conjI) + have "B\ carrier_mat n n" + using assms(1) assms(3) unitarily_equiv_carrier(1) by blast + have "U\ carrier_mat n n" + using assms(1) assms(3) unitarily_equiv_carrier(2) by auto + show u: "unitary (U*V)" + by (metis Complex_Matrix.unitary_def adjoint_dim_col assms(1) assms(2) + assms(3) assms(4) carrier_matD(2) index_mult_mat(3) unitarily_equivD(1) + unitarily_equiv_eq unitary_times_unitary) + thus l: "U * V * Complex_Matrix.adjoint (U * V) = 1\<^sub>m (dim_row A)" + by (metis Complex_Matrix.unitary_def assms(1) assms(2) carrier_matD(1) + carrier_matD(2) index_mult_mat(3) inverts_mat_def) + thus r: "Complex_Matrix.adjoint (U * V) * (U * V) = 1\<^sub>m (dim_row A)" using u + by (metis Complex_Matrix.unitary_def index_mult_mat(2) index_one_mat(2) + unitary_simps(1)) + show "{A, B, U * V, Complex_Matrix.adjoint (U * V)} \ + carrier_mat (dim_row A) (dim_row A)" + using \B \ carrier_mat n n\ \U \ carrier_mat n n\ adjoint_dim' assms + by auto + have "U * V * B * Complex_Matrix.adjoint (U * V) = + U * V * B * (Complex_Matrix.adjoint V * Complex_Matrix.adjoint U)" + by (metis \U \ carrier_mat n n\ adjoint_mult assms(2)) + also have "... = U * V * B * Complex_Matrix.adjoint V * + Complex_Matrix.adjoint U" + proof (rule assoc_mult_mat[symmetric], auto simp add: assms) + show "Complex_Matrix.adjoint V \ carrier_mat (dim_col B) (dim_col U)" + using \B \ carrier_mat n n\ \U \ carrier_mat n n\ adjoint_dim assms(2) + by auto + qed + also have "... = U * V * B * (Complex_Matrix.adjoint V * + Complex_Matrix.adjoint U)" + proof (rule assoc_mult_mat, auto simp add: assms) + show "Complex_Matrix.adjoint V \ carrier_mat (dim_col B) (dim_col U)" + by (metis \B \ carrier_mat n n\ \U \ carrier_mat n n\ adjoint_dim' + assms(2) carrier_matD(2)) + qed + also have "... = U * V * (B * (Complex_Matrix.adjoint V * + Complex_Matrix.adjoint U))" + proof (rule assoc_mult_mat, auto simp add: assms) + show "B \ carrier_mat (dim_col V) (dim_col V)" + by (metis \B \ carrier_mat n n\ assms(2) carrier_matD(2)) + qed + also have "... = U * (V * (B * (Complex_Matrix.adjoint V * + Complex_Matrix.adjoint U)))" + proof (rule assoc_mult_mat, auto simp add: assms) + show "V \ carrier_mat (dim_col U) (dim_row B)" + using \B \ carrier_mat n n\ \U \ carrier_mat n n\ assms(2) by auto + qed + finally have eq: "U * V * B * Complex_Matrix.adjoint (U * V) = + U * (V * (B * (Complex_Matrix.adjoint V * Complex_Matrix.adjoint U)))" . + have "V * (B * (Complex_Matrix.adjoint V * Complex_Matrix.adjoint U)) = + V * B * (Complex_Matrix.adjoint V * Complex_Matrix.adjoint U)" + proof (rule assoc_mult_mat[symmetric], auto simp add: assms) + show "B \ carrier_mat (dim_col V) (dim_col V)" + using \B \ carrier_mat n n\ assms(2) by auto + qed + also have "... = V * B * Complex_Matrix.adjoint V * Complex_Matrix.adjoint U" + proof (rule assoc_mult_mat[symmetric], auto simp add: assms) + show "Complex_Matrix.adjoint V \ carrier_mat (dim_col B) (dim_col U)" + by (metis \B \ carrier_mat n n\ \U \ carrier_mat n n\ + adjoint_dim_row assms(2) assms(5) carrier_matD(2) carrier_mat_triv + index_mult_mat(3)) + qed + also have "... = B * Complex_Matrix.adjoint U" using assms by simp + finally have "V *(B *(Complex_Matrix.adjoint V * Complex_Matrix.adjoint U)) = + B* Complex_Matrix.adjoint U" . + hence "U * V * B * Complex_Matrix.adjoint (U * V) = U * B * + Complex_Matrix.adjoint U" using eq + by (metis \B \ carrier_mat n n\ \U \ carrier_mat n n\ adjoint_dim' assoc_mult_mat) + also have "... = A" using assms unitarily_equiv_eq[of A B U] by simp + finally show "A = U * V * B * Complex_Matrix.adjoint (U * V)" by simp +qed + +definition real_diag_decomp where +"real_diag_decomp A B U \ unitary_diag A B U \ + (\i < dim_row B. B$$(i, i) \ Reals)" + +lemma real_diag_decompD[simp]: + assumes "real_diag_decomp A B U" + shows "unitary_diag A B U" + "(\i < dim_row B. B$$(i, i) \ Reals)" using assms + unfolding real_diag_decomp_def unitary_diag_def by auto + + +lemma hermitian_decomp_decomp': + fixes A::"complex Matrix.mat" + assumes "hermitian_decomp A B U" + shows "real_diag_decomp A B U" + using assms unfolding hermitian_decomp_def + by (metis real_diag_decomp_def unitarily_equiv_def unitary_diag_def) + +lemma real_diag_decomp_hermitian: + fixes A::"complex Matrix.mat" + assumes "real_diag_decomp A B U" + shows "hermitian A" +proof - + have ud: "unitary_diag A B U" using assms real_diag_decompD by simp + hence "A = U * B * (Complex_Matrix.adjoint U)" + by (simp add: unitarily_equiv_eq) + have "Complex_Matrix.adjoint A = + Complex_Matrix.adjoint (U * B * (Complex_Matrix.adjoint U))" + using ud assms unitarily_equiv_eq unitary_diag_imp_unitarily_equiv by blast + also have "... = Complex_Matrix.adjoint (Complex_Matrix.adjoint U) * + Complex_Matrix.adjoint B * Complex_Matrix.adjoint U" + by (smt (z3) ud Complex_Matrix.adjoint_adjoint Complex_Matrix.unitary_def + adjoint_dim_col adjoint_mult assms assoc_mult_mat calculation + carrier_matD(2) carrier_mat_triv index_mult_mat(2) index_mult_mat(3) + similar_mat_witD2(5) similar_mat_wit_dim_row unitary_diagD(1) + unitary_diagD(3)) + also have "... = U * Complex_Matrix.adjoint B * Complex_Matrix.adjoint U" + by (simp add: Complex_Matrix.adjoint_adjoint) + also have "... = U * B * Complex_Matrix.adjoint U" + using real_diagonal_hermitian + by (metis assms hermitian_def real_diag_decomp_def similar_mat_witD(5) + unitary_diagD(1) unitary_diagD(2)) + also have "... = A" using \A = U * B * (Complex_Matrix.adjoint U)\ by simp + finally show ?thesis unfolding hermitian_def by simp +qed + +lemma unitary_conjugate_real_diag_decomp: + assumes "A\ carrier_mat n n" + and "Us\ carrier_mat n n" + and "unitary Us" + and "real_diag_decomp (mat_conj (Complex_Matrix.adjoint Us) A) B U" + shows "real_diag_decomp A B (Us * U)" unfolding real_diag_decomp_def +proof (intro conjI allI impI) + show "\i. i < dim_row B \ B $$ (i, i) \ \" using assms + unfolding real_diag_decomp_def by simp + show "unitary_diag A B (Us * U)" unfolding unitary_diag_def + proof (rule conjI) + show "diagonal_mat B" using assms real_diag_decompD(1) unitary_diagD(2) + by metis + show "unitarily_equiv A B (Us * U)" + proof (rule unitarily_equiv_conjugate) + show "A\ carrier_mat n n" using assms by simp + show "unitary Us" using assms by simp + show "Us \ carrier_mat n n" using assms by simp + show "unitarily_equiv (mat_conj (Complex_Matrix.adjoint Us) A) B U" + using assms real_diag_decompD(1) unfolding unitary_diag_def by metis + thus "U \ carrier_mat n n" + by (metis (mono_tags) adjoint_dim' assms(2) carrier_matD(1) + index_mult_mat(2) mat_conj_def unitarily_equiv_carrier'(3)) + show "B\ carrier_mat n n" + using \unitarily_equiv (mat_conj (Complex_Matrix.adjoint Us) A) B U\ + assms(2) unitarily_equiv_carrier'(2) + by (metis \U \ carrier_mat n n\ carrier_matD(2) + unitarily_equiv_carrier'(3)) + qed + qed +qed + +subsection \On the spectrum of a matrix\ + +lemma similar_spectrum_eq: + fixes A::"complex Matrix.mat" + assumes "A\ carrier_mat n n" + and "similar_mat A B" + and "upper_triangular B" + shows "spectrum A = set (diag_mat B)" +proof - + have "(\a\(eigvals A). [:- a, 1:]) = char_poly A" + using eigvals_poly_length assms by simp + also have "... = char_poly B" + proof (rule char_poly_similar) + show "similar_mat A B" using assms real_diag_decompD(1) + using similar_mat_def by blast + qed + also have "... = (\a\diag_mat B. [:- a, 1:])" + proof (rule char_poly_upper_triangular) + show "B\ carrier_mat n n" using assms similar_matD by auto + thus "upper_triangular B" using assms by simp + qed + finally have "(\a\(eigvals A). [:- a, 1:]) = (\a\diag_mat B. [:- a, 1:])" . + thus ?thesis using poly_root_set_eq unfolding spectrum_def by metis +qed + +lemma unitary_diag_spectrum_eq: + fixes A::"complex Matrix.mat" + assumes "A\ carrier_mat n n" + and "unitary_diag A B U" +shows "spectrum A = set (diag_mat B)" +proof (rule similar_spectrum_eq) + show "A \ carrier_mat n n" using assms by simp + show "similar_mat A B" using assms unitary_diagD(1) + by (metis similar_mat_def) + show "upper_triangular B" using assms + unitary_diagD(2) unitary_diagD(1) diagonal_imp_upper_triangular + by (metis similar_mat_witD2(5)) +qed + +lemma unitary_diag_spectrum_eq': + fixes A::"complex Matrix.mat" + assumes "A\ carrier_mat n n" + and "unitary_diag A B U" +shows "spectrum A = diag_elems B" +proof - + have "spectrum A = set (diag_mat B)" using assms unitary_diag_spectrum_eq + by simp + also have "... = diag_elems B" using diag_elems_set_diag_mat[of B] by simp + finally show "spectrum A = diag_elems B" . +qed + +lemma hermitian_real_diag_decomp: + fixes A::"complex Matrix.mat" + assumes "A\ carrier_mat n n" + and "0 < n" + and "hermitian A" +obtains B U where "real_diag_decomp A B U" +proof - + { + have es: "char_poly A = (\ (e :: complex) \ (eigvals A). [:- e, 1:])" + using assms eigvals_poly_length by auto + obtain B U Q where us: "unitary_schur_decomposition A (eigvals A) = (B,U,Q)" + by (cases "unitary_schur_decomposition A (eigvals A)") + hence pr: "similar_mat_wit A B U (Complex_Matrix.adjoint U) \ diagonal_mat B \ + diag_mat B = (eigvals A) \ unitary U \ (\i < n. B$$(i, i) \ Reals)" + using hermitian_eigenvalue_real assms es by auto + moreover have "dim_row B = n" using assms similar_mat_wit_dim_row[of A] + pr by auto + ultimately have "real_diag_decomp A B U" using unitary_diagI[of A] + unfolding real_diag_decomp_def by simp + hence "\ B U. real_diag_decomp A B U" by auto + } + thus ?thesis using that by auto +qed + +lemma spectrum_smult: + fixes A::"complex Matrix.mat" + assumes "hermitian A" + and "A\ carrier_mat n n" + and "0 < n" +shows "spectrum (x \\<^sub>m A) = {x * a|a. a\ spectrum A}" +proof - + obtain B U where bu: "real_diag_decomp A B U" + using assms hermitian_real_diag_decomp[of A] by auto + hence "spectrum (x \\<^sub>m A) = set (diag_mat (x \\<^sub>m B))" + using assms unitary_diag_spectrum_eq[of "x \\<^sub>m A"] + unitarily_equiv_smult[of A] + by (meson diagonal_mat_smult real_diag_decompD(1) real_diag_decompD(2) + smult_carrier_mat unitary_diag_def) + also have "... = {x * a |a. a \ set (diag_mat B)}" + using assms set_diag_mat_smult[of B n x ] + by (meson bu real_diag_decompD(1) unitary_diag_carrier(1)) + also have "... = {x * a|a. a\ spectrum A}" + using assms unitary_diag_spectrum_eq[of A] bu real_diag_decompD(1) + by metis + finally show ?thesis . +qed + +lemma spectrum_uminus: + fixes A::"complex Matrix.mat" + assumes "hermitian A" + and "A\ carrier_mat n n" + and "0 < n" +shows "spectrum (-A) = {-a|a. a\ spectrum A}" +proof - + obtain B U where bu: "real_diag_decomp A B U" + using assms hermitian_real_diag_decomp[of A] by auto + hence "spectrum (-A) = set (diag_mat (-B))" + using assms unitary_diag_spectrum_eq[of "-A"] + unitarily_equiv_uminus[of A] + by (meson diagonal_mat_uminus real_diag_decompD uminus_carrier_iff_mat + unitary_diag_def) + also have "... = {-a |a. a \ set (diag_mat B)}" + using assms set_diag_mat_uminus[of B n] + by (meson bu real_diag_decompD(1) unitary_diag_carrier(1)) + also have "... = {-a|a. a\ spectrum A}" + using assms unitary_diag_spectrum_eq[of A] bu real_diag_decompD(1) + by metis + finally show ?thesis . +qed + +section \Properties of the inner product\ + +subsection \Some analysis complements\ + +lemma add_conj_le: + shows "z + cnj z \ 2 * cmod z" +proof - + have z: "z + cnj z = 2 * Re z" by (simp add: complex_add_cnj) + have "Re z \ cmod z" by (simp add: complex_Re_le_cmod) + hence "2 *complex_of_real (Re z) \ 2 * complex_of_real (cmod z)" + using less_eq_complex_def by auto + thus ?thesis using z by simp +qed + +lemma abs_real: + fixes x::complex + assumes "x\ Reals" + shows "abs x \ Reals" unfolding abs_complex_def by auto + +lemma csqrt_cmod_square: + shows "csqrt ((cmod z)\<^sup>2) = cmod z" +proof - + have "csqrt ((cmod z)\<^sup>2) = sqrt (Re ((cmod z)\<^sup>2))" by force + also have "... = cmod z" by simp + finally show ?thesis . +qed + +lemma cpx_real_le: + fixes z::complex + assumes "0 \ z" + and "0 \ u" + and "z\<^sup>2 \ u\<^sup>2" +shows "z \ u" +proof - + have "z^2 = Re (z^2)" "u^2 = Re (u^2)" using assms + by (metis Im_complex_of_real Im_power_real Re_complex_of_real + complex_eq_iff less_eq_complex_def zero_complex.sel(2))+ + hence rl: "Re (z^2) \ Re (u^2)" using assms less_eq_complex_def by simp + have "sqrt (Re (z^2)) = z" "sqrt (Re (u^2)) = u" using assms complex_eqI + less_eq_complex_def by auto + have "z = sqrt (Re (z^2))" using assms complex_eqI less_eq_complex_def + by auto + also have "... \ sqrt (Re (u^2))" using rl less_eq_complex_def by simp + finally show "z \ u" using assms complex_eqI less_eq_complex_def by auto +qed + +lemma mult_conj_real: + fixes v::complex + shows "v * (conjugate v) \ Reals" +proof - + have "0 \ v * (conjugate v)" using less_eq_complex_def by simp + thus ?thesis by (simp add: complex_is_Real_iff) +qed + +lemma real_sum_real: + assumes "\i. i < n \ ((f i)::complex) \ Reals" + shows "(\ i \ {0 ..< n}. f i) \ Reals" + using assms atLeastLessThan_iff by blast + +lemma real_mult_re: + assumes "a\ Reals" and "b\ Reals" + shows "Re (a * b) = Re a * Re b" using assms + by (metis Re_complex_of_real Reals_cases of_real_mult) + + +lemma complex_positive_Im: + fixes b::complex + assumes "0 \ b" + shows "Im b = 0" + by (metis assms less_eq_complex_def zero_complex.simps(2)) + +lemma cmod_pos: + fixes z::complex + assumes "0 \ z" + shows "cmod z = z" +proof - + have "Im z = 0" using assms complex_positive_Im by simp + thus ?thesis using complex_norm + by (metis assms complex.exhaust_sel complex_of_real_def less_eq_complex_def norm_of_real + real_sqrt_abs real_sqrt_pow2 real_sqrt_power zero_complex.simps(1)) +qed + +lemma cpx_pos_square_pos: + fixes z::complex + assumes "0 \ z" + shows "0 \ z\<^sup>2" +proof - + have "Im z = 0" using assms by (simp add: complex_positive_Im) + hence "Re (z\<^sup>2) = (Re z)\<^sup>2" by simp + moreover have "Im (z\<^sup>2) = 0" by (simp add: \Im z = 0\) + ultimately show ?thesis by (simp add: less_eq_complex_def) +qed + +lemma cmod_mult_pos: + fixes b:: complex + fixes z::complex + assumes "0 \ b" + shows "cmod (b * z) = Re b * cmod z" using complex_positive_Im + Im_complex_of_real Re_complex_of_real abs_of_nonneg assms cmod_Im_le_iff + less_eq_complex_def norm_mult of_real_0 + by (metis (full_types) cmod_eq_Re) + + + +lemma cmod_conjugate_square_eq: + fixes z::complex + shows "cmod (z * (conjugate z)) = z * (conjugate z)" +proof - + have "0 \ z * (conjugate z)" + using conjugate_square_positive less_eq_complex_def by auto + thus ?thesis using cmod_pos by simp +qed + + +lemma pos_sum_gt_comp: + assumes "finite I" +and "\i. i \ I \ (0::real) \ f i" +and "j\ I" +and "c < f j" +shows "c < sum f I" +proof - + have "c < f j" using assms by simp + also have "... \ f j + sum f (I -{j})" + by (smt (z3) DiffD1 assms(2) sum_nonneg) + also have "... = sum f I" using assms + by (simp add: sum_diff1) + finally show ?thesis . +qed + +lemma pos_sum_le_comp: + assumes "finite I" +and "\i. i \ I \ (0::real) \ f i" +and "sum f I \ c" +shows "\i \ I. f i \ c" +proof (rule ccontr) + assume "\ (\i\I. f i \ c)" + hence "\j\ I. c < f j" by fastforce + from this obtain j where "j\ I" and "c < f j" by auto + hence "c < sum f I" using assms pos_sum_gt_comp[of I] by simp + thus False using assms by simp +qed + + +lemma square_pos_mult_le: + assumes "finite I" + and "\i. i \ I \ ((0::real) \ f i \ f i \ 1)" +shows "sum (\x. f x * f x) I \ sum f I" using assms +proof (induct rule:finite_induct) +case empty + then show ?case by simp +next + case (insert x F) + have "sum (\x. f x * f x) (insert x F) = f x * f x + sum (\x. f x * f x) F" + by (simp add: insert) + also have "... \ f x * f x + sum f F" using insert by simp + also have "... \ f x + sum f F" using insert mult_left_le[of "f x" "f x"] + by simp + also have "... = sum f (insert x F)" using insert by simp + finally show ?case . +qed + + + +lemma square_pos_mult_lt: + assumes "finite I" + and "\i. i \ I \ ((0::real) \ f i \ f i \ 1)" + and "j \ I" + and "f j < 1" + and "0 < f j" +shows "sum (\x. f x * f x) I < sum f I" using assms +proof - + have "sum (\x. f x * f x) I = + sum (\x. f x * f x) {j} + sum (\x. f x * f x) (I-{j})" + using assms sum.remove by fastforce + also have "... = f j * f j + sum (\x. f x * f x) (I-{j})" by simp + also have "... < f j + sum (\x. f x * f x) (I-{j})" using assms by simp + also have "... \ f j + sum f (I - {j})" + using assms square_pos_mult_le[of "I - {j}"] by simp + also have "... = sum f I" + by (metis assms(1) assms(3) sum.remove) + finally show ?thesis . +qed + +subsection \Inner product results\ + +text \In particular we prove the triangle inequality, i.e. that for vectors $u$ and $v$ +we have $\| u+ v \| \leq \| u \| + \| v \|$.\ + +lemma inner_prod_vec_norm_pow2: + shows "(vec_norm v)\<^sup>2 = v \c v" using vec_norm_def + by (metis power2_csqrt) + +lemma inner_prod_mult_mat_vec_left: + assumes "v \ carrier_vec n" + and "w \ carrier_vec n'" + and "A \ carrier_mat m n" + and "B \ carrier_mat m n'" +shows "inner_prod (A *\<^sub>v v) (B *\<^sub>v w) = + inner_prod (((Complex_Matrix.adjoint B) * A) *\<^sub>v v) w" +proof - + have "inner_prod (A *\<^sub>v v) (B *\<^sub>v w) = + inner_prod (Complex_Matrix.adjoint B *\<^sub>v (A *\<^sub>v v)) w" + using adjoint_def_alter by (metis assms mult_mat_vec_carrier) + also have "... = inner_prod (((Complex_Matrix.adjoint B) * A) *\<^sub>v v) w" + proof - + have "Complex_Matrix.adjoint B *\<^sub>v (A *\<^sub>v v) = + ((Complex_Matrix.adjoint B) * A) *\<^sub>v v" + proof (rule assoc_mult_mat_vec[symmetric], (auto simp add: assms)) + show "v \ carrier_vec n" using assms by simp + show "A \ carrier_mat (dim_row B) n" using assms by auto + qed + thus ?thesis by simp + qed + finally show ?thesis . +qed + +lemma rank_1_proj_trace_inner: + fixes A :: "'a::conjugatable_field Matrix.mat" and v :: "'a Matrix.vec" + assumes A: "A \ carrier_mat n n" + and v: "v \ carrier_vec n" + shows "Complex_Matrix.trace (A * (rank_1_proj v)) = Complex_Matrix.inner_prod v (A *\<^sub>v v)" + using assms trace_outer_prod_right[of A] unfolding rank_1_proj_def by simp + +lemma unitary_inner_prod: + assumes "v\ carrier_vec n" + and "w \ carrier_vec n" + and "U \ carrier_mat n n" + and "Complex_Matrix.unitary U" +shows "inner_prod (U *\<^sub>v v) (U *\<^sub>v w) = inner_prod v w" +proof - + have "inner_prod (U *\<^sub>v v) (U *\<^sub>v w) = + inner_prod (((Complex_Matrix.adjoint U) * U) *\<^sub>v v) w" + using assms by (simp add: inner_prod_mult_mat_vec_left) + also have "... = inner_prod (1\<^sub>m n *\<^sub>v v) w" using assms by simp + also have "... = inner_prod v w" using assms by simp + finally show ?thesis . +qed + +lemma unitary_vec_norm: + assumes "v\ carrier_vec n" + and "U \ carrier_mat n n" + and "Complex_Matrix.unitary U" +shows "vec_norm (U *\<^sub>v v) = vec_norm v" using unitary_inner_prod assms unfolding vec_norm_def + by metis + +lemma unitary_col_norm_square: + assumes "unitary U" +and "U\ carrier_mat n n" + and "i < n" +shows "\Matrix.col U i\\<^sup>2 = 1" +proof - + define vn::"complex Matrix.vec" where "vn = unit_vec n i" + have "\Matrix.col U i\\<^sup>2 = (vec_norm (Matrix.col U i))\<^sup>2" using vec_norm_sq_cpx_vec_length_sq by simp + also have "... = (vec_norm vn)\<^sup>2" using assms unitary_vec_norm + by (metis mat_unit_vec_col unit_vec_carrier vn_def) + also have "... = \vn\\<^sup>2" using vec_norm_sq_cpx_vec_length_sq by simp + also have "... = 1" using assms unfolding vn_def by simp + finally show ?thesis by blast +qed + +lemma unitary_col_norm: + assumes "unitary U" +and "U\ carrier_mat n n" + and "i < n" +shows "\Matrix.col U i\ = 1" using assms unitary_col_norm_square cpx_vec_length_inner_prod + inner_prod_csqrt by (metis csqrt_1 of_real_eq_1_iff) + +lemma inner_mult_diag_expand: + fixes B::"complex Matrix.mat" + assumes "diagonal_mat B" + and "B \ carrier_mat n n" + and "v \ carrier_vec n" +shows "inner_prod (B *\<^sub>v v) v = + (\ i \ {0 ..< n}. (conjugate (B $$ (i,i))) * (vec_index v i * + (conjugate (vec_index v i))))" +proof - + have idx: "\i. i < n \ vec_index (B *\<^sub>v v) i = B $$ (i,i) * (vec_index v i)" + using assms diagonal_mat_mult_vec by blast + have "inner_prod (B *\<^sub>v v) v = + (\ i \ {0 ..< n}. vec_index v i * vec_index (conjugate (B *\<^sub>v v)) i)" + unfolding Matrix.scalar_prod_def using assms by fastforce + also have "... = (\ i \ {0 ..< n}. vec_index v i * conjugate (vec_index (B *\<^sub>v v) i))" + using assms by force + also have "... = (\ i \ {0 ..< n}. (conjugate (B $$ (i,i))) * (vec_index v i * + (conjugate (vec_index v i))))" + proof (rule sum.cong, simp) + show "\i. i \ {0 ..< n} \ vec_index v i * conjugate (vec_index (B *\<^sub>v v) i) = + (conjugate (B $$ (i,i))) * (vec_index v i * (conjugate (vec_index v i)))" + by (simp add: idx) + qed + finally show ?thesis . +qed + +lemma inner_mult_diag_expand': + fixes B::"complex Matrix.mat" + assumes "diagonal_mat B" + and "B \ carrier_mat n n" + and "v \ carrier_vec n" +shows "inner_prod v (B *\<^sub>v v) = + (\ i \ {0 ..< n}. B $$ (i,i) * (vec_index v i * + (conjugate (vec_index v i))))" +proof - + have idx: "\i. i < n \ vec_index (B *\<^sub>v v) i = B $$ (i,i) * (vec_index v i)" + using assms diagonal_mat_mult_vec by blast + have "inner_prod v (B *\<^sub>v v) = + (\ i \ {0 ..< n}. vec_index (B *\<^sub>v v) i * vec_index (conjugate v) i)" + unfolding Matrix.scalar_prod_def using assms by fastforce + also have "... = + (\ i \ {0 ..< n}. vec_index (B *\<^sub>v v) i * conjugate (vec_index v i))" + using assms by force + also have "... = (\ i \ {0 ..< n}. (B $$ (i,i)) * (vec_index v i * + (conjugate (vec_index v i))))" + proof (rule sum.cong, simp) + show "\i. i \ {0 ..< n} \ + vec_index (B *\<^sub>v v) i * conjugate (vec_index v i) = + (B $$ (i,i)) * (vec_index v i * (conjugate (vec_index v i)))" + by (simp add: idx) + qed + finally show ?thesis . +qed + +lemma self_inner_prod_real: + fixes v::"complex Matrix.vec" + shows "Complex_Matrix.inner_prod v v \ Reals" +proof - + have "Im (Complex_Matrix.inner_prod v v) = 0" + using self_cscalar_prod_geq_0 by simp + thus ?thesis using complex_is_Real_iff by auto +qed + +lemma inner_mult_diag_real: + fixes B::"complex Matrix.mat" + assumes "diagonal_mat B" + and "B \ carrier_mat n n" + and "\i < n. B$$(i, i) \ Reals" + and "v \ carrier_vec n" +shows "inner_prod (B *\<^sub>v v) v \ Reals" +proof - + have "inner_prod (B *\<^sub>v v) v = + (\ i \ {0 ..< n}. (conjugate (B $$ (i,i))) * (vec_index v i * + (conjugate (vec_index v i))))" using inner_mult_diag_expand assms + by simp + also have "... \ Reals" + proof (rule real_sum_real) + show "\i. i < n \ + conjugate (B $$ (i, i)) * + ((vec_index v i) * conjugate (vec_index v i)) \ \" + using assms mult_conj_real by auto + qed + finally show ?thesis . +qed + +lemma inner_mult_diag_real': + fixes B::"complex Matrix.mat" + assumes "diagonal_mat B" + and "B \ carrier_mat n n" + and "\i < n. B$$(i, i) \ Reals" + and "v \ carrier_vec n" +shows "inner_prod v (B *\<^sub>v v) \ Reals" +proof - + have "inner_prod v (B *\<^sub>v v) = + (\ i \ {0 ..< n}. B $$ (i,i) * (vec_index v i * + (conjugate (vec_index v i))))" + using inner_mult_diag_expand' assms by simp + also have "... \ Reals" + proof (rule real_sum_real) + show "\i. i < n \ + B $$ (i, i) * ((vec_index v i) * conjugate (vec_index v i)) \ \" + using assms mult_conj_real by auto + qed + finally show ?thesis . +qed + +lemma inner_prod_mult_mat_vec_right: +assumes "v \ carrier_vec n" + and "w \ carrier_vec n'" + and "A \ carrier_mat m n" + and "B \ carrier_mat m n'" +shows "inner_prod (A *\<^sub>v v) (B *\<^sub>v w) = + inner_prod v (((Complex_Matrix.adjoint A) * B) *\<^sub>v w)" +proof - + have "inner_prod (A *\<^sub>v v) (B *\<^sub>v w) = + inner_prod ((Complex_Matrix.adjoint (Complex_Matrix.adjoint A)) *\<^sub>v v) + (B *\<^sub>v w)" + by (simp add: Complex_Matrix.adjoint_adjoint) + also have "... = inner_prod v ((Complex_Matrix.adjoint A) *\<^sub>v (B *\<^sub>v w))" + proof (rule adjoint_def_alter[symmetric]) + show "v \ carrier_vec n" using assms by simp + show "B *\<^sub>v w \ carrier_vec m" using assms by simp + show "Complex_Matrix.adjoint A \ carrier_mat n m" + using assms adjoint_dim'[of A] by simp + qed + also have "... = inner_prod v (((Complex_Matrix.adjoint A) * B) *\<^sub>v w)" + using assms + proof - + have "(Complex_Matrix.adjoint A) *\<^sub>v (B *\<^sub>v w) = + ((Complex_Matrix.adjoint A) * B) *\<^sub>v w" + proof (rule assoc_mult_mat_vec[symmetric], (auto simp add: assms)) + show "w \ carrier_vec n'" using assms by simp + show "B \ carrier_mat (dim_row A) n'" using assms by auto + qed + thus ?thesis by simp + qed + finally show ?thesis . +qed + +lemma Cauchy_Schwarz_complex_vec_norm: +assumes "dim_vec x = dim_vec y" +shows "cmod (inner_prod x y) \ vec_norm x * vec_norm y" +proof - + have x: "x \ carrier_vec (dim_vec x)" by simp + moreover have y: "y \ carrier_vec (dim_vec x)" using assms by simp + ultimately have "(cmod (inner_prod x y))\<^sup>2 = inner_prod x y * inner_prod y x" + using complex_norm_square by (metis inner_prod_swap mult_conj_cmod_square) + also have "... \ inner_prod x x * inner_prod y y" + using Cauchy_Schwarz_complex_vec x y by blast + finally have "(cmod (inner_prod x y))\<^sup>2 \ inner_prod x x * inner_prod y y" . + hence "(cmod (inner_prod x y))\<^sup>2 \ Re (inner_prod x x) * Re (inner_prod y y)" + using less_eq_complex_def by simp + hence "sqrt ((cmod (inner_prod x y))\<^sup>2) \ + sqrt (Re (inner_prod x x) * Re (inner_prod y y))" + using real_sqrt_le_iff by blast + also have "... = sqrt (Re (inner_prod x x)) * sqrt (Re (inner_prod y y))" + by (simp add: real_sqrt_mult) + finally have "sqrt ((cmod (inner_prod x y))\<^sup>2) \ + sqrt (Re (inner_prod x x)) * sqrt (Re (inner_prod y y))" . + thus ?thesis using less_eq_complex_def by (simp add: vec_norm_def) +qed + +lemma vec_norm_triangle_sq: + fixes u::"complex Matrix.vec" + assumes "dim_vec u = dim_vec v" + shows "(vec_norm (u+ v))\<^sup>2 \ (vec_norm u + vec_norm v)\<^sup>2" +proof - + have "(vec_norm (u+v))\<^sup>2 = inner_prod (u+v) (u+v)" + by (simp add: inner_prod_vec_norm_pow2) + also have "... = inner_prod u u + inner_prod u v + inner_prod v u + + inner_prod v v" + using assms add_scalar_prod_distrib conjugate_add_vec + by (smt (z3) ab_semigroup_add_class.add_ac(1) carrier_vec_dim_vec + dim_vec_conjugate index_add_vec(2) scalar_prod_add_distrib) + also have "... = (vec_norm u)^2 + inner_prod u v + inner_prod v u + + (vec_norm v)^2" + by (simp add: inner_prod_vec_norm_pow2) + also have "... \ (vec_norm u)^2 + 2 * cmod (inner_prod u v) + (vec_norm v)^2" + by (metis add_conj_le add_left_mono add_right_mono assms + carrier_vec_dim_vec conjugate_complex_def inner_prod_swap + is_num_normalize(1)) + also have "... \ (vec_norm u)^2 + 2 * ((vec_norm u)*(vec_norm v)) + + (vec_norm v)^2" + using Cauchy_Schwarz_complex_vec_norm[of u v] assms less_eq_complex_def + by auto + also have "... = (vec_norm u + vec_norm v)\<^sup>2" by (simp add: power2_sum) + finally show ?thesis . +qed + +lemma vec_norm_triangle: +fixes u::"complex Matrix.vec" + assumes "dim_vec u = dim_vec v" + shows "vec_norm (u+ v) \ vec_norm u + vec_norm v" +proof (rule cpx_real_le) + show "(vec_norm (u + v))\<^sup>2 \ (vec_norm u + vec_norm v)\<^sup>2" + using assms vec_norm_triangle_sq by simp + show "0 \ vec_norm (u + v)" using vec_norm_geq_0 by simp + show "0 \ vec_norm u + vec_norm v" using vec_norm_geq_0 by simp +qed + + +section \Matrix decomposition\ + +lemma (in cpx_sq_mat) sum_decomp_cols: + fixes A::"complex Matrix.mat" + assumes "hermitian A" + and "A \ fc_mats" + and "unitary_diag A B U" +shows "sum_mat (\i. (diag_mat B ! i) \\<^sub>m rank_1_proj (Matrix.col U i)) + {..< dimR} = A" +proof - + have "similar_mat_wit A B U (Complex_Matrix.adjoint U) \ diagonal_mat B \ + unitary U" + by (metis assms(3) unitary_diagD(1) unitary_diagD(2) unitary_diagD(3)) + hence A: "A = U * B * (Complex_Matrix.adjoint U)" and dB: "diagonal_mat B" + and dimB: "B \ carrier_mat dimR dimR" and dimP: "U \ carrier_mat dimR dimR" + and unit: "unitary U" + unfolding similar_mat_wit_def Let_def using assms fc_mats_carrier by auto + have pz: "\i. i < dimR \ (Matrix.col U i) = zero_col U i" + unfolding zero_col_def by simp + have "sum_mat (\i. (diag_mat B ! i) \\<^sub>m + rank_1_proj (Matrix.col U i)) {..< dimR} = + U * B * Complex_Matrix.adjoint U" + proof (rule weighted_sum_rank_1_proj_unitary) + show "diagonal_mat B" using dB . + show "Complex_Matrix.unitary U" using unit . + show "U \ fc_mats" using fc_mats_carrier dim_eq dimP by simp + show "B\ fc_mats" using fc_mats_carrier dim_eq dimB by simp + qed + thus ?thesis using A by simp +qed + +lemma unitary_col_inner_prod: + assumes "A \ carrier_mat n n" + and "0 < n" +and "Complex_Matrix.unitary A" +and "j < n" +and "k < n" +shows "Complex_Matrix.inner_prod (Matrix.col A j) (Matrix.col A k) = + (1\<^sub>m n) $$ (j,k)" +proof - + have "Complex_Matrix.inner_prod (Matrix.col A j) (Matrix.col A k) = + (Complex_Matrix.adjoint A * A) $$ (j, k)" + using inner_prod_adjoint_comp[of A n A] assms + by simp + also have "... = (1\<^sub>m n) $$ (j,k)" using assms + unfolding Complex_Matrix.unitary_def + by (simp add: assms(3)) + finally show ?thesis . +qed + +lemma (in cpx_sq_mat) sum_mat_ortho_proj: + assumes "finite I" + and "j \ I" + and "A j * A j = A j" + and "\i. i\ I \ A i \ fc_mats" + and "\ i . i\ I \ i\ j \ A i * (A j) = (0\<^sub>m dimR dimR)" + shows "(sum_mat A I) * (A j) = (A j)" using assms +proof (induct rule:finite_induct) + case empty + then show ?case using dim_eq by auto +next + case (insert x F) + have "(sum_mat A (insert x F)) * (A j) = + (A x + sum_mat A F) * (A j)" using insert sum_mat_insert[of A] + by (simp add: image_subset_iff) + also have "... = A x * (A j) + sum_mat A F * (A j)" + proof (rule add_mult_distrib_mat) + show "A x \ carrier_mat dimR dimC" using insert fc_mats_carrier by simp + show "sum_mat A F \ carrier_mat dimR dimC" using insert + by (metis insert_iff local.fc_mats_carrier sum_mat_carrier) + show "A j \ carrier_mat dimC dimC" using insert dim_eq fc_mats_carrier by force + qed + also have "... = A j" + proof (cases "x = j") + case True + hence "j\ F" using insert by auto + hence "sum_mat A F * A j = 0\<^sub>m dimR dimR" using insert sum_mat_left_ortho_zero[of F A "A j"] + using True ball_insert dim_eq by auto + thus ?thesis using insert True dim_eq fc_mats_carrier by auto + next + case False + hence "j\ F" using insert by auto + moreover have "\i. i \ F \ A i \ fc_mats" using insert by simp + moreover have "\i. i \ F \ i \ j \ A i * A j = 0\<^sub>m dimR dimR" using insert by simp + ultimately have "sum_mat A F * A j = A j" using insert by simp + thus ?thesis using False dim_eq fc_mats_carrier insert by auto + qed + finally show ?case . +qed + +lemma (in cpx_sq_mat) sum_mat_ortho_one: + assumes "finite I" + and "j\ I" + and "B \ fc_mats" + and "\i. i\ I \ A i \ fc_mats" + and "\ i . i\ I \ i\ j \ A i * B = (0\<^sub>m dimR dimR)" + shows "(sum_mat A I) * B = A j * B" using assms +proof (induct rule:finite_induct) + case empty + then show ?case using dim_eq by auto +next + case (insert x F) + have "(sum_mat A (insert x F)) * B = + (A x + sum_mat A F) * B" using insert sum_mat_insert[of A] + by (simp add: image_subset_iff) + also have "... = A x * B + sum_mat A F * B" + proof (rule add_mult_distrib_mat) + show "A x \ carrier_mat dimR dimC" using insert fc_mats_carrier by simp + show "sum_mat A F \ carrier_mat dimR dimC" using insert + by (metis insert_iff local.fc_mats_carrier sum_mat_carrier) + show "B \ carrier_mat dimC dimC" using insert dim_eq fc_mats_carrier by force + qed + also have "... = A j * B" + proof (cases "x = j") + case True + hence "j\ F" using insert by auto + hence "sum_mat A F * B = 0\<^sub>m dimR dimR" using insert sum_mat_left_ortho_zero[of F A B] + using True ball_insert dim_eq by auto + thus ?thesis using insert True dim_eq fc_mats_carrier + by (metis Complex_Matrix.right_add_zero_mat cpx_sq_mat_mult) + next + case False + hence "j\ F" using insert by auto + moreover have "\i. i \ F \ A i \ fc_mats" using insert by simp + moreover have "\i. i \ F \ i \ j \ A i * B = 0\<^sub>m dimR dimR" using insert by simp + ultimately have "sum_mat A F * B = A j * B" using insert by simp + thus ?thesis using False dim_eq fc_mats_carrier insert + by (metis add_zero cpx_sq_mat_mult insertI1) + qed + finally show ?case . +qed + +lemma unitarily_equiv_rank_1_proj_col_carrier: + assumes "A\ carrier_mat n n" +and "unitarily_equiv A B U" +and "i < n" +shows "rank_1_proj (Matrix.col U i) \ carrier_mat n n" + using rank_1_proj_col_carrier assms + by (metis carrier_matD(1) carrier_matD(2) unitarily_equiv_carrier(2)) + +lemma decomp_eigenvector: + fixes A::"complex Matrix.mat" + assumes "A \ carrier_mat n n" + and "0 < n" + and "hermitian A" + and "unitary_diag A B U" +and "j < n" +shows "Complex_Matrix.trace (A * (rank_1_proj (Matrix.col U j))) = B $$(j,j)" +proof - + define fc::"complex Matrix.mat set" where "fc = carrier_mat n n" + interpret cpx_sq_mat n n fc + proof + show "0 < n" using assms by simp + qed (auto simp add: fc_def) + have rf: "\i. i < n \ rank_1_proj (Matrix.col U i) \ fc" using + assms unitarily_equiv_rank_1_proj_col_carrier + by (metis fc_def unitary_diag_imp_unitarily_equiv) + hence sm: "\i. i < n \ diag_mat B ! i \\<^sub>m rank_1_proj (Matrix.col U i) \ fc" + using fc_mats_carrier dim_eq by simp + have "A * (rank_1_proj (Matrix.col U j)) = + (sum_mat (\i. (diag_mat B ! i) \\<^sub>m (rank_1_proj (Matrix.col U i))) {..< n}) * + (rank_1_proj (Matrix.col U j))" using assms sum_decomp_cols + unfolding fc_def by simp + also have "... = diag_mat B ! j \\<^sub>m rank_1_proj (Matrix.col U j) * + rank_1_proj (Matrix.col U j)" + proof (rule sum_mat_ortho_one, (auto simp add: assms)) + show "rank_1_proj (Matrix.col U j) \ fc" by (simp add: assms rf) + show "\i. i < n \ diag_mat B ! i \\<^sub>m rank_1_proj (Matrix.col U i) \ fc" + by (simp add: sm) + show "\i. i < n \ i \ j \ + diag_mat B ! i \\<^sub>m rank_1_proj (Matrix.col U i) * + rank_1_proj (Matrix.col U j) = 0\<^sub>m n n" + proof - + fix i + assume "i < n" and "i \ j" + define OP where "OP = outer_prod (Matrix.col U i) (Matrix.col U j)" + have cm: "OP \ carrier_mat n n" unfolding OP_def + proof (rule outer_prod_dim) + have "dim_row U = n" + using assms unitary_diag_carrier(2) fc_mats_carrier + by (metis carrier_matD(1)) + thus "Matrix.col U i \ carrier_vec n" using\i < n\ + by (simp add: carrier_vecI) + show "Matrix.col U j \ carrier_vec n" using assms \dim_row U = n\ + by (simp add: carrier_vecI) + qed + have "rank_1_proj (Matrix.col U i) * rank_1_proj (Matrix.col U j) = + 1\<^sub>m n $$ (i, j) \\<^sub>m outer_prod (Matrix.col U i) (Matrix.col U j)" + proof (rule rank_1_proj_unitary, (auto simp add: \i < n\ assms)) + show "U \ fc" using assms unitary_diag_carrier(2) + fc_mats_carrier by simp + show "Complex_Matrix.unitary U" using assms unitary_diag_carrier + unitary_diagD(3) by blast + qed + also have "... = 0 \\<^sub>m outer_prod (Matrix.col U i) (Matrix.col U j)" + using \i \ j\ + by (metis \i < n\ assms(5) index_one_mat(1)) + also have "... = 0\<^sub>m n n" using cm smult_zero unfolding OP_def by auto + finally show "diag_mat B ! i \\<^sub>m rank_1_proj (Matrix.col U i) * + rank_1_proj (Matrix.col U j) = 0\<^sub>m n n" + by (metis \i < n\ \rank_1_proj (Matrix.col U j) \ fc\ + fc_mats_carrier mult_smult_assoc_mat rf smult_zero_mat) + qed + qed + also have "... = diag_mat B ! j \\<^sub>m rank_1_proj (Matrix.col U j)" + proof - + have "diag_mat B ! j \\<^sub>m rank_1_proj (Matrix.col U j) * + rank_1_proj (Matrix.col U j) = + diag_mat B ! j \\<^sub>m (rank_1_proj (Matrix.col U j) * + rank_1_proj (Matrix.col U j))" + proof (rule mult_smult_assoc_mat) + show "rank_1_proj (Matrix.col U j) \ carrier_mat n n" using \j < n\ rf + fc_mats_carrier by simp + show "rank_1_proj (Matrix.col U j) \ carrier_mat n n" + using assms rf fc_mats_carrier by simp + qed + moreover have "rank_1_proj (Matrix.col U j) * rank_1_proj (Matrix.col U j)= + rank_1_proj (Matrix.col U j)" + proof (rule rank_1_proj_unitary_eq, (auto simp add: assms)) + show "U \ fc" using assms unitary_diag_carrier(2) + using fc_mats_carrier by simp + show "Complex_Matrix.unitary U" using assms unitary_diagD by blast + qed + ultimately show ?thesis by simp + qed + finally have "A * (rank_1_proj (Matrix.col U j)) = + diag_mat B ! j \\<^sub>m rank_1_proj (Matrix.col U j)" . + hence "Complex_Matrix.trace (A * (rank_1_proj (Matrix.col U j))) = + diag_mat B ! j * Complex_Matrix.trace (rank_1_proj (Matrix.col U j))" + using \j < n\ rf fc_mats_carrier trace_smult dim_eq by auto + also have "... = diag_mat B ! j" + proof - + have "Complex_Matrix.trace (rank_1_proj (Matrix.col U j)) = 1" + proof (rule rank_1_proj_trace) + show "\Matrix.col U j\ = 1" using unitary_col_norm[of U n j] assms + unitary_diag_carrier(2) fc_mats_carrier + by (metis unitary_diagD(3)) + qed + thus ?thesis by simp + qed + also have "... = B $$ (j,j)" + proof - + have "dim_row B = n" using unitary_diag_carrier(1) assms fc_mats_carrier + by (metis carrier_matD(1)) + thus ?thesis using assms unfolding diag_mat_def by simp + qed + finally show ?thesis . +qed + +lemma positive_unitary_diag_pos: + fixes A::"complex Matrix.mat" + assumes "A \ carrier_mat n n" + and "Complex_Matrix.positive A" + and "unitary_diag A B U" +and "j < n" +shows "0 \ B $$ (j, j)" +proof - + define fc::"complex Matrix.mat set" where "fc = carrier_mat n n" + interpret cpx_sq_mat n n fc + proof + show "0 < n" using assms by simp + qed (auto simp add: fc_def) + define Uj where "Uj = Matrix.col U j" + have "dim_row U = n" using assms unitary_diag_carrier(2) by blast + hence uj: "Matrix.col U j \ carrier_vec n" by (simp add: carrier_vecI) + have "hermitian A" using assms positive_is_hermitian by simp + have "0 \ Complex_Matrix.inner_prod Uj (A *\<^sub>v Uj)" using assms Complex_Matrix.positive_def + by (metis Uj_def \dim_row U = n\ carrier_matD(2) dim_col) + also have "... = Complex_Matrix.trace (A * (rank_1_proj Uj))" using rank_1_proj_trace_inner uj + assms unfolding Uj_def by metis + also have "... = B $$ (j,j)" using decomp_eigenvector assms + \hermitian A\ unfolding Uj_def fc_def by simp + finally show ?thesis . +qed + +lemma unitary_diag_trace_mult_sum: + fixes A::"complex Matrix.mat" + assumes "A \ carrier_mat n n" + and "C \ carrier_mat n n" + and "hermitian A" + and "unitary_diag A B U" + and "0 < n" +shows "Complex_Matrix.trace (C * A) = + (\ i = 0 ..< n. B$$(i,i) * + Complex_Matrix.trace (C * rank_1_proj (Matrix.col U i)))" +proof - + define fc::"complex Matrix.mat set" where "fc = carrier_mat n n" + interpret cpx_sq_mat n n fc + proof + show "0 < n" using assms by simp + qed (auto simp add: fc_def) + have rf: "\i. i < n \ rank_1_proj (Matrix.col U i) \ carrier_mat n n" + using assms unitary_diag_imp_unitarily_equiv + unitarily_equiv_rank_1_proj_col_carrier + unfolding fc_def by blast + have "C * A = + C * (sum_mat (\i. (diag_mat B ! i) \\<^sub>m + rank_1_proj (Matrix.col U i)) {..< n})" + using sum_decomp_cols assms \hermitian A\ + unfolding fc_def by simp + also have "... = sum_mat (\i. C * ((diag_mat B ! i) \\<^sub>m + rank_1_proj (Matrix.col U i))) {..< n}" + by (rule sum_mat_distrib_left[symmetric], + (auto simp add: assms rf smult_mem fc_def)) + also have "... = sum_mat (\i. (diag_mat B ! i) \\<^sub>m + (C * rank_1_proj (Matrix.col U i))) {..< n}" + proof (rule sum_mat_cong, + (auto simp add: rf smult_mem assms unitarily_equiv_rank_1_proj_col_carrier + fc_def)) + show "\i. i < n \ diag_mat B ! i \\<^sub>m (C * rank_1_proj (Matrix.col U i)) \ + carrier_mat n n" + using assms unitarily_equiv_rank_1_proj_col_carrier cpx_sq_mat_mult smult_mem + by (simp add: rf) + show "\i. i < n \ C * (diag_mat B ! i \\<^sub>m rank_1_proj (Matrix.col U i)) \ + carrier_mat n n" + using assms unitarily_equiv_rank_1_proj_col_carrier cpx_sq_mat_mult + smult_mem by (simp add: rf) + show "\i. i < n \ C * (diag_mat B ! i \\<^sub>m rank_1_proj (Matrix.col U i)) = + diag_mat B ! i \\<^sub>m (C * rank_1_proj (Matrix.col U i))" + by (metis assms(2) fc_mats_carrier mult_smult_distrib rf) + qed + finally have ceq: "C * A = sum_mat (\i. (diag_mat B ! i) \\<^sub>m + (C * rank_1_proj (Matrix.col U i))) {..< n}" . + have "Complex_Matrix.trace (sum_mat (\i. (diag_mat B ! i) \\<^sub>m + (C * rank_1_proj (Matrix.col U i))) {..< n}) = (\ i = 0 ..< n. + Complex_Matrix.trace ((diag_mat B ! i) \\<^sub>m + (C * rank_1_proj (Matrix.col U i))))" + by (smt (z3) assms(2) atLeast0LessThan cpx_sq_mat_mult cpx_sq_mat_smult finite_lessThan + lessThan_iff rf sum.cong trace_sum_mat fc_def) + also have "... = (\ i = 0 ..< n. (diag_mat B ! i) * + Complex_Matrix.trace (C * rank_1_proj (Matrix.col U i)))" + proof (rule sum.cong, simp) + show "\x. x \ {0.. + Complex_Matrix.trace (diag_mat B ! x \\<^sub>m (C * rank_1_proj (Matrix.col U x))) = + diag_mat B ! x * Complex_Matrix.trace (C * rank_1_proj (Matrix.col U x))" using trace_smult + by (metis assms(2) atLeastLessThan_iff cpx_sq_mat_mult fc_mats_carrier rf) + qed + also have "... = (\ i = 0 ..< n. B $$ (i,i) * + Complex_Matrix.trace (C * rank_1_proj (Matrix.col U i)))" + proof (rule sum.cong, simp) + have "B \ carrier_mat n n" using unitary_diag_carrier(1) assms + fc_mats_carrier dim_eq by simp + hence "\x. x \ {0.. diag_mat B!x = B$$(x,x)" unfolding diag_mat_def by simp + thus "\x. x \ {0.. + diag_mat B ! x * Complex_Matrix.trace (C * rank_1_proj (Matrix.col U x)) = + B $$ (x, x) * Complex_Matrix.trace (C * rank_1_proj (Matrix.col U x))" by simp + qed + finally have "Complex_Matrix.trace + (sum_mat (\i. (diag_mat B ! i) \\<^sub>m (C * rank_1_proj (Matrix.col U i))) {..< n}) = + (\ i = 0 ..< n. B $$ (i,i) * Complex_Matrix.trace (C * rank_1_proj (Matrix.col U i)))" . + thus ?thesis using ceq by simp +qed + +lemma unitarily_equiv_trace: + assumes "A \ carrier_mat n n" + and "unitarily_equiv A B U" +shows "Complex_Matrix.trace A = Complex_Matrix.trace B" +proof - + have "Complex_Matrix.trace A = Complex_Matrix.trace (U * B * (Complex_Matrix.adjoint U))" + using assms unitarily_equiv_eq[of A] unitary_diag_imp_unitarily_equiv[of A] by simp + also have "... = Complex_Matrix.trace (Complex_Matrix.adjoint U * (U * B))" + using trace_comm assms + by (metis adjoint_dim' carrier_matD(2) carrier_matI index_mult_mat(2) + index_mult_mat(3) unitarily_equiv_carrier(1) unitarily_equiv_carrier(2)) + also have "... = Complex_Matrix.trace B" using assms + by (smt (z3) Complex_Matrix.unitary_def adjoint_dim_col assoc_mult_mat + carrier_matD(2) carrier_mat_triv index_mult_mat(3) left_mult_one_mat + unitarily_equivD(1) unitarily_equiv_carrier(1) unitarily_equiv_eq + unitary_simps(1)) + finally show ?thesis . +qed + +lemma unitarily_equiv_trace': + assumes "A \ carrier_mat n n" + and "unitarily_equiv A B U" +shows "Complex_Matrix.trace A = (\ i = 0 ..< dim_row A. B $$ (i,i))" +proof - + have "Complex_Matrix.trace A = Complex_Matrix.trace B" using assms unitarily_equiv_trace[of A] + by (meson unitary_diag_imp_unitarily_equiv) + also have "... = (\ i = 0 ..< dim_row A. B $$ (i,i))" using assms + by (metis Complex_Matrix.trace_def carrier_matD(1) unitarily_equiv_carrier(1)) + finally show ?thesis . +qed + +lemma positive_decomp_cmod_le: + fixes A::"complex Matrix.mat" + assumes "A\ carrier_mat n n" + and "C\ carrier_mat n n" + and "0 < n" +and "Complex_Matrix.positive A" +and "unitary_diag A B U" +and "\i. i < n \ cmod (Complex_Matrix.trace (C * rank_1_proj (Matrix.col U i))) \ M" +shows "cmod (Complex_Matrix.trace (C * A)) \ Re (Complex_Matrix.trace A) * M" +proof - + have "dim_row B = n" using assms unitary_diag_carrier(1) + by (metis carrier_matD(1)) + have "hermitian A" using assms positive_is_hermitian by simp + hence "cmod (Complex_Matrix.trace (C * A)) = + cmod (\ i = 0 ..< n. B$$(i,i) * Complex_Matrix.trace (C * rank_1_proj (Matrix.col U i)))" + using assms unitary_diag_trace_mult_sum by simp + also have "... \ (\ i = 0 ..< n. + cmod (B$$(i,i) * Complex_Matrix.trace (C * rank_1_proj (Matrix.col U i))))" + by (simp add: sum_norm_le) + also have "... = (\ i = 0 ..< n. + Re (B$$(i,i)) * cmod (Complex_Matrix.trace (C * rank_1_proj (Matrix.col U i))))" + proof (rule sum.cong, simp) + show "\x. x \ {0.. + cmod (B $$ (x, x) * Complex_Matrix.trace (C * rank_1_proj (Matrix.col U x))) = + Re (B $$ (x, x)) * cmod (Complex_Matrix.trace (C * rank_1_proj (Matrix.col U x)))" + using cmod_mult_pos positive_unitary_diag_pos assms by (metis atLeastLessThan_iff) + qed + also have "... \ (\ i = 0 ..< n. Re (B$$(i,i)) * M)" + proof - + have "\i. i < n \ 0 \ Re (B$$(i,i))" using assms positive_unitary_diag_pos + less_eq_complex_def by simp + thus ?thesis using assms by (meson atLeastLessThan_iff mult_left_mono sum_mono) + qed + also have "... = (\ i = 0 ..< n. Re (B$$(i,i))) * M" by (simp add: sum_distrib_right) + also have "... = Re (\ i = 0 ..< n. B$$(i,i)) * M" by (metis Re_sum) + also have "... = Re (Complex_Matrix.trace B) * M" unfolding Complex_Matrix.trace_def + using \dim_row B = n\ by simp + finally show ?thesis using assms unitarily_equiv_trace[of A] + by (metis unitary_diag_imp_unitarily_equiv) +qed +end \ No newline at end of file diff --git a/thys/Commuting_Hermitian/document/root.tex b/thys/Commuting_Hermitian/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Commuting_Hermitian/document/root.tex @@ -0,0 +1,66 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} +\newcommand{\mnset}[1]{\left\{#1\right\}}\newcommand{\set}[1]{\left\{#1\right\}} +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +%\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage{eurosym} + %for \ + +%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd} + %for \, \, \, \, \ + +%\usepackage{eufrak} + %for \ ... \, \ ... \ (also included in amssymb) + +%\usepackage{textcomp} + %for \, \, \, \, \, + %\ + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +% for uniform font size +%\renewcommand{\isastyle}{\isastyleminor} + + +\begin{document} + +\title{Simultaneous diagonalization of pairwise commuting Hermitian matrices} +\author{Mnacho Echenim} +\maketitle + +\begin{abstract} + A Hermitian matrix is a square complex matrix $A$ that is equal to its conjugate transpose $A^\dagger$. The (finite-dimensional) spectral theorem states that for any such matrix $A$, we have the equality $A = U\cdot B\cdot U^\dagger$, where $U$ is a unitary matrix and $B$ is a diagonal matrix containing only real elements. We formalize the generalization of this result, which states that if $\mnset{A_1, \ldots, A_n}$ are Hermitian and pairwise commuting matrices, then there exists a unitary matrix $U$ such that $A_i = U\cdot B_i \cdot U^\dagger$, for $i = 1,\ldots, n$, and each $B_i$ is diagonal and contains only real elements. Sets of pairwise commuting Hermitian matrices are called \emph{Complete Sets of Commuting Observables} in Quantum Mechanics, where they represent physical quantities that can be simultaneously measured to uniquely distinguish quantum states. +\end{abstract} + +\tableofcontents + +\paragraph{Acknowledgments} This work was partially supported by Agence Nationale de la Recherche, through \emph{Plan France 2030 (ref. ANR-22-PETQ-0007)}. + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +% generated text of all theories +\input{session} + +% optional bibliography +%\bibliographystyle{abbrv} +%\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,694 +1,695 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CSP_RefTK CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon +Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Cubic_Quartic_Equations DFS_Framework DOM_Components DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Dominance_CHK DPRM_Theorem DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Eval_FO Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier FO_Theory_Rewriting Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL Hyperdual IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model IsaNet Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp LP_Duality Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multiset_Ordering_NPC Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker Package_logic PAL PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quasi_Borel_Spaces Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Saturation_Framework_Extensions Schutz_Spacetime Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sophomores_Dream Solidity Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith VYDRA_MDL WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL