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 x, y, K, H
from proveit.logic import Iff, And, Forall, Equals, InSet, InClass
from proveit.numbers import sqrt
from proveit.abstract_algebra import Fields
from proveit.linear_algebra import VecSpaces, InnerProdSpaces, InnerProd, Norm

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

Out[3]:
inner_prod_space_def:

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

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

Out[4]:
norm_def:
In [5]:
%end axioms

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