# Theorems (or conjectures) for the theory of proveit.linear_algebra.addition¶

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 (
a, b, c, f, i, j, k, n, x, y, K, Q, V, fx, v, va, vi,
Function)
from proveit.core_expr_types import (
a_1_to_i, b_1_to_j, c_1_to_j, c_1_to_k, d_1_to_k, x_1_to_n,
f__b_1_to_j, Q__b_1_to_j)
from proveit.logic import Implies, Forall, Equals, InSet
from proveit.numbers import (
Natural, NaturalPos, Integer, Interval, Complex,
zero, one, Add,  subtract, Less, LessEq, sqrd, sqrt)
from proveit.numbers.summation import summation_b1toj_fQ
from proveit.linear_algebra import ScalarMult, VecSpaces, VecAdd, VecSum, InnerProd, Norm

In [2]:
%begin theorems

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


In [3]:
binary_closure = Forall(
K, Forall(
V, Forall((x, y), InSet(VecAdd(x, y), V),
domain=V),
domain=VecSpaces(K)))

binary_closure (conjecture without proof):

In [4]:
closure = Forall(
n, Forall(
K, Forall(
domain=V),
domain=VecSpaces(K))),
domain=NaturalPos)

closure (conjecture without proof):

In [5]:
summation_closure = Forall(
j, Forall(
(K, f, Q), Forall(
V, Implies(
Forall(b_1_to_j, InSet(f__b_1_to_j, V),
condition=Q__b_1_to_j),
InSet(vec_summation_b1toj_fQ, V))
.with_wrap_after_operator(),
domain=VecSpaces(K))),
domain=NaturalPos)

summation_closure (conjecture without proof):

### Association and disassociation of vector addition for a vector space over a field $K$¶

In [6]:
association = \
Forall(
K, Forall(
V, Forall((i,j,k),
Forall((a_1_to_i,b_1_to_j,c_1_to_k),
.with_wrapping_at(2),
domain=V),
domain=Natural),
domain=VecSpaces(K)))

association (conjecture without proof):

In [7]:
disassociation = \
Forall(
K, Forall(
V, Forall((i,j,k),
Forall((a_1_to_i,b_1_to_j,c_1_to_k),
.with_wrapping_at(2),
domain=V),
domain=Natural),
domain=VecSpaces(K)))

disassociation (conjecture without proof):

### Commutation (permutation) theorems¶

In [8]:
binary_permutation = Forall(
K, Forall(
domain=V),
domain=VecSpaces(K)))

binary_permutation (conjecture without proof):

In [9]:
leftward_permutation = Forall(
K, Forall(
V, Forall((i, j, k),
Forall((a_1_to_i, b_1_to_j, c, d_1_to_k),
.with_wrap_after_operator(),
domain=V),
domain=Natural),
domain=VecSpaces(K)))

leftward_permutation (conjecture without proof):

In [10]:
rightward_permutation = Forall(
K, Forall(
V, Forall((i, j, k),
Forall((a_1_to_i, b, c_1_to_j, d_1_to_k),
.with_wrap_after_operator(),
domain=V),
domain=Natural),
domain=VecSpaces(K)))

rightward_permutation (conjecture without proof):

### Vector summations and number reductions¶

In [11]:
# this may be problematic --- do we know that j, k \in K?
# would there be some other situation possible?
# does this mean that Integer is a subset of K?
vec_sum_of_constant_vec = (
Forall(K,
Forall((j, k),
Forall(V,
Forall(v,
Equals(VecSum(i, v, domain=Interval(j, k)),
),
domain = V),
domain = VecSpaces(K)),
domain=Integer,
conditions=[LessEq(j, k)])))

vec_sum_of_constant_vec (conjecture without proof):

In [12]:
number_add_reduction = Forall(
domain=Complex),
domain=NaturalPos)


In [13]:
number_summation_reduction = Forall(
(f, Q), Forall((n, j), Forall(x_1_to_n, Equals(vec_summation_b1toj_fQ,
summation_b1toj_fQ),
domain=Complex),
domain=NaturalPos))

number_summation_reduction (conjecture without proof):

In [14]:
vec_sum_split_after = (
Forall(v,
Forall([a, b, c],
Equals(VecSum(i, vi, domain=Interval(a, c)),
domain=Integer, conditions=[LessEq(a, b), Less(b, c)])
))

vec_sum_split_after (conjecture without proof):

In [15]:
vec_sum_split_before = (
Forall(v,
Forall([a, b, c],
Equals(VecSum(i, vi, domain=Interval(a, c)),
VecSum(i, vi, domain=Interval(b, c)))),
domain=Integer, conditions=[Less(a, b), LessEq(b, c)])
))

vec_sum_split_before (conjecture without proof):

In [16]:
vec_sum_split_first = (
Forall(v,
Forall([a, b],
Equals(VecSum(i, vi, domain=Interval(a, b)),
domain=Integer, conditions=[Less(a, b)])
))

vec_sum_split_first (conjecture without proof):

In [17]:
vec_sum_index_shift = (
Forall(v,
Forall((a, b, c),
Equals(VecSum(i, Function(v, i), domain=Interval(a, b)),
VecSum(i, Function(v, subtract(i, c)),
domain=Integer)
))

vec_sum_index_shift (conjecture without proof):

In [18]:
norm_of_sum_of_orthogonal_pair = Forall(
K, Forall(V, Forall((a, b), Equals(Norm(VecAdd(a, b)),

%end theorems

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