logo

Proof of proveit.physics.quantum.QPE._failure_upper_bound theorem

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, e, f, i, l, x, defaults, Lambda
from proveit.logic import Equals, InSet, NotEquals
from proveit.numbers import (
    zero, one, two, four, Add, Exp, frac, greater, greater_eq,
    Less, Mult, NaturalPos, Neg, Real, RealPos, subtract)
from proveit.numbers.functions import MonDecFuncs
from proveit.physics.quantum.QPE import (
    _t_in_natural_pos, _two_pow_t, _two_pow_t_minus_one_is_nat_pos, _phase_is_real,
    _mod_add_def, _b_floor, _best_floor_is_int, _delta_b_floor, _delta_b_is_real, 
    _scaled_delta_b_floor_in_interval, _diff_l_scaled_delta_floor)
from proveit.physics.quantum.QPE.phase_est_ops import Psuccess, Pfail, ModAdd
In [2]:
%proving _failure_upper_bound
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_failure_upper_bound:
(see dependencies)
In [3]:
defaults.assumptions = _failure_upper_bound.conditions
defaults.assumptions:

(1) Import & Instantiate the _failure_upper_bound_lemma

In [4]:
from proveit.physics.quantum.QPE import _failure_upper_bound_lemma
_failure_upper_bound_lemma
 ⊢  
In [5]:
_failure_upper_bound_lemma_inst = (
        _failure_upper_bound_lemma.instantiate(preserve_expr=Neg(Add(e, one))))
_failure_upper_bound_lemma_inst:  ⊢  

(2) Establish some convenient labels for important expressions

In [6]:
first_sum = _failure_upper_bound_lemma_inst.rhs.operands[1].operands[0]
first_sum:
In [7]:
second_sum = _failure_upper_bound_lemma_inst.rhs.operands[1].operands[1]
second_sum:
In [8]:
the_summand = first_sum.summand
the_summand:
In [9]:
first_sum_conditions = first_sum.conditions[0]
first_sum_conditions:
In [10]:
second_sum_conditions = second_sum.conditions[0]
second_sum_conditions:

(3) Some Initial Bounding of the Summand Denominator and variables $\ell$ and $e$

In [11]:
_scaled_delta_b_floor_in_interval
 ⊢  
In [12]:
_delta_b_is_real.instantiate({b:_b_floor})
 ⊢  
In [13]:
# Automatic incidental derivation, but want to label the result for later use
scaled_delta_lower_bound = _scaled_delta_b_floor_in_interval.derive_element_lower_bound()
scaled_delta_lower_bound:  ⊢  
In [14]:
# Automatic incidental derivation, but want to label the result for later use
scaled_delta_upper_bound = _scaled_delta_b_floor_in_interval.derive_element_upper_bound()
scaled_delta_upper_bound:  ⊢  
In [15]:
neg_scaled_delta_lower_bound = scaled_delta_upper_bound.left_mult_both_sides(Neg(one))
neg_scaled_delta_lower_bound:  ⊢  
In [16]:
neg_scaled_delta_upper_bound = scaled_delta_lower_bound.left_mult_both_sides(Neg(one))
neg_scaled_delta_upper_bound:  ⊢  
In [17]:
_diff_l_scaled_delta_floor.deduce_bound(neg_scaled_delta_lower_bound,
        assumptions=defaults.assumptions + (first_sum_conditions,))
,  ⊢  
In [18]:
# For the 1st Summation
diff_l_scaled_delta_upper_bound = _diff_l_scaled_delta_floor.deduce_bound(
        neg_scaled_delta_upper_bound.reversed(),
        assumptions=defaults.assumptions + (first_sum_conditions,))
diff_l_scaled_delta_upper_bound: ,  ⊢  
In [19]:
# For the 2nd Summation
diff_l_scaled_delta_upper_bound_2 = _diff_l_scaled_delta_floor.deduce_bound(
        neg_scaled_delta_lower_bound,
        assumptions=defaults.assumptions + (second_sum_conditions,))
diff_l_scaled_delta_upper_bound_2: ,  ⊢  

(4) Bound on the First Summand and First Sum

We can find an $\ell$-dependent upper bound on the first summand, then an upper bound on the first summation.

