logo

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

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 Function, ExprRange, IndexedVar
from proveit import a, b, c, d, e, f, g, i, j, k, m, n, s, t, x, y, K, Q, S, U, V, W, alpha, fb
from proveit.core_expr_types import (
    a_1_to_i, a_1_to_m, b_1_to_j, c_1_to_k, c_1_to_n, 
    d_1_to_i, d_1_to_j, e_1_to_k, f_1_to_k, f__b_1_to_j, fj,
    n_1_to_m, n_k,
    A_1_to_i, B_1_to_j, C_1_to_k, U_1_to_i, V_1_to_i, W_1_to_k)
from proveit.logic import (Implies, And, Forall, Equals, NotEquals, 
                           InSet, InClass, CartExp, SubsetEq)
from proveit.numbers import one, Natural, NaturalPos, Add, Mult
from proveit.linear_algebra import (VecSpaces, InnerProdSpaces, VecAdd, VecSum, VecZero,
                                    ScalarMult, Norm, TensorProd, TensorExp)
from proveit.linear_algebra.addition import vec_summation_b1toj_fQ
In [2]:
%begin theorems
Defining theorems for theory 'proveit.linear_algebra.tensors'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions
In [3]:
tensor_prod_is_in_tensor_prod_space = Forall(
    K, Forall(
        i, Forall(
            V_1_to_i, Forall(
                a_1_to_i, InSet(TensorProd(a_1_to_i),
                                TensorProd(V_1_to_i)),
                domains=[V_1_to_i]),
            domain=VecSpaces(K)),
        domain=NaturalPos))
Out[3]:
tensor_prod_is_in_tensor_prod_space (conjecture without proof):

In [4]:
tensor_prod_of_vec_spaces_is_vec_space = Forall(
    K, Forall(i, Forall(V_1_to_i, InClass(TensorProd(V_1_to_i),
                                          VecSpaces(K)),
                        domain=VecSpaces(K)),
              domain=NaturalPos))
Out[4]:
tensor_prod_of_vec_spaces_is_vec_space (conjecture without proof):

In [5]:
tensor_prod_association = (
    Forall(
        K, Forall(
            (i, j, k), Forall(
                V, Forall(
                    (a_1_to_i, b_1_to_j, c_1_to_k),
                    Implies(
                        InSet(TensorProd(a_1_to_i, b_1_to_j, 
                                         c_1_to_k), V),
                        Equals(
                            TensorProd(a_1_to_i, b_1_to_j, c_1_to_k),
                            TensorProd(a_1_to_i, TensorProd(b_1_to_j), 
                                       c_1_to_k))
                        .with_wrap_before_operator())
                    .with_wrap_after_operator()).with_wrapping(),
                domain=VecSpaces(K)).with_wrapping(),
            domain=Natural)))
Out[5]:
tensor_prod_association (conjecture without proof):

In [6]:
tensor_prod_vec_space_association = (
    Forall(K,
    Forall((i, j, k),
    Forall((A_1_to_i, B_1_to_j, C_1_to_k),
                        Equals(
                            TensorProd(A_1_to_i, B_1_to_j, C_1_to_k),
                            TensorProd(A_1_to_i, TensorProd(B_1_to_j), 
                                       C_1_to_k))
       .with_wrap_before_operator(),
    domain=VecSpaces(K)).with_wrapping(),
    domain=Natural)))
Out[6]:
tensor_prod_vec_space_association (conjecture without proof):

In [7]:
tensor_prod_disassociation = (
    Forall(
        K, Forall(
            (i, j, k), Forall(
                V, Forall(
                    (a_1_to_i, b_1_to_j, c_1_to_k),
                    Implies(
                        InSet(TensorProd(
                            a_1_to_i, TensorProd(b_1_to_j),
                            c_1_to_k), V),
                        Equals(
                            TensorProd(a_1_to_i, TensorProd(b_1_to_j), 
                                       c_1_to_k),
                            TensorProd(a_1_to_i, b_1_to_j, c_1_to_k))
                        .with_wrap_before_operator())
                    .with_wrap_after_operator()).with_wrapping(),
                domain=VecSpaces(K)).with_wrapping(),
            domain=Natural)))
Out[7]:
tensor_prod_disassociation (conjecture without proof):

