logo
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory

from proveit import defaults, Lambda
from proveit import a, b, c, e, f, l, m, x, y, A, B, C, N, Q, X, Omega
from proveit.logic import Or, Forall, InSet, Union, Disjoint
from proveit.logic.sets.functions.injections import subset_injection
from proveit.logic.sets.functions.bijections import bijection_transitivity
from proveit.numbers import (zero, one, Add, Neg, greater, Less)
from proveit.numbers.modular import interval_left_shift_bijection
from proveit.statistics import prob_of_disjoint_events_is_prob_sum
from proveit.physics.quantum import NumKet
from proveit.physics.quantum.QPE import (
    _t, _two_pow_t, _two_pow_t__minus_one,  _t_in_natural_pos,
    _two_pow_t_minus_one_is_nat_pos, _Omega,
    _b_floor, _best_floor_is_int, _best_floor_def,
    _alpha_m_def, _full_domain, _neg_domain, _pos_domain,
    _modabs_in_full_domain_simp, ModAdd, _sample_space_bijection,
    _Omega_is_sample_space, _outcome_prob, _fail_def,
    _fail_sum_prob_conds_equiv_lemma)
In [2]:
%proving _fail_sum
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_fail_sum:
(see dependencies)
In [3]:
defaults.assumptions = _fail_sum.all_conditions()
defaults.assumptions:
In [4]:
e_in_domain = defaults.assumptions[0]
e_in_domain:
In [5]:
defaults.preserved_exprs = {e_in_domain.domain.upper_bound.operands[0]}
defaults.preserved_exprs:

Start with the $P_{\textrm{fail}}$ definition

In [6]:
fail_def_inst = _fail_def.instantiate()
fail_def_inst:  ⊢  

We will next translate from $m \in \{0~\ldotp \ldotp~2^{t} - 1\}$ to $b_f \oplus l$ with $l \in \{-2^{t-1} + 1 ~\ldotp \ldotp~2^{t-1}\}$

In [7]:
lower_bound = _neg_domain.lower_bound
lower_bound:
In [8]:
upper_bound = _pos_domain.upper_bound
upper_bound:
In [9]:
interval_left_shift_bijection
In [10]:
lambda_map_bijection = interval_left_shift_bijection.instantiate(
    {a:lower_bound, b:upper_bound, c:_b_floor, N:_two_pow_t, x:l})
lambda_map_bijection:  ⊢  

Use the $\oplus$ notation within kets (but not otherwise, for simplification purposed):

In [11]:
b_modadd_l__def = ModAdd(_b_floor, l).definition(assumptions=[InSet(l, _full_domain)])
b_modadd_l__def:  ⊢  
In [12]:
defaults.replacements = [b_modadd_l__def.derive_reversed().substitution(NumKet(b_modadd_l__def.rhs, _t))]
defaults.replacements:
In [13]:
transformed_fail_def = fail_def_inst.inner_expr().rhs.transform(
    lambda_map_bijection.element, lambda_map_bijection.domain.domain, _Omega)
transformed_fail_def:  ⊢  

Proceed to split the probability of this event into the sum of two disjoint possibilities

Our goal will be to apply the following theorem:

In [14]:
prob_of_disjoint_events_is_prob_sum

Prove the $|l|_{\textrm{mod}~2^t} > e$ condition for either the positive or negative domain for simplification purposes

In [15]:
condition = transformed_fail_def.rhs.non_domain_condition()
condition:
In [16]:
neg_domain_assumptions = [InSet(l, _neg_domain), *_fail_sum.all_conditions()]
neg_domain_assumptions:
In [17]:
pos_domain_assumptions = [InSet(l, _pos_domain), *_fail_sum.all_conditions()]
pos_domain_assumptions:
In [18]:
_modabs_in_full_domain_simp
In [19]:
absmod_posdomain_simp = _modabs_in_full_domain_simp.instantiate(
    assumptions=pos_domain_assumptions)
absmod_posdomain_simp: ,  ⊢  
In [20]:
absmod_negdomain_simp = _modabs_in_full_domain_simp.instantiate(
    assumptions=neg_domain_assumptions)
absmod_negdomain_simp: ,  ⊢  
In [21]:
pos_cond_eval = absmod_posdomain_simp.sub_left_side_into(
    greater(l, e), assumptions=pos_domain_assumptions).evaluation()
pos_cond_eval: ,  ⊢  
In [22]:
neg_cond_eval = absmod_negdomain_simp.sub_left_side_into(
    greater(Neg(l), e), assumptions=neg_domain_assumptions).evaluation()
neg_cond_eval: ,  ⊢  

Prove the proper injective mapping condition then apply prob_of_disjoint_events_is_prob_sum

In [23]:
circuit_map = Lambda(l, transformed_fail_def.rhs.instance_expr)
circuit_map:
In [24]:
lambda_map_bijection
In [25]:
_sample_space_bijection
In [26]:
trans_bijection = lambda_map_bijection.apply_transitivity(_sample_space_bijection)
trans_bijection:  ⊢  
In [27]:
prob_eq_sum1 = prob_of_disjoint_events_is_prob_sum.instantiate(
    {Omega:_Omega, A:_neg_domain, B:_pos_domain, C:Union(_neg_domain, _pos_domain), 
     X:_full_domain, f:circuit_map, Q:Lambda(l, condition), x:l},
    replacements=[pos_cond_eval, neg_cond_eval]).with_wrap_after_operator()
prob_eq_sum1:  ⊢  

Compute the event probabilities in terms of summing outcome probabilities

