Theorem simultaneous_diagonalization_as_outer_prods of type Forall ¶

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

import proveit
# Automation is not needed when only building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_theorem_expr # Load the stored theorem expression as 'stored_expr'
# import the special expression
from proveit.physics.quantum.algebra import simultaneous_diagonalization_as_outer_prods

# check that the built expression is the same as the stored expression
assert simultaneous_diagonalization_as_outer_prods.expr == stored_expr
assert simultaneous_diagonalization_as_outer_prods.expr._style_id == stored_expr._style_id
print("Passed sanity check: simultaneous_diagonalization_as_outer_prods matches stored_expr")

Passed sanity check: simultaneous_diagonalization_as_outer_prods matches stored_expr

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\forall_{n \in \mathbb{N}^+}~\left[\begin{array}{l}\forall_{\mathcal{H} \underset{{\scriptscriptstyle c}}{\in} \textrm{HilbertSpaces}~|~\textrm{Dim}\left(\mathcal{H}\right) = n}~\\
\left[\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_{v_{1}, v_{2}, \ldots, v_{n}~|~\left\{v_{1}, v_{2}, \ldots, v_{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 \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right) \land  \\ \left(B = \left(\sum_{i=1}^{n} \left(b_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right) \end{array}\right)\end{array}\right]\end{array}\right] \end{array} \end{array}\right)\end{array}\right]\end{array}\right]

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

Theorem simultaneous_diagonalization_as_outer_prods of type Forall¶

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

Theorem simultaneous_diagonalization_as_outer_prods of type Forall ¶

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