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

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, VecZero, VecAdd, VecSum, InnerProd, Norm)
from proveit.linear_algebra.addition import vec_summation_b1toj_fQ

%begin theorems

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

A few basic properties of vector addition

These derive from the definition of a vector space.

vec_add_zero_right = Forall(
    K, Forall(V, Forall(x, Equals(VecAdd(x, VecZero(V)), 
                                  VecZero(V)),
                        domain=V),
              domain=VecSpaces(K)))

vec_add_zero_right (conjecture without proof):

vec_add_zero_left = Forall(
    K, Forall(V, Forall(x, Equals(VecAdd(VecZero(V), x), 
                                  VecZero(V)),
                        domain=V),
              domain=VecSpaces(K)))

vec_add_zero_left (conjecture without proof):

multi_vec_add_def = Forall(
    K, Forall(
        V, Forall(n, Forall((x_1_to_n, y),
                            Equals(VecAdd(x_1_to_n, y),
                                   VecAdd(VecAdd(x_1_to_n), y)),
                            domain=V).with_wrapping(),
                  domain=NaturalPos),
              domain=VecSpaces(K)))

multi_vec_add_def (conjecture without proof):

Closure of vector addition

binary_closure = Forall(
    K, Forall(
        V, Forall((x, y), InSet(VecAdd(x, y), V),
                  domain=V),
        domain=VecSpaces(K)))

binary_closure (conjecture without proof):

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)

closure (conjecture without proof):

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$

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

association (conjecture without proof):

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

disassociation (conjecture without proof):

Commutation (permutation) theorems

binary_permutation = Forall(
    K, Forall(
        V, Forall((a, b), Equals(VecAdd(a, b), VecAdd(b, a)),
                  domain=V),
        domain=VecSpaces(K)))

binary_permutation (conjecture without proof):

leftward_permutation = Forall(
    K, Forall(
        V, Forall((i, j, k),
                  Forall((a_1_to_i, b_1_to_j, c, d_1_to_k),
                         Equals(VecAdd(a_1_to_i, b_1_to_j, c, d_1_to_k),
                                VecAdd(a_1_to_i, c, b_1_to_j, d_1_to_k))
                         .with_wrap_after_operator(),
                         domain=V),
                  domain=Natural),
        domain=VecSpaces(K)))

leftward_permutation (conjecture without proof):

rightward_permutation = Forall(
    K, Forall(
        V, Forall((i, j, k),
                  Forall((a_1_to_i, b, c_1_to_j, d_1_to_k),
                         Equals(VecAdd(a_1_to_i, b, c_1_to_j, d_1_to_k),
                                VecAdd(a_1_to_i, c_1_to_j, b, 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

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

vec_sum_of_constant_vec (conjecture without proof):

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)

number_add_reduction (conjecture without proof):

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

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

vec_sum_split_after (conjecture without proof):

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

vec_sum_split_before (conjecture without proof):

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

vec_sum_split_first (conjecture without proof):

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

vec_sum_index_shift (conjecture without proof):

Normalization of vector addition

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

norm_of_sum_of_orthogonal_pair (conjecture without proof):

%end theorems

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