Automated part of the Allouche-Zeilberger paper

Note: This is a Plain TeX draft that will be incorporated in the main paper written in LaTex. Only for the use of J. -P. Allouche Automated proofs of Specific Finite Trigonometric Identities Given a multivariable polynomial P, any identity of the form,

P (sin( \frac{π}{n} ) , sin( \frac{2 π}{n} ), …, sin( \frac{(n − 1) π}{n} )) = 0 ,  (1)

for a specific, positive integer n, is routinely provable by Maple, and (probably) any other computer algebra system. In Maple the command is simplify. For example the original ‘Morrie’s law’[4], that Richard Feynman never forgot (also see [1])

cos(20^{o}) cos(40^{o}) cos(80^{o}) = \frac{1}{8} ,

can be automatically done (exactly!) by Maple. Just type

simplify(cos(Pi/9)*cos(2*Pi/9)*cos(4*Pi/9));

and you will get right away 1/8. Nowadays you don’t have to be a Gauss to (rigorously!) prove Gauss’ identity at the beginning of this article, just enter, in Maple

simplify((-1+sqrt(17)+sqrt(34-2*sqrt(17))+2*sqrt(17+3*sqrt(17)-sqrt(170+38*sqrt(17))))/16-
cos(2*Pi/17));

and in one nano-second you would get 0. To take another example, to prove the second identity on page 1, type

sin(3/7*Pi)**2/sin(2/7*Pi) - sin(2/7*Pi)**2/sin(1/7*Pi) + sin(1/7*Pi)**2/sin(3/7*Pi):
simplify(%); ,

and you would immediately get 0. The way Maple does it is to use Euler’s formula

sin x = \frac{e^{ix} − e^{−ix}}{2i} .

Then in (1) everything is a polynomial in z := e^{iπ/n}, getting, upon expansion, a polynomial in z and making sure that it is divisible by z^{n} +1. So numeric computations turn into routine, symbolic, ‘high-school algebra’ calculations that computer algebra systems excel at. Nine such identities are proved, by ‘advanced’ methods in [2]. See the output file

http://www.math.rutgers.edu/~zeilberg/tokhniot/oTrigSums14.txt ,

for automatic, elementary (high-school algebra) proofs of all of them. Automated Proofs of Infinite Families of Finite Trigonometric Sums More interesting are “infinite families” of finite trigonometric sums. We will describe how to automatically derive explicit polynomial expressions to the following eight families. Below n and k are arbitrary positive integers. Type Top

∑_{j=1}^{n} sin^{2k}(\frac{j π}{2n + 1}) .

Type Ton

∑_{j=1}^{n} csc^{2k}(\frac{j π}{2n + 1}) .

Type Tep

∑_{j=1}^{n} sin^{2k}(\frac{(2j − 1) π}{4n}) .

Type Ten

∑_{j=1}^{n} csc^{2k}(\frac{(2j − 1) π}{4n}) .

Type Uop

∑_{j=1}^{n−1} sin^{2k}(\frac{j π}{2n}) .

Type Uon

∑_{j=1}^{n−1} csc^{2k}(\frac{j π}{2n}) .

Type Uep

∑_{j=1}^{n} sin^{2k}(\frac{(2j − 1) π}{4n + 2} ) .

Type Uen

∑_{j=1}^{n} csc^{2k}(\frac{(2j − 1) π}{4n + 2} ) .

It turns out that to get closed-form expressions for general n and k for the four types Top,Tep,Uop, Uep, (i.e. for sums of positive even powers of the sines), one does not need computers. These are easy human exercises. Let’s just illustrate it with type Top.

Define z := e^{\frac{iπ}{2n+1}} . Note that z^{2n+1} = −1. Then sin(\frac{j π}{2n+1}) = (z^{j} − z^{−j})/(2i). We have:

∑_{j=1}^{n} sin^{2k}(\frac{j π}{2n + 1}) = ∑_{j=1}^{n} ((z^{j} − z^{−j})/(2i))^{2k} = \frac{(−1)^{k}}{4^{k}} ∑_{j=1}^{n}(z^{j} − z^{−j})^{2k} .

By the binomial theorem, this equals

\frac{(−1)^{k}}{4^{k}} ∑_{j=1}^{n} ∑_{r=0}^{2k}(−1)^{r} \frac{(2k)!}{r!(2k − r)!}z^{−jr+j(2k−r)} = \frac{(−1)^{k}}{4^{k}} ∑_{j=1}^{n} ∑_{r=0}^{2k}(−1)^{r} \frac{(2k)!}{r!(2k − r)!}z^{2j(k−r)}

= \frac{(−1)^{k}}{4^{k}} · n · (−1)^{k} \frac{(2k)!}{k!^{2}} + \frac{(−1)^{k}}{4^{k}} ∑_{j=1}^{n} ∑_{r=0}^{k−1}(−1)^{r} \frac{(2k)!}{r!(2k − r)!}(z^{2j(k−r)} + z^{−2j(k−r)})

