Expression of type Forall ¶

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 m, n
from proveit.logic import Equals, Forall
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 = Forall(instance_param_or_params = [m], instance_expr = 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), domain = 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())

\forall_{m \in \mathbb{N}^+}~\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]\right]

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	None/False	('with_wrapping',)
condition_wrapping	Wrap 'before' or 'after' the condition (or None).	None	None/False	('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_params	If 'True', wraps every two parameters AND wraps the Expression after the parameters	None	None/False	('with_params',)
justification	justify to the 'left', 'center', or 'right' in the array cells	center	center	('with_justification',)

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

Expression of type Forall¶

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

Expression of type Forall ¶

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