Expression of type ExprTuple

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, ExprTuple, 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 And, CartExp, Equals, Exists, Forall, InSet, Set
from proveit.numbers import Complex, Interval, Min, NaturalPos, 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 = ExprTuple(Lambda([m, n], Conditional(Forall(instance_param_or_params = [var_ket_psi], instance_expr = 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(), domain = TensorProd(sub_expr4, sub_expr3)).with_wrapping(), And(InSet(m, NaturalPos), 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())

\left(\left(m, n\right) \mapsto \left\{\begin{array}{l}\forall_{\lvert \psi \rangle \in \mathbb{C}^{m} {\otimes} \mathbb{C}^{n}}~\\
\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}\right]\end{array} \textrm{ if } m \in \mathbb{N}^+ ,  n \in \mathbb{N}^+\right..\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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