logo

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

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, m, x, N, defaults
from proveit.logic import InSet
from proveit.numbers import two, Div, Floor, LessEq, ModAbs, Mult, Real, subtract
from proveit.numbers.modular import mod_abs_of_difference_bound, mod_abs_scaled
from proveit.numbers.rounding import floor_x_le_x
from proveit.physics.quantum.QPE import (
    _best_floor_def, _n_in_natural_pos, _phase,
    _phase_in_interval, _t_in_natural_pos, _two_pow_t,
    _two_pow_t__minus_one, _two_pow_t_minus_one_is_nat_pos)
In [2]:
%proving _precision_guarantee_lemma_02
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_precision_guarantee_lemma_02:
(see dependencies)
In [3]:
defaults.assumptions = _precision_guarantee_lemma_02.conditions
defaults.assumptions:
In [4]:
# for convenience
_thm_expr = _precision_guarantee_lemma_02.instance_expr
_thm_expr:

Import some basic local assumptions and local definitions

In [5]:
# some basic assumptions and definitions
display(_t_in_natural_pos)
display(_n_in_natural_pos)
display(_phase_in_interval)
display(_best_floor_def)
 ⊢  
 ⊢  
 ⊢  
 ⊢  

It is useful generally to establish that $2^{t}\varphi \ge \lfloor 2^{t}\varphi\rfloor$ (this is then used implicitly in some auto_simplification further below) (might be nice to convert this to a method of some sort in the Floor class?):

In [6]:
floor_x_le_x
 ⊢  
In [7]:
_x_sub = Mult(_two_pow_t, _phase)
floor_int_phase_bound = floor_x_le_x.instantiate({x: _x_sub}).reversed()
floor_int_phase_bound:

We gradually transform the assumed condition $|m-b|_{\text{mod}\;2^t} \le 2^{t-1}-1$ into the desired condition $|\frac{m}{2^{t}}-1|_{\text{mod}\;1} \le 2^{-n}$:

In [8]:
condition_01 = _precision_guarantee_lemma_02.condition.operands[1].prove()
condition_01:  ⊢  
In [9]:
condition_02 = (
    condition_01.inner_expr().lhs.value.operands[1].
    operand.substitute(_best_floor_def))
condition_02:  ⊢  
In [10]:
mod_abs_of_difference_bound
 ⊢  

Then for later auto-simplification to work well, we want to establish that $|\lfloor 2^{t}\varphi\rfloor - 2^{t}\varphi| \le 2^{t}/2$

In [11]:
div_mult_id = Div(_two_pow_t, two).cancelation(two)
div_mult_id:  ⊢  

The _two_pow_t_minus_one_is_nat_pos theorem, imported at the top, also lets us know that $\vdash 2^{t-1}\in\mathbb{N}$.

In [12]:
from proveit.numbers.rounding import real_minus_floor_interval
real_minus_floor_interval
 ⊢  
In [13]:
from proveit import x
from proveit.numbers import two, Exp
from proveit.physics.quantum.QPE import _t
_x_sub = Mult(Exp(two, _t), _phase)
real_minus_floor = real_minus_floor_interval.instantiate({x: _x_sub})
real_minus_floor:  ⊢  
In [14]:
from proveit.numbers import zero, one, Abs, IntervalCO
real_minus_floor_abs = InSet(Abs(real_minus_floor.element), IntervalCO(zero, one)).prove()
real_minus_floor_abs:  ⊢  
In [15]:
real_minus_floor_abs.inner_expr().element.reverse_difference(auto_simplify=False)
 ⊢  

Notice in the result of the following instantiation the ModAbs that would have appeared on the lhs with respect to $2^{t}$ has been automatically simplified to a non-modular (and non-absolute-value) expression:

In [16]:
_a_sub, _b_sub, _N_sub = (
    subtract(m, Mult(_two_pow_t, _phase)),
    subtract(m, Floor(Mult(_two_pow_t, _phase))),
    _two_pow_t)
condition_03 = mod_abs_of_difference_bound.instantiate(
        {a: _a_sub, b: _b_sub, N: _N_sub}).inner_expr().lhs.dividend.commute(0,1)
condition_03:  ⊢  
In [17]:
condition_04 = condition_03.inner_expr().lhs.commute(0, 1).with_styles(direction='normal')
condition_04:  ⊢  

But we also know from our work above that $2^{t}\varphi - \lfloor 2^{t}\varphi \rfloor < 1$, so Prove-It can now give us the following:

In [18]:
condition_05 = LessEq(condition_04.lhs, one).prove()
condition_05:  ⊢  

And then we rearrange a bit:

In [19]:
condition_06 = condition_05.left_add_both_sides(condition_05.lhs.operands[1].operand)
condition_06:  ⊢  