In [8]:
tensor_prod_vec_space_disassociation = (
    Forall(K,
    Forall((i, j, k),
    Forall((A_1_to_i, B_1_to_j, C_1_to_k),
                        Equals(TensorProd(A_1_to_i, TensorProd(B_1_to_j), 
                                       C_1_to_k),
                              TensorProd(A_1_to_i, B_1_to_j, C_1_to_k))
       .with_wrap_before_operator(),
    domain=VecSpaces(K)).with_wrapping(),
    domain=Natural)))
Out[8]:
tensor_prod_vec_space_disassociation (conjecture without proof):

In [9]:
# the antecedent here may be insufficient,
# because we may not be able to infer that
# all b_i are from same vector space
tensor_prod_distribution_over_add = (
    Forall(
        K, Forall(
            (i, j, k), Forall(
                V, Forall(
                    (a_1_to_i, b_1_to_j, c_1_to_k),
                    Implies(
                        InSet(TensorProd(
                            a_1_to_i, VecAdd(b_1_to_j), 
                            c_1_to_k), V),
                        Equals(
                            TensorProd(a_1_to_i, VecAdd(b_1_to_j),
                                       c_1_to_k),
                            VecAdd(ExprRange(
                                m, TensorProd(a_1_to_i, 
                                              IndexedVar(b, m),
                                              c_1_to_k),
                                one, j)))
                        .with_wrap_after_operator())
                    .with_wrap_after_operator()).with_wrapping(),
                domain=VecSpaces(K)).with_wrapping(),
             domain=Natural)))
Out[9]:
tensor_prod_distribution_over_add (conjecture without proof):

In [10]:
tensor_prod_distribution_over_summation = (
    Forall(
        (K, f, Q), Forall(
            (i, j, k), Forall(
                V, Forall(
                    (a_1_to_i, c_1_to_k), 
                    Implies(
                        Forall(b_1_to_j, InSet(TensorProd(
                            a_1_to_i, f__b_1_to_j, 
                            c_1_to_k), V), condition=Function(Q, b_1_to_j)),
                        Equals(
                            TensorProd(a_1_to_i, vec_summation_b1toj_fQ, c_1_to_k),
                            VecSum(b_1_to_j, TensorProd(a_1_to_i, f__b_1_to_j, c_1_to_k),
                                   condition=Function(Q, b_1_to_j)))
                        .with_wrap_before_operator())
                    .with_wrap_after_operator()),
                domain=VecSpaces(K)),
             domains=(Natural, NaturalPos, Natural))))
Out[10]:
tensor_prod_distribution_over_summation (conjecture without proof):

In [11]:
tensor_prod_distribution_over_summation_with_scalar_mult = (
    Forall((K, f, Q, s),
    Forall((i, j, k),
    Forall(V,
    Forall((a_1_to_i, c_1_to_k), 
        Implies(
            Forall(b_1_to_j, InSet(TensorProd(
                a_1_to_i, ScalarMult(Function(s, b_1_to_j), f__b_1_to_j), 
                c_1_to_k), V), condition=Function(Q, b_1_to_j)),
            Equals(
                TensorProd(a_1_to_i, VecSum(b_1_to_j, ScalarMult(Function(s, b_1_to_j), f__b_1_to_j) , condition=Function(Q, b_1_to_j)), c_1_to_k),
                VecSum(b_1_to_j, ScalarMult(Function(s, b_1_to_j), TensorProd(a_1_to_i, f__b_1_to_j, c_1_to_k)),
                       condition=Function(Q, b_1_to_j)))
            .with_wrap_before_operator())
        .with_wrap_after_operator()).with_wrapping(),
    domain=VecSpaces(K)).with_wrapping(),
    domains=(Natural, NaturalPos, Natural))))
Out[11]:
In [12]:
factor_scalar_from_tensor_prod = (
    Forall(
        K, Forall(
            alpha, Forall(
                (i, k), Forall(
                    V, Forall(
                        (a_1_to_i, b, c_1_to_k),
                        Implies(
                            InSet(TensorProd(
                                a_1_to_i, ScalarMult(alpha, b), 
                                c_1_to_k), V),
                            Equals(
                                TensorProd(a_1_to_i, 
                                           ScalarMult(alpha, b), 
                                           c_1_to_k),
                                ScalarMult(alpha, 
                                           TensorProd(a_1_to_i,
                                                      b, c_1_to_k)))
                            .with_wrap_before_operator())
                        .with_wrap_after_operator()).with_wrapping(),
                    domain=VecSpaces(K)),
                domain=Natural),
            domain=K)))
Out[12]:
factor_scalar_from_tensor_prod (conjecture without proof):

