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

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import b, e, l, m, defaults
from proveit.logic import InSet
from proveit.numbers import Add, Neg, frac, one, four, NaturalPos, IntegerNeg
# import common expressions
from proveit.physics.quantum.QPE import _neg_domain, _pos_domain, ModAdd
# import theorems
from proveit.physics.quantum.QPE import (
_b_floor, _alpha_sqrd_upper_bound, _alpha_are_complex,
_t_in_natural_pos, _two_pow_t_is_nat_pos, _two_pow_t_minus_one_is_nat_pos,
_fail_sum, _delta_b_is_real, _best_floor_is_int,
_scaled_delta_b_not_eq_nonzeroInt)

In [2]:
%proving _failure_upper_bound_lemma

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_failure_upper_bound_lemma:
(see dependencies)
In [3]:
defaults.assumptions = _failure_upper_bound_lemma.conditions

defaults.assumptions:
In [4]:
defaults.preserved_exprs = {Neg(Add(e, one))} # don't simplify to -e - 1

defaults.preserved_exprs:

## Instantiate some needed theorems of this package¶

In [5]:
pos_assumptions = (InSet(l, _pos_domain),)+tuple(defaults.assumptions)

pos_assumptions:
In [6]:
neg_assumptions = (InSet(l, _neg_domain),)+tuple(defaults.assumptions)

neg_assumptions:
In [7]:
_alpha_sqrd_upper_bound.instantiate(assumptions=pos_assumptions).generalize(l, domain=_pos_domain)

In [8]:
_alpha_sqrd_upper_bound.instantiate(assumptions=neg_assumptions).generalize(l, domain=_neg_domain)

In [9]:
_best_floor_is_int

In [10]:
_delta_b_is_real

In [11]:
_delta_b_is_real.instantiate({b:_b_floor})

In [12]:
_scaled_delta_b_not_eq_nonzeroInt

In [13]:
_scaled_delta_b_not_eq_nonzeroInt.instantiate({b:_b_floor}, assumptions=pos_assumptions)

In [14]:
_scaled_delta_b_not_eq_nonzeroInt.instantiate({b:_b_floor}, assumptions=neg_assumptions)

In [15]:
_alpha_are_complex

In [16]:
_alpha_are_complex.instantiate({m:ModAdd(_b_floor, l)}, assumptions=pos_assumptions)

In [17]:
_alpha_are_complex.instantiate({m:ModAdd(_b_floor, l)}, assumptions=neg_assumptions)

In [18]:
fail_sum_inst = _fail_sum.instantiate()

fail_sum_inst:

## Upper bound each of the summations in fail_sum_inst via _alpha_sqrd_upper_bound¶

In [19]:
first_sum = fail_sum_inst.rhs.terms[0]

first_sum:
In [20]:
second_sum = fail_sum_inst.rhs.terms[1]

second_sum:
In [21]:
_alpha_sqrd_upper_bound

In [22]:
first_sum_bound = first_sum.deduce_bound(_alpha_sqrd_upper_bound)

first_sum_bound:
In [23]:
second_sum_bound = second_sum.deduce_bound(_alpha_sqrd_upper_bound)

second_sum_bound:

## Bound the sum of summations by the bound of the sum and simplify¶

In [24]:
bound_rhs = fail_sum_inst.rhs.deduce_bound([first_sum_bound, second_sum_bound])

bound_rhs:
_failure_upper_bound_lemma may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

In [25]:
not_yet_factored = fail_sum_inst.apply_transitivity(bound_rhs)

not_yet_factored:
In [26]:
not_yet_factored.inner_expr().rhs.factor(frac(one, four), auto_simplify=False)

In [27]:
%qed

proveit.physics.quantum.QPE._failure_upper_bound_lemma has been proven.