In [20]:
first_summand_bound_02 = the_summand.deduce_bound(scaled_delta_lower_bound.reversed(),
        assumptions=defaults.assumptions + (first_sum_conditions,))
first_summand_bound_02: ,  ⊢  
In [21]:
first_summand_bound_generalized = first_summand_bound_02.generalize((l), conditions=[first_sum_conditions])
first_summand_bound_generalized:  ⊢  
In [22]:
first_sum_bound = first_sum.deduce_bound(first_summand_bound_generalized)
first_sum_bound:  ⊢  

(5) Bound on the Second Summand and Second Sum

We can find an $\ell$-dependent upper bound on the second summand, then an upper bound on the second summation.

In [23]:
second_summand_bound_02 = the_summand.deduce_bound(diff_l_scaled_delta_upper_bound_2,
        assumptions=defaults.assumptions + (second_sum_conditions,))
second_summand_bound_02: ,  ⊢  
In [24]:
second_summand_bound_02_relaxed = second_summand_bound_02.derive_relaxed()
second_summand_bound_02_relaxed: ,  ⊢  
In [25]:
second_summand_bound_generalized = second_summand_bound_02.generalize([l], conditions=[second_sum_conditions])
second_summand_bound_generalized:  ⊢  
In [26]:
second_summand_bound_relaxed_generalized = second_summand_bound_02_relaxed.generalize([l], conditions=[second_sum_conditions])
second_summand_bound_relaxed_generalized:  ⊢  
In [27]:
second_sum_bound = second_sum.deduce_bound(second_summand_bound_relaxed_generalized)
second_sum_bound:  ⊢  

(6) Bound on the Sum of Summations

Now we're ready to invoke our deduce_bound() method utilizing the bounds we've established on each separate summation.
The following three steps correspond to the transition from (5.30) to (5.31) in Nielsen & Chuang (pg 224):

In [28]:
_failure_upper_bound_lemma_inst_bound_01 = _failure_upper_bound_lemma_inst.rhs.deduce_bound(first_sum_bound)
_failure_upper_bound_lemma_inst_bound_01:  ⊢  
In [29]:
_failure_upper_bound_lemma_inst_bound_02 = _failure_upper_bound_lemma_inst_bound_01.rhs.deduce_bound(second_sum_bound)
_failure_upper_bound_lemma_inst_bound_02:  ⊢  
In [30]:
_failure_upper_bound_lemma_inst_bound_03 = (
    _failure_upper_bound_lemma_inst_bound_01.apply_transitivity(_failure_upper_bound_lemma_inst_bound_02))
_failure_upper_bound_lemma_inst_bound_03:  ⊢  

Next, shift the index of the second summation to create identical summands in each of the summations:

In [31]:
_failure_upper_bound_lemma_inst_bound_04 = (
    _failure_upper_bound_lemma_inst_bound_03.inner_expr().rhs.operands[1].
    operands[1].shift(Neg(one)))
_failure_upper_bound_lemma_inst_bound_04:  ⊢  

Then negate and flip the order of indices on the first summation (possible because the summand is an even function).

In [32]:
_failure_upper_bound_lemma_inst_bound_05 = (
    _failure_upper_bound_lemma_inst_bound_04.inner_expr().rhs.operands[1].
    operands[0].negate_index())
_failure_upper_bound_lemma_inst_bound_05:  ⊢  

Now we're ready to split off the first element of the second summation.
Nielsen & Chuang originally split off the first element of the first summation, eventually leading to a bound requiring $e \ge 2$.
Instead, we split off the first term of the second summation, allowing us to eventually derive a bound valid for $e \ge 1$.
In doing so, the resulting expression is auto-simplified to combine the two resulting like-summations:

In [33]:
Mult.change_simplification_directives(distribute_numeric_rational=True)
bound_07 = _failure_upper_bound_lemma_inst_bound_05.inner_expr().rhs.factors[1].operands[1].split_first()
bound_07:  ⊢  
In [34]:
sum_bound_as_integral = bound_07.rhs.terms[0].factors[1].upper_bound_as_integral()
sum_bound_as_integral:  ⊢  
In [35]:
integral_bound = sum_bound_as_integral.rhs.bound_via_upper_limit_bound()
integral_bound:  ⊢  
In [36]:
bound_07.rhs.deduce_bound(sum_bound_as_integral.apply_transitivity(integral_bound))
 ⊢  
