One should remove the condition `state n v`

in `prob0`

and `prob1`

. The if/then/else structure here is useless. Of course, the condition `state n v`

should be listed among the assumptions in the subsequent lemmas whenever needed, but in the definition itself it's useless.

@Hanna Lachnitt @Yijun He

That would be good it gave me some problems in Deutsch-Jozsa

Also could we maybe use k instead of j in the def of select_index?

That would be good it gave me some problems in Deutsch-Jozsa

This is what I have in mind actually.

`prob0`

and `prob1`

have been simplify and `Quantum.thy`

has been updated on GitHub.

What about moving everything related to measurement from `Quantum.thy`

to a dedicated theory `Measurement.thy`

?

@Yijun He @Hanna Lachnitt

I would totally opt for that.

I also agree with that.

Ok, but to avoid a loop (Measurement.thy importing Quantum.thy and Quantum.thy importing Measurement.thy) I would need to put the definition of Bell states and everything related to them in Measurement.thy or in a dedicated theory Bell.thy.

@Hanna Lachnitt @Yijun He

Hmm... both does not sound perfect. Why don't you want to leave the definitions of the Bell states in Quantum.thy and move their measurement in Measurement.thy? Is it because facts about the Bell states would be scattered then or does it have another reason?

Hmm... both does not sound perfect. Why don't you want to leave the definitions of the Bell states in Quantum.thy and move their measurement in Measurement.thy? Is it because facts about the Bell states would be scattered then or does it have another reason?

Yes, it would be scattered, but actually I think it's fine and probably the best solution.

@Yijun He In Quantum.thy one proves that a unitary matrix is length-preserving. It would be nice to add the converse implication, namely that a length-preserving matrix is unitary. The proof is not difficult. We could mention this result in the section 2 of the article.

@Yijun He

I should probably rename `hermite_cnj`

with `dagger`

for conciseness.

I would also like to move this lemma into Quantum.thy if thats fine for you.

lemma cpx_mat_transpose_prod: fixes M N::"complex Matrix.mat" assumes "dim_col M = dim_row N" shows "(M * N)⇧t = N⇧t * (M⇧t)" proof fix i j::nat assume a0: "i < dim_row (N⇧t * (M⇧t))" and a1: "j < dim_col (N⇧t * (M⇧t))" then have "(M * N)⇧t $$ (i,j) = (M * N) $$ (j,i)" by auto also have "... = (∑k<dim_row M⇧t. M $$ (j,k) * N $$ (k,i))" using assms a0 a1 by auto also have "... = (∑k<dim_row M⇧t. N $$ (k,i) * M $$ (j,k))" by (simp add: semiring_normalization_rules(7)) also have "... = (∑k<dim_row M⇧t. ((N⇧t) $$ (i,k)) * (M⇧t) $$ (k,j))" using assms a0 a1 by auto finally show "((M * N)⇧t) $$ (i,j) = (N⇧t * (M⇧t)) $$ (i,j)" using assms a0 a1 by auto next show "dim_row ((M * N)⇧t) = dim_row (N⇧t * (M⇧t))" by auto next show "dim_col ((M * N)⇧t) = dim_col (N⇧t * (M⇧t))" by auto qed

I need it for the quantum fourier transform, but it fits into Quantum.thy much better. I can also make a pull request for this if you want to.

And also this

lemma cpx_mat_hermite_cnj_prod: fixes M N::"complex Matrix.mat" assumes "dim_col M = dim_row N" shows "(M * N)⇧† = N⇧† * (M⇧†)" proof- have "(M * N)⇧† = ((M * N)⇧⋆)⇧t" by auto also have "... = ((M⇧⋆) * (N⇧⋆))⇧t" using assms cpx_mat_cnj_prod by auto also have "... = (N⇧⋆)⇧t * ((M⇧⋆)⇧t)" by (metis assms cpx_mat_transpose_prod cnj_transpose hermite_cnj_dim_col hermite_cnj_dim_row index_transpose_mat(2) index_transpose_mat(3)) finally show "(M * N)⇧† = N⇧† * (M⇧†)" by auto qed

I would also like to move this lemma into Quantum.thy if thats fine for you.

@Hanna Lachnitt sure, please open a PR with your lemmas.

But first you may need to update your branch due to the recent changes I made in the master branch.

Yijun He In Quantum.thy one proves that a unitary matrix is length-preserving. It would be nice to add the converse implication, namely that a length-preserving matrix is unitary. The proof is not difficult. We could mention this result in the section 2 of the article.

@Anthony Bordg I will work on the lemma today and add it to the pull request.

Pull request is open :) I added another lemma about the product of two gates.

@Anthony Bordg I have finished the proof and updated the pull request, but the proof seems too complicated. I will try to clean it up tonight.

Anthony Bordg I have finished the proof and updated the pull request, but the proof seems too complicated. I will try to clean it up tonight.

@Yijun He Great!

One could use the following result:

$\lVert M|\psi\rangle\rVert^2 = \langle \psi|M^{\dagger}M|\psi\rangle\;.$

Then use

$(M^{\dagger}M)_{ii}= \langle e_i|M^{\dagger}M|e_i\rangle$

and the assumption that $M$ is length-preserving to prove that the diagonal elements of $M^{\dagger}M$ are $1$.

The result

$\lVert M|\psi\rangle\rVert^2 = \langle \psi|M^{\dagger}M|\psi\rangle$

can easily be formalized using `cpx_vec_length_inner_prod`

and `bra_mat_on_vec`

.

I finished cleaning up just now.

Last updated: Aug 15 2022 at 02:13 UTC