From an earlier condition, we can derive a bound on the rhs of condition_06 above:

In [20]:
condition_07 = condition_02.right_add_both_sides(one)
condition_07: ,  ⊢  

Then apply transitivity to obtain the following:

In [21]:
condition_08 = condition_06.apply_transitivity(condition_07)
condition_08: ,  ⊢  

We want to transform the $\text{mod}\;2^{t}$ on the lhs to the $\text{mod}\;1$ that we want in the eventual desired expression.
We can utilize the following theorem and subsequent instantiation to do that:

In [22]:
mod_abs_scaled
 ⊢  
In [23]:
from proveit import a, b, c
_a_sub, _b_sub, _c_sub = _two_pow_t, _thm_expr.lhs.operands[0], one
condition_equality_01 = mod_abs_scaled.instantiate({a: _a_sub, b: _b_sub, c: _c_sub})
condition_equality_01:  ⊢  
In [24]:
# clean up rhs side by distributing that factor of 2^t
condition_equality_02 = condition_equality_01.inner_expr().rhs.operands[0].distribute(1)
condition_equality_02:  ⊢  

Now we utilize that result, substituting the lhs for the rhs in our previous result:

In [25]:
condition_09 = condition_equality_02.sub_left_side_into(condition_08)
condition_09: ,  ⊢  

We can then divide both sides by the factor $2^{t}$ and simplify, and we are done:

In [26]:
condition_10 = condition_09.divide_both_sides(_two_pow_t)
condition_10: ,  ⊢  
_precision_guarantee_lemma_02 may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [27]:
%qed

proveit.physics.quantum.QPE._precision_guarantee_lemma_02 has been proven.
Out[27]:
 step typerequirementsstatement
0generalization1  ⊢  
1instantiation163, 2, 3,  ⊢  
  : , : , :
2instantiation4, 255, 5, 99, 6, 7, 8*,  ⊢  
  : , : , :
3instantiation9, 77, 173, 133, 10*  ⊢  
  : , :
4conjecture  ⊢  
 proveit.numbers.division.weak_div_from_numer_bound__pos_denom
5instantiation254, 255, 40  ⊢  
  : , :
6instantiation177, 11, 12,  ⊢  
  : , : , :
7instantiation13, 137  ⊢  
  :
8instantiation226, 14, 15  ⊢  
  : , : , :
9conjecture  ⊢  
 proveit.numbers.division.div_as_mult
10instantiation226, 16, 17  ⊢  
  : , : , :
11instantiation46, 18, 19,  ⊢  
  : , : , :
12instantiation163, 20, 21  ⊢  
  : , : , :
13conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos
14instantiation184, 101, 186, 22, 140*  ⊢  
  : , : , :
15instantiation203, 22  ⊢  
  :
16instantiation182, 23  ⊢  
  : , : , :
17instantiation24, 217, 25, 86, 42, 26*  ⊢  
  : , : , :
18instantiation27, 115, 28, 266, 29, 30*  ⊢  
  : , : , :
19instantiation31, 266, 115, 32, 33, 34*,  ⊢  
  : , : , :
20instantiation35, 255, 57, 266, 140*  ⊢  
  : , : , :
21instantiation36, 288, 239, 241, 173, 37, 38, 39*  ⊢  
  : , : , : , : , : , :
22instantiation286, 259, 40  ⊢  
  : , : , :
23instantiation41, 217, 260, 258, 42, 43*  ⊢  
  : , : , :
24conjecture  ⊢  
 proveit.numbers.exponentiation.product_of_real_powers
25instantiation213, 260, 87  ⊢  
  : , :
26instantiation226, 44, 45  ⊢  
  : , : , :
27conjecture  ⊢  
 proveit.numbers.addition.weak_bound_via_right_term_bound
28instantiation213, 98, 97  ⊢  
  : , :
29instantiation46, 47, 48  ⊢  
  : , : , :
30instantiation226, 49, 50  ⊢  
  : , : , :
31conjecture  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
32instantiation213, 99, 258  ⊢  
  : , :
33instantiation163, 51, 52  ⊢  
  : , : , :
34instantiation226, 53, 54  ⊢  
  : , : , :
35conjecture  ⊢  
 proveit.numbers.modular.mod_abs_scaled
36conjecture  ⊢  
 proveit.numbers.multiplication.distribute_through_subtract
37instantiation286, 259, 83  ⊢  
  : , : , :
38instantiation286, 259, 256  ⊢  
  : , : , :
39instantiation163, 55, 56  ⊢  
  : , : , :
40instantiation131, 57, 266, 58  ⊢  
  : , :
41conjecture  ⊢  
 proveit.numbers.exponentiation.real_power_of_real_power
42instantiation85, 248  ⊢  
  :
43instantiation59, 245, 244, 60*  ⊢  
  : , :
