# Axioms for the theory of proveit.linear_algebra.inner_products¶

In [1]:
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.

from proveit import n, v, w, x, y, K, H, P, X, Px, Py
from proveit.core_expr_types import x_1_to_n
from proveit.logic import Implies, Iff, And, Forall, Equals, InSet, NotInSet, Set, SubsetEq, InClass
from proveit.numbers import zero, NaturalPos, Complex, sqrt, KroneckerDelta
from proveit.abstract_algebra import Fields
from proveit.linear_algebra import (VecSpaces, LinMap, VecZero, Bases,
InnerProdSpaces, HilbertSpaces, Hspace, InnerProd, Norm, OrthoNormBases, OrthoProj)

In [2]:
%begin axioms

Defining axioms for theory 'proveit.linear_algebra.inner_products'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions


An inner product space is defined as a vector space which also defines an inner product binary operation that always produces a scalar.

In [3]:
inner_prod_space_def = Forall(
(K, H), Equals(
InClass(H, InnerProdSpaces(K)),
And(InClass(H, VecSpaces(K)),
Forall((x, y), InSet(InnerProd(x, y), K)))))

inner_prod_space_def:

A Hilbert space is an inner product space over the complex number field.

In [4]:
hilbert_space_def = Equals(HilbertSpaces, InnerProdSpaces(Complex))

hilbert_space_def:

We define the norm of a vector to be the square root of its inner product with itself.

In [5]:
norm_def = Forall(
K, Forall(H, Forall(x, Equals(Norm(x), sqrt(InnerProd(x, x))),
domain=H),
domain=InnerProdSpaces(K)))

norm_def:

An orthonormal basis is a basis in that is orthonormal meaning that its vectors have a norm of 1 and different vectors are orthogonal.

In [6]:
ortho_norm_bases_def = Forall(K, Forall(
H, Forall(
n, Forall(x_1_to_n,
Equals(InSet(Set(x_1_to_n), OrthoNormBases(H)),
And(InSet(Set(x_1_to_n), Bases(H)),
Forall((v, w), Equals(InnerProd(v, w),
KroneckerDelta(v, w)),
domain=Set(x_1_to_n)))).with_wrap_after_operator(),
domain=H),
domain=NaturalPos),
domain=InnerProdSpaces(K)))

ortho_norm_bases_def:

Define an orthogonal projection onto a subspace:

In [7]:
ortho_proj_def = Forall(
(Hspace, X), Forall(
P,
Iff(Equals(P, OrthoProj(Hspace, X)),
And(Forall(x, Equals(Px, x), domain=X),
Forall(y, Implies(Forall(x, Equals(InnerProd(x, y), zero),
domain=X),
Equals(Py, VecZero(Hspace))),
domain=Hspace)).with_wrap_after_operator())
.with_wrap_after_operator(),
domain=LinMap(Hspace, Hspace)
),
domain=HilbertSpaces, condition=SubsetEq(X, Hspace))

ortho_proj_def:
In [8]:
%end axioms

These axioms may now be imported from the theory package: proveit.linear_algebra.inner_products