# 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 typerequirementsstatement
0instantiation1, 2, 3
: , : , :
1conjecture
proveit.physics.quantum.circuits.rhs_prob_via_equiv
2instantiation212, 4, 5
: , : , :
3modus ponens6, 7
4instantiation226, 8, 9
: , : , :
5modus ponens10, 11
6instantiation105, 413, 408, 12
: , : , : , : , : , : , : , :
7instantiation13, 14
: , :
8instantiation212, 15, 28
: , : , :
9instantiation16, 310, 410, 396, 109, 17, 110, 18
: , : , : , : , : , : , :
10instantiation19, 181, 278, 20, 90, 106, 21*, 22*
: , : , : , : , : , :
11instantiation23, 410
:
12instantiation378
: , :
13conjecture
proveit.physics.quantum.circuits.equiv_reversal
14instantiation24, 396, 410, 25
: , : , :
15instantiation26, 410, 65, 109
: , : , :
16conjecture
proveit.physics.quantum.circuits.trivial_expansion_below
17instantiation212, 27, 28
: , : , :
18instantiation306, 29, 361, 30
: , : , : , :
19conjecture
proveit.physics.quantum.circuits.concat_onto_ideal_expt
20instantiation394, 31, 32
: , : , :
21instantiation374, 33, 34
: , : , :
22instantiation374, 35, 36
: , : , :
23conjecture
proveit.physics.quantum.QPE._psi_t_output
24axiom
proveit.physics.quantum.QPE.QPE_def
25axiom
proveit.physics.quantum.QPE._unitary_U
26conjecture
proveit.physics.quantum.circuits.unitary_gate_operation
27instantiation37, 38, 39, 109
: , : , : , :
28axiom
proveit.physics.quantum.QPE._Psi_def
29instantiation214, 211
: , :
30instantiation330, 40
: , :
31instantiation41, 181, 42, 75, 57, 43*
: , : , :
32instantiation44, 181, 45, 46, 47, 108, 109, 110
: , : , : , :
33instantiation386, 48
: , : , :
34instantiation330, 49
: , :
35instantiation386, 50
: , : , :
36instantiation330, 51
: , :
37conjecture
proveit.physics.quantum.algebra.qmult_op_ket_is_ket
38instantiation52, 75
:
39instantiation53, 75, 54
: , : , :
40instantiation214, 211
: , :
41conjecture
proveit.linear_algebra.tensors.tensor_prod_of_cart_exps_within_cart_exp
42instantiation378
: , :
43instantiation55, 367, 410, 396
: , : , :
44conjecture
proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space
45instantiation378
: , :
46instantiation56, 75
:
47instantiation56, 57
:
48instantiation60, 310, 58
: , : , :
49instantiation62, 59
: , :
50instantiation60, 310, 61
: , : , :
51instantiation62, 63
: , :
52conjecture
proveit.linear_algebra.inner_products.complex_vec_set_is_hilbert_space
53conjecture
proveit.physics.quantum.algebra.qmult_matrix_is_linmap
54instantiation394, 64, 65
: , : , :
55conjecture
proveit.numbers.exponentiation.product_of_posnat_powers
56conjecture
proveit.linear_algebra.complex_vec_set_is_vec_space
57instantiation117, 408, 213
: , :
58modus ponens66, 67
59modus ponens68, 69
60conjecture
proveit.core_expr_types.tuples.tuple_eq_via_elem_eq
61modus ponens70, 71
62conjecture
proveit.physics.quantum.circuits.prob_eq_via_equiv
63modus ponens72, 73
64instantiation74, 75
:
65instantiation76, 410
:
66instantiation92, 209, 77, 78, 79, 80, 81, 82, 83, 84
: , : , : , :
67instantiation99, 209, 85, 86, 87, 88, 89
: , : , :
68instantiation105, 408, 413, 357, 90, 358
: , : , : , : , : , : , : , :
69instantiation91, 181, 337, 410, 396, 108, 109, 110, 111, 112, 184, 113, 114, 115, 199, 357, 211, 215, 116, 196*
: , : , : , : , : , :
70instantiation92, 209, 278, 93, 94, 95, 96, 97, 98
: , : , : , :