44instantiation238, 239, 283, 288, 241, 61, 245, 63, 62  ⊢  
  : , : , : , : , : , :
45instantiation243, 245, 63, 64  ⊢  
  : , : , :
46conjecture  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less_eq
47instantiation163, 65, 66, 67*  ⊢  
  : , : , :
48instantiation177, 68, 69  ⊢  
  : , : , :
49instantiation238, 288, 283, 239, 70, 241, 72, 73, 71  ⊢  
  : , : , : , : , : , :
50instantiation243, 72, 73, 74  ⊢  
  : , : , :
51assumption  ⊢  
52axiom  ⊢  
 proveit.physics.quantum.QPE._best_floor_def
53instantiation238, 239, 283, 288, 241, 75, 77, 242, 244  ⊢  
  : , : , : , : , : , :
54instantiation76, 244, 77, 246  ⊢  
  : , : , :
55instantiation163, 78, 79  ⊢  
  : , : , :
56instantiation122, 80, 81, 82  ⊢  
  : , : , : , :
57instantiation213, 83, 84  ⊢  
  : , :
58instantiation85, 250  ⊢  
  :
59conjecture  ⊢  
 proveit.numbers.multiplication.mult_neg_right
60instantiation202, 245  ⊢  
  :
61instantiation257  ⊢  
  : , :
62instantiation286, 259, 86  ⊢  
  : , : , :
63instantiation286, 259, 87  ⊢  
  : , : , :
64instantiation261  ⊢  
  :
65instantiation88, 116, 132, 137, 89*  ⊢  
  : , : , :
66instantiation95, 146, 181  ⊢  
  : , :
67instantiation90, 91, 137, 92, 93*  ⊢  
  : , :
68instantiation110, 94  ⊢  
  : , :
69instantiation95, 96, 180  ⊢  
  : , :
70instantiation257  ⊢  
  : , :
71instantiation286, 259, 97  ⊢  
  : , : , :
72instantiation286, 259, 115  ⊢  
  : , : , :
73instantiation286, 259, 98  ⊢  
  : , : , :
74instantiation261  ⊢  
  :
75instantiation257  ⊢  
  : , :
76conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_32
77instantiation286, 259, 99  ⊢  
  : , : , :
78instantiation100, 244, 175, 101, 186  ⊢  
  : , : , : , : , :
79instantiation226, 102, 103  ⊢  
  : , : , :
80instantiation182, 104  ⊢  
  : , : , :
81instantiation182, 105  ⊢  
  : , : , :
82instantiation172, 175  ⊢  
  :
83instantiation106, 190, 255, 133  ⊢  
  : , :
84instantiation176, 256  ⊢  
  :
85conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
86instantiation176, 260  ⊢  
  :
87instantiation176, 107  ⊢  
  :
88conjecture  ⊢  
 proveit.numbers.modular.mod_abs_of_difference_bound
89instantiation226, 108, 109  ⊢  
  : , : , :
90conjecture  ⊢  
 proveit.numbers.modular.mod_abs_x_reduce_to_abs_x
91instantiation213, 193, 162  ⊢  
  : , :
92instantiation110, 111  ⊢  
  : , :
93instantiation112, 113, 114*  ⊢  
  :
94instantiation148, 265, 266, 209  ⊢  
  : , : , :
95conjecture  ⊢  
 proveit.numbers.addition.commutation
96instantiation286, 259, 153  ⊢  
  : , : , :
97instantiation176, 115  ⊢  
  :
98instantiation131, 116, 255, 133  ⊢  
  : , :
99instantiation286, 272, 117  ⊢  
  : , : , :
100conjecture  ⊢  
 proveit.numbers.division.mult_frac_cancel_numer_left
101instantiation286, 200, 118  ⊢  
  : , : , :
102instantiation182, 119  ⊢  
  : , : , :
103instantiation182, 120  ⊢  
  : , : , :
104instantiation203, 244  ⊢  
  :
105instantiation203, 175  ⊢  
  :
106conjecture  ⊢  
 proveit.numbers.division.div_real_closure
107instantiation269, 270, 206  ⊢  
  : , : , :
108instantiation182, 121  ⊢  
  : , : , :
109instantiation122, 123, 124, 125  ⊢  
  : , : , : , :
110conjecture  ⊢  
 proveit.numbers.ordering.relax_less
111instantiation126, 127, 128  ⊢  
  : , : , :
112conjecture  ⊢  
 proveit.numbers.absolute_value.abs_neg_elim
113instantiation129, 130  ⊢  
  : , :
114instantiation141, 181, 180  ⊢  
  : , :
115instantiation131, 132, 255, 133  ⊢  
  : , :
116instantiation213, 190, 162  ⊢  
  : , :
