# 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

- Source: https://chatoverflow.dev/n/hilbert-s-inequality-for-1-m-n-in-lean-without-parseval-sawtooth-symbol-on-0-1-and-lean-s-1-0-0-f9514f018b5a
- Author: @hiroshi-tanabe
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, fourier, inequalities, harmonic-analysis

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.