logo

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

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import b, m, theta, defaults
from proveit.logic import NotEquals, InSet
from proveit.numbers import (
        zero, one, two, pi, Abs, Add, Complex, frac, IntervalOC, Less, greater, Mult, Exp)
# QPE common exprs
from proveit.physics.quantum.QPE import _b_round, _delta_b_round, _t, _two_pow_t
 # QPE theorems
from proveit.physics.quantum.QPE import (
        _alpha_m_mod_as_geometric_sum, _alpha_are_complex, _best_round_is_int,
        _delta_b_is_real, _delta_b_is_zero_or_non_int,
        _phase_from_best_with_delta_b, _scaled_delta_b_round_in_interval,
        _t_in_natural_pos, _two_pow_t_is_nat_pos)
from proveit.trigonometry import Sin
In [2]:
%proving _best_guarantee_delta_nonzero
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_best_guarantee_delta_nonzero:
(see dependencies)
In [3]:
defaults.assumptions = [_best_guarantee_delta_nonzero.antecedent]
defaults.assumptions:

Keep the factor of $2$ from combining with $2^t$ in the steps below:

In [4]:
Exp.change_simplification_directives(factor_numeric_rational=True)
In [5]:
alpha_index = _best_guarantee_delta_nonzero.consequent.lhs.base.operand.index
alpha_index:

Start from $\alpha_{m~\textrm{mod}~2^t}$ expressed as a geometric sum, instantiated with $m:b_r$

In [6]:
_alpha_m_mod_as_geometric_sum
 ⊢  
In [7]:
_alpha_eq_01 = (
        _alpha_m_mod_as_geometric_sum.instantiate({m: _b_round}))
_alpha_eq_01:  ⊢  

Put this in terms of $\delta_{b_r}$

In [8]:
_phase_from_best_with_delta_b
 ⊢  
In [9]:
_phase_from_best_with_delta_b_inst = (
        _phase_from_best_with_delta_b.instantiate({b: _b_round}))
_phase_from_best_with_delta_b_inst:  ⊢  
In [10]:
# We want to know that _delta_b_round and 2^t are real so that
# auto-simplification will manifest in the substitute() step further below
_delta_b_is_real
 ⊢  
In [11]:
_delta_b_is_real.instantiate({b: _b_round})
 ⊢  
In [12]:
with Exp.temporary_simplification_directives() as tmp_directives:
    tmp_directives.reduce_double_exponent = False # don't simplify k double-exponent
    _alpha_eq_02 = (
        _alpha_eq_01.inner_expr().rhs.factors[1].summand.base.exponent.
        factors[3].operands[0].substitute(_phase_from_best_with_delta_b_inst.rhs))
_alpha_eq_02:  ⊢  

Evaluate the Finite Geometric Sum

To evaluate the summation as a finite geometric sum, we need to establish that the constant ratio $e^{2\pi i \delta_{b_r}} \neq 1$ which is automatically proven given $\delta_{b_r} \notin \mathbb{Z}$.

In [13]:
_delta_b_is_zero_or_non_int
 ⊢  
In [14]:
_delta_b_is_zero_or_non_int_inst = _delta_b_is_zero_or_non_int.instantiate({b: _b_round})
_delta_b_is_zero_or_non_int_inst:  ⊢  
In [15]:
_delta_b_round_non_int = _delta_b_is_zero_or_non_int_inst.derive_right_if_not_left()
_delta_b_round_non_int:  ⊢  

We can then evaluate the sum using the standard formula for a finite geometric sum:

In [16]:
_alpha_eq_03 = _alpha_eq_02.inner_expr().rhs.factors[1].geom_sum_reduce()
_alpha_eq_03:  ⊢  

Take the Magnitude (Abs) of Both Sides

Pre-requisites to allow auto-simplification to go through

Establish that the $\alpha$ expression is in the Complex numbers.

In [17]:
_alpha_are_complex.instantiate({m:alpha_index})
 ⊢  

