logo

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_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
from proveit.linear_algebra.addition import vec_summation_b1toj_fQ
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

Closure of vector addition

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

In [4]:
closure = Forall(
    n, Forall(
        K, Forall(
            V, Forall(x_1_to_n, InSet(VecAdd(x_1_to_n), V),
                      domain=V),
            domain=VecSpaces(K))),
    domain=NaturalPos)
Out[4]:
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)
Out[5]:
summation_closure (conjecture without proof):

Asssociation 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), 
                             Equals(VecAdd(a_1_to_i, b_1_to_j, c_1_to_k),
                                    VecAdd(a_1_to_i, VecAdd(b_1_to_j), c_1_to_k)) \
                             .with_wrapping_at(2),
                             domain=V),
                      domain=Natural),
            domain=VecSpaces(K)))
Out[6]:
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), 
                             Equals(VecAdd(a_1_to_i, VecAdd(b_1_to_j), c_1_to_k),
                                    VecAdd(a_1_to_i, b_1_to_j, c_1_to_k)) \
                             .with_wrapping_at(2),
                             domain=V),
                      domain=Natural),
            domain=VecSpaces(K)))
Out[7]:
disassociation (conjecture without proof):

We should add commutation theorems, but we may want to revise naming conventions (e.g., permutation) first.

In [8]:
# 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)),
                         ScalarMult(Add(subtract(k, j), one), v)
        ),
    domain = V),
    domain = VecSpaces(K)),
    domain=Integer,
    conditions=[LessEq(j, k)])))
Out[8]:
vec_sum_of_constant_vec (conjecture without proof):

In [9]:
number_add_reduction = Forall(
    n, Forall(x_1_to_n, Equals(VecAdd(x_1_to_n), 
                               Add(x_1_to_n)),
              domain=Complex),
    domain=NaturalPos)
Out[9]:
number_add_reduction (conjecture without proof):

In [10]:
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))
Out[10]:
number_summation_reduction (conjecture without proof):

In [11]:
vec_sum_split_after = (
    Forall(v,
           Forall([a, b, c],
                  Equals(VecSum(i, vi, domain=Interval(a, c)),
                         VecAdd(VecSum(i, vi, domain=Interval(a, b)),
                             VecSum(i, vi, domain=Interval(Add(b, one), c)))),
                   domain=Integer, conditions=[LessEq(a, b), Less(b, c)])
    ))
Out[11]:
vec_sum_split_after (conjecture without proof):

In [12]:
vec_sum_split_before = (
    Forall(v,
           Forall([a, b, c],
                  Equals(VecSum(i, vi, domain=Interval(a, c)),
                         VecAdd(VecSum(i, vi, domain=Interval(a, subtract(b, one))),
                             VecSum(i, vi, domain=Interval(b, c)))),
                   domain=Integer, conditions=[Less(a, b), LessEq(b, c)])
    ))
Out[12]:
vec_sum_split_before (conjecture without proof):

In [13]:
vec_sum_split_first = (
    Forall(v,
           Forall([a, b],
                  Equals(VecSum(i, vi, domain=Interval(a, b)),
                         VecAdd(va,
                             VecSum(i, vi, domain=Interval(Add(a, one), b)))),
                   domain=Integer, conditions=[Less(a, b)])
    ))
Out[13]:
vec_sum_split_first (conjecture without proof):

In [14]:
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=Interval(Add(a, c), Add(b, c)))),
                  domain=Integer)
    ))
Out[14]:
vec_sum_index_shift (conjecture without proof):

Normalization of vector addition

In [15]:
norm_of_sum_of_orthogonal_pair = Forall(
    K, Forall(V, Forall((a, b), Equals(Norm(VecAdd(a, b)),
                                       sqrt(Add(sqrd(Norm(a)), sqrd(Norm(b))))),
                        domain=V, condition=Equals(InnerProd(a, b), zero)),
              domain=VecSpaces(K)))
Out[15]:
norm_of_sum_of_orthogonal_pair (conjecture without proof):

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