Expression of type Forall ¶

from the theory of proveit.linear_algebra.inner_products ¶

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 A, B, i, n
from proveit.core_expr_types import a_1_to_n, a_i, b_1_to_n, b_i, x_1_to_n, x_i
from proveit.linear_algebra import Adj, Commutator, Hspace, LinMap, OrthoNormBases, OrthoProj, ScalarMult, Span, VecSum, VecZero
from proveit.logic import And, Equals, Exists, Forall, Iff, InSet, Set
from proveit.numbers import Complex, Interval, one

# build up the expression from sub-expressions
sub_expr1 = [i]
sub_expr2 = LinMap(Hspace, Hspace)
sub_expr3 = Interval(one, n)
sub_expr4 = OrthoProj(Hspace, Span(Set(x_i)))
expr = Forall(instance_param_or_params = [A, B], instance_expr = Iff(Equals(Commutator(A, B), VecZero(sub_expr2)), Exists(instance_param_or_params = [x_1_to_n], instance_expr = Exists(instance_param_or_params = [a_1_to_n, b_1_to_n], instance_expr = And(Equals(A, VecSum(index_or_indices = sub_expr1, summand = ScalarMult(a_i, sub_expr4), domain = sub_expr3)), Equals(B, VecSum(index_or_indices = sub_expr1, summand = ScalarMult(b_i, sub_expr4), domain = sub_expr3))).with_wrapping_at(2), domain = Complex).with_wrapping(), condition = InSet(Set(x_1_to_n), OrthoNormBases(Hspace))).with_wrapping()).with_wrapping_at(2), domain = sub_expr2, conditions = [Equals(Adj(A), A), Equals(Adj(B), B)]).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_{A, B \in \mathcal{L}\left(\mathcal{H}, \mathcal{H}\right)~|~A^{\dagger} = A, B^{\dagger} = B}~\\
\left(\begin{array}{c} \begin{array}{l} \left(\left[A, B\right] = \vec{0}\left(\mathcal{L}\left(\mathcal{H}, \mathcal{H}\right)\right)\right) \Leftrightarrow  \\ \left[\begin{array}{l}\exists_{x_{1}, x_{2}, \ldots, x_{n}~|~\left\{x_{1}, x_{2}, \ldots, x_{n}\right\} \in \textrm{O.N.Bases}\left(\mathcal{H}\right)}~\\
\left[\begin{array}{l}\exists_{a_{1}, a_{2}, \ldots, a_{n}, b_{1}, b_{2}, \ldots, b_{n} \in \mathbb{C}}~\\
\left(\begin{array}{c} \left(A = \left(\sum_{i=1}^{n} \left(a_{i} \cdot \textrm{OrthoProj}\left(\mathcal{H}, \textrm{Span}\left(\left\{x_{i}\right\}\right)\right)\right)\right)\right) \land  \\ \left(B = \left(\sum_{i=1}^{n} \left(b_{i} \cdot \textrm{OrthoProj}\left(\mathcal{H}, \textrm{Span}\left(\left\{x_{i}\right\}\right)\right)\right)\right)\right) \end{array}\right)\end{array}\right]\end{array}\right] \end{array} \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	parameters: 28 body: 4
4	Conditional	value: 5 condition: 6
5	Operation	operator: 7 operands: 8
6	Operation	operator: 59 operands: 9
7	Literal
8	ExprTuple	10, 11
9	ExprTuple	12, 13, 14, 15
10	Operation	operator: 68 operands: 16
11	Operation	operator: 40 operand: 24
12	Operation	operator: 98 operands: 18
13	Operation	operator: 98 operands: 19
14	Operation	operator: 68 operands: 20
15	Operation	operator: 68 operands: 21
16	ExprTuple	22, 23
17	ExprTuple	24
18	ExprTuple	72, 35
19	ExprTuple	74, 35
20	ExprTuple	25, 72
21	ExprTuple	26, 74
22	Operation	operator: 27 operands: 28
23	Operation	operator: 29 operand: 35
24	Lambda	parameters: 48 body: 31
25	Operation	operator: 33 operand: 72
26	Operation	operator: 33 operand: 74
27	Literal
28	ExprTuple	72, 74
29	Literal
30	ExprTuple	35
31	Conditional	value: 36 condition: 37
32	ExprTuple	72
33	Literal
34	ExprTuple	74
35	Operation	operator: 38 operands: 39
36	Operation	operator: 40 operand: 43
37	Operation	operator: 98 operands: 42
38	Literal
39	ExprTuple	110, 110
40	Literal
41	ExprTuple	43
42	ExprTuple	44, 45
43	Lambda	parameters: 46 body: 47
44	Operation	operator: 117 operands: 48
45	Operation	operator: 49 operand: 110
46	ExprTuple	51, 52
47	Conditional	value: 53 condition: 54
48	ExprTuple	55
49	Literal
50	ExprTuple	110
51	ExprRange	lambda_map: 56 start_index: 112 end_index: 113
52	ExprRange	lambda_map: 57 start_index: 112 end_index: 113
53	Operation	operator: 59 operands: 58
54	Operation	operator: 59 operands: 60
55	ExprRange	lambda_map: 61 start_index: 112 end_index: 113
56	Lambda	parameter: 94 body: 85
57	Lambda	parameter: 94 body: 86
58	ExprTuple	62, 63
59	Literal
60	ExprTuple	64, 65
61	Lambda	parameter: 94 body: 66
62	Operation	operator: 68 operands: 67
63	Operation	operator: 68 operands: 69
64	ExprRange	lambda_map: 70 start_index: 112 end_index: 113
65	ExprRange	lambda_map: 71 start_index: 112 end_index: 113
66	IndexedVar	variable: 120 index: 94
67	ExprTuple	72, 73
68	Literal
69	ExprTuple	74, 75
70	Lambda	parameter: 94 body: 76
71	Lambda	parameter: 94 body: 77
72	Variable
73	Operation	operator: 79 operand: 83
74	Variable
75	Operation	operator: 79 operand: 84
76	Operation	operator: 98 operands: 81
77	Operation	operator: 98 operands: 82
78	ExprTuple	83
79	Literal
80	ExprTuple	84
81	ExprTuple	85, 87
82	ExprTuple	86, 87
83	Lambda	parameter: 122 body: 88
84	Lambda	parameter: 122 body: 89
85	IndexedVar	variable: 104 index: 94
86	IndexedVar	variable: 105 index: 94
87	Literal
88	Conditional	value: 91 condition: 93
89	Conditional	value: 92 condition: 93
90	ExprTuple	94
91	Operation	operator: 96 operands: 95
92	Operation	operator: 96 operands: 97
93	Operation	operator: 98 operands: 99
94	Variable
95	ExprTuple	100, 102
96	Literal
97	ExprTuple	101, 102
98	Literal
99	ExprTuple	122, 103
100	IndexedVar	variable: 104 index: 122
101	IndexedVar	variable: 105 index: 122
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	Variable
111	Operation	operator: 114 operand: 116
112	Literal
113	Variable
114	Literal
115	ExprTuple	116
116	Operation	operator: 117 operand: 119
117	Literal
118	ExprTuple	119
119	IndexedVar	variable: 120 index: 122
120	Variable
121	ExprTuple	122
122	Variable

Expression of type Forall¶

from the theory of proveit.linear_algebra.inner_products¶

Expression of type Forall ¶

from the theory of proveit.linear_algebra.inner_products ¶