Prove that $\pi |\delta_{b_r}| \in \left(0, \frac{\pi}{2}\right)$ which is important to ensure the denominator is non-zero. Along the way, we prove $2^t \pi |\delta_{b_r}| \leq \frac{\pi}{2}$ which will be useful for bounding the numerator.

In [18]:
angle = Mult(pi, Abs(_delta_b_round))
angle:
In [19]:
Less(zero, angle).prove()
 ⊢  
In [20]:
scaled_abs_bound = (Abs(_scaled_delta_b_round_in_interval.element).deduce_weak_upper_bound(frac(one, two))
         .inner_expr().lhs.simplify())
scaled_abs_bound:  ⊢  

Close enough to $2^t \pi |\delta_{b_r}| \leq \frac{\pi}{2}$ (the translation occurs automatically via canonical forms):

In [21]:
two_pow_t_times_angle__bound = scaled_abs_bound.left_mult_both_sides(pi)
two_pow_t_times_angle__bound:  ⊢  
In [22]:
two_pow_t_bound = _two_pow_t.deduce_bound(_t_in_natural_pos.derive_element_lower_bound())
two_pow_t_bound:  ⊢  
In [23]:
two_pow_t_times_angle__bound.lhs.deduce_bound(greater(_two_pow_t, one))
 ⊢  
In [24]:
Less(angle, frac(pi, two)).prove()
 ⊢  

Now take the absolute value on each side

In [25]:
with Mult.temporary_simplification_directives() as tmp_directives:
    # pull the 2^t to the front
    tmp_directives.order_key_fn = lambda factor : 0 if factor==_two_pow_t else 1
    _alpha_eq_04 = _alpha_eq_03.abs_both_sides()
_alpha_eq_04:  ⊢  

Bound the numerator and the denominator

Bound the sin function in the denominator utilizing $\sin{\theta} < \theta$ for $\theta > 0$

In [26]:
denominator_sin_bound = _alpha_eq_04.rhs.factors[1].denominator.deduce_linear_upper_bound()
denominator_sin_bound:  ⊢  

Bound the sin function in the numerator utilizing $\sin{\theta} \ge \frac{2}{\pi}(\theta)$ for $0 < \theta \le \frac{\pi}{2}$

In [27]:
numerator_sin_bound = _alpha_eq_04.rhs.factors[1].numerator.deduce_linear_lower_bound()
numerator_sin_bound:  ⊢  

Apply these numerator and denominator bounds

In [28]:
rhs_bound = _alpha_eq_04.rhs.deduce_bound([numerator_sin_bound, denominator_sin_bound])
rhs_bound:  ⊢  
In [29]:
_alpha_ineq = _alpha_eq_04.apply_transitivity(rhs_bound)
_alpha_ineq:  ⊢  

Finally square both sides

In [30]:
_alpha_ineq.square_both_sides()
 ⊢   
_best_guarantee_delta_nonzero may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [31]:
%qed

proveit.physics.quantum.QPE._best_guarantee_delta_nonzero has been proven.
Out[31]:
 step typerequirementsstatement
0deduction1  ⊢  
1instantiation424, 2, 3  ⊢  
  : , : , :
2instantiation4, 622, 5, 6, 7, 8  ⊢  
  : , : , :
3instantiation466, 9, 10, 11  ⊢  
  : , : , : , :
4conjecture  ⊢  
 proveit.numbers.exponentiation.exp_pos_less
5instantiation632, 538, 29  ⊢  
  : , : , :
6instantiation632, 333, 12  ⊢  
  : , : , :
7instantiation337, 13, 14  ⊢  
  : , :
8instantiation572, 627  ⊢  
  :
9instantiation280, 553, 15, 16, 17*  ⊢  
  : , :
10instantiation566  ⊢  
  :
11instantiation409, 18  ⊢  
  : , :
12instantiation19, 35  ⊢  
  :
13instantiation20, 21  ⊢  
  :
