logo
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 ModAdd
from proveit.physics.quantum.QPE import (
        _alpha_are_complex, _alpha_summed,
        _b_floor, _best_floor_is_int, _delta_b_floor_diff_in_interval,
        _delta_b_is_real, _delta_b_not_eq_scaledNonzeroInt, _mod_add_closure,
        _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 = _mod_add_closure.instantiate({a: _b_floor, b:l})
_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]:
_alpha_are_complex.instantiate({m: ModAdd(_b_floor, l)})

(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) Bound the numerator and the denominator of the fraction.

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  ⊢  
 proveit.numbers.numerals.decimals.add_1_1
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  ⊢  
  : , : , :