Expression of type Lambda

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, Lambda, 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 = Lambda(m, 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)))

expr:

# 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())

m \mapsto \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()

no style options

# display the expression information
stored_expr.expr_info()

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