In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import n, t
from proveit.physics.quantum.QFT import invFT_is_unitary
from proveit.physics.quantum.QPE import (
_t, _t_in_natural_pos, _psi_t_ket_is_normalized_vec, _Psi_def)
In [2]:
%proving _Psi_ket_is_normalized_vec
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_Psi_ket_is_normalized_vec:
(see dependencies)
_Psi_ket_is_normalized_vec:
(see dependencies)
In [3]:
_psi_t_ket_is_normalized_vec.instantiate({t:_t})
In [4]:
_Psi_def
In [5]:
invFT_is_unitary
In [6]:
invFT_is_unitary.instantiate({n:_t})
In [7]:
_Psi_def.rhs.compute_norm(replacements=[_Psi_def.derive_reversed()])
In [8]:
%qed
Out[8]:
