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 A, V, W, i, j, m, n
from proveit.core_expr_types import v_1_to_m, v_i, w_1_to_n, w_j
from proveit.linear_algebra import LinMap, OrthoNormBases, VecSum
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import Interval, NaturalPos, one
from proveit.physics.quantum import Bra, Ket, Qmult
from proveit.physics.quantum.algebra import v_1_to_m_kets, w_1_to_n_kets

# build up the expression from sub-expressions
expr = Forall(instance_param_or_params = [A], instance_expr = Forall(instance_param_or_params = [m, n], instance_expr = Forall(instance_param_or_params = [v_1_to_m], instance_expr = Forall(instance_param_or_params = [w_1_to_n], instance_expr = Equals(A, VecSum(index_or_indices = [i], summand = VecSum(index_or_indices = [j], summand = Qmult(Bra(w_j), A, Ket(v_i), Ket(w_j), Bra(v_i)), domain = Interval(one, n)), domain = Interval(one, m))), condition = InSet(w_1_to_n_kets, OrthoNormBases(W))).with_wrapping(), condition = InSet(v_1_to_m_kets, OrthoNormBases(V))).with_wrapping(), domain = NaturalPos), domain = LinMap(V, W))

# 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_{A \in \mathcal{L}\left(V, W\right)}~\left[\forall_{m, n \in \mathbb{N}^+}~\left[\begin{array}{l}\forall_{v_{1}, v_{2}, \ldots, v_{m}~|~\left\{\lvert v_{1} \rangle, \lvert v_{2} \rangle, \ldots, \lvert v_{m} \rangle\right\} \in \textrm{O.N.Bases}\left(V\right)}~\\
\left[\begin{array}{l}\forall_{w_{1}, w_{2}, \ldots, w_{n}~|~\left\{\lvert w_{1} \rangle, \lvert w_{2} \rangle, \ldots, \lvert w_{n} \rangle\right\} \in \textrm{O.N.Bases}\left(W\right)}~\\
\left(A = \left(\sum_{i=1}^{m} \left(\sum_{j=1}^{n} \left(\langle w_{j} \rvert \thinspace A \thinspace \lvert v_{i} \rangle \thinspace \lvert w_{j} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right)\end{array}\right]\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: 32 operand: 2
1	ExprTuple	2
2	Lambda	parameter: 90 body: 4
3	ExprTuple	90
4	Conditional	value: 5 condition: 6
5	Operation	operator: 32 operand: 9
6	Operation	operator: 87 operands: 8
7	ExprTuple	9
8	ExprTuple	90, 10
9	Lambda	parameters: 11 body: 12
10	Operation	operator: 13 operands: 14
11	ExprTuple	83, 104
12	Conditional	value: 15 condition: 16
13	Literal
14	ExprTuple	46, 64
15	Operation	operator: 32 operand: 20
16	Operation	operator: 18 operands: 19
17	ExprTuple	20
18	Literal
19	ExprTuple	21, 22
20	Lambda	parameters: 23 body: 24
21	Operation	operator: 87 operands: 25
22	Operation	operator: 87 operands: 26
23	ExprTuple	27
24	Conditional	value: 28 condition: 29
25	ExprTuple	83, 30
26	ExprTuple	104, 30
27	ExprRange	lambda_map: 31 start_index: 103 end_index: 83
28	Operation	operator: 32 operand: 35
29	Operation	operator: 87 operands: 34
30	Literal
31	Lambda	parameter: 84 body: 65
32	Literal
33	ExprTuple	35
34	ExprTuple	36, 37
35	Lambda	parameters: 38 body: 39
36	Operation	operator: 57 operands: 40
37	Operation	operator: 59 operand: 46
38	ExprTuple	42
39	Conditional	value: 43 condition: 44
40	ExprTuple	45
41	ExprTuple	46
42	ExprRange	lambda_map: 47 start_index: 103 end_index: 104
43	Operation	operator: 48 operands: 49
44	Operation	operator: 87 operands: 50
45	ExprRange	lambda_map: 51 start_index: 103 end_index: 83
46	Variable
47	Lambda	parameter: 84 body: 77
48	Literal
49	ExprTuple	90, 52
50	ExprTuple	53, 54
51	Lambda	parameter: 84 body: 55
52	Operation	operator: 71 operand: 62
53	Operation	operator: 57 operands: 58
54	Operation	operator: 59 operand: 64
55	Operation	operator: 95 operand: 65
56	ExprTuple	62
57	Literal
58	ExprTuple	63
59	Literal
60	ExprTuple	64
61	ExprTuple	65
62	Lambda	parameter: 110 body: 66
63	ExprRange	lambda_map: 67 start_index: 103 end_index: 104
64	Variable
65	IndexedVar	variable: 107 index: 84
66	Conditional	value: 68 condition: 69
67	Lambda	parameter: 84 body: 70
68	Operation	operator: 71 operand: 75
69	Operation	operator: 87 operands: 73
70	Operation	operator: 95 operand: 77
71	Literal
72	ExprTuple	75
73	ExprTuple	110, 76
74	ExprTuple	77
75	Lambda	parameter: 109 body: 78
76	Operation	operator: 99 operands: 79
77	IndexedVar	variable: 105 index: 84
78	Conditional	value: 81 condition: 82
79	ExprTuple	103, 83
80	ExprTuple	84
81	Operation	operator: 85 operands: 86
82	Operation	operator: 87 operands: 88
83	Variable
84	Variable
85	Literal
86	ExprTuple	89, 90, 91, 92, 93
87	Literal
88	ExprTuple	109, 94
89	Operation	operator: 97 operand: 101
90	Variable
91	Operation	operator: 95 operand: 102
92	Operation	operator: 95 operand: 101
93	Operation	operator: 97 operand: 102
94	Operation	operator: 99 operands: 100
95	Literal
96	ExprTuple	101
97	Literal
98	ExprTuple	102
99	Literal
100	ExprTuple	103, 104
101	IndexedVar	variable: 105 index: 109
102	IndexedVar	variable: 107 index: 110
103	Literal
104	Variable
105	Variable
106	ExprTuple	109
107	Variable
108	ExprTuple	110
109	Variable
110	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 ¶