# Theory Projective_Measurements

(*
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⇩m dimR dimR) ∧
sum_mat (λj. meas_outcome_prj (M j)) {..< n} = 1⇩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⇩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⇩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⇩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)  ⋅⇩m (1⇩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) ⋅⇩m 1⇩m n) =
(complex_of_real ((1::real)/n)) *  (Complex_Matrix.trace ((1⇩m n)::complex Matrix.mat))"
using one_carrier_mat trace_smult[of "(1⇩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) ⋅⇩m 1⇩m n) =  1" .
next
show "Complex_Matrix.positive (complex_of_real (1 / real n) ⋅⇩m 1⇩m n)"
by (rule positive_smult, (auto simp add: positive_one less_eq_complex_def))
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)))) ⋅⇩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) ⋅⇩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))) ⋅⇩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 add: less_eq_complex_def)
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 less_eq_complex_def)
show "Complex_Matrix.positive (P * R * P)" using assms
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))) ⋅⇩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..<dim_row B])" proof fix x assume "x ∈ {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..<dim_row B])" by auto qed next show "set (map (λi. B$$ (i, i)) [0..<dim_row B]) ⊆ {B $$(i, i) |i. i < dim_row B}" proof fix x assume "x ∈ set (map (λi. B$$ (i, i)) [0..<dim_row B])"
thus "x ∈ {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} = diag_elems B" by (simp add: diag_idx_to_el_bij bij_betw_imp_surj_on) qed lemma diag_idx_to_el_less_inj: assumes "i < dist_el_card B" and "j < dist_el_card B" and "diag_idx_to_el B i = diag_idx_to_el B j" shows "i = j" proof - have "i ∈ {..< 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) {..<dist_el_card B}" using diag_idx_to_el_bij[of B] unfolding bij_betw_def by simp ultimately show ?thesis by (meson assms(3) inj_on_contraD) qed lemma diag_idx_to_el_less_surj: assumes "x∈ diag_elems B" shows "∃k ∈ {..< dist_el_card B}. x = diag_idx_to_el B k" proof - have "diag_idx_to_el B  {..<dist_el_card B} = diag_elems B" using diag_idx_to_el_bij[of B] unfolding bij_betw_def by simp thus ?thesis using assms by auto qed lemma diag_idx_to_el_img: assumes "k < dist_el_card B" shows "diag_idx_to_el B k ∈ diag_elems B" proof - have "diag_idx_to_el B  {..<dist_el_card B} = diag_elems B" using diag_idx_to_el_bij[of B] unfolding bij_betw_def by simp thus ?thesis using assms by auto qed lemma diag_elems_real: fixes B::"complex Matrix.mat" assumes "∀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}" unfolding disjoint_family_on_def
proof (intro ballI impI)
fix p m
assume "m∈ {..< 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<dist_el_card B. diag_elem_indices (diag_idx_to_el B i) B) ⊆ {..<dimR}"
proof
fix x
assume "x ∈ (⋃i<dist_el_card B. diag_elem_indices (diag_idx_to_el B i) B)"
hence "∃i < 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 "{..<dimR} ⊆ (⋃i<dist_el_card B. diag_elem_indices (diag_idx_to_el B i) B)"
proof
fix j
assume "j∈ {..< 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 ∈ (⋃i<dist_el_card B. diag_elem_indices (diag_idx_to_el B i) B)"
using kprop by auto
qed
qed

