In [1]:

```
import proveit
from proveit import Function
from proveit import a, b, c, f, i, j, k, l, m, n, x, fi, fij, A, B
from proveit.core_expr_types import f_1_to_i
from proveit.logic import Forall, InSet, Card
from proveit.numbers import zero, one, two, three, four, five, six, seven, eight, nine, infinity
from proveit.numbers import (Add, Exp, frac, greater, Less, LessEq, Mult, num, subtract, Sum )
from proveit.numbers import Complex, Integer, Interval, Natural, NaturalPos
from proveit.numbers.summation import al, bl, ak, bk
%begin demonstrations
```

Finite and infinite summations of the form $\sum_{i=m}^{n}f(i)$ arise in a wide variety of contexts, both as objects of study in their own right and as concise notational tools used within a variety of topics. Such summations are constructed in Prove-It using the `Sum`

class defined in `sum.py`

.

Summations are easy to construct using the Sum class, and such Sum objects are easily incorporated into other expressions. A summation object is created by invoking the `Sum`

class as follows:

```
Sum(index_or_indices, summand, domain=None, domains=None, condition=None,
conditions=None, _lambda_map=None)
```

Notice that the index argument and summand arguments are not optional. For example, we cannot create a generic summation expression such as $\sum f(x)$ with no index specified. We can create a summation, though, in which the domain for the index remains unspecified, such as $sum_{i}f(i)$.</br>

Notice also that Prove-It summations using the `Sum`

class are defined only for indices that range over contiguous integer domains such as an integral interval (created using the `Interval`

class) or the entire set of naturals $\mathbb{N}$ (for example, specified using `domain=Natural`

).

In [2]:

```
# A summation with summation index i, a generic summand, and no index domain
Sum(i, fi)
```

In [3]:

```
# A simple summation representing the sum of the first
# ten positive integers
sum_01 = Sum(i, Add(i, one), domain=Interval(zero, nine))
```

In [4]:

```
# An infinite geometric sum
sum_02 = Sum(i, frac(one, Exp(i, two)), domain=Natural)
```

In [5]:

```
# A more explicitly-indexed version of an infinite sum
sum_03 = Sum(m,Exp(x,m), domain=Interval(zero,infinity))
```

In [6]:

```
# A sum over multiple indices
sum_04 = Sum((i,j), Add(i,j))
```

In [7]:

```
# Even though we can create a summation over multiple indices,
# the Sum class is not yet implemented to handle such indices nor
# the extension to multiple index domains:
try:
sum_04 = Sum((i,j), Add(i,j), domains=[A, B])
except Exception as e:
print("Exception: {}".format(e))
```

Let's look at some simple examples of summations and their common attributes.

In [8]:

```
# Recall some enumerated sets defined earlier:
display(sum_01)
display(sum_02)
display(sum_03)
display(sum_04)
```

We can look at the construction of such expressions by calling expr_info() to see the table version of the expression's underlying directed acyclic graph (DAG) representation:

In [9]:

```
# See how a summation expression is constructed:
sum_01.expr_info()
```

We can access the various component elements of a Sum, including the index or indices, the summand, the domain, etc:

In [10]:

```
# the index
sum_02.index
```

In [11]:

```
# multiple ind4)
sum_04.indices
```

In [12]:

```
# the domain
display(sum_02)
sum_02.domain
```

In [13]:

```
# the domain's lower bound
display(sum_03)
sum_03.domain.lower_bound
```

In [14]:

```
# the summand
display(sum_02)
sum_02.summand
```

We can also dig into a Sum to find pieces of components:

In [15]:

```
display(sum_01)
sum_01.summand.operands[1]
```

The material below was developed to test various enumerated Set and Set-related methods. Some of this material could be integrated into the `_demonstrations_`

page eventually and/or deleted as development continues.

In [16]:

```
# define some summations for testing
sum_1_to_5, sum_2_to_6_i_plus_2, sum_a_to_b, sum_a_to_nine = (
Sum(i, i, domain=Interval(one, five)),
Sum(i, Add(i, two), domain=Interval(two, six)),
Sum(j, j, domain=Interval(a, b)),
Sum(k, subtract(k, two), domain=Interval(a, nine)))
```

In [17]:

```
# Integer
sum_1_to_5.deduce_in_number_set(Integer)
```

In [18]:

```
# Natural
sum_a_to_b.deduce_in_number_set(Natural, assumptions=[InSet(a, Natural), InSet(b, Natural)])
```

In [19]:

```
# NaturalPos
sum_a_to_b.deduce_in_number_set(NaturalPos, assumptions=[InSet(a, NaturalPos), InSet(b, NaturalPos)])
```

In [20]:

```
sum_2_to_6_i_plus_2.deduce_in_number_set(Complex)
```

In [21]:

```
example_geom_sum = Sum(i, Exp(two, i), domain=Interval(one, five))
```

In [22]:

```
# one of the theorems upon which the geom_sum_reduction() method is based:
from proveit.numbers.summation import gen_finite_geom_sum
gen_finite_geom_sum
```

In [23]:

```
self = example_geom_sum
```

In [24]:

```
example_geom_sum.geom_sum_reduction()
```

In [25]:

```
sum_2_to_6_i_plus_2.shifting(one)
```

In [26]:

```
sum_2_to_6_i_plus_2.shifting(one, auto_simplify=False)
```

In [27]:

```
sum_01.shifting(two)
```

In [28]:

