The Haagerup–Zsidó kernel

The Haagerup–Zsidó kernel is an integrable function k : ℝ → ℂ whose Fourier integral ∫ k(t) e^{itx} dt equals 1 / x for every |x| ≥ 1, and whose L¹ norm is exactly π / 2. Integrating a bounded operator-valued function against it is what gives the sharp constant π / 2 in the norm bound for the solution of the Sylvester equation AX - XB = C when the spectra of the self-adjoint operators A and B are separated pairwise, and hence in the corresponding Davis–Kahan sin Θ theorem. Those two identities are not proved in this file, which sets up the kernel and its elementary properties.

The kernel is built in four steps from the hyperbolic weight w(y) = tanh (π y / 2):

• TauCeti.HaagerupZsido.weight: the weight w(y) = tanh (π y / 2);
• TauCeti.HaagerupZsido.weightLaplaceTransform: its Laplace transform at |t|, L(t) = ∫_{y > 0} w(y) e^{-|t| y} dy;
• TauCeti.HaagerupZsido.realKernel: the real kernel r(t) = (sin t / 2) L(t);
• TauCeti.HaagerupZsido.reciprocalKernel: the kernel k(t) = -i r(t).

This file proves the elementary properties of these objects: the weight is continuous, odd, nonnegative on [0, ∞) and bounded there by min 1 (π y / 2); the Laplace transform is a genuine (absolutely convergent) integral for t ≠ 0, is even, nonnegative, measurable, and satisfies L(t) ≤ 1 / |t| and L(t) ≤ π / (2 t²); the two kernels are measurable and odd, with ‖k(t)‖ = |r(t)|. The two bounds on L give |r(t)| ≤ π / (2 (1 + t²)) (TauCeti.HaagerupZsido.abs_realKernel_le): near the origin |sin t| ≤ |t| cancels the 1 / |t| growth of L, and at infinity L decays like 1 / t² because w(y) ≤ π y / 2 near y = 0. Hence both kernels are integrable on ℝ.

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.

The hyperbolic weight

noncomputable def TauCeti.HaagerupZsido.weight (y : ℝ) : ℝ

The hyperbolic weight w(y) = tanh (π y / 2) of the Haagerup–Zsidó construction.

theorem TauCeti.HaagerupZsido.weight_def (y : ℝ) : weight y = Real.tanh (Real.pi * y / 2)

@[simp]

theorem TauCeti.HaagerupZsido.weight_zero : weight 0 = 0

@[simp]

theorem TauCeti.HaagerupZsido.weight_neg (y : ℝ) : weight (-y) = -weight y

The weight is odd.

theorem TauCeti.HaagerupZsido.weight_nonneg {y : ℝ} (hy : 0 ≤ y) : 0 ≤ weight y

The weight is nonnegative on [0, ∞).

theorem TauCeti.HaagerupZsido.weight_lt_one (y : ℝ) : weight y < 1

The weight is less than 1.

theorem TauCeti.HaagerupZsido.weight_le_pi_mul_div_two {y : ℝ} (hy : 0 ≤ y) : weight y ≤ Real.pi * y / 2

On [0, ∞) the weight lies below its tangent line π y / 2 at the origin.

theorem TauCeti.HaagerupZsido.continuous_weight : Continuous weight

The weight is continuous.

theorem TauCeti.HaagerupZsido.measurable_weight : Measurable weight

The Laplace transform of the weight

noncomputable def TauCeti.HaagerupZsido.weightLaplaceTransform (t : ℝ) : ℝ

The Laplace transform of the weight at |t|, L(t) = ∫_{y > 0} tanh (π y / 2) e^{-|t| y} dy. The integral converges absolutely for t ≠ 0 (integrableOn_weight_mul_exp); at t = 0 it diverges and the Bochner integral is 0.

theorem TauCeti.HaagerupZsido.weightLaplaceTransform_def (t : ℝ) : weightLaplaceTransform t = ∫ (y : ℝ) in Set.Ioi 0, weight y * Real.exp (-(|t| * y))

theorem TauCeti.HaagerupZsido.integrableOn_weight_mul_exp {t : ℝ} (ht : t ≠ 0) : MeasureTheory.IntegrableOn (fun (y : ℝ) => weight y * Real.exp (-(|t| * y))) (Set.Ioi 0) MeasureTheory.volume