subsubsection ‹Construction 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⇩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))
(⋃j<dist_el_card B. diag_elem_indices (diag_idx_to_el B j) B)"
unfolding project_vecs_def sum_mat_def
proof (rule disj_family_sum_with[symmetric])
show "∀j. 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 {..<dist_el_card B}" by simp
show "⋀i. i ∈ {..<dist_el_card B} ⟹ 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}"
unfolding disjoint_family_on_def
proof (intro ballI impI)
fix p m
assume "m∈ {..< 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 ∈ {..<dimR} ⟹ 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 ∈ {..<dimR} ⟹ rank_1_proj (Matrix.col U i) ∈ fc_mats" using dim_eq
by (metis lessThan_iff zero_col_col)
show "⋀i. i ∈ {..<dimR} ⟹ rank_1_proj (zero_col U i) = rank_1_proj (Matrix.col U i)"
qed
also have "... = 1⇩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⇩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⇩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⇩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⇩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⇩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⇩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⇩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)) {..<dist_el_card B}" unfolding inj_on_def proof (intro ballI impI) fix x y assume "x ∈ {..<dist_el_card B}" and "y ∈ {..<dist_el_card B}" and "meas_outcome_val (mk_meas_outcome B U x) = meas_outcome_val (mk_meas_outcome B U y)" note xy = this hence "diag_idx_to_el B x = Re (diag_idx_to_el B x)" using assms diag_idx_to_el_real by simp also have "... = Re (diag_idx_to_el B y)" using xy unfolding mk_meas_outcome_def meas_outcome_val_def by simp also have "... = diag_idx_to_el B y" using assms diag_idx_to_el_real xy by simp finally have "diag_idx_to_el B x = diag_idx_to_el B y" . thus "x = y " using diag_idx_to_el_less_inj xy by simp qed lemma (in cpx_sq_mat) mk_meas_outcome_fst_bij: assumes "∀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))) {..<dist_el_card B}"
using assms mk_meas_outcome_fst_inj by simp
moreover have  "{Re x|x. 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))
{..<dist_el_card B}" by simp
show "(λi. meas_outcome_val (mk_meas_outcome B U i))  {..<dist_el_card B} =
{Re x |x. x ∈ 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)))  {..<dist_el_card 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))) 
{..<dist_el_card B}" using diag_idx_to_el_less_surj by fastforce
qed
qed

subsubsection ‹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

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⇧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}"
using mk_meas_outcome_fst_inj[of B U]
‹n = dist_el_card B› ‹M = mk_meas_outcome B U› Bii fc_mats_carrier dimB by auto
show "∀j<n. meas_outcome_prj (M 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 "∀i<n. ∀j<n. i ≠ j ⟶ meas_outcome_prj (M i) * meas_outcome_prj (M j) =
0⇩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⇩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)) {..<n} = 1⇩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) {..<dist_el_card B} (diag_elems B)"
using diag_idx_to_el_bij[of B] by simp
hence "diag_idx_to_el B  {..< p} = diag_elems B" using ‹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))  {..<p}"
using spectrum_meas_outcome_val_eq assms by force
show "(λi. meas_outcome_val (M i))  {..<p} ⊆ {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)))  {..<p} ⊆
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)))  {..<p}"
by (metis Pair_inject assms equalityE  make_pm_decomp spectrum_meas_outcome_val_eq)
qed

