Proof of proveit.physics.quantum.QPE._Psi_output theorem¶

In [1]:

import proveit
theory = proveit.Theory() # the theorem's theory

from proveit import m, n, s, t, U
from proveit.numbers import zero
from proveit.physics.quantum import var_ket_psi, Ket
from proveit.physics.quantum.circuits import Qcircuit, unitary_gate_operation
from proveit.physics.quantum.QFT import InverseFourierTransform, invFT_is_unitary
from proveit.physics.quantum.QPE import (
    _s, _t, _U, _ket_u, _psi__t_ket, _psi_t_ket_is_normalized_vec,
    _s_in_nat_pos, _t_in_natural_pos, _unitary_U, _u_ket_register, QPE_def, 
    _Psi_def, _psi_t_output)

In [2]:

%proving _Psi_output

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_Psi_output:

(see dependencies)

In [3]:

QPE_def

⊢

In [4]:

QPE_def_inst = QPE_def.instantiate({s:_s, t:_t, U:_U})

QPE_def_inst: ⊢

In [5]:

invFT_is_unitary.instantiate({n:_t})

⊢

In [6]:

_psi_t_ket_is_normalized_vec.instantiate({t:_t})

⊢

In [7]:

unitary_gate_operation

⊢

In [8]:

qcircuit_prob1 = unitary_gate_operation.instantiate(
    {m:_t, U:InverseFourierTransform(_t), var_ket_psi:_psi__t_ket})

qcircuit_prob1: ⊢

In [9]:

_Psi_def

⊢

In [10]:

_Psi_output

In [11]:

qcircuit_prob2 = _Psi_def.sub_left_side_into(qcircuit_prob1)

qcircuit_prob2: ⊢

In [12]:

qcircuit_prob3 = Qcircuit.trivial_expansion_below(qcircuit_prob2, _ket_u, _s)

qcircuit_prob3: ⊢

In [13]:

psi_to_out = _psi_t_output.instantiate({t:_t})

psi_to_out: ⊢

In [14]:

qcircuit_prob4 = Qcircuit.concatenation(psi_to_out, qcircuit_prob3)

qcircuit_prob4: ⊢

In [15]:

QPE_def_inst

⊢

In [16]:

QPE_def_inst.sub_left_side_into(qcircuit_prob4)

⊢

_Psi_output has been proven.  Now simply execute "%qed".

In [17]:

%qed

proveit.physics.quantum.QPE._Psi_output has been proven.

Out[17]:

	step type	requirements	statement
0	instantiation	1, 2, 3	⊢
	: , : , :
1	conjecture		⊢
	proveit.physics.quantum.circuits.rhs_prob_via_equiv
2	instantiation	212, 4, 5	⊢
	: , : , :
3	modus ponens	6, 7	⊢
4	instantiation	226, 8, 9	⊢
	: , : , :
5	modus ponens	10, 11	⊢
6	instantiation	105, 413, 408, 12	⊢
	: , : , : , : , : , : , : , :
7	instantiation	13, 14	⊢
	: , :
8	instantiation	212, 15, 28	⊢
	: , : , :
9	instantiation	16, 310, 410, 396, 109, 17, 110, 18	⊢
	: , : , : , : , : , : , :
10	instantiation	19, 181, 278, 20, 90, 106, 21^, 22^	⊢
	: , : , : , : , : , :
11	instantiation	23, 410	⊢
	:
12	instantiation	378	⊢
	: , :
13	conjecture		⊢
	proveit.physics.quantum.circuits.equiv_reversal
14	instantiation	24, 396, 410, 25	⊢
	: , : , :
15	instantiation	26, 410, 65, 109	⊢
	: , : , :
16	conjecture		⊢
	proveit.physics.quantum.circuits.trivial_expansion_below
17	instantiation	212, 27, 28	⊢
	: , : , :
18	instantiation	306, 29, 361, 30	⊢
	: , : , : , :
