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

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

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

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

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

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

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

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
Forall(
K, Forall(
(i, j, k), Forall(
V, Forall(
(a_1_to_i, b_1_to_j, c_1_to_k),
Implies(
InSet(TensorProd(
c_1_to_k), V),
Equals(
c_1_to_k),
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)))


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

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

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

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

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

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

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

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

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

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

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