= \frac{n}{4^{k}} \frac{(2k)!}{k!^{2}} + \frac{(−1)^{k}}{4^{k}} ∑_{r=0}^{k−1}(−1)^{r} \frac{(2k)!}{r!(2k − r)!} ∑_{j=1}^{n}(z^{2j(k−r)} + z^{−2j(k−r)}) .

Note that, by summing the geometric series and using z^{2(2n+1)} = 1, we have:

∑_{j=1}^{n}(z^{2j(k−r)} + z^{−2j(k−r)}) = ∑_{j=−n}^{n}(z^{2(k−r)})^{j} − 1 = 0 − 1 = −1 .

Going back to the above, we have that our desired sum equals

= \frac{n}{4^{k}} \frac{(2k)!}{k!^{2}} + \frac{(−1)^{k+1}}{4^{k}} ∑_{r=0}^{k−1}(−1)^{r} \frac{(2k)!}{r!(2k − r)!} .

But (you prove it!)

∑_{r=0}^{k−1}(−1)^{r} \frac{(2k)!}{r!(2k − r)!} = \frac{1}{2}(−1)^{k+1} \frac{(2k)!}{k!^{2}} .

We have just proved, sans ordinateurs, the general identity.

Theorem Top:

∑_{j=1}^{n} sin^{2k}(\frac{j π}{2n + 1}) = \frac{1}{4^{k}} \frac{(2k)!}{k!^{2}} (n + \frac{1}{2}) .

Similar things can be done with the other three positive families, and they are left to the reader. Theorem Tep:

∑_{j=1}^{n} sin^{2k}(\frac{(2j − 1) π}{4n}) = \frac{n}{2^{2k−1}} \frac{(2k − 1)!}{(k − 1)!k!} .

Theorem Uop:

∑_{j=1}^{n−1} sin^{2k}(\frac{j π}{2n}) = \frac{n}{4^{k}} \frac{(2k)!}{k!^{2}} − \frac{1}{2} .

Theorem Uep:

∑_{j=1}^{n} sin^{2k}(\frac{(2j − 1) π}{4n + 2} ) = \frac{n}{4^{k}} \frac{(2k)!}{k!^{2}} + \frac{1}{4^{k}} \frac{(2k − 1)!}{k!(k − 1)!} − \frac{1}{2} .

Note that in the above four theorems we have closed-form expressions for general n and general k. Much more interesting is to derive expressions for the sum of the even powers of the cosecants (i.e. reciprocals of the sines). In this case there does not seem to be a general formula for n and k, but for each specific k, one can get an explicit expression, as a polynomial in n of degree 2k, for any desired k. We went as far as k ≤ 60, but readers are welcome to use our accompanying Maple package TrigSums.txt, available from the front of this article

https://sites.math.rutgers.edu/~zeilberg/mamarim/mamarimhtml/trig.html ,

to get as far as one wishes. We will illustrate it with the family of type Ton. Recall that the Chebyshev polynomial of the first kind, T_{n}(x) may be defined by

T_{n}(cos t) = cos(nt) .

It is well-known and easy to see [3], that

T_{n}(x) = \frac{n}{2} ∑_{k=0}^{⌊ \frac{n}{2} ⌋} \frac{(−1)^{k}2^{n−2k}(n − k − 1)!}{k!(n − 2k)!}x^{n−2k} .

Hence

\frac{T_{2n+1}(x)}{x} = (2n + 1) ∑_{k=0}^{n} \frac{(−1)^{k}4^{n−k}(2n − k)!}{k!(2n + 1 − 2k)!}(x^{2})^{n−k} .

Define the degree n polynomial

E_{n}(x) := \frac{T_{2n+1}(\sqrt{x})}{\sqrt{x}} .

Then

E_{n}(x) = (2n + 1) ∑_{k=0}^{n} \frac{(−1)^{k}4^{n−k}(2n − k)!}{k!(2n + 1 − 2k)!}x^{n−k} .

Note that the n roots of E_{n}(x) are sin^{2}(\frac{j π}{2n+1}), for j = 1, …, n. Define the reciprocal polynomial Ē_{n}(x) := x^{n}E_{n}(x^{−1}). Then we have

Ē_{n}(x) = (−1)^{n} (2n + 1) ∑_{k=0}^{n} \frac{(−1)^{k}4^{k}(n + k)!}{(n − k)!(2k + 1)!}x^{n−k} .

Note that the n roots of Ē_{n}(x) are csc^{2}(\frac{j π}{2n+1}). It follows immediately that, denoting, as usual, the degree k elementary symmetric function of of α_{1}, …, α_{n} by e_{k}(α_{1}, …, α_{n}), that Lemma Top:

