Theorems (or conjectures) for the theory of proveit.numbers.summation

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 (a, b, c, d, f, g, i, j, k, l, m, n, x, y, fa, fx,
                     gx, gy, R, S, Q, Qx)
from proveit import Function
from proveit.logic import Implies, Forall, Equals, InSet, Card, SetOfAll
from proveit import Operation
from proveit.core_expr_types import x_1_to_m, y_1_to_n, fi, fj, gi, gj
from proveit.logic import (Card, Equals, Forall, Implies, InSet, NotEquals,
                           SetOfAll, SubsetEq)
from proveit.numbers import (Add, Abs, Exp, frac, greater, Integrate, Less, LessEq,
                             Mult, Neg, number_ordering, subtract, Sum)
from proveit.numbers import ZeroSet, Natural, NaturalPos, Integer, IntervalCC, Real
from proveit.numbers import Complex, Interval, zero, one, two, infinity
from proveit.numbers.functions import MonDecFuncs
from proveit.numbers.summation import al, ak, bl, bk

%begin theorems

Defining theorems for theory 'proveit.numbers.summation'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

distributive_summation = (
    Forall(
        f,
    Forall(
        x,
    Forall(
    (j, k),
    Equals(Sum(i, Mult(x, fi), domain=Interval(j, k)),
           Mult(x, Sum(i, fi, domain=Interval(j, k)))),
    domain=Integer),
    domain=Complex)))

distributive_summation (conjecture without proof):

distributive_summation_spec = (
    Forall(
        (f, g),
    Forall(
        (x),
    Forall(
    (c, d),
    Equals(Sum(j, Mult(Mult(x, gj), fj), domain=Interval(c, d)),
           Mult(x, Sum(j, Mult(gj, fj), domain=Interval(c, d)))),
    domain=Integer),
    domain=Complex)))

distributive_summation_spec (conjecture without proof):

Several basic closure theorems: if we sum up terms each of which belongs to set S, we generally end up with a sum in set S as well.

summation_zero_closure = Forall(
    [f, Q], Implies(Forall(x, Equals(fx, zero), condition=Qx), 
                    InSet(Sum(x, fx, condition=Qx), domain=ZeroSet)))

summation_zero_closure (conjecture without proof):

summation_nat_closure = Forall(
    [f, Q], Implies(Forall(x, InSet(fx, Natural), condition=Qx), 
                    InSet(Sum(x, fx, condition=Qx), domain=Natural)))

summation_nat_closure (conjecture without proof):

summation_nat_pos_closure = Forall(
    [f, Q], Implies(Forall(x, InSet(fx, NaturalPos), condition=Qx), 
                    InSet(Sum(x, fx, condition=Qx), domain=NaturalPos)))

summation_nat_pos_closure (conjecture without proof):

summation_int_closure = Forall(
    [f, Q], Implies(Forall(x, InSet(fx, Integer), condition=Qx), 
                    InSet(Sum(x, fx, condition=Qx), domain=Integer)))

summation_int_closure (conjecture without proof):

summation_real_closure = Forall(
    [f, Q], Implies(Forall(x, InSet(fx, Real), condition=Qx), 
                       InSet(Sum(x, fx, condition=Qx), domain=Real)))

summation_real_closure (conjecture without proof):

summation_complex_closure = Forall(
    [f, Q], Implies(Forall(x, InSet(fx, Complex), condition=Qx), 
                       InSet(Sum(x, fx, condition=Qx), domain=Complex)))

summation_complex_closure (conjecture without proof):

Splitting up summations

sum_split_general = (
    Forall(f,
           Forall([a, b, c],
                  Equals(Sum(x, fx, domain=Interval(a, c)),
                         Add(Sum(x, fx, domain=Interval(a, b)),
                             Sum(x, fx, domain=Interval(Add(b, one), c)))),
                   domain=Integer, conditions=[number_ordering(LessEq(a, b), LessEq(b, c))])
    ))

sum_split_general (conjecture without proof):

