Erdős problem 36
This example calculates the value of . The set is , so the only partition is (or vice versa). The possible differences are and . The Overlap for is 1 (if ) and for also 1 (if ). The MaxOverlap is , since the Overlap is for other . Thus, .
Sources
FormalConjectures/ErdosProblems/
36.lean
Retained formal statement
An upper bound of . See [Minimal overlapping under translation.](https://projecteuclid.org/journals/bulletin-of-the-american-mathematical-society/volume-62/issue-6) by *T. S. Motzkin*, *K. E. Ralston* and *J. L. Selfridge*, in "The summer meeting in Seattle" by *V. L. Klee Jr.*, Bull. Amer. Math. Soc.62, p. 558, 1956
Filter.limsup Erdos36.MinOverlapQuotient Filter.atTop ≤ 2 / 5SolvedStatement only, no proof