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

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, l, m, defaults
from proveit.logic import InSet
from proveit.numbers import Abs, Integer, Real, subtract, Mult, Exp
from proveit.physics.quantum.QPE import (
_alpha_are_complex, _alpha_summed,
_b_floor, _best_floor_is_int, _delta_b_floor_diff_in_interval,
_scaled_abs_delta_b_floor_diff_interval, _scaled_delta_b_not_eq_nonzeroInt,
_scaled_delta_b_floor_in_interval, _non_int_delta_b_diff,
_t_in_natural_pos, _two_pow_t_is_nat_pos, _two_pow_t_minus_one_is_nat_pos)
In [2]:
%proving _alpha_sqrd_upper_bound
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_alpha_sqrd_upper_bound:
(see dependencies)
In [3]:
defaults.assumptions = _alpha_sqrd_upper_bound.all_conditions()
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)

### (1) Some basic domain information needed throughout the proof¶

In [5]:
_two_pow_t_minus_one_is_nat_pos
In [6]:
_scaled_delta_b_floor_in_interval
In [7]:
InSet(subtract(_scaled_delta_b_floor_in_interval.element, l), Real).prove()
In [8]:
_scaled_abs_delta_b_floor_diff_interval.instantiate()
In [9]:
_delta_b_not_eq_scaledNonzeroInt.instantiate({b: _b_floor})
In [10]:
_delta_b_floor_diff_in_interval.instantiate()
In [11]:
_scaled_delta_b_not_eq_nonzeroInt.instantiate({b: _b_floor})
In [12]:
_best_floor_is_int
In [13]:
_b_floor_plus_ell_in_interval:
In [14]:
_delta_b_is_real.instantiate({b: _b_floor})
In [15]:
_two_pow_t_is_nat_pos
In [16]:
_b_floor_plus_ell_in_interval.derive_element_in_integer()
In [17]:

### (2) Starting Point: _alpha_summed¶

In [18]:
_alpha_summed_inst = _alpha_summed.instantiate()
_alpha_summed_inst: ,  ⊢

### (3) Take Abs() of Both Sides & Allow Auto-Simplification of the Denominator¶

In [19]:
# We want to temporarily preserve the resulting numerator
# so it isn't auto-simplified, so we first give it a convenient label
numerator = Abs(_alpha_summed_inst.rhs.factors[1].numerator)
numerator:
In [20]:
_non_int_delta_b_diff
In [21]:
_non_int_delta_b_diff.instantiate({b:_b_floor})
In [22]:
# In applying the Abs() to both sides, we avoid the auto-simplifying
# chord-length simplification in the numerator by using 'preserve_expr':
_alpha_summed_inst_abs = _alpha_summed_inst.abs_both_sides(preserve_expr=numerator)
_alpha_summed_inst_abs: ,  ⊢
In [23]:
_alpha_summed_inst_abs_dist = (
_alpha_summed_inst_abs.inner_expr().rhs.distribute(preserve_expr=numerator))
_alpha_summed_inst_abs_dist: ,  ⊢

### 4(a) Use a triangle inequality for the numerator.¶

In [24]:
numer_bound = numerator.deduce_triangle_bound()
numer_bound:

### 4(b) Bound the $y = \sin(\theta)$ in the denominator by the chord $y = (\frac{2}{\pi}\theta)$¶

In [25]:
denom_sin = _alpha_summed_inst_abs_dist.rhs.denominator.factors[2]
denom_sin:
In [26]:
denom_sin_bound = denom_sin.deduce_linear_bound()
denom_sin_bound: ,  ⊢
In [27]:
sin_bound_is_positive = denom_sin_bound.rhs.deduce_positive()
sin_bound_is_positive: ,  ⊢
In [28]:
denom_sin_is_positive = denom_sin_bound.apply_transitivity(sin_bound_is_positive)
denom_sin_is_positive: ,  ⊢
In [29]:
denominator = _alpha_summed_inst_abs_dist.rhs.denominator
denominator:
In [30]:
denom_bound = denominator.deduce_bound(denom_sin_bound)
denom_bound: ,  ⊢
In [31]:
denom_is_positive = denominator.deduce_bound(denom_sin_is_positive)
denom_is_positive: ,  ⊢

### (5) Now we use the numerator and denominator bounds to bound $|\alpha_{b_{f}\oplus\ell}|$¶

In [32]:
# recall from earlier:
_alpha_summed_inst_abs_dist
In [33]:
rhs_bound = _alpha_summed_inst_abs_dist.rhs.deduce_bound([numer_bound, denom_bound])
rhs_bound: ,  ⊢
In [34]:
alpha_upper_bound_01 = _alpha_summed_inst_abs_dist.apply_transitivity(rhs_bound)
alpha_upper_bound_01: ,  ⊢

