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

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, Sum, 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

%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

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

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

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

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

InClass(V, VecSpaces(K))

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

distribution_over_vectors = \
    Forall(
        K, Forall(
            V, Forall(
                n, Forall(
                    a, Forall(
                        x_1_to_n, 
                        Equals(ScalarMult(a, VecAdd(x_1_to_n)),
                               VecAdd(ExprRange(j, ScalarMult(a, IndexedVar(x, j)),
                                                one, n))).with_wrap_after_operator(),
                        domain=V),
                    domain=K),
                domain=Natural),
            domain=VecSpaces(K)))

distribution_over_vectors (conjecture without proof):

factorization_from_vectors = \
    Forall(
        K, Forall(
            V, Forall(
                i, Forall((k, a_1_to_i), 
                          Equals(VecAdd(ExprRange(j, ScalarMult(k, IndexedVar(a, j)),
                                                  one, i)),
                                ScalarMult(k, VecAdd(a_1_to_i))) \
                          .with_wrapping_at(2),
                          domains=(K, V)),
                domain=Natural),
            domain=VecSpaces(K)))

factorization_from_vectors (conjecture with conjecture-based proof):

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

factorization_from_vec_sum = (
    Forall((K, f, Q),
    Forall(j,
    Forall(V,
    Forall(k, 
        Implies(InSet(vec_summation_b1toj_fQ, V),
                Equals(
                    VecSum(b_1_to_j, ScalarMult(k, f__b_1_to_j),
                           condition=Function(Q, b_1_to_j)),
                    ScalarMult(k, vec_summation_b1toj_fQ))
                        .with_wrap_before_operator())
                    .with_wrap_after_operator(),
    domain = K),
    domain=VecSpaces(K)),
    domain=NaturalPos)))

factorization_from_vec_sum (conjecture without proof):

scalar_sum_distribution = (
    Forall((K, f, Q),
    Forall(j,
    Forall(V,
    Forall(v, 
        Implies(InSet(vec_summation_b1toj_fQ, K),
                Equals(
                    ScalarMult(Sum(b_1_to_j, f__b_1_to_j, 
                                   condition=Function(Q, b_1_to_j)), v),
                    VecSum(b_1_to_j, ScalarMult(f__b_1_to_j, v), 
                           condition=Function(Q, b_1_to_j)))
                        .with_wrap_before_operator())
                    .with_wrap_after_operator(),
    domain = V),
    domain=VecSpaces(K)),
    domain=NaturalPos)))

scalar_sum_distribution (conjecture without proof):

scalar_sum_factorization = (
    Forall((K, f, Q),
    Forall(j,
    Forall(V,
    Forall(v, 
        Implies(InSet(vec_summation_b1toj_fQ, K),
                Equals(
                    VecSum(b_1_to_j, ScalarMult(f__b_1_to_j, v), 
                           condition=Function(Q, b_1_to_j)),
                    ScalarMult(Sum(b_1_to_j, f__b_1_to_j, 
                                   condition=Function(Q, b_1_to_j)), v))
                        .with_wrap_before_operator())
                    .with_wrap_after_operator(),
    domain = V),
    domain=VecSpaces(K)),
    domain=NaturalPos)))

scalar_sum_factorization (conjecture without proof):

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

factorization_from_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(
                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)),
                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)))
                ).with_wrap_before_operator()
                ).with_wrap_before_operator(),
                domain= K),
            domain=VecSpaces(K)),
        domain=NaturalPos)
    )

factorization_from_vec_sum_with_scalar_mult (conjecture without proof):

distribution_over_scalars = \
    Forall(
        K, Forall(
            V, Forall(
                n, Forall(
                    a_1_to_n, Forall(
                        v, Equals(ScalarMult(VecAdd(a_1_to_n), v),
                                  VecAdd(ExprRange(j, ScalarMult(IndexedVar(a, j), v),
                                                   one, n))).with_wrap_after_operator(),
                        domain=V),
                    domain=K),
                domain=Natural),
            domain=VecSpaces(K))
    )

distribution_over_scalars (conjecture without proof):

factorization_from_scalars = \
    Forall(
        K, Forall(
            V, Forall(
                i, Forall(
                    (a_1_to_i, v), 
                    Equals(VecAdd(ExprRange(
                               j, ScalarMult(IndexedVar(a, j), v),
                               one, i)),
                           ScalarMult(VecAdd(a_1_to_i), v))
                    .with_wrapping_at(2),
                    domains=(Complex, V)),
                domain=Natural),
            domain=VecSpaces(K))
    )

factorization_from_scalars (conjecture without proof):

# distribution_over_scalar_summation TODO

Associativity of scalar multiplication

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

Relations

# We don't need to specify domains because this follows from generic substitution
scalar_mult_eq = Forall(alpha, Forall((x, y), Equals(ScalarMult(alpha, x), ScalarMult(alpha, y)),
                                      condition=Equals(x, y)))

scalar_mult_eq (established theorem):

%end theorems

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