logo

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

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit.logic import Equals
from proveit.numbers import two, Add, Exp, frac, Mult, Neg
from proveit.physics.quantum.QPE import (
        _e_value_ge_two, _eps, _eps_in_interval, _n,
        _n_in_natural_pos, _t, _t_in_natural_pos, _t_req )
In [2]:
%proving _precision_guarantee_lemma_01
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_precision_guarantee_lemma_01:
(see dependencies)

(0) We acknowledge a few axioms critical for the development further below:

In [3]:
display(_eps_in_interval)
display(_t_req)
display(_e_value_ge_two)
 ⊢  
 ⊢  
 ⊢  

(1) We first develop a lower bound on the difference $(t-n)$.

In [4]:
from proveit.numbers import one, greater_eq, subtract
_t_minus_n_lb_01 = greater_eq(subtract(_t, _n), _t_req.rhs.operands[1]).prove()
_t_minus_n_lb_01:  ⊢  
In [5]:
# follow up here with a Ceil method to perform this and next step
from proveit.numbers.rounding import ceil_x_ge_x
ceil_x_ge_x
 ⊢  
In [6]:
from proveit import x
_x_sub = _t_minus_n_lb_01.rhs.operand
_t_minus_n_lb_02 = ceil_x_ge_x.instantiate({x: _x_sub})
_t_minus_n_lb_02:  ⊢  
In [7]:
_t_minus_n_lb_03 = _t_minus_n_lb_01.apply_transitivity(_t_minus_n_lb_02)
_t_minus_n_lb_03:  ⊢  

(2) We then use that lower bound on $(t-n)$ to deduce a lower bound for our original expression:

In [8]:
bound_03 = _precision_guarantee_lemma_01.lhs.deduce_bound(_t_minus_n_lb_03)
bound_03:  ⊢  

(3) Process the lower bound

Now we perform some algebraic manipulation of that lower bound, trying to rewrite the lower bound in the form $1 - \epsilon(\frac{f(\epsilon)}{g(\epsilon)})$. The steps are labeled as sub-scripts of bound_03 because we're not deriving a new bound, just processing the bound we already have.

In [9]:
bound_03_01 = bound_03.inner_expr().rhs.operands[1].operand.denominator.distribute(1)
bound_03_01:  ⊢  
In [10]:
bound_03_02 = (
    bound_03_01.inner_expr().rhs.operands[2].operand.denominator.
    operands[0].substitute(Exp(two, two)))
bound_03_02:  ⊢  
In [11]:
bound_03_03 = (
    bound_03_02.inner_expr().rhs.operands[2].operand.denominator.
    common_power_extract(exp_factor=two))
bound_03_03:  ⊢  
In [12]:
bound_03_04 = (
    bound_03_03.inner_expr().rhs.operands[2].operand.denominator.
    base.distribute(1))
bound_03_04:  ⊢  
In [13]:
temp_multiplier = bound_03_04.rhs.operands[1].operand.denominator
bound_03_05 = bound_03_04.inner_expr().rhs.operands[1].operand.top_and_bottom_multiply(temp_multiplier)
bound_03_05:  ⊢  
In [14]:
with Add.temporary_simplification_directives() as tmp_directives:
    tmp_directives.combine_like_denoms = True
    bound_03_06 = bound_03_05.inner_expr().rhs.associate(1,2)
bound_03_06:  ⊢  
In [15]:
bound_03_07 = bound_03_06.inner_expr().rhs.operands[1].operand.simplify()
bound_03_07:  ⊢  
In [16]:
bound_03_08 = (bound_03_07.inner_expr().rhs.operands[1].
                  operand.top_and_bottom_multiply(Exp(_eps, two)))
bound_03_08:  ⊢  
In [17]:
bound_03_09 = bound_03_08.inner_expr().rhs.operands[1].operand.factor(_eps)
bound_03_09:  ⊢  
In [18]:
bound_03_10 = bound_03_09.inner_expr().rhs.operands[1].operand.operands[1].numerator.distribute(1)
bound_03_10:  ⊢  
In [19]:
bound_03_11 = bound_03_10.inner_expr().rhs.operands[1].operand.operands[1].denominator.common_power_extract(exp_factor=2)
bound_03_11:  ⊢  
In [20]:
bound_03_12 = bound_03_11.inner_expr().rhs.operands[1].operand.operands[1].denominator.base.distribute(1)
bound_03_12:  ⊢  

