In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import e, m, X, defaults
from proveit.logic import Equals, InSet, NotEquals
from proveit.numbers import zero, one, two, Div, greater, NaturalPos, Neg, Real, subtract
# import common expressions
from proveit.physics.quantum.QPE import _Omega, _e_domain, _e_value, _two_pow_t
# import axioms, definitions
from proveit.physics.quantum.QPE import _n_ge_two, _success_def, _t_in_natural_pos, _t_req
# import theorems
from proveit.physics.quantum.QPE import (
_e_value_in_e_domain, _failure_upper_bound, _pfail_in_real, _phase_is_real,
_success_complements_failure, _precision_guarantee_lemma_01, _precision_guarantee_lemma_02,
_sample_space_def, _Omega_is_sample_space, _sample_space_bijection)
In [2]:
%proving _precision_guarantee
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_precision_guarantee:
(see dependencies)
_precision_guarantee:
(see dependencies)
We eventually need to show: $\left(|m - b|_{\text{mod}\,2^{t}}\le e \right) \Rightarrow \left(|\frac{m}{2^t}-\varphi|_{\text{mod}\,1} \le 2^{-n}\right)$
In [3]:
_success_def
In [4]:
_success_def_inst = _success_def.instantiate({e: _e_value})
_success_def_inst: ⊢ 
In [5]:
# keep this handy for later
success_prob = _success_def_inst.rhs
success_prob: 
In [6]:
_success_complements_failure
In [7]:
_success_complements_failure_inst = _success_complements_failure.instantiate({e: _e_value})
_success_complements_failure_inst: ⊢ 
In [8]:
_failure_upper_bound
In [9]:
fail_bound = _failure_upper_bound.instantiate({e: _e_value})
fail_bound: ⊢ 
In [10]:
# need this (and its instantiation) for deduce_bound effort further below
_pfail_in_real
In [11]:
_pfail_in_real.instantiate({e: _e_value})
In [12]:
bound_01 = (
_success_complements_failure_inst.rhs.deduce_bound(
fail_bound, assumptions=[InSet(e, _e_domain)]))
bound_01: ⊢ 
In [13]:
_precision_guarantee_lemma_01
In [14]:
greater(success_prob, _precision_guarantee_lemma_01.rhs).prove()
We prove the success_prob above is a lower bound of the desired probability¶
That is because the desired condition, $\left|\frac{m}{2^{t}} - \varphi\right|_{\rm{mod}\thinspace 1} \leq 2^{-n}$, is a weaker constraint than the $\left|m - b_{\textit{f}}\right|_{\rm{mod}\thinspace 2^{t}} \leq \left(2^{t - n} - 1\right)
$.
_sample_space_def, _Omega_is_sample_space, and sample_space_bijection are needed for this.
In [15]:
_precision_guarantee_lemma_02
In [16]:
thm_condition = _precision_guarantee_lemma_02.instantiate(
assumptions=_precision_guarantee_lemma_02.conditions)
thm_condition: 
, 
⊢ 
, 
⊢ 
In [17]:
success_prob.weaker_condition_bound(thm_condition.expr, _Omega)
In [18]:
%qed
Out[18]:
