@Hanna Lachnitt is working on the Deutsch-Jozsa algorithm.

@Yijun He I now its a long shot but have you have you already proven anything about the parity of a number in relation to bin_rep? In particular, I want to show that if the kth position in the binary representation is 0, then the result of the division I of this number by 2^(m-k) is even where m is the total number of bits. (Intuitively this is clear, if we cut off the bit after k digits and the last one is 0 then the resulting number is even)

Not yet, but I have proved something similar: `select_index_div_2`

in my `Quantum_Fourier_Transform.thy`

shows that only the last bit of `select_index`

is cut off when we divide a number by 2, and `select_index_eq_bin_rep`

in the same file shows that `select_index`

is exactly the same as `bin_rep`

(except one gives booleans, and the other give 1 and 0s). Therefore the method in `select_index_div_2`

might also help prove parity results about `bin_rep`

.

Not yet, but I have proved something similar:

`select_index_div_2`

in my`Quantum_Fourier_Transform.thy`

shows that only the last bit of`select_index`

is cut off when we divide a number by 2, and`select_index_eq_bin_rep`

in the same file shows that`select_index`

is exactly the same as`bin_rep`

(except one gives booleans, and the other give 1 and 0s). Therefore the method in`select_index_div_2`

might also help prove parity results about`bin_rep`

.

`select_index_div_2`

is in Measurement.thy

Great thanks a lot. I guess with a little induction this should help me a lot. Also that `select_index`

`bin_rep`

thing is something I was thinking of proving at some point :D

@Yijun He @Hanna Lachnitt

PR #19 and #20 have been merged.

The master branch has been tidied up.

Next is Hanna's Qft.

Last updated: Sep 25 2022 at 23:25 UTC