Proof of proveit.physics.quantum.QPE._e_value_in_e_domain theorem¶

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b # used in an instantiation dict
from proveit.numbers import (
zero, one, two, Add, frac, greater, Integer, Mult,
NaturalPos, Neg, Real, subtract)
from proveit.physics.quantum.QPE import (
_e_domain, _eps_in_interval, _e_value, _e_value_ge_two,
_n, _n_ge_two, _n_in_natural_pos, _t, _t_in_natural_pos, _t_req)

In [2]:
%proving _e_value_in_e_domain

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

In [4]:
_t_in_natural_pos

In [5]:
_n_ge_two

In [6]:
_t_req

In [7]:
_eps_in_interval

In [8]:
bound_01 = _t_req.right_add_both_sides(Neg(_n))

bound_01:
In [9]:
_eps_le_one = _eps_in_interval.derive_element_upper_bound()

_eps_le_one:
In [10]:
greater(Add(two, frac(one, two)), zero).prove()

In [11]:
bound_02 = bound_01.rhs.deduce_bound(_eps_le_one)

bound_02:
In [12]:
bound_03 = bound_01.apply_transitivity(bound_02)

bound_03:
In [13]:
from proveit.numbers.logarithms import log_base_large_a_greater_one
log_base_large_a_greater_one

In [14]:
_a_sub, _b_sub = (
bound_03.rhs.operand.base,
bound_03.rhs.operand.antilog)
log_base_2_of_stuff_greater_than_one = log_base_large_a_greater_one.instantiate(
{a: _a_sub, b: _b_sub})

log_base_2_of_stuff_greater_than_one:
In [15]:
bound_04 = bound_03.rhs.deduce_bound(log_base_2_of_stuff_greater_than_one)

bound_04:
In [16]:
bound_05 = bound_03.apply_transitivity(bound_04)

bound_05:
In [17]:
_e_value_ge_two

In [18]:
_n_ge_two

In [19]:
bound_06 = _e_value.deduce_bound(_n_ge_two)

bound_06:
In [20]:
bound_07 = bound_06.add_right(bound_06.rhs)

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

In [21]:
%qed

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