Out[27]:
step typerequirementsstatement
0generalization1
1instantiation2, 3, 4
: , : , :
2theorem
proveit.logic.equality.sub_right_side_into
3instantiation197, 5, 6
: , : , :
4instantiation192, 7, 8, 9
: , : , : , :
5instantiation10, 11, 12
: , : , :
6instantiation13, 288
:
7instantiation213, 14
: , : , :
8instantiation213, 15
: , : , :
9instantiation211, 16
: , :
10conjecture
proveit.numbers.ordering.transitivity_less_eq_less_eq
11instantiation137, 21, 17, 20, 18
: , : , :
12instantiation19, 20, 21, 22, 23
: , : , :
13conjecture
proveit.physics.quantum.QPE._fail_sum
14instantiation157, 24, 25
: , : , :
15instantiation157, 26, 27
: , : , :
16instantiation28, 289, 299, 207, 29, 208, 64, 30, 31
: , : , : , : , : , :
17modus ponens32, 33
18modus ponens34, 35
19conjecture
20modus ponens36, 37
21modus ponens38, 39
22modus ponens40, 41
23modus ponens42, 43
24instantiation213, 44
: , : , :
25instantiation211, 45
: , :
26instantiation213, 46
: , : , :
27instantiation211, 47
: , :
28conjecture
proveit.numbers.multiplication.distribute_through_sum
29instantiation103
: , :
30modus ponens48, 77
31modus ponens49, 81
32instantiation54
: , : , :
33generalization50
34instantiation56
: , : , :
35generalization51
36instantiation54
: , : , :
37generalization52
38instantiation54
: , : , :
39generalization53
40instantiation54
: , : , :
41generalization55
42instantiation56
: , : , :
43generalization57
44modus ponens58, 59
45instantiation60, 208, 64
: , :
46modus ponens61, 62
47instantiation63, 208, 64
: , :
48instantiation65
: , : , :
49instantiation65
: , : , :
50instantiation133, 66, 299,  ⊢
: , :
51instantiation73, 67, 186,  ⊢
:
52instantiation123, 261, 68, 69,  ⊢
: , :
53instantiation133, 70, 299,  ⊢
: , :
54conjecture
proveit.numbers.summation.summation_real_closure
55instantiation123, 261, 71, 72,  ⊢
: , :
56conjecture
proveit.numbers.summation.weak_summation_from_summands_bound
57instantiation73, 74, 191,  ⊢
:
58instantiation78, 267
: , : , : , : , : , : , :
59generalization75
60modus ponens76, 77
61instantiation78, 267
: , : , : , : , : , : , :
62generalization79
63modus ponens80, 81
64instantiation297, 260, 82
: , : , :
65conjecture
proveit.numbers.summation.summation_complex_closure
66instantiation297, 85, 83,  ⊢
: , : , :
67instantiation89, 235, 291, 200, 84,  ⊢
: , : , :
68instantiation203, 96, 119,  ⊢
: , :
69instantiation87, 299, 88, 109, 131,  ⊢
: , :
70instantiation297, 85, 86,  ⊢
: , : , :
71instantiation203, 96, 124,  ⊢
: , :
72instantiation87, 299, 88, 109, 135,  ⊢
: , :
73conjecture
proveit.physics.quantum.QPE._alpha_sqrd_upper_bound
74instantiation89, 235, 291, 223, 90,  ⊢
: , : , :
75instantiation211, 91,  ⊢
: , :
76instantiation94, 289, 267, 207
: , : , : , : , : , :
77generalization92
78conjecture
proveit.core_expr_types.lambda_maps.general_lambda_substitution
79instantiation211, 93,  ⊢
: , :
80instantiation94, 289, 267, 207
: , : , : , : , : , :
81generalization95
82instantiation123, 261, 96, 97
: , :
83instantiation101, 98,  ⊢
:
84instantiation104, 99, 100,  ⊢
: , :
85conjecture
proveit.numbers.number_sets.real_numbers.real_nonneg_within_real
86instantiation101, 102,  ⊢
:
87conjecture
proveit.numbers.multiplication.mult_not_eq_zero
88instantiation103
: , :
89conjecture
proveit.numbers.number_sets.integers.in_interval
90instantiation104, 105, 106,  ⊢
: , :
91instantiation108, 245, 109, 131, 110*,  ⊢
: , : , : , :
92instantiation297, 260, 107,  ⊢
: , : , :
93instantiation108, 245, 109, 135, 110*,  ⊢
: , : , : , :
94conjecture
proveit.numbers.multiplication.distribute_through_summation
95instantiation297, 260, 111,  ⊢
: , : , :
96instantiation297, 270, 112
: , : , :
97instantiation248, 152
:
98instantiation115, 113,  ⊢
:
99instantiation285, 235, 236, 237,  ⊢
: , : , :
100instantiation117, 114,  ⊢
: , :
101conjecture
proveit.numbers.absolute_value.abs_complex_closure
102instantiation115, 116,  ⊢
:
103conjecture
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
104theorem
proveit.logic.booleans.conjunction.and_if_both
105instantiation117, 118,  ⊢
: , :
106instantiation234, 255, 291, 256,  ⊢
: , : , :
107instantiation123, 261, 119, 120,  ⊢
: , :
108conjecture
proveit.numbers.division.prod_of_fracs
109instantiation297, 249, 121
: , : , :
110instantiation122, 245
:
111instantiation123, 261, 124, 125,  ⊢
: , :
112instantiation297, 277, 126
: , : , :
113instantiation129, 222, 200,  ⊢
: , :
114instantiation127, 202, 128,  ⊢
: , : , :
115conjecture
proveit.physics.quantum.QPE._alpha_are_complex
116instantiation129, 222, 223,  ⊢
: , :
117conjecture
proveit.numbers.ordering.relax_less
118instantiation217, 130, 224,  ⊢
: , : , :
119instantiation133, 163, 299,  ⊢
: , :
120instantiation134, 131,  ⊢
: