arminstraub.com

Computer proved monotonicity of some coefficients

Ming-Hua Lin from the University of Regina sent me the following problem:

Problem: Let \(p \geqslant 2\) be an integer, and define $$ f (t) = \left( \frac{1}{1 - t \left( \frac{1}{p} + \frac{p - 1}{2 p^2} t \right)} \right)^p = \sum_{n \geqslant 0} c_n t^n . $$ Show that \(c_2 > c_3 > c_4 > \cdots\).

Solution

The following two-step solution is meant to advertise the power of today's Ekhads.

First, we establish the recurrence $$ 2 p^2 (n + 2) c_{n + 2} = 2 p (n + 1 + p) c_{n + 1} + (p - 1) (2 p + n) c_n $$ which together with the initial conditions \(c_0 = c_1 = 1\) determines the coefficients in question. This can be done automatically, for instance, using Mathematica 7. More generally, recurrences like this one may be found using the powerful HolonomicFunctions package by Christoph Koutschan (written for Mathematica):

DFiniteDE2RE[Annihilator[(1/(1-t(1/p+(p-1)/(2p^2)t)))^p, Der[t]], t, n]
produces the above recurrence right away.

Next, we use cylindrical algebraic decomposition to prove that \(c_n > c_{n + 1}\) for \(n \geqslant 2\) and \(p > 1\). This can also be done automatically! In fact, the immensely useful package SumCracker by Manuel Kauers (also written for Mathematica) can do it in a single (self-explanatory) line:

ProveInequality[y[n+1] < y[n], Using->{p>1}, Variable->n, From->2,
  Where->{y[n+2] == (2p(n+1+p)y[n+1] + (p-1)(2p+n)y[n]) / (2p^2(n+2)),
    y[0] == 1, y[1] == 1}]}
The succinct output True constitutes (existence of) proof that the claimed result indeed holds for \(p > 1\) (not necessary integral).