Positive-semidefinite matrix algebra

This file supplements Mathlib's Matrix.PosSemidef API for matrices indexed by arbitrary types. It provides rank-one and constant matrices, finite pointwise sums and Schur products, Schur powers, and the quadratic-form characterization.

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

• TauCeti.posSemidef_rankOne: rank-one positive-semidefinite matrices.
• TauCeti.posSemidef_const_one and TauCeti.posSemidef_const_of_nonneg: constant matrices.
• TauCeti.posSemidef_iff_finite_sum: the quadratic-form characterization.
• TauCeti.posSemidef_finset_sum: finite pointwise sums.
• TauCeti.posSemidef_schur_finset_prod and TauCeti.posSemidef_schur_pow: finite Schur products and Schur powers.

References

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

theorem TauCeti.posSemidef_rankOne {α : Type v} {R : Type u} [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (g : α → R) : Matrix.PosSemidef fun (a b : α) => star (g a) * g b

The rank-one matrix (a, b) ↦ star (g a) · g b is positive semidefinite for an arbitrary index type. Such matrices are elementary building blocks for positive-semidefinite matrices; taking g ≡ 1 gives the constant matrix 1.

theorem TauCeti.posSemidef_const_one {α : Type v} {R : Type u} [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] : Matrix.PosSemidef fun (x x_1 : α) => 1

The constant matrix with value 1 is positive semidefinite.

theorem TauCeti.posSemidef_const_of_nonneg {α : Type v} {R : Type u} [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {c : R} (hc : 0 ≤ c) : Matrix.PosSemidef fun (x x_1 : α) => c

A nonnegative constant gives a positive-semidefinite constant matrix.

theorem TauCeti.posSemidef_iff_finite_sum {α : Type v} {R : Type u} [Ring R] [PartialOrder R] [StarRing R] {K : α → α → R} : Matrix.PosSemidef K ↔ (∀ (a b : α), star (K a b) = K b a) ∧ ∀ {ι : Type u_1} [inst : Fintype ι] (v : ι → α) (x : ι → R), 0 ≤ ∑ i : ι, ∑ j : ι, star (x i) * K (v i) (v j) * x j

The quadratic-form characterization of an arbitrary-index positive-semidefinite matrix. The reverse direction constructs positivity from conjugate symmetry and finite quadratic-form nonnegativity without unfolding Matrix.PosSemidef.

theorem TauCeti.posSemidef_finset_sum {α : Type v} {R : Type u} [Ring R] [PartialOrder R] [StarRing R] [AddLeftMono R] {ι : Type w} {s : Finset ι} {K : ι → α → α → R} (hK : ∀ i ∈ s, Matrix.PosSemidef (K i)) : Matrix.PosSemidef fun (a b : α) => ∑ i ∈ s, K i a b

Finite pointwise sums of positive-semidefinite matrices are positive semidefinite.

theorem TauCeti.posSemidef_schur_finset_prod {α : Type v} {𝕜 : Type u} [RCLike 𝕜] {ι : Type w} {s : Finset ι} {K : ι → α → α → 𝕜} (hK : ∀ i ∈ s, Matrix.PosSemidef (K i)) : Matrix.PosSemidef fun (a b : α) => ∏ i ∈ s, K i a b

Finite pointwise Schur products of positive-semidefinite matrices are positive semidefinite.

theorem TauCeti.posSemidef_schur_pow {α : Type v} {𝕜 : Type u} [RCLike 𝕜] {K : α → α → 𝕜} (hK : Matrix.PosSemidef K) (n : ℕ) : Matrix.PosSemidef fun (a b : α) => K a b ^ n

Schur powers of a positive-semidefinite matrix are positive semidefinite.