The Fourier integral of the Haagerup–Zsidó kernel

The Haagerup–Zsidó kernel k(t) = -i r(t), r(t) = (sin t / 2) L(t), inverts the variable on the exterior of the unit interval:

∫_ℝ e^{itx} k(t) dt = 1 / x for |x| ≥ 1.

Together with the exact mass ∫ ‖k‖ = π / 2, this is the property that makes the kernel useful: for self-adjoint A, B whose spectra are separated pairwise by at least 1, integrating e^{itA} C e^{-itB} against k solves the Sylvester equation AX - XB = C, and the mass bounds the solution by (π / 2) ‖C‖.

For x ≥ 1 the identity is computed by Fubini, using the absolute integrability of the superposition r(t) = ∫_{y > 0} (sin t / 2) w(y) e^{-|t| y} dy (TauCeti.HaagerupZsido.integrable_kernelIntegrand). Writing sin t through e^{±it}, the inner integral in t is a difference of two Lorentzians (TauCeti.integral_exp_mul_I_mul_exp_neg_mul_abs) centred at x ∓ 1, which differ by 2. The rotation by -i in k makes the result real, and the remaining y-integral of w(y) against the two Lorentzians is TauCeti.HaagerupZsido.integral_weight_mul_mul_inv_sub_inv. The case x ≤ -1 follows by oddness of the kernel.

Main results

• TauCeti.HaagerupZsido.integral_exp_mul_I_mul_reciprocalKernel: ∫ e^{itx} k(t) dt = 1 / x for |x| ≥ 1;
• TauCeti.HaagerupZsido.integral_realKernel_mul_sin: its real form ∫ r(t) sin (x t) dt = 1 / x for |x| ≥ 1;
• TauCeti.HaagerupZsido.integral_realKernel_mul_sin_mul_div: its rescaled form ∫ r(t) sin (a t / δ) dt = δ / a for 0 < δ ≤ |a|;
• TauCeti.HaagerupZsido.fourier_reciprocalKernel: the same identity in Mathlib's normalisation of the Fourier transform, 𝓕 k ξ = -1 / (2 π ξ) for 2 π |ξ| ≥ 1.

References

• U. Haagerup, L. Zsidó, the extremal kernel attaining the constant π / 2; see the account in S. Albeverio, K. A. Makarov, A. K. Motovilov, Graph subspaces and the spectral shift function, Canad. J. Math. 55 (2003), 449–503.
• R. Bhatia, C. Davis, A. McIntosh, Perturbation of spectral subspaces and solution of linear operator equations, Linear Algebra Appl. 52/53 (1983), 45–67.

theorem TauCeti.HaagerupZsido.integral_exp_mul_I_mul_reciprocalKernel {x : ℝ} (hx : 1 ≤ |x|) : ∫ (t : ℝ), Complex.exp (↑x * ↑t * Complex.I) * reciprocalKernel t = (↑x)⁻¹

The exterior reciprocal Fourier identity. For |x| ≥ 1, the Fourier integral of the Haagerup–Zsidó kernel is ∫ e^{itx} k(t) dt = 1 / x.

theorem TauCeti.HaagerupZsido.integral_realKernel_mul_sin {x : ℝ} (hx : 1 ≤ |x|) : ∫ (t : ℝ), realKernel t * Real.sin (x * t) = x⁻¹

The exterior reciprocal sine identity. For |x| ≥ 1, the real Haagerup–Zsidó kernel satisfies ∫ r(t) sin (x t) dt = 1 / x: the real part of TauCeti.HaagerupZsido.integral_exp_mul_I_mul_reciprocalKernel. Unlike the exponential form, it involves only real functions.

theorem TauCeti.HaagerupZsido.integral_realKernel_mul_sin_mul_div {a δ : ℝ} (hδ : 0 < δ) (ha : δ ≤ |a|) : ∫ (t : ℝ), realKernel t * Real.sin (a * (t / δ)) = δ * a⁻¹

The reciprocal sine identity at scale δ. For 0 < δ ≤ |a|, the real Haagerup–Zsidó kernel satisfies ∫ r(t) sin (a t / δ) dt = δ / a: the rescaled form of TauCeti.HaagerupZsido.integral_realKernel_mul_sin.

theorem TauCeti.HaagerupZsido.fourier_reciprocalKernel {ξ : ℝ} (hξ : 1 ≤ 2 * Real.pi * |ξ|) : FourierTransform.fourier reciprocalKernel ξ = -(↑(2 * Real.pi * ξ))⁻¹

The exterior reciprocal identity in Mathlib's Fourier normalisation. With 𝓕 f ξ = ∫ e^{-2πitξ} f(t) dt, the Haagerup–Zsidó kernel satisfies 𝓕 k ξ = -1 / (2 π ξ) whenever 2 π |ξ| ≥ 1.