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

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import m, n, defaults
from proveit.physics.quantum import var_ket_psi
from proveit.physics.quantum.circuits import born_rule_on_register, Qcircuit
from proveit.physics.quantum.QPE import (
_alpha_m_def, _ket_u, _Psi_ket, _Psi_ket_is_normalized_vec,
_Psi_output, _psi_t_ket_is_normalized_vec,
_s, _s_in_nat_pos, _t, _t_in_natural_pos, _u_ket_register)

In [2]:
%proving _outcome_prob

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_outcome_prob:
(see dependencies)
In [3]:
from proveit.numbers import Mult
Mult.change_simplification_directives(combine_all_exponents=True)

In [4]:
defaults.assumptions = _outcome_prob.conditions

defaults.assumptions:
In [5]:
_alpha_m_def

In [6]:
alpha_m_replacement = _alpha_m_def.instantiate().derive_reversed()

alpha_m_replacement:
In [7]:
born_rule_on_register

In [8]:
born_rule_prob = born_rule_on_register.instantiate({m:_t, n:m, var_ket_psi:_Psi_ket},
replacements=[alpha_m_replacement])

born_rule_prob:
In [9]:
qcircuit_prob2 = Qcircuit.trivial_expansion_below(born_rule_prob, _ket_u, _s)

qcircuit_prob2:
In [10]:
_Psi_output

In [11]:
qcircuit_prob3 = Qcircuit.concatenation(_Psi_output, qcircuit_prob2)

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

In [12]:
%qed

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

Out[12]:
step typerequirementsstatement
0generalization1
1instantiation193, 2, 3
: , : , :
2instantiation207, 4, 5
: , : , :
3modus ponens6, 7
4instantiation8, 393, 28, 122, 9*
: , : , :
5instantiation10, 289, 393, 379, 92, 11, 93, 12
: , : , : , : , : , : , :
6instantiation13, 163, 257, 14, 73, 89, 15*, 16*
: , : , : , : , : , :
7conjecture
proveit.physics.quantum.QPE._Psi_output
8conjecture
proveit.physics.quantum.circuits.born_rule_on_register
9instantiation309, 17
: , :
10conjecture
proveit.physics.quantum.circuits.trivial_expansion_below
11instantiation18, 393, 28
: , :
12instantiation285, 19, 341, 20
: , : , : , :
13conjecture
proveit.physics.quantum.circuits.concat_onto_ideal_expt
14instantiation377, 21, 22
: , : , :
15instantiation355, 23, 24
: , : , :
16instantiation355, 25, 26
: , : , :
17instantiation27, 28
:
18conjecture
proveit.physics.quantum.algebra.num_ket_in_register_space
19instantiation195, 192
: , :
20instantiation309, 29
: , :
21instantiation30, 163, 31, 42, 44, 32*
: , : , :
22instantiation33, 163, 34, 35, 36, 91, 92, 93
: , : , : , :
23instantiation368, 37
: , : , :
24instantiation309, 38
: , :
25instantiation368, 39
: , : , :
26instantiation309, 40
: , :
27axiom
proveit.physics.quantum.QPE._alpha_m_def
28assumption
29instantiation195, 192
: , :
30conjecture
proveit.linear_algebra.tensors.tensor_prod_of_cart_exps_within_cart_exp
31instantiation359
: , :
32instantiation41, 347, 393, 379
: , : , :
33conjecture
proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space
34instantiation359
: , :
35instantiation43, 42
:
36instantiation43, 44
:
37instantiation47, 289, 45
: , : , :
38instantiation49, 46
: , :
39instantiation47, 289, 48
: , : , :
40instantiation49, 50
: , :
41conjecture
proveit.numbers.exponentiation.product_of_posnat_powers
42instantiation51, 391, 192
: , :
43conjecture
proveit.linear_algebra.complex_vec_set_is_vec_space
44instantiation51, 391, 194
: , :
45modus ponens52, 53
46modus ponens54, 55
47conjecture
proveit.core_expr_types.tuples.tuple_eq_via_elem_eq
48modus ponens56, 57
49conjecture
proveit.physics.quantum.circuits.prob_eq_via_equiv
50modus ponens58, 59
51conjecture
proveit.numbers.exponentiation.exp_natpos_closure
52instantiation75, 190, 60, 61, 62, 63, 64, 65, 66, 67
: , : , : , :
53instantiation82, 190, 68, 69, 70, 71, 72
: , : , :
54instantiation88, 391, 396, 337, 73, 338
: , : , : , : , : , : , : , :
55instantiation74, 163, 316, 393, 379, 91, 92, 93, 94, 95, 166, 96, 97, 98, 180, 337, 192, 196, 99, 177*
: , : , : , : , : , :
56instantiation75, 190, 257, 76, 77, 78, 79, 80, 81
: , : , : , :
57instantiation82, 190, 83, 84, 85, 86, 87
: , : , :
58instantiation88, 337, 396, 391, 338, 89
: , : , : , : , : , : , :