# from the theory of proveit.linear_algebra.inner_products¶

In [1]:
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.
# import Expression classes needed to build the expression
from proveit import Conditional, Lambda, P, Px, Py, X, x, y
from proveit.linear_algebra import HilbertSpaces, Hspace, InnerProd, LinMap, OrthoProj, VecZero
from proveit.logic import And, Equals, Forall, Iff, Implies, InClass, SubsetEq
from proveit.numbers import zero

In [2]:
# build up the expression from sub-expressions
sub_expr1 = [x]
expr = Lambda([Hspace, X], Conditional(Forall(instance_param_or_params = [P], instance_expr = Iff(Equals(P, OrthoProj(Hspace, X)), And(Forall(instance_param_or_params = sub_expr1, instance_expr = Equals(Px, x), domain = X), Forall(instance_param_or_params = [y], instance_expr = Implies(Forall(instance_param_or_params = sub_expr1, instance_expr = Equals(InnerProd(x, y), zero), domain = X), Equals(Py, VecZero(Hspace))), domain = Hspace)).with_wrapping_at(2)).with_wrapping_at(2), domain = LinMap(Hspace, Hspace)), And(InClass(Hspace, HilbertSpaces), InClass(X, HilbertSpaces), SubsetEq(X, Hspace))))

expr:
In [3]:
# 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

In [4]:
# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\left(\mathcal{H}, X\right) \mapsto \left\{\forall_{P \in \mathcal{L}\left(\mathcal{H}, \mathcal{H}\right)}~\left(\begin{array}{c} \begin{array}{l} \left(P = \textrm{OrthoProj}\left(\mathcal{H}, X\right)\right) \Leftrightarrow  \\ \left(\begin{array}{c} \left[\forall_{x \in X}~\left(P\left(x\right) = x\right)\right] \land  \\ \left[\forall_{y \in \mathcal{H}}~\left(\left[\forall_{x \in X}~\left(\left \langle x, y\right \rangle = 0\right)\right] \Rightarrow \left(P\left(y\right) = \vec{0}\left(\mathcal{H}\right)\right)\right)\right] \end{array}\right) \end{array} \end{array}\right) \textrm{ if } \mathcal{H} \underset{{\scriptscriptstyle c}}{\in} \textrm{HilbertSpaces} ,  X \underset{{\scriptscriptstyle c}}{\in} \textrm{HilbertSpaces} ,  X \subseteq \mathcal{H}\right..

In [5]:
stored_expr.style_options()

no style options
In [6]:
# display the expression information
stored_expr.expr_info()

core typesub-expressionsexpression
0Lambdaparameters: 35
body: 1
1Conditionalvalue: 2
condition: 3
2Operationoperator: 52
operand: 6
3Operationoperator: 27
operands: 5
4ExprTuple6
5ExprTuple7, 8, 9
6Lambdaparameter: 60
body: 11
7Operationoperator: 13
operands: 12
8Operationoperator: 13
operands: 14
9Operationoperator: 15
operands: 16
10ExprTuple60
11Conditionalvalue: 17
condition: 18
12ExprTuple66, 19
13Literal
14ExprTuple73, 19
15Literal
16ExprTuple73, 66
17Operationoperator: 20
operands: 21
18Operationoperator: 69
operands: 22
19Literal
20Literal
21ExprTuple23, 24
22ExprTuple60, 25
23Operationoperator: 67
operands: 26
24Operationoperator: 27
operands: 28
25Operationoperator: 29
operands: 30
26ExprTuple60, 31
27Literal
28ExprTuple32, 33
29Literal
30ExprTuple66, 66
31Operationoperator: 34
operands: 35
32Operationoperator: 52
operand: 38
33Operationoperator: 52
operand: 39
34Literal
35ExprTuple66, 73
36ExprTuple38
37ExprTuple39
38Lambdaparameter: 76
body: 40
39Lambdaparameter: 77
body: 41
40Conditionalvalue: 42
condition: 65
41Conditionalvalue: 43
condition: 44
42Operationoperator: 67
operands: 45
43Operationoperator: 46
operands: 47
44Operationoperator: 69
operands: 48
45ExprTuple49, 76
46Literal
47ExprTuple50, 51
48ExprTuple77, 66
49Operationoperator: 60
operand: 76
50Operationoperator: 52
operand: 55
51Operationoperator: 67
operands: 54
52Literal
53ExprTuple55
54ExprTuple56, 57
55Lambdaparameter: 76
body: 59
56Operationoperator: 60
operand: 77
57Operationoperator: 62
operand: 66
58ExprTuple76
59Conditionalvalue: 64
condition: 65
60Variable
61ExprTuple77
62Literal
63ExprTuple66
64Operationoperator: 67
operands: 68
65Operationoperator: 69
operands: 70
66Variable
67Literal
68ExprTuple71, 72
69Literal
70ExprTuple76, 73
71Operationoperator: 74
operands: 75
72Literal
73Variable
74Literal
75ExprTuple76, 77
76Variable
77Variable