### (6) Simplify and square both sides¶

In [35]:
alpha_upper_bound_02 = alpha_upper_bound_01.inner_expr().rhs.denominator.associate(1, 2)
alpha_upper_bound_02: ,  ⊢
In [36]:
alpha_upper_bound_03 = (
alpha_upper_bound_02.inner_expr().rhs.denominator.operands[1].distribute(1))
alpha_upper_bound_03: ,  ⊢
In [37]:
with Exp.temporary_simplification_directives() as tmp_directives:
tmp_directives.distribute_exponent=True
alpha_upper_bound_03.square_both_sides()
_alpha_sqrd_upper_bound may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [38]:
%qed
proveit.physics.quantum.QPE._alpha_sqrd_upper_bound has been proven.
Out[38]:
step typerequirementsstatement
0generalization1
1instantiation576, 2, 3,  ⊢
: , : , :
2instantiation4, 684, 5, 6, 7, 8, 9*,  ⊢
: , : , :
3instantiation667, 10
: , : , :
4conjecture
proveit.numbers.exponentiation.exp_pos_lesseq
5instantiation705, 500, 21
: , : , :
6instantiation428, 657, 24, 16,  ⊢
: , :
7instantiation343, 11, 12,  ⊢
: , :
8instantiation13, 696
:
9instantiation14, 642, 15, 696, 16, 17*, 18*,  ⊢
: , : , :
10instantiation667, 19
: , : , :
11instantiation20, 21
:
12instantiation576, 22, 23,  ⊢
: , : , :
13conjecture
proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
14conjecture
proveit.numbers.exponentiation.posnat_power_of_quotient
15instantiation705, 683, 24
: , : , :
16instantiation418, 704, 25, 611, 26,  ⊢
: , :
17instantiation27, 677
:
18instantiation28, 677, 29, 696, 30*, 31*
: , : , :
19instantiation32, 413, 702, 668*, 33*
: , :
20conjecture
proveit.numbers.number_sets.real_numbers.nonneg_if_in_real_nonneg
21instantiation525, 82
:
22instantiation576, 34, 35,  ⊢
: , : , :
23instantiation36, 702, 704, 593, 594, 107, 37, 543, 38, 39*,  ⊢
: , : , : , : , : , :
24instantiation638, 684, 41
: , :
25instantiation645
: , :
26instantiation705, 633, 40,  ⊢
: , : , :
27conjecture
proveit.numbers.exponentiation.exponentiated_one
28conjecture
proveit.numbers.exponentiation.posnat_power_of_product
29instantiation705, 683, 41
: , : , :
30instantiation579, 42, 43, 569
: , : , : , :
31instantiation44, 440
:
32conjecture
proveit.numbers.exponentiation.even_pow_is_even_fn_rev
33instantiation579, 45, 46, 47
: , : , : , :
34instantiation331, 48, 49,  ⊢
: , : , :
35instantiation534, 702, 704, 593, 197, 594, 677, 470, 459
: , : , : , : , : , :
36conjecture
proveit.numbers.multiplication.distribute_through_abs_sum
37instantiation645
: , :
38instantiation705, 683, 50,  ⊢
: , : , :
39instantiation540, 470, 51, 52*,  ⊢
: , :
40instantiation705, 620, 53,  ⊢
: , : , :
41instantiation705, 500, 54
: , : , :
42instantiation55, 696, 677
: , :
43instantiation56, 704, 57, 629, 58
: , : , : , :
44conjecture
proveit.numbers.exponentiation.square_abs_real_simp
45instantiation59, 73, 596
: , :
46instantiation389, 60, 596
: , :
47instantiation658
:
48instantiation61, 62, 63,  ⊢
: , : , :
49instantiation576, 64, 65,  ⊢
: , : , :
50instantiation705, 690, 66,  ⊢
: , : , :
51instantiation705, 683, 67,  ⊢
: , : , :
52instantiation576, 68, 69
: , : , :
53instantiation441, 70,  ⊢
:
54instantiation525, 413
:
55conjecture
proveit.numbers.exponentiation.exp_nat_pos_expansion
56conjecture
proveit.core_expr_types.operations.operands_substitution_via_tuple
57instantiation71, 704
: , :
58instantiation72
:
59conjecture
proveit.numbers.negation.distribute_neg_through_subtract
60instantiation539, 73
:
61conjecture
proveit.numbers.ordering.transitivity_less_eq_less_eq
62instantiation74, 103, 156, 684, 75, 104,  ⊢
: , : , :
63instantiation76, 106, 77, 78, 79, 80*,  ⊢
: , : , :
64instantiation81, 82, 83, 84, 85*,  ⊢
: , :
65instantiation287, 642, 122, 230, 86, 87*, 88*,  ⊢
: , : , : , :
66instantiation705, 671, 89,  ⊢
: , : , :
67instantiation705, 690, 90,  ⊢
: , : , :
68instantiation576, 91, 92
: , : , :
69instantiation579, 93, 94, 95
: , : , : , :
70instantiation462, 413, 96,  ⊢
:
71conjecture
proveit.core_expr_types.tuples.range_from1_len_typical_eq
72conjecture
proveit.numbers.numerals.decimals.reduce_2_repeats
73instantiation705, 683, 460
: , : , :
74conjecture
proveit.numbers.division.weak_div_from_numer_bound__pos_denom
75instantiation97, 642, 247, 98*
: , :
76conjecture
proveit.numbers.division.weak_div_from_denom_bound__all_pos
77instantiation99, 529, 100, 101, 138, 414,  ⊢
: , :
78instantiation102, 103, 104,  ⊢
:
79instantiation105, 704, 593, 260, 594, 106, 107, 246, 108*,  ⊢
: , : , : , : , : , :
80instantiation579, 109, 110, 111,  ⊢
: , : , : , :
81conjecture
proveit.numbers.absolute_value.abs_eq
82instantiation112, 113
:
83instantiation528, 116, 117,  ⊢
: , :
84instantiation114, 679, 504,  ⊢
:
85instantiation337, 696, 115, 116, 117, 118*, 119*,  ⊢
: , :
86instantiation120, 611, 121,  ⊢
: , :
87instantiation666, 122
:
88instantiation652, 123, 124,  ⊢
: , : , :
89instantiation125, 126,  ⊢
:
90instantiation705, 671, 126,  ⊢
: , : , :
91instantiation127, 642, 596, 230, 610
: , : , : , : , :
92instantiation652, 128, 129
: , : , :
93instantiation667, 614
: , : , :
94instantiation667, 130
: , : , :
95instantiation666, 596
:
96instantiation485, 131,  ⊢
: , :
97conjecture
proveit.numbers.absolute_value.triangle_inequality
98instantiation652, 132, 133
: , : , :
99conjecture
proveit.numbers.multiplication.mult_real_pos_closure
100instantiation550
: , : , :
101instantiation705, 345, 134
: , : , :
102conjecture
proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
103instantiation576, 135, 136,  ⊢
: , : , :
104instantiation137, 704, 593, 260, 594, 314, 138, 217, 139*,  ⊢
: , : , : , : , : , :
105conjecture
proveit.numbers.multiplication.weak_bound_via_factor_bound
106instantiation705, 141, 140
: , : , :
107instantiation705, 141, 142
: , : , :
108instantiation652, 143, 144
: , : , :
109instantiation652, 145, 146,  ⊢
: , : , :
110instantiation658
:
111instantiation455, 147,  ⊢
: , :
112conjecture
proveit.physics.quantum.QPE._alpha_are_complex
113instantiation148, 619, 670
: , :
114conjecture
proveit.physics.quantum.QPE._alpha_summed
115instantiation645
: , :
116instantiation705, 683, 149
: , : , :
117instantiation286, 218, 152, 153,  ⊢
: , :
118instantiation369, 150
:
119instantiation151, 218, 152, 153, 154*,  ⊢
: , :
120conjecture
proveit.numbers.multiplication.mult_complex_nonzero_closure_bin
121instantiation462, 167, 155,  ⊢
:
122instantiation705, 683, 156
: , : , :
123instantiation591, 702, 704, 593, 157, 594, 470, 677, 167,  ⊢
: , : , : , : , : , :
124instantiation533, 593, 702, 594, 470, 677, 167,  ⊢
: , : , : , : , : , : , :
125conjecture
proveit.numbers.negation.rational_nonzero_closure
126instantiation158, 159, 291,  ⊢
: , :
127conjecture
proveit.numbers.division.mult_frac_cancel_numer_left
128instantiation667, 160
: , : , :
129instantiation667, 161
: , : , :
130instantiation669, 596
:
131instantiation162, 503, 670, 504,  ⊢
: , :
132instantiation627, 704, 163, 164, 165, 166
: , : , : , :
133conjecture
134instantiation705, 674, 606
: , : , :
135instantiation638, 290, 216,  ⊢
: , :
136instantiation591, 593, 704, 702, 594, 260, 677, 470, 167,  ⊢
: , : , : , : , : , :
137conjecture
proveit.numbers.multiplication.strong_bound_via_factor_bound
138instantiation705, 345, 233
: , : , :
139instantiation168, 704, 593, 260, 594, 677, 470
: , : , : , :
140instantiation705, 169, 704
: , : , :
141conjecture
proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
142instantiation705, 169, 170
: , : , :
143instantiation591, 704, 593, 260, 458, 594, 677, 470, 459
: , : , :