e_{k}(\{sin^{2}(j π/(2n + 1), j = 1 … n)\}) = \frac{4^{−k} (2n − k)! (2n + 1)}{k! (2n − 2k + 1)!}

Lemma Ton:

e_{k}(\{csc^{2}(j π/(2n + 1)), j = 1 … n)\}) = \frac{(n + k)!4^{k}}{(n − k)! (2k + 1)!} .

Now we use Newton’s identities [5] (see [6] for a lovely combinatorial proof). Let

p_{k}(α_{1}, …, α_{n}) := ∑_{j=1}^{n} α_{j}^{k}

be the power-sum functions, then

ke_{k}(α_{1}, …, α_{n})) = ∑_{i=1}^{k}(−1)^{i−1}e_{k−i}(α_{1}, …, α_{n})p_{i}(α_{1}, …, α_{n}) .

This enables us (and our computers) to recursively find explicit expressions for the power sums of both {sin^{2}(j π/(2n + 1)), j = 1 … n)} and {csc^{2}(j π/(2n + 1)), j = 1 … n)}. Of course, for the former case we don’t need it, since we have Theorem Top above but it is still nice to know that it agrees up to k = 60. For types Tep and Ten, the underlying polynomial is T_{2n}(\sqrt{x}) whose roots are

{sin^{2}((2j + 1)π/(4n)), j = 1 … n)} ,

and we have, analogously Lemma Tep:

e_{k}(\{sin^{2}((2j + 1) π/(4n)), j = 1 … n\}) = \frac{2n 4^{−k} (2n − k − 1)!}{k! (2n − 2k)!} .

Lemma Ten:

e_{k}(\{csc^{2}((2j + 1) π/(4n)), j = 1 … n\}) = \frac{n (n + k − 1)!4^{k}}{(n − k)! (2k)!} .

For types Uop and Uon, the underlying polynomial is U_{2n−1}(\sqrt{x})/\sqrt{x} whose roots are

{sin^{2}(jπ/(2n)), j = 1 … n − 1)}

and we have, analogously Lemma Uop:

e_{k}(\{sin^{2}(j π/(2n)), j = 1 … n − 1\}) = \frac{4^{−k} (2n − k − 1)!}{(2n − 2k − 1)!k!} .

Lemma Uon:

e_{k}(\{csc^{2}(j π/(2n)), j = 1 … n − 1\}) = \frac{4^{k} (n + k)! (n − 1)!}{(2k + 1)! (n − k − 1)!n!} .

For types Uep and Uen, the underlying polynomial is U_{2n}(\sqrt{x}) whose roots are

{sin^{2}((2j − 1)π/(4n + 2), j = 1 … n)} ,

and we have, analogously Lemma Uep:

e_{k}(\{sin^{2}((2j − 1) π/(4n + 2)), j = 1 … n\}) = \frac{4^{−k} (2n − k)!}{(2n − 2k)!k!} ,

Lemma Uen:

e_{k}(\{csc^{2}((2j − 1) π/(4n + 2)), j = 1 … n\}) = \frac{(n + k)!4^{k}}{(2k)! (n − k)!} .

From these, combined with Netwon’s identities one can find as many sum-of-powers as one wishes. Appendix by Shalosh B. Ekhad Type Ton Proposition Ton[1]

∑_{j=1}^{n} csc^{2}(\frac{πj}{2n + 1}) = \frac{2 (n + 1) n}{3} .

Proposition Ton[2]

∑_{j=1}^{n} csc^{4}(\frac{πj}{2n + 1}) = \frac{8 (n + 1) n (n^{2} + n + 3)}{45}

Proposition Ton[3]

∑_{j=1}^{n} csc^{6}(\frac{πj}{2n + 1}) = \frac{8 (n + 1) n (8n^{4} + 16n^{3} + 35n^{2} + 27n + 54)}{945} .

Proposition Ton[4]

∑_{j=1}^{n} csc^{8}(\frac{πj}{2n + 1}) = \frac{128 (n + 1) n (n^{2} + n + 3) (3n^{4} + 6n^{3} + 7n^{2} + 4n + 15)}{14175} .

Proposition Ton[5]

∑_{j=1}^{n} csc^{10}(\frac{πj}{2n + 1}) = \frac{64 (n + 1) n (16n^{8} + 64n^{7} + 182n^{6} + 322n^{5} + 493n^{4} + 524n^{3} + 579n^{2} + 360n + 540)}{93555} .

For Propositions Ton[k] for 6 ≤ k ≤ 50, see the output file

https://sites.math.rutgers.edu/~zeilberg/tokhniot/oTrigSums1.txt .

Type Ten Proposition Ten[1]

∑_{j=1}^{n} csc^{2}(\frac{π(2j − 1)}{4n}) = 2 n^{2} .

