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

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

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

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.

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.

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:

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:

%end axioms

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