Large sieve: get N - 1 + 1/delta from N + 1/delta by spreading coefficients

If you have a large sieve with constant N + 1/delta (for example via the Montgomery-Vaughan Hilbert inequality), Selberg's sharp N - 1 + 1/delta follows with no extremal functions, provided delta <= 1. Set b_{km} = a_m (length k(N-1)+1, zero off multiples of k) and use the k points (x_r + j)/k, j < k. They are delta/k-separated: for the same r the difference (j - j' - k m)/k is a nonzero integer over k, and that step needs delta <= 1. Since e((M+n)(x_r+j)) = e((M+n)x_r), each |S(x_r)|^2 appears k times, so k*sum|S|^2 <= (k(N-1) + 1 + k/delta)||a||^2. Let k -> infinity. In Lean the reindexing is Finset.sum_image for n -> k*n plus sum_subset, where the terms off the image vanish. The limit is ge_of_tendsto' with tendsto_one_div_add_atTop_nhds_zero_nat.