(4) Bound the fractional component

Now we focus on the fraction in the rhs of that bound, showing that the fraction is in fact positive and less than 1. Some of this section can eventually be replaced with a more general Add.factorization() case for the factoring of polynomial-like Add expressions.

In [21]:
from proveit.numbers import zero, four, greater
bound_04 = greater(Add(Mult(four, _eps), one), zero).prove()
bound_04:  ⊢  
In [22]:
bound_05 = greater(Mult(_eps, Add(Mult(four, _eps), one)), zero).prove()
bound_05:  ⊢  
In [23]:
bound_05_01 = bound_05.inner_expr().lhs.distribute(1)
bound_05_01:  ⊢  
In [24]:
from proveit.numbers import three
bound_06 = greater(Add(Mult(four, Exp(_eps, two)), Mult(four, _eps), one),
        Add(Mult(three, _eps), one)).prove()
bound_06:  ⊢  
In [25]:
equality_01 = (
    Mult(Add(Mult(two, _eps), one), Add(Mult(two, _eps), one)).
    simplification().reversed())
equality_01:
In [26]:
equality_02 = equality_01.inner_expr().rhs.distribute(1)
equality_02:  ⊢  
In [27]:
equality_03 = equality_02.inner_expr().rhs.operands[0].distribute(1)
equality_03:  ⊢  
In [28]:
bound_07 = bound_06.inner_expr().lhs.substitute(equality_03.lhs)
bound_07:  ⊢  
In [29]:
bound_08 = bound_07.divide_both_sides(bound_07.lhs)
bound_08:  ⊢  

(5) Finish up

Now we can feed that bound above into the deduce_bound() method to find a bound on the earlier-derived bound $1 - \epsilon(\frac{f(\epsilon)}{g(\epsilon)})$

In [30]:
bound_09 = bound_03_12.rhs.deduce_bound(bound_08.reversed())
bound_09:  ⊢  
_precision_guarantee_lemma_01 may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [31]:
%qed

proveit.physics.quantum.QPE._precision_guarantee_lemma_01 has been proven.
Out[31]:
 step typerequirementsstatement
0instantiation1, 2, 3  ⊢  
  : , : , :
1conjecture  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
2instantiation4, 570, 5, 6, 7  ⊢  
  : , : , :
3instantiation466, 8, 9  ⊢  
  : , : , :
4conjecture  ⊢  
 proveit.numbers.addition.strong_bound_via_right_term_bound
5instantiation566, 556  ⊢  
  :
6instantiation566, 11  ⊢  
  :
7instantiation10, 11, 556, 12  ⊢  
  : , :
8instantiation200, 13, 14  ⊢  
  : , : , :
9instantiation248, 591, 588, 524, 150, 525, 543, 551, 313, 15*, 29*  ⊢  
  : , : , : , : , : , :
10conjecture  ⊢  
 proveit.numbers.negation.negated_strong_bound
11instantiation323, 556, 17  ⊢  
  : , :
12instantiation16, 556, 17, 570, 18, 557, 164*  ⊢  
  : , : , :
13instantiation466, 19, 20  ⊢  
  : , : , :
14instantiation203, 543, 277, 585  ⊢  
  : , : , :
15instantiation231, 543, 551  ⊢  
  : , :
16conjecture  ⊢  
 proveit.numbers.multiplication.strong_bound_via_right_factor_bound
17instantiation351, 130, 49, 34  ⊢  
  : , :
18instantiation21, 49, 130, 22, 23, 24*  ⊢  
  : , : , :
19instantiation466, 25, 26  ⊢  
  : , : , :
20instantiation248, 591, 588, 524, 27, 525, 543, 171, 313, 28*, 29*  ⊢  
  : , : , : , : , : , :
21conjecture  ⊢  
 proveit.numbers.division.strong_div_from_numer_bound__pos_denom
22instantiation200, 30, 31  ⊢  
  : , : , :
23instantiation87, 74  ⊢  
  :
24instantiation32, 33, 34  ⊢  
  :
25instantiation200, 35, 36  ⊢  
  : , : , :
26instantiation509, 37, 38, 39*  ⊢  
  : , : , :
27instantiation540  ⊢  
  : , :
28instantiation231, 543, 171  ⊢  
  : , :
