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, v_1_to_n, v_i, w_1_to_n, w_i,
A_i, A_1_to_i, A_1_to_n, B_1_to_j, C_1_to_k,
V_i, U_1_to_i, V_1_to_i, V_1_to_j, V_1_to_n, W_i, W_1_to_k, W_1_to_n)
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, LinMap, InnerProdSpaces, VecAdd, VecSum, VecZero,
ScalarMult, Norm, TensorProd, TensorExp)
from proveit.linear_algebra.addition import vec_summation_b1toj_fQ
In [2]:
%begin theorems
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))
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))
In [5]:
tensor_prod_of_linear_maps = Forall(
K, Forall(
n, Forall(
(V_1_to_n, W_1_to_n), Forall(
A_1_to_n, Forall(
v_1_to_n,
Equals(Function(TensorProd(A_1_to_n),
TensorProd(v_1_to_n)),
TensorProd(ExprRange(i, Function(A_i, v_i), one, n))),
domains=[V_1_to_n]).with_wrapping(),
domains=[ExprRange(i, LinMap(V_i, W_i), one, n)]).with_wrapping(),
domain=VecSpaces(K)).with_wrapping(),
domain=NaturalPos))
In [6]:
tensor_prod_association = (
Forall(
K, Forall(
(i, j, k), Forall(
(U_1_to_i, V_1_to_j, W_1_to_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_after_operator(),
domains=(U_1_to_i, V_1_to_j, W_1_to_k)).with_wrapping(),
domain=VecSpaces(K)).with_wrapping(),
domain=Natural)))
In [7]:
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)))
In [8]:
tensor_prod_disassociation = (
Forall(
K, Forall(
(i, j, k), Forall(
(U_1_to_i, V_1_to_j, W_1_to_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(),
domains=(U_1_to_i, V_1_to_j, W_1_to_k)).with_wrapping(),
domain=VecSpaces(K)).with_wrapping(),
domain=Natural)))
In [9]:
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)))
In [10]:
# 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)))
In [11]:
tensor_prod_factorization_from_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(
VecAdd(ExprRange(
m, TensorProd(a_1_to_i,
IndexedVar(b, m),
c_1_to_k),
one, j)),
TensorProd(a_1_to_i, VecAdd(b_1_to_j),
c_1_to_k))
.with_wrap_after_operator())
.with_wrap_after_operator()).with_wrapping(),
domain=VecSpaces(K)).with_wrapping(),
domain=Natural)))
In [12]:
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()).with_wrapping(),
domain=VecSpaces(K)).with_wrapping(),
domains=(Natural, NaturalPos, Natural))))
In [13]:
tensor_prod_factorization_from_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(
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)),
TensorProd(a_1_to_i, vec_summation_b1toj_fQ, c_1_to_k))
.with_wrap_before_operator())
.with_wrap_after_operator()),
domain=VecSpaces(K)),
domains=(Natural, NaturalPos, Natural))))
In [14]:
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 [15]:
tensor_prod_factorization_from_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(
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)),
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))
.with_wrap_before_operator())
.with_wrap_after_operator()).with_wrapping(),
domain=VecSpaces(K)).with_wrapping(),
domains=(Natural, NaturalPos, Natural))))
In [16]:
factor_scalar_from_tensor_prod = (
Forall(
K, Forall(
alpha, Forall(
(i, k), Forall(
(U_1_to_i, V, W_1_to_k), Forall(
(a_1_to_i, b, c_1_to_k),
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(),
domains=(U_1_to_i, V, W_1_to_k)).with_wrapping(),
domain=VecSpaces(K)).with_wrapping(),
domain=Natural),
domain=K)))
In [17]:
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)))
In [18]:
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)))
In [19]:
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))
In [20]:
tensor_exp_inclusion = Forall(
K, Forall(
n, Forall(V, SubsetEq(TensorExp(V, n), CartExp(V, n)),
domain=VecSpaces(K)),
domain=NaturalPos))
In [21]:
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))
Normalization of tensor product¶
In [22]:
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))
In [23]:
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))
In [24]:
%end theorems