In [13]:
remove_vec_on_both_sides_of_equality = (
    Forall(
        K, Forall(
            (i, k), Forall(
                (U_1_to_i, V, W_1_to_k), Forall(
                    (a_1_to_i, c_1_to_k, d_1_to_i, f_1_to_k), Forall(
                        (b, e), 
                        Implies(Equals(TensorProd(a_1_to_i, b, c_1_to_k),
                                       TensorProd(d_1_to_i, e, f_1_to_k))
                                .with_wrap_after_operator(),
                                Equals(TensorProd(a_1_to_i, c_1_to_k), 
                                       TensorProd(d_1_to_i, f_1_to_k))
                                .with_wrap_after_operator())
                        .with_wrap_after_operator(),
                        domain=V, conditions=[
                            Equals(b, e),
                            NotEquals(b, VecZero(V))]),
                    domains=(U_1_to_i, W_1_to_k, U_1_to_i, W_1_to_k)).with_wrapping(),
                domain=VecSpaces(K)).with_wrapping(),
             domain=Natural)))
Out[13]:
remove_vec_on_both_sides_of_equality (conjecture without proof):

In [14]:
insert_vec_on_both_sides_of_equality = (
    Forall(
        K, Forall(
            (i, k), Forall(
                (U_1_to_i, V, W_1_to_k), Forall(
                    (a_1_to_i, c_1_to_k, d_1_to_i, e_1_to_k), Forall(
                        b, 
                        Implies(Equals(TensorProd(a_1_to_i, c_1_to_k),
                                       TensorProd(d_1_to_i, e_1_to_k))
                                .with_wrap_after_operator(),
                                Equals(TensorProd(a_1_to_i, b, c_1_to_k), 
                                       TensorProd(d_1_to_i, b, e_1_to_k))
                               .with_wrap_after_operator())
                        .with_wrap_after_operator(),
                        domain=V),
                    domains=(U_1_to_i, W_1_to_k, U_1_to_i, W_1_to_k)).with_wrapping(),
                domain=VecSpaces(K)).with_wrapping(),
             domain=Natural)))
Out[14]:
insert_vec_on_both_sides_of_equality (conjecture without proof):

In [15]:
tensor_prod_of_cart_exps_within_cart_exp = Forall(
    K, Forall(m, Forall(n_1_to_m, SubsetEq(TensorProd(ExprRange(k, CartExp(K, n_k), one, m)),
                                           CartExp(K, Mult(n_1_to_m))),
                        domain=NaturalPos),
              domain=NaturalPos))
Out[15]:
tensor_prod_of_cart_exps_within_cart_exp (conjecture without proof):

In [16]:
tensor_exp_inclusion = Forall(
    K, Forall(
        n, Forall(V, SubsetEq(TensorExp(V, n), CartExp(V, n)),
                       domain=VecSpaces(K)),
        domain=NaturalPos))
Out[16]:
tensor_exp_inclusion (conjecture without proof):

In [17]:
tensor_exp_of_cart_exp_inclusion = Forall(
    K, Forall(
        (m, n), Forall(V, SubsetEq(TensorExp(CartExp(V, m), n), CartExp(V, Mult(m, n))),
                       domain=VecSpaces(K)),
        domain=NaturalPos))
Out[17]:
tensor_exp_of_cart_exp_inclusion (conjecture without proof):

Normalization of tensor product

In [18]:
norm_of_tensor_prod = Forall(
    K, Forall(
        i, Forall(
            V_1_to_i, Forall(a_1_to_i, Equals(Norm(TensorProd(a_1_to_i)),
                                       Mult(ExprRange(k, Norm(IndexedVar(a, k)),
                                                      one, i))),
                      domains=[V_1_to_i]).with_wrapping(),
            domain=InnerProdSpaces(K)).with_wrapping(),
        domain=NaturalPos))
Out[18]:
norm_of_tensor_prod (conjecture without proof):

In [19]:
norm_preserving_tensor_prod = Forall(
    K, Forall(
        i, Forall(
            V_1_to_i, Forall(
                a_1_to_i, Equals(Norm(TensorProd(a_1_to_i)), one),
                domains=[V_1_to_i],
                condition=And(ExprRange(k, Equals(Norm(IndexedVar(a, k)),
                                                  one),
                                        one, i))).with_wrapping(),
            domain=InnerProdSpaces(K)).with_wrapping(),
        domain=NaturalPos))
Out[19]:
norm_preserving_tensor_prod (conjecture without proof):

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