Hilbert's inequality for 1/(m-n) in Lean without Parseval: sawtooth symbol on [0,1], and Lean's 1/0 = 0 handles the diagonal

Goal: |∑_{m∈s}∑_{n∈t} a_m b_n/(m-n)| ≤ π‖a‖₂‖b‖₂ for finite s, t ⊆ ℤ (HLP Thm 294), with the sharp constant π.

Route: work on the real interval [0,1] with e_k(x) = Complex.exp (2*π*I*k*x). Avoid AddCircle and the L² Fourier API entirely. (1) ∫₀¹ e_k = [k=0]: integral_exp_mul_complex + Complex.exp_int_mul_two_pi_mul_I. The term 2*π*I*k*x parses as (2*π*I*k) * x, so it matches c * ↑x directly. (2) ψ(x) = 2πi(x-1/2) has ∫₀¹ ψ e_k = 1/k. Use the antiderivative ((x-1/2)/c - 1/c²)e^{cx} and integral_eq_sub_of_hasDerivAt. Write the derivative via (hasDerivAt_id x).ofReal_comp, then convert … using 1; field_simp; ring. At k = 0 the integral is 0, and in Lean 1/(0:ℂ) = 0, so the statement = 1/(k:ℂ) holds uniformly. The diagonal m = n of ∑∑ a b/(m-n) also vanishes by div_zero, so no m ≠ n side condition is needed anywhere. (3) ∑∑ a_m b_n/(m-n) = ∫₀¹ ψ A conj(B), and ∫|A|² = ∑a² by expanding the double finite sum. Use Complex.mul_conj' to get z*conj z = ‖z‖^2, then pass to ℂ via intervalIntegral.integral_ofReal and Complex.ofReal_injective. (4) |ψ| ≤ π and 2|A||B| ≤ |A|²+|B|² give (π/2)(‖a‖²+‖b‖²). Get the product form by scaling a ↦ τa, b ↦ b/τ with τ² = β/α, treating α = 0 or β = 0 separately. Sharpness: put a on m ≥ 1 and b on n ≤ -1, so that m - n = m'+n'+2, and reuse a sharpness proof for the kernel 1/(m'+n'+2). To cut an ℝ≥0∞ double tsum to a finite square: rw [← ENNReal.tsum_prod, ENNReal.tsum_eq_iSup_sum] at h, lt_iSup_iff, then Finset.sum_le_sum_of_subset into range N ×ˢ range N. Gotcha (again): intervalIntegral.integral_finsetSum and integral_add fail to rewrite when the integrand is built with .mul or .pow, because they produce Pi-products (f * g) x. Pass (f := fun m x ↦ …) explicitly.