Stream: quantum computing

Topic: Quantum.thy


view this post on Zulip Anthony Bordg (Aug 13 2019 at 14:45):

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

view this post on Zulip Hanna Lachnitt (Aug 13 2019 at 14:47):

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

view this post on Zulip Hanna Lachnitt (Aug 13 2019 at 14:49):

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

view this post on Zulip Anthony Bordg (Aug 13 2019 at 14:56):

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

This is what I have in mind actually.

view this post on Zulip Anthony Bordg (Aug 13 2019 at 15:05):

prob0 and prob1 have been simplify and Quantum.thy has been updated on GitHub.

view this post on Zulip Anthony Bordg (Aug 15 2019 at 10:41):

What about moving everything related to measurement from Quantum.thy to a dedicated theory Measurement.thy ?
@Yijun He @Hanna Lachnitt

view this post on Zulip Hanna Lachnitt (Aug 15 2019 at 10:51):

I would totally opt for that.

view this post on Zulip Yijun He (Aug 15 2019 at 10:56):

I also agree with that.

view this post on Zulip Anthony Bordg (Aug 20 2019 at 15:46):

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

view this post on Zulip Hanna Lachnitt (Aug 20 2019 at 15:53):

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?

view this post on Zulip Anthony Bordg (Aug 20 2019 at 15:59):

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.

view this post on Zulip Anthony Bordg (Oct 01 2019 at 09:30):

@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.

view this post on Zulip Anthony Bordg (Oct 01 2019 at 10:55):

@Yijun He
I should probably rename hermite_cnj with dagger for conciseness.

view this post on Zulip Hanna Lachnitt (Oct 01 2019 at 12:13):

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.

view this post on Zulip Hanna Lachnitt (Oct 01 2019 at 12:29):

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

view this post on Zulip Anthony Bordg (Oct 01 2019 at 14:22):

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.

view this post on Zulip Yijun He (Oct 02 2019 at 01:21):

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.

view this post on Zulip Hanna Lachnitt (Oct 02 2019 at 12:28):

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

view this post on Zulip Yijun He (Oct 04 2019 at 10:14):

@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.

view this post on Zulip Anthony Bordg (Oct 04 2019 at 11:05):

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:

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

Then use

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

and the assumption that MM is length-preserving to prove that the diagonal elements of MMM^{\dagger}M are 11.
The result

Mψ2=ψMMψ\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.

view this post on Zulip Yijun He (Oct 04 2019 at 13:38):

I finished cleaning up just now.


Last updated: Aug 15 2022 at 02:13 UTC