Theory Projective_Measurements.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) = 0m dimR dimR) 
    sum_mat (λj. meas_outcome_prj (M j)) {..< n} = 1m 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) = 0m 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} = 1m 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 * 1m 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 (1m 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 1m n) = 
    (complex_of_real ((1::real)/n)) *  (Complex_Matrix.trace ((1m n)::complex Matrix.mat))" 
    using one_carrier_mat trace_smult[of "(1m 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 1m n) =  1" .
next
  show "Complex_Matrix.positive (complex_of_real (1 / real n) m 1m 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 
          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))) 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)} = 1m 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)"
      by (simp add: zero_col_col) 
  qed
  also have "... = 1m 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) = 0m 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 = 0m 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 = 0m 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 = 0m 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) = 0m 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) = 0m 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 "idiag_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 "idiag_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) = 0m 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 = (aas. [:- 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 = (aas. [:- 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 = (aas. [:- 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 "k2 = 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) = 
      0m 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) = 0m 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} = 1m 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)"
      by (simp add: diag_elem_indices_finite)
    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)"
      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)) 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 "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 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)) m meas_outcome_prj (M i) 
      else (0m 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)) 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 m eigen_projector A a else (0m 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} = spectrum_to_pm_idx A ` spectrum A" using (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))) 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 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 {..<p} = spectrum_to_pm_idx A ` spectrum A by simp
  also have "... = sum_mat (λi. (meas_outcome_val (M i)) m meas_outcome_prj (M i)) {..<p}"
  proof (rule sum_mat_cong, simp)
    fix i
    assume "i  {..< p}"
    hence "i < p" by simp
    show "g i  fc_mats" using g by simp
    show "g i = (meas_outcome_val (M i)) m meas_outcome_prj (M i)" unfolding g_def 
      using i < p by simp
    show "(meas_outcome_val (M i)) 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 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 m eigen_projector A i" unfolding h_def by simp
    show "h i  fc_mats" using h by simp
    show "i m eigen_projector A i  fc_mats" using eigen_projector_carrier[of A i] assms 
        i spectrum A by (metis h i = i m eigen_projector A i h)
  qed
  ultimately show ?thesis by simp
qed



end