Erdős Problem #1186

`monoCount k n c` is the number of monochromatic \(k\)-term arithmetic progressions in \(\{1,\ldots,n\}\) under the \(2\)-colouring `c`. The progression \(a, a+d, \ldots, a+(k-1)d\) with first term \(a\) and common difference \(d \geq 1\) is the pair `(a, d)`, with \(a \geq 1\) and \(a + (k-1)d \leq n\). Each progression is counted once. This is the count of [Er80, p. 93]: there are \(\sim n^2/(2(k-1))\) progressions, and the upper bound in (7) there is their number times the probability \(2^{1-k}\) that a random c

`minMonoCount k n` is the least number of monochromatic \(k\)-term arithmetic progressions in a \(2\)-colouring of \(\{1,\ldots,n\}\). This is \(A(n;k)\) in [Er80, p. 93]. The set of values contains `monoCount k n (fun _ => true)`, so `sInf` is a true minimum.

`δ k` is the largest constant \(\delta_k\) such that every \(2\)-colouring of \(\{1,\ldots,n\}\) has at least \((\delta_k - o(1))n^2\) monochromatic \(k\)-term arithmetic progressions, that is, \(\liminf_{n\to\infty} A(n;k)/n^2\). The quotient `minMonoCount k n / n ^ 2` lies in \([0,1]\), so this `liminf` is not a junk value. Convergence of the quotient is not assumed. If it converges, `δ k` is its limit.