In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import defaults
from proveit.physics.quantum.QPE import _phase_is_real, _two_pow_t_is_nat_pos
In [2]:
%proving _phase_from_best_with_delta_b
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_phase_from_best_with_delta_b:
(see dependencies)
_phase_from_best_with_delta_b:
(see dependencies)
In [3]:
defaults.assumptions = _phase_from_best_with_delta_b.all_conditions()
defaults.assumptions: 
In [4]:
from proveit.physics.quantum.QPE import _delta_b_def
_delta_b_def
In [5]:
_delta_b_def_inst = _delta_b_def.instantiate()
_delta_b_def_inst: 
⊢ 
⊢ 
In [6]:
_delta_b_def_inst.substitution(_phase_from_best_with_delta_b.instance_expr.rhs)
In [7]:
%qed
Out[7]:
