Expression of type Lambda

from the theory of proveit.physics.quantum.algebra

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 A, B, Conditional, Lambda, i, n
from proveit.core_expr_types import a_1_to_n, a_i, b_1_to_n, b_i, v_1_to_n, v_i
from proveit.linear_algebra import Adj, Commutator, Dim, HilbertSpaces, Hspace, LinMap, OrthoNormBases, ScalarMult, VecSum, VecZero
from proveit.logic import And, Equals, Exists, Forall, Iff, InSet, Set
from proveit.numbers import Complex, Interval, NaturalPos, one
from proveit.physics.quantum import Bra, Ket, Qmult

# build up the expression from sub-expressions
sub_expr1 = [i]
sub_expr2 = LinMap(Hspace, Hspace)
sub_expr3 = Interval(one, n)
sub_expr4 = Qmult(Ket(v_i), Bra(v_i))
expr = Lambda(n, Conditional(Forall(instance_param_or_params = [Hspace], instance_expr = Forall(instance_param_or_params = [A, B], instance_expr = Iff(Equals(Commutator(A, B), VecZero(sub_expr2)), Exists(instance_param_or_params = [v_1_to_n], instance_expr = Exists(instance_param_or_params = [a_1_to_n, b_1_to_n], instance_expr = And(Equals(A, VecSum(index_or_indices = sub_expr1, summand = ScalarMult(a_i, sub_expr4), domain = sub_expr3)), Equals(B, VecSum(index_or_indices = sub_expr1, summand = ScalarMult(b_i, sub_expr4), domain = sub_expr3))).with_wrapping_at(2), domain = Complex).with_wrapping(), condition = InSet(Set(v_1_to_n), OrthoNormBases(Hspace))).with_wrapping()).with_wrapping_at(2), domain = sub_expr2, conditions = [Equals(Adj(A), A), Equals(Adj(B), B)]).with_wrapping(), domain = HilbertSpaces, condition = Equals(Dim(Hspace), n)).with_wrapping(), InSet(n, 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())

n \mapsto \left\{\begin{array}{l}\forall_{\mathcal{H} \underset{{\scriptscriptstyle c}}{\in} \textrm{HilbertSpaces}~|~\textrm{Dim}\left(\mathcal{H}\right) = n}~\\
\left[\begin{array}{l}\forall_{A, B \in \mathcal{L}\left(\mathcal{H}, \mathcal{H}\right)~|~A^{\dagger} = A, B^{\dagger} = B}~\\
\left(\begin{array}{c} \begin{array}{l} \left(\left[A, B\right] = \vec{0}\left(\mathcal{L}\left(\mathcal{H}, \mathcal{H}\right)\right)\right) \Leftrightarrow  \\ \left[\begin{array}{l}\exists_{v_{1}, v_{2}, \ldots, v_{n}~|~\left\{v_{1}, v_{2}, \ldots, v_{n}\right\} \in \textrm{O.N.Bases}\left(\mathcal{H}\right)}~\\
\left[\begin{array}{l}\exists_{a_{1}, a_{2}, \ldots, a_{n}, b_{1}, b_{2}, \ldots, b_{n} \in \mathbb{C}}~\\
\left(\begin{array}{c} \left(A = \left(\sum_{i=1}^{n} \left(a_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right) \land  \\ \left(B = \left(\sum_{i=1}^{n} \left(b_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right) \end{array}\right)\end{array}\right]\end{array}\right] \end{array} \end{array}\right)\end{array}\right]\end{array} \textrm{ if } n \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: 135 body: 2
1	ExprTuple	135
2	Conditional	value: 3 condition: 4
3	Operation	operator: 12 operand: 7
4	Operation	operator: 120 operands: 6
5	ExprTuple	7
6	ExprTuple	135, 8
7	Lambda	parameter: 77 body: 9
8	Literal
9	Conditional	value: 10 condition: 11
10	Operation	operator: 12 operand: 15
11	Operation	operator: 81 operands: 14
12	Literal
13	ExprTuple	15
14	ExprTuple	16, 17
15	Lambda	parameters: 48 body: 18
16	Operation	operator: 19 operands: 20
17	Operation	operator: 90 operands: 21
18	Conditional	value: 22 condition: 23
19	Literal
20	ExprTuple	77, 24
21	ExprTuple	25, 135
22	Operation	operator: 26 operands: 27
23	Operation	operator: 81 operands: 28
24	Literal
25	Operation	operator: 29 operand: 77
26	Literal
27	ExprTuple	30, 31
28	ExprTuple	32, 33, 34, 35
29	Literal
30	Operation	operator: 90 operands: 36
31	Operation	operator: 60 operand: 44
32	Operation	operator: 120 operands: 38
33	Operation	operator: 120 operands: 39
34	Operation	operator: 90 operands: 40
35	Operation	operator: 90 operands: 41
36	ExprTuple	42, 43
37	ExprTuple	44
38	ExprTuple	94, 55
39	ExprTuple	96, 55
40	ExprTuple	45, 94
41	ExprTuple	46, 96
42	Operation	operator: 47 operands: 48
43	Operation	operator: 49 operand: 55
44	Lambda	parameters: 69 body: 51
45	Operation	operator: 53 operand: 94
46	Operation	operator: 53 operand: 96
47	Literal
48	ExprTuple	94, 96
49	Literal
50	ExprTuple	55
51	Conditional	value: 56 condition: 57
52	ExprTuple	94
53	Literal
54	ExprTuple	96
55	Operation	operator: 58 operands: 59
56	Operation	operator: 60 operand: 63
57	Operation	operator: 120 operands: 62
58	Literal
59	ExprTuple	77, 77
60	Literal
61	ExprTuple	63
62	ExprTuple	64, 65
63	Lambda	parameters: 66 body: 67
64	Operation	operator: 68 operands: 69
65	Operation	operator: 70 operand: 77
66	ExprTuple	72, 73
67	Conditional	value: 74 condition: 75
68	Literal
69	ExprTuple	76
70	Literal
71	ExprTuple	77
72	ExprRange	lambda_map: 78 start_index: 134 end_index: 135
73	ExprRange	lambda_map: 79 start_index: 134 end_index: 135
74	Operation	operator: 81 operands: 80
75	Operation	operator: 81 operands: 82
76	ExprRange	lambda_map: 83 start_index: 134 end_index: 135
77	Variable
78	Lambda	parameter: 116 body: 107
79	Lambda	parameter: 116 body: 108
80	ExprTuple	84, 85
81	Literal
82	ExprTuple	86, 87
83	Lambda	parameter: 116 body: 88
84	Operation	operator: 90 operands: 89
85	Operation	operator: 90 operands: 91
86	ExprRange	lambda_map: 92 start_index: 134 end_index: 135
87	ExprRange	lambda_map: 93 start_index: 134 end_index: 135
88	IndexedVar	variable: 140 index: 116
89	ExprTuple	94, 95
90	Literal
91	ExprTuple	96, 97
92	Lambda	parameter: 116 body: 98
93	Lambda	parameter: 116 body: 99
94	Variable
95	Operation	operator: 101 operand: 105
96	Variable
97	Operation	operator: 101 operand: 106
98	Operation	operator: 120 operands: 103
99	Operation	operator: 120 operands: 104
100	ExprTuple	105
101	Literal
102	ExprTuple	106
103	ExprTuple	107, 109
104	ExprTuple	108, 109
105	Lambda	parameter: 142 body: 110
106	Lambda	parameter: 142 body: 111
107	IndexedVar	variable: 126 index: 116
108	IndexedVar	variable: 127 index: 116
109	Literal
110	Conditional	value: 113 condition: 115
111	Conditional	value: 114 condition: 115
112	ExprTuple	116
113	Operation	operator: 118 operands: 117
114	Operation	operator: 118 operands: 119
115	Operation	operator: 120 operands: 121
116	Variable
117	ExprTuple	122, 124
118	Literal
119	ExprTuple	123, 124
120	Literal
121	ExprTuple	142, 125
122	IndexedVar	variable: 126 index: 142
123	IndexedVar	variable: 127 index: 142
124	Operation	operator: 128 operands: 129
125	Operation	operator: 130 operands: 131
126	Variable
127	Variable
128	Literal
129	ExprTuple	132, 133
130	Literal
131	ExprTuple	134, 135
132	Operation	operator: 136 operand: 139
133	Operation	operator: 137 operand: 139
134	Literal
135	Variable
136	Literal
137	Literal
138	ExprTuple	139
139	IndexedVar	variable: 140 index: 142
140	Variable
141	ExprTuple	142
142	Variable