In [37]:
%qed

proveit.physics.quantum.QPE._failure_upper_bound has been proven.
Out[37]:
 step typerequirementsstatement
0generalization1  ⊢  
1instantiation469, 2, 3  ⊢  
  : , : , :
2instantiation79, 4, 5  ⊢  
  : , : , :
3instantiation243, 525, 6, 7, 8, 9  ⊢  
  : , : , : , :
4instantiation79, 10, 11  ⊢  
  : , : , :
5instantiation147, 12, 13, 14, 15  ⊢  
  : , : , :
6instantiation459  ⊢  
  : , :
7instantiation459  ⊢  
  : , :
8instantiation205, 16  ⊢  
  : , :
9instantiation205, 17  ⊢  
  : , :
10instantiation18, 514  ⊢  
  :
11instantiation469, 19, 20, 21*  ⊢  
  : , : , :
12instantiation22, 179, 204  ⊢  
  : , :
13instantiation22, 175, 314  ⊢  
  : , :
14instantiation22, 175, 23  ⊢  
  : , :
15instantiation114, 175, 314, 23, 24, 25  ⊢  
  : , : , :
16instantiation29, 26, 27, 28  ⊢  
  : , : , : , :
17instantiation29, 30, 31, 32  ⊢  
  : , : , : , :
18conjecture  ⊢  
 proveit.physics.quantum.QPE._failure_upper_bound_lemma
19instantiation469, 33, 34  ⊢  
  : , : , :
20instantiation35, 497, 479, 133  ⊢  
  : , : , : , :
21instantiation404, 36, 37  ⊢  
  : , : , :
22conjecture  ⊢  
 proveit.numbers.multiplication.mult_real_closure_bin
23instantiation370, 493, 456, 224  ⊢  
  : , :
24instantiation79, 38, 39  ⊢  
  : , : , :
25instantiation400, 40  ⊢  
  : , :
26instantiation110, 483, 41, 42, 43*  ⊢  
  : , :
27instantiation325  ⊢  
  :
28instantiation205, 44  ⊢  
  : , :
29conjecture  ⊢  
 proveit.logic.equality.four_chain_transitivity
30instantiation110, 483, 45, 46, 47*  ⊢  
  : , :
31instantiation325  ⊢  
  :
32instantiation205, 48  ⊢  
  : , :
33instantiation469, 49, 50  ⊢  
  : , : , :
34instantiation51, 451, 452, 52*, 53*, 54*  ⊢  
  : , : , : , :
35conjecture  ⊢  
 proveit.numbers.summation.sum_split_first
36instantiation234, 55  ⊢  
  : , : , :
37instantiation239, 515, 525, 444, 56, 445, 144, 57, 163, 58*  ⊢  
  : , : , : , : , : , :
38instantiation59, 60, 61, 478, 479, 62, 63, 83*  ⊢  
  : , : , : , :
39instantiation64, 65, 66, 67  ⊢  
  : , :
40instantiation194, 262  ⊢  
  :
41instantiation93, 461, 226  ⊢  
  : , :
42instantiation73, 525, 68, 249, 69  ⊢  
  : , :
43instantiation404, 70, 71  ⊢  
  : , : , :
44instantiation234, 72  ⊢  
  : , : , :
45instantiation93, 286, 140  ⊢  
  : , :
46instantiation73, 525, 74, 177, 75  ⊢  
  : , :
47instantiation404, 76, 77  ⊢  
  : , : , :
48instantiation234, 78  ⊢  
  : , : , :
49instantiation79, 80, 81  ⊢  
  : , : , :
50instantiation82, 478, 517, 491, 83*, 84*  ⊢  
  : , : , : , : , :
51conjecture  ⊢  
 proveit.numbers.summation.index_negate
52instantiation280, 85  ⊢  
  :
53instantiation86, 87, 483, 88*  ⊢  
  : , :
54instantiation89, 90, 515, 267*,  ⊢  
  : , :
55instantiation404, 91, 92  ⊢  
  : , : , :
56instantiation459  ⊢  
  : , :
57instantiation93, 461, 283  ⊢  
  : , :
58instantiation404, 94, 95  ⊢  
  : , : , :
59conjecture  ⊢  
 proveit.numbers.summation.integral_upper_bound_of_sum
