logo

Axioms for the theory of proveit.linear_algebra

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 Function
from proveit import m, n, v, x, y, A, B, K, S, T, V, W
from proveit.core_expr_types import a_i, v_i, a_1_to_n, x_1_to_n, A_1_to_m
from proveit.logic import (And, Iff, Equals, Forall, Exists, Set,
                           InSet, NotInSet)
from proveit.numbers import one, Add, NaturalPos, Interval
from proveit.linear_algebra import lin_comb_axn, some_nonzero_a
from proveit.linear_algebra import (LinMap, LinMapAdd, 
                                    VecAdd, ScalarMult,
                                    VecSpaces, SpanningSets, Bases,
                                    VecZero, LinDepSets,
                                    TensorProd, TensorExp)
In [2]:
%begin axioms

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

TODO: We need axioms to define vectors spaces (over fields and for specific vector addition and scalar multiplication operators to be fully abstract; alternatively, we could use the normal addition and multiplication operators and use literal generalization to be more general). We then define a LinMap according to its properties (see lin_map_domains and lin_map_linearity in the theorems).

Define the addition of linear maps.

In [3]:
linear_map_unary_addition = Forall(
    (V, W), Forall(S, Equals(LinMapAdd(S), S),
                   domain=LinMap(V, W)))
linear_map_unary_addition:
In [4]:
linear_map_binary_addition = Forall(
    (V, W), Forall((S, T), 
                   Forall(v, Equals(Function(LinMapAdd(S, T), v),
                                    Add(Function(S, v),
                                        Function(T, v))),
                          domain=V),
                   domain=LinMap(V, W)))
linear_map_binary_addition:
In [5]:
linear_map_multi_addition = Forall(
    m, Forall((A_1_to_m, B), 
              Equals(LinMapAdd(A_1_to_m, B), 
                     LinMapAdd(LinMapAdd(A_1_to_m), B)).with_wrap_after_operator()),
           domain=NaturalPos)
linear_map_multi_addition:
In [6]:
tensor_exp_one = Forall(x, Equals(TensorExp(x, one), x))
tensor_exp_one:
In [7]:
%end axioms

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