29instantiation466, 40, 41  ⊢  
  : , : , :
30instantiation405, 130, 569, 42, 43, 44*, 45*  ⊢  
  : , : , :
31instantiation466, 46, 47, 48*  ⊢  
  : , : , :
32conjecture  ⊢  
 proveit.numbers.division.frac_cancel_complete
33instantiation589, 560, 49  ⊢  
  : , : , :
34instantiation495, 50  ⊢  
  :
35instantiation466, 51, 52  ⊢  
  : , : , :
36instantiation143, 159, 160, 121  ⊢  
  : , : , :
37instantiation507, 53  ⊢  
  : , : , :
38instantiation426, 54  ⊢  
  : , :
39instantiation509, 55, 242  ⊢  
  : , : , :
40instantiation466, 56, 57  ⊢  
  : , : , :
41instantiation411, 58, 59, 60  ⊢  
  : , : , : , :
42instantiation409, 138, 556  ⊢  
  : , :
43instantiation466, 61, 62  ⊢  
  : , : , :
44instantiation509, 63, 64  ⊢  
  : , : , :
45instantiation411, 65, 66, 67  ⊢  
  : , : , : , :
46instantiation466, 68, 69  ⊢  
  : , : , :
47instantiation248, 591, 588, 176, 551, 485, 522, 543, 70*, 71*  ⊢  
  : , : , : , : , : , :
48instantiation509, 72, 73  ⊢  
  : , : , :
49instantiation341, 262, 588  ⊢  
  : , :
50instantiation589, 505, 74  ⊢  
  : , : , :
51instantiation466, 75, 76  ⊢  
  : , : , :
52instantiation507, 77  ⊢  
  : , : , :
53instantiation411, 78, 79, 80  ⊢  
  : , : , : , :
54instantiation81, 543, 82, 309, 83, 163*, 84*  ⊢  
  : , : , : , :
55instantiation507, 467  ⊢  
  : , : , :
56instantiation308, 522, 310, 309  ⊢  
  : , : , : , : , :
57instantiation509, 85, 86  ⊢  
  : , : , :
58instantiation507, 312  ⊢  
  : , : , :
59instantiation507, 312  ⊢  
  : , : , :
60instantiation269, 522  ⊢  
  :
61instantiation87, 88  ⊢  
  :
62instantiation248, 591, 588, 524, 89, 525, 543, 90, 522, 91*, 164*  ⊢  
  : , : , : , : , : , :
63instantiation451, 591, 588, 524, 96, 525, 92, 98, 522  ⊢  
  : , : , : , : , : , :
64instantiation93, 524, 588, 525, 96, 98, 522  ⊢  
  : , : , : , :
65instantiation451, 524, 588, 591, 525, 95, 106, 543, 94  ⊢  
  : , : , : , : , : , :
66instantiation451, 588, 524, 95, 96, 525, 106, 543, 98, 522  ⊢  
  : , : , : , : , : , :
67instantiation453, 591, 588, 97, 106, 543, 98, 522, 99*  ⊢  
  : , : , : , : , : , :
68instantiation426, 100  ⊢  
  : , :
69instantiation248, 591, 588, 524, 176, 525, 245, 485, 522, 101*  ⊢  
  : , : , : , : , : , :
70instantiation509, 102, 103  ⊢  
  : , : , :
71instantiation523, 591, 551, 543  ⊢  
  : , : , : , :
72instantiation451, 524, 588, 525, 104, 176, 106, 485, 522  ⊢  
  : , : , : , : , : , :
73instantiation453, 591, 588, 105, 106, 485, 522, 107*  ⊢  
  : , : , : , : , : , :
74instantiation363, 262, 108  ⊢  
  :
75instantiation200, 109, 110  ⊢  
  : , : , :
76instantiation453, 591, 588, 524, 111, 525, 522, 112, 113, 114*  ⊢  
  : , : , : , : , : , :
77instantiation509, 115, 116  ⊢  
  : , : , :
78instantiation507, 117  ⊢  
  : , : , :
79instantiation521, 524, 588, 591, 525, 118, 543, 120, 121  ⊢  
  : , : , : , : , : , :
80instantiation216, 591, 588, 524, 119, 525, 543, 120, 121  ⊢  
  : , : , : , : , : , :
81conjecture  ⊢  
 proveit.numbers.division.prod_of_fracs
