diff --git a/thys/Projective_Measurements/CHSH_Inequality.thy b/thys/Projective_Measurements/CHSH_Inequality.thy new file mode 100644 --- /dev/null +++ b/thys/Projective_Measurements/CHSH_Inequality.thy @@ -0,0 +1,1457 @@ +(* +Author: + Mnacho Echenim, Université Grenoble Alpes +*) + +theory CHSH_Inequality imports + Projective_Measurements + + +begin + + +section \The CHSH inequality\ + +text \The local hidden variable assumption for quantum mechanics was developed to make the case +that quantum theory was incomplete. In this part we formalize the CHSH inequality, which provides +an upper-bound of a quantity involving expectations in a probability space, and exploit this +inequality to show that the local hidden variable assumption does not hold.\ + +subsection \Inequality statement\ + +lemma chsh_real: + fixes A0::real + assumes "\A0 * B1\ \ 1" + and "\A0 * B0\ \ 1" + and "\A1 * B0\ \ 1" + and "\A1 * B1\ \ 1" + shows "\A0 * B1 - A0 * B0 + A1 * B0 + A1*B1\ \ 2" +proof - + have "A0 * B1 - A0 * B0 = A0 * B1 - A0 * B0 + A0 * B1 * A1 * B0 - A0 * B1 * A1 * B0" by simp + also have "... = A0 * B1 * (1 + A1*B0) - A0 * B0 * (1 + A1* B1)" + by (metis (no_types, hide_lams) add_diff_cancel_right calculation diff_add_eq + group_cancel.sub1 mult.commute mult.right_neutral + vector_space_over_itself.scale_left_commute + vector_space_over_itself.scale_right_diff_distrib + vector_space_over_itself.scale_right_distrib + vector_space_over_itself.scale_scale) + finally have "A0 * B1 - A0 * B0 = A0 * B1 * (1 + A1*B0) - A0 * B0 * (1 + A1* B1)" . + hence "\A0 * B1 - A0 * B0\ \ \A0 * B1 * (1 + A1*B0)\ + \A0 * B0 * (1 + A1* B1)\" by simp + also have "... = \A0 * B1\ * \(1 + A1*B0)\ + \A0 * B0\ * \(1 + A1* B1)\" by (simp add: abs_mult) + also have "... \ \(1 + A1*B0)\ + \(1 + A1* B1)\" + proof- + have "\A0 * B1\ * \(1 + A1*B0)\ \ \(1 + A1*B0)\" + using assms(1) mult_left_le_one_le[of "\(1 + A1*B0)\"] by simp + moreover have "\A0 * B0\ *\(1 + A1* B1)\ \ \(1 + A1* B1)\" + using assms mult_left_le_one_le[of "\(1 + A1*B1)\"] by simp + ultimately show ?thesis by simp + qed + also have "... = 1 + A1*B0 + 1 + A1* B1" using assms by (simp add: abs_le_iff) + also have "... = 2 + A1 * B0 + A1 * B1" by simp + finally have pls: "\A0 * B1 - A0 * B0\ \ 2 + A1 * B0 + A1 * B1" . + have "A0 * B1 - A0 * B0 = A0 * B1 - A0 * B0 + A0 * B1 * A1 * B0 - A0 * B1 * A1 * B0" by simp + also have "... = A0 * B1 * (1 - A1*B0) - A0 * B0 * (1 - A1* B1)" + proof - + have "A0 * (B1 - (B0 - A1 * (B1 * B0)) - A1 * (B1 * B0)) = A0 * (B1 - B0)" + by fastforce + then show ?thesis + by (metis (no_types) add.commute calculation diff_diff_add mult.right_neutral + vector_space_over_itself.scale_left_commute + vector_space_over_itself.scale_right_diff_distrib vector_space_over_itself.scale_scale) + qed + finally have "A0 * B1 - A0 * B0 = A0 * B1 * (1 - A1*B0) - A0 * B0 * (1 - A1* B1)" . + hence "\A0 * B1 - A0 * B0\ \ \A0 * B1 * (1 - A1*B0)\ + \A0 * B0 * (1 - A1* B1)\" by simp + also have "... = \A0 * B1\ * \(1 - A1*B0)\ + \A0 * B0\ * \(1 - A1* B1)\" by (simp add: abs_mult) + also have "... \ \(1 - A1*B0)\ + \(1 - A1* B1)\" + proof- + have "\A0 * B1\ * \(1 - A1*B0)\ \ \(1 - A1*B0)\" + using assms(1) mult_left_le_one_le[of "\(1 - A1*B0)\"] by simp + moreover have "\A0 * B0\ *\(1 - A1* B1)\ \ \(1 - A1* B1)\" + using assms mult_left_le_one_le[of "\(1 - A1*B1)\"] by simp + ultimately show ?thesis by simp + qed + also have "... = 1 - A1*B0 + 1 - A1* B1" using assms by (simp add: abs_le_iff) + also have "... = 2 - A1 * B0 - A1 * B1" by simp + finally have mns: "\A0 * B1 - A0 * B0\ \ 2 - (A1 * B0 + A1 * B1)" by simp + have ls: "\A0 * B1 - A0 * B0\ \ 2 - \A1 * B0 + A1 * B1\" + proof (cases "0 \ A1 * B0 + A1 * B1") + case True + then show ?thesis using mns by simp + next + case False + then show ?thesis using pls by simp + qed + have "\A0 * B1 - A0 * B0 + A1 * B0 + A1 * B1\ \ \A0 * B1 - A0 * B0\ + \A1 * B0 + A1 * B1\" + by simp + also have "... \ 2" using ls by simp + finally show ?thesis . +qed + +lemma (in prob_space) chsh_expect: + fixes A0::"'a \ real" + assumes "AE w in M. \A0 w\ \ 1" + and "AE w in M. \A1 w\ \ 1" + and "AE w in M. \B0 w\ \ 1" + and "AE w in M. \B1 w\ \ 1" +and "integrable M (\w. A0 w * B1 w)" +and "integrable M (\w. A1 w * B1 w)" +and "integrable M (\w. A1 w * B0 w)" +and "integrable M (\w. A0 w * B0 w)" +shows "\expectation (\w. A1 w * B0 w) + expectation (\w. A0 w *B1 w) + + expectation (\w. A1 w * B1 w) - expectation (\w. A0 w * B0 w)\ \ 2" +proof - + have exeq: "expectation (\w. A1 w * B0 w) + expectation (\w. A0 w * B1 w) + + expectation (\w. A1 w * B1 w) - expectation (\w. A0 w * B0 w) = + expectation (\w. A0 w * B1 w - A0 w * B0 w + A1 w * B0 w + A1 w * B1 w)" + using assms by auto + have "\expectation (\w. A0 w * B1 w - A0 w * B0 w + A1 w * B0 w + A1 w * B1 w)\ \ + expectation (\w. \A0 w * B1 w - A0 w * B0 w + A1 w * B0 w + A1 w * B1 w\)" + using integral_abs_bound by blast + also have "... \ 2" + proof (rule integral_le_const) + show "AE w in M. \A0 w * B1 w - A0 w * B0 w + A1 w * B0 w + A1 w * B1 w\ \ (2::real)" + proof (rule AE_mp) + show "AE w in M. \A0 w\ \ 1 \ \A1 w\ \ 1 \ \B0 w\ \ 1 \ \B1 w\ \ 1" + using assms by simp + show "AE w in M. \A0 w\ \ 1 \ \A1 w\ \ 1 \ \B0 w\ \ 1 \ \B1 w\ \ 1 \ + \A0 w * B1 w - A0 w * B0 w + A1 w * B0 w + A1 w * B1 w\ \ 2" + proof + fix w + assume "w\ space M" + show "\A0 w\ \ 1 \ \A1 w\ \ 1 \ \B0 w\ \ 1 \ \B1 w\ \ 1 \ + \A0 w * B1 w - A0 w * B0 w + A1 w * B0 w + A1 w * B1 w\ \ 2" + proof + assume ineq: "\A0 w\ \ 1 \ \A1 w\ \ 1 \ \B0 w\ \ 1 \ \B1 w\ \ 1" + show "\A0 w * B1 w - A0 w * B0 w + A1 w * B0 w + A1 w * B1 w\ \ 2" + proof (rule chsh_real) + show "\A0 w * B1 w\ \ 1" using ineq by (simp add: abs_mult mult_le_one) + show "\A0 w * B0 w\ \ 1" using ineq by (simp add: abs_mult mult_le_one) + show "\A1 w * B1 w\ \ 1" using ineq by (simp add: abs_mult mult_le_one) + show "\A1 w * B0 w\ \ 1" using ineq by (simp add: abs_mult mult_le_one) + qed + qed + qed + qed + show "integrable M (\x. \A0 x * B1 x - A0 x * B0 x + A1 x * B0 x + A1 x * B1 x\)" + proof (rule Bochner_Integration.integrable_abs) + show "integrable M (\x. A0 x * B1 x - A0 x * B0 x + A1 x * B0 x + A1 x * B1 x)" + using assms by auto + qed + qed + finally show ?thesis using exeq by simp +qed + +text \The local hidden variable assumption states that separated quantum measurements are +independent. It is standard for this assumption to be stated in a context where the hidden +variable admits a density; it is stated here in a more general contest involving expectations, +with no assumption on the existence of a density.\ + +definition pos_rv:: "'a measure \ ('a \ real) \ bool" where +"pos_rv M Xr \ Xr \ borel_measurable M \ (AE w in M. (0::real) \ Xr w)" + +definition prv_sum:: "'a measure \ complex Matrix.mat \ (complex \ 'a \ real) \ bool" where +"prv_sum M A Xr \ (AE w in M. (\ a\ spectrum A. Xr a w) = 1)" + +definition (in cpx_sq_mat) lhv where +"lhv M A B R XA XB \ + prob_space M \ + (\a \spectrum A. pos_rv M (XA a)) \ + (prv_sum M A XA) \ + (\b \spectrum B. pos_rv M (XB b)) \ + (prv_sum M B XB) \ + (\a \spectrum A . \b \ spectrum B. + (integrable M (\w. XA a w * XB b w)) \ + integral\<^sup>L M (\w. XA a w * XB b w) = + Re (Complex_Matrix.trace(eigen_projector A a * (eigen_projector B b) * R)))" + +(*definition (in cpx_sq_mat) lhv where +"lhv M A B R XA XB \ + prob_space M \ + (\a \spectrum A. (XA a \ borel_measurable M) \ + (AE w in M. ((0::real) \ XA a w))) \ + (AE w in M. (\ a\ spectrum A. XA a w) = 1) \ + (\b \spectrum B. (XB b \ borel_measurable M) \ + (AE w in M. (0 \ XB b w))) \ + (AE w in M. (\ b\ spectrum B. XB b w) = 1) \ + (\a \spectrum A . \b \ spectrum B. + (integrable M (\w. XA a w * XB b w)) \ + integral\<^sup>L M (\w. XA a w * XB b w) = + Re (Complex_Matrix.trace(eigen_projector A a * (eigen_projector B b) * R)))"*) + +lemma (in cpx_sq_mat) lhv_posl: + assumes "lhv M A B R XA XB" + shows "AE w in M. (\ a \ spectrum A. 0 \ XA a w)" +proof (rule AE_ball_countable[THEN iffD2]) + show "countable (spectrum A)" using spectrum_finite[of A] + by (simp add: countable_finite) + show "\a\spectrum A. AE w in M. 0 \ XA a w" using assms unfolding lhv_def pos_rv_def by simp +qed + +lemma (in cpx_sq_mat) lhv_lt1_l: + assumes "lhv M A B R XA XB" + shows "AE w in M. (\ a \ spectrum A. XA a w \ 1)" +proof (rule AE_mp) + show "AE w in M. (\ a \ spectrum A. 0 \ XA a w) \ (\ a\ spectrum A. XA a w) = 1" + using lhv_posl assms unfolding lhv_def pos_rv_def prv_sum_def by simp + show "AE w in M. (\a\spectrum A. 0 \ XA a w) \ (\a\spectrum A. XA a w) = 1 \ + (\a\spectrum A. XA a w \ 1)" + proof + fix w + assume "w\ space M" + show "(\a\spectrum A. 0 \ XA a w) \ (\a\spectrum A. XA a w) = 1 \ + (\a\spectrum A. XA a w \ 1)" + proof (rule impI) + assume pr: "(\a\spectrum A. 0 \ XA a w) \ (\a\spectrum A. XA a w) = 1" + show "\a\spectrum A. XA a w \ 1" + proof + fix a + assume "a\ spectrum A" + show "XA a w \ 1" + proof (rule pos_sum_1_le[of "spectrum A"]) + show "finite (spectrum A)" using spectrum_finite[of A] by simp + show "a \ spectrum A" using \a \ spectrum A\ . + show " \i\spectrum A. 0 \ XA i w" using pr by simp + show "(\i\spectrum A. XA i w) = 1" using pr by simp + qed + qed + qed + qed +qed + +lemma (in cpx_sq_mat) lhv_posr: + assumes "lhv M A B R XA XB" + shows "AE w in M. (\ b \ spectrum B. 0 \ XB b w)" +proof (rule AE_ball_countable[THEN iffD2]) + show "countable (spectrum B)" using spectrum_finite[of B] + by (simp add: countable_finite) + show "\b\spectrum B. AE w in M. 0 \ XB b w" using assms unfolding lhv_def pos_rv_def by simp +qed + +lemma (in cpx_sq_mat) lhv_lt1_r: + assumes "lhv M A B R XA XB" + shows "AE w in M. (\ a \ spectrum B. XB a w \ 1)" +proof (rule AE_mp) + show "AE w in M. (\ a \ spectrum B. 0 \ XB a w) \ (\ a\ spectrum B. XB a w) = 1" + using lhv_posr assms unfolding lhv_def prv_sum_def pos_rv_def by simp + show "AE w in M. (\a\spectrum B. 0 \ XB a w) \ (\a\spectrum B. XB a w) = 1 \ + (\a\spectrum B. XB a w \ 1)" + proof + fix w + assume "w\ space M" + show "(\a\spectrum B. 0 \ XB a w) \ (\a\spectrum B. XB a w) = 1 \ + (\a\spectrum B. XB a w \ 1)" + proof (rule impI) + assume pr: "(\a\spectrum B. 0 \ XB a w) \ (\a\spectrum B. XB a w) = 1" + show "\a\spectrum B. XB a w \ 1" + proof + fix a + assume "a\ spectrum B" + show "XB a w \ 1" + proof (rule pos_sum_1_le[of "spectrum B"]) + show "finite (spectrum B)" using spectrum_finite[of B] by simp + show "a \ spectrum B" using \a \ spectrum B\ . + show " \i\spectrum B. 0 \ XB i w" using pr by simp + show "(\i\spectrum B. XB i w) = 1" using pr by simp + qed + qed + qed + qed +qed + +lemma (in cpx_sq_mat) lhv_AE_propl: + assumes "lhv M A B R XA XB" + shows "AE w in M. (\ a \ spectrum A. 0 \ XA a w \ XA a w \ 1) \ (\ a\ spectrum A. XA a w) = 1" +proof (rule AE_conjI) + show "AE w in M. \a\spectrum A. 0 \ XA a w \ XA a w \ 1" + proof (rule AE_mp) + show "AE w in M. (\ a \ spectrum A. 0 \ XA a w) \ (\ a \ spectrum A. XA a w \ 1)" + using assms lhv_posl[of M A] lhv_lt1_l[of M A] by simp + show "AE w in M. (\a\spectrum A. 0 \ XA a w) \ (\a\spectrum A. XA a w \ 1) \ + (\a\spectrum A. 0 \ XA a w \ XA a w \ 1)" by auto + qed + show "AE w in M. (\a\spectrum A. XA a w) = 1" using assms unfolding lhv_def prv_sum_def + by simp +qed + +lemma (in cpx_sq_mat) lhv_AE_propr: + assumes "lhv M A B R XA XB" + shows "AE w in M. (\ a \ spectrum B. 0 \ XB a w \ XB a w \ 1) \ (\ a\ spectrum B. XB a w) = 1" +proof (rule AE_conjI) + show "AE w in M. \a\spectrum B. 0 \ XB a w \ XB a w \ 1" + proof (rule AE_mp) + show "AE w in M. (\ a \ spectrum B. 0 \ XB a w) \ (\ a \ spectrum B. XB a w \ 1)" + using assms lhv_posr[of M _ B] lhv_lt1_r[of M _ B] by simp + show "AE w in M. (\a\spectrum B. 0 \ XB a w) \ (\a\spectrum B. XB a w \ 1) \ + (\a\spectrum B. 0 \ XB a w \ XB a w \ 1)" by auto + qed + show "AE w in M. (\a\spectrum B. XB a w) = 1" using assms unfolding lhv_def prv_sum_def + by simp +qed + +lemma (in cpx_sq_mat) lhv_integral_eq: + fixes c::real + assumes "lhv M A B R XA XB" + and "a\ spectrum A" +and "b\ spectrum B" +shows "integral\<^sup>L M (\w. XA a w * XB b w) = + Re (Complex_Matrix.trace(eigen_projector A a * (eigen_projector B b) * R))" + using assms unfolding lhv_def by simp + +lemma (in cpx_sq_mat) lhv_integrable: + fixes c::real + assumes "lhv M A B R XA XB" + and "a\ spectrum A" +and "b\ spectrum B" +shows "integrable M (\w. XA a w * XB b w)" using assms unfolding lhv_def by simp + +lemma (in cpx_sq_mat) lhv_scal_integrable: + fixes c::real + assumes "lhv M A B R XA XB" + and "a\ spectrum A" +and "b\ spectrum B" +shows "integrable M (\w. c *XA a w * d * XB b w)" +proof - + { + fix x + assume "x\ space M" + have "c * d * (XA a x * XB b x) = c * XA a x * d * XB b x" by simp + } note eq = this + have "integrable M (\w. XA a w * XB b w)" using assms unfolding lhv_def by simp + hence g:"integrable M (\w. c * d * (XA a w * XB b w))" using integrable_real_mult_right by simp + show ?thesis + proof (rule Bochner_Integration.integrable_cong[THEN iffD2], simp) + show "integrable M (\w. c * d * (XA a w * XB b w))" using g . + show "\x. x \ space M \ c * XA a x * d * XB b x = c * d * (XA a x * XB b x)" using eq by simp + qed +qed + +lemma (in cpx_sq_mat) lhv_lsum_scal_integrable: + assumes "lhv M A B R XA XB" + and "a\ spectrum A" +shows "integrable M (\x. \b\spectrum B. c * XA a x * (f b) * XB b x)" +proof (rule Bochner_Integration.integrable_sum) + fix b + assume "b\ spectrum B" + thus "integrable M (\x. c * XA a x * f b *XB b x)" using \a\ spectrum A\ assms + lhv_scal_integrable[of M] by simp +qed + +lemma (in cpx_sq_mat) lhv_sum_integrable: + assumes "lhv M A B R XA XB" +shows "integrable M (\w. (\ a \ spectrum A. (\ b \ spectrum B. f a * XA a w * g b * XB b w)))" +proof (rule Bochner_Integration.integrable_sum) + fix a + assume "a\ spectrum A" + thus "integrable M (\x. \b\spectrum B. f a * XA a x * g b * XB b x)" + using assms lhv_lsum_scal_integrable[of M] + by simp +qed + +lemma (in cpx_sq_mat) spectrum_abs_1_weighted_suml: + assumes "lhv M A B R Va Vb" +and "{Re x |x. x \ spectrum A} \ {}" + and "{Re x |x. x \ spectrum A} \ {- 1, 1}" +and "hermitian A" + and "A\ fc_mats" +shows "AE w in M. \(\a\spectrum A. Re a * Va a w)\ \ 1" +proof (rule AE_mp) + show "AE w in M. (\a\spectrum A. 0 \ Va a w \ Va a w \ 1) \ (\a\spectrum A. Va a w) = 1" + using assms lhv_AE_propl[of M A B _ Va] by simp + show "AE w in M. (\a\spectrum A. 0 \ Va a w \ Va a w \ 1) \ (\a\spectrum A. Va a w) = 1 \ + \\a\spectrum A. Re a * Va a w\ \ 1" + proof + fix w + assume "w\ space M" + show "(\a\spectrum A. 0 \ Va a w \ Va a w \ 1) \ (\a\spectrum A. Va a w) = 1 \ + \\a\spectrum A. Re a * Va a w\ \ 1" + proof (intro impI) + assume pr: "(\a\spectrum A. 0 \ Va a w \ Va a w \ 1) \ (\a\spectrum A. Va a w) = 1" + show "\(\a\spectrum A. Re a * Va a w)\ \ 1" + proof (cases "{Re x |x. x \ spectrum A} = {- 1, 1}") + case True + hence sp: "spectrum A = {-1, 1}" using hermitian_Re_spectrum[of A] assms by simp + hence scsum: "(\a\spectrum A. Re a * Va a w) = Va 1 w - Va (-1) w" + using sum_2_elems by simp + have sum: "(\a\spectrum A. Va a w) = Va (-1) w + Va 1 w" + using sp sum_2_elems by simp + have "\Va 1 w - Va (-1) w\ \ 1" + proof (rule fct_bound') + have "1 \ spectrum A" using sp by simp + thus "0 \ Va 1 w" using pr by simp + have "-1 \ spectrum A" using sp by simp + thus "0 \ Va (- 1) w" using pr by simp + show "Va (- 1) w + Va 1 w = 1" using pr sum by simp + qed + thus ?thesis using scsum by simp + next + case False + then show ?thesis + proof (cases "{Re x |x. x \ spectrum A} = {- 1}") + case True + hence "spectrum A = {-1}" using hermitian_Re_spectrum[of A] assms by simp + hence "(\a\spectrum A. Re a * Va a w) = - Va (-1) w" by simp + moreover have "-1 \ spectrum A" using \spectrum A = {-1}\ by simp + ultimately show ?thesis using pr by simp + next + case False + hence "{Re x |x. x \ spectrum A} = {1}" using assms \{Re x |x. x \ spectrum A} \ {-1, 1}\ + last_subset[of "{Re x |x. x \ spectrum A}"] by simp + hence "spectrum A = {1}" using hermitian_Re_spectrum[of A] assms by simp + hence "(\a\spectrum A. Re a * Va a w) = Va 1 w" by simp + moreover have "1 \ spectrum A" using \spectrum A = {1}\ by simp + ultimately show ?thesis using pr by simp + qed + qed + qed + qed +qed + +lemma (in cpx_sq_mat) spectrum_abs_1_weighted_sumr: + assumes "lhv M B A R Vb Va" +and "{Re x |x. x \ spectrum A} \ {}" + and "{Re x |x. x \ spectrum A} \ {- 1, 1}" +and "hermitian A" + and "A\ fc_mats" +shows "AE w in M. \(\a\spectrum A. Re a * Va a w)\ \ 1" +proof (rule AE_mp) + show "AE w in M. (\a\spectrum A. 0 \ Va a w \ Va a w \ 1) \ (\a\spectrum A. Va a w) = 1" + using assms lhv_AE_propr[of M B A _ Vb] by simp + show "AE w in M. (\a\spectrum A. 0 \ Va a w \ Va a w \ 1) \ (\a\spectrum A. Va a w) = 1 \ + \\a\spectrum A. Re a * Va a w\ \ 1" + proof + fix w + assume "w\ space M" + show "(\a\spectrum A. 0 \ Va a w \ Va a w \ 1) \ (\a\spectrum A. Va a w) = 1 \ + \\a\spectrum A. Re a * Va a w\ \ 1" + proof (intro impI) + assume pr: "(\a\spectrum A. 0 \ Va a w \ Va a w \ 1) \ (\a\spectrum A. Va a w) = 1" + show "\(\a\spectrum A. Re a * Va a w)\ \ 1" + proof (cases "{Re x |x. x \ spectrum A} = {- 1, 1}") + case True + hence sp: "spectrum A = {-1, 1}" using hermitian_Re_spectrum[of A] assms by simp + hence scsum: "(\a\spectrum A. Re a * Va a w) = Va 1 w - Va (-1) w" + using sum_2_elems by simp + have sum: "(\a\spectrum A. Va a w) = Va (-1) w + Va 1 w" + using sp sum_2_elems by simp + have "\Va 1 w - Va (-1) w\ \ 1" + proof (rule fct_bound') + have "1 \ spectrum A" using sp by simp + thus "0 \ Va 1 w" using pr by simp + have "-1 \ spectrum A" using sp by simp + thus "0 \ Va (- 1) w" using pr by simp + show "Va (- 1) w + Va 1 w = 1" using pr sum by simp + qed + thus ?thesis using scsum by simp + next + case False + then show ?thesis + proof (cases "{Re x |x. x \ spectrum A} = {- 1}") + case True + hence "spectrum A = {-1}" using hermitian_Re_spectrum[of A] assms by simp + hence "(\a\spectrum A. Re a * Va a w) = - Va (-1) w" by simp + moreover have "-1 \ spectrum A" using \spectrum A = {-1}\ by simp + ultimately show ?thesis using pr by simp + next + case False + hence "{Re x |x. x \ spectrum A} = {1}" using assms \{Re x |x. x \ spectrum A} \ {-1, 1}\ + last_subset[of "{Re x |x. x \ spectrum A}"] by simp + hence "spectrum A = {1}" using hermitian_Re_spectrum[of A] assms by simp + hence "(\a\spectrum A. Re a * Va a w) = Va 1 w" by simp + moreover have "1 \ spectrum A" using \spectrum A = {1}\ by simp + ultimately show ?thesis using pr by simp + qed + qed + qed + qed +qed + +definition qt_expect where +"qt_expect A Va = (\w. (\a\spectrum A. Re a * Va a w))" + +lemma (in cpx_sq_mat) spectr_sum_integrable: +assumes "lhv M A B R Va Vb" +shows "integrable M (\w. qt_expect A Va w * qt_expect B Vb w)" +proof (rule Bochner_Integration.integrable_cong[THEN iffD2]) + show "M = M" by simp + show "\w. w \ space M \ qt_expect A Va w * qt_expect B Vb w = + (\a\spectrum A. (\b\spectrum B. Re a * Va a w * Re b * Vb b w))" + proof - + fix w + assume "w\ space M" + show "qt_expect A Va w * qt_expect B Vb w = + (\a\spectrum A. (\b\spectrum B. Re a * Va a w * Re b * Vb b w))" unfolding qt_expect_def + by (metis (mono_tags, lifting) Finite_Cartesian_Product.sum_cong_aux sum_product + vector_space_over_itself.scale_scale) + qed + show "integrable M (\w. \a\spectrum A. (\b\spectrum B. Re a * Va a w * Re b * Vb b w))" + using lhv_sum_integrable[of M] assms by simp +qed + +lemma (in cpx_sq_mat) lhv_sum_integral': + assumes "lhv M A B R XA XB" +shows "integral\<^sup>L M (\w. (\ a \ spectrum A. f a * XA a w) * (\ b \ spectrum B. g b * XB b w)) = + (\ a \ spectrum A. f a * (\ b \ spectrum B. g b * integral\<^sup>L M (\w. XA a w * XB b w)))" +proof - + have "integral\<^sup>L M (\w. (\ a \ spectrum A. f a * XA a w) * (\ b \ spectrum B. g b * XB b w)) = + integral\<^sup>L M (\w. (\ a \ spectrum A. (\ b \ spectrum B. f a * XA a w * g b * XB b w)))" + proof (rule Bochner_Integration.integral_cong, simp) + fix w + assume "w\ space M" + show "(\a\spectrum A. f a * XA a w) * (\b\spectrum B. g b * XB b w) = + (\a\spectrum A. (\b\spectrum B. f a * XA a w * (g b) * XB b w))" + by (simp add: sum_product vector_space_over_itself.scale_scale) + qed + also have "... = (\ a \ spectrum A. + integral\<^sup>L M (\w. (\ b \ spectrum B. f a * XA a w * g b * XB b w)))" + proof (rule Bochner_Integration.integral_sum) + fix a + assume "a\ spectrum A" + thus "integrable M (\x. \b\spectrum B. f a * XA a x * g b * XB b x)" + using lhv_lsum_scal_integrable[of M] assms by simp + qed + also have "... = (\ a \ spectrum A. f a * + integral\<^sup>L M (\w. (\ b \ spectrum B. XA a w * g b * XB b w)))" + proof - + have "\ a\ spectrum A. integral\<^sup>L M (\w. (\ b \ spectrum B. f a * XA a w * g b * XB b w)) = + f a * integral\<^sup>L M (\w. (\ b \ spectrum B. XA a w * g b * XB b w))" + proof + fix a + assume "a\ spectrum A" + have "(LINT w|M. (\b\spectrum B. f a * XA a w * g b * XB b w)) = + (LINT w|M. f a* (\b\spectrum B. XA a w * g b * XB b w))" + proof (rule Bochner_Integration.integral_cong, simp) + fix x + assume "x \ space M" + show "(\b\spectrum B. f a * XA a x * g b * XB b x) = + f a * (\b\spectrum B. XA a x * g b * XB b x)" + by (metis (no_types, lifting) Finite_Cartesian_Product.sum_cong_aux + vector_space_over_itself.scale_scale vector_space_over_itself.scale_sum_right) + qed + also have "... = f a * (LINT w|M. (\b\spectrum B. XA a w * g b * XB b w))" by simp + finally show "(LINT w|M. (\b\spectrum B. f a * XA a w * g b * XB b w)) = + f a * (LINT w|M. (\b\spectrum B. XA a w * g b * XB b w))" . + qed + thus ?thesis by simp + qed + also have "... = (\ a \ spectrum A. f a * (\ b \ spectrum B. g b * + integral\<^sup>L M (\w. XA a w * XB b w)))" + proof (rule sum.cong, simp) + fix a + assume "a\ spectrum A" + have "integral\<^sup>L M (\w. (\ b \ spectrum B. XA a w * g b * XB b w)) = (\ b \ spectrum B. + integral\<^sup>L M (\w. XA a w * g b * XB b w))" + proof (rule Bochner_Integration.integral_sum) + show "\b. b \ spectrum B \ integrable M (\x. XA a x * g b * XB b x)" + proof - + fix b + assume "b\ spectrum B" + thus "integrable M (\x. XA a x * g b * XB b x)" + using assms lhv_scal_integrable[of M _ _ _ _ _ a b 1] \a\ spectrum A\ by simp + qed + qed + also have "... = (\ b \ spectrum B. g b * integral\<^sup>L M (\w. XA a w * XB b w))" + proof (rule sum.cong, simp) + fix x + assume "x\ spectrum B" + have "LINT w|M. XA a w * g x * XB x w = LINT w|M. g x * (XA a w * XB x w)" + by (rule Bochner_Integration.integral_cong, auto) + also have "... = g x * (LINT w|M. XA a w * XB x w)" + using Bochner_Integration.integral_mult_right_zero[of M "g x" "\w. XA a w * XB x w"] + by simp + finally show "LINT w|M. XA a w * g x * XB x w = g x * (LINT w|M. XA a w * XB x w)" . + qed + finally have "integral\<^sup>L M (\w. (\ b \ spectrum B. XA a w * g b * XB b w)) = + (\ b \ spectrum B. g b * integral\<^sup>L M (\w. XA a w * XB b w))" . + thus "f a * (LINT w|M. (\b\spectrum B. XA a w * g b * XB b w)) = + f a * (\ b \ spectrum B. g b * integral\<^sup>L M (\w. XA a w * XB b w))" by simp + qed + finally show ?thesis . +qed + +lemma (in cpx_sq_mat) sum_qt_expect_trace: + assumes "lhv M A B R XA XB" + shows "(\ a \ spectrum A. f a * (\ b \ spectrum B. g b * integral\<^sup>L M (\w. XA a w * XB b w))) = + (\ a \ spectrum A. f a * (\ b \ spectrum B. g b * + Re (Complex_Matrix.trace(eigen_projector A a * (eigen_projector B b) * R))))" +proof (rule sum.cong, simp) + fix a + assume "a\ spectrum A" + have "(\b\spectrum B. g b * (LINT w|M. XA a w * XB b w)) = + (\b\spectrum B. g b * + Re (Complex_Matrix.trace (eigen_projector A a * eigen_projector B b * R)))" + proof (rule sum.cong, simp) + fix b + assume "b\ spectrum B" + show "g b * (LINT w|M. XA a w * XB b w) = + g b * Re (Complex_Matrix.trace (eigen_projector A a * eigen_projector B b * R))" + using lhv_integral_eq[of M] assms \a \ spectrum A\ \b \ spectrum B\ by simp + qed + thus "f a * (\b\spectrum B. g b * (LINT w|M. XA a w * XB b w)) = + f a * (\b\spectrum B. g b * + Re (Complex_Matrix.trace (eigen_projector A a * eigen_projector B b * R)))" by simp +qed + +lemma (in cpx_sq_mat) sum_eigen_projector_trace_dist: + assumes "hermitian B" +and "A\ fc_mats" +and "B\ fc_mats" +and "R\ fc_mats" + shows "(\ b \ spectrum B. (b * + Complex_Matrix.trace(A * (eigen_projector B b) * R))) = Complex_Matrix.trace(A * B * R)" +proof - + have "(\b\spectrum B. b * Complex_Matrix.trace (A * eigen_projector B b * R)) = + (\b\spectrum B. Complex_Matrix.trace (A * (b \\<^sub>m (eigen_projector B b)) * R))" + proof (rule sum.cong, simp) + fix b + assume "b\ spectrum B" + have "b * Complex_Matrix.trace (A * eigen_projector B b * R) = + Complex_Matrix.trace (b \\<^sub>m (A * eigen_projector B b * R))" + proof (rule trace_smult[symmetric]) + show "A * eigen_projector B b * R \ carrier_mat dimR dimR" using eigen_projector_carrier + assms fc_mats_carrier dim_eq \b \ spectrum B\ cpx_sq_mat_mult by meson + qed + also have "... = Complex_Matrix.trace (A * (b \\<^sub>m eigen_projector B b) * R)" + proof - + have "b \\<^sub>m (A * eigen_projector B b * R) = b \\<^sub>m (A * (eigen_projector B b * R))" + proof - + have "A * eigen_projector B b * R = A * (eigen_projector B b * R)" + by (metis \b \ spectrum B\ assms(1) assms(2) assms(3) assms(4) assoc_mult_mat dim_eq + fc_mats_carrier eigen_projector_carrier) + thus ?thesis by simp + qed + also have "... = A * (b \\<^sub>m (eigen_projector B b * R))" + proof (rule mult_smult_distrib[symmetric]) + show "A \ carrier_mat dimR dimR" using eigen_projector_carrier assms + fc_mats_carrier dim_eq by simp + show "eigen_projector B b * R \ carrier_mat dimR dimR" using eigen_projector_carrier + \b \ spectrum B\ assms fc_mats_carrier dim_eq cpx_sq_mat_mult by blast + qed + also have "... = A * ((b \\<^sub>m eigen_projector B b) * R)" + proof - + have "b \\<^sub>m (eigen_projector B b * R) = (b \\<^sub>m eigen_projector B b) * R" + proof (rule mult_smult_assoc_mat[symmetric]) + show "eigen_projector B b \ carrier_mat dimR dimR" using eigen_projector_carrier + \b \ spectrum B\ assms fc_mats_carrier dim_eq by simp + show "R \ carrier_mat dimR dimR" using assms fc_mats_carrier dim_eq by simp + qed + thus ?thesis by simp + qed + also have "... = A * (b \\<^sub>m eigen_projector B b) * R" + by (metis \b \ spectrum B\ assms(1) assms(2) assms(3) assms(4) assoc_mult_mat + cpx_sq_mat_smult dim_eq fc_mats_carrier eigen_projector_carrier) + finally have "b \\<^sub>m (A * eigen_projector B b * R) = A * (b \\<^sub>m eigen_projector B b) * R" . + then show ?thesis by simp + qed + finally show "b * Complex_Matrix.trace (A * eigen_projector B b * R) = + Complex_Matrix.trace (A * (b \\<^sub>m eigen_projector B b) * R)" . + qed + also have "... = Complex_Matrix.trace (A * + (sum_mat (\b. b \\<^sub>m eigen_projector B b) (spectrum B)) * R)" + proof (rule trace_sum_mat_mat_distrib, (auto simp add: assms)) + show "finite (spectrum B)" using spectrum_finite[of B] by simp + fix b + assume "b\ spectrum B" + show "b \\<^sub>m eigen_projector B b \ fc_mats" + by (simp add: \b \ spectrum B\ assms(1) assms(3) cpx_sq_mat_smult eigen_projector_carrier) + qed + also have "... = Complex_Matrix.trace (A * B * R)" + proof - + have "sum_mat (\b. b \\<^sub>m eigen_projector B b) (spectrum B) = B" using make_pm_sum' assms by simp + thus ?thesis by simp + qed + finally show ?thesis . +qed + +lemma (in cpx_sq_mat) sum_eigen_projector_trace_right: + assumes "hermitian A" +and "A\ fc_mats" +and "B\ fc_mats" +shows "(\ a \ spectrum A. Complex_Matrix.trace (a \\<^sub>m eigen_projector A a * B)) = + Complex_Matrix.trace (A * B)" +proof - + have "sum_mat (\a. a \\<^sub>m eigen_projector A a * B) (spectrum A) = + sum_mat (\a. a \\<^sub>m eigen_projector A a) (spectrum A) * B" + proof (rule mult_sum_mat_distrib_right) + show "finite (spectrum A)" using spectrum_finite[of A] by simp + show "\a. a \ spectrum A \ a \\<^sub>m eigen_projector A a \ fc_mats" + using assms(1) assms(2) cpx_sq_mat_smult eigen_projector_carrier by blast + show "B\ fc_mats" using assms by simp + qed + also have "... = A * B" using make_pm_sum' assms by simp + finally have seq: "sum_mat (\a. a \\<^sub>m eigen_projector A a * B) (spectrum A) = A * B" . + have "(\ a \ spectrum A. Complex_Matrix.trace (a \\<^sub>m eigen_projector A a * B)) = + Complex_Matrix.trace (sum_mat (\a. a \\<^sub>m eigen_projector A a * B) (spectrum A))" + proof (rule trace_sum_mat[symmetric]) + show "finite (spectrum A)" using spectrum_finite[of A] by simp + show "\a. a \ spectrum A \ a \\<^sub>m eigen_projector A a * B \ fc_mats" + by (simp add: assms(1) assms(2) assms(3) cpx_sq_mat_mult cpx_sq_mat_smult + eigen_projector_carrier) + qed + also have "... = Complex_Matrix.trace (A * B)" using seq by simp + finally show ?thesis . +qed + +lemma (in cpx_sq_mat) sum_eigen_projector_trace: + assumes "hermitian A" + and "hermitian B" + and "A\ fc_mats" + and "B\ fc_mats" +and "R\ fc_mats" + shows "(\ a \ spectrum A. a * (\ b \ spectrum B. (b * + Complex_Matrix.trace(eigen_projector A a * (eigen_projector B b) * R)))) = + Complex_Matrix.trace(A * B * R)" +proof - + have "(\ a \ spectrum A. a * (\ b \ spectrum B. (b * + Complex_Matrix.trace(eigen_projector A a * (eigen_projector B b) * R)))) = (\ a \ spectrum A. + Complex_Matrix.trace (a \\<^sub>m eigen_projector A a * (B * R)))" + proof (rule sum.cong, simp) + fix a + assume "a\ spectrum A" + hence "(\b\spectrum B. b * + Complex_Matrix.trace (eigen_projector A a * eigen_projector B b * R)) = + Complex_Matrix.trace (eigen_projector A a * B * R)" using + sum_eigen_projector_trace_dist[of B "eigen_projector A a" R] assms eigen_projector_carrier + by blast + hence "a * (\ b \ spectrum B. (b * + Complex_Matrix.trace(eigen_projector A a * (eigen_projector B b) * R))) = + a * Complex_Matrix.trace (eigen_projector A a * B * R)" by simp + also have "... = Complex_Matrix.trace (a \\<^sub>m (eigen_projector A a * B * R))" + using trace_smult[symmetric, of "eigen_projector A a * B * R" dimR a] assms + \a \ spectrum A\ cpx_sq_mat_mult dim_eq fc_mats_carrier eigen_projector_carrier by force + also have "... = Complex_Matrix.trace (a \\<^sub>m eigen_projector A a * (B * R))" + proof - + have "a \\<^sub>m (eigen_projector A a * B * R) = a \\<^sub>m (eigen_projector A a * B) * R" + proof (rule mult_smult_assoc_mat[symmetric]) + show "R\ carrier_mat dimR dimR" using assms fc_mats_carrier dim_eq by simp + show "eigen_projector A a * B \ carrier_mat dimR dimR" using assms eigen_projector_carrier + cpx_sq_mat_mult fc_mats_carrier dim_eq \a \ spectrum A\ by blast + qed + also have "... = a \\<^sub>m eigen_projector A a * B * R" + proof - + have "a \\<^sub>m (eigen_projector A a * B) = a \\<^sub>m eigen_projector A a * B" + using mult_smult_assoc_mat[symmetric] + proof - + show ?thesis + by (metis \\nr nc n k B A. \A \ carrier_mat nr n; B \ carrier_mat n nc\ \ + k \\<^sub>m (A * B) = k \\<^sub>m A * B\ \a \ spectrum A\ assms(1) assms(3) assms(4) dim_eq + fc_mats_carrier eigen_projector_carrier) + qed + thus ?thesis by simp + qed + also have "... = a \\<^sub>m eigen_projector A a * (B * R)" + by (metis \a \ spectrum A\ assms(1) assms(3) assms(4) assms(5) assoc_mult_mat + cpx_sq_mat_smult dim_eq fc_mats_carrier eigen_projector_carrier) + finally show ?thesis by simp + qed + finally show "a * (\ b \ spectrum B. (b * + Complex_Matrix.trace(eigen_projector A a * (eigen_projector B b) * R))) = + Complex_Matrix.trace (a \\<^sub>m eigen_projector A a * (B * R))" . + qed + also have "... = Complex_Matrix.trace (A * (B * R))" + using sum_eigen_projector_trace_right[of A "B * R"] assms by (simp add: cpx_sq_mat_mult) + also have "... = Complex_Matrix.trace (A * B * R)" + proof - + have "A * (B * R) = A * B * R" + proof (rule assoc_mult_mat[symmetric]) + show "A\ carrier_mat dimR dimR" using assms fc_mats_carrier dim_eq by simp + show "B\ carrier_mat dimR dimR" using assms fc_mats_carrier dim_eq by simp + show "R\ carrier_mat dimR dimR" using assms fc_mats_carrier dim_eq by simp + qed + thus ?thesis by simp + qed + finally show ?thesis . +qed + +text \We obtain the main result of this part, which relates the quantum expectation value of a +joint measurement with an expectation.\ + +lemma (in cpx_sq_mat) sum_qt_expect: + assumes "lhv M A B R XA XB" + and "A\ fc_mats" + and "B\ fc_mats" + and "R\ fc_mats" + and "hermitian A" + and "hermitian B" + shows "integral\<^sup>L M (\w. (qt_expect A XA w) * (qt_expect B XB w)) = + Re (Complex_Matrix.trace(A * B * R))" +proof - + have br: "\ b \ spectrum B. b\ Reals" using assms hermitian_spectrum_real[of B] by auto + have ar: "\a \ spectrum A. a\ Reals" using hermitian_spectrum_real[of A] assms by auto + have "integral\<^sup>L M (\w. (\ a \ spectrum A. Re a* XA a w) * (\ b \ spectrum B. Re b *XB b w)) = + (\ a \ spectrum A. Re a * (\ b \ spectrum B. Re b * integral\<^sup>L M (\w. XA a w * XB b w)))" + using lhv_sum_integral'[of M] assms by simp + also have "... = (\ a \ spectrum A. Re a * (\ b \ spectrum B. Re b * + Re (Complex_Matrix.trace(eigen_projector A a * (eigen_projector B b) * R))))" + using assms sum_qt_expect_trace[of M] by simp + also have "... = (\ a \ spectrum A. Re a * Re (\ b \ spectrum B. (b * + Complex_Matrix.trace(eigen_projector A a * (eigen_projector B b) * R))))" + proof (rule sum.cong, simp) + fix a + assume "a\ spectrum A" + have "(\b\spectrum B. Re b * + Re (Complex_Matrix.trace (eigen_projector A a * eigen_projector B b * R))) = + (\ b \ spectrum B. Re (b * + Complex_Matrix.trace(eigen_projector A a * (eigen_projector B b) * R)))" + proof (rule sum.cong, simp) + fix b + assume "b\ spectrum B" + hence "b\ Reals" using hermitian_spectrum_real[of B] assms by simp + hence "Re b = b" by simp + thus "Re b * Re (Complex_Matrix.trace (eigen_projector A a * eigen_projector B b * R)) = + Re (b * Complex_Matrix.trace (eigen_projector A a * eigen_projector B b * R))" + using hermitian_spectrum_real using \b \ \\ mult_real_cpx by auto + qed + also have "... = + Re (\ b \ spectrum B. b * + Complex_Matrix.trace(eigen_projector A a * (eigen_projector B b) * R))" by simp + finally have "(\b\spectrum B. Re b * + Re (Complex_Matrix.trace (eigen_projector A a * eigen_projector B b * R))) = + Re (\ b \ spectrum B. b * + Complex_Matrix.trace(eigen_projector A a * (eigen_projector B b) * R))" . + thus "Re a * (\b\spectrum B. Re b * + Re (Complex_Matrix.trace (eigen_projector A a * eigen_projector B b * R))) = + Re a * Re (\b\spectrum B. + (b * Complex_Matrix.trace (eigen_projector A a * eigen_projector B b * R)))" + by simp + qed + also have "... = (\ a \ spectrum A. Re (a * (\ b \ spectrum B. (b * + Complex_Matrix.trace(eigen_projector A a * (eigen_projector B b) * R)))))" + proof (rule sum.cong, simp) + fix x + assume "x\ spectrum A" + hence "Re x = x" using ar by simp + thus "Re x * Re (\b\spectrum B. b * + Complex_Matrix.trace (eigen_projector A x * eigen_projector B b * R)) = + Re (x * (\b\spectrum B. b * + Complex_Matrix.trace (eigen_projector A x * eigen_projector B b * R)))" + using \x \ spectrum A\ ar mult_real_cpx by auto + qed + also have "... = Re (\ a \ spectrum A. a * (\ b \ spectrum B. (b * + Complex_Matrix.trace(eigen_projector A a * (eigen_projector B b) * R))))" by simp + also have "... = Re (Complex_Matrix.trace(A *B * R))" using assms + sum_eigen_projector_trace[of A B] by simp + finally show ?thesis unfolding qt_expect_def . +qed + + +subsection \Properties of specific observables\ + +text \In this part we consider a specific density operator and specific observables corresponding +to joint bipartite measurements. We will compute the quantum expectation value of this system and +prove that it violates the CHSH inequality, thus proving that the local hidden variable assumption +cannot hold.\ + +subsubsection \Ket 0, Ket 1 and the corresponding projectors\ + +definition ket_0::"complex Matrix.vec" where +"ket_0 = unit_vec 2 0" + +lemma ket_0_dim: + shows "dim_vec ket_0 = 2" unfolding ket_0_def by simp + +lemma ket_0_norm: + shows "\ket_0\ = 1" using unit_cpx_vec_length unfolding ket_0_def by simp + +lemma ket_0_mat: + shows "ket_vec ket_0 = Matrix.mat_of_cols_list 2 [[1, 0]]" + by (auto simp add: ket_vec_def Matrix.mat_of_cols_list_def ket_0_def) + +definition ket_1::"complex Matrix.vec" where +"ket_1 = unit_vec 2 1" + +lemma ket_1_dim: + shows "dim_vec ket_1 = 2" unfolding ket_1_def by simp + +lemma ket_1_norm: + shows "\ket_1\ = 1" using unit_cpx_vec_length unfolding ket_1_def by simp + +definition ket_01 + where "ket_01 = tensor_vec ket_0 ket_1" + +lemma ket_01_dim: + shows "dim_vec ket_01 = 4" unfolding ket_01_def + by (simp add: ket_0_dim ket_1_dim) + +definition ket_10 + where "ket_10 = tensor_vec ket_1 ket_0" + +lemma ket_10_dim: + shows "dim_vec ket_10 = 4" unfolding ket_10_def by (simp add: ket_0_dim ket_1_dim) + +text \We define \verb+ket_psim+, one of the Bell states (or EPR pair).\ + +definition ket_psim where +"ket_psim = 1/(sqrt 2) \\<^sub>v (ket_01 - ket_10)" + +lemma ket_psim_dim: + shows "dim_vec ket_psim = 4" using ket_01_dim ket_10_dim unfolding ket_psim_def by simp + +lemma ket_psim_norm: + shows "\ket_psim\ = 1" +proof - + have "dim_vec ket_psim = 2\<^sup>2" unfolding ket_psim_def ket_01_def ket_10_def ket_0_def ket_1_def + by simp + moreover have "(\i<4. (cmod (vec_index ket_psim i))\<^sup>2) = 1" + apply (auto simp add: ket_psim_def ket_01_def ket_10_def ket_0_def ket_1_def) + apply (simp add: sum_4_elems) + done + ultimately show ?thesis by (simp add: cpx_vec_length_def) +qed + +text \\verb+rho_psim+ represents the density operator associated with the quantum +state \verb+ket_psim+.\ + +definition rho_psim where +"rho_psim = rank_1_proj ket_psim" + +lemma rho_psim_carrier: + shows "rho_psim \ carrier_mat 4 4" using rank_1_proj_carrier[of ket_psim] ket_psim_dim + rho_psim_def by simp + +lemma rho_psim_dim_row: + shows "dim_row rho_psim = 4" using rho_psim_carrier by simp + +lemma rho_psim_density: + shows "density_operator rho_psim" unfolding density_operator_def +proof + show "Complex_Matrix.positive rho_psim" using rank_1_proj_positive[of ket_psim] ket_psim_norm + rho_psim_def by simp + show "Complex_Matrix.trace rho_psim = 1" using rank_1_proj_trace[of ket_psim] ket_psim_norm + rho_psim_def by simp +qed + + +subsubsection \The X and Z matrices and two of their combinations\ + +text \In this part we prove properties of two standard matrices in quantum theory, $X$ and $Z$, +as well as two of their combinations: $\frac{X+Z}{\sqrt{2}}$ and $\frac{Z - X}{\sqrt{2}}$. +Note that all of these matrices are observables, they will be used to violate the CHSH inequality.\ + +lemma Z_carrier: shows "Z \ carrier_mat 2 2" unfolding Z_def by simp + +lemma Z_hermitian: + shows "hermitian Z" using dagger_adjoint dagger_of_Z unfolding hermitian_def by simp + +lemma unitary_Z: + shows "Complex_Matrix.unitary Z" +proof - + have "Complex_Matrix.adjoint Z * Z = (1\<^sub>m 2)" using dagger_adjoint[of Z] by simp + thus ?thesis unfolding unitary_def + by (metis Complex_Matrix.adjoint_adjoint Complex_Matrix.unitary_def Z_carrier adjoint_dim + carrier_matD(1) inverts_mat_def unitary_adjoint) +qed + +lemma X_carrier: shows "X \ carrier_mat 2 2" unfolding X_def by simp + +lemma X_hermitian: + shows "hermitian X" using dagger_adjoint dagger_of_X unfolding hermitian_def by simp + +lemma unitary_X: + shows "Complex_Matrix.unitary X" +proof - + have "Complex_Matrix.adjoint X * X = (1\<^sub>m 2)" using dagger_adjoint[of X] by simp + thus ?thesis unfolding unitary_def + by (metis Complex_Matrix.adjoint_adjoint Complex_Matrix.unitary_def X_carrier adjoint_dim + carrier_matD(1) inverts_mat_def unitary_adjoint) +qed + +definition XpZ + where "XpZ = -1/sqrt(2) \\<^sub>m (X + Z)" + +lemma XpZ_carrier: + shows "XpZ \ carrier_mat 2 2" unfolding XpZ_def X_def Z_def by simp + +lemma XpZ_hermitian: + shows "hermitian XpZ" +proof - + have "X + Z \ carrier_mat 2 2" using Z_carrier X_carrier by simp + moreover have "hermitian (X + Z)" using X_hermitian Z_hermitian hermitian_add Matrix.mat_carrier + unfolding X_def Z_def by blast + ultimately show ?thesis using hermitian_smult[of "X + Z" 2 "- 1 / sqrt 2"] unfolding XpZ_def + by auto +qed + +lemma XpZ_inv: + "XpZ * XpZ = 1\<^sub>m 2" unfolding XpZ_def X_def Z_def times_mat_def one_mat_def + apply (rule cong_mat, simp+) + apply (auto simp add: Matrix.scalar_prod_def) + apply (auto simp add: Gates.csqrt_2_sq) + done + +lemma unitary_XpZ: + shows "Complex_Matrix.unitary XpZ" +proof - + have "Complex_Matrix.adjoint XpZ * XpZ = (1\<^sub>m 2)" using XpZ_inv XpZ_hermitian + unfolding hermitian_def by simp + thus ?thesis unfolding unitary_def + by (metis Complex_Matrix.adjoint_adjoint Complex_Matrix.unitary_def XpZ_carrier adjoint_dim + carrier_matD(1) inverts_mat_def unitary_adjoint) +qed + +definition ZmX + where "ZmX = 1/sqrt(2) \\<^sub>m (Z - X)" + +lemma ZmX_carrier: + shows "ZmX \ carrier_mat 2 2" unfolding ZmX_def X_def Z_def + by (simp add: minus_carrier_mat') + +lemma ZmX_hermitian: + shows "hermitian ZmX" +proof - + have "Z - X \ carrier_mat 2 2" unfolding X_def Z_def + by (simp add: minus_carrier_mat) + moreover have "hermitian (Z - X)" using X_hermitian Z_hermitian hermitian_minus Matrix.mat_carrier + unfolding X_def Z_def by blast + ultimately show ?thesis using hermitian_smult[of "Z - X" 2 "1 / sqrt 2"] unfolding ZmX_def + by auto +qed + +lemma ZmX_inv: + "ZmX * ZmX = 1\<^sub>m 2" unfolding ZmX_def X_def Z_def times_mat_def one_mat_def + apply (rule cong_mat, simp+) + apply (auto simp add: Matrix.scalar_prod_def) + apply (auto simp add: Gates.csqrt_2_sq) + done + +lemma unitary_ZmX: + shows "Complex_Matrix.unitary ZmX" +proof - + have "Complex_Matrix.adjoint ZmX * ZmX = (1\<^sub>m 2)" using ZmX_inv ZmX_hermitian + unfolding hermitian_def by simp + thus ?thesis unfolding unitary_def + by (metis Complex_Matrix.adjoint_adjoint Complex_Matrix.unitary_def ZmX_carrier adjoint_dim + carrier_matD(1) inverts_mat_def unitary_adjoint) +qed + +definition Z_XpZ + where "Z_XpZ = tensor_mat Z XpZ" + +lemma Z_XpZ_carrier: + shows "Z_XpZ \ carrier_mat 4 4" unfolding Z_XpZ_def using tensor_mat_carrier XpZ_carrier + Z_carrier by auto + +definition X_XpZ + where "X_XpZ = tensor_mat X XpZ" + +lemma X_XpZ_carrier: + shows "X_XpZ \ carrier_mat 4 4" using tensor_mat_carrier XpZ_carrier X_carrier + unfolding X_XpZ_def by auto + +definition Z_ZmX + where "Z_ZmX = tensor_mat Z ZmX" + +lemma Z_ZmX_carrier: + shows "Z_ZmX \ carrier_mat 4 4" using tensor_mat_carrier ZmX_carrier Z_carrier + unfolding Z_ZmX_def by auto + +definition X_ZmX + where "X_ZmX = tensor_mat X ZmX" + +lemma X_ZmX_carrier: + shows "X_ZmX \ carrier_mat 4 4" using tensor_mat_carrier X_carrier ZmX_carrier + unfolding X_ZmX_def by auto + +lemma X_ZmX_rho_psim[simp]: + shows "Complex_Matrix.trace (rho_psim * X_ZmX) = 1/ (sqrt 2)" + apply (auto simp add: ket_10_def ket_1_def X_ZmX_def ZmX_def X_def ket_01_def + Z_def rho_psim_def ket_psim_def rank_1_proj_def outer_prod_def ket_0_def) + apply (auto simp add: Complex_Matrix.trace_def) + apply (simp add: sum_4_elems) + apply (simp add: csqrt_2_sq) + done + +lemma Z_ZmX_rho_psim[simp]: + shows "Complex_Matrix.trace (rho_psim * Z_ZmX) = -1/ (sqrt 2)" + apply (auto simp add: rho_psim_def ket_psim_def ket_10_def) + apply (auto simp add: Z_ZmX_def Z_def ZmX_def X_def) + apply (auto simp add: rank_1_proj_def outer_prod_def ket_01_def ket_1_def ket_0_def) + apply (auto simp add: Complex_Matrix.trace_def sum_4_elems) + apply (simp add: csqrt_2_sq) + done + +lemma X_XpZ_rho_psim[simp]: + shows "Complex_Matrix.trace (rho_psim * X_XpZ) =1/ (sqrt 2)" + apply (auto simp add: rho_psim_def ket_psim_def ket_10_def) + apply (auto simp add: X_XpZ_def Z_def XpZ_def X_def) + apply (auto simp add: rank_1_proj_def outer_prod_def ket_01_def ket_1_def ket_0_def) + apply (auto simp add: Complex_Matrix.trace_def sum_4_elems) + apply (simp add: csqrt_2_sq) + done + +lemma Z_XpZ_rho_psim[simp]: + shows "Complex_Matrix.trace (rho_psim * Z_XpZ) =1/ (sqrt 2)" + apply (auto simp add: rho_psim_def ket_psim_def ket_10_def) + apply (auto simp add: Z_XpZ_def XpZ_def X_def Z_def) + apply (auto simp add: rank_1_proj_def outer_prod_def ket_01_def ket_1_def ket_0_def) + apply (auto simp add: Complex_Matrix.trace_def sum_4_elems) + apply (simp add: csqrt_2_sq) + done + +definition Z_I where +"Z_I = tensor_mat Z (1\<^sub>m 2)" + +lemma Z_I_carrier: + shows "Z_I \ carrier_mat 4 4" using tensor_mat_carrier Z_carrier unfolding Z_I_def by auto + +lemma Z_I_hermitian: + shows "hermitian Z_I" unfolding Z_I_def using tensor_mat_hermitian[of Z 2 "1\<^sub>m 2" 2] + by (simp add: Z_carrier Z_hermitian hermitian_one) + +lemma Z_I_unitary: + shows "unitary Z_I" unfolding Z_I_def using tensor_mat_unitary[of Z "1\<^sub>m 2"] Z_carrier unitary_Z + using unitary_one by auto + +lemma Z_I_spectrum: + shows "{Re x |x. x \ spectrum Z_I} \ {- 1, 1}" using unitary_hermitian_Re_spectrum Z_I_hermitian + Z_I_unitary Z_I_carrier by simp + +definition X_I where +"X_I = tensor_mat X (1\<^sub>m 2)" + +lemma X_I_carrier: + shows "X_I \ carrier_mat 4 4" using tensor_mat_carrier X_carrier unfolding X_I_def by auto + +lemma X_I_hermitian: + shows "hermitian X_I" unfolding X_I_def using tensor_mat_hermitian[of X 2 "1\<^sub>m 2" 2] + by (simp add: X_carrier X_hermitian hermitian_one) + +lemma X_I_unitary: + shows "unitary X_I" unfolding X_I_def using tensor_mat_unitary[of X "1\<^sub>m 2"] X_carrier unitary_X + using unitary_one by auto + +lemma X_I_spectrum: + shows "{Re x |x. x \ spectrum X_I} \ {- 1, 1}" using unitary_hermitian_Re_spectrum X_I_hermitian + X_I_unitary X_I_carrier by simp + +definition I_XpZ where +"I_XpZ = tensor_mat (1\<^sub>m 2) XpZ" + +lemma I_XpZ_carrier: + shows "I_XpZ \ carrier_mat 4 4" using tensor_mat_carrier XpZ_carrier unfolding I_XpZ_def by auto + +lemma I_XpZ_hermitian: + shows "hermitian I_XpZ" unfolding I_XpZ_def using tensor_mat_hermitian[of "1\<^sub>m 2" 2 XpZ 2] + by (simp add: XpZ_carrier XpZ_hermitian hermitian_one) + +lemma I_XpZ_unitary: + shows "unitary I_XpZ" unfolding I_XpZ_def using tensor_mat_unitary[of "1\<^sub>m 2" XpZ] XpZ_carrier + unitary_XpZ using unitary_one by auto + +lemma I_XpZ_spectrum: + shows "{Re x |x. x \ spectrum I_XpZ} \ {- 1, 1}" using unitary_hermitian_Re_spectrum + I_XpZ_hermitian I_XpZ_unitary I_XpZ_carrier by simp + +definition I_ZmX where +"I_ZmX = tensor_mat (1\<^sub>m 2) ZmX" + +lemma I_ZmX_carrier: + shows "I_ZmX \ carrier_mat 4 4" using tensor_mat_carrier ZmX_carrier unfolding I_ZmX_def by auto + +lemma I_ZmX_hermitian: + shows "hermitian I_ZmX" unfolding I_ZmX_def using tensor_mat_hermitian[of "1\<^sub>m 2" 2 ZmX 2] + by (simp add: ZmX_carrier ZmX_hermitian hermitian_one) + +lemma I_ZmX_unitary: + shows "unitary I_ZmX" unfolding I_ZmX_def using tensor_mat_unitary[of "1\<^sub>m 2" ZmX] ZmX_carrier + unitary_ZmX using unitary_one by auto + +lemma I_ZmX_spectrum: + shows "{Re x |x. x \ spectrum I_ZmX} \ {- 1, 1}" using unitary_hermitian_Re_spectrum I_ZmX_hermitian + I_ZmX_unitary I_ZmX_carrier by simp + +lemma X_I_ZmX_eq: + shows "X_I * I_ZmX = X_ZmX" unfolding X_I_def I_ZmX_def X_ZmX_def using mult_distr_tensor + by (metis (no_types, lifting) X_inv ZmX_inv index_mult_mat(2) index_mult_mat(3) index_one_mat(2) + index_one_mat(3) left_mult_one_mat' pos2 right_mult_one_mat') + +lemma X_I_XpZ_eq: + shows "X_I * I_XpZ = X_XpZ" unfolding X_I_def I_XpZ_def X_XpZ_def using mult_distr_tensor + by (metis (no_types, lifting) X_inv XpZ_inv index_mult_mat(2) index_mult_mat(3) index_one_mat(2) + index_one_mat(3) left_mult_one_mat' pos2 right_mult_one_mat') + +lemma Z_I_XpZ_eq: + shows "Z_I * I_XpZ = Z_XpZ" unfolding Z_I_def I_XpZ_def Z_XpZ_def using mult_distr_tensor + by (metis (no_types, lifting) Z_inv XpZ_inv index_mult_mat(2) index_mult_mat(3) index_one_mat(2) + index_one_mat(3) left_mult_one_mat' pos2 right_mult_one_mat') + +lemma Z_I_ZmX_eq: + shows "Z_I * I_ZmX = Z_ZmX" unfolding Z_I_def I_ZmX_def Z_ZmX_def using mult_distr_tensor + by (metis (no_types, lifting) Z_inv ZmX_inv index_mult_mat(2) index_mult_mat(3) index_one_mat(2) + index_one_mat(3) left_mult_one_mat' pos2 right_mult_one_mat') + + +subsubsection \No local hidden variable\ + +text \We show that the local hidden variable hypothesis cannot hold by exhibiting a quantum +expectation value that is greater than the upper-bound givven by the CHSH inequality.\ + +locale bin_cpx = cpx_sq_mat + + assumes dim4: "dimR = 4" + +lemma (in bin_cpx) X_I_XpZ_trace: + assumes "lhv M X_I I_XpZ R Vx Vp" + and "R\ fc_mats" + shows "LINT w|M. (qt_expect X_I Vx w) * (qt_expect I_XpZ Vp w) = + Re (Complex_Matrix.trace (R * X_XpZ))" +proof - + have "LINT w|M. (qt_expect X_I Vx w) * (qt_expect I_XpZ Vp w) = + Re (Complex_Matrix.trace (X_I * I_XpZ * R))" + proof (rule sum_qt_expect, (simp add: assms)) + show "X_I \ fc_mats" using X_I_carrier dim4 fc_mats_carrier dim_eq by simp + show "R\ fc_mats" using assms by simp + show "I_XpZ \ fc_mats" using I_XpZ_carrier dim4 fc_mats_carrier dim_eq by simp + show "hermitian X_I" using X_I_hermitian . + show "hermitian I_XpZ" using I_XpZ_hermitian . + qed + also have "... = Re (Complex_Matrix.trace (X_XpZ * R))" using X_I_XpZ_eq by simp + also have "... = Re (Complex_Matrix.trace (R * X_XpZ))" + proof - + have "Complex_Matrix.trace (X_XpZ * R) = Complex_Matrix.trace (R * X_XpZ)" + using trace_comm[of X_XpZ 4 R] X_XpZ_carrier assms dim4 fc_mats_carrier dim_eq by simp + thus ?thesis by simp + qed + finally show ?thesis . +qed + +lemma (in bin_cpx) X_I_XpZ_chsh: + assumes "lhv M X_I I_XpZ rho_psim Vx Vp" + shows "LINT w|M. (qt_expect X_I Vx w) * (qt_expect I_XpZ Vp w) = + 1/sqrt 2" +proof - + have "LINT w|M. (qt_expect X_I Vx w) * (qt_expect I_XpZ Vp w) = + Re (Complex_Matrix.trace (rho_psim * X_XpZ))" + proof (rule X_I_XpZ_trace, (simp add: assms)) + show "rho_psim \ fc_mats" using rho_psim_carrier fc_mats_carrier dim_eq dim4 by simp + qed + also have "... = 1/sqrt 2" using X_XpZ_rho_psim by simp + finally show ?thesis . +qed + +lemma (in bin_cpx) Z_I_XpZ_trace: + assumes "lhv M Z_I I_XpZ R Vz Vp" + and "R\ fc_mats" + shows "LINT w|M. (qt_expect Z_I Vz w) * (qt_expect I_XpZ Vp w) = + Re (Complex_Matrix.trace (R * Z_XpZ))" +proof - + have "LINT w|M. (qt_expect Z_I Vz w) * (qt_expect I_XpZ Vp w) = + Re (Complex_Matrix.trace (Z_I * I_XpZ * R))" + proof (rule sum_qt_expect, (simp add: assms)) + show "Z_I \ fc_mats" using Z_I_carrier dim4 fc_mats_carrier dim_eq by simp + show "R\ fc_mats" using assms by simp + show "I_XpZ \ fc_mats" using I_XpZ_carrier dim4 fc_mats_carrier dim_eq by simp + show "hermitian Z_I" using Z_I_hermitian . + show "hermitian I_XpZ" using I_XpZ_hermitian . + qed + also have "... = Re (Complex_Matrix.trace (Z_XpZ * R))" using Z_I_XpZ_eq by simp + also have "... = Re (Complex_Matrix.trace (R * Z_XpZ))" + proof - + have "Complex_Matrix.trace (Z_XpZ * R) = Complex_Matrix.trace (R * Z_XpZ)" + using trace_comm[of Z_XpZ 4 R] Z_XpZ_carrier assms dim4 fc_mats_carrier dim_eq by simp + thus ?thesis by simp + qed + finally show ?thesis . +qed + +lemma (in bin_cpx) Z_I_XpZ_chsh: + assumes "lhv M Z_I I_XpZ rho_psim Vz Vp" + shows "LINT w|M. (qt_expect Z_I Vz w) * (qt_expect I_XpZ Vp w) = + 1/sqrt 2" +proof - + have "LINT w|M. (qt_expect Z_I Vz w) * (qt_expect I_XpZ Vp w) = + Re (Complex_Matrix.trace (rho_psim * Z_XpZ))" + proof (rule Z_I_XpZ_trace, (simp add: assms)) + show "rho_psim \ fc_mats" using rho_psim_carrier fc_mats_carrier dim_eq dim4 by simp + qed + also have "... = 1/sqrt 2" using Z_XpZ_rho_psim by simp + finally show ?thesis unfolding qt_expect_def . +qed + +lemma (in bin_cpx) X_I_ZmX_trace: + assumes "lhv M X_I I_ZmX R Vx Vp" + and "R\ fc_mats" + shows "LINT w|M. (qt_expect X_I Vx w) * (qt_expect I_ZmX Vp w) = + Re (Complex_Matrix.trace (R * X_ZmX))" +proof - + have "LINT w|M. (qt_expect X_I Vx w) * (qt_expect I_ZmX Vp w) = + Re (Complex_Matrix.trace (X_I * I_ZmX * R))" + proof (rule sum_qt_expect, (simp add: assms)) + show "X_I \ fc_mats" using X_I_carrier dim4 fc_mats_carrier dim_eq by simp + show "R\ fc_mats" using assms by simp + show "I_ZmX \ fc_mats" using I_ZmX_carrier dim4 fc_mats_carrier dim_eq by simp + show "hermitian X_I" using X_I_hermitian . + show "hermitian I_ZmX" using I_ZmX_hermitian . + qed + also have "... = Re (Complex_Matrix.trace (X_ZmX * R))" using X_I_ZmX_eq by simp + also have "... = Re (Complex_Matrix.trace (R * X_ZmX))" + proof - + have "Complex_Matrix.trace (X_ZmX * R) = Complex_Matrix.trace (R * X_ZmX)" + using trace_comm[of X_ZmX 4 R] X_ZmX_carrier assms dim4 fc_mats_carrier dim_eq by simp + thus ?thesis by simp + qed + finally show ?thesis . +qed + +lemma (in bin_cpx) X_I_ZmX_chsh: + assumes "lhv M X_I I_ZmX rho_psim Vx Vp" + shows "LINT w|M. (qt_expect X_I Vx w) * (qt_expect I_ZmX Vp w) = + 1/sqrt 2" +proof - + have "LINT w|M. (qt_expect X_I Vx w) * (qt_expect I_ZmX Vp w) = + Re (Complex_Matrix.trace (rho_psim * X_ZmX))" + proof (rule X_I_ZmX_trace, (simp add: assms)) + show "rho_psim \ fc_mats" using rho_psim_carrier fc_mats_carrier dim_eq dim4 by simp + qed + also have "... = 1/sqrt 2" using X_ZmX_rho_psim by simp + finally show ?thesis unfolding qt_expect_def . +qed + +lemma (in bin_cpx) Z_I_ZmX_trace: + assumes "lhv M Z_I I_ZmX R Vz Vp" + and "R\ fc_mats" + shows "LINT w|M. (qt_expect Z_I Vz w) * (qt_expect I_ZmX Vp w) = + Re (Complex_Matrix.trace (R * Z_ZmX))" +proof - + have "LINT w|M. (qt_expect Z_I Vz w) * (qt_expect I_ZmX Vp w) = + Re (Complex_Matrix.trace (Z_I * I_ZmX * R))" + proof (rule sum_qt_expect, (simp add: assms)) + show "Z_I \ fc_mats" using Z_I_carrier dim4 fc_mats_carrier dim_eq by simp + show "R\ fc_mats" using assms by simp + show "I_ZmX \ fc_mats" using I_ZmX_carrier dim4 fc_mats_carrier dim_eq by simp + show "hermitian Z_I" using Z_I_hermitian . + show "hermitian I_ZmX" using I_ZmX_hermitian . + qed + also have "... = Re (Complex_Matrix.trace (Z_ZmX * R))" using Z_I_ZmX_eq by simp + also have "... = Re (Complex_Matrix.trace (R * Z_ZmX))" + proof - + have "Complex_Matrix.trace (Z_ZmX * R) = Complex_Matrix.trace (R * Z_ZmX)" + using trace_comm[of Z_ZmX 4 R] Z_ZmX_carrier assms dim4 fc_mats_carrier dim_eq by simp + thus ?thesis by simp + qed + finally show ?thesis . +qed + +lemma (in bin_cpx) Z_I_ZmX_chsh: + assumes "lhv M Z_I I_ZmX rho_psim Vz Vp" +shows "LINT w|M. (qt_expect Z_I Vz w) * (qt_expect I_ZmX Vp w) = + -1/sqrt 2" +proof - + have "LINT w|M. (qt_expect Z_I Vz w) * (qt_expect I_ZmX Vp w) = + Re (Complex_Matrix.trace (rho_psim * Z_ZmX))" + proof (rule Z_I_ZmX_trace, (simp add: assms)) + show "rho_psim \ fc_mats" using rho_psim_carrier fc_mats_carrier dim_eq dim4 by simp + qed + also have "... = -1/sqrt 2" using Z_ZmX_rho_psim by simp + finally show ?thesis unfolding qt_expect_def . +qed + +lemma (in bin_cpx) chsh_upper_bound: + assumes "prob_space M" + and "lhv M X_I I_XpZ rho_psim Vx Vp" + and "lhv M Z_I I_XpZ rho_psim Vz Vp" + and "lhv M X_I I_ZmX rho_psim Vx Vm" + and "lhv M Z_I I_ZmX rho_psim Vz Vm" +shows "\(LINT w|M. qt_expect X_I Vx w * qt_expect I_ZmX Vm w) + + (LINT w|M. qt_expect Z_I Vz w * qt_expect I_XpZ Vp w) + + (LINT w|M. qt_expect X_I Vx w * qt_expect I_XpZ Vp w) - + (LINT w|M. qt_expect Z_I Vz w * qt_expect I_ZmX Vm w)\ + \ 2" +proof (rule prob_space.chsh_expect) + show "AE w in M. \qt_expect X_I Vx w\ \ 1" unfolding qt_expect_def + proof (rule spectrum_abs_1_weighted_suml) + show "X_I \ fc_mats" using X_I_carrier fc_mats_carrier dim_eq dim4 by simp + show "hermitian X_I" using X_I_hermitian . + show "lhv M X_I I_XpZ rho_psim Vx Vp" using assms by simp + show "{Re x |x. x \ spectrum X_I} \ {- 1, 1}" using X_I_spectrum by simp + show "{Re x |x. x \ spectrum X_I} \ {}" using spectrum_ne X_I_hermitian \X_I \ fc_mats\ by auto + qed + show "AE w in M. \qt_expect Z_I Vz w\ \ 1" unfolding qt_expect_def + proof (rule spectrum_abs_1_weighted_suml) + show "Z_I \ fc_mats" using Z_I_carrier fc_mats_carrier dim_eq dim4 by simp + show "hermitian Z_I" using Z_I_hermitian . + show "lhv M Z_I I_XpZ rho_psim Vz Vp" using assms by simp + show "{Re x |x. x \ spectrum Z_I} \ {- 1, 1}" using Z_I_spectrum by simp + show "{Re x |x. x \ spectrum Z_I} \ {}" using spectrum_ne Z_I_hermitian \Z_I \ fc_mats\ by auto + qed + show "AE w in M. \qt_expect I_XpZ Vp w\ \ 1" unfolding qt_expect_def + proof (rule spectrum_abs_1_weighted_sumr) + show "I_XpZ \ fc_mats" using I_XpZ_carrier fc_mats_carrier dim_eq dim4 by simp + show "hermitian I_XpZ" using I_XpZ_hermitian . + show "lhv M Z_I I_XpZ rho_psim Vz Vp" using assms by simp + show "{Re x |x. x \ spectrum I_XpZ} \ {- 1, 1}" using I_XpZ_spectrum by simp + show "{Re x |x. x \ spectrum I_XpZ} \ {}" using spectrum_ne I_XpZ_hermitian \I_XpZ \ fc_mats\ + by auto + qed + show "AE w in M. \qt_expect I_ZmX Vm w\ \ 1" unfolding qt_expect_def + proof (rule spectrum_abs_1_weighted_sumr) + show "I_ZmX \ fc_mats" using I_ZmX_carrier fc_mats_carrier dim_eq dim4 by simp + show "hermitian I_ZmX" using I_ZmX_hermitian . + show "lhv M Z_I I_ZmX rho_psim Vz Vm" using assms by simp + show "{Re x |x. x \ spectrum I_ZmX} \ {- 1, 1}" using I_ZmX_spectrum by simp + show "{Re x |x. x \ spectrum I_ZmX} \ {}" using spectrum_ne I_ZmX_hermitian \I_ZmX \ fc_mats\ + by auto + qed + show "prob_space M" using assms by simp + show "integrable M (\w. qt_expect X_I Vx w * qt_expect I_ZmX Vm w)" + using spectr_sum_integrable[of M] assms by simp + show "integrable M (\w. qt_expect Z_I Vz w * qt_expect I_ZmX Vm w)" + using spectr_sum_integrable[of M] assms by simp + show "integrable M (\w. qt_expect X_I Vx w * qt_expect I_XpZ Vp w)" + using spectr_sum_integrable[of M] assms by simp + show "integrable M (\w. qt_expect Z_I Vz w * qt_expect I_XpZ Vp w)" + using spectr_sum_integrable[of M] assms by simp +qed + +lemma (in bin_cpx) quantum_value: + assumes "lhv M X_I I_XpZ rho_psim Vx Vp" + and "lhv M Z_I I_XpZ rho_psim Vz Vp" + and "lhv M X_I I_ZmX rho_psim Vx Vm" + and "lhv M Z_I I_ZmX rho_psim Vz Vm" +shows "\(LINT w|M. qt_expect X_I Vx w * qt_expect I_ZmX Vm w) + + (LINT w|M. qt_expect Z_I Vz w * qt_expect I_XpZ Vp w) + + (LINT w|M. qt_expect X_I Vx w * qt_expect I_XpZ Vp w) - + (LINT w|M. qt_expect Z_I Vz w * qt_expect I_ZmX Vm w)\ + = 2* sqrt 2" +proof - + have "LINT w|M. qt_expect X_I Vx w * qt_expect I_ZmX Vm w = 1/sqrt 2" + using X_I_ZmX_chsh[of M] assms unfolding qt_expect_def by simp + moreover have b: "LINT w|M. qt_expect X_I Vx w * qt_expect I_XpZ Vp w = 1/sqrt 2" + using X_I_XpZ_chsh[of M] assms unfolding qt_expect_def by simp + moreover have c: "LINT w|M. qt_expect Z_I Vz w * qt_expect I_XpZ Vp w = 1/sqrt 2" + using Z_I_XpZ_chsh[of M] assms unfolding qt_expect_def by simp + moreover have "LINT w|M. qt_expect Z_I Vz w * qt_expect I_ZmX Vm w = -1/sqrt 2" + using Z_I_ZmX_chsh[of M] assms unfolding qt_expect_def by simp + ultimately have "(LINT w|M. qt_expect X_I Vx w * qt_expect I_ZmX Vm w) + + (LINT w|M. qt_expect X_I Vx w * qt_expect I_XpZ Vp w) + + (LINT w|M. qt_expect Z_I Vz w * qt_expect I_XpZ Vp w) - + (LINT w|M. qt_expect Z_I Vz w * qt_expect I_ZmX Vm w) = 4/(sqrt 2)" by simp + also have "... = (4 * (sqrt 2))/(sqrt 2 * (sqrt 2))" + by (metis mult_numeral_1_right real_divide_square_eq times_divide_eq_right) + also have "... = (4 * (sqrt 2)) / 2" by simp + also have "... = 2 * (sqrt 2)" by simp + finally have "(LINT w|M. qt_expect X_I Vx w * qt_expect I_ZmX Vm w) + + (LINT w|M. qt_expect X_I Vx w * qt_expect I_XpZ Vp w) + + (LINT w|M. qt_expect Z_I Vz w * qt_expect I_XpZ Vp w) - + (LINT w|M. qt_expect Z_I Vz w * qt_expect I_ZmX Vm w) = 2 * sqrt 2" . + thus ?thesis by (simp add: b c) +qed + +lemma (in bin_cpx) no_lhv: + assumes "lhv M X_I I_XpZ rho_psim Vx Vp" + and "lhv M Z_I I_XpZ rho_psim Vz Vp" + and "lhv M X_I I_ZmX rho_psim Vx Vm" + and "lhv M Z_I I_ZmX rho_psim Vz Vm" +shows False +proof - + have "prob_space M" using assms unfolding lhv_def by simp + have "2 * sqrt 2 = \(LINT w|M. qt_expect X_I Vx w * qt_expect I_ZmX Vm w) + + (LINT w|M. qt_expect Z_I Vz w * qt_expect I_XpZ Vp w) + + (LINT w|M. qt_expect X_I Vx w * qt_expect I_XpZ Vp w) - + (LINT w|M. qt_expect Z_I Vz w * qt_expect I_ZmX Vm w)\" + using assms quantum_value[of M] by simp + also have "... \ 2" using chsh_upper_bound[of M] assms \prob_space M\ by simp + finally have "2 * sqrt 2 \ 2" . + thus False by simp +qed + + +end \ No newline at end of file diff --git a/thys/Projective_Measurements/Linear_Algebra_Complements.thy b/thys/Projective_Measurements/Linear_Algebra_Complements.thy new file mode 100644 --- /dev/null +++ b/thys/Projective_Measurements/Linear_Algebra_Complements.thy @@ -0,0 +1,2269 @@ +(* +Author: + Mnacho Echenim, Université Grenoble Alpes +*) + +theory Linear_Algebra_Complements imports + "Isabelle_Marries_Dirac.Tensor" + "Isabelle_Marries_Dirac.More_Tensor" + "QHLProver.Gates" + "HOL-Types_To_Sets.Group_On_With" + "HOL-Probability.Probability" + + +begin +hide_const(open) S +section \Preliminaries\ + + +subsection \Misc\ + +lemma mult_real_cpx: + fixes a::complex + fixes b::complex + assumes "a\ Reals" + shows "a* (Re b) = Re (a * b)" using assms + by (metis Reals_cases complex.exhaust complex.sel(1) complex_of_real_mult_Complex of_real_mult) + +lemma fct_bound: + fixes f::"complex\ real" + assumes "f(-1) + f 1 = 1" +and "0 \ f 1" +and "0 \ f (-1)" +shows "-1 \ f 1 - f(-1) \ f 1 - f(-1) \ 1" +proof + have "f 1 - f(-1) = 1 - f(-1) - f(-1)" using assms by simp + also have "...\ -1" using assms by simp + finally show "-1 \ f 1 - f(-1)" . +next + have "f(-1) - f 1 = 1 - f 1 - f 1 " using assms by simp + also have "... \ -1" using assms by simp + finally have "-1 \ f(-1) - f 1" . + thus "f 1 - f (-1) \ 1" by simp +qed + +lemma fct_bound': + fixes f::"complex\ real" + assumes "f(-1) + f 1 = 1" +and "0 \ f 1" +and "0 \ f (-1)" +shows "\f 1 - f(-1)\ \ 1" using assms fct_bound by auto + +lemma pos_sum_1_le: + assumes "finite I" +and "\ i \ I. (0::real) \ f i" +and "(\i\ I. f i) = 1" +and "j\ I" +shows "f j \ 1" +proof (rule ccontr) + assume "\ f j \ 1" + hence "1 < f j" by simp + hence "1 < (\i\ I. f i)" using assms by (metis \\ f j \ 1\ sum_nonneg_leq_bound) + thus False using assms by simp +qed + +lemma last_subset: + assumes "A \ {a,b}" + and "a\ b" +and "A \ {a, b}" +and "A\ {}" +and "A \ {a}" +shows "A = {b}" using assms by blast + +lemma disjoint_Un: + assumes "disjoint_family_on A (insert x F)" + and "x\ F" +shows "(A x) \ (\ a\ F. A a) = {}" +proof - + have "(A x) \ (\ a\ F. A a) = (\i\F. (A x) \ A i)" using Int_UN_distrib by simp + also have "... = (\i\F. {})" using assms disjoint_family_onD by fastforce + also have "... = {}" using SUP_bot_conv(2) by simp + finally show ?thesis . +qed + +lemma sum_but_one: + assumes "\j < (n::nat). j \i \ f j = (0::'a::ring)" + and "i < n" + shows "(\ j \ {0 ..< n}. f j * g j) = f i * g i" +proof - + have "sum (\x. f x * g x) (({0 ..< n} - {i}) \ {i}) = sum (\x. f x * g x) ({0 ..< n} - {i}) + + sum (\x. f x * g x) {i}" by (rule sum.union_disjoint, auto) + also have "... = sum (\x. f x * g x) {i}" using assms by auto + also have "... = f i * g i" by simp + finally have "sum (\x. f x * g x) (({0 ..< n} - {i}) \ {i}) = f i * g i" . + moreover have "{0 ..< n} = ({0 ..< n} - {i}) \ {i}" using assms by auto + ultimately show ?thesis by simp +qed + +lemma sum_2_elems: + assumes "I = {a,b}" + and "a\ b" + shows "(\a\I. f a) = f a + f b" +proof - + have "(\a\I. f a) = (\a\(insert a {b}). f a)" using assms by simp + also have "... = f a + (\a\{b}. f a)" + proof (rule sum.insert) + show "finite {b}" by simp + show "a\ {b}" using assms by simp + qed + also have "... = f a + f b" by simp + finally show ?thesis . +qed + +lemma sum_4_elems: + shows "(\i<(4::nat). f i) = f 0 + f 1 + f 2 + f 3" +proof - + have "(\i<(4::nat). f i) = (\i<(3::nat). f i) + f 3" + by (metis Suc_numeral semiring_norm(2) semiring_norm(8) sum.lessThan_Suc) + moreover have "(\i<(3::nat). f i) = (\i<(2::nat). f i) + f 2" + by (metis Suc_1 add_2_eq_Suc' nat_1_add_1 numeral_code(3) numerals(1) + one_plus_numeral_commute sum.lessThan_Suc) + moreover have "(\i<(2::nat). f i) = (\i<(1::nat). f i) + f 1" + by (metis Suc_1 sum.lessThan_Suc) + ultimately show ?thesis by simp +qed + +lemma disj_family_sum: + shows "finite I \ disjoint_family_on A I \ (\i. i \ I \ finite (A i)) \ + (\ i \ (\n \ I. A n). f i) = (\ n\ I. (\ i \ A n. f i))" +proof (induct rule:finite_induct) + case empty + then show ?case by simp +next + case (insert x F) + hence "disjoint_family_on A F" + by (meson disjoint_family_on_mono subset_insertI) + have "(\n \ (insert x F). A n) = A x \ (\n \ F. A n)" using insert by simp + hence "(\ i \ (\n \ (insert x F). A n). f i) = (\ i \ (A x \ (\n \ F. A n)). f i)" by simp + also have "... = (\ i \ A x. f i) + (\ i \ (\n \ F. A n). f i)" + by (rule sum.union_disjoint, (simp add: insert disjoint_Un)+) + also have "... = (\ i \ A x. f i) + (\n\F. sum f (A n))" using \disjoint_family_on A F\ + by (simp add: insert) + also have "... = (\n\(insert x F). sum f (A n))" using insert by simp + finally show ?case . +qed + +lemma integrable_real_mult_right: + fixes c::real + assumes "integrable M f" + shows "integrable M (\w. c * f w)" +proof (cases "c = 0") + case True + thus ?thesis by simp +next + case False + thus ?thesis using integrable_mult_right[of c] assms by simp +qed + + +subsection \Unifying notions between Isabelle Marries Dirac and QHLProver\ + +lemma mult_conj_cmod_square: + fixes z::complex + shows "z * conjugate z = (cmod z)\<^sup>2" +proof - + have "z * conjugate z = (Re z)\<^sup>2 + (Im z)\<^sup>2" using complex_mult_cnj by auto + also have "... = (cmod z)\<^sup>2" unfolding cmod_def by simp + finally show ?thesis . +qed + +lemma vec_norm_sq_cpx_vec_length_sq: + shows "(vec_norm v)\<^sup>2 = (cpx_vec_length v)\<^sup>2" +proof - + have "(vec_norm v)\<^sup>2 = inner_prod v v" unfolding vec_norm_def using power2_csqrt by blast + also have "... = (\i2)" unfolding Matrix.scalar_prod_def + proof - + have "\i. i < dim_vec v \ Matrix.vec_index v i * conjugate (Matrix.vec_index v i) = + (cmod (Matrix.vec_index v i))\<^sup>2" using mult_conj_cmod_square by simp + thus "(\i = 0..i2)" + by (simp add: lessThan_atLeast0) + qed + finally show "(vec_norm v)\<^sup>2 = (cpx_vec_length v)\<^sup>2" unfolding cpx_vec_length_def + by (simp add: sum_nonneg) +qed + +lemma vec_norm_eq_cpx_vec_length: + shows "vec_norm v = cpx_vec_length v" using vec_norm_sq_cpx_vec_length_sq +by (metis cpx_vec_length_inner_prod inner_prod_csqrt power2_csqrt vec_norm_def) + +lemma cpx_vec_length_square: + shows "\v\\<^sup>2 = (\i = 0..2)" unfolding cpx_vec_length_def + by (simp add: lessThan_atLeast0 sum_nonneg) + +lemma state_qbit_norm_sq: + assumes "v\ state_qbit n" + shows "(cpx_vec_length v)\<^sup>2 = 1" +proof - + have "cpx_vec_length v = 1" using assms unfolding state_qbit_def by simp + thus ?thesis by simp +qed + +lemma dagger_adjoint: +shows "dagger M = Complex_Matrix.adjoint M" unfolding dagger_def Complex_Matrix.adjoint_def + by (simp add: cong_mat) + + +subsection \Types to sets lemmata transfers\ + +context ab_group_add_on_with begin + +context includes lifting_syntax assumes ltd: "\(Rep::'s \ 'a) (Abs::'a \ 's). + type_definition Rep Abs S" begin +interpretation local_typedef_ab_group_add_on_with pls z mns um S "TYPE('s)" by unfold_locales fact + +lemmas lt_sum_union_disjoint = sum.union_disjoint + [var_simplified explicit_ab_group_add, + unoverload_type 'c, + OF type.comm_monoid_add_axioms, + untransferred] + +lemmas lt_disj_family_sum = disj_family_sum + [var_simplified explicit_ab_group_add, + unoverload_type 'd, +OF type.comm_monoid_add_axioms, + untransferred] + +lemmas lt_sum_reindex_cong = sum.reindex_cong + [var_simplified explicit_ab_group_add, + unoverload_type 'd, +OF type.comm_monoid_add_axioms, + untransferred] +end + +lemmas sum_with_union_disjoint = + lt_sum_union_disjoint + [cancel_type_definition, + OF carrier_ne, + simplified pred_fun_def, simplified] + +lemmas disj_family_sum_with = + lt_disj_family_sum + [cancel_type_definition, + OF carrier_ne, + simplified pred_fun_def, simplified] + +lemmas sum_with_reindex_cong = + lt_sum_reindex_cong + [cancel_type_definition, + OF carrier_ne, + simplified pred_fun_def, simplified] + +end + +lemma (in comm_monoid_add_on_with) sum_with_cong': + shows "finite I \ (\i. i\ I \ A i = B i) \ (\i. i\ I \ A i \ S) \ + (\i. i\ I \ B i \ S) \ sum_with pls z A I = sum_with pls z B I" +proof (induct rule: finite_induct) + case empty + then show ?case by simp +next + case (insert x F) + have "sum_with pls z A (insert x F) = pls (A x) (sum_with pls z A F)" using insert + sum_with_insert[of A] by (simp add: image_subset_iff) + also have "... = pls (B x) (sum_with pls z B F)" using insert by simp + also have "... = sum_with pls z B (insert x F)" using insert sum_with_insert[of B] + by (simp add: image_subset_iff) + finally show ?case . +qed + + +section \Linear algebra complements\ + +subsection \Additional properties of matrices\ + +lemma smult_one: + shows "(1::'a::monoid_mult) \\<^sub>m A = A" by (simp add:eq_matI) + +lemma times_diag_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 "Matrix.vec_index (Matrix.row (A*B) j) i = diag_mat B ! i *A $$ (j, i)" +proof - + have "Matrix.vec_index (Matrix.row (A*B) j) i = (A*B) $$ (j,i)" + using Matrix.row_def[of "A*B" ] assms by simp + also have "... = Matrix.scalar_prod (Matrix.row A j) (Matrix.col B i)" using assms + times_mat_def[of A] by simp + also have "... = Matrix.scalar_prod (Matrix.col B i) (Matrix.row A j)" + using comm_scalar_prod[of "Matrix.row A j" n] assms by auto + also have "... = (Matrix.vec_index (Matrix.col B i) i) * (Matrix.vec_index (Matrix.row A j) i)" + unfolding Matrix.scalar_prod_def + proof (rule sum_but_one) + show "i < dim_vec (Matrix.row A j)" using assms by simp + show "\ia i \ Matrix.vec_index (Matrix.col B i) ia = 0" using assms + by (metis carrier_matD(1) carrier_matD(2) diagonal_mat_def index_col index_row(2)) + qed + also have "... = B $$(i,i) * (Matrix.vec_index (Matrix.row A j) i)" using assms by auto + also have "... = diag_mat B ! i * (Matrix.vec_index (Matrix.row A j) i)" unfolding diag_mat_def + using assms by simp + also have "... = diag_mat B ! i * A $$ (j, i)" using assms by simp + finally show ?thesis . +qed + +lemma inner_prod_adjoint_comp: + assumes "(U::'a::conjugatable_field Matrix.mat) \ carrier_mat n n" +and "(V::'a::conjugatable_field Matrix.mat) \ carrier_mat n n" +and "i < n" +and "j < n" +shows "Complex_Matrix.inner_prod (Matrix.col V i) (Matrix.col U j) = + ((Complex_Matrix.adjoint V) * U) $$ (i, j)" +proof - + have "Complex_Matrix.inner_prod (Matrix.col V i) (Matrix.col U j) = + Matrix.scalar_prod (Matrix.col U j) (Matrix.row (Complex_Matrix.adjoint V) i)" + using adjoint_row[of i V] assms by simp + also have "... = Matrix.scalar_prod (Matrix.row (Complex_Matrix.adjoint V) i) (Matrix.col U j)" + by (metis adjoint_row assms(1) assms(2) assms(3) carrier_matD(1) carrier_matD(2) Matrix.col_dim + conjugate_vec_sprod_comm) + also have "... = ((Complex_Matrix.adjoint V) * U) $$ (i, j)" using assms + by (simp add:times_mat_def) + finally show ?thesis . +qed + +lemma mat_unit_vec_col: + assumes "(A::'a::conjugatable_field Matrix.mat) \ carrier_mat n n" +and "i < n" +shows "A *\<^sub>v (unit_vec n i) = Matrix.col A i" +proof + show "dim_vec (A *\<^sub>v unit_vec n i) = dim_vec (Matrix.col A i)" using assms by simp + show "\j. j < dim_vec (Matrix.col A i) \ Matrix.vec_index (A *\<^sub>v unit_vec n i) j = + Matrix.vec_index (Matrix.col A i) j" + proof - + fix j + assume "j < dim_vec (Matrix.col A i)" + hence "Matrix.vec_index (A *\<^sub>v unit_vec n i) j = + Matrix.scalar_prod (Matrix.row A j) (unit_vec n i)" unfolding mult_mat_vec_def by simp + also have "... = Matrix.scalar_prod (unit_vec n i) (Matrix.row A j)" using comm_scalar_prod + assms by auto + also have "... = (Matrix.vec_index (unit_vec n i) i) * (Matrix.vec_index (Matrix.row A j) i)" + unfolding Matrix.scalar_prod_def + proof (rule sum_but_one) + show "i < dim_vec (Matrix.row A j)" using assms by auto + show "\ia i \ Matrix.vec_index (unit_vec n i) ia = 0" + using assms unfolding unit_vec_def by auto + qed + also have "... = (Matrix.vec_index (Matrix.row A j) i)" using assms by simp + also have "... = A $$ (j, i)" using assms \j < dim_vec (Matrix.col A i)\ by simp + also have "... = Matrix.vec_index (Matrix.col A i) j" using assms \j < dim_vec (Matrix.col A i)\ by simp + finally show "Matrix.vec_index (A *\<^sub>v unit_vec n i) j = + Matrix.vec_index (Matrix.col A i) j" . + qed +qed + +lemma mat_prod_unit_vec_cong: + assumes "(A::'a::conjugatable_field Matrix.mat) \ carrier_mat n n" +and "B\ carrier_mat n n" +and "\i. i < n \ A *\<^sub>v (unit_vec n i) = B *\<^sub>v (unit_vec n i)" +shows "A = B" +proof + show "dim_row A = dim_row B" using assms by simp + show "dim_col A = dim_col B" using assms by simp + show "\i j. i < dim_row B \ j < dim_col B \ A $$ (i, j) = B $$ (i, j)" + proof - + fix i j + assume ij: "i < dim_row B" "j < dim_col B" + hence "A $$ (i,j) = Matrix.vec_index (Matrix.col A j) i" using assms by simp + also have "... = Matrix.vec_index (A *\<^sub>v (unit_vec n j)) i" using mat_unit_vec_col[of A] ij assms + by simp + also have "... = Matrix.vec_index (B *\<^sub>v (unit_vec n j)) i" using assms ij by simp + also have "... = Matrix.vec_index (Matrix.col B j) i" using mat_unit_vec_col ij assms by simp + also have "... = B $$ (i,j)" using assms ij by simp + finally show "A $$ (i, j) = B $$ (i, j)" . + qed +qed + +lemma smult_smult_times: + fixes a::"'a::semigroup_mult" + shows "a\\<^sub>m (k \\<^sub>m A) = (a * k)\\<^sub>m A" +proof + show r:"dim_row (a \\<^sub>m (k \\<^sub>m A)) = dim_row (a * k \\<^sub>m A)" by simp + show c:"dim_col (a \\<^sub>m (k \\<^sub>m A)) = dim_col (a * k \\<^sub>m A)" by simp + show "\i j. i < dim_row (a * k \\<^sub>m A) \ + j < dim_col (a * k \\<^sub>m A) \ (a \\<^sub>m (k \\<^sub>m A)) $$ (i, j) = (a * k \\<^sub>m A) $$ (i, j)" + proof - + fix i j + assume "i < dim_row (a * k \\<^sub>m A)" and "j < dim_col (a * k \\<^sub>m A)" note ij = this + hence "(a \\<^sub>m (k \\<^sub>m A)) $$ (i, j) = a * (k \\<^sub>m A) $$ (i, j)" by simp + also have "... = a * (k * A $$ (i,j))" using ij by simp + also have "... = (a * k) * A $$ (i,j)" + by (simp add: semigroup_mult_class.mult.assoc) + also have "... = (a * k \\<^sub>m A) $$ (i, j)" using r c ij by simp + finally show "(a \\<^sub>m (k \\<^sub>m A)) $$ (i, j) = (a * k \\<^sub>m A) $$ (i, j)" . + qed +qed + +lemma mat_minus_minus: + fixes A :: "'a :: ab_group_add Matrix.mat" + assumes "A \ carrier_mat n m" + and "B\ carrier_mat n m" + and "C\ carrier_mat n m" +shows "A - (B - C) = A - B + C" +proof + show "dim_row (A - (B - C)) = dim_row (A - B + C)" using assms by simp + show "dim_col (A - (B - C)) = dim_col (A - B + C)" using assms by simp + show "\i j. i < dim_row (A - B + C) \ j < dim_col (A - B + C) \ + (A - (B - C)) $$ (i, j) = (A - B + C) $$ (i, j)" + proof - + fix i j + assume "i < dim_row (A - B + C)" and "j < dim_col (A - B + C)" note ij = this + have "(A - (B - C)) $$ (i, j) = (A $$ (i,j) - B $$ (i,j) + C $$ (i,j))" using ij assms by simp + also have "... = (A - B + C) $$ (i, j)" using assms ij by simp + finally show "(A - (B - C)) $$ (i, j) = (A - B + C) $$ (i, j)" . + qed +qed + + +subsection \Complements on complex matrices\ + +lemma hermitian_square: + assumes "hermitian M" + shows "M \ carrier_mat (dim_row M) (dim_row M)" +proof - + have "dim_col M = dim_row M" using assms unfolding hermitian_def adjoint_def + by (metis adjoint_dim_col) + thus ?thesis by auto +qed + +lemma hermitian_add: + assumes "A\ carrier_mat n n" + and "B\ carrier_mat n n" +and "hermitian A" +and "hermitian B" +shows "hermitian (A + B)" unfolding hermitian_def + by (metis adjoint_add assms hermitian_def) + +lemma hermitian_minus: + assumes "A\ carrier_mat n n" + and "B\ carrier_mat n n" +and "hermitian A" +and "hermitian B" +shows "hermitian (A - B)" unfolding hermitian_def + by (metis adjoint_minus assms hermitian_def) + +lemma hermitian_smult: + fixes a::real + fixes A::"complex Matrix.mat" + assumes "A \ carrier_mat n n" +and "hermitian A" +shows "hermitian (a \\<^sub>m A)" +proof - + have dim: "Complex_Matrix.adjoint A \ carrier_mat n n" using assms by (simp add: adjoint_dim) + { + fix i j + assume "i < n" and "j < n" + hence "Complex_Matrix.adjoint (a \\<^sub>m A) $$ (i,j) = a * (Complex_Matrix.adjoint A $$ (i,j))" + using adjoint_scale[of a A] assms by simp + also have "... = a * (A $$ (i,j))" using assms unfolding hermitian_def by simp + also have "... = (a \\<^sub>m A) $$ (i,j)" using \i < n\ \j < n\ assms by simp + finally have "Complex_Matrix.adjoint (a \\<^sub>m A) $$ (i,j) = (a \\<^sub>m A) $$ (i,j)" . + } + thus ?thesis using dim assms unfolding hermitian_def by auto +qed + +lemma unitary_eigenvalues_norm_square: + fixes U::"complex Matrix.mat" + assumes "unitary U" + and "U \ carrier_mat n n" + and "eigenvalue U k" +shows "conjugate k * k = 1" +proof - + have "\v. eigenvector U v k" using assms unfolding eigenvalue_def by simp + from this obtain v where "eigenvector U v k" by auto + define vn where "vn = vec_normalize v" + have "eigenvector U vn k" using normalize_keep_eigenvector \eigenvector U v k\ + using assms(2) eigenvector_def vn_def by blast + have "vn \ carrier_vec n" + using \eigenvector U v k\ assms(2) eigenvector_def normalized_vec_dim vn_def by blast + have "Complex_Matrix.inner_prod vn vn = 1" using \vn = vec_normalize v\ \eigenvector U v k\ + eigenvector_def normalized_vec_norm by blast + hence "conjugate k * k = conjugate k * k * Complex_Matrix.inner_prod vn vn" by simp + also have "... = conjugate k * Complex_Matrix.inner_prod vn (k \\<^sub>v vn)" + proof - + have "k * Complex_Matrix.inner_prod vn vn = Complex_Matrix.inner_prod vn (k \\<^sub>v vn)" + using inner_prod_smult_left[of vn n vn k] \vn \ carrier_vec n\ by simp + thus ?thesis by simp + qed + also have "... = Complex_Matrix.inner_prod (k \\<^sub>v vn) (k \\<^sub>v vn)" + using inner_prod_smult_right[of vn n _ k] by (simp add: \vn \ carrier_vec n\) + also have "... = Complex_Matrix.inner_prod (U *\<^sub>v vn) (U *\<^sub>v vn)" + using \eigenvector U vn k\ unfolding eigenvector_def by simp + also have "... = + Complex_Matrix.inner_prod (Complex_Matrix.adjoint U *\<^sub>v (U *\<^sub>v vn)) vn" + using adjoint_def_alter[of "U *\<^sub>v vn" n vn n U] assms + by (metis \eigenvector U vn k\ carrier_matD(1) carrier_vec_dim_vec dim_mult_mat_vec + eigenvector_def) + also have "... = Complex_Matrix.inner_prod vn vn" + proof - + have "Complex_Matrix.adjoint U *\<^sub>v (U *\<^sub>v vn) = (Complex_Matrix.adjoint U * U) *\<^sub>v vn" + using assms + by (metis \eigenvector U vn k\ adjoint_dim assoc_mult_mat_vec carrier_matD(1) eigenvector_def) + also have "... = vn" using assms unfolding unitary_def inverts_mat_def + by (metis \eigenvector U vn k\ assms(1) eigenvector_def one_mult_mat_vec unitary_simps(1)) + finally show ?thesis by simp + qed + also have "... = 1" using \vn = vec_normalize v\ \eigenvector U v k\ eigenvector_def + normalized_vec_norm by blast + finally show ?thesis . +qed + +lemma outer_prod_smult_left: + fixes v::"complex Matrix.vec" + shows "outer_prod (a \\<^sub>v v) w = a \\<^sub>m outer_prod v w" +proof - + define paw where "paw = outer_prod (a \\<^sub>v v) w" + define apw where "apw = a \\<^sub>m outer_prod v w" + have "paw = apw" + proof + have "dim_row paw = dim_vec v" unfolding paw_def using outer_prod_dim + by (metis carrier_matD(1) carrier_vec_dim_vec index_smult_vec(2)) + also have "... = dim_row apw" unfolding apw_def using outer_prod_dim + by (metis carrier_matD(1) carrier_vec_dim_vec index_smult_mat(2)) + finally show dr: "dim_row paw = dim_row apw" . + have "dim_col paw = dim_vec w" unfolding paw_def using outer_prod_dim + using carrier_vec_dim_vec by blast + also have "... = dim_col apw" unfolding apw_def using outer_prod_dim + by (metis apw_def carrier_matD(2) carrier_vec_dim_vec smult_carrier_mat) + finally show dc: "dim_col paw = dim_col apw" . + show "\i j. i < dim_row apw \ j < dim_col apw \ paw $$ (i, j) = apw $$ (i, j)" + proof - + fix i j + assume "i < dim_row apw" and "j < dim_col apw" note ij = this + hence "paw $$ (i,j) = a * (Matrix.vec_index v i) * cnj (Matrix.vec_index w j)" + using dr dc unfolding paw_def outer_prod_def by simp + also have "... = apw $$ (i,j)" using dr dc ij unfolding apw_def outer_prod_def by simp + finally show "paw $$ (i, j) = apw $$ (i, j)" . + qed + qed + thus ?thesis unfolding paw_def apw_def by simp +qed + +lemma outer_prod_smult_right: + fixes v::"complex Matrix.vec" + shows "outer_prod v (a \\<^sub>v w) = (conjugate a) \\<^sub>m outer_prod v w" +proof - + define paw where "paw = outer_prod v (a \\<^sub>v w)" + define apw where "apw = (conjugate a) \\<^sub>m outer_prod v w" + have "paw = apw" + proof + have "dim_row paw = dim_vec v" unfolding paw_def using outer_prod_dim + by (metis carrier_matD(1) carrier_vec_dim_vec) + also have "... = dim_row apw" unfolding apw_def using outer_prod_dim + by (metis carrier_matD(1) carrier_vec_dim_vec index_smult_mat(2)) + finally show dr: "dim_row paw = dim_row apw" . + have "dim_col paw = dim_vec w" unfolding paw_def using outer_prod_dim + using carrier_vec_dim_vec by (metis carrier_matD(2) index_smult_vec(2)) + also have "... = dim_col apw" unfolding apw_def using outer_prod_dim + by (metis apw_def carrier_matD(2) carrier_vec_dim_vec smult_carrier_mat) + finally show dc: "dim_col paw = dim_col apw" . + show "\i j. i < dim_row apw \ j < dim_col apw \ paw $$ (i, j) = apw $$ (i, j)" + proof - + fix i j + assume "i < dim_row apw" and "j < dim_col apw" note ij = this + hence "paw $$ (i,j) = (conjugate a) * (Matrix.vec_index v i) * cnj (Matrix.vec_index w j)" + using dr dc unfolding paw_def outer_prod_def by simp + also have "... = apw $$ (i,j)" using dr dc ij unfolding apw_def outer_prod_def by simp + finally show "paw $$ (i, j) = apw $$ (i, j)" . + qed + qed + thus ?thesis unfolding paw_def apw_def by simp +qed + +lemma outer_prod_add_left: + fixes v::"complex Matrix.vec" + assumes "dim_vec v = dim_vec x" + shows "outer_prod (v + x) w = outer_prod v w + (outer_prod x w)" +proof - + define paw where "paw = outer_prod (v+x) w" + define apw where "apw = outer_prod v w + (outer_prod x w)" + have "paw = apw" + proof + have rv: "dim_row paw = dim_vec v" unfolding paw_def using outer_prod_dim assms + by (metis carrier_matD(1) carrier_vec_dim_vec index_add_vec(2) paw_def) + also have "... = dim_row apw" unfolding apw_def using outer_prod_dim assms + by (metis carrier_matD(1) carrier_vec_dim_vec index_add_mat(2)) + finally show dr: "dim_row paw = dim_row apw" . + have cw: "dim_col paw = dim_vec w" unfolding paw_def using outer_prod_dim assms + using carrier_vec_dim_vec by (metis carrier_matD(2)) + also have "... = dim_col apw" unfolding apw_def using outer_prod_dim + by (metis apw_def carrier_matD(2) carrier_vec_dim_vec add_carrier_mat) + finally show dc: "dim_col paw = dim_col apw" . + show "\i j. i < dim_row apw \ j < dim_col apw \ paw $$ (i, j) = apw $$ (i, j)" + proof - + fix i j + assume "i < dim_row apw" and "j < dim_col apw" note ij = this + hence "paw $$ (i,j) = (Matrix.vec_index v i + Matrix.vec_index x i) * + cnj (Matrix.vec_index w j)" + using dr dc unfolding paw_def outer_prod_def by simp + also have "... = Matrix.vec_index v i * cnj (Matrix.vec_index w j) + + Matrix.vec_index x i * cnj (Matrix.vec_index w j)" + by (simp add: ring_class.ring_distribs(2)) + also have "... = (outer_prod v w) $$ (i,j) + (outer_prod x w) $$ (i,j)" + using rv cw dr dc ij assms unfolding outer_prod_def by auto + also have "... = apw $$ (i,j)" using dr dc ij unfolding apw_def outer_prod_def by simp + finally show "paw $$ (i, j) = apw $$ (i, j)" . + qed + qed + thus ?thesis unfolding paw_def apw_def by simp +qed + +lemma outer_prod_add_right: + fixes v::"complex Matrix.vec" + assumes "dim_vec w = dim_vec x" + shows "outer_prod v (w + x) = outer_prod v w + (outer_prod v x)" +proof - + define paw where "paw = outer_prod v (w+x)" + define apw where "apw = outer_prod v w + (outer_prod v x)" + have "paw = apw" + proof + have rv: "dim_row paw = dim_vec v" unfolding paw_def using outer_prod_dim assms + by (metis carrier_matD(1) carrier_vec_dim_vec index_add_vec(2) paw_def) + also have "... = dim_row apw" unfolding apw_def using outer_prod_dim assms + by (metis carrier_matD(1) carrier_vec_dim_vec index_add_mat(2)) + finally show dr: "dim_row paw = dim_row apw" . + have cw: "dim_col paw = dim_vec w" unfolding paw_def using outer_prod_dim assms + using carrier_vec_dim_vec + by (metis carrier_matD(2) index_add_vec(2) paw_def) + also have "... = dim_col apw" unfolding apw_def using outer_prod_dim + by (metis assms carrier_matD(2) carrier_vec_dim_vec index_add_mat(3)) + finally show dc: "dim_col paw = dim_col apw" . + show "\i j. i < dim_row apw \ j < dim_col apw \ paw $$ (i, j) = apw $$ (i, j)" + proof - + fix i j + assume "i < dim_row apw" and "j < dim_col apw" note ij = this + hence "paw $$ (i,j) = Matrix.vec_index v i * + (cnj (Matrix.vec_index w j + (Matrix.vec_index x j)))" + using dr dc unfolding paw_def outer_prod_def by simp + also have "... = Matrix.vec_index v i * cnj (Matrix.vec_index w j) + + Matrix.vec_index v i * cnj (Matrix.vec_index x j)" + by (simp add: ring_class.ring_distribs(1)) + also have "... = (outer_prod v w) $$ (i,j) + (outer_prod v x) $$ (i,j)" + using rv cw dr dc ij assms unfolding outer_prod_def by auto + also have "... = apw $$ (i,j)" using dr dc ij unfolding apw_def outer_prod_def by simp + finally show "paw $$ (i, j) = apw $$ (i, j)" . + qed + qed + thus ?thesis unfolding paw_def apw_def by simp +qed + +lemma outer_prod_minus_left: + fixes v::"complex Matrix.vec" + assumes "dim_vec v = dim_vec x" + shows "outer_prod (v - x) w = outer_prod v w - (outer_prod x w)" +proof - + define paw where "paw = outer_prod (v-x) w" + define apw where "apw = outer_prod v w - (outer_prod x w)" + have "paw = apw" + proof + have rv: "dim_row paw = dim_vec v" unfolding paw_def using outer_prod_dim assms + by (metis carrier_matD(1) carrier_vec_dim_vec index_minus_vec(2) paw_def) + also have "... = dim_row apw" unfolding apw_def using outer_prod_dim assms + by (metis carrier_matD(1) carrier_vec_dim_vec index_minus_mat(2)) + finally show dr: "dim_row paw = dim_row apw" . + have cw: "dim_col paw = dim_vec w" unfolding paw_def using outer_prod_dim assms + using carrier_vec_dim_vec by (metis carrier_matD(2)) + also have "... = dim_col apw" unfolding apw_def using outer_prod_dim + by (metis apw_def carrier_matD(2) carrier_vec_dim_vec minus_carrier_mat) + finally show dc: "dim_col paw = dim_col apw" . + show "\i j. i < dim_row apw \ j < dim_col apw \ paw $$ (i, j) = apw $$ (i, j)" + proof - + fix i j + assume "i < dim_row apw" and "j < dim_col apw" note ij = this + hence "paw $$ (i,j) = (Matrix.vec_index v i - Matrix.vec_index x i) * + cnj (Matrix.vec_index w j)" + using dr dc unfolding paw_def outer_prod_def by simp + also have "... = Matrix.vec_index v i * cnj (Matrix.vec_index w j) - + Matrix.vec_index x i * cnj (Matrix.vec_index w j)" + by (simp add: ring_class.ring_distribs) + also have "... = (outer_prod v w) $$ (i,j) - (outer_prod x w) $$ (i,j)" + using rv cw dr dc ij assms unfolding outer_prod_def by auto + also have "... = apw $$ (i,j)" using dr dc ij unfolding apw_def outer_prod_def by simp + finally show "paw $$ (i, j) = apw $$ (i, j)" . + qed + qed + thus ?thesis unfolding paw_def apw_def by simp +qed + +lemma outer_prod_minus_right: + fixes v::"complex Matrix.vec" + assumes "dim_vec w = dim_vec x" + shows "outer_prod v (w - x) = outer_prod v w - (outer_prod v x)" +proof - + define paw where "paw = outer_prod v (w-x)" + define apw where "apw = outer_prod v w - (outer_prod v x)" + have "paw = apw" + proof + have rv: "dim_row paw = dim_vec v" unfolding paw_def using outer_prod_dim assms + by (metis carrier_matD(1) carrier_vec_dim_vec paw_def) + also have "... = dim_row apw" unfolding apw_def using outer_prod_dim assms + by (metis carrier_matD(1) carrier_vec_dim_vec index_minus_mat(2)) + finally show dr: "dim_row paw = dim_row apw" . + have cw: "dim_col paw = dim_vec w" unfolding paw_def using outer_prod_dim assms + using carrier_vec_dim_vec + by (metis carrier_matD(2) index_minus_vec(2) paw_def) + also have "... = dim_col apw" unfolding apw_def using outer_prod_dim + by (metis assms carrier_matD(2) carrier_vec_dim_vec index_minus_mat(3)) + finally show dc: "dim_col paw = dim_col apw" . + show "\i j. i < dim_row apw \ j < dim_col apw \ paw $$ (i, j) = apw $$ (i, j)" + proof - + fix i j + assume "i < dim_row apw" and "j < dim_col apw" note ij = this + hence "paw $$ (i,j) = Matrix.vec_index v i * + (cnj (Matrix.vec_index w j - (Matrix.vec_index x j)))" + using dr dc unfolding paw_def outer_prod_def by simp + also have "... = Matrix.vec_index v i * cnj (Matrix.vec_index w j) - + Matrix.vec_index v i * cnj (Matrix.vec_index x j)" + by (simp add: ring_class.ring_distribs) + also have "... = (outer_prod v w) $$ (i,j) - (outer_prod v x) $$ (i,j)" + using rv cw dr dc ij assms unfolding outer_prod_def by auto + also have "... = apw $$ (i,j)" using dr dc ij unfolding apw_def outer_prod_def by simp + finally show "paw $$ (i, j) = apw $$ (i, j)" . + qed + qed + thus ?thesis unfolding paw_def apw_def by simp +qed + +lemma outer_minus_minus: + fixes a::"complex Matrix.vec" + assumes "dim_vec a = dim_vec b" + and "dim_vec u = dim_vec v" + shows "outer_prod (a - b) (u - v) = outer_prod a u - outer_prod a v - + outer_prod b u + outer_prod b v" +proof - + have "outer_prod (a - b) (u - v) = outer_prod a (u - v) + - outer_prod b (u - v)" using outer_prod_minus_left assms by simp + also have "... = outer_prod a u - outer_prod a v - + outer_prod b (u - v)" using assms outer_prod_minus_right by simp + also have "... = outer_prod a u - outer_prod a v - + (outer_prod b u - outer_prod b v)" using assms outer_prod_minus_right by simp + also have "... = outer_prod a u - outer_prod a v - + outer_prod b u + outer_prod b v" + proof (rule mat_minus_minus) + show "outer_prod b u \ carrier_mat (dim_vec b) (dim_vec u)" by simp + show "outer_prod b v \ carrier_mat (dim_vec b) (dim_vec u)" using assms by simp + show "outer_prod a u - outer_prod a v \ carrier_mat (dim_vec b) (dim_vec u)" using assms + by (metis carrier_vecI minus_carrier_mat outer_prod_dim) + qed + finally show ?thesis . +qed + +lemma outer_trace_inner: + assumes "A \ carrier_mat n n" + and "dim_vec u = n" +and "dim_vec v = n" + shows "Complex_Matrix.trace (outer_prod u v * A) = Complex_Matrix.inner_prod v (A *\<^sub>v u)" +proof - + have "Complex_Matrix.trace (outer_prod u v * A) = Complex_Matrix.trace (A * outer_prod u v)" + proof (rule trace_comm) + show "A \ carrier_mat n n" using assms by simp + show "outer_prod u v \ carrier_mat n n" using assms + by (metis carrier_vec_dim_vec outer_prod_dim) + qed + also have "... = Complex_Matrix.inner_prod v (A *\<^sub>v u)" using trace_outer_prod_right[of A n u v] + assms carrier_vec_dim_vec by metis + finally show ?thesis . +qed + +lemma zero_hermitian: + shows "hermitian (0\<^sub>m n n)" unfolding hermitian_def + by (metis adjoint_minus hermitian_def hermitian_one minus_r_inv_mat one_carrier_mat) + +lemma trace_1: + shows "Complex_Matrix.trace ((1\<^sub>m n)::complex Matrix.mat) =(n::complex)" using one_mat_def + by (simp add: Complex_Matrix.trace_def Matrix.mat_def) + +lemma trace_add: + assumes "square_mat A" + and "square_mat B" + and "dim_row A = dim_row B" + shows "Complex_Matrix.trace (A + B) = Complex_Matrix.trace A + Complex_Matrix.trace B" + using assms by (simp add: Complex_Matrix.trace_def sum.distrib) + +lemma bra_vec_carrier: + shows "bra_vec v \ carrier_mat 1 (dim_vec v)" +proof - + have "dim_row (ket_vec v) = dim_vec v" unfolding ket_vec_def by simp + thus ?thesis using bra_bra_vec[of v] bra_def[of "ket_vec v"] by simp +qed + +lemma mat_mult_ket_carrier: + assumes "A\ carrier_mat n m" +shows "A * |v\ \ carrier_mat n 1" using assms + by (metis bra_bra_vec bra_vec_carrier carrier_matD(1) carrier_matI dagger_of_ket_is_bra + dim_row_of_dagger index_mult_mat(2) index_mult_mat(3)) + +lemma mat_mult_ket: + assumes "A \ carrier_mat n m" +and "dim_vec v = m" +shows "A * |v\ = |A *\<^sub>v v\" +proof - + have rn: "dim_row (A * |v\) = n" unfolding times_mat_def using assms by simp + have co: "dim_col |A *\<^sub>v v\ = 1" using assms unfolding ket_vec_def by simp + have cov: "dim_col |v\ = 1" using assms unfolding ket_vec_def by simp + have er: "dim_row (A * |v\) = dim_row |A *\<^sub>v v\" using assms + by (metis bra_bra_vec bra_vec_carrier carrier_matD(2) dagger_of_ket_is_bra dim_col_of_dagger + dim_mult_mat_vec index_mult_mat(2)) + have ec: "dim_col (A * |v\) = dim_col |A *\<^sub>v v\" using assms + by (metis carrier_matD(2) index_mult_mat(3) mat_mult_ket_carrier) + { + fix i::nat + fix j::nat + assume "i < n" + and "j < 1" + hence "j = 0" by simp + have "(A * |v\) $$ (i,0) = Matrix.scalar_prod (Matrix.row A i) (Matrix.col |v\ 0)" + using times_mat_def[of A] \i < n\ rn cov by simp + also have "... = Matrix.scalar_prod (Matrix.row A i) v" using ket_vec_col by simp + also have "... = |A *\<^sub>v v\ $$ (i,j)" unfolding mult_mat_vec_def + using \i < n\ \j = 0\ assms(1) by auto + } note idx = this + have "A * |v\ = Matrix.mat n 1 (\(i, j). Matrix.scalar_prod (Matrix.row A i) (Matrix.col |v\ j))" + using assms unfolding times_mat_def ket_vec_def by simp + also have "... = |A *\<^sub>v v\" using er ec idx rn co by auto + finally show ?thesis . +qed + +lemma unitary_density: + assumes "density_operator R" + and "unitary U" + and "R\ carrier_mat n n" + and "U\ carrier_mat n n" +shows "density_operator (U * R * (Complex_Matrix.adjoint U))" unfolding density_operator_def +proof (intro conjI) + show "Complex_Matrix.positive (U * R * Complex_Matrix.adjoint U)" + proof (rule positive_close_under_left_right_mult_adjoint) + show "U \ carrier_mat n n" using assms by simp + show "R \ carrier_mat n n" using assms by simp + show "Complex_Matrix.positive R" using assms unfolding density_operator_def by simp + qed + have "Complex_Matrix.trace (U * R * Complex_Matrix.adjoint U) = + Complex_Matrix.trace (Complex_Matrix.adjoint U * U * R)" + using trace_comm[of "U * R" n "Complex_Matrix.adjoint U"] assms + by (metis adjoint_dim mat_assoc_test(10)) + also have "... = Complex_Matrix.trace R" using assms by simp + also have "... = 1" using assms unfolding density_operator_def by simp + finally show "Complex_Matrix.trace (U * R * Complex_Matrix.adjoint U) = 1" . +qed + + +subsection \Tensor product complements\ + +lemma tensor_vec_dim[simp]: + shows "dim_vec (tensor_vec u v) = dim_vec u * (dim_vec v)" +proof - + have "length (mult.vec_vec_Tensor (*) (list_of_vec u) (list_of_vec v)) = + length (list_of_vec u) * length (list_of_vec v)" + using mult.vec_vec_Tensor_length[of "1::real" "(*)" "list_of_vec u" "list_of_vec v"] + by (simp add: Matrix_Tensor.mult_def) + thus ?thesis unfolding tensor_vec_def by simp +qed + +lemma index_tensor_vec[simp]: + assumes "0 < dim_vec v" + and "i < dim_vec u * dim_vec v" +shows "vec_index (tensor_vec u v) i = + vec_index u (i div (dim_vec v)) * vec_index v (i mod dim_vec v)" +proof - + have m: "Matrix_Tensor.mult (1::complex) (*)" by (simp add: Matrix_Tensor.mult_def) + have "length (list_of_vec v) = dim_vec v" using assms by simp + hence "vec_index (tensor_vec u v) i = (*) (vec_index u (i div dim_vec v)) (vec_index v (i mod dim_vec v))" + unfolding tensor_vec_def using mult.vec_vec_Tensor_elements assms m + by (metis (mono_tags, lifting) length_greater_0_conv length_list_of_vec list_of_vec_index + mult.vec_vec_Tensor_elements vec_of_list_index) + thus ?thesis by simp +qed + +lemma outer_prod_tensor_comm: + fixes a::"complex Matrix.vec" + fixes u::"complex Matrix.vec" + assumes "0 < dim_vec a" + and "0 < dim_vec b" +shows "outer_prod (tensor_vec u v) (tensor_vec a b) = tensor_mat (outer_prod u a) (outer_prod v b)" +proof - + define ot where "ot = outer_prod (tensor_vec u v) (tensor_vec a b)" + define to where "to = tensor_mat (outer_prod u a) (outer_prod v b)" + define dv where "dv = dim_vec v" + define db where "db = dim_vec b" + have "ot = to" + proof + have ro: "dim_row ot = dim_vec u * dim_vec v" unfolding ot_def outer_prod_def by simp + have "dim_row to = dim_row (outer_prod u a) * dim_row (outer_prod v b)" + unfolding to_def by simp + also have "... = dim_vec u * dim_vec v" using outer_prod_dim + by (metis carrier_matD(1) carrier_vec_dim_vec) + finally have rt: "dim_row to = dim_vec u * dim_vec v" . + show "dim_row ot = dim_row to" using ro rt by simp + have co: "dim_col ot = dim_vec a * dim_vec b" unfolding ot_def outer_prod_def by simp + have "dim_col to = dim_col (outer_prod u a) * dim_col (outer_prod v b)" unfolding to_def by simp + also have "... = dim_vec a * dim_vec b" using outer_prod_dim + by (metis carrier_matD(2) carrier_vec_dim_vec) + finally have ct: "dim_col to = dim_vec a * dim_vec b" . + show "dim_col ot = dim_col to" using co ct by simp + show "\i j. i < dim_row to \ j < dim_col to \ ot $$ (i, j) = to $$ (i, j)" + proof - + fix i j + assume "i < dim_row to" and "j < dim_col to" note ij = this + have "ot $$ (i,j) = Matrix.vec_index (tensor_vec u v) i * + (conjugate (Matrix.vec_index (tensor_vec a b) j))" + unfolding ot_def outer_prod_def using ij rt ct by simp + also have "... = vec_index u (i div dv) * vec_index v (i mod dv) * + (conjugate (Matrix.vec_index (tensor_vec a b) j))" using ij rt assms + unfolding dv_def + by (metis index_tensor_vec less_nat_zero_code nat_0_less_mult_iff neq0_conv) + also have "... = vec_index u (i div dv) * vec_index v (i mod dv) * + (conjugate (vec_index a (j div db) * vec_index b (j mod db)))" using ij ct assms + unfolding db_def by simp + also have "... = vec_index u (i div dv) * vec_index v (i mod dv) * + (conjugate (vec_index a (j div db))) * (conjugate (vec_index b (j mod db)))" by simp + also have "... = vec_index u (i div dv) * (conjugate (vec_index a (j div db))) * + vec_index v (i mod dv) * (conjugate (vec_index b (j mod db)))" by simp + also have "... = (outer_prod u a) $$ (i div dv, j div db) * + vec_index v (i mod dv) * (conjugate (vec_index b (j mod db)))" + proof - + have "i div dv < dim_vec u" using ij rt unfolding dv_def + by (simp add: less_mult_imp_div_less) + moreover have "j div db < dim_vec a" using ij ct assms unfolding db_def + by (simp add: less_mult_imp_div_less) + ultimately have "vec_index u (i div dv) * (conjugate (vec_index a (j div db))) = + (outer_prod u a) $$ (i div dv, j div db)" unfolding outer_prod_def by simp + thus ?thesis by simp + qed + also have "... = (outer_prod u a) $$ (i div dv, j div db) * + (outer_prod v b) $$ (i mod dv, j mod db)" + proof - + have "i mod dv < dim_vec v" using ij rt unfolding dv_def + using assms mod_less_divisor + by (metis less_nat_zero_code mult.commute neq0_conv times_nat.simps(1)) + moreover have "j mod db < dim_vec b" using ij ct assms unfolding db_def + by (simp add: less_mult_imp_div_less) + ultimately have "vec_index v (i mod dv) * (conjugate (vec_index b (j mod db))) = + (outer_prod v b) $$ (i mod dv, j mod db)" unfolding outer_prod_def by simp + thus ?thesis by simp + qed + also have "... = tensor_mat (outer_prod u a) (outer_prod v b) $$ (i, j)" + proof (rule index_tensor_mat[symmetric]) + show "dim_row (outer_prod u a) = dim_vec u" unfolding outer_prod_def by simp + show "dim_row (outer_prod v b) = dv" unfolding outer_prod_def dv_def by simp + show "dim_col (outer_prod v b) = db" unfolding db_def outer_prod_def by simp + show "i < dim_vec u * dv" unfolding dv_def using ij rt by simp + show "dim_col (outer_prod u a) = dim_vec a" unfolding outer_prod_def by simp + show "j < dim_vec a * db" unfolding db_def using ij ct by simp + show "0 < dim_vec a" using assms by simp + show "0 < db" unfolding db_def using assms by simp + qed + finally show "ot $$ (i, j) = to $$ (i, j)" unfolding to_def . + qed + qed + thus ?thesis unfolding ot_def to_def by simp +qed + +lemma tensor_mat_adjoint: + assumes "m1 \ carrier_mat r1 c1" + and "m2 \ carrier_mat r2 c2" + and "0 < c1" + and "0 < c2" +and "0 < r1" +and "0 < r2" + shows "Complex_Matrix.adjoint (tensor_mat m1 m2) = + tensor_mat (Complex_Matrix.adjoint m1) (Complex_Matrix.adjoint m2)" + apply (rule eq_matI, auto) +proof - + fix i j + assume "i < dim_col m1 * dim_col m2" and "j < dim_row m1 * dim_row m2" note ij = this + have c1: "dim_col m1 = c1" using assms by simp + have r1: "dim_row m1 = r1" using assms by simp + have c2: "dim_col m2 = c2" using assms by simp + have r2: "dim_row m2 = r2" using assms by simp + have "Complex_Matrix.adjoint (m1 \ m2) $$ (i, j) = conjugate ((m1 \ m2) $$ (j, i))" + using ij by (simp add: adjoint_eval) + also have "... = conjugate (m1 $$ (j div r2, i div c2) * m2 $$ (j mod r2, i mod c2))" + proof - + have "(m1 \ m2) $$ (j, i) = m1 $$ (j div r2, i div c2) * m2 $$ (j mod r2, i mod c2)" + proof (rule index_tensor_mat[of m1 r1 c1 m2 r2 c2 j i], (auto simp add: assms ij c1 c2 r1 r2)) + show "j < r1 * r2" using ij r1 r2 by simp + show "i < c1 * c2" using ij c1 c2 by simp + qed + thus ?thesis by simp + qed + also have "... = conjugate (m1 $$ (j div r2, i div c2)) * conjugate ( m2 $$ (j mod r2, i mod c2))" + by simp + also have "... = (Complex_Matrix.adjoint m1) $$ (i div c2, j div r2) * + conjugate ( m2 $$ (j mod r2, i mod c2))" + by (metis adjoint_eval c2 ij less_mult_imp_div_less r2) + also have "... = (Complex_Matrix.adjoint m1) $$ (i div c2, j div r2) * + (Complex_Matrix.adjoint m2) $$ (i mod c2, j mod r2)" + by (metis Euclidean_Division.div_eq_0_iff adjoint_eval assms(4) bits_mod_div_trivial c2 + gr_implies_not_zero ij(2) mult_not_zero r2) + also have "... = (tensor_mat (Complex_Matrix.adjoint m1) (Complex_Matrix.adjoint m2)) $$ (i,j)" + proof (rule index_tensor_mat[symmetric], (simp add: ij c1 c2 r1 r2) +) + show "i < c1 * c2" using ij c1 c2 by simp + show "j < r1 * r2" using ij r1 r2 by simp + show "0 < r1" using assms by simp + show "0 < r2" using assms by simp + qed + finally show "Complex_Matrix.adjoint (m1 \ m2) $$ (i, j) = + (Complex_Matrix.adjoint m1 \ Complex_Matrix.adjoint m2) $$ (i, j)" . +qed + +lemma index_tensor_mat': + assumes "0 < dim_col A" + and "0 < dim_col B" + and "i < dim_row A * dim_row B" + and "j < dim_col A * dim_col B" + shows "(A \ B) $$ (i, j) = + A $$ (i div (dim_row B), j div (dim_col B)) * B $$ (i mod (dim_row B), j mod (dim_col B))" + by (rule index_tensor_mat, (simp add: assms)+) + +lemma tensor_mat_carrier: + shows "tensor_mat U V \ carrier_mat (dim_row U * dim_row V) (dim_col U * dim_col V)" by auto + +lemma tensor_mat_id: + assumes "0 < d1" + and "0 < d2" +shows "tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) = 1\<^sub>m (d1 * d2)" +proof (rule eq_matI, auto) + show "tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) $$ (i, i) = 1" if "i < (d1 * d2)" for i + using that index_tensor_mat'[of "1\<^sub>m d1" "1\<^sub>m d2"] + by (simp add: assms less_mult_imp_div_less) +next + show "tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) $$ (i, j) = 0" if "i < d1 * d2" "j < d1 * d2" "i \ j" for i j + using that index_tensor_mat[of "1\<^sub>m d1" d1 d1 "1\<^sub>m d2" d2 d2 i j] + by (metis assms(1) assms(2) index_one_mat(1) index_one_mat(2) index_one_mat(3) + less_mult_imp_div_less mod_less_divisor mult_div_mod_eq mult_not_zero) +qed + +lemma tensor_mat_hermitian: + assumes "A \ carrier_mat n n" + and "B \ carrier_mat n' n'" + and "0 < n" + and "0 < n'" + and "hermitian A" + and "hermitian B" + shows "hermitian (tensor_mat A B)" using assms by (metis hermitian_def tensor_mat_adjoint) + +lemma tensor_mat_unitary: + assumes "Complex_Matrix.unitary U" + and "Complex_Matrix.unitary V" +and "0 < dim_row U" +and "0 < dim_row V" +shows "Complex_Matrix.unitary (tensor_mat U V)" +proof - + define UI where "UI = tensor_mat U V" + have "Complex_Matrix.adjoint UI = + tensor_mat (Complex_Matrix.adjoint U) (Complex_Matrix.adjoint V)" unfolding UI_def + proof (rule tensor_mat_adjoint) + show "U \ carrier_mat (dim_row U) (dim_row U)" using assms unfolding Complex_Matrix.unitary_def + by simp + show "V \ carrier_mat (dim_row V) (dim_row V)" using assms unfolding Complex_Matrix.unitary_def + by simp + show "0 < dim_row V" using assms by simp + show "0 < dim_row U" using assms by simp + show "0 < dim_row V" using assms by simp + show "0 < dim_row U" using assms by simp + qed + hence "UI * (Complex_Matrix.adjoint UI) = + tensor_mat (U * Complex_Matrix.adjoint U) (V * Complex_Matrix.adjoint V)" + using mult_distr_tensor[of U "Complex_Matrix.adjoint U" "V" "Complex_Matrix.adjoint V"] + unfolding UI_def + by (metis (no_types, lifting) Complex_Matrix.unitary_def adjoint_dim_col adjoint_dim_row + assms carrier_matD(2) ) + also have "... = tensor_mat (1\<^sub>m (dim_row U)) (1\<^sub>m (dim_row V))" using assms unitary_simps(2) + by (metis Complex_Matrix.unitary_def) + also have "... = (1\<^sub>m (dim_row U * dim_row V))" using tensor_mat_id assms by simp + finally have "UI * (Complex_Matrix.adjoint UI) = (1\<^sub>m (dim_row U * dim_row V))" . + hence "inverts_mat UI (Complex_Matrix.adjoint UI)" unfolding inverts_mat_def UI_def by simp + thus ?thesis using assms unfolding Complex_Matrix.unitary_def UI_def + by (metis carrier_matD(2) carrier_matI dim_col_tensor_mat dim_row_tensor_mat) +qed + + +subsection \Fixed carrier matrices locale\ + +text \We define a locale for matrices with a fixed number of rows and columns, and define a +finite sum operation on this locale. The \verb+Type_To_Sets+ transfer tools then permits to obtain +lemmata on the locale for free. \ + +locale fixed_carrier_mat = + fixes fc_mats::"'a::field Matrix.mat set" + fixes dimR dimC + assumes fc_mats_carrier: "fc_mats = carrier_mat dimR dimC" +begin + +sublocale semigroup_add_on_with fc_mats "(+)" +proof (unfold_locales) + show "\a b. a \ fc_mats \ b \ fc_mats \ a + b \ fc_mats" using fc_mats_carrier by simp + show "\a b c. a \ fc_mats \ b \ fc_mats \ c \ fc_mats \ a + b + c = a + (b + c)" + using fc_mats_carrier by simp +qed + +sublocale ab_semigroup_add_on_with fc_mats "(+)" +proof (unfold_locales) + show "\a b. a \ fc_mats \ b \ fc_mats \ a + b = b + a" using fc_mats_carrier + by (simp add: comm_add_mat) +qed + +sublocale comm_monoid_add_on_with fc_mats "(+)" "0\<^sub>m dimR dimC" +proof (unfold_locales) + show "0\<^sub>m dimR dimC \ fc_mats" using fc_mats_carrier by simp + show "\a. a \ fc_mats \ 0\<^sub>m dimR dimC + a = a" using fc_mats_carrier by simp +qed + +sublocale ab_group_add_on_with fc_mats "(+)" "0\<^sub>m dimR dimC" "(-)" "uminus" +proof (unfold_locales) + show "\a. a \ fc_mats \ - a + a = 0\<^sub>m dimR dimC" using fc_mats_carrier by simp + show "\a b. a \ fc_mats \ b \ fc_mats \ a - b = a + - b" using fc_mats_carrier + by (simp add: add_uminus_minus_mat) + show "\a. a \ fc_mats \ - a \ fc_mats" using fc_mats_carrier by simp +qed +end + +lemma (in fixed_carrier_mat) smult_mem: + assumes "A \ fc_mats" + shows "a \\<^sub>m A \ fc_mats" using fc_mats_carrier assms by auto + +definition (in fixed_carrier_mat) sum_mat where +"sum_mat A I = sum_with (+) (0\<^sub>m dimR dimC) A I" + +lemma (in fixed_carrier_mat) sum_mat_empty[simp]: + shows "sum_mat A {} = 0\<^sub>m dimR dimC" unfolding sum_mat_def by simp + +lemma (in fixed_carrier_mat) sum_mat_carrier: + shows "(\i. i \ I \ (A i)\ fc_mats) \ sum_mat A I \ carrier_mat dimR dimC" + unfolding sum_mat_def using sum_with_mem[of A I] fc_mats_carrier by auto + +lemma (in fixed_carrier_mat) sum_mat_insert: + assumes "A x \ fc_mats" "A ` I \ fc_mats" + and A: "finite I" and x: "x \ I" + shows "sum_mat A (insert x I) = A x + sum_mat A I" unfolding sum_mat_def + using assms sum_with_insert[of A x I] by simp + + +subsection \A locale for square matrices\ + +locale cpx_sq_mat = fixed_carrier_mat "fc_mats::complex Matrix.mat set" for fc_mats + + assumes dim_eq: "dimR = dimC" + and npos: "0 < dimR" + +lemma (in cpx_sq_mat) one_mem: + shows "1\<^sub>m dimR \ fc_mats" using fc_mats_carrier dim_eq by simp + +lemma (in cpx_sq_mat) square_mats: + assumes "A \ fc_mats" + shows "square_mat A" using fc_mats_carrier dim_eq assms by simp + +lemma (in cpx_sq_mat) cpx_sq_mat_mult: + assumes "A \ fc_mats" + and "B \ fc_mats" +shows "A * B \ fc_mats" +proof - + have "dim_row (A * B) = dimR" using assms fc_mats_carrier by simp + moreover have "dim_col (A * B) = dimR" using assms fc_mats_carrier dim_eq by simp + ultimately show ?thesis using fc_mats_carrier carrier_mat_def dim_eq by auto +qed + +lemma (in cpx_sq_mat) sum_mat_distrib_left: + shows "finite I \ R\ fc_mats \ (\i. i \ I \ (A i)\ fc_mats) \ + sum_mat (\i. R * (A i)) I = R * (sum_mat A I)" +proof (induct rule: finite_induct) + case empty + hence a: "sum_mat (\i. R * (A i)) {} = 0\<^sub>m dimR dimC" unfolding sum_mat_def by simp + have "sum_mat A {} = 0\<^sub>m dimR dimC" unfolding sum_mat_def by simp + hence "R * (sum_mat A {}) = 0\<^sub>m dimR dimC" using fc_mats_carrier + right_mult_zero_mat[of R dimR dimC dimC] empty dim_eq by simp + thus ?case using a by simp +next + case (insert x F) + hence "sum_mat (\i. R * A i) (insert x F) = R * (A x) + sum_mat (\i. R * A i) F" + using sum_mat_insert[of "\i. R * A i" x F] by (simp add: image_subsetI fc_mats_carrier dim_eq) + also have "... = R * (A x) + R * (sum_mat A F)" using insert by simp + also have "... = R * (A x + (sum_mat A F))" + by (metis dim_eq fc_mats_carrier insert.prems(1) insert.prems(2) insertCI mult_add_distrib_mat + sum_mat_carrier) + also have "... = R * sum_mat A (insert x F)" + proof - + have "A x + (sum_mat A F) = sum_mat A (insert x F)" + by (rule sum_mat_insert[symmetric], (auto simp add: insert)) + thus ?thesis by simp + qed + finally show ?case . +qed + +lemma (in cpx_sq_mat) sum_mat_distrib_right: + shows "finite I \ R\ fc_mats \ (\i. i \ I \ (A i)\ fc_mats) \ + sum_mat (\i. (A i) * R) I = (sum_mat A I) * R" +proof (induct rule: finite_induct) + case empty + hence a: "sum_mat (\i. (A i) * R) {} = 0\<^sub>m dimR dimC" unfolding sum_mat_def by simp + have "sum_mat A {} = 0\<^sub>m dimR dimC" unfolding sum_mat_def by simp + hence "(sum_mat A {}) * R = 0\<^sub>m dimR dimC" using fc_mats_carrier right_mult_zero_mat[of R ] + dim_eq empty by simp + thus ?case using a by simp +next + case (insert x F) + have a: "(\i. A i * R) ` F \ fc_mats" using insert cpx_sq_mat_mult + by (simp add: image_subsetI) + have "A x * R \ fc_mats" using insert + by (metis insertI1 local.fc_mats_carrier mult_carrier_mat dim_eq) + hence "sum_mat (\i. A i * R) (insert x F) = (A x) * R + sum_mat (\i. A i * R) F" using insert a + using sum_mat_insert[of "\i. A i * R" x F] by (simp add: image_subsetI local.fc_mats_carrier) + also have "... = (A x) * R + (sum_mat A F) * R" using insert by simp + also have "... = (A x + (sum_mat A F)) * R" + proof (rule add_mult_distrib_mat[symmetric]) + 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 fc_mats_carrier sum_mat_carrier by blast + show "R \ carrier_mat dimC dimC" using insert fc_mats_carrier dim_eq by simp + qed + also have "... = sum_mat A (insert x F) * R" + proof - + have "A x + (sum_mat A F) = sum_mat A (insert x F)" + by (rule sum_mat_insert[symmetric], (auto simp add: insert)) + thus ?thesis by simp + qed + finally show ?case . +qed + +lemma (in cpx_sq_mat) trace_sum_mat: + fixes A::"'b \ complex Matrix.mat" + shows "finite I \ (\i. i \ I \ (A i)\ fc_mats) \ + Complex_Matrix.trace (sum_mat A I) = (\ i\ I. Complex_Matrix.trace (A i))" unfolding sum_mat_def +proof (induct rule: finite_induct) + case empty + then show ?case using trace_zero dim_eq by simp +next + case (insert x F) + have "Complex_Matrix.trace (sum_with (+) (0\<^sub>m dimR dimC) A (insert x F)) = + Complex_Matrix.trace (A x + sum_with (+) (0\<^sub>m dimR dimC) A F)" + using sum_with_insert[of A x F] insert by (simp add: image_subset_iff dim_eq) + also have "... = Complex_Matrix.trace (A x) + + Complex_Matrix.trace (sum_with (+) (0\<^sub>m dimR dimC) A F)" using trace_add square_mats insert + by (metis carrier_matD(1) fc_mats_carrier image_subset_iff insert_iff sum_with_mem) + also have "... = Complex_Matrix.trace (A x) + (\ i\ F. Complex_Matrix.trace (A i))" + using insert by simp + also have "... = (\ i\ (insert x F). Complex_Matrix.trace (A i))" + using sum_with_insert[of A x F] insert by (simp add: image_subset_iff) + finally show ?case . +qed + +lemma (in cpx_sq_mat) cpx_sq_mat_smult: + assumes "A \ fc_mats" + shows "x \\<^sub>m A \ fc_mats" + using assms fc_mats_carrier by auto + +lemma (in cpx_sq_mat) mult_add_distrib_right: + assumes "A\ fc_mats" "B\ fc_mats" "C\ fc_mats" + shows "A * (B + C) = A * B + A * C" + using assms fc_mats_carrier mult_add_distrib_mat dim_eq by simp + +lemma (in cpx_sq_mat) mult_add_distrib_left: + assumes "A\ fc_mats" "B\ fc_mats" "C\ fc_mats" + shows "(B + C) * A = B * A + C * A" + using assms fc_mats_carrier add_mult_distrib_mat dim_eq by simp + +lemma (in cpx_sq_mat) mult_sum_mat_distrib_left: + shows "finite I \ (\i. i \ I \ (A i)\ fc_mats) \ B \ fc_mats \ + (sum_mat (\i. B * (A i)) I) = B * (sum_mat A I)" +proof (induct rule: finite_induct) + case empty + hence "sum_mat A {} = 0\<^sub>m dimR dimC" using sum_mat_empty by simp + hence "B * (sum_mat A {}) = 0\<^sub>m dimR dimC" using empty by (simp add: fc_mats_carrier dim_eq) + moreover have "sum_mat (\i. B * (A i)) {} = 0\<^sub>m dimR dimC" using sum_mat_empty[of "\i. B * (A i)"] + by simp + ultimately show ?case by simp +next + case (insert x F) + have "sum_mat (\i. B * (A i)) (insert x F) = B * (A x) + sum_mat (\i. B * (A i)) F" + using sum_with_insert[of "\i. B * (A i)" x F] insert + by (simp add: image_subset_iff local.sum_mat_def cpx_sq_mat_mult) + also have "... = B * (A x) + B * (sum_mat A F)" using insert by simp + also have "... = B * (A x + (sum_mat A F))" + proof (rule mult_add_distrib_right[symmetric]) + show "B\ fc_mats" using insert by simp + show "A x \ fc_mats" using insert by simp + show "sum_mat A F \ fc_mats" using insert by (simp add: fc_mats_carrier sum_mat_carrier) + qed + also have "... = B * (sum_mat A (insert x F))" using sum_with_insert[of A x F] insert + by (simp add: image_subset_iff sum_mat_def) + finally show ?case . +qed + +lemma (in cpx_sq_mat) mult_sum_mat_distrib_right: + shows "finite I \ (\i. i \ I \ (A i)\ fc_mats) \ B \ fc_mats \ + (sum_mat (\i. (A i) * B) I) = (sum_mat A I) * B" +proof (induct rule: finite_induct) + case empty + hence "sum_mat A {} = 0\<^sub>m dimR dimC" using sum_mat_empty by simp + hence "(sum_mat A {}) * B = 0\<^sub>m dimR dimC" using empty by (simp add: fc_mats_carrier dim_eq) + moreover have "sum_mat (\i. (A i) * B) {} = 0\<^sub>m dimR dimC" by simp + ultimately show ?case by simp +next + case (insert x F) + have "sum_mat (\i. (A i) * B) (insert x F) = (A x) * B + sum_mat (\i. (A i) * B) F" + using sum_with_insert[of "\i. (A i) * B" x F] insert + by (simp add: image_subset_iff local.sum_mat_def cpx_sq_mat_mult) + also have "... = (A x) * B + (sum_mat A F) * B" using insert by simp + also have "... = (A x + (sum_mat A F)) * B" + proof (rule mult_add_distrib_left[symmetric]) + show "B\ fc_mats" using insert by simp + show "A x \ fc_mats" using insert by simp + show "sum_mat A F \ fc_mats" using insert by (simp add: fc_mats_carrier sum_mat_carrier) + qed + also have "... = (sum_mat A (insert x F)) * B" using sum_with_insert[of A x F] insert + by (simp add: image_subset_iff sum_mat_def) + finally show ?case . +qed + +lemma (in cpx_sq_mat) trace_sum_mat_mat_distrib: + assumes "finite I" +and "\i. i\ I \ B i \ fc_mats" +and "A\ fc_mats" +and "C \ fc_mats" +shows "(\ i\ I. Complex_Matrix.trace(A * (B i) * C)) = + Complex_Matrix.trace (A * (sum_mat B I) * C)" +proof - + have seq: "sum_mat (\i. A * (B i) * C) I = A * (sum_mat B I) * C" + proof - + have "sum_mat (\i. A * (B i) * C) I = (sum_mat (\i. A * (B i)) I) * C" + proof (rule mult_sum_mat_distrib_right) + show "finite I" using assms by simp + show "C\ fc_mats" using assms by simp + show "\i. i \ I \ A * B i \ fc_mats" using assms cpx_sq_mat_mult by simp + qed + moreover have "sum_mat (\i. A * (B i)) I = A * (sum_mat B I)" + by (rule mult_sum_mat_distrib_left, (auto simp add: assms)) + ultimately show "sum_mat (\i. A * (B i) * C) I = A * (sum_mat B I) * C" by simp + qed + have "(\ i\ I. Complex_Matrix.trace(A * (B i) * C)) = + Complex_Matrix.trace (sum_mat (\i. A * (B i) * C) I)" + proof (rule trace_sum_mat[symmetric]) + show "finite I" using assms by simp + fix i + assume "i\ I" + thus "A * B i * C \ fc_mats" using assms by (simp add: cpx_sq_mat_mult) + qed + also have "... = Complex_Matrix.trace (A * (sum_mat B I) * C)" using seq by simp + finally show ?thesis . +qed + +definition (in cpx_sq_mat) zero_col where +"zero_col U = (\i. if i < dimR then Matrix.col U i else 0\<^sub>v dimR)" + +lemma (in cpx_sq_mat) zero_col_dim: + assumes "U \ fc_mats" + shows "dim_vec (zero_col U i) = dimR" using assms fc_mats_carrier unfolding zero_col_def by simp + +lemma (in cpx_sq_mat) zero_col_col: + assumes "i < dimR" + shows "zero_col U i = Matrix.col U i" using assms unfolding zero_col_def by simp + +lemma (in cpx_sq_mat) sum_mat_index: + shows "finite I \ (\i. i \ I \ (A i)\ fc_mats) \ i < dimR \ j < dimC \ + (sum_mat (\k. (A k)) I) $$ (i,j) = (\ k\I. (A k) $$ (i,j))" +proof (induct rule: finite_induct) + case empty + thus ?case unfolding sum_mat_def by simp +next + case (insert x F) + hence "(sum_mat (\k. (A k)) (insert x F)) $$ (i,j) = + (A x + (sum_mat (\k. (A k)) F)) $$ (i,j)" using insert sum_mat_insert[of A] + by (simp add: image_subsetI local.fc_mats_carrier) + also have "... = (A x) $$ (i,j) + (sum_mat (\k. (A k)) F) $$ (i,j)" using insert + sum_mat_carrier[of F A] fc_mats_carrier by simp + also have "... = (A x) $$ (i,j) + (\ k\F. (A k) $$ (i,j))" using insert by simp + also have "... = (\ k\(insert x F). (A k) $$ (i,j))" using insert by simp + finally show ?case . +qed + +lemma (in cpx_sq_mat) sum_mat_cong: + shows "finite I \ (\i. i\ I \ A i = B i) \ (\i. i\ I \ A i \ fc_mats) \ + (\i. i\ I \ B i \ fc_mats) \ sum_mat A I = sum_mat B I" +proof (induct rule: finite_induct) + case empty + then show ?case by simp +next + case (insert x F) + have "sum_mat A (insert x F) = A x + sum_mat A F" using insert sum_mat_insert[of A] + by (simp add: image_subset_iff) + also have "... = B x + sum_mat B F" using insert by simp + also have "... = sum_mat B (insert x F)" using insert sum_mat_insert[of B] + by (simp add: image_subset_iff) + finally show ?case . +qed + +lemma (in cpx_sq_mat) smult_sum_mat: + shows "finite I \ (\i. i\ I \ A i \ fc_mats) \ a \\<^sub>m sum_mat A I = sum_mat (\i. a \\<^sub>m (A i)) I" +proof (induct rule: finite_induct) + case empty + then show ?case by simp +next + case (insert x F) + have "a \\<^sub>m sum_mat A (insert x F) = a \\<^sub>m (A x + sum_mat A F)" using insert sum_mat_insert[of A] + by (simp add: image_subset_iff) + also have "... = a \\<^sub>m A x + a \\<^sub>m (sum_mat A F)" using insert + by (metis add_smult_distrib_left_mat fc_mats_carrier insert_iff sum_mat_carrier) + also have "... = a \\<^sub>m A x + sum_mat (\i. a \\<^sub>m (A i)) F" using insert by simp + also have "... = sum_mat (\i. a \\<^sub>m (A i)) (insert x F)" using insert + sum_mat_insert[of "(\i. a \\<^sub>m (A i))"] by (simp add: image_subset_iff cpx_sq_mat_smult) + finally show ?case . +qed + +lemma (in cpx_sq_mat) zero_sum_mat: + shows "finite I \ sum_mat (\i. ((0\<^sub>m dimR dimR)::complex Matrix.mat)) I = ((0\<^sub>m dimR dimR)::complex Matrix.mat)" +proof (induct rule:finite_induct) + case empty + then show ?case using dim_eq sum_mat_empty by auto +next + case (insert x F) + have "sum_mat (\i. ((0\<^sub>m dimR dimR)::complex Matrix.mat)) (insert x F) = + 0\<^sub>m dimR dimR + sum_mat (\i. 0\<^sub>m dimR dimR) F" + using insert dim_eq zero_mem sum_mat_insert[of "\i. ((0\<^sub>m dimR dimR)::complex Matrix.mat)"] + by fastforce + also have "... = ((0\<^sub>m dimR dimR)::complex Matrix.mat)" using insert by auto + finally show ?case . +qed + +lemma (in cpx_sq_mat) sum_mat_adjoint: + shows "finite I \ (\i. i\ I \ A i \ fc_mats) \ + Complex_Matrix.adjoint (sum_mat A I) = sum_mat (\i. Complex_Matrix.adjoint (A i)) I" +proof (induct rule: finite_induct) + case empty + then show ?case using zero_hermitian[of dimR] + by (metis (no_types) dim_eq hermitian_def sum_mat_empty) +next + case (insert x F) + have "Complex_Matrix.adjoint (sum_mat A (insert x F)) = + Complex_Matrix.adjoint (A x + sum_mat A F)" using insert sum_mat_insert[of A] + by (simp add: image_subset_iff) + also have "... = Complex_Matrix.adjoint (A x) + Complex_Matrix.adjoint (sum_mat A F)" + proof (rule adjoint_add) + 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 fc_mats_carrier sum_mat_carrier[of F] + by simp + qed + also have "... = Complex_Matrix.adjoint (A x) + sum_mat (\i. Complex_Matrix.adjoint (A i)) F" + using insert by simp + also have "... = sum_mat (\i. Complex_Matrix.adjoint (A i)) (insert x F)" + proof (rule sum_mat_insert[symmetric], (auto simp add: insert)) + show "Complex_Matrix.adjoint (A x) \ fc_mats" using insert fc_mats_carrier dim_eq + by (simp add: adjoint_dim) + show "\i. i \ F \ Complex_Matrix.adjoint (A i) \ fc_mats" using insert fc_mats_carrier dim_eq + by (simp add: adjoint_dim) + qed + finally show ?case . +qed + +lemma (in cpx_sq_mat) sum_mat_hermitian: + assumes "finite I" +and "\i\ I. hermitian (A i)" +and "\i\ I. A i\ fc_mats" +shows "hermitian (sum_mat A I)" +proof - + have "Complex_Matrix.adjoint (sum_mat A I) = sum_mat (\i. Complex_Matrix.adjoint (A i)) I" + using assms sum_mat_adjoint[of I] by simp + also have "... = sum_mat A I" + proof (rule sum_mat_cong, (auto simp add: assms)) + show "\i. i \ I \ Complex_Matrix.adjoint (A i) = A i" using assms + unfolding hermitian_def by simp + show "\i. i \ I \ Complex_Matrix.adjoint (A i) \ fc_mats" using assms fc_mats_carrier dim_eq + by (simp add: adjoint_dim) + qed + finally show ?thesis unfolding hermitian_def . +qed + +lemma (in cpx_sq_mat) sum_mat_positive: +shows "finite I \ (\i. i\ I \ Complex_Matrix.positive (A i)) \ + (\i. i \ I \ A i \ fc_mats) \ Complex_Matrix.positive (sum_mat A I)" +proof (induct rule: finite_induct) + case empty + then show ?case using positive_zero[of dimR] by (metis (no_types) dim_eq sum_mat_empty) +next + case (insert x F) + hence "sum_mat A (insert x F) = A x + (sum_mat A F)" using sum_mat_insert[of A] + by (simp add: image_subset_iff) + moreover have "Complex_Matrix.positive (A x + (sum_mat A F))" + proof (rule positive_add, (auto simp add: insert)) + show "A x \ carrier_mat dimR dimR" using insert fc_mats_carrier dim_eq by simp + show "sum_mat A F \ carrier_mat dimR dimR" using insert sum_mat_carrier dim_eq + by (metis insertCI) + qed + ultimately show "Complex_Matrix.positive (sum_mat A (insert x F))" by simp +qed + +lemma (in cpx_sq_mat) sum_mat_left_ortho_zero: + shows "finite I \ + (\i. i\ I \ A i \ fc_mats) \ (B \ fc_mats) \ + (\ i. i\ I \ A i * B = (0\<^sub>m dimR dimR)) \ + (sum_mat A I) * B = 0\<^sub>m dimR dimR" +proof (induct rule:finite_induct) + case empty + then show ?case using dim_eq + by (metis finite.intros(1) sum_mat_empty mult_sum_mat_distrib_right) +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 dimR" using insert fc_mats_carrier dim_eq by simp + qed + also have "... = A x * B + (0\<^sub>m dimR dimR)" using insert by simp + also have "... = 0\<^sub>m dimR dimR" using insert by simp + finally show ?case . +qed + +lemma (in cpx_sq_mat) sum_mat_right_ortho_zero: + shows "finite I \ + (\i. i\ I \ A i \ fc_mats) \ (B \ fc_mats) \ + (\ i. i\ I \ B * A i = (0\<^sub>m dimR dimR)) \ + B * (sum_mat A I) = 0\<^sub>m dimR dimR" +proof (induct rule:finite_induct) + case empty + then show ?case using dim_eq + by (metis finite.intros(1) sum_mat_empty mult_sum_mat_distrib_left) +next + case (insert x F) + have "B * (sum_mat A (insert x F)) = + B * (A x + sum_mat A F)" using insert sum_mat_insert[of A] + by (simp add: image_subset_iff) + also have "... = B * A x + B * sum_mat A F" + proof (rule mult_add_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 dimR" using insert fc_mats_carrier dim_eq by simp + qed + also have "... = B * A x + (0\<^sub>m dimR dimR)" using insert by simp + also have "... = 0\<^sub>m dimR dimR" using insert by simp + finally show ?case . +qed + +lemma (in cpx_sq_mat) sum_mat_ortho_square: + shows "finite I \ (\i. i\ I \ ((A i)::complex Matrix.mat) * (A i) = A i) \ + (\i. i\ I \ A i \ fc_mats) \ + (\ i j. i\ I \ j\ I \ i\ j \ A i * (A j) = (0\<^sub>m dimR dimR)) \ + (sum_mat A I) * (sum_mat A I) = (sum_mat A I)" +proof (induct rule:finite_induct) + case empty + then show ?case using dim_eq + by (metis fc_mats_carrier right_mult_zero_mat sum_mat_empty zero_mem) +next + case (insert x F) + have "(sum_mat A (insert x F)) * (sum_mat A (insert x F)) = + (A x + sum_mat A F) * (A x + sum_mat A F)" using insert sum_mat_insert[of A] + by (simp add: \\i. i \ insert x F \ A i * A i = A i\ image_subset_iff) + also have "... = A x * (A x + sum_mat A F) + sum_mat A F * (A x + sum_mat A F)" + 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) + thus "A x + sum_mat A F \ carrier_mat dimC dimC" using insert dim_eq by simp + qed + also have "... = A x * A x + A x * (sum_mat A F) + sum_mat A F * (A x + sum_mat A F)" + proof - + have "A x * (A x + sum_mat A F) = A x * A x + A x * (sum_mat A F)" + using dim_eq insert.prems(2) mult_add_distrib_right sum_mat_carrier + by (metis fc_mats_carrier insertI1 subsetD subset_insertI) + thus ?thesis by simp + qed + also have "... = A x * A x + A x * (sum_mat A F) + sum_mat A F * A x + + sum_mat A F * (sum_mat A F)" + proof - + have "sum_mat A F * (A x + local.sum_mat A F) = + sum_mat A F * A x + local.sum_mat A F * local.sum_mat A F" + using insert dim_eq add_assoc add_mem mult_add_distrib_right cpx_sq_mat_mult sum_mat_carrier + by (metis fc_mats_carrier insertI1 subsetD subset_insertI) + hence "A x * A x + A x * sum_mat A F + sum_mat A F * (A x + sum_mat A F) = + A x * A x + A x * sum_mat A F + (sum_mat A F * A x + sum_mat A F * sum_mat A F)" by simp + also have "... = A x * A x + A x * sum_mat A F + sum_mat A F * A x + sum_mat A F * sum_mat A F" + proof (rule assoc_add_mat[symmetric]) + show "A x * A x + A x * sum_mat A F \ carrier_mat dimR dimR" using sum_mat_carrier insert + dim_eq fc_mats_carrier by (metis add_mem cpx_sq_mat_mult insertCI) + show "sum_mat A F * A x \ carrier_mat dimR dimR" using sum_mat_carrier insert + dim_eq fc_mats_carrier by (metis cpx_sq_mat_mult insertCI) + show "sum_mat A F * sum_mat A F \ carrier_mat dimR dimR" using sum_mat_carrier insert + dim_eq fc_mats_carrier by (metis cpx_sq_mat_mult insertCI) + qed + finally show ?thesis . + qed + also have "... = A x + sum_mat A F" + proof - + have "A x * A x = A x" using insert by simp + moreover have "sum_mat A F * sum_mat A F = sum_mat A F" using insert by simp + moreover have "A x * (sum_mat A F) = 0\<^sub>m dimR dimR" + proof - + have "A x * (sum_mat A F) = sum_mat (\i. A x * (A i)) F" + by (rule sum_mat_distrib_left[symmetric], (simp add: insert)+) + also have "... = sum_mat (\i. 0\<^sub>m dimR dimR) F" + proof (rule sum_mat_cong, (auto simp add: insert zero_mem)) + show "\i. i \ F \ A x * A i = 0\<^sub>m dimR dimR" using insert by auto + show "\i. i \ F \ A x * A i \ fc_mats" using insert cpx_sq_mat_mult by auto + show "\i. i \ F \ 0\<^sub>m dimR dimR \ fc_mats" using zero_mem dim_eq by simp + qed + also have "... = 0\<^sub>m dimR dimR" using zero_sum_mat insert by simp + finally show ?thesis . + qed + moreover have "sum_mat A F * A x = 0\<^sub>m dimR dimR" + proof - + have "sum_mat A F * A x = sum_mat (\i. A i * (A x)) F" + by (rule sum_mat_distrib_right[symmetric], (simp add: insert)+) + also have "... = sum_mat (\i. 0\<^sub>m dimR dimR) F" + proof (rule sum_mat_cong, (auto simp add: insert zero_mem)) + show "\i. i \ F \ A i * A x = 0\<^sub>m dimR dimR" using insert by auto + show "\i. i \ F \ A i * A x \ fc_mats" using insert cpx_sq_mat_mult by auto + show "\i. i \ F \ 0\<^sub>m dimR dimR \ fc_mats" using zero_mem dim_eq by simp + qed + also have "... = 0\<^sub>m dimR dimR" using zero_sum_mat insert by simp + finally show ?thesis . + qed + ultimately show ?thesis using add_commute add_zero insert.prems(2) zero_mem dim_eq by auto + qed + also have "... = sum_mat A (insert x F)" using insert sum_mat_insert[of A x F] + by (simp add: \\i. i \ insert x F \ A i * A i = A i\ image_subsetI) + finally show ?case . +qed + +lemma diagonal_unit_vec: + assumes "B \ carrier_mat n n" +and "diagonal_mat (B::complex Matrix.mat)" +shows "B *\<^sub>v (unit_vec n i) = B $$ (i,i) \\<^sub>v (unit_vec n i)" +proof - + define v::"complex Matrix.vec" where "v = unit_vec n i" + have "B *\<^sub>v v = Matrix.vec n (\ i. Matrix.scalar_prod (Matrix.row B i) v)" + using assms unfolding mult_mat_vec_def by simp + also have "... = Matrix.vec n (\ i. B $$(i,i) * Matrix.vec_index v i)" + proof - + have "\i < n. (Matrix.scalar_prod (Matrix.row B i) v = B $$(i,i) * Matrix.vec_index v i)" + proof (intro allI impI) + fix i + assume "i < n" + have "(Matrix.scalar_prod (Matrix.row B i) v) = + (\ j \ {0 ..< n}. Matrix.vec_index (Matrix.row B i) j * Matrix.vec_index v j)" using assms + unfolding Matrix.scalar_prod_def v_def by simp + also have "... = Matrix.vec_index (Matrix.row B i) i * Matrix.vec_index v i" + proof (rule sum_but_one) + show "\j < n. j \ i \ Matrix.vec_index (Matrix.row B i) j = 0" + proof (intro allI impI) + fix j + assume "j < n" and "j \ i" + hence "Matrix.vec_index (Matrix.row B i) j = B $$ (i,j)" using \i < n\ \j < n\ assms + by auto + also have "... = 0" using assms \i < n\ \j < n\ \j\ i\ unfolding diagonal_mat_def by simp + finally show "Matrix.vec_index (Matrix.row B i) j = 0" . + qed + show "i < n" using \i < n\ . + qed + also have "... = B $$(i,i) * Matrix.vec_index v i" using assms \i < n\ by auto + finally show "(Matrix.scalar_prod (Matrix.row B i) v) = B $$(i,i) * Matrix.vec_index v i" . + qed + thus ?thesis by auto + qed + also have "... = B $$ (i,i) \\<^sub>v v" unfolding v_def unit_vec_def by auto + finally have "B *\<^sub>v v = B $$ (i,i) \\<^sub>v v" . + thus ?thesis unfolding v_def by simp +qed + +lemma mat_vec_mult_assoc: + assumes "A \ carrier_mat n p" +and "B\ carrier_mat p q" +and "dim_vec v = q" +shows "A *\<^sub>v (B *\<^sub>v v) = (A * B) *\<^sub>v v" using assms by auto + +lemma (in cpx_sq_mat) similar_eigenvectors: + assumes "A\ fc_mats" + and "B\ fc_mats" + and "P\ fc_mats" + and "similar_mat_wit A B P (Complex_Matrix.adjoint P)" + and "diagonal_mat B" + and "i < n" +shows "A *\<^sub>v (P *\<^sub>v (unit_vec dimR i)) = B $$ (i,i) \\<^sub>v (P *\<^sub>v (unit_vec dimR i))" +proof - + have "A *\<^sub>v (P *\<^sub>v (unit_vec dimR i)) = + (P * B * (Complex_Matrix.adjoint P)) *\<^sub>v (P *\<^sub>v (unit_vec dimR i))" + using assms unfolding similar_mat_wit_def by metis + also have "... = P * B * (Complex_Matrix.adjoint P) * P *\<^sub>v (unit_vec dimR i)" + proof (rule mat_vec_mult_assoc[of _ dimR dimR], (auto simp add: assms fc_mats_carrier)) + show "P \ carrier_mat dimR dimR" using assms fc_mats_carrier dim_eq by simp + show "P * B * Complex_Matrix.adjoint P \ carrier_mat dimR dimR" + using assms fc_mats_carrier by auto + qed + also have "... = P * B * ((Complex_Matrix.adjoint P) * P) *\<^sub>v (unit_vec dimR i)" using assms dim_eq + by (smt fc_mats_carrier mat_assoc_test(1) similar_mat_witD2(6) similar_mat_wit_sym) + also have "... = P * B *\<^sub>v (unit_vec dimR i)" + proof - + have "(Complex_Matrix.adjoint P) * P = 1\<^sub>m dimR" using assms dim_eq unfolding similar_mat_wit_def + by (simp add: fc_mats_carrier) + thus ?thesis using assms(2) local.fc_mats_carrier dim_eq by auto + qed + also have "... = P *\<^sub>v (B *\<^sub>v (unit_vec dimR i))" using mat_vec_mult_assoc assms fc_mats_carrier + dim_eq by simp + also have "... = P *\<^sub>v (B $$ (i,i) \\<^sub>v (unit_vec dimR i))" using assms diagonal_unit_vec + fc_mats_carrier dim_eq by simp + also have "... = B $$ (i,i) \\<^sub>v (P *\<^sub>v (unit_vec dimR i))" + proof (rule mult_mat_vec) + show "P \ carrier_mat dimR dimC" using assms fc_mats_carrier by simp + show "unit_vec dimR i \ carrier_vec dimC" using dim_eq by simp + qed + finally show ?thesis . +qed + + +subsection \Projectors\ + +definition projector where +"projector M \ (hermitian M \ M * M = M)" + +lemma projector_hermitian: + assumes "projector M" + shows "hermitian M" using assms unfolding projector_def by simp + +lemma zero_projector[simp]: + shows "projector (0\<^sub>m n n)" unfolding projector_def +proof + show "hermitian (0\<^sub>m n n)" using zero_hermitian[of n] by simp + show "0\<^sub>m n n * 0\<^sub>m n n = 0\<^sub>m n n" by simp +qed + +lemma projector_square_eq: + assumes "projector M" + shows "M * M = M" using assms unfolding projector_def by simp + +lemma projector_positive: + assumes "projector M" + shows "Complex_Matrix.positive M" +proof (rule positive_if_decomp) + show "M \ carrier_mat (dim_row M) (dim_row M)" using assms projector_hermitian hermitian_square + by auto +next + have "M = Complex_Matrix.adjoint M" using assms projector_hermitian[of M] + unfolding hermitian_def by simp + hence "M * Complex_Matrix.adjoint M = M * M" by simp + also have "... = M" using assms projector_square_eq by auto + finally have "M * Complex_Matrix.adjoint M = M" . + thus "\Ma. Ma * Complex_Matrix.adjoint Ma = M" by auto +qed + +lemma projector_collapse_trace: + assumes "projector (P::complex Matrix.mat)" + and "P \ carrier_mat n n" + and "R\ carrier_mat n n" +shows "Complex_Matrix.trace (P * R * P) = Complex_Matrix.trace (R * P)" +proof - + have "Complex_Matrix.trace (R * P) = Complex_Matrix.trace (P * R)" using trace_comm assms by auto + also have "... = Complex_Matrix.trace ((P * P) * R)" using assms projector_square_eq[of P] by simp + also have "... = Complex_Matrix.trace (P * (P * R))" using assms by auto + also have "... = Complex_Matrix.trace (P * R * P)" using trace_comm[of P n "P * R"] assms by auto + finally have "Complex_Matrix.trace (R * P) = Complex_Matrix.trace (P * R * P)" . + thus ?thesis by simp +qed + +lemma positive_proj_trace: + assumes "projector (P::complex Matrix.mat)" + and "Complex_Matrix.positive R" + and "P \ carrier_mat n n" + and "R\ carrier_mat n n" +shows "Complex_Matrix.trace (R * P) \ 0" +proof - + have "Complex_Matrix.trace (R * P) = Complex_Matrix.trace ((P * R) * P)" + using assms projector_collapse_trace by auto + also have "... = Complex_Matrix.trace ((P * R) * (Complex_Matrix.adjoint P))" + using assms projector_hermitian[of P] + unfolding hermitian_def by simp + also have "... \ 0" + proof (rule positive_trace) + show " P * R * Complex_Matrix.adjoint P \ carrier_mat n n" using assms by auto + show "Complex_Matrix.positive (P * R * Complex_Matrix.adjoint P)" + by (rule positive_close_under_left_right_mult_adjoint[of _ n], (auto simp add: assms)) + qed + finally show ?thesis . +qed + +lemma trace_proj_pos_real: + assumes "projector (P::complex Matrix.mat)" + and "Complex_Matrix.positive R" + and "P \ carrier_mat n n" + and "R\ carrier_mat n n" +shows "Re (Complex_Matrix.trace (R * P)) = Complex_Matrix.trace (R * P)" +proof - + have "Complex_Matrix.trace (R * P) \ 0" using assms positive_proj_trace by simp + thus ?thesis by (simp add: complex_eqI) +qed + +lemma (in cpx_sq_mat) trace_sum_mat_proj_pos_real: + fixes f::"'a \ real" + assumes "finite I" + and "\ i\ I. projector (P i)" + and "Complex_Matrix.positive R" + and "\i\ I. P i \ fc_mats" + and "R \ fc_mats" +shows "Complex_Matrix.trace (R * (sum_mat (\i. f i \\<^sub>m (P i)) I)) = + Re (Complex_Matrix.trace (R * (sum_mat (\i. f i \\<^sub>m (P i)) I)))" +proof - + have sm: "\x. x \ I \ Complex_Matrix.trace (f x \\<^sub>m (R * P x)) = + f x * Complex_Matrix.trace (R * P x)" + proof - + fix i + assume "i\ I" + show "Complex_Matrix.trace (f i \\<^sub>m (R * P i)) = f i * Complex_Matrix.trace (R * P i)" + proof (rule trace_smult) + show "R * P i \ carrier_mat dimR dimR" using assms cpx_sq_mat_mult fc_mats_carrier \i\ I\ + dim_eq by simp + qed + qed + have sw: "\x. x \ I \ R * (f x \\<^sub>m P x) = f x \\<^sub>m (R * P x)" + proof - + fix i + assume "i \ I" + show "R * (f i \\<^sub>m P i) = f i \\<^sub>m (R * P i)" + proof (rule mult_smult_distrib) + show "R\ carrier_mat dimR dimR" using assms fc_mats_carrier dim_eq by simp + show "P i \ carrier_mat dimR dimR" using assms \i\ I\ fc_mats_carrier dim_eq by simp + qed + qed + have dr: "Complex_Matrix.trace (R * (sum_mat (\i. f i \\<^sub>m (P i)) I)) = + Complex_Matrix.trace (sum_mat (\i. (R * (f i \\<^sub>m (P i)))) I)" + using sum_mat_distrib_left[of I] assms by (simp add: cpx_sq_mat_smult) + also have trs: "... = (\ i\ I. Complex_Matrix.trace (R * (f i \\<^sub>m (P i))))" + proof (rule trace_sum_mat, (simp add: assms)) + show "\i. i \ I \ R * (f i \\<^sub>m P i) \ fc_mats" using assms + by (simp add: cpx_sq_mat_smult cpx_sq_mat_mult) + qed + also have "... = (\ i\ I. Complex_Matrix.trace (f i \\<^sub>m (R * (P i))))" + by (rule sum.cong, (simp add: sw)+) + also have "... = (\ i\ I. f i * Complex_Matrix.trace (R * (P i)))" + by (rule sum.cong, (simp add: sm)+) + also have "... = (\ i\ I. complex_of_real (f i * Re (Complex_Matrix.trace (R * (P i)))))" + proof (rule sum.cong, simp) + show "\x. x \ I \ + complex_of_real (f x) * Complex_Matrix.trace (R * P x) = + complex_of_real (f x * Re (Complex_Matrix.trace (R * P x)))" + proof - + fix x + assume "x\ I" + have "complex_of_real (f x) * Complex_Matrix.trace (R * P x) = + complex_of_real (f x) * complex_of_real (Re (Complex_Matrix.trace (R * P x)))" + using assms sum.cong[of I I] fc_mats_carrier trace_proj_pos_real \x \ I\ dim_eq by auto + also have "... = complex_of_real (f x * Re (Complex_Matrix.trace (R * P x)))" by simp + finally show "complex_of_real (f x) * Complex_Matrix.trace (R * P x) = + complex_of_real (f x * Re (Complex_Matrix.trace (R * P x)))" . + qed + qed + also have "... = (\ i\ I. f i * Re (Complex_Matrix.trace (R * (P i))))" by simp + also have "... = (\ i\ I. Re (Complex_Matrix.trace (f i \\<^sub>m (R * (P i)))))" + proof - + have "(\ i\ I. f i * Re (Complex_Matrix.trace (R * (P i)))) = + (\ i\ I. Re (Complex_Matrix.trace (f i \\<^sub>m (R * (P i)))))" + by (rule sum.cong, (simp add: sm)+) + thus ?thesis by simp + qed + also have "... = (\ i\ I. Re (Complex_Matrix.trace (R * (f i \\<^sub>m (P i)))))" + proof - + have "\i. i \ I \ f i \\<^sub>m (R * (P i)) = R * (f i \\<^sub>m (P i))" using sw by simp + thus ?thesis by simp + qed + also have "... = Re (\ i\ I. (Complex_Matrix.trace (R * (f i \\<^sub>m (P i)))))" by simp + also have "... = Re (Complex_Matrix.trace (sum_mat (\i. R * (f i \\<^sub>m (P i))) I))" using trs by simp + also have "... = Re (Complex_Matrix.trace (R * (sum_mat (\i. f i \\<^sub>m (P i))) I))" using dr by simp + finally show ?thesis . +qed + + +subsection \Rank 1 projection\ + +definition rank_1_proj where +"rank_1_proj v = outer_prod v v" + +lemma rank_1_proj_square_mat: + shows "square_mat (rank_1_proj v)" using outer_prod_dim unfolding rank_1_proj_def + by (metis carrier_matD(1) carrier_matD(2) carrier_vec_dim_vec square_mat.simps) + +lemma rank_1_proj_dim[simp]: + shows "dim_row (rank_1_proj v) = dim_vec v" using outer_prod_dim unfolding rank_1_proj_def + using carrier_vecI by blast + +lemma rank_1_proj_carrier[simp]: + shows "rank_1_proj v \ carrier_mat (dim_vec v) (dim_vec v)" using outer_prod_dim + unfolding rank_1_proj_def using carrier_vecI by blast + +lemma rank_1_proj_coord: + assumes "i < dim_vec v" + and "j < dim_vec v" +shows "(rank_1_proj v) $$ (i, j) = Matrix.vec_index v i * (cnj (Matrix.vec_index v j))" using assms + unfolding rank_1_proj_def outer_prod_def by auto + +lemma rank_1_proj_adjoint: + shows "Complex_Matrix.adjoint (rank_1_proj (v::complex Matrix.vec)) = rank_1_proj v" +proof + show "dim_row (Complex_Matrix.adjoint (rank_1_proj v)) = dim_row (rank_1_proj v)" + using rank_1_proj_square_mat by auto + thus "dim_col (Complex_Matrix.adjoint (rank_1_proj v)) = dim_col (rank_1_proj v)" by auto + fix i j + assume "i < dim_row (rank_1_proj v)" and "j < dim_col (rank_1_proj v)" note ij = this + have "Complex_Matrix.adjoint (rank_1_proj v) $$ (i, j) = conjugate ((rank_1_proj v) $$ (j, i))" + using ij \dim_col (Complex_Matrix.adjoint (rank_1_proj v)) = dim_col (rank_1_proj v)\ + adjoint_eval by fastforce + also have "... = conjugate (Matrix.vec_index v j * (cnj (Matrix.vec_index v i)))" + using rank_1_proj_coord ij + by (metis \dim_col (Complex_Matrix.adjoint (rank_1_proj v)) = dim_col (rank_1_proj v)\ + adjoint_dim_col rank_1_proj_dim) + also have "... = Matrix.vec_index v i * (cnj (Matrix.vec_index v j))" by simp + also have "... = rank_1_proj v $$ (i, j)" using ij rank_1_proj_coord + by (metis \dim_col (Complex_Matrix.adjoint (rank_1_proj v)) = dim_col (rank_1_proj v)\ + adjoint_dim_col rank_1_proj_dim) + finally show "Complex_Matrix.adjoint (rank_1_proj v) $$ (i, j) = rank_1_proj v $$ (i, j)". +qed + +lemma rank_1_proj_hermitian: + shows "hermitian (rank_1_proj (v::complex Matrix.vec))" using rank_1_proj_adjoint + unfolding hermitian_def by simp + +lemma rank_1_proj_trace: + assumes "\v\ = 1" + shows "Complex_Matrix.trace (rank_1_proj v) = 1" +proof - + have "Complex_Matrix.trace (rank_1_proj v) = inner_prod v v" using trace_outer_prod + unfolding rank_1_proj_def using carrier_vecI by blast + also have "... = (vec_norm v)\<^sup>2" unfolding vec_norm_def using power2_csqrt by presburger + also have "... = \v\\<^sup>2" using vec_norm_sq_cpx_vec_length_sq by simp + also have "... = 1" using assms by simp + finally show ?thesis . +qed + +lemma rank_1_proj_mat_col: + assumes "A \ carrier_mat n n" + and "i < n" + and "j < n" + and "k < n" +shows "(rank_1_proj (Matrix.col A i)) $$ (j, k) = A $$ (j, i) * conjugate (A $$ (k,i))" +proof - + have "(rank_1_proj (Matrix.col A i)) $$ (j, k) = Matrix.vec_index (Matrix.col A i) j * + conjugate (Matrix.vec_index (Matrix.col A i) k)" using index_outer_prod[of "Matrix.col A i" n "Matrix.col A i" n] + assms unfolding rank_1_proj_def by simp + also have "... = A $$ (j, i) * conjugate (A $$ (k,i))" using assms by simp + finally show ?thesis . +qed + +lemma (in cpx_sq_mat) weighted_sum_rank_1_proj_unitary_index: + assumes "A \ fc_mats" +and "B \ fc_mats" +and "diagonal_mat B" +and "Complex_Matrix.unitary A" +and "j < dimR" +and "k < dimR" +shows "(sum_mat (\i. (diag_mat B)!i \\<^sub>m rank_1_proj (Matrix.col A i)) {..< dimR}) $$ (j,k) = + (A * B * (Complex_Matrix.adjoint A)) $$ (j,k)" +proof - + have "(sum_mat (\i. (diag_mat B)!i \\<^sub>m rank_1_proj (Matrix.col A i)) {..< dimR}) $$ (j,k) = + (\ i\ {..< dimR}. ((diag_mat B)!i \\<^sub>m rank_1_proj (Matrix.col A i)) $$ (j,k))" + proof (rule sum_mat_index, (auto simp add: fc_mats_carrier assms)) + show "\i. i < dimR \ (diag_mat B)!i \\<^sub>m rank_1_proj (Matrix.col A i) \ carrier_mat dimR dimC" + using rank_1_proj_carrier assms fc_mats_carrier dim_eq + by (metis smult_carrier_mat zero_col_col zero_col_dim) + show "k < dimC" using assms dim_eq by simp + qed + also have "... = (\ i\ {..< dimR}. (diag_mat B)!i* A $$ (j, i) * conjugate (A $$ (k,i)))" + proof (rule sum.cong, simp) + have idx: "\x. x \ {.. (rank_1_proj (Matrix.col A x)) $$ (j, k) = + A $$ (j, x) * conjugate (A $$ (k, x))" using rank_1_proj_mat_col assms fc_mats_carrier dim_eq + by blast + show "\x. x \ {.. ((diag_mat B)!x \\<^sub>m rank_1_proj (Matrix.col A x)) $$ (j, k) = + (diag_mat B)!x * A $$ (j, x) * conjugate (A $$ (k, x))" + proof - + fix x + assume "x\ {..< dimR}" + have "((diag_mat B)!x \\<^sub>m rank_1_proj (Matrix.col A x)) $$ (j, k) = + (diag_mat B)!x * (rank_1_proj (Matrix.col A x)) $$ (j, k)" + proof (rule index_smult_mat) + show "j < dim_row (rank_1_proj (Matrix.col A x))" using \x\ {..< dimR}\ assms fc_mats_carrier by simp + show "k < dim_col (rank_1_proj (Matrix.col A x))" using \x\ {..< dimR}\ assms fc_mats_carrier + rank_1_proj_carrier[of "Matrix.col A x"] by simp + qed + thus "((diag_mat B)!x \\<^sub>m rank_1_proj (Matrix.col A x)) $$ (j, k) = + (diag_mat B)!x * A $$ (j, x) * conjugate (A $$ (k, x))" using idx \x\ {..< dimR}\ by simp + qed + qed + also have "... = Matrix.scalar_prod (Matrix.col (Complex_Matrix.adjoint A) k) (Matrix.row (A*B) j) " + unfolding Matrix.scalar_prod_def + proof (rule sum.cong) + show "{..x. x \ {0.. + diag_mat B ! x * A $$ (j, x) * conjugate (A $$ (k, x)) = + Matrix.vec_index ((Matrix.col (Complex_Matrix.adjoint A) k)) x * + Matrix.vec_index (Matrix.row (A*B) j) x" + proof - + fix x + assume "x\ {0.. {0.. carrier_mat dimR dimR" using assms fc_mats_carrier dim_eq by simp + show "B \ carrier_mat dimR dimR" using assms fc_mats_carrier dim_eq by simp + show "x < dimR" using \x\{0..< dimR}\ by simp + qed + moreover have "conjugate (A $$ (k, x)) = + Matrix.vec_index ((Matrix.col (Complex_Matrix.adjoint A) k)) x" using \x\ {0.. assms + fc_mats_carrier dim_eq by (simp add: adjoint_col) + ultimately show "diag_mat B ! x * A $$ (j, x) * conjugate (A $$ (k, x)) = + Matrix.vec_index ((Matrix.col (Complex_Matrix.adjoint A) k)) x * + Matrix.vec_index (Matrix.row (A*B) j) x" by simp + qed + qed + also have "... = (A*B * (Complex_Matrix.adjoint A)) $$ (j,k)" + proof - + have "Matrix.mat (dim_row (A*B)) (dim_col (Complex_Matrix.adjoint A)) + (\(i, j). Matrix.scalar_prod (Matrix.row (A*B) i) (Matrix.col (Complex_Matrix.adjoint A) j)) $$ + (j, k) = Matrix.scalar_prod (Matrix.row (A*B) j) (Matrix.col (Complex_Matrix.adjoint A) k)" + using assms fc_mats_carrier by simp + also have "... = Matrix.scalar_prod (Matrix.col (Complex_Matrix.adjoint A) k) (Matrix.row (A*B) j)" + using assms comm_scalar_prod[of "Matrix.row (A*B) j" dimR] fc_mats_carrier dim_eq + by (metis adjoint_dim Matrix.col_carrier_vec row_carrier_vec cpx_sq_mat_mult) + thus ?thesis using assms fc_mats_carrier unfolding times_mat_def by simp + qed + finally show ?thesis . +qed + +lemma (in cpx_sq_mat) weighted_sum_rank_1_proj_unitary: + assumes "A \ fc_mats" +and "B \ fc_mats" +and "diagonal_mat B" +and "Complex_Matrix.unitary A" +shows "(sum_mat (\i. (diag_mat B)!i \\<^sub>m rank_1_proj (Matrix.col A i)) {..< dimR}) = + (A * B * (Complex_Matrix.adjoint A))" +proof + show "dim_row (sum_mat (\i. diag_mat B ! i \\<^sub>m rank_1_proj (Matrix.col A i)) {..i. diag_mat B ! i \\<^sub>m rank_1_proj (Matrix.col A i)) {..i j. i < dim_row (A * B * Complex_Matrix.adjoint A) \ + j < dim_col (A * B * Complex_Matrix.adjoint A) \ + local.sum_mat (\i. diag_mat B ! i \\<^sub>m rank_1_proj (Matrix.col A i)) {..v\ = 1" + shows "projector (rank_1_proj v)" +proof - + have "Complex_Matrix.adjoint (rank_1_proj v) = rank_1_proj v" using rank_1_proj_adjoint by simp + hence a: "hermitian (rank_1_proj v)" unfolding hermitian_def by simp + have "rank_1_proj v * rank_1_proj v = inner_prod v v \\<^sub>m outer_prod v v" unfolding rank_1_proj_def + using outer_prod_mult_outer_prod assms using carrier_vec_dim_vec by blast + also have "... = (vec_norm v)\<^sup>2 \\<^sub>m outer_prod v v" unfolding vec_norm_def using power2_csqrt + by presburger + also have "... = (cpx_vec_length v)\<^sup>2 \\<^sub>m outer_prod v v " using vec_norm_sq_cpx_vec_length_sq + by simp + also have "... = outer_prod v v" using assms state_qbit_norm_sq smult_one[of "outer_prod v v"] + by simp + also have "... = rank_1_proj v" unfolding rank_1_proj_def by simp + finally show ?thesis using a unfolding projector_def by simp +qed + +lemma rank_1_proj_positive: + assumes "\v\ = 1" + shows "Complex_Matrix.positive (rank_1_proj v)" +proof - + have "projector (rank_1_proj v)" using assms rank_1_proj_projector by simp + thus ?thesis using projector_positive by simp +qed + +lemma rank_1_proj_density: + assumes "\v\ = 1" + shows "density_operator (rank_1_proj v)" unfolding density_operator_def using assms + by (simp add: rank_1_proj_positive rank_1_proj_trace) + +lemma (in cpx_sq_mat) sum_rank_1_proj_unitary_index: + assumes "A \ fc_mats" +and "Complex_Matrix.unitary A" +and "j < dimR" +and "k < dimR" +shows "(sum_mat (\i. rank_1_proj (Matrix.col A i)) {..< dimR}) $$ (j,k) = (1\<^sub>m dimR) $$ (j,k)" +proof - + have "(sum_mat (\i. rank_1_proj (Matrix.col A i)) {..< dimR}) $$ (j,k) = + (\ i\ {..< dimR}. (rank_1_proj (Matrix.col A i)) $$ (j,k))" + proof (rule sum_mat_index, (auto simp add: fc_mats_carrier assms)) + show "\i. i < dimR \ rank_1_proj (Matrix.col A i) \ carrier_mat dimR dimC" + proof - + fix i + assume "i < dimR" + hence "dim_vec (Matrix.col A i) = dimR" using assms fc_mats_carrier by simp + thus "rank_1_proj (Matrix.col A i) \ carrier_mat dimR dimC" using rank_1_proj_carrier assms + fc_mats_carrier dim_eq fc_mats_carrier by (metis dim_col fc_mats_carrier) + qed + show "k < dimC" using assms dim_eq by simp + qed + also have "... = (\ i\ {..< dimR}. A $$ (j, i) * conjugate (A $$ (k,i)))" + proof (rule sum.cong, simp) + show "\x. x \ {.. rank_1_proj (Matrix.col A x) $$ (j, k) = + A $$ (j, x) * conjugate (A $$ (k, x))" + using rank_1_proj_mat_col assms using local.fc_mats_carrier dim_eq by blast + qed + also have "... = Matrix.scalar_prod (Matrix.col (Complex_Matrix.adjoint A) k) (Matrix.row A j) " + unfolding Matrix.scalar_prod_def + proof (rule sum.cong) + show "{..x. x \ {0.. + A $$ (j, x) * conjugate (A $$ (k, x)) = + Matrix.vec_index ((Matrix.col (Complex_Matrix.adjoint A) k)) x * Matrix.vec_index (Matrix.row A j) x" + proof - + fix x + assume "x\ {0.. {0..x\ {0.. + assms fc_mats_carrier dim_eq by simp + moreover have "conjugate (A $$ (k, x)) = + Matrix.vec_index ((Matrix.col (Complex_Matrix.adjoint A) k)) x" using \x\ {0.. + assms fc_mats_carrier dim_eq by (simp add: adjoint_col) + ultimately show "A $$ (j, x) * conjugate (A $$ (k, x)) = + Matrix.vec_index ((Matrix.col (Complex_Matrix.adjoint A) k)) x * + Matrix.vec_index (Matrix.row A j) x" by simp + qed + qed + also have "... = (A * (Complex_Matrix.adjoint A)) $$ (j,k)" + proof - + have "Matrix.mat (dim_row A) (dim_col (Complex_Matrix.adjoint A)) + (\(i, j). Matrix.scalar_prod (Matrix.row A i) (Matrix.col (Complex_Matrix.adjoint A) j)) $$ + (j, k) = Matrix.scalar_prod (Matrix.row A j) (Matrix.col (Complex_Matrix.adjoint A) k)" + using assms fc_mats_carrier by simp + also have "... = Matrix.scalar_prod (Matrix.col (Complex_Matrix.adjoint A) k) (Matrix.row A j)" + using assms comm_scalar_prod[of "Matrix.row A j" dimR] fc_mats_carrier + by (simp add: adjoint_dim dim_eq) + thus ?thesis using assms fc_mats_carrier unfolding times_mat_def by simp + qed + also have "... = (1\<^sub>m dimR) $$ (j,k)" using assms dim_eq by (simp add: fc_mats_carrier) + finally show ?thesis . +qed + +lemma (in cpx_sq_mat) rank_1_proj_sum_density: + assumes "finite I" + and "\i\ I. \u i\ = 1" + and "\i\ I. dim_vec (u i) = dimR" + and "\i\ I. 0 \ p i" + and "(\i\ I. p i) = 1" +shows "density_operator (sum_mat (\i. p i \\<^sub>m (rank_1_proj (u i))) I)" unfolding density_operator_def +proof + have "Complex_Matrix.trace (sum_mat (\i. p i \\<^sub>m rank_1_proj (u i)) I) = + (\i\ I. Complex_Matrix.trace (p i \\<^sub>m rank_1_proj (u i)))" + proof (rule trace_sum_mat, (simp add: assms)) + show "\i. i \ I \ p i \\<^sub>m rank_1_proj (u i) \ fc_mats" using assms smult_mem fc_mats_carrier + dim_eq by auto + qed + also have "... = (\i\ I. p i * Complex_Matrix.trace (rank_1_proj (u i)))" + proof - + { + fix i + assume "i \ I" + hence "Complex_Matrix.trace (p i \\<^sub>m rank_1_proj (u i)) = + p i * Complex_Matrix.trace (rank_1_proj (u i))" + using trace_smult[of "rank_1_proj (u i)" dimR] assms fc_mats_carrier dim_eq by auto + } + thus ?thesis by simp + qed + also have "... = 1" using assms rank_1_proj_trace assms by auto + finally show "Complex_Matrix.trace (sum_mat (\i. p i \\<^sub>m rank_1_proj (u i)) I) = 1" . +next + show "Complex_Matrix.positive (sum_mat (\i. p i \\<^sub>m rank_1_proj (u i)) I)" + proof (rule sum_mat_positive, (simp add: assms)) + fix i + assume "i\ I" + thus "p i \\<^sub>m rank_1_proj (u i) \ fc_mats" using assms smult_mem fc_mats_carrier dim_eq by auto + show "Complex_Matrix.positive (p i \\<^sub>m rank_1_proj (u i))" using assms \i\ I\ + rank_1_proj_positive positive_smult[of "rank_1_proj (u i)" dimR] dim_eq by auto + qed +qed + + + +lemma (in cpx_sq_mat) sum_rank_1_proj_unitary: + assumes "A \ fc_mats" +and "Complex_Matrix.unitary A" +shows "(sum_mat (\i. rank_1_proj (Matrix.col A i)) {..< dimR})= (1\<^sub>m dimR)" +proof + show "dim_row (sum_mat (\i. rank_1_proj (Matrix.col A i)) {..m dimR)" + using assms fc_mats_carrier + by (metis carrier_matD(1) dim_col dim_eq index_one_mat(2) rank_1_proj_carrier sum_mat_carrier) + show "dim_col (sum_mat (\i. rank_1_proj (Matrix.col A i)) {..m dimR)" + using assms fc_mats_carrier rank_1_proj_carrier sum_mat_carrier + by (metis carrier_matD(2) dim_col dim_eq index_one_mat(3) square_mat.simps square_mats) + show "\i j. i < dim_row (1\<^sub>m dimR) \ + j < dim_col (1\<^sub>m dimR) \ sum_mat (\i. rank_1_proj (Matrix.col A i)) {..m dimR $$ (i, j)" + using assms sum_rank_1_proj_unitary_index by simp +qed + +lemma (in cpx_sq_mat) rank_1_proj_unitary: + assumes "A \ fc_mats" +and "Complex_Matrix.unitary A" +and "j < dimR" +and "k < dimR" +shows "rank_1_proj (Matrix.col A j) * (rank_1_proj (Matrix.col A k)) = + (1\<^sub>m dimR) $$ (j,k) \\<^sub>m (outer_prod (Matrix.col A j) (Matrix.col A k))" +proof - + have "rank_1_proj (Matrix.col A j) * (rank_1_proj (Matrix.col A k)) = + Complex_Matrix.inner_prod (Matrix.col A j) (Matrix.col A k) \\<^sub>m outer_prod (Matrix.col A j) (Matrix.col A k)" + using outer_prod_mult_outer_prod assms Matrix.col_dim local.fc_mats_carrier unfolding rank_1_proj_def + by blast + also have "... = (Complex_Matrix.adjoint A * A) $$ (j, k)\\<^sub>m (outer_prod (Matrix.col A j) (Matrix.col A k))" + using inner_prod_adjoint_comp[of A dimR A] assms fc_mats_carrier dim_eq by simp + also have "... = (1\<^sub>m dimR) $$ (j,k) \\<^sub>m (outer_prod (Matrix.col A j) (Matrix.col A k))" using assms + unfolding Complex_Matrix.unitary_def + by (metis add_commute assms(2) index_add_mat(2) index_one_mat(2) one_mem unitary_simps(1)) + finally show ?thesis . +qed + +lemma (in cpx_sq_mat) rank_1_proj_unitary_ne: + assumes "A \ fc_mats" +and "Complex_Matrix.unitary A" +and "j < dimR" +and "k < dimR" +and "j\ k" +shows "rank_1_proj (Matrix.col A j) * (rank_1_proj (Matrix.col A k)) = (0\<^sub>m dimR dimR)" +proof - + have "dim_row (0 \\<^sub>m outer_prod (Matrix.col A j) (Matrix.col A k)) = dim_row (outer_prod (Matrix.col A j) (Matrix.col A k))" + by simp + also have "... = dimR" using assms fc_mats_carrier dim_eq by auto + finally have rw: "dim_row (0 \\<^sub>m outer_prod (Matrix.col A j) (Matrix.col A k)) = dimR" . + have "dim_col (0 \\<^sub>m outer_prod (Matrix.col A j) (Matrix.col A k)) = dim_col (outer_prod (Matrix.col A j) (Matrix.col A k))" + by simp + also have "... = dimR" using assms fc_mats_carrier dim_eq by auto + finally have cl: "dim_col (0 \\<^sub>m outer_prod (Matrix.col A j) (Matrix.col A k)) = dimR" . + have "rank_1_proj (Matrix.col A j) * (rank_1_proj (Matrix.col A k)) = + (0::complex) \\<^sub>m (outer_prod (Matrix.col A j) (Matrix.col A k))" + using assms rank_1_proj_unitary by simp + also have "... = (0\<^sub>m dimR dimR)" + proof + show "dim_row (0 \\<^sub>m outer_prod (Matrix.col A j) (Matrix.col A k)) = dim_row (0\<^sub>m dimR dimR)" using rw by simp + next + show "dim_col (0 \\<^sub>m outer_prod (Matrix.col A j) (Matrix.col A k)) = dim_col (0\<^sub>m dimR dimR)" using cl by simp + next + show "\i p. i < dim_row (0\<^sub>m dimR dimR) \ p < dim_col (0\<^sub>m dimR dimR) \ + (0 \\<^sub>m outer_prod (Matrix.col A j) (Matrix.col A k)) $$ (i, p) = 0\<^sub>m dimR dimR $$ (i, p)" using rw cl by auto + qed + finally show ?thesis . +qed + +lemma (in cpx_sq_mat) rank_1_proj_unitary_eq: + assumes "A \ fc_mats" +and "Complex_Matrix.unitary A" +and "j < dimR" +shows "rank_1_proj (Matrix.col A j) * (rank_1_proj (Matrix.col A j)) = rank_1_proj (Matrix.col A j)" +proof - + have "rank_1_proj (Matrix.col A j) * (rank_1_proj (Matrix.col A j)) = (1::complex) \\<^sub>m (rank_1_proj (Matrix.col A j))" + using assms rank_1_proj_unitary unfolding rank_1_proj_def by simp + also have "... = (rank_1_proj (Matrix.col A j))" by (simp add: smult_one) + finally show ?thesis . +qed + + +end \ No newline at end of file diff --git a/thys/Projective_Measurements/Projective_Measurements.thy b/thys/Projective_Measurements/Projective_Measurements.thy new file mode 100644 --- /dev/null +++ b/thys/Projective_Measurements/Projective_Measurements.thy @@ -0,0 +1,1670 @@ +(* +Author: + Mnacho Echenim, Université Grenoble Alpes +*) + +theory Projective_Measurements imports + Linear_Algebra_Complements + + +begin + + +section \Projective measurements\ + +text \In this part we define projective measurements, also refered to as von Neumann measurements. + The latter are characterized by a set of orthogonal projectors, which are used to compute the +probabilities of measure outcomes and to represent the state of the system after the measurement.\ + +text \The state of the system (a density operator in this case) after a measurement is represented by +the \verb+density_collapse+ function.\ + +subsection \First definitions\ + +text \We begin by defining a type synonym for couples of measurement values (reals) and the +associated projectors (complex matrices).\ + +type_synonym measure_outcome = "real \ complex Matrix.mat" + +text \The corresponding values and projectors are retrieved thanks to \verb+meas_outcome_val+ +and \verb+meas_outcome_prj+.\ + +definition meas_outcome_val::"measure_outcome \ real" where +"meas_outcome_val Mi = fst Mi" + +definition meas_outcome_prj::"measure_outcome \ complex Matrix.mat" where +"meas_outcome_prj Mi = snd Mi" + +text \We define a predicate for projective measurements. A projective measurement is characterized +by the number $p$ of possible measure outcomes, and a function $M$ mapping outcome $i$ to the +corresponding \verb+measure_outcome+.\ + +definition (in cpx_sq_mat) proj_measurement::"nat \ (nat \ measure_outcome) \ bool" where + "proj_measurement n M \ + (inj_on (\i. meas_outcome_val (M i)) {..< n}) \ + (\j < n. meas_outcome_prj (M j) \ fc_mats \ + projector (meas_outcome_prj (M j))) \ + (\ i < n. \ j < n. i \ j \ + meas_outcome_prj (M i) * meas_outcome_prj (M j) = 0\<^sub>m dimR dimR) \ + sum_mat (\j. meas_outcome_prj (M j)) {..< n} = 1\<^sub>m dimR" + +lemma (in cpx_sq_mat) proj_measurement_inj: + assumes "proj_measurement p M" + shows "inj_on (\i. meas_outcome_val (M i)) {..< p}" using assms + unfolding proj_measurement_def by simp + +lemma (in cpx_sq_mat) proj_measurement_carrier: + assumes "proj_measurement p M" + and "i < p" + shows "meas_outcome_prj (M i) \ fc_mats" using assms + unfolding proj_measurement_def by simp + +lemma (in cpx_sq_mat) proj_measurement_ortho: + assumes "proj_measurement p M" +and "i < p" +and "j < p" +and "i\ j" +shows "meas_outcome_prj (M i) * meas_outcome_prj (M j) = 0\<^sub>m dimR dimR" using assms + unfolding proj_measurement_def by simp + +lemma (in cpx_sq_mat) proj_measurement_id: + assumes "proj_measurement p M" + shows "sum_mat (\j. meas_outcome_prj (M j)) {..< p} = 1\<^sub>m dimR" using assms + unfolding proj_measurement_def by simp + +lemma (in cpx_sq_mat) proj_measurement_square: + assumes "proj_measurement p M" +and "i < p" +shows "meas_outcome_prj (M i) \ fc_mats" using assms unfolding proj_measurement_def by simp + +lemma (in cpx_sq_mat) proj_measurement_proj: + assumes "proj_measurement p M" +and "i < p" +shows "projector (meas_outcome_prj (M i))" using assms unfolding proj_measurement_def by simp + +text \We define the probability of obtaining a measurement outcome: this is a positive number and +the sum over all the measurement outcomes is 1.\ + +definition (in cpx_sq_mat) meas_outcome_prob :: "complex Matrix.mat \ + (nat \ real \ complex Matrix.mat) \ nat \ complex" where +"meas_outcome_prob R M i = Complex_Matrix.trace (R* (meas_outcome_prj (M i)))" + +lemma (in cpx_sq_mat) meas_outcome_prob_real: +assumes "R\ fc_mats" + and "density_operator R" + and "proj_measurement n M" + and "i < n" +shows "meas_outcome_prob R M i \ \" +proof - + have "complex_of_real (Re (Complex_Matrix.trace (R * meas_outcome_prj (M i)))) = + Complex_Matrix.trace (R * meas_outcome_prj (M i))" + proof (rule trace_proj_pos_real) + show "R \ carrier_mat dimR dimR" using assms fc_mats_carrier dim_eq by simp + show "Complex_Matrix.positive R" using assms unfolding density_operator_def by simp + show "projector (meas_outcome_prj (M i))" using assms proj_measurement_proj by simp + show "meas_outcome_prj (M i) \ carrier_mat dimR dimR" using assms proj_measurement_carrier + fc_mats_carrier dim_eq by simp + qed + thus ?thesis unfolding meas_outcome_prob_def by (metis Reals_of_real) +qed + +lemma (in cpx_sq_mat) meas_outcome_prob_pos: + assumes "R\ fc_mats" + and "density_operator R" + and "proj_measurement n M" + and "i < n" +shows "0 \ meas_outcome_prob R M i" unfolding meas_outcome_prob_def +proof (rule positive_proj_trace) + show "R \ carrier_mat dimR dimR" using assms fc_mats_carrier dim_eq by simp + show "Complex_Matrix.positive R" using assms unfolding density_operator_def by simp + show "projector (meas_outcome_prj (M i))" using assms proj_measurement_proj by simp + show "meas_outcome_prj (M i) \ carrier_mat dimR dimR" using assms proj_measurement_carrier + fc_mats_carrier dim_eq by simp +qed + +lemma (in cpx_sq_mat) meas_outcome_prob_sum: + assumes "density_operator R" + and "R\ fc_mats" + and" proj_measurement n M" +shows "(\ j \ {..< n}. meas_outcome_prob R M j) = 1" +proof - + have "(\ j \ {..< n}. Complex_Matrix.trace (R* (meas_outcome_prj (M j)))) = + Complex_Matrix.trace (sum_mat (\j. R* (meas_outcome_prj (M j))) {..< n})" + proof (rule trace_sum_mat[symmetric], auto) + fix j + assume "j < n" + thus "R * meas_outcome_prj (M j) \ fc_mats" using cpx_sq_mat_mult assms + unfolding proj_measurement_def by simp + qed + also have "... = Complex_Matrix.trace (R * (sum_mat (\j. (meas_outcome_prj (M j))) {..< n}))" + proof - + have "sum_mat (\j. R* (meas_outcome_prj (M j))) {..< n} = + R * (sum_mat (\j. (meas_outcome_prj (M j))) {..< n})" + proof (rule mult_sum_mat_distrib_left, (auto simp add: assms)) + fix j + assume "j < n" + thus "meas_outcome_prj (M j) \ fc_mats" using assms unfolding proj_measurement_def by simp + qed + thus ?thesis by simp + qed + also have "... = Complex_Matrix.trace (R * 1\<^sub>m dimR)" using assms unfolding proj_measurement_def + by simp + also have "... = Complex_Matrix.trace R" using assms by (simp add: fc_mats_carrier dim_eq) + also have "... = 1" using assms unfolding density_operator_def by simp + finally show ?thesis unfolding meas_outcome_prob_def . +qed + +text \We introduce the maximally mixed density operator. Intuitively, this density operator +corresponds to a uniform distribution of the states of an orthonormal basis. +This operator will be used to define the density operator after a measurement for the measure +outcome probabilities equal to zero.\ + +definition max_mix_density :: "nat \ complex Matrix.mat" where +"max_mix_density n = ((1::real)/ n) \\<^sub>m (1\<^sub>m n)" + +lemma max_mix_density_carrier: + shows "max_mix_density n \ carrier_mat n n" unfolding max_mix_density_def by simp + +lemma max_mix_is_density: + assumes "0 < n" + shows "density_operator (max_mix_density n)" unfolding density_operator_def max_mix_density_def +proof + have "Complex_Matrix.trace (complex_of_real ((1::real)/n) \\<^sub>m 1\<^sub>m n) = + (complex_of_real ((1::real)/n)) * (Complex_Matrix.trace ((1\<^sub>m n)::complex Matrix.mat))" + using one_carrier_mat trace_smult[of "(1\<^sub>m n)::complex Matrix.mat"] by blast + also have "... = (complex_of_real ((1::real)/n)) * (real n)" using trace_1[of n] by simp + also have "... = 1" using assms by simp + finally show "Complex_Matrix.trace (complex_of_real ((1::real)/n) \\<^sub>m 1\<^sub>m n) = 1" . +next + show "Complex_Matrix.positive (complex_of_real (1 / real n) \\<^sub>m 1\<^sub>m n)" + by (rule positive_smult, (auto simp add: positive_one)) +qed + +lemma (in cpx_sq_mat) max_mix_density_square: + shows "max_mix_density dimR \ fc_mats" unfolding max_mix_density_def + using fc_mats_carrier dim_eq by simp + +text \Given a measurement outcome, \verb+density_collapse+ represents the resulting density +operator. In practice only the measure outcomes with nonzero probabilities are of interest; we +(arbitrarily) collapse the density operator for zero-probability outcomes to the maximally mixed +density operator.\ + +definition density_collapse ::"complex Matrix.mat \ complex Matrix.mat \ complex Matrix.mat" where +"density_collapse R P = (if ((Complex_Matrix.trace (R * P)) = 0) then (max_mix_density (dim_row R)) + else ((1::real)/ ((Complex_Matrix.trace (R * P)))) \\<^sub>m (P * R * P))" + +lemma density_collapse_carrier: + assumes "0 < dim_row R" + and "P \ carrier_mat n n" + and "R \ carrier_mat n n" +shows "(density_collapse R P) \ carrier_mat n n" +proof (cases "(Complex_Matrix.trace (R * P)) = 0") + case True + hence "density_collapse R P = max_mix_density (dim_row R)" unfolding density_collapse_def by simp + then show ?thesis using max_mix_is_density assms max_mix_density_carrier by auto +next + case False + hence "density_collapse R P = complex_of_real 1 / Complex_Matrix.trace (R * P) \\<^sub>m (P * R * P)" + unfolding density_collapse_def by simp + thus ?thesis using assms by auto +qed + +lemma density_collapse_operator: + assumes "projector P" + and "density_operator R" + and "0 < dim_row R" + and "P \ carrier_mat n n" + and "R \ carrier_mat n n" +shows "density_operator (density_collapse R P)" +proof (cases "(Complex_Matrix.trace (R * P)) = 0") + case True + hence "density_collapse R P = max_mix_density (dim_row R)" unfolding density_collapse_def by simp + then show ?thesis using max_mix_is_density assms by simp +next + case False + show ?thesis unfolding density_operator_def + proof (intro conjI) + have "Complex_Matrix.positive ((1 / (Complex_Matrix.trace (R * P))) \\<^sub>m (P * R * P))" + proof (rule positive_smult) + show "P * R * P \ carrier_mat n n" using assms by simp + have "Complex_Matrix.positive R" using assms unfolding density_operator_def by simp + hence "0 \ (Complex_Matrix.trace (R * P))" using positive_proj_trace[of P R n] assms + False by auto + hence "0 \ Re (Complex_Matrix.trace (R * P))" by simp + hence "0 \ 1/(Re (Complex_Matrix.trace (R * P)))" by simp + have "Re (Complex_Matrix.trace (R * P)) = Complex_Matrix.trace (R * P)" + using assms \Complex_Matrix.positive R\ trace_proj_pos_real by simp + hence inv: "1/ (Complex_Matrix.trace (R * P)) = 1/(Re (Complex_Matrix.trace (R * P)))" by simp + thus "0 \ 1/ (Complex_Matrix.trace (R * P))" + using \0 \ 1/(Re (Complex_Matrix.trace (R * P)))\ by (simp add: inv) + show "Complex_Matrix.positive (P * R * P)" using assms + positive_close_under_left_right_mult_adjoint[of P n R] + by (simp add: \Complex_Matrix.positive R\ hermitian_def projector_def) + qed + thus "Complex_Matrix.positive (density_collapse R P)" using False + unfolding density_collapse_def by simp + next + have "Complex_Matrix.trace (density_collapse R P) = + Complex_Matrix.trace ((1/ (Complex_Matrix.trace (R * P))) \\<^sub>m (P * R * P))" + using False unfolding density_collapse_def by simp + also have "... = 1/ (Complex_Matrix.trace (R * P)) * Complex_Matrix.trace (P * R * P)" + using trace_smult[of "P * R * P" n] assms by simp + also have "... = 1/ (Complex_Matrix.trace (R * P)) * Complex_Matrix.trace (R * P)" + using projector_collapse_trace assms by simp + also have "... = 1" using False by simp + finally show "Complex_Matrix.trace (density_collapse R P) = 1" . + qed +qed + + +subsection \Measurements with observables\ + +text \It is standard in quantum mechanics to represent projective measurements with so-called +\emph{observables}. These are Hermitian matrices which encode projective measurements as follows: +the eigenvalues of an observable represent the possible projective measurement outcomes, and the +associated projectors are the projectors onto the corresponding eigenspaces. The results in this +part are based on the spectral theorem, which states that any Hermitian matrix admits an +orthonormal basis consisting of eigenvectors of the matrix.\ + + +subsubsection \On the diagonal elements of a matrix\ + +text \We begin by introducing definitions that will be used on the diagonalized version of a +Hermitian matrix.\ + +definition diag_elems where +"diag_elems B = {B$$(i,i) |i. i < dim_row B}" + +text \Relationship between \verb+diag_elems+ and the list \verb+diag_mat+\ + +lemma diag_elems_set_diag_mat: + shows "diag_elems B = set (diag_mat B)" unfolding diag_mat_def diag_elems_def +proof + show "{B $$ (i, i) |i. i < dim_row B} \ set (map (\i. B $$ (i, i)) [0.. {B $$ (i, i) |i. i < dim_row B}" + hence "\i < dim_row B. x = B $$(i,i)" by auto + from this obtain i where "i < dim_row B" and "x = B $$(i,i)" by auto + thus "x \ set (map (\i. B $$ (i, i)) [0..i. B $$ (i, i)) [0.. {B $$ (i, i) |i. i < dim_row B}" + proof + fix x + assume "x \ set (map (\i. B $$ (i, i)) [0.. {B $$ (i, i) |i. i < dim_row B}" by auto + qed +qed + +lemma diag_elems_finite[simp]: + shows "finite (diag_elems B)" unfolding diag_elems_def by simp + +lemma diag_elems_mem[simp]: + assumes "i < dim_row B" + shows "B $$(i,i) \ diag_elems B" using assms unfolding diag_elems_def by auto + +text \When $x$ is a diagonal element of $B$, \verb+diag_elem_indices+ returns the set of diagonal +indices of $B$ with value $x$.\ + +definition diag_elem_indices where +"diag_elem_indices x B = {i|i. i < dim_row B \ B $$ (i,i) = x}" + +lemma diag_elem_indices_elem: + assumes "a \ diag_elem_indices x B" + shows "a < dim_row B \ B$$(a,a) = x" using assms unfolding diag_elem_indices_def by simp + +lemma diag_elem_indices_itself: + assumes "i < dim_row B" + shows "i \ diag_elem_indices (B $$(i,i)) B" using assms unfolding diag_elem_indices_def by simp + +lemma diag_elem_indices_finite: + shows "finite (diag_elem_indices x B)" unfolding diag_elem_indices_def by simp + +text \We can therefore partition the diagonal indices of a matrix $B$ depending on the value +of the diagonal elements. If $B$ admits $p$ elements on its diagonal, then we define bijections +between its set of diagonal elements and the initial segment $[0..p-1]$.\ + +definition dist_el_card where +"dist_el_card B = card (diag_elems B)" + +definition diag_idx_to_el where +"diag_idx_to_el B = (SOME h. bij_betw h {..< dist_el_card B} (diag_elems B))" + +definition diag_el_to_idx where +"diag_el_to_idx B = inv_into {..< dist_el_card B} (diag_idx_to_el B)" + +lemma diag_idx_to_el_bij: + shows "bij_betw (diag_idx_to_el B) {..< dist_el_card B} (diag_elems B)" +proof - + let ?V = "SOME h. bij_betw h {..< dist_el_card B} (diag_elems B)" + have vprop: "bij_betw ?V {..< dist_el_card B} (diag_elems B)" using + someI_ex[of "\h. bij_betw h {..< dist_el_card B} (diag_elems B)"] + diag_elems_finite unfolding dist_el_card_def using bij_betw_from_nat_into_finite by blast + show ?thesis by (simp add:diag_idx_to_el_def vprop) +qed + +lemma diag_el_to_idx_bij: + shows "bij_betw (diag_el_to_idx B) (diag_elems B) {..< dist_el_card B}" + unfolding diag_el_to_idx_def +proof (rule bij_betw_inv_into_subset[of _ _ "diag_elems B"], (simp add: diag_idx_to_el_bij)+) + show "diag_idx_to_el B ` {.. {..< dist_el_card B}" using assms by simp + moreover have "j\ {..< dist_el_card B}" using assms by simp + moreover have "inj_on (diag_idx_to_el B) {.. diag_elems B" +shows "\k \ {..< dist_el_card B}. x = diag_idx_to_el B k" +proof - + have "diag_idx_to_el B ` {.. diag_elems B" +proof - + have "diag_idx_to_el B ` {..i < dim_row B. B$$(i,i) \ Reals" + shows "diag_elems B \ Reals" +proof + fix x + assume "x\ diag_elems B" + hence "\i < dim_row B. x = B $$(i,i)" using assms unfolding diag_elems_def by auto + from this obtain i where "i < dim_row B" "x = B $$ (i,i)" by auto + thus "x \ Reals" using assms by simp +qed + +lemma diag_elems_Re: + fixes B::"complex Matrix.mat" + assumes "\i < (dim_row B). B$$(i,i) \ Reals" + shows "{Re x|x. x\ diag_elems B} = diag_elems B" +proof + show "{complex_of_real (Re x) |x. x \ diag_elems B} \ diag_elems B" + proof + fix x + assume "x \ {complex_of_real (Re x) |x. x \ diag_elems B}" + hence "\y \ diag_elems B. x = Re y" by auto + from this obtain y where "y\ diag_elems B" and "x = Re y" by auto + hence "y = x" using assms diag_elems_real[of B] by auto + thus "x\ diag_elems B" using \y\ diag_elems B\ by simp + qed + show "diag_elems B \ {complex_of_real (Re x) |x. x \ diag_elems B}" + proof + fix x + assume "x \ diag_elems B" + hence "Re x = x" using assms diag_elems_real[of B] by auto + thus "x\ {complex_of_real (Re x) |x. x \ diag_elems B}" using \x\ diag_elems B\ by force + qed +qed + +lemma diag_idx_to_el_real: + fixes B::"complex Matrix.mat" + assumes "\i < dim_row B. B$$(i,i) \ Reals" +and "i < dist_el_card B" +shows "Re (diag_idx_to_el B i) = diag_idx_to_el B i" +proof - + have "diag_idx_to_el B i \ diag_elems B" using diag_idx_to_el_img[of i B] assms by simp + hence "diag_idx_to_el B i \ Reals" using diag_elems_real[of B] assms by auto + thus ?thesis by simp +qed + +lemma diag_elem_indices_empty: + assumes "B \ carrier_mat dimR dimC" + and "i < (dist_el_card B)" +and "j < (dist_el_card B)" +and "i\ j" +shows "diag_elem_indices (diag_idx_to_el B i) B \ + (diag_elem_indices (diag_idx_to_el B j) B) = {}" +proof (rule ccontr) + assume "diag_elem_indices (diag_idx_to_el B i) B \ + diag_elem_indices (diag_idx_to_el B j) B \ {}" + hence "\x. x\ diag_elem_indices (diag_idx_to_el B i) B \ + diag_elem_indices (diag_idx_to_el B j) B" by auto + from this obtain x where + xprop: "x\ diag_elem_indices (diag_idx_to_el B i) B \ + diag_elem_indices (diag_idx_to_el B j) B" by auto + hence "B $$ (x,x) = (diag_idx_to_el B i)" + using diag_elem_indices_elem[of x "diag_idx_to_el B i"] by simp + moreover have "B $$ (x,x) = (diag_idx_to_el B j)" + using diag_elem_indices_elem[of x "diag_idx_to_el B j"] xprop by simp + ultimately have "diag_idx_to_el B i = diag_idx_to_el B j" by simp + hence "i = j" using diag_idx_to_el_less_inj assms by auto + thus False using assms by simp +qed + +lemma (in cpx_sq_mat) diag_elem_indices_disjoint: + assumes "B\ carrier_mat dimR dimC" + shows "disjoint_family_on (\n. diag_elem_indices (diag_idx_to_el B n) B) + {.. {..< dist_el_card B}" and "p\ {..< dist_el_card B}" and "m\ p" + thus "diag_elem_indices (diag_idx_to_el B m) B \ + diag_elem_indices (diag_idx_to_el B p) B = {}" + using diag_elem_indices_empty assms fc_mats_carrier by simp +qed + +lemma diag_elem_indices_union: + assumes "B\ carrier_mat dimR dimC" + shows "(\ i \ {..< dist_el_card B}. diag_elem_indices (diag_idx_to_el B i) B) = + {..< dimR}" +proof + show "(\i {.. (\ii < dist_el_card B. x\ diag_elem_indices (diag_idx_to_el B i) B" by auto + from this obtain i where "i < dist_el_card B" + "x\ diag_elem_indices (diag_idx_to_el B i) B" by auto + hence "x < dimR" using diag_elem_indices_elem[of x _ B] assms by simp + thus "x \ {..< dimR}" by auto + qed +next + show "{.. (\i {..< dimR}" + hence "j < dim_row B" using assms by simp + hence "B$$(j,j) \ diag_elems B" by simp + hence "\k \ {..< dist_el_card B}. B$$(j,j) = diag_idx_to_el B k" + using diag_idx_to_el_less_surj[of "B $$(j,j)"] by simp + from this obtain k where kprop: "k \ {..< dist_el_card B}" + "B$$(j,j) = diag_idx_to_el B k" by auto + hence "j \ diag_elem_indices (diag_idx_to_el B k) B" using \j < dim_row B\ + diag_elem_indices_itself by fastforce + thus "j \ (\iConstruction of measurement outcomes\ + +text \The construction of a projective measurement for a hermitian matrix $A$ is based on the Schur +decomposition $A = U*B*U^\dagger$, where $B$ is diagonal and $U$ is unitary. The columns of $U$ are +normalized and pairwise orthogonal; they are used to construct the projectors associated with +a measurement value\ + +definition (in cpx_sq_mat) project_vecs where +"project_vecs (f::nat \ complex Matrix.vec) N = sum_mat (\i. rank_1_proj (f i)) N" + +lemma (in cpx_sq_mat) project_vecs_dim: + assumes "\i \ N. dim_vec (f i) = dimR" + shows "project_vecs f N \ fc_mats" +proof - + have "project_vecs f N \ carrier_mat dimR dimC" unfolding project_vecs_def + proof (rule sum_mat_carrier) + show "\i. i \ N \ rank_1_proj (f i) \ fc_mats" using assms fc_mats_carrier rank_1_proj_dim + dim_eq rank_1_proj_carrier by fastforce + qed + thus ?thesis using fc_mats_carrier by simp +qed + +definition (in cpx_sq_mat) mk_meas_outcome where +"mk_meas_outcome B U = (\i. (Re (diag_idx_to_el B i), + project_vecs (\i. zero_col U i) (diag_elem_indices (diag_idx_to_el B i) B)))" + +lemma (in cpx_sq_mat) mk_meas_outcome_carrier: + assumes "Complex_Matrix.unitary U" + and "U \ fc_mats" + and "B\ fc_mats" +shows "meas_outcome_prj ((mk_meas_outcome B U) j) \ fc_mats" +proof - + have "project_vecs (\i. zero_col U i) (diag_elem_indices (diag_idx_to_el B j) B) \ fc_mats" + using project_vecs_dim by (simp add: assms(2) zero_col_dim) + thus ?thesis unfolding mk_meas_outcome_def meas_outcome_prj_def by simp +qed + +lemma (in cpx_sq_mat) mk_meas_outcome_sum_id: + assumes "Complex_Matrix.unitary U" + and "U \ fc_mats" + and "B\ fc_mats" +shows "sum_mat (\j. meas_outcome_prj ((mk_meas_outcome B U) j)) + {..<(dist_el_card B)} = 1\<^sub>m dimR" +proof - + have "sum_mat (\j. meas_outcome_prj ((mk_meas_outcome B U) j)) {..<(dist_el_card B)} = + sum_mat (\j. project_vecs (\i. zero_col U i) (diag_elem_indices (diag_idx_to_el B j) B)) + {..<(dist_el_card B)}" + unfolding mk_meas_outcome_def meas_outcome_prj_def by simp + also have "... = sum_mat (\i. rank_1_proj (zero_col U i)) + (\jj. rank_1_proj (zero_col U j) \ fc_mats" using zero_col_dim fc_mats_carrier dim_eq + by (metis assms(2) rank_1_proj_carrier) + show "finite {..i. i \ {.. finite (diag_elem_indices (diag_idx_to_el B i) B)" + using diag_elem_indices_finite by simp + show "disjoint_family_on (\n. diag_elem_indices (diag_idx_to_el B n) B) + {.. {..< dist_el_card B}" and "p\ {..< dist_el_card B}" and "m\ p" + thus "diag_elem_indices (diag_idx_to_el B m) B \ + diag_elem_indices (diag_idx_to_el B p) B = {}" + using diag_elem_indices_empty assms fc_mats_carrier by simp + qed + qed + also have "... = sum_mat (\i. rank_1_proj (zero_col U i)) {..< dimR}" + using diag_elem_indices_union[of B] assms fc_mats_carrier by simp + also have "... = sum_mat (\i. rank_1_proj (Matrix.col U i)) {..< dimR}" + proof (rule sum_mat_cong, simp) + show "\i. i \ {.. rank_1_proj (zero_col U i) \ fc_mats" using dim_eq + by (metis assms(2) local.fc_mats_carrier rank_1_proj_carrier zero_col_dim) + thus "\i. i \ {.. rank_1_proj (Matrix.col U i) \ fc_mats" using dim_eq + by (metis lessThan_iff zero_col_col) + show "\i. i \ {.. rank_1_proj (zero_col U i) = rank_1_proj (Matrix.col U i)" + by (simp add: zero_col_col) + qed + also have "... = 1\<^sub>m dimR" using sum_rank_1_proj_unitary assms by simp + finally show ?thesis . +qed + +lemma (in cpx_sq_mat) make_meas_outcome_prj_ortho: + assumes "Complex_Matrix.unitary U" + and "U \ fc_mats" + and "B\ fc_mats" + and "i < dist_el_card B" + and "j < dist_el_card B" + and "i \ j" +shows "meas_outcome_prj ((mk_meas_outcome B U) i) * + meas_outcome_prj ((mk_meas_outcome B U) j) = 0\<^sub>m dimR dimR" +proof - + define Pi where "Pi = sum_mat (\k. rank_1_proj (zero_col U k)) + (diag_elem_indices (diag_idx_to_el B i) B)" + have sneqi: "meas_outcome_prj (mk_meas_outcome B U i) = Pi" + unfolding mk_meas_outcome_def project_vecs_def Pi_def meas_outcome_prj_def by simp + define Pj where "Pj = sum_mat (\k. rank_1_proj (zero_col U k)) + (diag_elem_indices (diag_idx_to_el B j) B)" + have sneqj: "meas_outcome_prj (mk_meas_outcome B U j) = Pj" + unfolding mk_meas_outcome_def project_vecs_def Pj_def meas_outcome_prj_def by simp + have "Pi * Pj = 0\<^sub>m dimR dimR" unfolding Pi_def + proof (rule sum_mat_left_ortho_zero) + show "finite (diag_elem_indices (diag_idx_to_el B i) B)" + using diag_elem_indices_finite[of _ B] by simp + show km: "\k. k \ diag_elem_indices (diag_idx_to_el B i) B \ + rank_1_proj (zero_col U k) \ fc_mats" using zero_col_dim assms fc_mats_carrier dim_eq + by (metis rank_1_proj_carrier) + show "Pj \ fc_mats" using sneqj assms mk_meas_outcome_carrier by auto + show "\k. k \ diag_elem_indices (diag_idx_to_el B i) B \ + rank_1_proj (zero_col U k) * Pj = 0\<^sub>m dimR dimR" + proof - + fix k + assume "k \ diag_elem_indices (diag_idx_to_el B i) B" + show "rank_1_proj (zero_col U k) * Pj = 0\<^sub>m dimR dimR" unfolding Pj_def + proof (rule sum_mat_right_ortho_zero) + show "finite (diag_elem_indices (diag_idx_to_el B j) B)" + using diag_elem_indices_finite[of _ B] by simp + show "\i. i \ diag_elem_indices (diag_idx_to_el B j) B \ + rank_1_proj (zero_col U i) \ fc_mats" using zero_col_dim assms fc_mats_carrier dim_eq + by (metis rank_1_proj_carrier) + show "rank_1_proj (zero_col U k) \ fc_mats" + by (simp add: km \k \ diag_elem_indices (diag_idx_to_el B i) B\) + show "\i. i \ diag_elem_indices (diag_idx_to_el B j) B \ + rank_1_proj (zero_col U k) * rank_1_proj (zero_col U i) = 0\<^sub>m dimR dimR" + proof - + fix m + assume "m \ diag_elem_indices (diag_idx_to_el B j) B" + hence "m \ k" using \k \ diag_elem_indices (diag_idx_to_el B i) B\ + diag_elem_indices_disjoint[of B] fc_mats_carrier assms unfolding disjoint_family_on_def by auto + have "\i. i \ diag_elem_indices (diag_idx_to_el B j) B \ i < dimR" + using diag_elem_indices_elem fc_mats_carrier assms dim_eq by (metis carrier_matD(1)) + hence "m < dimR" using \m \ diag_elem_indices (diag_idx_to_el B j) B\ by simp + have "\k. k \ diag_elem_indices (diag_idx_to_el B i) B \ k < dimR" + using diag_elem_indices_elem fc_mats_carrier assms dim_eq by (metis carrier_matD(1)) + hence "k < dimR" using \k \ diag_elem_indices (diag_idx_to_el B i) B\ by simp + show "rank_1_proj (zero_col U k) * rank_1_proj (zero_col U m) = 0\<^sub>m dimR dimR" + using rank_1_proj_unitary_ne[of U k m] assms \m < dimR\ \k < dimR\ + by (metis \m \ k\ zero_col_col) + qed + qed + qed + qed + thus ?thesis using sneqi sneqj by simp +qed + +lemma (in cpx_sq_mat) make_meas_outcome_prjectors: + assumes "Complex_Matrix.unitary U" + and "U \ fc_mats" + and "B\ fc_mats" + and "j < dist_el_card B" +shows "projector (meas_outcome_prj ((mk_meas_outcome B U) j))" unfolding projector_def +proof + define Pj where "Pj = sum_mat (\i. rank_1_proj (zero_col U i)) + (diag_elem_indices (diag_idx_to_el B j) B)" + have sneq: "meas_outcome_prj (mk_meas_outcome B U j) = Pj" + unfolding mk_meas_outcome_def project_vecs_def Pj_def meas_outcome_prj_def by simp + moreover have "hermitian Pj" unfolding Pj_def + proof (rule sum_mat_hermitian) + show "finite (diag_elem_indices (diag_idx_to_el B j) B)" + using diag_elem_indices_finite[of _ B] by simp + show "\i\diag_elem_indices (diag_idx_to_el B j) B. hermitian (rank_1_proj (zero_col U i))" + using rank_1_proj_hermitian by simp + show "\i\diag_elem_indices (diag_idx_to_el B j) B. rank_1_proj (zero_col U i) \ fc_mats" + using zero_col_dim fc_mats_carrier dim_eq by (metis assms(2) rank_1_proj_carrier) + qed + ultimately show "hermitian (meas_outcome_prj (mk_meas_outcome B U j))" by simp + have "Pj * Pj = Pj" unfolding Pj_def + proof (rule sum_mat_ortho_square) + show "finite (diag_elem_indices (diag_idx_to_el B j) B)" + using diag_elem_indices_finite[of _ B] by simp + show "\i. i \ diag_elem_indices (diag_idx_to_el B j) B \ + rank_1_proj (zero_col U i) * rank_1_proj (zero_col U i) = rank_1_proj (zero_col U i)" + proof - + fix i + assume imem: "i\ diag_elem_indices (diag_idx_to_el B j) B" + hence "i < dimR" using diag_elem_indices_elem fc_mats_carrier assms dim_eq + by (metis carrier_matD(1)) + hence "zero_col U i = Matrix.col U i" using zero_col_col[of i] by simp + hence "rank_1_proj (zero_col U i) = rank_1_proj (Matrix.col U i)" by simp + moreover have "rank_1_proj (Matrix.col U i) * rank_1_proj (Matrix.col U i) = + rank_1_proj (Matrix.col U i)" by (rule rank_1_proj_unitary_eq, (auto simp add: assms \i < dimR\)) + ultimately show "rank_1_proj (zero_col U i) * rank_1_proj (zero_col U i) = + rank_1_proj (zero_col U i)" by simp + qed + show "\i. i \ diag_elem_indices (diag_idx_to_el B j) B \ + rank_1_proj (zero_col U i) \ fc_mats" + using zero_col_dim assms fc_mats_carrier dim_eq by (metis rank_1_proj_carrier) + have "\i. i \ diag_elem_indices (diag_idx_to_el B j) B \ i < dimR" + using diag_elem_indices_elem fc_mats_carrier assms dim_eq by (metis carrier_matD(1)) + thus "\i ja. + i \ diag_elem_indices (diag_idx_to_el B j) B \ + ja \ diag_elem_indices (diag_idx_to_el B j) B \ + i \ ja \ rank_1_proj (zero_col U i) * rank_1_proj (zero_col U ja) = 0\<^sub>m dimR dimR" + using rank_1_proj_unitary_ne by (simp add: assms(1) assms(2) zero_col_col) + qed + thus "meas_outcome_prj (mk_meas_outcome B U j) * + meas_outcome_prj (mk_meas_outcome B U j) = + meas_outcome_prj (mk_meas_outcome B U j)" + using sneq by simp +qed + +lemma (in cpx_sq_mat) mk_meas_outcome_fst_inj: + assumes "\i < (dim_row B). B$$(i,i) \ Reals" + shows "inj_on (\i. meas_outcome_val ((mk_meas_outcome B U) i)) {.. {.. {..i < (dim_row B). B$$(i,i) \ Reals" + shows "bij_betw (\i. meas_outcome_val ((mk_meas_outcome B U) i)) {..< dist_el_card B} + {Re x|x. x\ diag_elems B}" + unfolding bij_betw_def +proof + have "inj_on (\x. (meas_outcome_val (mk_meas_outcome B U x))) {.. diag_elems B} = diag_elems B" using diag_elems_Re[of B] assms by simp + ultimately show "inj_on (\x. meas_outcome_val (mk_meas_outcome B U x)) + {..i. meas_outcome_val (mk_meas_outcome B U i)) ` {.. diag_elems B}" unfolding meas_outcome_val_def mk_meas_outcome_def + proof + show "(\i. fst (Re (diag_idx_to_el B i), project_vecs (zero_col U) + (diag_elem_indices (diag_idx_to_el B i) B))) ` {.. + {Re x |x. x \ diag_elems B}" + using diag_idx_to_el_bij[of B] bij_betw_apply by fastforce + show "{Re x |x. x \ diag_elems B} + \ (\i. fst (Re (diag_idx_to_el B i), + project_vecs (zero_col U) (diag_elem_indices (diag_idx_to_el B i) B))) ` + {..Projective measurement associated with an observable\ + +definition eigvals where +"eigvals M = (SOME as. char_poly M = (\a\as. [:- a, 1:]) \ length as = dim_row M)" + +lemma eigvals_poly_length: + assumes "(M::complex Matrix.mat) \ carrier_mat n n" + shows "char_poly M = (\a\(eigvals M). [:- a, 1:]) \ length (eigvals M) = dim_row M" +proof - + let ?V = "SOME as. char_poly M = (\a\as. [:- a, 1:]) \ length as = dim_row M" + have vprop: "char_poly M = (\a\?V. [:- a, 1:]) \ length ?V = dim_row M" using + someI_ex[of "\as. char_poly M = (\a\as. [:- a, 1:]) \ length as = dim_row M"] + complex_mat_char_poly_factorizable assms by blast + show ?thesis by (metis (no_types) eigvals_def vprop) +qed + +text \We define the spectrum of a matrix $A$: this is its set of eigenvalues; its elements are +roots of the characteristic polynomial of $A$.\ + +definition spectrum where +"spectrum M = set (eigvals M)" + +lemma spectrum_finite: + shows "finite (spectrum M)" unfolding spectrum_def by simp + +lemma spectrum_char_poly_root: + fixes A::"complex Matrix.mat" + assumes "A\ carrier_mat n n" +and "k \ spectrum A" +shows "poly (char_poly A) k = 0" using eigvals_poly_length[of A n] assms + unfolding spectrum_def eigenvalue_root_char_poly + by (simp add: linear_poly_root) + +lemma spectrum_eigenvalues: + fixes A::"complex Matrix.mat" + assumes "A\ carrier_mat n n" +and "k\ spectrum A" +shows "eigenvalue A k" using eigenvalue_root_char_poly[of A n k] + spectrum_char_poly_root[of A n k] assms by simp + +text \The main result that is used to construct a projective measurement for a Hermitian matrix +is that it is always possible to decompose it as $A = U*B*U^\dagger$, where $B$ is diagonal and +only contains real elements, and $U$ is unitary.\ + +definition hermitian_decomp where +"hermitian_decomp A B U \ similar_mat_wit A B U (Complex_Matrix.adjoint U) \ diagonal_mat B \ + diag_mat B = (eigvals A) \ unitary U \ (\i < dim_row B. B$$(i, i) \ Reals)" + +lemma hermitian_decomp_sim: + assumes "hermitian_decomp A B U" + shows "similar_mat_wit A B U (Complex_Matrix.adjoint U)" using assms + unfolding hermitian_decomp_def by simp + +lemma hermitian_decomp_diag_mat: + assumes "hermitian_decomp A B U" + shows "diagonal_mat B" using assms + unfolding hermitian_decomp_def by simp + +lemma hermitian_decomp_eigenvalues: + assumes "hermitian_decomp A B U" + shows "diag_mat B = (eigvals A)" using assms + unfolding hermitian_decomp_def by simp + +lemma hermitian_decomp_unitary: + assumes "hermitian_decomp A B U" + shows "unitary U" using assms + unfolding hermitian_decomp_def by simp + +lemma hermitian_decomp_real_eigvals: + assumes "hermitian_decomp A B U" + shows "\i < dim_row B. B$$(i, i) \ Reals" using assms + unfolding hermitian_decomp_def by simp + +lemma hermitian_decomp_dim_carrier: + assumes "hermitian_decomp A B U" + shows "B \ carrier_mat (dim_row A) (dim_col A)" using assms + unfolding hermitian_decomp_def similar_mat_wit_def + by (metis (full_types) index_mult_mat(3) index_one_mat(3) insert_subset) + +lemma similar_mat_wit_dim_row: + assumes "similar_mat_wit A B Q R" + shows "dim_row B = dim_row A" using assms Let_def unfolding similar_mat_wit_def + by (meson carrier_matD(1) insert_subset) + +lemma (in cpx_sq_mat) hermitian_schur_decomp: + assumes "hermitian A" + and "A\ fc_mats" +obtains B U where "hermitian_decomp A B U" +proof - + { + have es: "char_poly A = (\ (e :: complex) \ (eigvals A). [:- e, 1:])" + using assms fc_mats_carrier eigvals_poly_length dim_eq 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 < dimR. B$$(i, i) \ Reals)" + using hermitian_eigenvalue_real assms fc_mats_carrier es dim_eq by auto + moreover have "dim_row B = dimR" using assms fc_mats_carrier dim_eq similar_mat_wit_dim_row[of A] + pr by auto + ultimately have "hermitian_decomp A B U" unfolding hermitian_decomp_def by simp + hence "\ B U. hermitian_decomp A B U" by auto + } + thus ?thesis using that by auto +qed + +lemma (in cpx_sq_mat) hermitian_spectrum_real: + assumes "A \ fc_mats" + and "hermitian A" + and "a \ spectrum A" +shows "a \ Reals" +proof - + obtain B U where bu: "hermitian_decomp A B U" using assms hermitian_schur_decomp by auto + hence dimB: "B \ carrier_mat dimR dimR" using assms fc_mats_carrier + dim_eq hermitian_decomp_dim_carrier[of A] by simp + hence Bii: "\i. i < dimR \ B$$(i, i) \ Reals" using hermitian_decomp_real_eigvals[of A B U] + bu assms fc_mats_carrier by simp + have "diag_mat B = (eigvals A)" using bu hermitian_decomp_eigenvalues[of A B] by simp + hence "a \ set (diag_mat B)" using assms unfolding spectrum_def by simp + hence "\i < length (diag_mat B). a = diag_mat B ! i" by (metis in_set_conv_nth) + from this obtain i where "i < length (diag_mat B)" and "a = diag_mat B ! i" by auto + hence "a = B $$ (i,i)" unfolding diag_mat_def by simp + moreover have "i < dimR" using dimB \i < length (diag_mat B)\ unfolding diag_mat_def by simp + ultimately show ?thesis using Bii by simp +qed + +lemma (in cpx_sq_mat) spectrum_ne: + assumes "A\ fc_mats" +and "hermitian A" +shows "spectrum A \ {}" +proof - + obtain B U where bu: "hermitian_decomp A B U" using assms hermitian_schur_decomp by auto + hence dimB: "B \ carrier_mat dimR dimR" using assms fc_mats_carrier + dim_eq hermitian_decomp_dim_carrier[of A] by simp + have "diag_mat B = (eigvals A)" using bu hermitian_decomp_eigenvalues[of A B] by simp + have "B$$(0,0) \ set (diag_mat B)" using dimB npos unfolding diag_mat_def by simp + hence "set (diag_mat B) \ {}" by auto + thus ?thesis unfolding spectrum_def using \diag_mat B = eigvals A\ by auto +qed + +lemma unitary_hermitian_eigenvalues: + fixes U::"complex Matrix.mat" + assumes "unitary U" + and "hermitian U" + and "U \ carrier_mat n n" + and "0 < n" + and "k \ spectrum U" +shows "k \ {-1, 1}" +proof - + have "cpx_sq_mat n n (carrier_mat n n)" by (unfold_locales, (simp add: assms)+) + have "eigenvalue U k" using spectrum_eigenvalues assms by simp + have "k \ Reals" using assms \cpx_sq_mat n n (carrier_mat n n)\ + cpx_sq_mat.hermitian_spectrum_real by simp + hence "conjugate k = k" by (simp add: Reals_cnj_iff) + hence "k\<^sup>2 = 1" using unitary_eigenvalues_norm_square[of U n k] assms + by (simp add: \eigenvalue U k\ power2_eq_square) + thus ?thesis using power2_eq_1_iff by auto +qed + +lemma unitary_hermitian_Re_spectrum: + fixes U::"complex Matrix.mat" + assumes "unitary U" + and "hermitian U" + and "U \ carrier_mat n n" + and "0 < n" + shows "{Re x|x. x\ spectrum U} \ {-1,1}" +proof + fix y + assume "y\ {Re x|x. x\ spectrum U}" + hence "\x \ spectrum U. y = Re x" by auto + from this obtain x where "x\ spectrum U" and "y = Re x" by auto + hence "x\ {-1,1}" using unitary_hermitian_eigenvalues assms by simp + thus "y \ {-1, 1}" using \y = Re x\ by auto +qed + +text \The projective measurement associated with matrix $M$ is obtained from its Schur +decomposition, by considering the number of distinct elements on the resulting diagonal matrix +and constructing the projectors associated with each of them.\ + +type_synonym proj_meas_rep = "nat \ (nat \ measure_outcome)" + +definition proj_meas_size::"proj_meas_rep \ nat" where +"proj_meas_size P = fst P" + +definition proj_meas_outcomes::"proj_meas_rep \ (nat \ measure_outcome)" where +"proj_meas_outcomes P = snd P" + +definition (in cpx_sq_mat) make_pm::"complex Matrix.mat \ proj_meas_rep" where +"make_pm A = (let (B,U,_) = unitary_schur_decomposition A (eigvals A) in + (dist_el_card B, mk_meas_outcome B U))" + +lemma (in cpx_sq_mat) make_pm_decomp: + shows "make_pm A = (proj_meas_size (make_pm A), proj_meas_outcomes (make_pm A))" + unfolding proj_meas_size_def proj_meas_outcomes_def by simp + +lemma (in cpx_sq_mat) make_pm_proj_measurement: + assumes "A \ fc_mats" + and "hermitian A" + and "make_pm A = (n, M)" +shows "proj_measurement n M" +proof - + have es: "char_poly A = (\ (e :: complex) \ (eigvals A). [:- e, 1:])" + using assms fc_mats_carrier eigvals_poly_length dim_eq 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)", auto) + then have "similar_mat_wit A B U (Complex_Matrix.adjoint U) \ diagonal_mat B \ + diag_mat B = (eigvals A) \ unitary U \ (\i < dimR. B$$(i, i) \ Reals)" + using hermitian_eigenvalue_real assms fc_mats_carrier es dim_eq by auto + hence A: "A = U * B * (Complex_Matrix.adjoint U)" and dB: "diagonal_mat B" + and Bii: "\i. i < dimR \ B$$(i, i) \ Reals" + and dimB: "B \ carrier_mat dimR dimR" and dimP: "U \ carrier_mat dimR dimR" and + dimaP: "Complex_Matrix.adjoint U \ carrier_mat dimR dimR" and unit: "unitary U" + unfolding similar_mat_wit_def Let_def using assms fc_mats_carrier by auto + hence mpeq: "make_pm A = (dist_el_card B, mk_meas_outcome B U)" using us Let_def + unfolding make_pm_def by simp + hence "n = dist_el_card B" using assms by simp + have "M = mk_meas_outcome B U" using assms mpeq by simp + show ?thesis unfolding proj_measurement_def + proof (intro conjI) + show "inj_on (\i. meas_outcome_val (M i)) {..n = dist_el_card B\ \M = mk_meas_outcome B U\ Bii fc_mats_carrier dimB by auto + show "\j fc_mats \ projector (meas_outcome_prj (M j))" + proof (intro allI impI conjI) + fix j + assume "j < n" + show "meas_outcome_prj (M j) \ fc_mats" using \M = mk_meas_outcome B U\ assms + fc_mats_carrier \j < n\ \n = dist_el_card B\ dim_eq mk_meas_outcome_carrier + dimB dimP unit by blast + show "projector (meas_outcome_prj (M j))" using make_meas_outcome_prjectors + \M = mk_meas_outcome B U\ + fc_mats_carrier \n = dist_el_card B\ unit \j < n\ dimB dimP dim_eq by blast + qed + show "\ij j \ meas_outcome_prj (M i) * meas_outcome_prj (M j) = + 0\<^sub>m dimR dimR" + proof (intro allI impI) + fix i + fix j + assume "i < n" and "j < n" and "i\ j" + thus "meas_outcome_prj (M i) * meas_outcome_prj (M j) = 0\<^sub>m dimR dimR" + using make_meas_outcome_prj_ortho[of U B i j] assms dimB dimP fc_mats_carrier dim_eq + by (simp add: \M = mk_meas_outcome B U\ \n = dist_el_card B\ unit) + qed + show "sum_mat (\j. meas_outcome_prj (M j)) {..m dimR" using + mk_meas_outcome_sum_id + \M = mk_meas_outcome B U\ fc_mats_carrier dim_eq \n = dist_el_card B\ unit dimB dimP + by blast + qed +qed + +lemma (in cpx_sq_mat) make_pm_proj_measurement': + assumes "A\ fc_mats" + and "hermitian A" +shows "proj_measurement (proj_meas_size (make_pm A)) (proj_meas_outcomes (make_pm A))" + unfolding proj_meas_size_def proj_meas_outcomes_def + by (rule make_pm_proj_measurement[of A], (simp add: assms)+) + +lemma (in cpx_sq_mat) make_pm_projectors: + assumes "A\ fc_mats" + and "hermitian A" +and "i < proj_meas_size (make_pm A)" +shows "projector (meas_outcome_prj (proj_meas_outcomes (make_pm A) i))" +proof - + have "proj_measurement (proj_meas_size (make_pm A)) (proj_meas_outcomes (make_pm A))" + using assms make_pm_proj_measurement' by simp + thus ?thesis using proj_measurement_proj assms by simp +qed + +lemma (in cpx_sq_mat) make_pm_square: + assumes "A\ fc_mats" + and "hermitian A" +and "i < proj_meas_size (make_pm A)" +shows "meas_outcome_prj (proj_meas_outcomes (make_pm A) i) \ fc_mats" +proof - + have "proj_measurement (proj_meas_size (make_pm A)) (proj_meas_outcomes (make_pm A))" + using assms make_pm_proj_measurement' by simp + thus ?thesis using proj_measurement_square assms by simp +qed + + +subsubsection \Properties on the spectrum of a Hermitian matrix\ + +lemma (in cpx_sq_mat) hermitian_schur_decomp': + assumes "hermitian A" + and "A\ fc_mats" +obtains B U where "hermitian_decomp A B U \ + make_pm A = (dist_el_card B, mk_meas_outcome B U)" +proof - + { + have es: "char_poly A = (\ (e :: complex) \ (eigvals A). [:- e, 1:])" + using assms fc_mats_carrier eigvals_poly_length dim_eq 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 < dimR. B$$(i, i) \ Reals)" + using hermitian_eigenvalue_real assms fc_mats_carrier es dim_eq by auto + moreover have "dim_row B = dimR" using assms fc_mats_carrier dim_eq similar_mat_wit_dim_row[of A] + pr by auto + ultimately have "hermitian_decomp A B U" unfolding hermitian_decomp_def by simp + moreover have "make_pm A = (dist_el_card B, mk_meas_outcome B U)" using us Let_def + unfolding make_pm_def hermitian_decomp_def by simp + ultimately have "\ B U. hermitian_decomp A B U \ + make_pm A = (dist_el_card B, mk_meas_outcome B U)" by auto + } + thus ?thesis using that by auto +qed + +lemma (in cpx_sq_mat) spectrum_meas_outcome_val_eq: + assumes "hermitian A" + and "A \ fc_mats" +and "make_pm A = (p, M)" +shows "spectrum A = (\i. meas_outcome_val (M i)) `{..< p}" +proof - + obtain B U where bu: "hermitian_decomp A B U \ + make_pm A = (dist_el_card B, mk_meas_outcome B U)" + using assms hermitian_schur_decomp'[OF assms(1)] by auto + hence "p = dist_el_card B" using assms by simp + have dimB: "B \ carrier_mat dimR dimR" using hermitian_decomp_dim_carrier[of A] dim_eq bu assms + fc_mats_carrier by auto + have Bvals: "diag_mat B = eigvals A" using bu hermitian_decomp_eigenvalues[of A B U] by simp + have Bii: "\i. i < dimR \ B$$(i, i) \ Reals" using bu hermitian_decomp_real_eigvals[of A B U] + dimB by simp + have "diag_elems B = set (eigvals A)" using dimB Bvals diag_elems_set_diag_mat[of B] by simp + have "M = mk_meas_outcome B U" using assms bu by simp + { + fix i + assume "i < p" + have "meas_outcome_val (M i) = Re (diag_idx_to_el B i)" + using \M = mk_meas_outcome B U\ + unfolding meas_outcome_val_def mk_meas_outcome_def by simp + also have "... = diag_idx_to_el B i" using diag_idx_to_el_real dimB \i < p\ + \p = dist_el_card B\ Bii by simp + finally have "meas_outcome_val (M i) = diag_idx_to_el B i" . + } note eq = this + have "bij_betw (diag_idx_to_el B) {..p = dist_el_card B\ + unfolding bij_betw_def by simp + thus ?thesis using eq \diag_elems B = set (eigvals A)\ unfolding spectrum_def by auto +qed + +lemma (in cpx_sq_mat) spectrum_meas_outcome_val_eq': + assumes "hermitian A" + and "A \ fc_mats" +and "make_pm A = (p, M)" +shows "{Re x|x. x\ spectrum A} = (\i. meas_outcome_val (M i)) `{..< p}" +proof + show "{Re x |x. x \ spectrum A} \ (\i. meas_outcome_val (M i)) ` {..i. meas_outcome_val (M i)) ` {.. {Re x |x. x \ spectrum A}" + using spectrum_meas_outcome_val_eq assms by force +qed + +lemma (in cpx_sq_mat) make_pm_eigenvalues: + assumes "A\ fc_mats" + and "hermitian A" +and "i < proj_meas_size (make_pm A)" +shows "meas_outcome_val (proj_meas_outcomes (make_pm A) i) \ spectrum A" + using spectrum_meas_outcome_val_eq[of A] assms make_pm_decomp by auto + +lemma (in cpx_sq_mat) make_pm_spectrum: + assumes "A\ fc_mats" + and "hermitian A" + and "make_pm A = (p,M)" +shows "(\i. meas_outcome_val (proj_meas_outcomes (make_pm A) i)) ` {..< p} = spectrum A" +proof + show "(\x. complex_of_real (meas_outcome_val (proj_meas_outcomes (make_pm A) x))) ` {.. + spectrum A" + using assms make_pm_eigenvalues make_pm_decomp + by (metis (mono_tags, lifting) Pair_inject image_subsetI lessThan_iff) + show "spectrum A \ + (\x. complex_of_real (meas_outcome_val (proj_meas_outcomes (make_pm A) x))) ` {.. fc_mats" +and "make_pm A = (p, M)" +shows "p = card (spectrum A)" +proof - + obtain B U where bu: "hermitian_decomp A B U \ + make_pm A = (dist_el_card B, mk_meas_outcome B U)" + using assms hermitian_schur_decomp'[OF assms(1)] by auto + hence "p = dist_el_card B" using assms by simp + have "spectrum A = set (diag_mat B)" using bu hermitian_decomp_eigenvalues[of A B U] + unfolding spectrum_def by simp + also have "... = diag_elems B" using diag_elems_set_diag_mat[of B] by simp + finally have "spectrum A = diag_elems B" . + thus ?thesis using \p = dist_el_card B\ unfolding dist_el_card_def by simp +qed + +lemma (in cpx_sq_mat) spectrum_size': + assumes "hermitian A" +and "A\ fc_mats" +shows "proj_meas_size (make_pm A) = card (spectrum A)" using spectrum_size + unfolding proj_meas_size_def + by (metis assms fst_conv surj_pair) + +lemma (in cpx_sq_mat) make_pm_projectors': + assumes "hermitian A" + and "A \ fc_mats" + and "a fc_mats" + and "a fc_mats" +proof (rule proj_measurement_square) + show "proj_measurement (proj_meas_size (make_pm A)) (proj_meas_outcomes (make_pm A))" + using make_pm_proj_measurement' assms by simp + show "a < proj_meas_size (make_pm A)" using assms + spectrum_size[of _ "proj_meas_size (make_pm A)"] make_pm_decomp[of A] by simp +qed + +lemma (in cpx_sq_mat) meas_outcome_prj_trace_real: + assumes "hermitian A" + and "density_operator R" + and "R \ fc_mats" + and "A\ fc_mats" + and "a carrier_mat dimR dimR" using fc_mats_carrier assms dim_eq by simp + show "Complex_Matrix.positive R" using assms unfolding density_operator_def by simp + show "projector (meas_outcome_prj (proj_meas_outcomes (make_pm A) a))" using assms + make_pm_projectors' by simp + show "meas_outcome_prj (proj_meas_outcomes (make_pm A) a) \ carrier_mat dimR dimR" + using meas_outcome_prj_carrier assms + dim_eq fc_mats_carrier by simp +qed + +lemma (in cpx_sq_mat) sum_over_spectrum: + assumes "A\ fc_mats" +and "hermitian A" +and "make_pm A = (p, M)" +shows "(\ y \ spectrum A. f y) = (\ i < p. f (meas_outcome_val (M i)))" +proof (rule sum.reindex_cong) +show "spectrum A =(\x. (meas_outcome_val (M x)))` {..< p}" + using spectrum_meas_outcome_val_eq assms by simp + show "inj_on (\x. complex_of_real (meas_outcome_val (M x))) {..x. (meas_outcome_val (M x))) {.. fc_mats" +and "hermitian A" +and "make_pm A = (p, M)" +shows "(\ y \ {Re x|x. x \ spectrum A}. f y) = (\ i < p. f (meas_outcome_val (M i)))" +proof (rule sum.reindex_cong) + show "{Re x|x. x \ spectrum A} =(\x. (meas_outcome_val (M x)))` {..< p}" + using spectrum_meas_outcome_val_eq' assms by simp + show "inj_on (\x. (meas_outcome_val (M x))) {..When a matrix $A$ is decomposed into a projective measurement $\{(\lambda_a, \pi_a)\}$, it +can be recovered by the formula $A = \sum \lambda_a \pi_a$.\ + +lemma (in cpx_sq_mat) make_pm_sum: + assumes "A \ fc_mats" + and "hermitian A" + and "make_pm A = (p, M)" +shows "sum_mat (\i. (meas_outcome_val (M i)) \\<^sub>m meas_outcome_prj (M i)) {..< p} = A" +proof - + have es: "char_poly A = (\ (e :: complex) \ (eigvals A). [:- e, 1:])" + using assms fc_mats_carrier eigvals_poly_length dim_eq 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)", auto) + then have "similar_mat_wit A B U (Complex_Matrix.adjoint U) \ diagonal_mat B \ + diag_mat B = (eigvals A) + \ unitary U \ (\i < dimR. B$$(i, i) \ Reals)" + using hermitian_eigenvalue_real assms fc_mats_carrier es dim_eq by auto + hence A: "A = U * B * (Complex_Matrix.adjoint U)" and dB: "diagonal_mat B" + and Bii: "\i. i < dimR \ B$$(i, i) \ Reals" + and dimB: "B \ carrier_mat dimR dimR" and dimP: "U \ carrier_mat dimR dimR" and + dimaP: "Complex_Matrix.adjoint U \ carrier_mat dimR dimR" and unit: "unitary U" + unfolding similar_mat_wit_def Let_def using assms fc_mats_carrier by auto + hence mpeq: "make_pm A = (dist_el_card B, mk_meas_outcome B U)" using us Let_def + unfolding make_pm_def by simp + hence "p = dist_el_card B" using assms by simp + have "M = mk_meas_outcome B U" using assms mpeq by simp + have "sum_mat (\i. meas_outcome_val (M i) \\<^sub>m meas_outcome_prj (M i)) {..< p} = + sum_mat (\j. Re (diag_idx_to_el B j)\\<^sub>m project_vecs (\i. zero_col U i) + (diag_elem_indices (diag_idx_to_el B j) B)) {..<(dist_el_card B)}" + using \p = dist_el_card B\ + \M = mk_meas_outcome B U\ unfolding meas_outcome_val_def meas_outcome_prj_def + mk_meas_outcome_def by simp + also have "... = sum_mat + (\j. sum_mat (\i. (Re (diag_idx_to_el B j)) \\<^sub>m rank_1_proj (zero_col U i)) + (diag_elem_indices (diag_idx_to_el B j) B)) {..i. i \ {.. + complex_of_real (Re (diag_idx_to_el B i)) \\<^sub>m + sum_mat (\i. rank_1_proj (zero_col U i)) (diag_elem_indices (diag_idx_to_el B i) B) + \ fc_mats" using assms fc_mats_carrier dimP project_vecs_def project_vecs_dim zero_col_dim + dim_eq by auto + show "\i. i \ {.. + sum_mat (\ia. complex_of_real (Re (diag_idx_to_el B i)) \\<^sub>m rank_1_proj (zero_col U ia)) + (diag_elem_indices (diag_idx_to_el B i) B) \ fc_mats" using assms fc_mats_carrier dimP + project_vecs_def project_vecs_dim zero_col_dim dim_eq + by (metis (no_types, lifting) rank_1_proj_carrier cpx_sq_mat_smult sum_mat_carrier) + show "\j. j \ {.. + (Re (diag_idx_to_el B j)) \\<^sub>m sum_mat (\i. rank_1_proj (zero_col U i)) + (diag_elem_indices (diag_idx_to_el B j) B) = + sum_mat (\i. complex_of_real (Re (diag_idx_to_el B j)) \\<^sub>m rank_1_proj (zero_col U i)) + (diag_elem_indices (diag_idx_to_el B j) B)" + proof - + fix j + assume "j \ {..\<^sub>m sum_mat (\i. rank_1_proj (zero_col U i)) + (diag_elem_indices (diag_idx_to_el B j) B) = + sum_mat (\i. (Re (diag_idx_to_el B j)) \\<^sub>m rank_1_proj (zero_col U i)) + (diag_elem_indices (diag_idx_to_el B j) B)" + proof (rule smult_sum_mat) + show "finite (diag_elem_indices (diag_idx_to_el B j) B)" + using diag_elem_indices_finite[of _ B] by simp + show "\i. i \ diag_elem_indices (diag_idx_to_el B j) B \ + rank_1_proj (zero_col U i) \ fc_mats" + using dim_eq by (metis dimP local.fc_mats_carrier rank_1_proj_carrier zero_col_dim) + qed + qed + qed + also have "... = sum_mat + (\j. sum_mat (\ia. (diag_mat B ! ia) \\<^sub>m rank_1_proj (zero_col U ia)) + (diag_elem_indices (diag_idx_to_el B j) B)) {..i. i \ {.. + sum_mat (\ia. complex_of_real (Re (diag_idx_to_el B i)) \\<^sub>m rank_1_proj (zero_col U ia)) + (diag_elem_indices (diag_idx_to_el B i) B) \ fc_mats" using assms fc_mats_carrier dimP + project_vecs_def project_vecs_dim zero_col_dim dim_eq + by (metis (no_types, lifting) rank_1_proj_carrier cpx_sq_mat_smult sum_mat_carrier) + show "\i. i \ {.. + local.sum_mat (\ia. (diag_mat B ! ia) \\<^sub>m rank_1_proj (zero_col U ia)) + (diag_elem_indices (diag_idx_to_el B i) B) \ fc_mats" using assms fc_mats_carrier dimP + project_vecs_def project_vecs_dim zero_col_dim dim_eq + by (metis (no_types, lifting) rank_1_proj_carrier cpx_sq_mat_smult sum_mat_carrier) + show "\i. i \ {.. + sum_mat (\ia. (Re (diag_idx_to_el B i)) \\<^sub>m rank_1_proj (zero_col U ia)) + (diag_elem_indices (diag_idx_to_el B i) B) = + sum_mat (\ia. (diag_mat B ! ia) \\<^sub>m rank_1_proj (zero_col U ia)) + (diag_elem_indices (diag_idx_to_el B i) B)" + proof - + fix i + assume "i\ {..< dist_el_card B}" + show "sum_mat (\ia. (Re (diag_idx_to_el B i)) \\<^sub>m rank_1_proj (zero_col U ia)) + (diag_elem_indices (diag_idx_to_el B i) B) = + sum_mat (\ia. (diag_mat B ! ia) \\<^sub>m rank_1_proj (zero_col U ia)) + (diag_elem_indices (diag_idx_to_el B i) B)" + proof (rule sum_mat_cong) + show "finite (diag_elem_indices (diag_idx_to_el B i) B)" + using diag_elem_indices_finite[of _ B] by simp + show "\ia. ia \ diag_elem_indices (diag_idx_to_el B i) B \ + (Re (diag_idx_to_el B i)) \\<^sub>m rank_1_proj (zero_col U ia) \ fc_mats" + using assms fc_mats_carrier dimP project_vecs_def project_vecs_dim zero_col_dim dim_eq + by (metis (no_types, lifting) rank_1_proj_carrier cpx_sq_mat_smult) + show "\ia. ia \ diag_elem_indices (diag_idx_to_el B i) B \ + (diag_mat B !ia) \\<^sub>m rank_1_proj (zero_col U ia) \ fc_mats" + using assms fc_mats_carrier dimP project_vecs_def project_vecs_dim zero_col_dim dim_eq + by (metis (no_types, lifting) rank_1_proj_carrier cpx_sq_mat_smult) + show "\ia. ia \ diag_elem_indices (diag_idx_to_el B i) B \ + (Re (diag_idx_to_el B i)) \\<^sub>m rank_1_proj (zero_col U ia) = + (diag_mat B ! ia) \\<^sub>m rank_1_proj (zero_col U ia)" + proof - + fix ia + assume ia: "ia \ diag_elem_indices (diag_idx_to_el B i) B" + hence "ia < dim_row B" using diag_elem_indices_elem[of ia _ B] by simp + have "Re (diag_idx_to_el B i) = Re (B $$ (ia, ia))" + using diag_elem_indices_elem[of ia _ B] ia by simp + also have "... = B $$ (ia, ia)" using Bii using \ia < dim_row B\ dimB of_real_Re by blast + also have "... = diag_mat B ! ia" using \ia < dim_row B\ unfolding diag_mat_def by simp + finally have "Re (diag_idx_to_el B i) = diag_mat B ! ia" . + thus "(Re (diag_idx_to_el B i)) \\<^sub>m rank_1_proj (zero_col U ia) = + (diag_mat B ! ia) \\<^sub>m rank_1_proj (zero_col U ia)" by simp + qed + qed + qed + qed + also have "... = sum_mat + (\i. (diag_mat B ! i) \\<^sub>m rank_1_proj (zero_col U i)) + (\jj. (diag_mat B ! j) \\<^sub>m rank_1_proj (zero_col U j) \ fc_mats" using assms fc_mats_carrier dimP + project_vecs_def project_vecs_dim zero_col_dim dim_eq + by (metis (no_types, lifting) rank_1_proj_carrier cpx_sq_mat_smult) + show "\i. i \ {.. finite (diag_elem_indices (diag_idx_to_el B i) B)" + by (simp add: diag_elem_indices_finite) + show "disjoint_family_on (\n. diag_elem_indices (diag_idx_to_el B n) B) + {..i. (diag_mat B ! i) \\<^sub>m rank_1_proj (zero_col U i)) {..< dimR}" + using diag_elem_indices_union[of B] dimB dim_eq by simp + also have "... = sum_mat (\i. (diag_mat B ! i) \\<^sub>mrank_1_proj (Matrix.col U i)) {..< dimR}" + proof (rule sum_mat_cong, simp) + show res: "\i. i \ {.. (diag_mat B ! i) \\<^sub>m rank_1_proj (zero_col U i) \ fc_mats" + using assms fc_mats_carrier dimP project_vecs_def project_vecs_dim zero_col_dim dim_eq + by (metis (no_types, lifting) rank_1_proj_carrier cpx_sq_mat_smult) + show "\i. i \ {.. (diag_mat B ! i) \\<^sub>m rank_1_proj (Matrix.col U i) \ fc_mats" + using assms fc_mats_carrier dimP project_vecs_def project_vecs_dim zero_col_dim + by (metis res lessThan_iff zero_col_col) + show "\i. i \ {.. (diag_mat B ! i) \\<^sub>m rank_1_proj (zero_col U i) = + (diag_mat B ! i) \\<^sub>m rank_1_proj (Matrix.col U i)" + by (simp add: zero_col_col) + qed + also have "... = 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 + also have "... = A" using A by simp + finally show ?thesis . +qed + +lemma (in cpx_sq_mat) trace_hermitian_pos_real: + fixes f::"'a \ real" + assumes "hermitian A" + and "Complex_Matrix.positive R" + and "A \ fc_mats" + and "R \ fc_mats" +shows "Complex_Matrix.trace (R * A) = + Re (Complex_Matrix.trace (R * A))" +proof - + define prj_mems where "prj_mems = make_pm A" + define p where "p = proj_meas_size prj_mems" + define meas where "meas = proj_meas_outcomes prj_mems" + have tre: "Complex_Matrix.trace (R * A) = + Complex_Matrix.trace (R * + sum_mat (\i. (meas_outcome_val (meas i)) \\<^sub>m meas_outcome_prj (meas i)) {..< p})" + using make_pm_sum assms meas_def p_def proj_meas_size_def proj_meas_outcomes_def prj_mems_def + meas_outcome_val_def meas_outcome_prj_def by auto + also have "... = Re (Complex_Matrix.trace (R * + sum_mat (\i. (meas_outcome_val (meas i)) \\<^sub>m meas_outcome_prj (meas i)) {..< p}))" + proof (rule trace_sum_mat_proj_pos_real, (auto simp add: assms)) + fix i + assume "i < p" + thus "projector (meas_outcome_prj (meas i))" using make_pm_projectors assms + unfolding p_def meas_def prj_mems_def by simp + show "meas_outcome_prj (meas i) \ fc_mats" using make_pm_square assms \i < p\ + unfolding p_def meas_def prj_mems_def by simp + qed + also have "... = Re (Complex_Matrix.trace (R * A))" using tre by simp + finally show ?thesis . +qed + +lemma (in cpx_sq_mat) hermitian_Re_spectrum: + assumes "hermitian A" +and "A\ fc_mats" +and "{Re x |x. x \ spectrum A} = {a,b}" +shows "spectrum A = {complex_of_real a, complex_of_real b}" +proof + have ar: "\(a::complex). a \ spectrum A \ Re a = a" using hermitian_spectrum_real assms by simp + show "spectrum A \ {complex_of_real a, complex_of_real b}" + proof + fix x + assume "x\ spectrum A" + hence "Re x = x" using ar by simp + have "Re x \ {a,b}" using \x\ spectrum A\ assms by blast + thus "x \ {complex_of_real a, complex_of_real b}" using \Re x = x\ by auto + qed + show "{complex_of_real a, complex_of_real b} \ spectrum A" + proof + fix x + assume "x \ {complex_of_real a, complex_of_real b}" + hence "x \ {complex_of_real (Re x) |x. x \ spectrum A}" using assms + proof - + have "\r. r \ {a, b} \ (\c. r = Re c \ c \ spectrum A)" + using \{Re x |x. x \ spectrum A} = {a, b}\ by blast + then show ?thesis + using \x \ {complex_of_real a, complex_of_real b}\ by blast + qed + thus "x\ spectrum A" using ar by auto + qed +qed + + +subsubsection \Similar properties for eigenvalues rather than spectrum indices\ + +text \In this part we go the other way round: given an eigenvalue of $A$, \verb+spectrum_to_pm_idx+ +permits to retrieve its index in the associated projective measurement\ + +definition (in cpx_sq_mat) spectrum_to_pm_idx + where "spectrum_to_pm_idx A x = (let (B,U,_) = unitary_schur_decomposition A (eigvals A) in + diag_el_to_idx B x)" + +lemma (in cpx_sq_mat) spectrum_to_pm_idx_bij: +assumes "hermitian A" + and "A\ fc_mats" +shows "bij_betw (spectrum_to_pm_idx A) (spectrum A) {..< card (spectrum A)}" +proof - + define p where "p = proj_meas_size (make_pm A)" + define M where "M = proj_meas_outcomes (make_pm A)" + have es: "char_poly A = (\ (e :: complex) \ (eigvals A). [:- e, 1:])" + using assms fc_mats_carrier eigvals_poly_length dim_eq 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) \ + diag_mat B = (eigvals A)" + using hermitian_eigenvalue_real assms fc_mats_carrier es dim_eq by auto + have "(p,M) = make_pm A" unfolding p_def M_def using make_pm_decomp by simp + hence "p = dist_el_card B" using assms us unfolding make_pm_def by simp + have dimB: "B \ carrier_mat dimR dimR" using dim_eq pr assms + fc_mats_carrier unfolding similar_mat_wit_def by auto + have Bvals: "diag_mat B = eigvals A" using pr hermitian_decomp_eigenvalues[of A B U] by simp + have "diag_elems B = spectrum A" unfolding spectrum_def using dimB Bvals + diag_elems_set_diag_mat[of B] by simp + moreover have "dist_el_card B = card (spectrum A)" using spectrum_size[of A p M] assms + \(p,M) = make_pm A\ \p = dist_el_card B\ by simp + ultimately show "bij_betw (spectrum_to_pm_idx A) (spectrum A) {..< card (spectrum A)}" + using diag_el_to_idx_bij us unfolding spectrum_to_pm_idx_def Let_def + by (metis (mono_tags, lifting) bij_betw_cong case_prod_conv) +qed + +lemma (in cpx_sq_mat) spectrum_to_pm_idx_lt_card: +assumes "A\ fc_mats" + and "hermitian A" +and "a\ spectrum A" +shows "spectrum_to_pm_idx A a < card (spectrum A)" using spectrum_to_pm_idx_bij[of A] assms + by (meson bij_betw_apply lessThan_iff) + +lemma (in cpx_sq_mat) spectrum_to_pm_idx_inj: +assumes "hermitian A" + and "A\ fc_mats" +shows "inj_on (spectrum_to_pm_idx A) (spectrum A)" using assms spectrum_to_pm_idx_bij + unfolding bij_betw_def by simp + +lemma (in cpx_sq_mat) spectrum_meas_outcome_val_inv: +assumes "A\ fc_mats" + and "hermitian A" +and "make_pm A = (p,M)" +and "i < p" +shows "spectrum_to_pm_idx A (meas_outcome_val (M i)) = i" +proof - + have es: "char_poly A = (\ (e :: complex) \ (eigvals A). [:- e, 1:])" + using assms fc_mats_carrier eigvals_poly_length dim_eq 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) \ + diag_mat B = (eigvals A) \ (\i < dimR. B$$(i, i) \ Reals)" + using hermitian_eigenvalue_real assms fc_mats_carrier es dim_eq by auto + have "dim_row B = dimR" using assms fc_mats_carrier dim_eq similar_mat_wit_dim_row[of A] + pr by auto + hence "(p,M) = (dist_el_card B, mk_meas_outcome B U)" using assms us + unfolding make_pm_def by simp + hence "M = mk_meas_outcome B U" by simp + have "meas_outcome_val (M i) = Re (diag_idx_to_el B i)" + using \M = mk_meas_outcome B U\ unfolding mk_meas_outcome_def + meas_outcome_val_def by simp + also have "... = diag_idx_to_el B i" using pr + \(p, M) = (dist_el_card B, mk_meas_outcome B U)\ \dim_row B = dimR\ assms + diag_idx_to_el_real by auto + finally have "meas_outcome_val (M i) = diag_idx_to_el B i" . + hence "spectrum_to_pm_idx A (meas_outcome_val (M i)) = + spectrum_to_pm_idx A (diag_idx_to_el B i)" by simp + also have "... = diag_el_to_idx B (diag_idx_to_el B i)" unfolding spectrum_to_pm_idx_def + using us by simp + also have "... = i" using assms unfolding diag_el_to_idx_def + using \(p, M) = (dist_el_card B, mk_meas_outcome B U)\ bij_betw_inv_into_left + diag_idx_to_el_bij by fastforce + finally show ?thesis . +qed + +lemma (in cpx_sq_mat) meas_outcome_val_spectrum_inv: + assumes "A\ fc_mats" + and "hermitian A" +and "x\ spectrum A" +and "make_pm A = (p,M)" +shows "meas_outcome_val (M (spectrum_to_pm_idx A x)) = x" +proof - + have es: "char_poly A = (\ (e :: complex) \ (eigvals A). [:- e, 1:])" + using assms fc_mats_carrier eigvals_poly_length dim_eq 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 < dimR. B$$(i, i) \ Reals)" + using hermitian_eigenvalue_real assms fc_mats_carrier es dim_eq by auto + have "dim_row B = dimR" using assms fc_mats_carrier dim_eq similar_mat_wit_dim_row[of A] + pr by auto + hence "(p,M) = (dist_el_card B, mk_meas_outcome B U)" using assms us + unfolding make_pm_def by simp + hence "M = mk_meas_outcome B U" by simp + have "diag_mat B = (eigvals A)" using pr by simp + hence "x \ set (diag_mat B)" using \diag_mat B = eigvals A\ assms unfolding spectrum_def by simp + hence "x \ diag_elems B" using diag_elems_set_diag_mat[of B] by simp + hence "diag_idx_to_el B (diag_el_to_idx B x) = x" unfolding diag_el_to_idx_def + by (meson bij_betw_inv_into_right diag_idx_to_el_bij) + moreover have "spectrum_to_pm_idx A x = diag_el_to_idx B x" unfolding spectrum_to_pm_idx_def + using us by simp + moreover have "meas_outcome_val (M (spectrum_to_pm_idx A x)) = + Re (diag_idx_to_el B (diag_el_to_idx B x))" using \M = mk_meas_outcome B U\ + unfolding mk_meas_outcome_def meas_outcome_val_def by (simp add: calculation(2)) + ultimately show ?thesis by simp +qed + +definition (in cpx_sq_mat) eigen_projector where +"eigen_projector A a = + meas_outcome_prj ((proj_meas_outcomes (make_pm A)) (spectrum_to_pm_idx A a))" + +lemma (in cpx_sq_mat) eigen_projector_carrier: + assumes "A\ fc_mats" + and "a\ spectrum A" + and "hermitian A" +shows "eigen_projector A a \ fc_mats" unfolding eigen_projector_def + using meas_outcome_prj_carrier[of A "spectrum_to_pm_idx A a"] + spectrum_to_pm_idx_lt_card[of A a] assms by simp + +text \We obtain the following result, which is similar to \verb+make_pm_sum+ but with a sum on +the elements of the spectrum of Hermitian matrix $A$, which is a more standard statement of the +spectral decomposition theorem.\ + +lemma (in cpx_sq_mat) make_pm_sum': + assumes "A \ fc_mats" + and "hermitian A" +shows "sum_mat (\a. a \\<^sub>m (eigen_projector A a)) (spectrum A) = A" +proof - + define p where "p = proj_meas_size (make_pm A)" + define M where "M = proj_meas_outcomes (make_pm A)" + have "(p,M) = make_pm A" unfolding p_def M_def using make_pm_decomp by simp + define g where + "g = (\i. (if i < p + then complex_of_real (meas_outcome_val (M i)) \\<^sub>m meas_outcome_prj (M i) + else (0\<^sub>m dimR dimC)))" + have g: "\x. g x \ fc_mats" + proof + fix x + show "g x \ fc_mats" + proof (cases "x < p") + case True + hence "(meas_outcome_val (M x)) \\<^sub>m meas_outcome_prj (M x) \ fc_mats" + using meas_outcome_prj_carrier + spectrum_size assms cpx_sq_mat_smult make_pm_proj_measurement proj_measurement_square + \(p,M) = make_pm A\ by metis + then show ?thesis unfolding g_def using True by simp + next + case False + then show ?thesis unfolding g_def using zero_mem by simp + qed + qed + define h where "h = (\a. (if a \ (spectrum A) then a \\<^sub>m eigen_projector A a else (0\<^sub>m dimR dimC)))" + have h: "\x. h x \ fc_mats" + proof + fix x + show "h x \ fc_mats" + proof (cases "x\ spectrum A") + case True + then show ?thesis unfolding h_def using eigen_projector_carrier[of A x] assms True + by (simp add: cpx_sq_mat_smult) + next + case False + then show ?thesis unfolding h_def using zero_mem by simp + qed + qed + have "inj_on (spectrum_to_pm_idx A) (spectrum A)" using assms spectrum_to_pm_idx_inj by simp + moreover have "{..(p,M) = make_pm A\ + spectrum_to_pm_idx_bij spectrum_size unfolding bij_betw_def + by (metis assms(1) assms(2)) + moreover have "\x. x \ spectrum A \ g (spectrum_to_pm_idx A x) = h x" + proof - + fix a + assume "a \ spectrum A" + hence "Re a = a" using hermitian_spectrum_real assms by simp + have "spectrum_to_pm_idx A a < p" using spectrum_to_pm_idx_lt_card[of A] spectrum_size assms + \a \ spectrum A\ \(p,M) = make_pm A\ by metis + have "g (spectrum_to_pm_idx A a) = + (meas_outcome_val (M (spectrum_to_pm_idx A a))) \\<^sub>m + meas_outcome_prj (M (spectrum_to_pm_idx A a))" + using \spectrum_to_pm_idx A a < p\ unfolding g_def by simp + also have "... = a \\<^sub>m meas_outcome_prj (M (spectrum_to_pm_idx A a))" + using meas_outcome_val_spectrum_inv[of A "Re a"] \Re a = a\ assms \a \ spectrum A\ + \(p,M) = make_pm A\ by metis + also have "... = h a" using \a \ spectrum A\ unfolding eigen_projector_def M_def h_def by simp + finally show "g (spectrum_to_pm_idx A a) = h a" . + qed + ultimately have "sum_mat h (spectrum A) = + sum_mat g (spectrum_to_pm_idx A ` spectrum A)" unfolding sum_mat_def + using sum_with_reindex_cong[symmetric, of g h "spectrum_to_pm_idx A" "spectrum A" "{..< p}"] + g h by simp + also have "... = sum_mat g {..< p}" using \{.. by simp + also have "... = sum_mat (\i. (meas_outcome_val (M i)) \\<^sub>m meas_outcome_prj (M i)) {.. {..< p}" + hence "i < p" by simp + show "g i \ fc_mats" using g by simp + show "g i = (meas_outcome_val (M i)) \\<^sub>m meas_outcome_prj (M i)" unfolding g_def + using \i < p\ by simp + show "(meas_outcome_val (M i)) \\<^sub>m meas_outcome_prj (M i) \ fc_mats" + using meas_outcome_prj_carrier spectrum_size assms cpx_sq_mat_smult + make_pm_proj_measurement proj_measurement_square \i < p\ \(p,M) = make_pm A\ by metis + qed + also have "... = A" using make_pm_sum assms \(p,M) = make_pm A\ unfolding g_def by simp + finally have "sum_mat h (spectrum A) = A" . + moreover have "sum_mat h (spectrum A) = sum_mat (\a. a \\<^sub>m (eigen_projector A a)) (spectrum A)" + proof (rule sum_mat_cong) + show "finite (spectrum A)" using spectrum_finite[of A] by simp + fix i + assume "i\ spectrum A" + thus "h i = i \\<^sub>m eigen_projector A i" unfolding h_def by simp + show "h i \ fc_mats" using h by simp + show "i \\<^sub>m eigen_projector A i \ fc_mats" using eigen_projector_carrier[of A i] assms + \i\ spectrum A\ by (metis \h i = i \\<^sub>m eigen_projector A i\ h) + qed + ultimately show ?thesis by simp +qed + + + +end \ No newline at end of file diff --git a/thys/Projective_Measurements/ROOT b/thys/Projective_Measurements/ROOT new file mode 100644 --- /dev/null +++ b/thys/Projective_Measurements/ROOT @@ -0,0 +1,14 @@ +chapter AFP + +session Projective_Measurements (AFP) = "HOL-Probability" + + options [timeout = 600] + sessions + Isabelle_Marries_Dirac + QHLProver + "HOL-Types_To_Sets" + theories + Linear_Algebra_Complements + Projective_Measurements + CHSH_Inequality + document_files + "root.tex" diff --git a/thys/Projective_Measurements/document/root.tex b/thys/Projective_Measurements/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Projective_Measurements/document/root.tex @@ -0,0 +1,59 @@ +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} + +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +%\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage{eurosym} + %for \ + +%\usepackage[only,bigsqcap]{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{Projective-Measurements} +\author{Mnacho} +\maketitle + +\tableofcontents + +% 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: