jcreed blog > The Functional Programmer's -1/12 (2)

The Functional Programmer's -1/12 (2)

I notice there's a family of different derivations you can go through to still obtain \[1+2+3+\cdots = -1/12\] Instead of computing $\alpha(q) + \alpha(-q)$, we can compute \[\sum_{i=0}^{n-1} \alpha(\zeta^i q)\] for $\zeta$ an $n^{th}$ root of unity. First let's just do the $n=3$ case as a warm-up:

Multiples of 3

Recall we start with \[\alpha(q) = {q\over (1-q)^2} = q + 2q^2 + 3q^3 + 4q^4 + \cdots\] Instead of computing $\alpha(q) + \alpha(-q)$, let's pick a cube root of unity, $\omega = e^{2\pi i/3}$, and compute (using the facts that $\omega^3 = 1$ and $1 + \omega + \omega^2 = 0$) \[\alpha(q) + \alpha(\omega q) + \alpha(\omega^2 q) = {}\] \[ (q + 2q^2 + 3q^3 + 4q^4 + \cdots) + {}\] \[ (\omega q + 2\omega^2q^2 + 3q^3 + 4\omega q^4 + \cdots) + {}\] \[ (\omega^2 q + 2\omega q^2 + 3q^3 + 4\omega^2 q^4 + \cdots)\] \[ = (1 + \omega + \omega^2)q + (1+\omega^2+\omega)2q^2 + (1+1+1)3q^3 + \cdots\] \[ = 9q^3 + 18q^6 + 27q^9 + \cdots\] \[ = 9\alpha(q^3) \] But now let's expand out $\alpha(\omega q)$ and $\alpha(\omega^w q)$ according to their definition: \[\alpha(q) + {\omega q \over (1-\omega q)^2} + {\omega^2 q \over (1-\omega^2 q)^2} = 9\alpha(q^3) \tag{*}\] Now observe that $(q-1)(q-\omega)(q-\omega^2) = q^3 - 1$ means \[(1-q)(1-\omega q)(1-\omega^2 q) = 1 - q^3\] and dividing both sides by $(1-q)$ we get \[(1-\omega q)(1-\omega^2 q) = 1 + q + q^2\] So now let's multiply both sides of $(*)$ by $(1-\omega q)^2(1-\omega^2 q)^2 = (1 + q + q^2)^2$ to clear denominators. \[\alpha(q)(1+q+q^2)^2 + \omega q (1 - \omega^2 q)^2 + \omega^2 q (1 - \omega q)^2 = 9\alpha(q^3)(1+q+q^2)^2\] We have to do a little more reasoning about $\omega$: observe that \[\omega q (1 - \omega^2 q)^2 + \omega^2 q (1 - \omega q)^2 =\omega q (1 - 2\omega^2 q + \omega q^2) + \omega^2 q (1 - 2\omega q + \omega^2 q^2)\] \[ = (\omega q - 2 q^2 + \omega^2 q^3) + (\omega^2 q - 2 q^2 + \omega q^3)\] \[ = (\omega+\omega^2) q - 4 q^2 + (\omega +\omega^2) q^3\] \[ = -(q + 4q^2 + q^3)\] Somewhat surprisingly, all appearances of $\omega$ can be eliminated. So now we know \[\alpha(q)(1+q+q^2)^2 - (q + 4q^2 + q^3) = 9\alpha(q^3)(1+q+q^2)^2\] Moving the negative polynomial in $q$ to the right, we get \[\alpha(q)(1+q+q^2)^2 = (q + 4q^2 + q^3) + 9\alpha(q^3)(1+q+q^2)^2\] And so we guess that there is a simple functional program realizing this isomorphism.

Already we can see that if we substitute $q=1$, we obtain \[9\alpha(1) = 6 + 81\alpha(1)\] which also tells us that $\alpha(1) = 6/(9-81) = -1/12$.

Multiples of $n$

