Expression of type Conditional ¶

from the theory of proveit.physics.quantum.circuits ¶

import proveit
# Automation is not needed when building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_expr # Load the stored expression as 'stored_expr'
# import Expression classes needed to build the expression
from proveit import Conditional, m, n
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import Abs, Exp, NaturalPos, two
from proveit.physics.quantum import NumBra, Qmult, m_bit_interval, m_ket_domain, normalized_var_ket_psi, var_ket_psi
from proveit.physics.quantum.circuits import register_meas
from proveit.statistics import Prob

# build up the expression from sub-expressions
expr = Conditional(Forall(instance_param_or_params = [n], instance_expr = Forall(instance_param_or_params = [var_ket_psi], instance_expr = Equals(Prob(register_meas), Exp(Abs(Qmult(NumBra(n, m), var_ket_psi)), two)), domain = m_ket_domain, condition = normalized_var_ket_psi), domain = m_bit_interval), InSet(m, NaturalPos))

# check that the built expression is the same as the stored expression
assert expr == stored_expr
assert expr._style_id == stored_expr._style_id
print("Passed sanity check: expr matches stored_expr")

Passed sanity check: expr matches stored_expr

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\left\{\forall_{n \in \{0~\ldotp \ldotp~2^{m} - 1\}}~\left[\forall_{\lvert \psi \rangle \in \mathbb{C}^{2^{m}}~|~\left \|\lvert \psi \rangle\right \| = 1}~\left(\textrm{Pr}\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\multiqin{3}{\lvert \psi \rangle} & \meter & \multiqout{3}{\lvert n \rangle_{m}} \\
\ghostqin{\lvert \psi \rangle} & \meter & \ghostqout{\lvert n \rangle_{m}} \\
\ghostqin{\lvert \psi \rangle} & \measure{\begin{array}{c}:\\ \left(m - 3\right) \times \\:\end{array}} \qw & \ghostqout{\lvert n \rangle_{m}} \\
\ghostqin{\lvert \psi \rangle} & \meter & \ghostqout{\lvert n \rangle_{m}}
} \end{array}\right) = \left|{_{m}}\langle n \rvert \thinspace \lvert \psi \rangle\right|^{2}\right)\right] \textrm{ if } m \in \mathbb{N}^+\right..

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions
0	Conditional	value: 1 condition: 2
1	Operation	operator: 11 operand: 5
2	Operation	operator: 35 operands: 4
3	ExprTuple	5
4	ExprTuple	98, 6
5	Lambda	parameter: 97 body: 8
6	Literal
7	ExprTuple	97
8	Conditional	value: 9 condition: 10
9	Operation	operator: 11 operand: 14
10	Operation	operator: 35 operands: 13
11	Literal
12	ExprTuple	14
13	ExprTuple	97, 15
14	Lambda	parameter: 91 body: 16
15	Operation	operator: 89 operands: 17
16	Conditional	value: 18 condition: 19
17	ExprTuple	20, 21
18	Operation	operator: 37 operands: 22
19	Operation	operator: 23 operands: 24
20	Literal
21	Operation	operator: 25 operands: 26
22	ExprTuple	27, 28
23	Literal
24	ExprTuple	29, 30
25	Literal
26	ExprTuple	58, 31
27	Operation	operator: 32 operand: 41
28	Operation	operator: 64 operands: 34
29	Operation	operator: 35 operands: 36
30	Operation	operator: 37 operands: 38
31	Operation	operator: 39 operand: 94
32	Literal
33	ExprTuple	41
34	ExprTuple	42, 70
35	Literal
36	ExprTuple	91, 43
37	Literal
38	ExprTuple	44, 94
39	Literal
40	ExprTuple	94
41	Operation	operator: 45 operands: 46
42	Operation	operator: 47 operand: 56
43	Operation	operator: 49 operands: 50
44	Operation	operator: 51 operand: 91
45	Literal
46	ExprTuple	53, 54, 55
47	Literal
48	ExprTuple	56
49	Literal
50	ExprTuple	57, 58
51	Literal
52	ExprTuple	91
53	ExprTuple	59
54	ExprTuple	60
55	ExprTuple	61
56	Operation	operator: 62 operands: 63
57	Literal
58	Operation	operator: 64 operands: 65
59	ExprRange	lambda_map: 66 start_index: 94 end_index: 98
60	ExprRange	lambda_map: 67 start_index: 94 end_index: 98
61	ExprRange	lambda_map: 68 start_index: 94 end_index: 98
62	Literal
63	ExprTuple	69, 91
64	Literal
65	ExprTuple	70, 98
66	Lambda	parameter: 93 body: 71
67	Lambda	parameter: 93 body: 72
68	Lambda	parameter: 93 body: 74
69	Operation	operator: 75 operands: 96
70	Literal
71	Operation	operator: 79 operands: 76
72	Operation	operator: 77 operands: 78
73	ExprTuple	93
74	Operation	operator: 79 operands: 80
75	Literal
76	NamedExprs	element: 81 targets: 84
77	Literal
78	NamedExprs	basis: 82
79	Literal
80	NamedExprs	element: 83 targets: 84
81	Operation	operator: 85 operands: 86
82	Literal
83	Operation	operator: 87 operands: 88
84	Operation	operator: 89 operands: 90
85	Literal
86	NamedExprs	state: 91 part: 93
87	Literal
88	NamedExprs	state: 92 part: 93
89	Literal
90	ExprTuple	94, 98
91	Variable
92	Operation	operator: 95 operands: 96
93	Variable
94	Literal
95	Literal
96	ExprTuple	97, 98
97	Variable
98	Variable

Expression of type Conditional¶

from the theory of proveit.physics.quantum.circuits¶

Expression of type Conditional ¶

from the theory of proveit.physics.quantum.circuits ¶