logo

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

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 ExprRange, Function, IndexedVar
from proveit import a, b, c, d, f, i, j, k, m, n, x, y, v, K, Q, V, alpha, beta
from proveit.core_expr_types import (
    a_1_to_i, a_1_to_m, a_1_to_n, b_1_to_j, c_1_to_k, f__b_1_to_j, x_1_to_n)
from proveit.logic import Equals, Forall, Implies, InClass, InSet
from proveit.numbers import one, Add, Complex, Interval, Mult, Natural, NaturalPos
from proveit.abstract_algebra import Fields, FieldAdd, FieldMult
from proveit.linear_algebra import VecSpaces, VecAdd, VecSum, ScalarMult
from proveit.linear_algebra import binary_lin_comb_ax_by, lin_comb_axn
from proveit.linear_algebra.addition import vec_summation_b1toj_fQ
In [2]:
%begin theorems
Defining theorems for theory 'proveit.linear_algebra.scalar_multiplication'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

Closure of linear combinations

In [3]:
scalar_mult_closure = Forall(
    K, Forall(
        V, Forall(a, Forall(x, InSet(ScalarMult(a, x), V),
                            domain=V),
                  domain=K),
        domain=VecSpaces(K)))
Out[3]:
scalar_mult_closure (conjecture without proof):

In [4]:
binary_lin_comb_closure = Forall(
    K, Forall(
        V, Forall((a, b), Forall((x, y), InSet(binary_lin_comb_ax_by, V),
                                 domain=V),
                  domain=K),
        domain=VecSpaces(K)))
Out[4]:
binary_lin_comb_closure (conjecture without proof):

In [5]:
lin_comb_closure = Forall(
    n, Forall(
        K, Forall(
            V, Forall(a_1_to_n, Forall(x_1_to_n, InSet(lin_comb_axn, V),
                                       domain=V),
                      domain=K),
            domain=VecSpaces(K))),
    domain=NaturalPos)
Out[5]:
lin_comb_closure (conjecture without proof):

ScalarMult Identity

In [6]:
one_as_scalar_mult_id = Forall(
    K,
    Forall(
        (v, V),
        Equals(ScalarMult(one, v), v),
        conditions=[InSet(v, V), InClass(V, VecSpaces(K))]),
    conditions=[InSet(one, K)])
Out[6]:
one_as_scalar_mult_id (conjecture without proof):

Distribution over the addition of vectors or scalars (for a vector space over a field $K$)

In [7]:
distribution_over_vectors = \
    Forall(
        K, Forall(
            V, Forall(
                i, Forall((k, a_1_to_i), 
                          Equals(ScalarMult(k, VecAdd(a_1_to_i)),
                                 VecAdd(ExprRange(j, ScalarMult(k, IndexedVar(a, j)),
                                                  one, i))) \
                          .with_wrapping_at(2),
                          domains=(K, V)),
                domain=Natural),
            domain=VecSpaces(K)))
Out[7]:
distribution_over_vectors (conjecture without proof):

In [8]:
distribution_over_vec_sum = (
    Forall((K, f, Q),
    Forall(j,
    Forall(V,
    Forall(k, 
        Implies(InSet(vec_summation_b1toj_fQ, V),
                Equals(
                    ScalarMult(k, vec_summation_b1toj_fQ),
                    VecSum(b_1_to_j, ScalarMult(k, f__b_1_to_j),
                           condition=Function(Q, b_1_to_j)))
                        .with_wrap_before_operator())
                    .with_wrap_after_operator(),
    domain = K),
    domain=VecSpaces(K)),
    domain=NaturalPos)))
Out[8]:
distribution_over_vec_sum (conjecture without proof):

In [9]:
distribution_over_vec_sum_with_scalar_mult = \
    Forall((K, f, Q, c),
        Forall(j,
            Forall(V,
                Forall(k,
                Implies(
                InSet(VecSum(b_1_to_j, ScalarMult(Function(c, b_1_to_j), f__b_1_to_j), condition=Function(Q, b_1_to_j)), V), 
                Equals(
                ScalarMult(k, VecSum(b_1_to_j, ScalarMult(Function(c, b_1_to_j), f__b_1_to_j), condition=Function(Q, b_1_to_j))),
                VecSum(b_1_to_j, ScalarMult(Mult(k, Function(c, b_1_to_j)), f__b_1_to_j), condition=Function(Q, b_1_to_j))
                ).with_wrap_before_operator()
                ).with_wrap_before_operator(),
                domain= K),
            domain=VecSpaces(K)),
        domain=NaturalPos)
    )
Out[9]:
distribution_over_vec_sum_with_scalar_mult (conjecture without proof):

In [10]:
distribution_over_scalars = \
    Forall(
        K, Forall(
            V, Forall(
                i, Forall(
                    (a_1_to_i, v), 
                    Equals(ScalarMult(VecAdd(a_1_to_i), v),
                           VecAdd(ExprRange(
                               j, ScalarMult(IndexedVar(a, j), v),
                               one, i)))
                    .with_wrapping_at(2),
                    domains=(Complex, V)),
                domain=Natural),
            domain=VecSpaces(K))
    )
Out[10]:
distribution_over_scalars (conjecture without proof):

In [11]:
# distribution_over_scalar_summation TODO

Associativity of scalar multiplication

In [12]:
doubly_scaled_as_singly_scaled = (
    Forall(
        K, Forall(
            V, Forall(
                x, Forall(
                    (alpha, beta),
                    Equals(ScalarMult(alpha, 
                                      ScalarMult(beta, x)),
                           ScalarMult(ScalarMult(alpha, beta), 
                                      x)),
                    domain=K),
                domain=V),
            domain=VecSpaces(K))
    ))
Out[12]:
doubly_scaled_as_singly_scaled (conjecture without proof):

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