lemma (in cpx_sq_mat) spectrum_size:
assumes "hermitian A"
and "A∈ 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<card (spectrum A)"
shows "projector (meas_outcome_prj (proj_meas_outcomes (make_pm A) a))"
by (rule make_pm_projectors, (simp add: assms spectrum_size')+)

lemma (in cpx_sq_mat) meas_outcome_prj_carrier:
assumes "hermitian A"
and "A ∈ fc_mats"
and "a<card (spectrum A)"
shows "meas_outcome_prj (proj_meas_outcomes (make_pm A) 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<card (spectrum A)"
shows "Re (Complex_Matrix.trace (R * meas_outcome_prj (proj_meas_outcomes (make_pm A) a))) =
Complex_Matrix.trace (R * meas_outcome_prj (proj_meas_outcomes (make_pm A) a))"
proof (rule trace_proj_pos_real)
show "R ∈ 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))) {..<p}"
proof -
have "inj_on (λx. (meas_outcome_val (M x))) {..<p}"
using make_pm_proj_measurement[of A p M] assms proj_measurement_inj by simp
thus ?thesis by (simp add: inj_on_def)
qed
qed simp

lemma (in cpx_sq_mat) sum_over_spectrum':
assumes "A∈ 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))) {..<p}" using make_pm_proj_measurement[of A p M]
assms proj_measurement_inj by simp
qed simp

text ‹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)) ⋅⇩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) ⋅⇩m meas_outcome_prj (M i)) {..< p} =
sum_mat (λj. Re (diag_idx_to_el B j)⋅⇩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)) ⋅⇩m rank_1_proj (zero_col U i))
(diag_elem_indices (diag_idx_to_el B j) B)) {..<dist_el_card B}"
unfolding project_vecs_def
proof (rule sum_mat_cong)
show "finite {..<dist_el_card B}" by simp
show "⋀i. i ∈ {..<dist_el_card B} ⟹
complex_of_real (Re (diag_idx_to_el B i)) ⋅⇩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 ∈ {..<dist_el_card B} ⟹
sum_mat (λia. complex_of_real (Re (diag_idx_to_el B i)) ⋅⇩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 ∈ {..<dist_el_card B} ⟹
(Re (diag_idx_to_el B j)) ⋅⇩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)) ⋅⇩m rank_1_proj (zero_col U i))
(diag_elem_indices (diag_idx_to_el B j) B)"
proof -
fix j
assume "j ∈ {..<dist_el_card B}"
show " (Re (diag_idx_to_el B j)) ⋅⇩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)) ⋅⇩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) ⋅⇩m rank_1_proj (zero_col U ia))
(diag_elem_indices (diag_idx_to_el B j) B)) {..<dist_el_card B}"
proof (rule sum_mat_cong)
show "finite {..<dist_el_card B}" by simp
show "⋀i. i ∈ {..<dist_el_card B} ⟹
sum_mat (λia. complex_of_real (Re (diag_idx_to_el B i)) ⋅⇩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 ∈ {..<dist_el_card B} ⟹
local.sum_mat (λia.  (diag_mat B ! ia) ⋅⇩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 ∈ {..<dist_el_card B} ⟹
sum_mat (λia. (Re (diag_idx_to_el B i)) ⋅⇩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) ⋅⇩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)) ⋅⇩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) ⋅⇩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)) ⋅⇩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) ⋅⇩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)) ⋅⇩m rank_1_proj (zero_col U ia) =
(diag_mat B ! ia) ⋅⇩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)) ⋅⇩m rank_1_proj (zero_col U ia) =
(diag_mat B ! ia) ⋅⇩m rank_1_proj (zero_col U ia)" by simp
qed
qed
qed
qed
also have "... = sum_mat
(λi. (diag_mat B ! i) ⋅⇩m rank_1_proj (zero_col U i))
(⋃j<dist_el_card B. diag_elem_indices (diag_idx_to_el B j) B)"
unfolding project_vecs_def sum_mat_def
proof (rule disj_family_sum_with[symmetric])
show "finite {..<dist_el_card B}" by simp
show "∀j. (diag_mat B ! j) ⋅⇩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 ∈ {..<dist_el_card B} ⟹ finite (diag_elem_indices (diag_idx_to_el B i) B)"
show "disjoint_family_on (λn. diag_elem_indices (diag_idx_to_el B n) B)
{..<dist_el_card B}"
using diag_elem_indices_disjoint[of B] dimB dim_eq by simp
qed
also have "... = sum_mat (λi. (diag_mat B ! i) ⋅⇩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) ⋅⇩mrank_1_proj (Matrix.col U i)) {..< dimR}"
proof (rule sum_mat_cong, simp)
show res: "⋀i. i ∈ {..<dimR} ⟹ (diag_mat B ! i) ⋅⇩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 ∈ {..<dimR} ⟹ (diag_mat B ! i) ⋅⇩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 ∈ {..<dimR} ⟹ (diag_mat B ! i) ⋅⇩m rank_1_proj (zero_col U i) =
(diag_mat B ! i) ⋅⇩m rank_1_proj (Matrix.col U i)"
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)) ⋅⇩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)) ⋅⇩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