ZET Demo File

Loading the package

<<  "../Zet.m"

Definition of Sequences

Use DefineSequence for defining sequences by their defining relations and initial values.

Example: Define the sequence  f0[n] == (∑_(i = 1)^n) i

DefineSequence[summand[i + 1] == summand[i] +  1,  
      summand[0] == 0]

DefineSequence[f0[n + 1] == f0[n] + summand[n + 1],  
      f0[0] == 0]

The first argument is the recurrence, subsequent arguments specify initial conditions.

Both, recurrence and initial conditions are optional, but at least one equation has to be specified.

Example: Define a free sequence without defining relations

DefineSequence[f1[0] == 0]

This defines a sequence f1 about which nothing is known except that f1[0]==0.

Example: Define a sequence without initial conditions

DefineSequence[
      fibLike[n + 2] == fibLike[n + 1] + fibLike[n]]

This defines an object fibLike which obeys the Fibonacci recurrence, but nothing is assumed about its initial values.

The right hand side of the recurrence may involve sequence which have been defined before, but also indefinite sums, products, continued fractions, and expressions like (2^((2^n)))may be input directly. The function complains if it is not able to convert a given recurrence into an appropriate internal form.

Examples

Sum[i, {i, 1, n}]

DefineSequence[f2[n] == %]

Cfrac[
      Product[(i^2 + 1)/Harmonic[2*i + 5], {i, 1, k}] - 
        1/Sum[2^2^i, {i, 1, k}], {k, 1, n}]

DefineSequence[f3[n] == %]

Fib[2^n] + f0[n]/f1[n]

DefineSequence[f4[n] == %]

Definitions of sequences are stored in a database. The database can be reset to its initial state by the command ClearDefinitions[]. It is not possible to delete single definitions from the database.

ClearDefinitions[]

Evaluating Sequences at integer points

The command GetValue allows the evaluation of sequences at given integer points.

Example: Compute the 500th Fibonacci number

GetValue[Fib[500]]

