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 M, i, n
from proveit.core_expr_types import a_1_to_n, a_i, v_1_to_n, v_i
from proveit.linear_algebra import Adj, Dim, HilbertSpaces, Hspace, LinMap, OrthoNormBases, ScalarMult, VecSum
from proveit.logic import Equals, Exists, Forall, Iff, InSet, Set
from proveit.numbers import Complex, Interval, one
from proveit.physics.quantum import Bra, Ket, Qmult
from proveit.physics.quantum.algebra import v_1_to_n_kets

# build up the expression from sub-expressions
sub_expr1 = Adj(M)
expr = Forall(instance_param_or_params = [Hspace], instance_expr = Forall(instance_param_or_params = [M], instance_expr = Iff(Equals(Qmult(sub_expr1, M), Qmult(M, sub_expr1)), Exists(instance_param_or_params = [v_1_to_n], instance_expr = Exists(instance_param_or_params = [a_1_to_n], instance_expr = Equals(M, VecSum(index_or_indices = [i], summand = ScalarMult(a_i, Qmult(Ket(v_i), Bra(v_i))), domain = Interval(one, n))), domain = Complex).with_wrapping(), condition = InSet(Set(v_1_to_n_kets), OrthoNormBases(Hspace))).with_wrapping()).with_wrapping_at(2), domain = LinMap(Hspace, Hspace)), domain = HilbertSpaces, condition = Equals(Dim(Hspace), n)).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_{\mathcal{H} \underset{{\scriptscriptstyle c}}{\in} \textrm{HilbertSpaces}~|~\textrm{Dim}\left(\mathcal{H}\right) = n}~\\
\left[\forall_{M \in \mathcal{L}\left(\mathcal{H}, \mathcal{H}\right)}~\left(\begin{array}{c} \begin{array}{l} \left(\left(M^{\dagger} \thinspace M\right) = \left(M \thinspace M^{\dagger}\right)\right) \Leftrightarrow  \\ \left[\begin{array}{l}\exists_{v_{1}, v_{2}, \ldots, v_{n}~|~\left\{\left\{\lvert v_{1} \rangle, \lvert v_{2} \rangle, \ldots, \lvert v_{n} \rangle\right\}\right\} \in \textrm{O.N.Bases}\left(\mathcal{H}\right)}~\\
\left[\begin{array}{l}\exists_{a_{1}, a_{2}, \ldots, a_{n} \in \mathbb{C}}~\\
\left(M = \left(\sum_{i=1}^{n} \left(a_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right)\end{array}\right]\end{array}\right] \end{array} \end{array}\right)\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: 6 operand: 2
1	ExprTuple	2
2	Lambda	parameter: 60 body: 3
3	Conditional	value: 4 condition: 5
4	Operation	operator: 6 operand: 9
5	Operation	operator: 64 operands: 8
6	Literal
7	ExprTuple	9
8	ExprTuple	10, 11
9	Lambda	parameter: 68 body: 12
10	Operation	operator: 13 operands: 14
11	Operation	operator: 62 operands: 15
12	Conditional	value: 16 condition: 17
13	Literal
14	ExprTuple	60, 18
15	ExprTuple	19, 104
16	Operation	operator: 20 operands: 21
17	Operation	operator: 89 operands: 22
18	Literal
19	Operation	operator: 23 operand: 60
20	Literal
21	ExprTuple	24, 25
22	ExprTuple	68, 26
23	Literal
24	Operation	operator: 62 operands: 27
25	Operation	operator: 45 operand: 33
26	Operation	operator: 29 operands: 30
27	ExprTuple	31, 32
28	ExprTuple	33
29	Literal
30	ExprTuple	60, 60
31	Operation	operator: 97 operands: 34
32	Operation	operator: 97 operands: 35
33	Lambda	parameters: 36 body: 37
34	ExprTuple	38, 68
35	ExprTuple	68, 38
36	ExprTuple	39
37	Conditional	value: 40 condition: 41
38	Operation	operator: 42 operand: 68
39	ExprRange	lambda_map: 44 start_index: 103 end_index: 104
40	Operation	operator: 45 operand: 48
41	Operation	operator: 89 operands: 47
42	Literal
43	ExprTuple	68
44	Lambda	parameter: 95 body: 86
45	Literal
46	ExprTuple	48
47	ExprTuple	49, 50
48	Lambda	parameters: 51 body: 52
49	Operation	operator: 66 operand: 59
50	Operation	operator: 54 operand: 60
51	ExprTuple	56
52	Conditional	value: 57 condition: 58
53	ExprTuple	59
54	Literal
55	ExprTuple	60
56	ExprRange	lambda_map: 61 start_index: 103 end_index: 104
57	Operation	operator: 62 operands: 63
58	Operation	operator: 64 operands: 65
59	Operation	operator: 66 operands: 67
60	Variable
61	Lambda	parameter: 95 body: 84
62	Literal
63	ExprTuple	68, 69
64	Literal
65	ExprTuple	70
66	Literal
67	ExprTuple	71
68	Variable
69	Operation	operator: 72 operand: 76
70	ExprRange	lambda_map: 74 start_index: 103 end_index: 104
71	ExprRange	lambda_map: 75 start_index: 103 end_index: 104
72	Literal
73	ExprTuple	76
74	Lambda	parameter: 95 body: 77
75	Lambda	parameter: 95 body: 78
76	Lambda	parameter: 111 body: 79
77	Operation	operator: 89 operands: 80
78	Operation	operator: 105 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: 109 index: 95
87	Literal
88	ExprTuple	92, 93
89	Literal
90	ExprTuple	111, 94
91	ExprTuple	95
92	IndexedVar	variable: 96 index: 111
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: 105 operand: 108
102	Operation	operator: 106 operand: 108
103	Literal
104	Variable
105	Literal
106	Literal
107	ExprTuple	108
108	IndexedVar	variable: 109 index: 111
109	Variable
110	ExprTuple	111
111	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 ¶