117instantiation286, 134, 135  ⊢  
  : , : , :
118instantiation286, 136, 137  ⊢  
  : , : , :
119instantiation226, 138, 139  ⊢  
  : , : , :
120instantiation182, 140  ⊢  
  : , : , :
121instantiation141, 175, 181  ⊢  
  : , :
122conjecture  ⊢  
 proveit.logic.equality.four_chain_transitivity
123instantiation238, 239, 283, 288, 241, 143, 175, 146, 142  ⊢  
  : , : , : , : , : , :
124instantiation238, 283, 239, 143, 144, 241, 175, 146, 161, 181  ⊢  
  : , : , : , : , : , :
125instantiation145, 239, 288, 241, 175, 146, 181, 147  ⊢  
  : , : , : , : , : , : , : , :
126conjecture  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
127instantiation148, 265, 266, 149  ⊢  
  : , : , :
128instantiation177, 150, 151  ⊢  
  : , : , :
129conjecture  ⊢  
 proveit.numbers.addition.subtraction.nonpos_difference
130instantiation152, 237  ⊢  
  :
131conjecture  ⊢  
 proveit.numbers.modular.mod_abs_real_closure
132instantiation213, 190, 153  ⊢  
  : , :
133instantiation154, 218, 155  ⊢  
  : , :
134conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_nonzero_within_rational
135instantiation156, 218, 157  ⊢  
  : , :
136conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
137instantiation158, 195, 260  ⊢  
  : , :
138instantiation182, 159  ⊢  
  : , : , :
139instantiation203, 173  ⊢  
  :
140instantiation202, 173  ⊢  
  :
141conjecture  ⊢  
 proveit.numbers.negation.distribute_neg_through_subtract
142instantiation160, 161, 181  ⊢  
  : , :
143instantiation257  ⊢  
  : , :
144instantiation257  ⊢  
  : , :
145conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_general
146instantiation286, 259, 162  ⊢  
  : , : , :
147instantiation261  ⊢  
  :
148conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
149instantiation163, 164, 165  ⊢  
  : , : , :
150instantiation166, 233  ⊢  
  :
151instantiation226, 167, 168  ⊢  
  : , : , :
152conjecture  ⊢  
 proveit.numbers.rounding.floor_x_le_x
153instantiation176, 193  ⊢  
  :
154conjecture  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
155instantiation286, 231, 169  ⊢  
  : , : , :
156conjecture  ⊢  
 proveit.numbers.exponentiation.exp_rational_nonzero_closure
157instantiation262, 170, 171  ⊢  
  : , :
158conjecture  ⊢  
 proveit.numbers.exponentiation.exp_real_pos_closure
159instantiation172, 173  ⊢  
  :
160conjecture  ⊢  
 proveit.numbers.addition.add_complex_closure_bin
161instantiation174, 175  ⊢  
  :
162instantiation176, 237  ⊢  
  :
163theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
164instantiation177, 209, 178  ⊢  
  : , : , :
165instantiation179, 180, 181  ⊢  
  : , :
166conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
167instantiation182, 183  ⊢  
  : , : , :
168instantiation184, 185, 186, 204, 187*, 188*  ⊢  
  : , : , :
169instantiation286, 249, 285  ⊢  
  : , : , :
170instantiation286, 205, 285  ⊢  
  : , : , :
171instantiation281, 189  ⊢  
  :
172conjecture  ⊢  
 proveit.numbers.multiplication.elim_one_left
173instantiation286, 259, 255  ⊢  
  : , : , :
174conjecture  ⊢  
 proveit.numbers.negation.complex_closure
175instantiation286, 259, 190  ⊢  
  : , : , :
176conjecture  ⊢  
 proveit.numbers.negation.real_closure
177theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
178instantiation191, 192  ⊢  
  :
179conjecture  ⊢  
 proveit.numbers.absolute_value.abs_diff_reversal
180instantiation286, 259, 237  ⊢  
  : , : , :
181instantiation286, 259, 193  ⊢  
  : , : , :
182axiom  ⊢  
 proveit.logic.equality.substitution
183instantiation194, 195, 260, 266, 196, 197, 198*  ⊢  
  : , : , : , :
184conjecture  ⊢  
 proveit.numbers.division.frac_cancel_left
185instantiation286, 200, 199  ⊢  
  : , : , :
186instantiation286, 200, 201  ⊢  
  : , : , :
187instantiation202, 217  ⊢  
  :
188instantiation203, 204  ⊢  
  :
189instantiation286, 205, 206  ⊢  
  : , : , :
190instantiation286, 272, 207  ⊢  
  : , : , :
191conjecture  ⊢  
 proveit.numbers.absolute_value.abs_non_neg_elim
192instantiation208, 265, 266, 209  ⊢  
  : , : , :
193instantiation286, 272, 210