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 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 = 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(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..

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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