```
sum_a_to_b.shifting(three, assumptions=[InSet(a, Natural), InSet(b, Natural)])
```

`Sum.partition()`

, `Sum.partition_first()`

, and `Sum.partition_last`

methods¶Notice that we also see a limited simplification of the resulting index and summand expressions.

In [29]:

```
# Basic splitting. Notice the lower index value expression for
# the second sum has been simplified from 4+1 to 5
sum_2_to_6_i_plus_2.partition(four)
```

In [30]:

```
# Still pretty basic, but with a variable lower-bound; again, the
# lower index value for second sum as been simplifed (7 + 1 = 8)
sum_a_to_nine.partition(seven, assumptions=[InSet(a, Integer), LessEq(a, seven)])
```

In [31]:

```
# This allows the splitting off of the last term but still keeping it
# in a summation by disabling auto-simplification.
sum_a_to_nine.partition(eight, assumptions=[InSet(a, Integer), LessEq(a, seven)],
auto_simplify=False)
```

In [32]:

```
# Auto-simplification reduces the last term appropriately.
sum_a_to_nine.partition(eight, assumptions=[InSet(a, Integer), LessEq(a, seven)])
```

In [33]:

```
# Or we can also explicitly use partition_last and allow
# simplification of the term being peeled off. The result is the
# same, but the proof is potentially simpler (not so much right now
# because the proof of 9-1=8 is overly complicated at the moment).
sum_a_to_nine.partition_last(assumptions=[InSet(a, Integer), LessEq(a, seven)])
```

In [34]:

```
sum_a_to_nine.partition(nine, side='before', assumptions=[InSet(a, Integer), LessEq(a, seven)])
```

In [35]:

```
# The same thing is accomplished by partitioning this way
# where we can recognize that we are splitting off just the last term.
sum_a_to_nine.partition(nine, side='before', assumptions=[InSet(a, Integer), LessEq(a, seven)])
```

In [36]:

```
# We can also explicitly use partition_last and suppress the
# simplification of the term being peeled off
sum_a_to_nine.partition_last(assumptions=[InSet(a, Integer), LessEq(a, seven)],
auto_simplify=False)
```

In [37]:

```
# Here we call split, which in turn calls split_off_first
sum_2_to_6_i_plus_2.partition(two, side='after')
```

In [38]:

```
# Or we can manually call partition_first
sum_2_to_6_i_plus_2.partition_first()
```

In [39]:

```
# Notice that the split of term is automatically simplified unless
# we suppress auto-simplification.
sum_2_to_6_i_plus_2.partition_first(auto_simplify=False)
```

`Sum.joining()`

method¶In [40]:

```
# define two simple, contiguous summations:
sum_1_to_5_i_squared, sum_6_to_9_i_squared, sum_5_plus_1_to_9_i_squared = (
Sum(i, Exp(i, two), domain=Interval(one, five)),
Sum(i, Exp(i, two), domain=Interval(six, nine)),
Sum(i, Exp(i, two), domain=Interval(Add(five, one), nine)))
```

In [41]:

```
sum_7_to_9_i_squared = Sum(i, Exp(i, two), domain=Interval(seven, nine))
```

In [42]:

```
# This format used to be required, where the upper index value of first sum
# and lower index value of second sum had to be explicitly related by a ±1
# This still works as originally coded but should now also simplify the
# index values if desired and possible
sum_1_to_5_i_squared.joining(sum_5_plus_1_to_9_i_squared)
```

In [43]:

```
# Now we can also proceed with the implicit ±1 relationship
# between the upper index value of first sum and lower index value
# of second sum, at least in simple cases.
sum_1_to_5_i_squared.joining(sum_6_to_9_i_squared)
```

In [44]:

```
from proveit import UnsatisfiedPrerequisites
try:
sum_1_to_5_i_squared.joining(sum_7_to_9_i_squared)
assert False
except UnsatisfiedPrerequisites as myException:
print("Expected Error: {}".format(myException))
```

In [45]:

```
sum_expr = Sum(l, al, domain=Interval(m, n))
```

In [46]:

```
weak_summand_relation = Forall(k, LessEq(ak, bk), domain=Interval(m, n))
```

In [47]:

```
sum_expr.deduce_bound(weak_summand_relation, assumptions=[weak_summand_relation])
```

In [48]:

```
strong_summand_relation = Forall(k, Less(ak, bk), domain=Interval(m, n))
```

In [49]:

```
# Note, with some added Interval automation, we should be able to get this to
# work assuming m >= n rather than |{m...n}| > 0. Change this in the future.
sum_expr.deduce_bound(strong_summand_relation,
assumptions=[strong_summand_relation,
greater(Card(Interval(m, n)), zero)])
```

In [50]:

```
sum_expr = Sum(l, Mult(c, Add(l, one)), domain=Integer)
```

In [51]:

```
sum_expr.factorization(c, assumptions=[InSet(c, Complex)])
```

In [52]:

```
sum_expr.factorization(c, pull='right',
assumptions=[InSet(c, Complex)])
```

In [53]:

```
sum_expr = Sum(l, Mult(a, b, Add(l, one)), domain=Integer)
```

In [54]:

```
sum_expr.factorization(Mult(a, b), assumptions=[InSet(a, Complex), InSet(b, Complex)])
```

In [55]:

```
sum_expr.factorization(Mult(a, b), pull='right', assumptions=[InSet(a, Complex), InSet(b, Complex)])
```

In [56]:

```
%end demonstrations
```