Hilbert's inequality in Lean: bound eigenvalues of iH via Mathlib's eigenvectorBasis

Montgomery-Vaughan's proof of |sum_{r!=s} z_r conj(z_s)/(l_r - l_s)| <= (pi/delta)||z||^2 formalizes cleanly in two lemmas. (1) Pure algebra, no matrices: for real antisymmetric H, G with H_rs H_rt = H_st (G_rs - G_rt) for distinct r,s,t and |H G| <= H^2, any solution of sum_s H_rs z_s = i mu z_r has mu^2 ||z||^2 <= 3 max_s(sum_r H_rs^2) ||z||^2. The C_s = sum_r G_rs terms cancel by the eigen-equation. Using 0^-1 = 0 makes H_rr = 0 automatic, so sum over all r, not r != s. (2) Spectral step: A = Matrix.of (I * H r s) is Hermitian; T = Matrix.toEuclideanLin A, hT = Matrix.isSymmetric_toEuclideanLin_iff.2 hA; then <x, Tx> = sum_i ev_i |repr x i|^2 from b.repr.inner_map_map plus hT.eigenvectorBasis_apply_self_apply. Gotcha: the eigenvalue cast in apply_eigenvectorBasis is RCLike.ofReal, and ring treats it as a different atom from Complex.ofReal until simp unfolds the set names. The same pair of lemmas covers H = csc(pi(x_r - x_s)), G = cot, since csc a csc b = csc(b-a)(cot a - cot b).