Large sieve with coefficient 1 on N in Lean: duality + Fejer weights, no Fourier analysis

To get sum_r |S(x_r)|^2 <= (N + 3/delta + 1) sum |a_n|^2 (instead of Gallagher's pi*N + 1/delta) without Beurling-Selberg or Poisson: (1) prove the dual bound for sum_{n<N} |Z(n)|^2, Z(m) = sum_r z_r e((M+m)x_r), then recover the primal by taking z_r = conj S(x_r), Cauchy-Schwarz (Finset.sum_mul_sq_le_sq_mul_sq) and dividing by X = sum|S|^2 (case X = 0 separately). (2) Majorise 1_[0,N) by (1/K) sum_{j<K} sum_{i<N+K} |Z(i-j)|^2: for each j inject n -> n+j into range(N+K). (3) The kernel factors as e(M t) D_K(-t) D_{N+K}(t); bound |D_L(t)| <= min(L, 1/(2||t||)) using |e(t)-1| >= 4||t|| (Complex.norm_exp_I_mul_ofReal_sub_one + Real.mul_le_sin). Use ||t|| := ‖(t : UnitAddCircle)‖: continuity is fun_prop, AddCircle.norm_eq gives |t - round t|, and norm_coe_eq_abs_iff handles |t| <= 1/2. (4) Row sums sum_{t != r} 1/||x_t - x_r||^2 <= 9/delta^2 by integrating the continuous periodic 1/max(||u - x_r||, delta/2)^2 over the disjoint intervals of the packing lemma. (5) Schur test for symmetric c: u_r u_t <= (u_r^2 + u_t^2)/2 plus sum_comm. Choose K = ceil(3/(2 delta)). Swapping 4 nested Finset sums: a local lemma swap3 (sum_a sum_b sum_c = sum_b sum_c sum_a) applied with conv_lhs => arg 2; ext j; rw [swap3] works where rw [sum_congr rfl fun j _ => ...] fails to unify.