Example: Evaluate the 5-fold sum \(TraditionalForm\`∑\+\(i = 1\)\%n\(∑\+\(j = 1\)\%i\(∑\+\(k = 1\)\%j\(∑\+\(l = 1\)\%k\(∑\+\(m = 1\)\%l 1\/m\)\)\)\)\) for n = 100.

DefineSequence[
      f5[n] ==  
        Sum[Sum[Sum[
              Sum[Sum[1/i4,  {i4, 1, i3}], {i3, 1, i2}], {i2, 1, i1}], {i1, 
              1, i0}], {i0, 1, n}]]

GetValue[f5[100]]

We could also have given the sum directly to GetValue but this is usually less efficient.

f5[50]  //  GetValue  //  Timing

Sum[
          Sum[Sum[Sum[Sum[1/i4,  {i4, 1, i3}], {i3, 1, i2}], {i2, 1, 
                i1}], {i1, 1, i0}], {i0, 1, 50}]  //  GetValue  //  
      Timing

Deciding Zero Equivalence of Sequences

In order to decide if a sequence is equivalent to zero, use the command ZeroQ.

Example: Prove (∑_(i = 1)^n) 
          i = (1/2) (n^2) + (1/2) n.

ZeroQ[Sum[i, {i, 1, n}] - 1/2*n^2 - 1/2*n,  
      ForAll  ->  n]

The first argument has to be a sequence defined by DefineSequence or any expression which can be the right hand side of the recurrence in DefineSequence. Observe the ForAll option specifying the induction variable.

As an alternative to ZeroQ, the command IdenticalQ may be used, which checks an equation for being true rather than a sequence for being zero. It calls ZeroQ on the difference between right hand side and left hand side.

Example: Prove (∑_(i = 1)^n) 
          i = (1/2) (n^2) + (1/2) n.

IdenticalQ[Sum[i, {i, 1, n}] == 1/2*n^2 + 1/2*n,  
      ForAll  ->  n]

The option field specifies whether free sequences should be put into the coefficient field. By default, this option is turned off. As a consequence, the algorithm may not terminate if arbitrary sequences are involved.

Example: Prove \(TraditionalForm\`\((∑\+\(i = 1\)\%n x\_i)\)\^2 = ∑\+\(i = 1\)\%n x\_i\%2 + 
          2 \(∑\+\(i = 1\)\%n x\_i\ \(∑\+\(j = 1\)\%\(i - 1\)x\_j\)\)\)

id  =  
      Sum[x[i], {i, 1, n}]^2 == 
        Sum[x[i]^2, {i, 1, n}] + 
          2*Sum[x[i]*Sum[x[j], {j, 1, i - 1}], {i, 1, n}]

IdenticalQ[id,  ForAll  ->  n]

IdenticalQ[id,  ForAll  ->  n,  
      Field  ->  True]

The behaviour of ZeroQ and IdenticalQ can be governed by the following options:
ForAll (symbol) specifies the induction variable
From (integer) specifies the starting point for the induction
MaxOrder (integer) specifies the number of iterations after which to give up
OrderMessage (True or False) specifies if a message should be printed for each iteration
Field (True or False) specifies if free variables should go into the coefficient field
GroebnerBasis (symbol) specifies the function which to use for Groebner basis computation
StartOrder (integer) the number of shifts to be started with (0 by default).
CheckInitialValues (True or False) specifies if initial values should be checked.

Example Gallery

Example 1: Multinomial Theorem

ClearDefinitions[]

mt = (1 + Sum[x[i],{i,1,n}])^2 == 
    1 + 2*Sum[x[i],{i,1,n}] + 
     2*Sum[Sum[x[j], {j, 1, -1 + i}]*x[i],{i,1,n}] +
        Sum[x[i]^2,{i,1,n}]

IdenticalQ[mt,  ForAll  ->  n,  
      Field  ->  True]

Example 2: from Carsten

ClearDefinitions[]

Sum[(-Fib[1 + k] + (1 + k)*
                Fib[k]*(1 + Harmonic[k]))/((1 + 
                  Harmonic[k])*(2 + 
                  k + (1 + k)*Harmonic[k])), {k, 
          0, -1 + n}] == (-1 + Fib[-1 + n] + Fib[n] - 
            Harmonic[n])/(1 + Harmonic[n])

IdenticalQ[%,  ForAll  ->  n]

Example 3: GKP, Exercise 5.93 (indefinite sum)

ClearDefinitions[]

Sum[
        Product[α + x[i], {i, 1, -1 + k}]/
          Product[x[i], {i, 1, k}], {k, 1, 
          n}] == (-1 + 
            Product[(α + x[k])/x[k], {k, 1, 
                n}])/α

IdenticalQ[%,  ForAll  ->  n]

Example 4: from Carsten

ClearDefinitions[]

Sum[
        Harmonic[k]*Sum[x[i], {i, 1, k}], {k, 1, 
          n}] == (-n + (1 + n)*Harmonic[n])*
          Sum[x[i], {i, 1, n}] - 
        Sum[k*x[k]*(-1 + Harmonic[k]), {k, 1, n}]

IdenticalQ[%,  ForAll  ->  n]

Example 5: GKP, Exercise 6.61 (Fibonacci)

ClearDefinitions[]

Sum[1/Fib[2^k], {k, 0, n}] == 
      3 - Fib[-1 + 2^n]/Fib[2^n]

IdenticalQ[%,  ForAll  ->  n]

Example 6: from Carsten

ClearDefinitions[]

Sum[
        Sum[Product[x[k]/(1 + x[k]), {k, 1, l}], {l, 1, r}]/(1 + 
              x[r]), {r, 1, n}] == 
      Sum[Product[x[i]/(1 + x[i]), {i, 1, k}]/(1 + x[k]), {k, 1, 
            n}] + Sum[(1 + x[i])^(-1), {i, 1, n}]*
          Sum[Product[x[k]/(1 + x[k]), {k, 1, i}], {i, 1, n}] - 
        Sum[Product[x[i]/(1 + x[i]), {i, 1, k}]*
            Sum[(1 + x[i])^(-1), {i, 1, k}], {k, 1, 
            n}]

IdenticalQ[%,  ForAll  ->  n]

Example 7: GEA, Theorem 5.2.4 (Christoffel-Darboux)

ClearDefinitions[]

DefineSequence[
      px[n + 2] == (x - c[n + 2])*px[n + 1] - λ[n + 2]*
            px[n], px[-1] == 0, px[0] == 1]

DefineSequence[
      pu[n + 2] == (u - c[n + 2])*pu[n + 1] - λ[n + 2]*
            pu[n], pu[-1] == 0, pu[0] == 1]

cd = 
      Sum[pu[k]*px[k]/Product[λ[i], {i, 1, k + 1}], {k, 0, 
            n}] == (px[n + 1]*pu[n] - px[n]*pu[n + 1])/(x - 
                u)/Product[λ[i], {i, 1, n + 1}]

IdenticalQ[cd, ForAll -> n,  Field -> True]

Example 8: GEA, Exercise 5.12 (Continuants)

ClearDefinitions[]

DefineSequence[κ1[n + 2] == 
        x[n + 2]*κ1[n + 1] + y[n + 2]*κ1[n], κ1[
          0] == x[0], κ1[1] == 
        x[0]*x[1] + y[1]]

DefineSequence[κ2[n + 2] == 
        x[n + 2]*κ2[n + 1] + y[n + 2]*κ2[n], κ2[
          0] == 1, κ2[1] == x[1]]

andrews = κ1[n]/κ2[n] == 
        x[0] + Sum[(-1)^(k + 1)*Product[
                    y[i], {i, 1, k}]/κ2[k - 1]/κ2[k], {k, 1, 
              n}]

IdenticalQ[andrews,  ForAll  ->  n]