For t ≠ 0 the integrand of the Laplace transform is integrable on (0, ∞): it is dominated by e^{-|t| y}.

theorem TauCeti.HaagerupZsido.weightLaplaceTransform_nonneg (t : ℝ) : 0 ≤ weightLaplaceTransform t

The Laplace transform of the weight is nonnegative.

@[simp]

theorem TauCeti.HaagerupZsido.weightLaplaceTransform_neg (t : ℝ) : weightLaplaceTransform (-t) = weightLaplaceTransform t

The Laplace transform of the weight is even.

theorem TauCeti.HaagerupZsido.measurable_weightLaplaceTransform : Measurable weightLaplaceTransform

The Laplace transform of the weight is measurable.

theorem TauCeti.HaagerupZsido.weightLaplaceTransform_le_inv_abs {t : ℝ} (ht : t ≠ 0) : weightLaplaceTransform t ≤ |t|⁻¹

Since the weight is less than 1, L(t) ≤ ∫_{y > 0} e^{-|t| y} dy = 1 / |t|.

theorem TauCeti.HaagerupZsido.weightLaplaceTransform_le_pi_div_two_mul_sq {t : ℝ} (ht : t ≠ 0) : weightLaplaceTransform t ≤ Real.pi / (2 * t ^ 2)

Since the weight lies below π y / 2, L(t) ≤ (π / 2) ∫_{y > 0} y e^{-|t| y} dy = π / (2 t²).

The real and reciprocal kernels

noncomputable def TauCeti.HaagerupZsido.realKernel (t : ℝ) : ℝ

The real Haagerup–Zsidó kernel r(t) = (sin t / 2) L(t).

theorem TauCeti.HaagerupZsido.realKernel_def (t : ℝ) : realKernel t = Real.sin t / 2 * weightLaplaceTransform t

noncomputable def TauCeti.HaagerupZsido.reciprocalKernel (t : ℝ) : ℂ

The Haagerup–Zsidó kernel k(t) = -i r(t). For |x| ≥ 1, the rotation by -i turns the Fourier integral ∫ r(t) e^{itx} dt = i / x of the odd real kernel into ∫ k(t) e^{itx} dt = 1 / x.

theorem TauCeti.HaagerupZsido.reciprocalKernel_def (t : ℝ) : reciprocalKernel t = -Complex.I * ↑(realKernel t)

theorem TauCeti.HaagerupZsido.measurable_realKernel : Measurable realKernel

theorem TauCeti.HaagerupZsido.measurable_reciprocalKernel : Measurable reciprocalKernel

@[simp]

theorem TauCeti.HaagerupZsido.realKernel_neg (t : ℝ) : realKernel (-t) = -realKernel t

The real kernel is odd.

@[simp]

theorem TauCeti.HaagerupZsido.reciprocalKernel_neg (t : ℝ) : reciprocalKernel (-t) = -reciprocalKernel t

The kernel is odd.

@[simp]

theorem TauCeti.HaagerupZsido.norm_reciprocalKernel (t : ℝ) : ‖reciprocalKernel t‖ = |realKernel t|

The kernel has the same modulus as the real kernel.

theorem TauCeti.HaagerupZsido.abs_realKernel_le (t : ℝ) : |realKernel t| ≤ Real.pi / (2 * (1 + t ^ 2))

The decay bound for the real kernel. For every t, |r(t)| ≤ π / (2 (1 + t²)). For |t| ≤ 1 this combines |sin t| ≤ |t| with L(t) ≤ 1 / |t|; for |t| ≥ 1 it combines |sin t| ≤ 1 with L(t) ≤ π / (2 t²).

theorem TauCeti.HaagerupZsido.integrable_realKernel : MeasureTheory.Integrable realKernel MeasureTheory.volume

The real kernel is integrable on ℝ: it is dominated by π / (2 (1 + t²)).

theorem TauCeti.HaagerupZsido.integrable_realKernel_mul_sin (x : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => realKernel t * Real.sin (x * t)) MeasureTheory.volume

The real Haagerup–Zsidó kernel times a sine is integrable.

theorem TauCeti.HaagerupZsido.integrable_reciprocalKernel : MeasureTheory.Integrable reciprocalKernel MeasureTheory.volume

The Haagerup–Zsidó kernel is integrable on ℝ.