To get the general case, we're going to engage in some generating-function shenanigans. Notice that we can define (See Epilog for how I obtained these apparently magical guesses!) \[\begin{align*} \beta(z, q) &= {z (1+zq)\over (1-zq)(1-zq^2)(1-z)}\\ \mu(z, q) &= {z^2 (1+zq)\over (1-zq)^3(1-zq^2)(1-z)}\\ \rho(z, q) &= {z(1+zq)\over (1-zq)^3} \end{align*} \] And expand $\mu, \beta, \rho$ as power series in $z$, yielding a sequence of finite polynomials in $q$:
\(\mu = \)\(\beta =\)\(\rho =\)
$z+{}$$z+{}$
$z^2 +{}$$z^2(1 + q)^2+{}$$4z^2q+{}$
$z^3(1 + 4q + q^2)+{}$$z^3(1 + q + q^2)^2+{}$$9z^3q^2+{}$
$z^4(1 + 4q + 10q^2 + 4q^3 + q^4)+{}$$z^4(1 + q + q^2 + q^3 )^2+{}$$16z^4q^3+{}$
$\cdots$$\cdots$$\cdots$

Notice that

Now we'll prove an easy identity that holds between these functions.

Lemma \[ \beta = (1-q)^2\mu + \rho\]

Proof: \[ \beta - (1-q)^2\mu = {z (1+zq)\over (1-zq)(1-zq^2)(1-z)} - {z^2 (1+zq)(1-q)^2 \over (1-zq)^3(1-zq^2)(1-z)}\] \[= {z (1+zq)(1-zq)^2 - z^2 (1+zq)(1-q)^2 \over (1-zq)^3(1-zq^2)(1-z)}\] \[= {z(1+zq)( (1-zq)^2 - z (1-q)^2) \over (1-zq)^3(1-zq^2)(1-z)}\] \[= {z(1+zq)(1-zq^2)(1-z) \over (1-zq)^3(1-zq^2)(1-z)}\] \[= {z(1+zq) \over (1-zq)^3}\] ∎

Now let's see what this equation tells us at the $z^n$ coefficient in particular. We have \[ [n]_q^2 = (1-q)^2M_n + n^2 q^{n-1}\] Multiply both sides by $q/(1-q)^2$: \[{q\over (1-q)^2} [n]_q^2 = qM_n + n^2 {q^{n}\over (1-q)^2}\] but $[n]_q = (1-q^n)/(1-q)$ so \[{1\over (1-q)^2} = {[n]_q^2\over (1-q^n)^2}\] which means \[{q\over (1-q)^2} [n]_q^2 = qM_n + n^2 {q^{n} [n]_q^2 \over (1-q^n)^2}\] that is,

\[\alpha(q) [n]_q^2 = qM_n + n^2 [n]_q^2 \alpha(q^n) \tag{**}\]

Conjecture: For all $n$, there is a functional program that realizes this equality as an isomorphism of types.

Getting -1/12 Again

We now want to set $q=1$. The $q$-deformed integer $[n]_q^2$ just becomes the regular integer $n^2$, but we need to evaluate $M_n$ at $q=1$. We look to its generating function, and find that we get $\mu(z,1) = z^2(1+z)/(1-z)^5$. This produces the sequence \[z^2 + 6z^3 + 20z^4 + 50z^5 + 105z^6 + 196z^7 + 336z^8 +\cdots\] which is A002415, the 4-d square pyramidal numbers, which are given by $n^2(n^2-1)/12$. So we find \[\alpha(1) n^2 = n^2(n^2-1)/12 + n^4 \alpha(1) \] \[\alpha(1) (n^2-n^4) = n^2(n^2-1)/12 \] \[\alpha(1) n^2(1-n^2) = n^2(n^2-1)/12 \] \[\alpha(1) = -1/12 \]

Epilog: Multiples of $n$, the Hard Way

 Okay, but how the heck did I come up with those magic generating functions? I arrived at them after already figuring out that $(**)$ was the equation I wanted by doing a bunch of experiments with complex-coefficient polynomials.

We start with $\alpha(q)$, and compute from the sum \[\sum_{i=0}^{n-1} \alpha(\zeta^i q) = \sum_{i=0}^{n-1} \sum_{t=0}^\infty t (\zeta^i q)^t\] \[= \sum_{i=0}^{n-1} \sum_{t=0}^\infty t \zeta^{it} q^t\] \[=\sum_{t=0}^\infty t q^t \sum_{i=0}^{n-1} \zeta^{it} \] \[=\sum_{t=0}^\infty t q^t \left(\begin{cases}n & \hbox{if $t\equiv 0\pmod n$;} \\ 0 &\hbox{otherwise.}\end{cases} \right)\] \[=\sum_{t=0}^\infty n^2t q^{nt} \] \[=n^2 \alpha(q^n) \] Now we single out the summand where $i=0$: \[\alpha(q) + \sum_{i=1}^{n-1} \alpha(\zeta^i q) = n^2 \alpha(q^n)\] and expand the definition of $\alpha$ in all summands except for $i=0$: \[\alpha(q) + \sum_{i=1}^{n-1} \left(\zeta^i q\over (1-\zeta^i q)^2\right) = n^2 \alpha(q^n) \tag{\dag}\] Let's now define \[ P_{ab\ldots}(n) = { 1-q^n \over (1-\zeta^{a}q)(1-\zeta^{b}q)\cdots }\] We will drop the $(n)$ when it is clear from context. Now multiply both sides of $(\dag)$ by $P_0^2$, to obtain \[\alpha(q) P_0^2 + q \sum_{i=1}^{n-1} \zeta^i P_{0i}^2 = n^2 P_0^2 \alpha(q^n) \tag{\ddag}\] Both $P_0^2$ and $-\sum_{i=1}^{n-1} \zeta^i P^2_{0i}$ turn out to be polynomials in $q$ with positive integer coefficients.

Lemma\[P_i = \sum_{j=0}^{n-1} q^j \zeta^{ij} \]

Proof: \[\left(\sum_{j=0}^{n-1} q^j \zeta^{ij}\right)(1-\zeta^i q) = \left(\sum_{j=0}^{n-1} q^j \zeta^{ij}\right) - \left(\sum_{j=0}^{n-1} q^{j+1} \zeta^{i(j+1)}\right)\] \[= \left(\sum_{j=0}^{n-1} q^j \zeta^{ij}\right) - \left(\sum_{j=1}^{n} q^j \zeta^{ij}\right) = 1 - q^n\zeta^{in} = 1- q^n\] ∎

In particular this means $P_0(n)$ is the $q$-integer $[n]_q = \sum_{j=0}^{n-1} q^j$.

Lemma \[ \sum_{j=0}^{n-1} \zeta^j P_j^2 = n^2 q^{n-1}\]

Proof: \[ \sum_{j=0}^{n-1} \zeta^j P_j^2 = \sum_{j=0}^{n-1} \zeta^j \left(\sum_{k=0}^{n-1} q^k \zeta^{jk} \right)^2\] \[= \sum_{j=0}^{n-1} \zeta^j \sum_{k_1=0}^{n-1} \sum_{k_2=0}^{n-1} q^{k_1+k_2} \zeta^{j(k_1 + k_2)} \] \[= \sum_{j=0}^{n-1} \zeta^j \left( \left(\sum_{p=0}^{n-2} (p+1)q^p\zeta^{jp} \right) + nq^{n-1}\zeta^{j(n-1)} + \left(\sum_{p=n}^{2n-2} (2n-p-1)q^p \zeta^{jp}\right) \right)\] \[= \left(\sum_{j=0}^{n-1} \sum_{p=0}^{n-2} (p+1)q^p\zeta^{j(p+1)} \right) + n^2q^{n-1} + \left(\sum_{j=0}^{n-1}\sum_{p=n}^{2n-2} (2n-p-1)q^p \zeta^{j(p+1)} \right)\] \[= \left( \sum_{p=0}^{n-2} (p+1)q^p\sum_{j=0}^{n-1} \zeta^{j(p+1)} \right) + n^2q^{n-1} + \left(\sum_{p=n}^{2n-2} (2n-p-1)q^p\sum_{j=0}^{n-1} \zeta^{j(p+1)} \right)\] \[ = n^2q^{n-1}\] ∎

Lemma \[\sum_{j=1}^{n-1} \zeta^j P^2_{0j} = {- [n]_q^2 + n^2q^{n-1} \over (1-q)^2} \]

Proof: \[\sum_{j=1}^{n-1} \zeta^j P^2_j =\sum_{j=1}^{n-1} \zeta^i P_{0j}^2 = {\sum_{j=1}^{n-1} \zeta^j P_j^2 \over (1-q)^2} = {- [n]_q^2 + \sum_{j=0}^{n-1} \zeta^j P_j^2 \over (1-q)^2} = {- [n]_q^2 + n^2q^{n-1} \over (1-q)^2}\] ∎