60conjecture  ⊢  
 proveit.numbers.functions.one_over_x_sqrd_in_mon_dec_fxns
61instantiation494, 96  ⊢  
  : , :
62instantiation147, 493, 456, 215, 216, 173*  ⊢  
  : , : , :
63instantiation97, 98  ⊢  
  : , : , :
64conjecture  ⊢  
 proveit.numbers.integration.boundedInvSqrdIntegral
65instantiation523, 330, 99  ⊢  
  : , : , :
66instantiation169, 253, 100  ⊢  
  :
67instantiation400, 133  ⊢  
  : , :
68instantiation459  ⊢  
  : , :
69instantiation523, 287, 101  ⊢  
  : , : , :
70instantiation234, 102  ⊢  
  : , : , :
71instantiation404, 103, 104  ⊢  
  : , : , :
72instantiation110, 483, 226, 224, 105*  ⊢  
  : , :
73conjecture  ⊢  
 proveit.numbers.multiplication.mult_not_eq_zero
74instantiation459  ⊢  
  : , :
75instantiation106, 140, 238  ⊢  
  :
76instantiation234, 107  ⊢  
  : , : , :
77instantiation404, 108, 109  ⊢  
  : , : , :
78instantiation110, 483, 140, 238, 111*  ⊢  
  : , :
79conjecture  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less_eq
80instantiation114, 179, 112, 115, 113, 118  ⊢  
  : , : , :
81instantiation114, 179, 115, 116, 117, 118  ⊢  
  : , : , :
82conjecture  ⊢  
 proveit.numbers.summation.index_shift
83instantiation404, 119, 120  ⊢  
  : , : , :
84instantiation404, 121, 122,  ⊢  
  : , : , :
85instantiation523, 492, 123  ⊢  
  : , : , :
86conjecture  ⊢  
 proveit.numbers.negation.distribute_neg_through_binary_sum
87instantiation523, 492, 124  ⊢  
  : , : , :
88instantiation280, 260  ⊢  
  :
89conjecture  ⊢  
 proveit.numbers.exponentiation.even_pow_is_even_fn
90instantiation523, 492, 389,  ⊢  
  : , : , :
91instantiation256, 515, 525, 444, 125, 445, 283, 163  ⊢  
  : , : , : , : , : , :
92instantiation404, 126, 127  ⊢  
  : , : , :
93conjecture  ⊢  
 proveit.numbers.multiplication.mult_complex_closure_bin
94instantiation424, 515, 525, 444, 128, 445, 144, 461, 283  ⊢  
  : , : , : , : , : , :
95instantiation129, 444, 525, 515, 445, 130, 144, 461, 283, 131*  ⊢  
  : , : , : , : , : , :
96conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
97theorem  ⊢  
 proveit.logic.sets.inclusion.fold_subset_eq
98generalization132  ⊢  
99instantiation523, 349, 490  ⊢  
  : , : , :
100instantiation419, 498, 133  ⊢  
  : , : , :
101instantiation523, 316, 282  ⊢  
  : , : , :
102instantiation139, 461, 226, 384, 134, 224, 135*  ⊢  
  : , : , :
103instantiation424, 515, 525, 444, 136, 445, 483, 137, 138  ⊢  
  : , : , : , : , : , :
104instantiation443, 444, 525, 445, 136, 137, 138  ⊢  
  : , : , : , :
105instantiation285, 138  ⊢  
  :
106conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero
107instantiation139, 286, 140, 384, 141, 238, 142*, 180*  ⊢  
  : , : , :
108instantiation424, 515, 525, 444, 143, 445, 483, 144, 181  ⊢  
  : , : , : , : , : , :
109instantiation443, 444, 525, 445, 143, 144, 181  ⊢  
  : , : , : , :
110conjecture  ⊢  
 proveit.numbers.division.div_as_mult
111instantiation404, 145, 146  ⊢  
  : , : , :
112instantiation396, 148, 151  ⊢  
  : , :
113instantiation147, 151, 148, 150, 149  ⊢  
  : , : , :
114conjecture  ⊢  
 proveit.numbers.multiplication.weak_bound_via_right_factor_bound
115instantiation396, 150, 151  ⊢  
  : , :
116instantiation396, 150, 152  ⊢  
  : , :
117instantiation343, 150, 151, 152, 153  ⊢  
  :