The Haagerup–Zsidó weight against adjacent Cauchy resolvents

For a ≥ 0, the weight w(y) = tanh (π y / 2) of the Haagerup–Zsidó kernel satisfies

∫_{y > 0} w(y) y ((y² + a²)⁻¹ - (y² + (a + 2)²)⁻¹) dy = 2 / (a + 1).

This is the y-integral to which the Fourier integral ∫ k(t) e^{itx} dt of the kernel reduces by Fubini at x = a + 1 ≥ 1: pairing the oscillation sin t e^{itx} with the damped exponential e^{-|t| y} produces the two Lorentzians y / (y² + (x ∓ 1)²), whose centres differ by 2. Evaluating it is the analytic core of the exterior reciprocal identity ∫ k(t) e^{itx} dt = 1 / x for |x| ≥ 1.

The proof expands the weight into its odd poles, w(y) y = (4 / π) ∑_{n ≥ 0} y² / (y² + (2 n + 1)²) (TauCeti.hasSum_pi_div_two_mul_tanh). Each term integrates against the two resolvents by TauCeti.integral_Ioi_sq_div_sq_add_sq_mul_sq_add_sq, to 2 (1 / (a + 2 n + 1) - 1 / (a + 2 n + 3)). These terms are nonnegative, so the sum and the integral commute, and the series telescopes to 2 / (a + 1).

Main results

• TauCeti.HaagerupZsido.integral_weight_mul_mul_inv_sub_inv: the value 2 / (a + 1);
• TauCeti.HaagerupZsido.integrableOn_weight_mul_mul_inv_sub_inv: the integrand is integrable on (0, ∞).

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.

theorem TauCeti.HaagerupZsido.integral_weight_mul_mul_inv_sub_inv {a : ℝ} (ha : 0 ≤ a) : ∫ (y : ℝ) in Set.Ioi 0, weight y * y * ((y ^ 2 + a ^ 2)⁻¹ - (y ^ 2 + (a + 2) ^ 2)⁻¹) = 2 / (a + 1)

The weight against adjacent Cauchy resolvents. For a ≥ 0, ∫_{y > 0} w(y) y ((y² + a²)⁻¹ - (y² + (a + 2)²)⁻¹) dy = 2 / (a + 1), where w(y) = tanh (π y / 2) is the Haagerup–Zsidó weight.

theorem TauCeti.HaagerupZsido.integrableOn_weight_mul_mul_inv_sub_inv {a : ℝ} (ha : 0 ≤ a) : MeasureTheory.IntegrableOn (fun (y : ℝ) => weight y * y * ((y ^ 2 + a ^ 2)⁻¹ - (y ^ 2 + (a + 2) ^ 2)⁻¹)) (Set.Ioi 0) MeasureTheory.volume

For a ≥ 0, the function w(y) y ((y² + a²)⁻¹ - (y² + (a + 2)²)⁻¹) is integrable on (0, ∞).