Recap

We've proven enough to show that $(\ddag)$ above, namely \[\alpha(q) [n]_q^2 + q \sum_{i=1}^{n-1} \zeta^i P_{0i}^2 = n^2 [n]_q^2 \alpha(q^n) \] is the same as
\[\alpha(q) [n]_q^2 = q\left( [n]_q^2 - n^2q^{n-1} \over (1-q)^2\right) + n^2 [n]_q^2 \alpha(q^n) \]

We've eliminated all appearances of $\zeta$, but we still need to check that we actually get positive integer coefficients when we divide by $(1-q)^2$ in order to even conjecture that there is an implementable bijection between types. If we define \[M_n = { [n]_q^2(n) - n^2q^{n-1} \over (1-q)^2}\] and inspect a few small examples, and their consecutive differences, we see:

$n$\(M_n\)\(M_n - M_{n-1}\)
$1$$0$
$2$$1$$1$
$3$$1 + 4q + q^2$ $4q + q^2$
$4$$1 + 4q + 10q^2 + 4q^3 + q^4$ $9q^2 + 4q^3 + q^4$
$5$$1 + 4q + 10q^2 + 20q^3 + 10q^4 + 4q^5 + q^6$ $16q^3 + 9q^4 + 4q^5 + q^6$

Looks like a clear pattern. The consecutive differences involve sums of consecutive square numbers.

Deriving the generating function $\mu$

This was the point at which I started trying to think in terms of generating functions, trying to find a nice expression for $\sum_{n} z^n M_n$. So if we wanted to find a $\mu$ such that \[z^{-2}\mu(z,q) = 1 + z(1 + 4q + q^2) + z^2(1 + 4q + 10q^2 + 4q^3 + q^4)+ \cdots\] then we could take differences by multiplying both sides by $(1-z)$: \[ (1-z)z^{-2}\mu(z,q) = 1 + z(4q + q^2) + z^2(9q^2 + 4q^3 + q^4) + \cdots\] and do some substitutions ($z \gets ab^2, q \gets b^{-1}$) to rearrange more perspicuously \[ (1-ab^2)a^{-2}b^{-4} \mu(ab^2,b^{-1}) = 1 + a(4b + 1) + a^2(9b^2 + 4b + 1) + \cdots\] Taking differences again by multiplying $(1-a)$, we get \[ (1-ab^2)(1-a)a^{-2}b^{-4}\mu(ab^2,b^{-1}) = 1 + 4ab + 9a^2b^2+ 16a^3b^3 + \cdots\] And we recognize the right-hand side as $h(ab)$ for \[ h(x) = 1 + 4x + 9x^2+ 16x^3 + \cdots\] for which it is easy to see (by hitting both sides of $1/(1-x) = 1 + x + x^2 + \cdots$ with the operator $D_x x D_x$) that \[ h(x) = {x+1\over (1-x)^3}\] therefore \[(1-ab^2)(1-a)a^{-2}b^{-4}\mu(ab^2, b^{-1}) = {1 + ab\over (1-ab)^3}\] and, reversing our substitutions $a \gets zq^2$ and $b \gets q^{-1}$, we find \[(1-z)(1-zq^2)\mu(z, q) = {1 + zq\over (1-zq)^3}\] so \[\mu(z, q) = {z^2(1 + zq)\over (1-zq^2)(1-zq)^3(1-z)}\]

Deriving the generating function $\beta$