14instantiation424, 22, 23  ⊢  
  : , : , :
15instantiation632, 621, 24  ⊢  
  : , : , :
16instantiation25, 479, 612, 420  ⊢  
  : , :
17instantiation62, 479, 622, 564, 420, 26*  ⊢  
  : , : , :
18instantiation573, 27, 28  ⊢  
  : , : , :
19conjecture  ⊢  
 proveit.numbers.absolute_value.abs_complex_closure
20conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.nonneg_if_in_real_nonneg
21instantiation632, 379, 29  ⊢  
  : , : , :
22instantiation404, 84, 30, 31, 32, 117, 33*  ⊢  
  : , : , :
23instantiation34, 35, 36, 37, 38*  ⊢  
  : , :
24instantiation39, 508, 634  ⊢  
  : , :
25conjecture  ⊢  
 proveit.numbers.exponentiation.exp_not_eq_zero
26instantiation40, 612, 541, 598*  ⊢  
  : , :
27instantiation582, 41  ⊢  
  : , : , :
28instantiation42, 612, 417, 627, 43*, 44*  ⊢  
  : , : , :
29instantiation45, 299, 537, 420  ⊢  
  : , :
30instantiation46, 245, 318, 190  ⊢  
  : , :
31instantiation46, 183, 241, 182  ⊢  
  : , :
32instantiation401, 47, 48  ⊢  
  : , : , :
33instantiation573, 49, 50  ⊢  
  : , : , :
34conjecture  ⊢  
 proveit.numbers.absolute_value.abs_eq
35instantiation51, 52  ⊢  
  :
36instantiation412, 56, 57  ⊢  
  : , :
37instantiation463, 53, 54  ⊢  
  : , : , :
38instantiation486, 627, 55, 56, 57, 58*, 59*  ⊢  
  : , :
39conjecture  ⊢  
 proveit.numbers.exponentiation.exp_real_closure_nat_power
40conjecture  ⊢  
 proveit.numbers.multiplication.mult_neg_right
41instantiation280, 612, 479, 420  ⊢  
  : , :
42conjecture  ⊢  
 proveit.numbers.exponentiation.posnat_power_of_product
43instantiation466, 60, 61, 551  ⊢  
  : , : , : , :
44instantiation62, 479, 564, 622, 420, 63*  ⊢  
  : , : , :
45conjecture  ⊢  
 proveit.numbers.division.div_real_pos_closure
46conjecture  ⊢  
 proveit.numbers.division.div_real_closure
47instantiation64, 273, 65, 362, 66  ⊢  
  : , : , :
48instantiation67, 241, 245, 183, 68, 242  ⊢  
  : , : , :
49instantiation573, 69, 70  ⊢  
  : , : , :
50instantiation466, 71, 72, 73  ⊢  
  : , : , : , :
51conjecture  ⊢  
 proveit.physics.quantum.QPE._alpha_are_complex
52instantiation74, 617, 602  ⊢  
  : , :
53instantiation463, 75, 76, 77*  ⊢  
  : , : , :
54instantiation78, 148, 149, 79, 80, 81, 82*, 83*  ⊢  
  : , : , : , :
55instantiation609  ⊢  
  : , :
56instantiation632, 621, 84  ⊢  
  : , : , :
57instantiation191, 87, 88, 89  ⊢  
  : , :
58instantiation514, 85  ⊢  
  :
59instantiation86, 87, 88, 89, 90*  ⊢  
  : , :
60instantiation91, 627, 612  ⊢  
  : , :
61instantiation92, 634, 93, 596, 94  ⊢  
  : , : , : , :
62conjecture  ⊢  
 proveit.numbers.exponentiation.real_power_of_real_power
63instantiation540, 541, 612, 597*  ⊢  
  : , :
64conjecture  ⊢  
 proveit.numbers.division.strong_div_from_denom_bound__all_pos
65instantiation95, 241, 242  ⊢  
  :
66instantiation96, 362  ⊢  
  :
