Analytic bounds for positive-semidefinite matrices

This file supplements the foundational API in TauCeti.LinearAlgebra.Matrix.PosSemidef with scalar Cauchy--Schwarz and vanishing bounds for RCLike-valued positive-semidefinite matrices, together with the resulting estimate for Hankel matrices: a sequence bounded above whose Hankel matrix (m, n) ↦ a (m + n) is positive semidefinite cannot increase at the first step.

The results apply in particular to positive-definite kernels, represented directly as matrices, but do not depend on Tau Ceti's positive-definite-function theory.

They supply the matrix prerequisites for Part C of the OneParameterSemigroups roadmap, including the positive-definite-function/kernel correspondence and the GNS/Kolmogorov decomposition. No Mathlib code is vendored.

Main declarations

• Matrix.PosSemidef.normSq_le: scalar Cauchy--Schwarz.
• Matrix.PosSemidef.eq_zero_of_apply_self_eq_zero_left and Matrix.PosSemidef.eq_zero_of_apply_self_eq_zero_right: zero-diagonal vanishing.
• Matrix.PosSemidef.norm_le_one_of_apply_self_eq_one: the normalized scalar bound.
• Matrix.PosSemidef.norm_le_of_norm_apply_self_le: the diagonal bounds every entry.
• TauCeti.sub_nonneg_of_posSemidef_hankel: a positive-semidefinite Hankel sequence bounded above does not increase at the first step.

References

• C. Berg, J. P. R. Christensen, P. Ressel, Harmonic Analysis on Semigroups (GTM 100, 1984), Chapter 3.

theorem Matrix.PosSemidef.normSq_le {α : Type v} {𝕜 : Type u} [RCLike 𝕜] {K : α → α → 𝕜} (hK : PosSemidef K) (a b : α) : RCLike.normSq (K a b) ≤ RCLike.re (K a a) * RCLike.re (K b b)

Scalar Cauchy--Schwarz for an RCLike-valued positive-semidefinite matrix.

theorem Matrix.PosSemidef.eq_zero_of_apply_self_eq_zero_left {α : Type v} {𝕜 : Type u} [RCLike 𝕜] {K : α → α → 𝕜} (hK : PosSemidef K) {a b : α} (ha : K a a = 0) : K a b = 0

A zero diagonal entry forces the corresponding row entry to vanish.

theorem Matrix.PosSemidef.eq_zero_of_apply_self_eq_zero_right {α : Type v} {𝕜 : Type u} [RCLike 𝕜] {K : α → α → 𝕜} (hK : PosSemidef K) {a b : α} (hb : K b b = 0) : K a b = 0

A zero diagonal entry forces the corresponding column entry to vanish.

theorem Matrix.PosSemidef.norm_le_one_of_apply_self_eq_one {α : Type v} {𝕜 : Type u} [RCLike 𝕜] {K : α → α → 𝕜} (hK : PosSemidef K) {a b : α} (ha : K a a = 1) (hb : K b b = 1) : ‖K a b‖ ≤ 1

If two diagonal entries are 1, then the corresponding off-diagonal entry has norm at most 1.

theorem Matrix.PosSemidef.norm_le_of_norm_apply_self_le {α : Type v} {𝕜 : Type u} [RCLike 𝕜] {K : α → α → 𝕜} {C : ℝ} (hK : PosSemidef K) (hdiag : ∀ (i : α), ‖K i i‖ ≤ C) (a b : α) : ‖K a b‖ ≤ C

The diagonal of a positive-semidefinite matrix bounds all of its entries. Cauchy--Schwarz turns a uniform bound on the (nonnegative real) diagonal entries into the same bound everywhere.

Bounded positive-semidefinite Hankel sequences

theorem TauCeti.sub_nonneg_of_posSemidef_hankel {𝕜 : Type u_1} [RCLike 𝕜] {a : ℕ → 𝕜} {D : ℝ} (ha : Matrix.PosSemidef fun (m n : ℕ) => a (m + n)) (hbd : ∀ (n : ℕ), RCLike.re (a n) ≤ D) : 0 ≤ a 0 - a 1

A positive-semidefinite Hankel sequence bounded above does not increase at the first step. If (m, n) ↦ a (m + n) is positive semidefinite and the real parts of a are bounded above by D — the entries are automatically real — then a 1 ≤ a 0 in the RCLike order. Cauchy--Schwarz alone gives a n ^ 2 ≤ a 0 * a (2 n), and the bound rules out a ratio a 1 / a 0 greater than 1.