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 Schur products, Schur powers, products of weights over unions of finite sets, 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.

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_schur_finset_prod and Matrix.PosSemidef.hadamard_pow: finite Schur products and Schur powers.
• TauCeti.posSemidef_prod_union: the matrix (i, j) ↦ ∏_{a ∈ L i ∪ L j} w a for weights in [0, 1].

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} [Ring 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: conjugate symmetry and nonnegativity on every finite family, allowing repeated indices.

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_prod_union {α : Type v} {ι : Type w} [DecidableEq α] (L : ι → Finset α) {w : α → ℝ} (hw₀ : ∀ (a : α), 0 ≤ w a) (hw₁ : ∀ (a : α), w a ≤ 1) : Matrix.PosSemidef fun (i j : ι) => ∏ a ∈ L i ∪ L j, w a

For weights w in [0, 1] and finite sets L i, the matrix (i, j) ↦ ∏_{a ∈ L i ∪ L j} w a is positive semidefinite.

theorem Matrix.PosSemidef.hadamard_pow {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {K : α → α → 𝕜} (hK : PosSemidef K) (n : ℕ) : PosSemidef fun (a b : α) => K a b ^ n

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