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, ExprRange, IndexedVar, Lambda, Variable, i, lambda_, m, n
from proveit.core_expr_types import a_1_to_m, a_i, b_1_to_n, b_i, lambda_i
from proveit.linear_algebra import OrthoNormBases, ScalarMult, TensorProd, VecSum
from proveit.logic import CartExp, Equals, Exists, InSet, Set
from proveit.numbers import Complex, Interval, Min, RealNonNeg, one
from proveit.physics.quantum import Ket, Qmult, var_ket_psi
from proveit.physics.quantum.algebra import a_1_to_m_kets, b_1_to_n_kets

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = Min(m, n)
sub_expr3 = CartExp(Complex, n)
sub_expr4 = CartExp(Complex, m)
expr = Lambda(var_ket_psi, Conditional(Exists(instance_param_or_params = [a_1_to_m], instance_expr = Exists(instance_param_or_params = [b_1_to_n], instance_expr = Exists(instance_param_or_params = [ExprRange(sub_expr1, IndexedVar(lambda_, sub_expr1), one, sub_expr2)], instance_expr = Equals(var_ket_psi, VecSum(index_or_indices = [i], summand = ScalarMult(lambda_i, Qmult(Ket(a_i), Ket(b_i))), domain = Interval(one, sub_expr2))), domain = RealNonNeg).with_wrapping(), condition = InSet(Set(b_1_to_n_kets), OrthoNormBases(sub_expr3))).with_wrapping(), condition = InSet(Set(a_1_to_m_kets), OrthoNormBases(sub_expr4))).with_wrapping(), InSet(var_ket_psi, TensorProd(sub_expr4, sub_expr3))))

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

\lvert \psi \rangle \mapsto \left\{\begin{array}{l}\exists_{a_{1}, a_{2}, \ldots, a_{m}~|~\left\{\left\{\lvert a_{1} \rangle, \lvert a_{2} \rangle, \ldots, \lvert a_{m} \rangle\right\}\right\} \in \textrm{O.N.Bases}\left(\mathbb{C}^{m}\right)}~\\
\left[\begin{array}{l}\exists_{b_{1}, b_{2}, \ldots, b_{n}~|~\left\{\left\{\lvert b_{1} \rangle, \lvert b_{2} \rangle, \ldots, \lvert b_{n} \rangle\right\}\right\} \in \textrm{O.N.Bases}\left(\mathbb{C}^{n}\right)}~\\
\left[\begin{array}{l}\exists_{\lambda_{1}, \lambda_{2}, \ldots, \lambda_{{\rm Min}\left(m, n\right)} \in \mathbb{R}^{\ge 0}}~\\
\left(\lvert \psi \rangle = \left(\sum_{i=1}^{{\rm Min}\left(m, n\right)} \left(\lambda_{i} \cdot \left(\lvert a_{i} \rangle \thinspace \lvert b_{i} \rangle\right)\right)\right)\right)\end{array}\right]\end{array}\right]\end{array} \textrm{ if } \lvert \psi \rangle \in \left(\mathbb{C}^{m} {\otimes} \mathbb{C}^{n}\right)\right..

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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