sum_split_after = (
    Forall(f,
           Forall([a, b, c],
                  Equals(Sum(x, fx, domain=Interval(a, c)),
                         Add(Sum(x, fx, domain=Interval(a, b)),
                             Sum(x, fx, domain=Interval(Add(b, one), c)))),
                   domain=Integer, conditions=[LessEq(a, b), Less(b, c)])
    ))

sum_split_after (conjecture without proof):

sum_split_before = (
    Forall(f,
           Forall([a, b, c],
                  Equals(Sum(x, fx, domain=Interval(a, c)),
                         Add(Sum(x, fx, domain=Interval(a, subtract(b, one))),
                             Sum(x, fx, domain=Interval(b, c)))),
                  domain=Integer,
                  conditions=[Less(a, b), LessEq(b, c)])
    ))

sum_split_before (conjecture without proof):

sum_split_first = (
    Forall(f,
        Forall((a, b),
               Equals(Sum(x, fx, domain=Interval(a, b)),
                      Add(fa, Sum(x, fx, domain=Interval(Add(a, one), b)))),
        domain=Integer,
        conditions=[Less(a, b)])
      ))

sum_split_first (conjecture without proof):

Index shifting

index_shift = (
    Forall(f,
           Forall((a, b, c),
                  Equals(Sum(x, Function(f, x), domain=Interval(a, b)),
                         Sum(x, Function(f, subtract(x, c)),
                             domain=Interval(Add(a, c), Add(b, c)))),
                  domain=Integer)
    ))

index_shift (conjecture without proof):

Index negation

# This can be generalized later when we establish a
# class of even functions
index_negate = (
    Forall(f,
           Forall((a, b),
                  Equals(Sum(x, Function(f, x), domain=Interval(a, b)),
                         Sum(x, Function(f, Neg(x)),
                             domain=Interval(Neg(b), Neg(a)))),
                  domain=Integer)
    ))

index_negate (conjecture without proof):

sum_zero_and_one = (
    Forall(f,
           Equals(Sum(n, Function(f, n), domain=Interval(zero, one)),
                  Add(Function(f, zero), Function(f, one)))
    ))

sum_zero_and_one (conjecture without proof):

Some specific summation formulas

trivial_sum = Forall(
    (a, b), Forall(x, Equals(Sum(i, x, domain=Interval(a, b)),
                             Mult(Add(b, Neg(a), one), x)),
                   domain=Complex),
    domain=Integer)

trivial_sum (conjecture without proof):

# finite_geom_sum = (
#     Forall([x, n],
#            Equals(Sum(m, Exp(x, m), domain=Interval(zero, n)),
#                   frac(subtract(one, Exp(x, Add(n, one))),
#                        subtract(one, x))),
#            domains=[Complex, NaturalPos]))

finite_geom_sum = (
    Forall([x, n],
           Equals(Sum(i, Exp(x, i), domain=Interval(zero, n)),
                  frac(subtract(one, Exp(x, Add(n, one))),
                       subtract(one, x))),
           domains=[Complex, Natural],
           conditions=[NotEquals(x, one)]))

finite_geom_sum (conjecture with conjecture-based proof):

gen_finite_geom_sum = (
        Forall(x,
        Forall((j, k),
               Equals(Sum(i, Exp(x, i), domain=Interval(j, k)),
                      frac(subtract(Exp(x, j), Exp(x, Add(k, one))), subtract(one, x))),
        domain=Integer, condition=LessEq(j, k)),
        domain=Complex, condition=NotEquals(x, one)))

gen_finite_geom_sum (conjecture without proof):

inf_geom_sum = Forall(x, Equals(Sum(m,Exp(x,m),
                                  domain=Interval(zero, infinity)), 
                              frac(one,subtract(one,x))),
                    domain=Complex, condition=Less(Abs(x), one))

inf_geom_sum (conjecture without proof):

sum_first_n_int = Forall(n,
                       Equals( Sum(k, k, domain=Interval(one, n)),
                               frac(Mult(n, Add(n, one)), two) ),
                       domain=NaturalPos)

