Demonstrations for the theory of proveit.numbers.summation

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

Summations $\sum_{i=1}^{n}f(i)$

Introduction
Simple Expressions involving the Sum class
Common Attributes of a Sum
Further Demonstrations

1. TBA
2. TBA
3. TBA

Miscellaneous Testing

Introduction

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.

Simple Expressions Involving Summations

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

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

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

sum_01:

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

sum_02:

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

sum_03:

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

sum_04:

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

Exception: Sum class not yet implemented for multiple domains nor for multiple indices.

Common Attributes of Sum expressions

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

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

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

	core type	sub-expressions	expression
0	Operation	operator: 1 operand: 3
1	Literal
2	ExprTuple	3
3	Lambda	parameter: 13 body: 5
4	ExprTuple	13
5	Conditional	value: 6 condition: 7
6	Operation	operator: 8 operands: 9
7	Operation	operator: 10 operands: 11
8	Literal
9	ExprTuple	13, 12
10	Literal
11	ExprTuple	13, 14
12	Literal
13	Variable
14	Operation	operator: 15 operands: 16
15	Literal
16	ExprTuple	17, 18
17	Literal
18	Literal

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

# the index
sum_02.index

# multiple ind4)
sum_04.indices

# the domain
display(sum_02)
sum_02.domain

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

# the summand
display(sum_02)
sum_02.summand

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

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

Demonstrations

1. TBA

2. TBA

3. TBA

Miscellaneous Testing

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.

Testing Sum.deduce_in_number_set()

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

sum_1_to_5:

sum_2_to_6_i_plus_2:

sum_a_to_b:

sum_a_to_nine:

# Integer
sum_1_to_5.deduce_in_number_set(Integer)

 ⊢  

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

,  ⊢  

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

,  ⊢  

sum_2_to_6_i_plus_2.deduce_in_number_set(Complex)

 ⊢  

Testing the Sum.geom_sum_reduction() method

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

example_geom_sum:

# 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

 ⊢  

self = example_geom_sum

self:

example_geom_sum.geom_sum_reduction()

 ⊢  

Testing the Sum.shifting() method

sum_2_to_6_i_plus_2.shifting(one)

 ⊢  

sum_2_to_6_i_plus_2.shifting(one, auto_simplify=False)

 ⊢  

sum_01.shifting(two)

 ⊢  

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

,  ⊢  

Testing the 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.

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

 ⊢  

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

,  ⊢  

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

,  ⊢  

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

,  ⊢  

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

,  ⊢  

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

,  ⊢  

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

,  ⊢  

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

,  ⊢  

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

 ⊢  

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

 ⊢  

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

 ⊢  

Testing the Sum.joining() method

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

sum_1_to_5_i_squared:

sum_6_to_9_i_squared:

sum_5_plus_1_to_9_i_squared:

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

sum_7_to_9_i_squared:

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

 ⊢  

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

 ⊢  

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

Expected Error: Prerequisites not met while assuming (): Sum joining using Sum.join() only implemented for when there is an explicit (or easily verified) increment of one unit from the first summation's upper bound to the second summation's lower bound (or decrement of one unit from second summation's lower bound to first summation's upper bound). We have first summation upper bound of 5 with the second summation lower bound of 7. If these appear to have the necessary relationship, you might need to prove this before calling the Sum.join() method.

Testing Sum.deduce_bound()

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

sum_expr:

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

weak_summand_relation:

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

 ⊢  

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

strong_summand_relation:

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

,  ⊢  

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

sum_expr:

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

 ⊢  

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

 ⊢  

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

sum_expr:

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

,  ⊢  

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

,  ⊢  

%end demonstrations