logo

Demonstrations for the theory of proveit.linear_algebra

In [1]:
import proveit
from proveit import defaults
from proveit import a, b, c, X, Y, Z
from proveit.logic import InSet, InClass, CartExp
from proveit.numbers import Real, three
from proveit.linear_algebra import VecSpaces, VecAdd, ScalarMult
%begin demonstrations

Vector space closure proofs under addition and scalar multiplication

In [2]:
R3 = CartExp(Real, three)
R3:
In [3]:
defaults.assumptions = [InSet(a, Real), InSet(b, Real), InSet(c, Real),
                        InSet(X, R3), InSet(Y, R3), InSet(Z, R3)]
defaults.assumptions:
In [4]:
InSet(ScalarMult(a, X), R3).prove()
,  ⊢  
In [5]:
InSet(VecAdd(X, Y, Z), R3).prove()
, ,  ⊢  
In [6]:
lin_comb = VecAdd(ScalarMult(a, X), ScalarMult(b, Y), ScalarMult(c, Z))
lin_comb:
In [7]:
InSet(lin_comb, R3).prove()
, , , , ,  ⊢  
BEGIN Testing: working on a generalization of the VecAdd.factorization() method.
In [8]:
from proveit import a, b, c, i, j, k, u, v, w, x, y, z, IndexedVar
from proveit.linear_algebra import ScalarMult, TensorProd, VecAdd, VecSum
from proveit.numbers import one, nine, Interval, Mult
In [9]:
defaults.assumptions = [InSet(a, Real), InSet(b, Real), InSet(c, Real),
                        InSet(u, R3), InSet(v, R3), InSet(w, R3),
                        InSet(x, R3), InSet(y, R3), InSet(z, R3)]
defaults.assumptions:

Some work below on a possible function to check for a factor in a vector expression, the issue being that we might have a vector expression with heterogeneous components such as a VecAdd of a ScalarMult and a VecSum, etc.

In [10]:
def has_factor(vec, factor):
    if vec == factor:
        return True
    if isinstance(vec, ScalarMult):
        vec_simplified = vec.shallow_simplified()
        if (vec_simplified.scalar == factor or
          (isinstance(vec_simplified.scalar, Mult) and
           factor in vec_simplified.scalar.operands)):
                return True
        else:
            return has_factor(vec_simplified.scaled, factor)
    if isinstance(vec, TensorProd):
        print("We have a TensorProd: {}".format(vec))
        return any([has_factor(v, factor) for v in vec.operands])
    if isinstance(vec, VecSum):
        print("We have a VecSum: {}".format(vec))
        return has_factor(vec.summand, factor)
    if isinstance(vec, VecAdd):
        return all([has_factor(v, factor) for v in vec.operands])
In [11]:
example_01 = VecAdd(x, y, z)
example_01:
In [12]:
example_02 = VecAdd(x, ScalarMult(a, x), TensorProd(x, y))
example_02:
In [13]:
example_vec_sum_01 = VecSum(i, TensorProd(x, IndexedVar(y, i)), domain=Interval(one, nine))
example_vec_sum_01:
In [14]:
example_03 = VecAdd(x, ScalarMult(a, x), TensorProd(x, y), example_vec_sum_01)
example_03:
In [15]:
has_factor(example_03, x)

We have a TensorProd: x otimes y
We have a VecSum: Sum_{i=1}^{9} (x otimes y_{i})
We have a TensorProd: x otimes y_{i}

True
In [16]:
# containing a nested ScalarMult
example_04 = VecAdd(x, ScalarMult(a, ScalarMult(b, x)), TensorProd(x, y), example_vec_sum_01)
example_04:
In [17]:
has_factor(example_04, x)

We have a TensorProd: x otimes y
We have a VecSum: Sum_{i=1}^{9} (x otimes y_{i})
We have a TensorProd: x otimes y_{i}

True
END Testing
In [18]:
%end demonstrations