Theory Projective_Measurements.Projective_Measurements
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
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)} = 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)"
by (simp add: zero_col_col)
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
by (simp add: linear_poly_root)
lemma spectrum_eigenvalues:
fixes A::"complex Matrix.mat"
assumes "A∈ carrier_mat n n"
and "k∈ spectrum A"
shows "eigenvalue A k" using eigenvalue_root_char_poly[of A n k]
spectrum_char_poly_root[of A n k] assms by simp
text ‹The main result that is used to construct a projective measurement for a Hermitian matrix
is that it is always possible to decompose it as $A = U*B*U^\dagger$, where $B$ is diagonal and
only contains real elements, and $U$ is unitary.›
definition hermitian_decomp where
"hermitian_decomp A B U ≡ similar_mat_wit A B U (Complex_Matrix.adjoint U) ∧ diagonal_mat B ∧
diag_mat B = (eigvals A) ∧ unitary U ∧ (∀i < dim_row B. B$$(i, i) ∈ Reals)"
lemma hermitian_decomp_sim:
assumes "hermitian_decomp A B U"
shows "similar_mat_wit A B U (Complex_Matrix.adjoint U)" using assms
unfolding hermitian_decomp_def by simp
lemma hermitian_decomp_diag_mat:
assumes "hermitian_decomp A B U"
shows "diagonal_mat B" using assms
unfolding hermitian_decomp_def by simp
lemma hermitian_decomp_eigenvalues:
assumes "hermitian_decomp A B U"
shows "diag_mat B = (eigvals A)" using assms
unfolding hermitian_decomp_def by simp
lemma hermitian_decomp_unitary:
assumes "hermitian_decomp A B U"
shows "unitary U" using assms
unfolding hermitian_decomp_def by simp
lemma hermitian_decomp_real_eigvals:
assumes "hermitian_decomp A B U"
shows "∀i < dim_row B. B$$(i, i) ∈ Reals" using assms
unfolding hermitian_decomp_def by simp
lemma hermitian_decomp_dim_carrier:
assumes "hermitian_decomp A B U"
shows "B ∈ carrier_mat (dim_row A) (dim_col A)" using assms
unfolding hermitian_decomp_def similar_mat_wit_def
by (metis (full_types) index_mult_mat(3) index_one_mat(3) insert_subset)
lemma similar_mat_wit_dim_row:
assumes "similar_mat_wit A B Q R"
shows "dim_row B = dim_row A" using assms Let_def unfolding similar_mat_wit_def
by (meson carrier_matD(1) insert_subset)
lemma (in cpx_sq_mat) hermitian_schur_decomp:
assumes "hermitian A"
and "A∈ fc_mats"
obtains B U where "hermitian_decomp A B U"
proof -
{
have es: "char_poly A = (∏ (e :: complex) ← (eigvals A). [:- e, 1:])"
using assms fc_mats_carrier eigvals_poly_length dim_eq by auto
obtain B U Q where us: "unitary_schur_decomposition A (eigvals A) = (B,U,Q)"
by (cases "unitary_schur_decomposition A (eigvals A)")
hence pr: "similar_mat_wit A B U (Complex_Matrix.adjoint U) ∧ diagonal_mat B ∧
diag_mat B = (eigvals A) ∧ unitary U ∧ (∀i < dimR. B$$(i, i) ∈ Reals)"
using hermitian_eigenvalue_real assms fc_mats_carrier es dim_eq by auto
moreover have "dim_row B = dimR" using assms fc_mats_carrier dim_eq similar_mat_wit_dim_row[of A]
pr by auto
ultimately have "hermitian_decomp A B U" unfolding hermitian_decomp_def by simp
hence "∃ B U. hermitian_decomp A B U" by auto
}
thus ?thesis using that by auto
qed
lemma (in cpx_sq_mat) hermitian_spectrum_real:
assumes "A ∈ fc_mats"
and "hermitian A"
and "a ∈ spectrum A"
shows "a ∈ Reals"
proof -
obtain B U where bu: "hermitian_decomp A B U" using assms hermitian_schur_decomp by auto
hence dimB: "B ∈ carrier_mat dimR dimR" using assms fc_mats_carrier
dim_eq hermitian_decomp_dim_carrier[of A] by simp
hence Bii: "⋀i. i < dimR ⟹ B$$(i, i) ∈ Reals" using hermitian_decomp_real_eigvals[of A B U]
bu assms fc_mats_carrier by simp
have "diag_mat B = (eigvals A)" using bu hermitian_decomp_eigenvalues[of A B] by simp
hence "a ∈ set (diag_mat B)" using assms unfolding spectrum_def by simp
hence "∃i < length (diag_mat B). a = diag_mat B ! i" by (metis in_set_conv_nth)
from this obtain i where "i < length (diag_mat B)" and "a = diag_mat B ! i" by auto
hence "a = B $$ (i,i)" unfolding diag_mat_def by simp
moreover have "i < dimR" using dimB ‹i < length (diag_mat B)› unfolding diag_mat_def by simp
ultimately show ?thesis using Bii by simp
qed
lemma (in cpx_sq_mat) spectrum_ne:
assumes "A∈ fc_mats"
and "hermitian A"
shows "spectrum A ≠ {}"
proof -
obtain B U where bu: "hermitian_decomp A B U" using assms hermitian_schur_decomp by auto
hence dimB: "B ∈ carrier_mat dimR dimR" using assms fc_mats_carrier
dim_eq hermitian_decomp_dim_carrier[of A] by simp
have "diag_mat B = (eigvals A)" using bu hermitian_decomp_eigenvalues[of A B] by simp
have "B$$(0,0) ∈ set (diag_mat B)" using dimB npos unfolding diag_mat_def by simp
hence "set (diag_mat B) ≠ {}" by auto
thus ?thesis unfolding spectrum_def using ‹diag_mat B = eigvals A› by auto
qed
lemma unitary_hermitian_eigenvalues:
fixes U::"complex Matrix.mat"
assumes "unitary U"
and "hermitian U"
and "U ∈ carrier_mat n n"
and "0 < n"
and "k ∈ spectrum U"
shows "k ∈ {-1, 1}"
proof -
have "cpx_sq_mat n n (carrier_mat n n)" by (unfold_locales, (simp add: assms)+)
have "eigenvalue U k" using spectrum_eigenvalues assms by simp
have "k ∈ Reals" using assms ‹cpx_sq_mat n n (carrier_mat n n)›
cpx_sq_mat.hermitian_spectrum_real by simp
hence "conjugate k = k" by (simp add: Reals_cnj_iff)
hence "k⇧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)"
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 (0⇩m dimR dimC)))"
have g: "∀x. g x ∈ fc_mats"
proof
fix x
show "g x ∈ fc_mats"
proof (cases "x < p")
case True
hence "(meas_outcome_val (M x)) ⋅⇩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 (0⇩m dimR dimC)))"
have h: "∀x. h x ∈ fc_mats"
proof
fix x
show "h x ∈ fc_mats"
proof (cases "x∈ spectrum A")
case True
then show ?thesis unfolding h_def using eigen_projector_carrier[of A x] assms True
by (simp add: cpx_sq_mat_smult)
next
case False
then show ?thesis unfolding h_def using zero_mem by simp
qed
qed
have "inj_on (spectrum_to_pm_idx A) (spectrum A)" using assms spectrum_to_pm_idx_inj by simp
moreover have "{..<p} = 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