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

# build up the expression from sub-expressions
sub_expr1 = Adj(M)
expr = Lambda(Hspace, Conditional(Forall(instance_param_or_params = [M], instance_expr = Iff(Equals(Qmult(sub_expr1, M), Qmult(M, sub_expr1)), Exists(instance_param_or_params = [v_1_to_n], instance_expr = Exists(instance_param_or_params = [a_1_to_n], instance_expr = Equals(M, VecSum(index_or_indices = [i], summand = ScalarMult(a_i, Qmult(Ket(v_i), Bra(v_i))), domain = Interval(one, n))), domain = Complex).with_wrapping(), condition = InSet(Set(v_1_to_n_kets), OrthoNormBases(Hspace))).with_wrapping()).with_wrapping_at(2), domain = LinMap(Hspace, Hspace)), And(InClass(Hspace, HilbertSpaces), Equals(Dim(Hspace), n))))

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

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