Expression of type Conditional

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, 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 = 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\{\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()

name	description	default	current value	related methods
condition_delimiter	'comma' or 'and'	comma	comma	('with_comma_delimiter', 'with_conjunction_delimiter')

# display the expression information
stored_expr.expr_info()

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