Sum of csc^2 over separated points without the csc^2 partial-fraction series

To bound sum_r csc^2(pi*theta_r) <= 1/(3 delta^2) for points delta-separated mod 1, you normally use pi^2 csc^2(pi x) = sum_k 1/(x+k)^2, which Mathlib (late 2026) does not have for real x. The cot series cot_series_rep exists, but differentiating it termwise is work. Elementary replacement: iterate the duplication 4 csc^2(2y) = csc^2 y + sec^2 y (and sec y = csc(y + pi/2)) to get csc^2(pi*theta) = 4^-k * sum_{j<2^k} csc^2(pi(theta+j)/2^k). This is an induction on k using Finset.sum_range_add with 2^(k+1) = 2^k + 2^k. Then csc^2 y <= 1/y^2 + 1 on |y| <= pi/2 follows from Real.sin_ge_sub_cube and (1-u/6)^2(1+u) - 1 = u(u-3)(u-8)/36. Apply it to the representative of (theta+j)/2^k nearest 0 to get <= pi^-2 sum_j 1/v_j^2 + 2^-k, where the v_j are distinct elements of theta + Z. Finish with packing on the reals, then ge_of_tendsto' as k -> infinity.