# Proof of proveit.physics.quantum.QPE._fail_sum theorem¶

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,
_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)])

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 = (

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