sum_first_n_int (conjecture with conjecture-based proof):

same_sums = (
    Forall((f, g),
           Forall((m, n),
                  Implies(Forall(k,
                                 Equals(Function(f, k), Function(g, k)),
                                 domain=Interval(m, n)),
                          Equals(Sum(l, Function(f, l), domain=Interval(m, n)),
                                 Sum(l, Function(g, l), domain=Interval(m, n)))),
                  domain=Integer)))

same_sums (conjecture without proof):

# Could also make such a theorem to apply whenever addition is
# commutative, not just for the Complex numbers.
# See alternate version below controlling mapping from S to R
# to be bijective.
# equiv_sums = (
#     Forall((f, g, R, S),
#            Implies(Forall(a, InSet(fa, Complex), domain=R),
#                    Equals(Sum(x, fx, domain=R),
#                           Sum(y, Function(f, gy), domain=S))),
#            conditions=[Equals(SetOfAll(y, gy, domain=S), R)]))

equiv_sums = Forall(
    n, 
    Forall((f, g, R, S),
           Implies(Forall(a, InSet(fa, Complex), domain=R),
                   Equals(Sum(x, fx, domain=R),
                          Sum(y, Function(f, gy), domain=S))),
           conditions=[Equals(SetOfAll(y, gy, domain=S), R),
                       Equals(Card(S), n), Equals(Card(R), n)]),
    domain=Natural)

equiv_sums (conjecture without proof):

Bounding Theorems

bounded_sum = Forall((S, f, g), Implies(Forall(x, LessEq(
    fx, gx), domain=S), LessEq(Sum(x, fx, domain=S), Sum(x, gx, domain=S))))

bounded_sum (conjecture without proof):

weak_summation_from_summands_bound = Forall(
    (a, b, S), Implies(Forall(k, LessEq(ak, bk), domain=S),
                       LessEq(Sum(l, al, domain=S),
                              Sum(l, bl, domain=S))))

weak_summation_from_summands_bound (conjecture without proof):

strong_summation_from_summands_bound = Forall(
    (a, b, S), Implies(Forall(k, Less(ak, bk), domain=S),
                       Less(Sum(l, al, domain=S),
                            Sum(l, bl, domain=S))),
                      condition=greater(Card(S), zero))

strong_summation_from_summands_bound (conjecture without proof):

# sum_integrate_ineq = (
#     Forall(f,
#     Forall((a,b),
#         LessEq(
#             Sum(x, Function(f,x), domain=Interval(a,b)),
#             Add(fa, Integrate(x, Function(f, x), domain=IntervalCC(a,b)))),
#     domain=Integer, condition=LessEq(a,b)),
#     domain=MonDecFuncs))

integral_upper_bound_of_sum_lemma = (
    Forall(S,
    Forall(f,
    Forall((a,b), LessEq(
            Sum(x, Function(f,x), domain=Interval(a,b)),
            Add(fa, Integrate(x, Function(f, x), domain=IntervalCC(a,b)))),
        domain=Integer, conditions=[LessEq(a,b), SubsetEq(IntervalCC(a, b), S)]),
        domain=MonDecFuncs(S),
        condition=SubsetEq(S, Real))))

integral_upper_bound_of_sum_lemma (conjecture without proof):

integral_upper_bound_of_sum = (
    Forall(S,
    Forall(f,
    Forall((a,b), LessEq(
            Sum(x, Function(f,x), domain=Interval(a, b)),
            Integrate(x, Function(f, x), domain=IntervalCC(subtract(a, one),b))),
        domain=Integer, conditions=[LessEq(a,b), 
                                    SubsetEq(IntervalCC(subtract(a, one), b), S)]),
        domain=MonDecFuncs(S),
        condition=SubsetEq(S, Real))))

integral_upper_bound_of_sum (conjecture without proof):

%end theorems

These theorems may now be imported from the theory package: proveit.numbers.summation