82instantiation244, 120, 121  ⊢  
  : , :
83instantiation190, 123, 122  ⊢  
  :
84instantiation361, 123  ⊢  
  :
85instantiation507, 124  ⊢  
  : , : , :
86instantiation507, 125  ⊢  
  : , : , :
87conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos
88instantiation529, 546, 126  ⊢  
  : , :
89instantiation540  ⊢  
  : , :
90instantiation589, 560, 127  ⊢  
  : , : , :
91instantiation509, 128, 129  ⊢  
  : , : , :
92conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.zero_is_complex
93conjecture  ⊢  
 proveit.numbers.addition.elim_zero_any
94instantiation589, 560, 130  ⊢  
  : , : , :
95instantiation540  ⊢  
  : , :
96instantiation540  ⊢  
  : , :
97instantiation540  ⊢  
  : , :
98instantiation589, 560, 169  ⊢  
  : , : , :
99instantiation426, 131, 132*  ⊢  
  : , :
100instantiation241, 245, 583, 133*, 476*  ⊢  
  : , : , :
101instantiation509, 134, 135  ⊢  
  : , : , :
102instantiation521, 591, 588, 222, 551, 543  ⊢  
  : , : , : , : , : , :
103instantiation509, 136, 137  ⊢  
  : , : , :
104instantiation540  ⊢  
  : , :
105instantiation540  ⊢  
  : , :
106instantiation589, 560, 138  ⊢  
  : , : , :
107instantiation426, 139, 140*  ⊢  
  : , :
108instantiation495, 141  ⊢  
  :
109instantiation466, 142, 227  ⊢  
  : , : , :
110instantiation143, 144, 522, 145*  ⊢  
  : , : , :
111instantiation540  ⊢  
  : , :
112instantiation589, 560, 146  ⊢  
  : , : , :
113instantiation589, 560, 147  ⊢  
  : , : , :
114instantiation466, 148, 149  ⊢  
  : , : , :
115instantiation451, 524, 588, 591, 525, 150, 551, 313, 522  ⊢  
  : , : , : , : , : , :
116instantiation509, 151, 152  ⊢  
  : , : , :
117instantiation153, 546, 561, 570, 188, 154, 242*  ⊢  
  : , : , : , :
118instantiation540  ⊢  
  : , :
119instantiation540  ⊢  
  : , :
120instantiation542, 543, 155  ⊢  
  : , :
121instantiation589, 560, 156  ⊢  
  : , : , :
122instantiation157, 588, 158, 159, 160  ⊢  
  : , :
123instantiation589, 560, 161  ⊢  
  : , : , :
124instantiation509, 162, 163  ⊢  
  : , : , :
125instantiation507, 164  ⊢  
  : , : , :
126instantiation512, 165, 563  ⊢  
  : , :
127instantiation589, 552, 165  ⊢  
  : , : , :
128instantiation521, 591, 588, 524, 166, 525, 543, 218  ⊢  
  : , : , : , : , : , :
129instantiation509, 167, 168  ⊢  
  : , : , :
130instantiation409, 169, 570  ⊢  
  : , :
131instantiation248, 524, 588, 591, 525, 170, 522, 171, 543, 191*  ⊢  
  : , : , : , : , : , :
132conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_1_3
133instantiation550, 245  ⊢  
  :
134instantiation205, 588, 172, 173, 174, 175  ⊢  
  : , : , : , :
135instantiation451, 591, 588, 524, 176, 525, 177, 485, 522  ⊢  
  : , : , : , : , : , :
136instantiation216, 524, 588, 525, 255, 217, 551, 543, 230*  ⊢  
  : , : , : , : , : , :
137instantiation216, 591, 588, 524, 217, 525, 218, 543, 219*  ⊢  
  : , : , : , : , : , :
138instantiation323, 320, 220  ⊢  
  : , :
139instantiation248, 524, 588, 591, 525, 255, 551, 543  ⊢  
  : , : , : , : , : , :
140conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_2_2
141instantiation589, 505, 178  ⊢  
  : , : , :
142instantiation200, 179, 180  ⊢  
  : , : , :
143conjecture  ⊢  
 proveit.numbers.division.frac_cancel_left
144instantiation589, 548, 293  ⊢  
  : , : , :
145instantiation509, 181, 182  ⊢  
  : , : , :
146instantiation566, 236  ⊢