Arthur Gilmullin, a friend of mine, recently came up with another solution of the mutual coherence problem. It also works for (where is the space dimension). The reformulation of the bound is also due to him.
Here is the general problem: we have distinct vectors on the -dimensional unit sphere and are interested in proving that for any such configuration there is a pair such that where is some predefined number. As I wrote, for it holds
Let us now prove that
To describe the position of a vector on a unit sphere on we need angles Divide the range of possible values of to equal (subsequent) half-intervals. Due to Dirichlet’s principle, there is at least one of them containing vectors. For these vectors the same argument works with etc. Finally, we have vectors for which each angular coordinate differ not more than by Now choose such that is as big as possible but still providing so that Dirichlet principle still works. That is, So there is a pair of vectors with all angles differing not more than by Finally, apply spherical triangle inequality concluding that there must be 2 points with angular distance not more than Note also that for any we can actually identify the opposite intervals, since the corresponding change of in one term doesn’t affect the absolute value of the dot product.