The positive-definite cone is open and measurable

On the symmetric subspace, positive definiteness cuts out an open subset: the Hermitian condition holds identically there, so the cone is the preimage of the open set of matrices with positive quadratic form, TauCeti.isOpen_setOfPred_dotProduct_mulVec_pos.

The Wishart densities are supported on this cone, so its measurability is part of the carrier API.

The cone is also packaged as a subtype, TauCeti.PosDefMatrix, which is the carrier the Wishart and Cholesky APIs are stated on.

Main declarations

• TauCeti.PosDefMatrix — the positive-definite cone in the space of real symmetric matrices.
• TauCeti.isOpen_setOfPred_posDefMatrix — the positive-definite cone is open in the symmetric subspace.
• TauCeti.measurableSet_posDefMatrix — the positive-definite cone is measurable.

@[reducible, inline]

abbrev TauCeti.PosDefMatrix (p : ℕ) : Type

The cone of positive-definite real symmetric matrices of size p.

Equations

• TauCeti.PosDefMatrix p = { A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) // (↑A).PosDef }

theorem TauCeti.isOpen_setOfPred_posDefMatrix (p : ℕ) : IsOpen {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}

The positive-definite cone is open in the symmetric subspace.

theorem TauCeti.measurableSet_posDefMatrix (p : ℕ) : MeasurableSet {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}

The positive-definite cone is measurable in the symmetric subspace.