Proposition Ten[2]

∑_{j=1}^{n} csc^{4}(\frac{π(2j − 1)}{4n}) = \frac{4n^{2} (2n^{2} + 1)}{3} .

Proposition Ten[3]

∑_{j=1}^{n} csc^{6}(\frac{π(2j − 1)}{4n}) = \frac{8n^{2} (8n^{4} + 5n^{2} + 2)}{15} .

Proposition Ten[4]

∑_{j=1}^{n} csc^{8}(\frac{π(2j − 1)}{4n}) = \frac{16n^{2} (136n^{6} + 112n^{4} + 49n^{2} + 18)}{315} .

Proposition Ten[5]

∑_{j=1}^{n} csc^{10}(\frac{π(2j − 1)}{4n}) = \frac{32n^{2} (992n^{8} + 1020n^{6} + 546n^{4} + 205n^{2} + 72)}{2835} .

For Propositions Ten[k] for 6 ≤ k ≤ 50, see the output file

https://sites.math.rutgers.edu/~zeilberg/tokhniot/oTrigSums5.txt .

Type Uon Proposition Uon[1]

∑_{j=1}^{n−1} csc^{2}(\frac{j π}{2n}) = \frac{2 (n + 1) (n − 1)}{3} .

Proposition Uon[2]

∑_{j=1}^{n−1} csc^{4}(\frac{j π}{2n}) = \frac{4 (n + 1) (n − 1) (2n^{2} + 7)}{45} .

Proposition Uon[3]

∑_{j=1}^{n−1} csc^{6}(\frac{j π}{2n}) = \frac{8 (n + 1) (n − 1) (8n^{4} + 29n^{2} + 71)}{945} .

Proposition Uon[4]

∑_{j=1}^{n−1} csc^{8}(\frac{j π}{2n}) = \frac{16 (n + 1) (n − 1) (24n^{6} + 104n^{4} + 251n^{2} + 521)}{14175} .

Proposition Uon[5]

∑_{j=1}^{n−1} csc^{10}(\frac{j π}{2n}) = \frac{32 (n + 1) (n − 1) (32n^{8} + 164n^{6} + 450n^{4} + 901n^{2} + 1693)}{93555} .

For Propositions Uon[k] for 6 ≤ k ≤ 50, see the output file

https://sites.math.rutgers.edu/~zeilberg/tokhniot/oTrigSums9.txt .

Type Uen Proposition Uen[1]

∑_{j=1}^{n} csc^{2}(\frac{(2j − 1) π}{4n + 2} ) = 2 (n + 1) n .

Proposition Uen[2]

∑_{j=1}^{n} csc^{4}(\frac{(2j − 1) π}{4n + 2} ) = \frac{8 (n + 1) n (n^{2} + n + 1)}{3} .

Proposition Uen[3]

∑_{j=1}^{n} csc^{6}(\frac{(2j − 1) π}{4n + 2} ) = \frac{8 (n + 1) n (8n^{4} + 16n^{3} + 19n^{2} + 11n + 6)}{15} .

Proposition Uen[4]

∑_{j=1}^{n} csc^{8}(\frac{(2j − 1) π}{4n + 2} ) = \frac{128 (n + 1) n (n^{2} + n + 1) (17n^{4} + 34n^{3} + 31n^{2} + 14n + 9)}{315} .

Proposition Uen[5]

∑_{j=1}^{n} csc^{10}(\frac{(2j − 1) π}{4n + 2} )

= \frac{64 (n + 1) n (496n^{8} + 1984n^{7} + 4106n^{6} + 5374n^{5} + 4979n^{4} + 3316n^{3} + 1669n^{2} + 576n + 180)}{2835} .

For Propositions Uen[k] for 6 ≤ k ≤ 50, see the output file

https://sites.math.rutgers.edu/~zeilberg/tokhniot/oTrigSums12.txt .

References

[1] J. Louck, W. Beyer, and D. Zeilberger, A generalization of a curiosity that Feynman remembered all his life, ‘Math Bite’, Math. Magazine, 69(1)(Feb. 1996), 43-44.

https://sites.math.rutgers.edu/~zeilberg/mamarim/mamarimhtml/feynman.html

[2] G. Vinay, H. T. Shwetha and K. N. Harshitha, Non-trivial trigonometric sums arising from some of Ramanujan Theta function identities, Palestinian J. Mathematics 11(1)(2022), 130-134.

[3] The Wikipedia Foundation, Chebyshev polynomials.

[4] The Wikipedia Foundation, Morrie’s Law .

[5] The Wikipedia Foundation, Newton’s identities.

[6] D. Zeilberger, A combinatorial proof of Newton’s identities, Discrete Mathematics 49 (1984), 319.

https://sites.math.rutgers.edu/~zeilberg/mamarimY/DZ1984.pdf