In [28]:
outcome_prob_pos = _outcome_prob.instantiate({m:ModAdd(_b_floor, l)}, assumptions=pos_domain_assumptions)
outcome_prob_pos: ,  ⊢  
In [29]:
outcome_prob_neg = _outcome_prob.instantiate({m:ModAdd(_b_floor, l)}, assumptions=neg_domain_assumptions)
outcome_prob_neg: ,  ⊢  
In [30]:
subset_injection
In [31]:
subset_injection.instantiate({A:_pos_domain, B:_full_domain, C:_Omega, f:trans_bijection.element})
In [32]:
subset_injection.instantiate({A:_neg_domain, B:_full_domain, C:_Omega, f:trans_bijection.element})
In [33]:
prob_eq_sum2 = prob_eq_sum1.inner_expr().rhs.operands[0].compute(_Omega, replacements=[outcome_prob_neg])
prob_eq_sum2:  ⊢  
In [34]:
prob_eq_sum3 = prob_eq_sum2.inner_expr().rhs.operands[1].compute(_Omega, replacements=[outcome_prob_pos])
prob_eq_sum3:  ⊢  

That logical equivalence of conditions is handled in a separate lemma, _fail_sum_prob_conds_equiv_lemma:

In [35]:
_fail_sum_prob_conds_equiv_lemma
In [36]:
# Here we explicitly preserve the -(e+1) expression; otherwise it becomes (-e-1) and
# later won't match up with the expression to be substituted for
conditions_equiv = (
    _fail_sum_prob_conds_equiv_lemma.instantiate(preserve_expr=Neg(Add(e, one)))
    .instantiate(preserve_expr=Neg(Add(e, one)), sideeffect_automation=False))
conditions_equiv:  ⊢  
In [37]:
prob_eq_sum4 = prob_eq_sum3.inner_expr().lhs.operand.body
prob_eq_sum4:
In [38]:
prob_eq_sum4 = prob_eq_sum3.inner_expr().lhs.operand.body.substitute_condition(
    conditions_equiv, preserve_all=True, sideeffect_automation=False)
prob_eq_sum4:  ⊢  
_fail_sum may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [39]:
%qed
proveit.physics.quantum.QPE._fail_sum has been proven.
Out[39]:
 step typerequirementsstatement
0generalization1  ⊢  
1instantiation412, 2, 5  ⊢  
  : , : , :
2instantiation363, 3, 4, 5  ⊢  
  : , : , : , :
3instantiation337, 6, 7  ⊢  
  : , : , :
4instantiation337, 8, 9  ⊢  
  : , : , :
5instantiation378, 10  ⊢  
  : , : , :
6instantiation11, 428  ⊢  
  :
7instantiation12, 45, 13, 226, 224*, 14*  ⊢  
  : , : , : , : , : , : , : , :
8instantiation337, 15, 16  ⊢  
  : , : , :
9modus ponens17, 18  ⊢  
10instantiation378, 19  ⊢  
  : , : , :
11axiom  ⊢  
 proveit.physics.quantum.QPE._fail_def
12conjecture  ⊢  
 proveit.statistics.prob_of_all_events_transformation
13instantiation88, 20  ⊢  
  : , :
14instantiation21, 349, 446, 351, 22, 79, 23, 24*  ⊢  
  : , : , : , : , : , :
15instantiation337, 25, 26  ⊢  
  : , : , :
16instantiation44, 45, 27, 28*, 43*, 29*  ⊢  
  : , : , : , : , :
17instantiation53, 391  ⊢  
  : , : , : , : , : , :
18generalization30  ⊢  
19modus ponens31, 32  ⊢  
20instantiation118, 227  ⊢  
  : , : , :
21conjecture  ⊢  
 proveit.numbers.modular.redundant_mod_elimination_in_sum_in_modabs
22instantiation452, 439, 33  ⊢  
  : , : , :
23instantiation452, 34, 35  ⊢  
  : , : , :
24instantiation331, 36, 37  ⊢  
  : , : , :
25instantiation38, 45, 39, 40, 41, 71, 42*, 48*, 43*  ⊢  
  : , : , : , : , : , : , : , :
26instantiation44, 45, 46, 47*, 48*, 49*  ⊢  
  : , : , : , : , :
27instantiation69, 64, 71  ⊢  
  : , : , : , :
28instantiation72, 50,  ⊢  
  :
29instantiation74, 446, 349, 351  ⊢  
  : , : , : , : , :
30instantiation51, 52  ⊢  
  : , : , :
31instantiation53, 391  ⊢  
  : , : , : , : , : , :
32generalization54  ⊢  
33instantiation452, 447, 55  ⊢  
  : , : , :
34conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
35instantiation452, 56, 254  ⊢  
  : , : , :
36instantiation348, 349, 454, 446, 351, 57, 59, 60, 58  ⊢  
  : , : , : , : , : , :
37instantiation182, 59, 60, 61  ⊢  
  : , : , :
38conjecture  ⊢  
 proveit.statistics.prob_of_disjoint_events_is_prob_sum
39instantiation62, 430, 63, 70, 64  ⊢  
  : , : , :
40instantiation352  ⊢  
  :
41instantiation65, 340, 341, 357, 444, 66  ⊢  
  : , : , : , :
42instantiation67, 68,  ⊢  
  :
43instantiation74, 446, 349, 351  ⊢  
  : , : , : , : , :
44conjecture  ⊢  
 proveit.statistics.prob_of_all_as_sum
45conjecture  ⊢  
 proveit.physics.quantum.QPE._Omega_is_sample_space
46instantiation69, 70, 71  ⊢  
  : , : , : , :
47instantiation72, 73,  ⊢  
  :
48instantiation74, 446, 349, 351  ⊢