19	conjecture		⊢
	proveit.physics.quantum.circuits.concat_onto_ideal_expt
20	instantiation	394, 31, 32	⊢
	: , : , :
21	instantiation	374, 33, 34	⊢
	: , : , :
22	instantiation	374, 35, 36	⊢
	: , : , :
23	conjecture		⊢
	proveit.physics.quantum.QPE._psi_t_output
24	axiom		⊢
	proveit.physics.quantum.QPE.QPE_def
25	axiom		⊢
	proveit.physics.quantum.QPE._unitary_U
26	conjecture		⊢
	proveit.physics.quantum.circuits.unitary_gate_operation
27	instantiation	37, 38, 39, 109	⊢
	: , : , : , :
28	axiom		⊢
	proveit.physics.quantum.QPE._Psi_def
29	instantiation	214, 211	⊢
	: , :
30	instantiation	330, 40	⊢
	: , :
31	instantiation	41, 181, 42, 75, 57, 43^*	⊢
	: , : , :
32	instantiation	44, 181, 45, 46, 47, 108, 109, 110	⊢
	: , : , : , :
33	instantiation	386, 48	⊢
	: , : , :
34	instantiation	330, 49	⊢
	: , :
35	instantiation	386, 50	⊢
	: , : , :
36	instantiation	330, 51	⊢
	: , :
37	conjecture		⊢
	proveit.physics.quantum.algebra.qmult_op_ket_is_ket
38	instantiation	52, 75	⊢
	:
39	instantiation	53, 75, 54	⊢
	: , : , :
40	instantiation	214, 211	⊢
	: , :
41	conjecture		⊢
	proveit.linear_algebra.tensors.tensor_prod_of_cart_exps_within_cart_exp
42	instantiation	378	⊢
	: , :
43	instantiation	55, 367, 410, 396	⊢
	: , : , :
44	conjecture		⊢
	proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space
45	instantiation	378	⊢
	: , :
46	instantiation	56, 75	⊢
	:
47	instantiation	56, 57	⊢
	:
48	instantiation	60, 310, 58	⊢
	: , : , :
49	instantiation	62, 59	⊢
	: , :
50	instantiation	60, 310, 61	⊢
	: , : , :
51	instantiation	62, 63	⊢
	: , :
52	conjecture		⊢
	proveit.linear_algebra.inner_products.complex_vec_set_is_hilbert_space
53	conjecture		⊢
	proveit.physics.quantum.algebra.qmult_matrix_is_linmap
54	instantiation	394, 64, 65	⊢
	: , : , :
55	conjecture		⊢
	proveit.numbers.exponentiation.product_of_posnat_powers
56	conjecture		⊢
	proveit.linear_algebra.complex_vec_set_is_vec_space
57	instantiation	117, 408, 213	⊢
	: , :
58	modus ponens	66, 67	⊢
59	modus ponens	68, 69	⊢
60	conjecture		⊢
	proveit.core_expr_types.tuples.tuple_eq_via_elem_eq
61	modus ponens	70, 71	⊢
62	conjecture		⊢
	proveit.physics.quantum.circuits.prob_eq_via_equiv
63	modus ponens	72, 73	⊢
64	instantiation	74, 75	⊢
	:
65	instantiation	76, 410	⊢
	:
66	instantiation	92, 209, 77, 78, 79, 80, 81, 82, 83, 84	⊢
	: , : , : , :
67	instantiation	99, 209, 85, 86, 87, 88, 89	⊢
	: , : , :
68	instantiation	105, 408, 413, 357, 90, 358	⊢
	: , : , : , : , : , : , : , :
69	instantiation	91, 181, 337, 410, 396, 108, 109, 110, 111, 112, 184, 113, 114, 115, 199, 357, 211, 215, 116, 196^*	⊢
	: , : , : , : , : , :
70	instantiation	92, 209, 278, 93, 94, 95, 96, 97, 98	⊢
	: , : , : , :