I went through a similar process for $\beta(z,q)$. So my goal is to find a nice expression for \[\beta(z,q) = \sum_{n} z^n [n]_q^2 \] So I stare at \[\beta(z, q) = z + z^2(1 + q)^2 + z^3(1 + q + q^2)^2 + \cdots\] \[z^{-1}\beta(z, q) = 1 + z(1 + q)^2 + z^2(1 + q + q^2)^2 + \cdots\] \[ = 1 + z(1 + 2q + q^2) + z^2(1 + 2q + 3q^2 + 2q^3 + q^4) + \cdots\] Now take differences by multiplying $(1-z)$: \[z^{-1}(1-z)\beta(z, q) = 1 + z(2q + q^2) + z^2(2q^2 + 2q^3 + q^4) + z^3(2q^3 + 2q^4 + 2q^5 + q^6)+ \cdots\] \[= 1 + zq(2 + q) + (zq)^2(1 + 2q + q^2) + (zq)^3(2 + 2q + 2q^2 + q^3)+ \cdots\] Now do the substitution $z \gets a q^{-1}$: \[a^{-1}q(1-aq^{-1})\beta(aq^{-1}, q) = 1 + a(2 + q) + a^2(2 + 2q + q^2) + a^3(2 + 2q + 2q^2 + q^3)+ \cdots\] Take differences again, multiplying $(1-a)$: \[a^{-1}q(1-aq^{-1})(1-a)\beta(aq^{-1}, q) = 1 + a(1 + q) + a^2(q + q^2) + a^3(q^2 + q^3)+ \cdots\] Subtract 1 and divide by $a(1+q)$: \[{a^{-1}q(1-aq^{-1})(1-a)\beta(aq^{-1}, q)-1\over a(1+q)} = 1 + aq + a^2q^2 + a^3q^3+ \cdots\] Now this is recognizably \[{a^{-1}q(1-aq^{-1})(1-a)\beta(aq^{-1}, q)-1\over a(1+q)} = {1\over (1-aq)}\] So reverse the substitution, $a \gets zq$: \[{z^{-1}(1-z)(1-zq)\beta(z, q)-1\over zq(1+q)} = {1\over (1-zq^2)}\] The remainder is mere algebra: \[{z^{-1}(1-z)(1-zq)\beta(z, q)-1 } = {zq(1+q)\over (1-zq^2)}\] \[{z^{-1}(1-z)(1-zq)\beta(z, q) } = {zq(1+q) + (1-zq^2)\over (1-zq^2)}\] \[{\beta(z, q) } = {z^2q(1+q) + z(1-zq^2)\over (1-zq^2)(1-z)(1-zq)}\] \[ = {z^2q + z^2q^2 + z-z^2q^2\over (1-zq^2)(1-z)(1-zq)}\] \[ = {z^2q + z\over (1-zq^2)(1-z)(1-zq)}\] \[\beta(z,q) = {z(1+zq)\over (1-zq)(1-zq^2)(1-z)}\]

Appendix: One More 12-ish Phenomenon

Let's take another look at \[ x^2(1+x)/(1-x)^5 = x^2 + 6x^3 + 20x^4 + 50x^5 + 105x^6 + 196x^7 + 336x^8 +\cdots\] This is allegedly $\sum_n x^n (n^4 - n^2)/12$, so we should find that \[{12x^2(1+x)\over (1-x)^5} + \sum_n x^n n^2 = \sum_n x^n n^4\] We can mechanically find that \[\sum_n x^n n^2 = (xD)^2 {1\over 1-x} = {x(x+1) \over (1-x)^3}\] \[\sum_n x^n n^4 = (xD)^4 {1\over 1-x} = {x(x^3+11x^2+11x+1) \over (1-x)^5}\] So it should be the case that \[{12x^2(1+x)\over (1-x)^5} + {x(1+x)\over (1-x)^3} = {x(1+11x+11x^2+x^3) \over (1-x)^5}\] And indeed it is: \[{12x^2(1+x)\over (1-x)^5} + {x(1+x)\over (1-x)^3} = {12x^2(1+x) + x(1+x)(1-x)^2\over (1-x)^5}\] \[= {12x^2+12x^3 + x-x^2-x^3+x^4\over (1-x)^5}\] \[= {x(1+11x+11x^2+x^3) \over (1-x)^5}\]

Another Interpretation

For any number $p$ and type $\tau$, let $R_p(\tau)$ be the dependent sum type $(n:\N) \x \tau^n \x n^p$. That is, an element of $R_p(\tau)$ consists of a tuple of $\tau$s of some finite length, and a choice of $p$ pointers into that tuple. Claim: there is an isomorphism
\[(12, \tau,\tau?, [\tau], [\tau], [\tau], [\tau], [\tau]) + R_2(\tau) \cong R_4(\tau)\]
where $\tau?$ is $\tau + 1$ and $[\tau]$ is lists of $\tau$ and $(\cdots,\cdots)$ is tuple formation.