# 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

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

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

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)

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

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),
one, i))) \
.with_wrapping_at(2),
domains=(K, V)),
domain=Natural),
domain=VecSpaces(K)))

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

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

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),
j, ScalarMult(IndexedVar(a, j), v),
one, i)))
.with_wrapping_at(2),
domains=(Complex, V)),
domain=Natural),
domain=VecSpaces(K))
)

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

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