The exact L¹ mass of the Haagerup–Zsidó kernel

The Haagerup–Zsidó kernel k(t) = -i r(t), r(t) = (sin t / 2) L(t), is a superposition over y > 0 of the damped oscillations (sin t / 2) w(y) e^{-|t| y}, where w(y) = tanh (π y / 2) and L is the Laplace transform of w. This file shows that the superposition is absolutely integrable on (0, ∞) × ℝ, so that integrals against the kernel may be computed by Fubini, and computes the mass of the kernel exactly:

∫_ℝ ‖k(t)‖ dt = ∫_ℝ |r(t)| dt = π / 2.

By Tonelli, the mass is ∫_{y > 0} (w(y) / 2) ∫_ℝ |sin t| e^{-y |t|} dt dy. The Laplace transform of |sin| is 2 (1 + e^{-π y}) / ((1 - e^{-π y}) (1 + y²)), and the weight w(y) = (1 - e^{-π y}) / (1 + e^{-π y}) is exactly the factor that cancels the periodic part, leaving ∫_{y > 0} (1 + y²)⁻¹ dy = π / 2. This value is the sharp constant π / 2 in the norm bound for the Sylvester equation AX - XB = C with pairwise separated spectra. In that bound the kernel is integrated against a bounded vector-valued function F, and the mass gives ‖∫ k(t) • F(t) dt‖ ≤ (π / 2) sup ‖F‖.

Main results

• TauCeti.HaagerupZsido.integrable_kernelIntegrand: the integrand (y, t) ↦ (sin t / 2) w(y) e^{-|t| y} is integrable on (0, ∞) × ℝ;
• TauCeti.HaagerupZsido.integral_abs_realKernel: ∫_ℝ |r(t)| dt = π / 2;
• TauCeti.HaagerupZsido.integral_norm_reciprocalKernel: ∫_ℝ ‖k(t)‖ dt = π / 2;
• TauCeti.HaagerupZsido.norm_integral_reciprocalKernel_smul_le: if ‖F(t)‖ ≤ C almost everywhere, then ‖∫_ℝ k(t) • F(t) dt‖ ≤ (π / 2) C.

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.

noncomputable def TauCeti.HaagerupZsido.kernelIntegrand (p : ℝ × ℝ) : ℝ

The integrand (y, t) ↦ (sin t / 2) w(y) e^{-|t| y} whose integral over y > 0 is the real kernel r(t).

theorem TauCeti.HaagerupZsido.kernelIntegrand_def (p : ℝ × ℝ) : kernelIntegrand p = Real.sin p.2 / 2 * (weight p.1 * Real.exp (-(|p.2| * p.1)))

theorem TauCeti.HaagerupZsido.continuous_kernelIntegrand : Continuous kernelIntegrand

theorem TauCeti.HaagerupZsido.integral_kernelIntegrand (t : ℝ) : ∫ (y : ℝ) in Set.Ioi 0, kernelIntegrand (y, t) = realKernel t

The real kernel is the integral of kernelIntegrand over y > 0.

theorem TauCeti.HaagerupZsido.integrable_kernelIntegrand : MeasureTheory.Integrable kernelIntegrand ((MeasureTheory.volume.restrict (Set.Ioi 0)).prod MeasureTheory.volume)

The product integrability certificate. The integrand (y, t) ↦ (sin t / 2) w(y) e^{-|t| y} is integrable on (0, ∞) × ℝ. Integrals against the kernel can therefore be computed by exchanging the order of integration.

theorem TauCeti.HaagerupZsido.integral_abs_realKernel : ∫ (t : ℝ), |realKernel t| = Real.pi / 2

The exact mass of the real kernel. ∫_ℝ |r(t)| dt = π / 2.

theorem TauCeti.HaagerupZsido.integral_norm_reciprocalKernel : ∫ (t : ℝ), ‖reciprocalKernel t‖ = Real.pi / 2

The exact mass of the Haagerup–Zsidó kernel. ∫_ℝ ‖k(t)‖ dt = π / 2.

theorem TauCeti.HaagerupZsido.integrable_reciprocalKernel_smul {G : Type u_1} [NormedAddCommGroup G] [NormedSpace ℂ G] {F : ℝ → G} {C : ℝ} (hF : MeasureTheory.AEStronglyMeasurable F MeasureTheory.volume) (hFC : ∀ᵐ (t : ℝ), ‖F t‖ ≤ C) : MeasureTheory.Integrable (fun (t : ℝ) => reciprocalKernel t • F t) MeasureTheory.volume

Against the Haagerup–Zsidó kernel k, every almost everywhere strongly measurable and essentially bounded function F : ℝ → G into a complex normed space gives an integrable product t ↦ k(t) • F(t).

theorem TauCeti.HaagerupZsido.norm_integral_reciprocalKernel_smul_le {G : Type u_1} [NormedAddCommGroup G] [NormedSpace ℂ G] {F : ℝ → G} {C : ℝ} (hFC : ∀ᵐ (t : ℝ), ‖F t‖ ≤ C) : ‖∫ (t : ℝ), reciprocalKernel t • F t‖ ≤ Real.pi / 2 * C

The kernel-mass integral bound. If F : ℝ → G takes values in a complex normed space and ‖F(t)‖ ≤ C almost everywhere, then ‖∫ k(t) • F(t) dt‖ ≤ (π / 2) C, where k is the Haagerup–Zsidó kernel.