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

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