Out[21]:
step typerequirementsstatement
0instantiation1, 2, 3, 4, 5
: , : , :
1conjecture
proveit.numbers.number_sets.integers.in_interval
2reference316
3instantiation110, 6, 112
: , :
4instantiation110, 7, 31
: , :
5instantiation170, 8, 9
: , :
6instantiation10, 280, 11
: , :
7instantiation317, 116, 12
: , : , :
8instantiation158, 90, 264, 13, 14, 15*, 16*
: , : , :
9instantiation17, 18, 19
: , : , :
10conjecture
proveit.numbers.exponentiation.exp_int_closure
11instantiation103, 20, 21
:
12instantiation59, 290, 67
: , :
13instantiation177, 26, 311
: , :
14instantiation126, 264, 26, 311, 22, 23
: , : , :
15instantiation24, 272, 251, 142
: , : , :
16instantiation224, 25
: , : , :
17theorem
proveit.logic.equality.sub_right_side_into
18instantiation126, 26, 60, 27, 28, 29*
: , : , :
19instantiation224, 30
: , : , :
20instantiation110, 111, 31
: , :
21instantiation113, 32
: , :
22conjecture
proveit.physics.quantum.QPE._e_value_ge_two
23instantiation250, 319
:
24conjecture
25instantiation245, 33, 34
: , : , :
26instantiation177, 57, 90
: , :
27instantiation158, 90, 57, 92, 35
: , : , :
28instantiation158, 90, 311, 92, 36, 37*
: , : , :
29instantiation136, 38, 39, 40
: , : , : , :
30instantiation224, 41
: , : , :
31instantiation317, 117, 42
: , : , :
32instantiation47, 200
:
33instantiation191, 192, 290, 319, 193, 43, 44, 65, 272
: , : , : , : , : , :
34instantiation168, 272, 44, 50
: , : , :
35instantiation45, 264, 127, 86, 291, 46
: , : , :
36instantiation47, 48
:
37instantiation49, 272, 50
: , :
38instantiation191, 192, 290, 319, 193, 52, 84, 65, 51
: , : , : , : , : , :
39instantiation191, 290, 192, 52, 193, 84, 65
: , : , : , : , : , :
40instantiation136, 53, 54, 55
: , : , : , :
41instantiation56, 65, 169
: , :
42instantiation121, 295
:
43instantiation270
: , :
44instantiation317, 279, 57
: , : , :
45conjecture
proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
46instantiation187, 179, 217, 178, 58
: , : , :
47conjecture
proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
48instantiation59, 290, 99
: , :
49conjecture
50instantiation219
:
51instantiation317, 279, 60
: , : , :
52instantiation270
: , :
53instantiation106, 319, 84, 65
: , : , : , : , : , : , :
54instantiation107, 192, 290, 193, 61, 63, 84, 65, 62*
: , : , : , : , : , :
55instantiation107, 319, 290, 192, 63, 193, 64, 65, 66*
: , : , : , : , : , :
56conjecture
57instantiation98, 264, 67
: , :
58instantiation68, 264, 240, 119
: , :
59conjecture
proveit.numbers.exponentiation.exp_natpos_closure
60instantiation177, 92, 90
: , :
61instantiation270
: , :
62instantiation69, 70, 71*
: , :
63instantiation270
: , :
64instantiation72, 251, 73
: , :
65instantiation164, 272
:
66instantiation74, 272, 251, 142
: , : , :
67instantiation103, 75, 76
:
68conjecture
proveit.numbers.negation.negated_weak_bound
69theorem
proveit.logic.equality.equals_reversal
70instantiation77, 192, 290, 319, 193, 78, 272, 84, 79*
: , : , : , : , : , :
71instantiation245, 80, 81
: , : , :
72conjecture
proveit.numbers.exponentiation.exp_complex_closure
73instantiation317, 279, 82
: , : , :
74conjecture
75instantiation110, 111, 83
: , :
76instantiation113, 120
: , :
77conjecture
proveit.numbers.multiplication.distribute_through_sum
78instantiation270
: , :
79instantiation238, 84
:
80instantiation224, 142
: , : , :
81instantiation85, 251, 311, 86, 87, 88*, 89*
: , : , :
82instantiation177, 90, 179
: , :
83instantiation317, 117, 91
: , : , :
84instantiation317, 279, 92
: , : , :
85conjecture
proveit.numbers.exponentiation.product_of_real_powers
86instantiation317, 313, 93
: , : , :
87instantiation94, 307
:
88instantiation95, 251
:
89instantiation245, 96, 97
: , : , :
90instantiation239, 311
:
91instantiation121, 256
:
92instantiation98, 264, 99
: , :
93instantiation317, 315, 104
: , : , :
94conjecture
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
95conjecture
proveit.numbers.exponentiation.complex_x_to_first_power_is_x
96instantiation191, 319, 290, 192, 100, 193, 272, 169, 150
: , : , : , : , : , :
97instantiation245, 101, 102
: , : , :
98conjecture
proveit.numbers.exponentiation.exp_real_closure_nat_power
99instantiation103, 104, 105
:
100instantiation270
: , :
101instantiation106, 319, 192, 193, 272, 169, 150
: , : , : , : , : , : , :
102instantiation107, 192, 290, 319, 193, 108, 272, 150, 169, 109*
: , : , : , : , : , :
103conjecture
proveit.numbers.number_sets.integers.nonneg_int_is_natural
104instantiation110, 111, 112
: , :
105instantiation113, 114
: , :
106conjecture
107conjecture
108instantiation270
: , :
109instantiation115, 272, 251, 142
: , : , :
110conjecture
111instantiation317, 116, 200
: , : , :
112instantiation317, 117, 118
: , : , :
113conjecture
114instantiation143, 119, 120
: , : , :
115conjecture
116conjecture
proveit.numbers.number_sets.integers.nat_pos_within_int
117conjecture
proveit.numbers.number_sets.integers.neg_int_within_int
118instantiation121, 307
:
119axiom
proveit.physics.quantum.QPE._n_ge_two
120instantiation158, 162, 264, 122, 123, 124*, 125*
: , : , :
121conjecture
proveit.numbers.negation.int_neg_closure
122instantiation177, 127, 264
: , :
123instantiation126, 264, 127, 128, 234
: , : , :
124instantiation245, 129, 130
: , : , :
125instantiation245, 131, 132
: , : , :
126conjecture
127instantiation177, 179, 217
: , :
128instantiation143, 133, 134
: , : , :
129instantiation191, 319, 290, 192, 149, 193, 251, 197, 150
: , : , : , : , : , :
130instantiation196, 251, 197, 167
: , : , :
131instantiation224, 135
: , : , :
132instantiation136, 137, 138, 139
: , : , : , :
133instantiation140, 316, 156, 141, 142*
: , :
134instantiation143, 144, 145
: , : , :
135instantiation191, 192, 290, 319, 193, 166, 169, 195, 251
: , : , : , : , : , :
136conjecture
proveit.logic.equality.four_chain_transitivity
137instantiation191, 192, 147, 319, 193, 148, 169, 195, 251, 146
: , : , : , : , : , :
138instantiation191, 147, 290, 192, 148, 149, 193, 169, 195, 251, 197, 150
: , : , : , : , : , :
139instantiation245, 151, 152
: , : , :
140conjecture
proveit.numbers.rounding.ceil_of_real_above_int
141instantiation153, 299, 173, 154
: , :
142conjecture
143conjecture
proveit.numbers.ordering.transitivity_less_eq_less_eq
144instantiation155, 156, 268, 157
: , :
145instantiation158, 217, 159, 179, 160, 161*
: , : , :
146instantiation317, 279, 162
: , : , :
147conjecture
proveit.numbers.numerals.decimals.nat3
148instantiation163
: , : , :
149instantiation270
: , :
150instantiation164, 251
:
151instantiation165, 290, 319, 192, 166, 193, 169, 195, 251, 197, 167
: , : , : , : , : , : , : , :
152instantiation168, 197, 169, 199
: , : , :
153conjecture
proveit.numbers.logarithms.log_base_large_a_greater_one
154instantiation170, 291, 171
: , :
155conjecture
proveit.numbers.rounding.ceil_increasing_less_eq
156instantiation274, 299, 173, 276
: , :
157instantiation172, 299, 173, 275, 174, 291
: , : , :
158conjecture
159instantiation177, 240, 218
: , :
160axiom
proveit.physics.quantum.QPE._t_req
161instantiation245, 175, 176
: , : , :
162instantiation177, 240, 178
: , :
163conjecture
proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
164conjecture
proveit.numbers.negation.complex_closure
165conjecture
166instantiation270
: , :
167instantiation219
:
168conjecture
169instantiation317, 279, 179
: , : , :
170theorem
proveit.logic.booleans.conjunction.and_if_both
171instantiation180, 264, 181, 182, 183, 184*, 185*
: , : , :
172conjecture
proveit.numbers.logarithms.log_increasing_less_eq
173instantiation317, 301, 186
: , : , :
174instantiation187, 264, 258, 188, 189, 190*
: , : , :
175instantiation191, 192, 290, 319, 193, 194, 197, 198, 195
: , : , : , : , : , :
176instantiation196, 197, 198, 199
: , : , :
177conjecture
178instantiation239, 264
:
179instantiation254, 255, 200
: , : , :
180conjecture
181instantiation201, 258, 310
: , :
182instantiation317, 313, 202
: , : , :
183instantiation203, 258, 310, 311, 204, 205
: , : , :
184instantiation245, 206, 207
: , : , :
185instantiation245, 208, 209
: , : , :
186instantiation285, 210, 302
: , :
187conjecture
188instantiation317, 211, 282
: , : , :
189instantiation212, 213, 297, 299, 214
: , : , :
190instantiation226, 280, 316, 227*, 215*, 216*
: , : , : , :
191conjecture
192axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
193conjecture
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
194instantiation270
: , :
195instantiation317, 279, 217
: , : , :
196conjecture
197instantiation317, 279, 240
: , : , :
198instantiation317, 279, 218
: , : , :
199instantiation219
:
200axiom
proveit.physics.quantum.QPE._t_in_natural_pos
201conjecture
proveit.numbers.multiplication.mult_real_closure_bin
202instantiation220, 269, 314
: , :
203conjecture
proveit.numbers.multiplication.strong_bound_via_right_factor_bound
204conjecture
proveit.numbers.numerals.decimals.less_0_1
205instantiation221, 278
:
206instantiation224, 222
: , : , :
207instantiation223, 251
:
208instantiation224, 225
: , : , :
209instantiation226, 316, 280, 227*, 228*, 235*
: , : , : , :
210instantiation317, 306, 229
: , : , :
211conjecture
proveit.numbers.number_sets.real_numbers.real_pos_within_real
212conjecture
proveit.numbers.division.weak_div_from_denom_bound__all_pos
213instantiation317, 230, 231
: , : , :
214instantiation232, 264, 304, 311, 233, 234, 235*
: , : , :
215instantiation245, 236, 237
: , : , :
216instantiation238, 251
:
217instantiation239, 240
:
218instantiation317, 313, 241
: , : , :
219axiom
proveit.logic.equality.equals_reflexivity
220conjecture
proveit.numbers.multiplication.mult_rational_closure_bin
221conjecture
proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
222instantiation242, 243
:
223conjecture
224axiom
proveit.logic.equality.substitution
225instantiation271, 243
:
226conjecture
227instantiation244, 251
:
228instantiation245, 246, 247
: , : , :
229conjecture
proveit.numbers.numerals.decimals.posnat5
230conjecture
proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
231instantiation317, 248, 319
: , : , :
232conjecture
proveit.numbers.multiplication.weak_bound_via_right_factor_bound
233instantiation249, 310, 311, 312
: , : , :
234instantiation250, 290
:
235instantiation271, 251
:
236instantiation259, 290, 252, 253, 263, 262
: , : , : , :
237conjecture