Axioms for the theory of proveit.linear_algebra.addition

import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.

from proveit import a, b, i, j, f, v, x, Q, fa, fx, va, vb, vi
from proveit.core_expr_types import (
    a_1_to_i, b_1_to_j, f__b_1_to_j, Q__b_1_to_j)
from proveit.logic import Implies, Forall, Equals, InSet
from proveit.numbers import NaturalPos, Integer, Interval, Complex
from proveit.numbers import one, Add, subtract, Less
from proveit.numbers.summation import summation_b1toj_fQ
from proveit.linear_algebra import VecAdd, VecSum
from proveit.linear_algebra.addition import vec_summation_b1toj_fQ

%begin axioms

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

Vector addition and number addition are the same when applied to complex numbers:

scalar_add_extends_number_add = Forall(
    i, Forall(
        a_1_to_i, Equals(VecAdd(a_1_to_i), Add(a_1_to_i)),
        domain=Complex),
    domain=NaturalPos)

scalar_add_extends_number_add:

VecSum (vector summation) Axioms

scalar_sum_extends_number_sum = Forall(
    j, Forall(
        (f, Q), 
        Implies(
            Forall(b_1_to_j, InSet(f__b_1_to_j, Complex), 
                   condition=Q__b_1_to_j),
            Equals(vec_summation_b1toj_fQ,
                   summation_b1toj_fQ))
        .with_wrap_after_operator()),
    domain=NaturalPos)

scalar_sum_extends_number_sum:

In the axioms below, we use the notation $v(i)$ to indicate a vector $v$ that is a function of $i$. For example, $v(k)$ might represent a vector like $e^{\pi \mathrm{i} \varphi 2^{k}} |k\rangle$. These axioms are largely analogous to the summation-related axioms found in the numbers/summation package.

vec_sum_single = Forall(v,
                   Forall(a,
                          Equals(VecSum(i, vi, domain=Interval(a,a)), va),
                          domain=Integer)
                  )

vec_sum_single:

vec_sum_split_last = (
    Forall(v,
           Forall((a, b),
                  Equals(VecSum(i, vi, domain=Interval(a, b)),
                         VecAdd(VecSum(i, vi, domain=Interval(a, subtract(b, one))), vb)),
                  domain = Integer,
                  conditions = [Less(a, b)])
          ))

vec_sum_split_last:

%end axioms

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