Documentation

TauCeti.Analysis.PositiveDefinite.Kernel.Shift

Bounded positive-definite kernels decrease along a symmetric shift #

Let K be a positive-definite kernel on a type α and let σ : α → α be a symmetric shift, meaning K (σ p) q = K p (σ q). If the diagonal of K is bounded — which by Cauchy--Schwarz is the same as K being bounded — then the shifted kernel is dominated by K: the difference

(p, q) ↦ K p q - K (σ p) q

is again positive definite. Boundedness cannot be dropped — for K p q = exp (p + q) on ℝ and σ = (· + 1) the difference is negative definite — and it is exactly what the proof consumes.

The mechanism is a moment-problem estimate. Fixing a finite family of points and coefficients, the numbers a n = ∑ᵢⱼ conj (cᵢ) K (σⁿ pᵢ) (pⱼ) c ⱼ form a positive-semidefinite Hankel matrix (m, n) ↦ a (m + n), because the shift can be moved from one argument to the other, and they are bounded above. The matrix estimate TauCeti.sub_nonneg_of_posSemidef_hankel then gives a 0 - a 1 ≥ 0, which is the quadratic form of the difference kernel.

This advances TauCetiRoadmap/OneParameterSemigroups/README.md, Part C, Milestone 2 ("BCR semigroup--Bochner"): applied to the Berg--Christensen--Ressel kernel of a bounded positive-definite function on [0,∞) × V with the time shift, it is the step that turns positive definiteness into complete monotonicity in the time variable.

Main declarations #

References #

Positive-definite kernels and symmetric shifts #

source
theorem TauCeti.posSemidef_sub_comp_shift {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} {σ : α → α} {C : ℝ} (hK : Matrix.PosSemidef K) (hshift : ∀ (p q : α), K (σ p) q = K p (σ q)) (hbdd : ∀ (p : α), ‖K p p‖ ≤ C) :
Matrix.PosSemidef fun (p q : α) => K p q - K (σ p) q

The difference of a bounded positive-definite kernel and its shift is positive definite. Here σ is a symmetric shift, K (σ p) q = K p (σ q), and the diagonal of K is bounded in norm by C — which by Cauchy--Schwarz bounds K everywhere. Boundedness is essential: for the (unbounded) kernel (p, q) ↦ exp (p + q) on ℝ and the shift σ = (· + 1) the difference below is the negative of a positive-definite kernel.