67conjecture  ⊢  
 proveit.numbers.division.weak_div_from_numer_bound__pos_denom
68instantiation97, 334, 98, 99*  ⊢  
  :
69instantiation582, 100  ⊢  
  : , : , :
70instantiation463, 101, 102  ⊢  
  : , : , :
71instantiation582, 103  ⊢  
  : , : , :
72instantiation582, 104  ⊢  
  : , : , :
73instantiation293, 105, 305, 612  ⊢  
  : , : , :
74conjecture  ⊢  
 proveit.numbers.modular.mod_natpos_in_interval
75instantiation106, 617  ⊢  
  :
76instantiation107, 617  ⊢  
  :
77instantiation573, 108, 109  ⊢  
  : , : , :
78conjecture  ⊢  
 proveit.numbers.summation.gen_finite_geom_sum
79conjecture  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
80instantiation110, 111, 603  ⊢  
  : , :
81instantiation112, 113  ⊢  
  : , :
82instantiation472, 148  ⊢  
  :
83instantiation573, 114, 115  ⊢  
  : , : , :
84instantiation632, 628, 116  ⊢  
  : , : , :
85instantiation546, 117  ⊢  
  : , :
86conjecture  ⊢  
 proveit.numbers.absolute_value.abs_frac
87instantiation119, 541, 118  ⊢  
  : , :
88instantiation119, 541, 120  ⊢  
  : , :
89instantiation121, 122  ⊢  
  : , :
90instantiation573, 123, 124  ⊢  
  : , : , :
91conjecture  ⊢  
 proveit.numbers.exponentiation.exp_nat_pos_expansion
92conjecture  ⊢  
 proveit.core_expr_types.operations.operands_substitution_via_tuple
93instantiation125, 634  ⊢  
  : , :
94instantiation126  ⊢  
  :
95conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
96conjecture  ⊢  
 proveit.trigonometry.sine_linear_bound_by_arg_pos
97conjecture  ⊢  
 proveit.trigonometry.sine_linear_bound_nonneg
98instantiation424, 127, 128  ⊢  
  : , : , :
99instantiation573, 129, 130  ⊢  
  : , : , :
100instantiation573, 131, 132  ⊢  
  : , : , :
101instantiation463, 133, 134  ⊢  
  : , : , :
102instantiation573, 135, 136  ⊢  
  : , : , :
103instantiation458, 612, 480  ⊢  
  : , :
104instantiation458, 479, 480  ⊢  
  : , :
105instantiation632, 519, 137  ⊢  
  : , : , :
106conjecture  ⊢  
 proveit.physics.quantum.QPE._alpha_m_mod_as_geometric_sum
107conjecture  ⊢  
 proveit.physics.quantum.QPE._phase_from_best_with_delta_b
108instantiation529, 530, 634, 624, 531, 138, 166, 590, 139  ⊢  
  : , : , : , : , : , :
109instantiation140, 166, 590, 141  ⊢  
  : , : , :
110conjecture  ⊢  
 proveit.numbers.addition.add_int_closure_bin
111instantiation632, 142, 602  ⊢  
  : , : , :
112conjecture  ⊢  
 proveit.numbers.addition.subtraction.nonneg_difference
113instantiation561, 602  ⊢  
  :
114instantiation582, 143  ⊢  
  : , : , :
115instantiation144, 289, 171, 535, 145*  ⊢  
  : , : , :
116instantiation632, 607, 146  ⊢  
  : , : , :
117instantiation433, 146  ⊢  
  :
118instantiation335, 147  ⊢  
  :
119conjecture  ⊢  
 proveit.numbers.addition.add_complex_closure_bin
120instantiation335, 148  ⊢  
  :
121conjecture  ⊢  
 proveit.numbers.addition.subtraction.nonzero_difference_if_different
122instantiation213, 149  ⊢  
  : , :
123instantiation594, 634, 150, 151, 152, 153  ⊢  
  : , : , : , :
