Expression of type Forall ¶

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

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

\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}

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	True	('with_wrapping',)
condition_wrapping	Wrap 'before' or 'after' the condition (or None).	None	None/False	('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_params	If 'True', wraps every two parameters AND wraps the Expression after the parameters	None	None/False	('with_params',)
justification	justify to the 'left', 'center', or 'right' in the array cells	center	center	('with_justification',)

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

Expression of type Forall¶

from the theory of proveit.physics.quantum.algebra¶

Expression of type Forall ¶

from the theory of proveit.physics.quantum.algebra ¶