Expression of type Conditional

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 Conditional, Function, f, 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 Dim, HilbertSpaces, Hspace, OrthoNormBases, ScalarMult, VecSum
from proveit.logic import Equals, Forall, Functions, 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 = [i]
sub_expr2 = Interval(one, n)
sub_expr3 = Qmult(Ket(v_i), Bra(v_i))
expr = Conditional(Forall(instance_param_or_params = [Hspace], instance_expr = Forall(instance_param_or_params = [v_1_to_n], instance_expr = Forall(instance_param_or_params = [a_1_to_n], instance_expr = Forall(instance_param_or_params = [f], instance_expr = Equals(Function(f, [VecSum(index_or_indices = sub_expr1, summand = ScalarMult(a_i, sub_expr3), domain = sub_expr2)]), VecSum(index_or_indices = sub_expr1, summand = ScalarMult(Function(f, [a_i]), sub_expr3), domain = sub_expr2)), domain = Functions(Complex, Complex)), domain = Complex), condition = InSet(Set(v_1_to_n_kets), OrthoNormBases(Hspace))).with_wrapping(), domain = HilbertSpaces, condition = Equals(Dim(Hspace), n)).with_wrapping(), InSet(n, NaturalPos))

expr:

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

\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_{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[\forall_{a_{1}, a_{2}, \ldots, a_{n} \in \mathbb{C}}~\left[\forall_{f \in \left[\mathbb{C} \rightarrow \mathbb{C}\right]}~\left(f\left(\sum_{i=1}^{n} \left(a_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right) = \left(\sum_{i=1}^{n} \left(f\left(a_{i}\right) \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right)\right]\right]\end{array}\right]\end{array} \textrm{ if } n \in \mathbb{N}^+\right..

stored_expr.style_options()

name	description	default	current value	related methods
condition_delimiter	'comma' or 'and'	comma	comma	('with_comma_delimiter', 'with_conjunction_delimiter')

# display the expression information
stored_expr.expr_info()

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