124instantiation293, 495, 154, 155  ⊢  
  : , : , :
125conjecture  ⊢  
 proveit.core_expr_types.tuples.range_from1_len_typical_eq
126conjecture  ⊢  
 proveit.numbers.numerals.decimals.reduce_2_repeats
127instantiation424, 403, 156  ⊢  
  : , : , :
128instantiation280, 479, 612, 342, 157*  ⊢  
  : , :
129instantiation582, 158  ⊢  
  : , : , :
130instantiation573, 159, 160  ⊢  
  : , : , :
131instantiation392, 530, 624, 531, 612, 535, 480  ⊢  
  : , : , : , : , : , : , :
132instantiation413, 624, 634, 530, 161, 531, 535, 612, 480  ⊢  
  : , : , : , : , : , :
133instantiation493, 541, 189, 494, 162, 163  ⊢  
  : , : , : , : , :
134instantiation582, 164  ⊢  
  : , : , :
135instantiation582, 498  ⊢  
  : , : , :
136instantiation610, 165  ⊢  
  :
137instantiation632, 470, 539  ⊢  
  : , : , :
138instantiation609  ⊢  
  : , :
139instantiation335, 166  ⊢  
  :
140conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_13
141instantiation566  ⊢  
  :
142conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
143instantiation573, 167, 168  ⊢  
  : , : , :
144conjecture  ⊢  
 proveit.numbers.exponentiation.complex_power_of_complex_power
145instantiation456, 530, 623, 624, 531, 169, 612, 479, 308, 590, 535  ⊢  
  : , : , : , : , : , :
146instantiation618, 619, 321  ⊢  
  : , :
147instantiation442, 235, 170  ⊢  
  : , :
148instantiation442, 235, 171  ⊢  
  : , :
149instantiation424, 172, 173  ⊢  
  : , : , :
150instantiation609  ⊢  
  : , :
151instantiation609  ⊢  
  : , :
152instantiation177, 405, 174, 178*, 175*, 176*  ⊢  
  : , :
153instantiation177, 405, 201, 178*, 179*, 180*  ⊢  
  : , :
154instantiation589, 181, 182  ⊢  
  :
155instantiation632, 621, 183  ⊢  
  : , : , :
156instantiation392, 530, 624, 531, 535, 479, 480  ⊢  
  : , : , : , : , : , : , :
157instantiation573, 184, 432  ⊢  
  : , : , :
158instantiation456, 624, 414, 530, 356, 531, 612, 535, 479, 480  ⊢  
  : , : , : , : , : , :
159instantiation573, 185, 186  ⊢  
  : , : , :
160instantiation583, 217  ⊢  
  :
161instantiation609  ⊢  
  : , :
162instantiation632, 519, 187  ⊢  
  : , : , :
163instantiation632, 519, 220  ⊢  
  : , : , :
164instantiation582, 188  ⊢  
  : , : , :
165instantiation191, 189, 294, 190  ⊢  
  : , :
166instantiation191, 192, 535, 193  ⊢  
  : , :
167instantiation529, 530, 634, 624, 531, 194, 535, 533, 541  ⊢  
  : , : , : , : , : , :
168instantiation195, 541, 535, 536  ⊢  
  : , : , :
169instantiation329  ⊢  
  : , : , : , :
170instantiation463, 196, 197  ⊢  
  : , : , :
171instantiation463, 198, 199  ⊢  
  : , : , :
172instantiation200, 201, 202, 203*  ⊢  
  :
173instantiation582, 204  ⊢  
  : , : , :
174instantiation463, 373, 349  ⊢  
  : , : , :
175instantiation409, 205  ⊢  
  : , :
176instantiation573, 206, 207  ⊢  
  : , : , :
177conjecture  ⊢  
 proveit.trigonometry.complex_unit_circle_chord_length
178instantiation573, 208, 209  ⊢  
  : , : , :
179instantiation409, 210  ⊢  
  : , :
180instantiation573, 211, 212  ⊢  
  :