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, MatrixSpace, OrthoNormBases, ScalarMult, VecSum
from proveit.logic import CartExp, Equals, Exists, Forall, Iff, InSet, Set
from proveit.numbers import Complex, Interval, NaturalPos, 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 = [n], 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(CartExp(Complex, n)))).with_wrapping()).with_wrapping_at(2), domain = MatrixSpace(field = Complex, rows = n, columns = n)), domain = NaturalPos)

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

\forall_{n \in \mathbb{N}^+}~\left[\forall_{M \in \mathbb{C}^{n \times n}}~\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(\mathbb{C}^{n}\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]

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