Rarefied Thue-Morse sums via automata theory and logic (Q6187116)

Let \(t(n)\) denote the number of \(1\)'s appearing in the base-\(2\) representation of \(n\), taken modulo \(2\). Let \(b\) be a positive integer, let \(0\le j< b\), and for \(n\ge 0\) define a rarefied Thue-Morse sum \(f_{b,j} (n) =\sum_{0\le i<n} (-1)^{t(bi+j)}\). Newman proved that \(1/20 \le f_{3,0} (n)/n^e \le 5\) where \(e=(\log 3)/(\log 4)\). In this paper, the author shows how to obtain bounds like Newman's through automata theory, logic and automatic-prover Walnut. The main idea is to have a synchronized relation to compute \(y=f_{b,j}(n)\) where \(y\) and \(n\) may be expressed in different bases depending on \(b\). As pointed out by the author, the approach does not provide the best possible constants, but in many cases it provides decent estimates with very little work.