Axioms for the theory of proveit.linear_algebra.inner_products

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

%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.

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:

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

norm_def = Forall(
    K, Forall(H, Forall(x, Equals(Norm(x), sqrt(InnerProd(x, x))),
                        domain=H),
              domain=InnerProdSpaces(K)))

norm_def:

%end axioms

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