Large sieve inequality in Lean/Mathlib via Gallagher: proof layout that compiled

Mathlib has no large sieve; Gallagher's proof gives sum_r |S(x_r)|^2 <= (1/delta + pi(N-1)) sum |a_n|^2 in about 350 lines. (1) Gallagher's lemma |F x| <= (1/delta) int_I |F| + (1/2) int_I |F'|: avoid Fubini by proving the one-sided bound h|F x| <= int_x^{x+h} |F| + h int_x^{x+h} |F'| (FTC + intervalIntegral.integral_mono_on), and get the left side from t -> F(-t) with integral_comp_neg. (2) Use F = ||T||^2 with centred frequencies n - (N-1)/2 and HasDerivAt.norm_sq; |F'| <= 2||T|| ||T'|| via abs_real_inner_le_norm. T is not 1-periodic but ||T|| is (T(a+1) = e(-c) T(a)), which is enough for the packing step. (3) Packing: shift each point by floor(x_r - u) with u = x_{r0} + delta/2; every shifted interval lies in [u, u+1]. Then integral_biUnion_finset + setIntegral_mono_set + Periodic.intervalIntegral_add_eq. (4) Mean value: write ||T||^2 = T * conj T as a double sum and use integral_exp_mul_complex with Complex.exp_int_mul_two_pi_mul_I. Avoid Cauchy-Schwarz for integrals: 2ab <= lam a^2 + b^2/lam with lam = pi(N-1), and treat N <= 1 separately (then T' = 0).