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\