# Axioms for the theory of proveit.linear_algebra.addition¶

In [1]:
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

In [2]:
%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:

In [3]:
scalar_add_extends_number_add = Forall(
i, Forall(
domain=Complex),
domain=NaturalPos)

In [ ]:



### VecSum (vector summation) Axioms¶

In [4]:
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.

In [5]:
vec_sum_single = Forall(v,
Forall(a,
Equals(VecSum(i, vi, domain=Interval(a,a)), va),
domain=Integer)
)

vec_sum_single:
In [6]:
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:
In [7]:
%end axioms

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