logo

Theorems (or conjectures) for the theory of proveit.linear_algebra.inner_products

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

from proveit import n, a, b, x, y, z, K, H, alpha
from proveit.logic import Forall, InSet, CartExp, InClass, Equals
from proveit.numbers import NaturalPos, Rational, Real, RealNonNeg, Complex
from proveit.numbers import Add, Mult, Abs, LessEq
from proveit.linear_algebra import (VecSpaces, InnerProdSpaces, VecAdd, ScalarMult, 
                                    InnerProd, Norm)
In [2]:
%begin theorems
Defining theorems for theory 'proveit.linear_algebra.inner_products'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions
In [3]:
inner_prod_space_is_vec_space = Forall(
    K, Forall(H, InClass(H, VecSpaces(K)),
              domain=InnerProdSpaces(K)))
Out[3]:
inner_prod_space_is_vec_space (conjecture without proof):

Number field vector sets are inner product spaces:

In [4]:
rational_vec_set_is_inner_prod_space = Forall(
    n, InClass(CartExp(Rational, n), InnerProdSpaces(Rational)),
    domain = NaturalPos)
Out[4]:
rational_vec_set_is_inner_prod_space (conjecture without proof):

In [5]:
real_vec_set_is_inner_prod_space = Forall(
    n, InClass(CartExp(Real, n), InnerProdSpaces(Real)),
    domain = NaturalPos)
Out[5]:
real_vec_set_is_inner_prod_space (conjecture without proof):

In [6]:
complex_vec_set_is_inner_prod_space = Forall(
    n, InClass(CartExp(Complex, n), InnerProdSpaces(Complex)),
    domain = NaturalPos)
Out[6]:
complex_vec_set_is_inner_prod_space (conjecture without proof):

As special cases, number fields are also inner product spaces:

In [7]:
rational_set_is_inner_prod_space = InClass(Rational, 
                                           InnerProdSpaces(Rational))
Out[7]:
rational_set_is_inner_prod_space (conjecture without proof):

In [8]:
real_set_is_inner_prod_space = InClass(Real, 
                                       InnerProdSpaces(Real))
Out[8]:
real_set_is_inner_prod_space (conjecture without proof):

In [9]:
complex_set_is_inner_prod_space = InClass(Complex, 
                                          InnerProdSpaces(Complex))
Out[9]:
complex_set_is_inner_prod_space (conjecture without proof):

Inner product linearity properties

In [10]:
inner_prod_linearity = Forall(
    K, Forall(
        H, Forall(
            (a, b), Forall(
                (x, y, z),
                Equals(InnerProd(VecAdd(ScalarMult(a, x), ScalarMult(b, y)), z),
                       VecAdd(ScalarMult(a, InnerProd(x, z)), 
                              ScalarMult(b, InnerProd(y, z)))),
                domain=H),
            domain=K),
        domain=InnerProdSpaces(K)))
Out[10]:
inner_prod_linearity (conjecture without proof):

In [11]:
inner_prod_scalar_mult_left = Forall(
    K, Forall(
        H, Forall(
            a, Forall(
                (x, y),
                Equals(InnerProd(ScalarMult(a, x), y),
                       ScalarMult(a, InnerProd(x, y))),
                domain=H),
            domain=K),
        domain = InnerProdSpaces(K)))
Out[11]:
inner_prod_scalar_mult_left (conjecture without proof):

In [12]:
inner_prod_scalar_mult_right = Forall(
    K, Forall(
        H, Forall(
            a, Forall(
                (x, y),
                Equals(InnerProd(x, ScalarMult(a, y)),
                       ScalarMult(a, InnerProd(x, y))),
                domain=H),
            domain=K),
        domain = InnerProdSpaces(K)))
Out[12]:
inner_prod_scalar_mult_right (conjecture without proof):

In [13]:
inner_prod_vec_add_left = Forall(
    K, Forall(
        H, Forall(
            (x, y, z),
            Equals(InnerProd(VecAdd(x, y), z),
                   VecAdd(InnerProd(x, z), InnerProd(x, z))),
            domain=H),
        domain = InnerProdSpaces(K)))
Out[13]:
inner_prod_vec_add_left (conjecture without proof):

In [14]:
inner_prod_vec_add_right = Forall(
    K, Forall(
        H, Forall(
            (x, y, z),
            Equals(InnerProd(x, VecAdd(y, z)),
                   VecAdd(InnerProd(x, y), InnerProd(x, z))),
            domain=H),
        domain = InnerProdSpaces(K)))
Out[14]:
inner_prod_vec_add_right (conjecture without proof):

Our specific Norm definition satisfy the properties of an abstract normalization

In [15]:
norm_is_nonneg = Forall(
    K, Forall(H, Forall(x, InSet(Norm(x), RealNonNeg),
                        domain=H),
              domain=InnerProdSpaces(H)))
Out[15]:
norm_is_nonneg (conjecture without proof):

In [16]:
scaled_norm = Forall(
    K, Forall(H, Forall((alpha, x), Equals(Norm(ScalarMult(alpha, x)), 
                                           Mult(Abs(alpha), Norm(x))),
                        domains=(K, H)),
              domain=InnerProdSpaces(K)))
Out[16]:
scaled_norm (conjecture without proof):

In [17]:
norm_triangle_ineq = Forall(
    K, Forall(H, Forall((x, y), LessEq(Norm(VecAdd(x, y)),
                                       Add(Norm(x), Norm(y))),
                        domain=H),
              domain=InnerProdSpaces(K)))
Out[17]:
norm_triangle_ineq (conjecture without proof):

In [18]:
%end theorems
These theorems may now be imported from the theory package: proveit.linear_algebra.inner_products