The positive-definite cone in the space of all square matrices

Positivity of x ⬝ᵥ M *ᵥ x on nonzero vectors cuts out an open set of real square matrices, symmetric or not.

The positive-definite cone itself is not open in the space of all square matrices — the Hermitian condition cuts out a proper subspace once there are at least two rows — but on the symmetric subspace, where the Hermitian condition holds identically, the cone is the preimage of this open set and hence open; see TauCeti.MeasureTheory.Measure.SymmetricMatrix.PosDef. Ambiently the cone is still measurable, being the intersection of the closed Hermitian condition with that open one.

Main declarations

• TauCeti.isOpen_setOfPred_dotProduct_mulVec_pos — positivity of the quadratic form on nonzero vectors is an open condition on real square matrices;
• Matrix.posDef_fin_one_iff — a real 1 × 1 matrix is positive definite exactly when its single entry is positive;
• TauCeti.measurableSet_setOfPred_posDef — the positive-definite matrices form a measurable set.

@[simp]

theorem Matrix.posDef_fin_one_iff (M : Matrix (Fin 1) (Fin 1) ℝ) : M.PosDef ↔ 0 < M 0 0

A real 1 × 1 matrix is positive definite exactly when its single entry is positive.

theorem TauCeti.isOpen_setOfPred_dotProduct_mulVec_pos {ι : Type u_1} [Fintype ι] : IsOpen {M : Matrix ι ι ℝ | ∀ (x : ι → ℝ), x ≠ 0 → 0 < x ⬝ᵥ M.mulVec x}

Positivity of the quadratic form on nonzero vectors is an open condition on square real matrices, symmetric or not.

theorem TauCeti.measurableSet_setOfPred_posDef {ι : Type u_1} [Finite ι] : MeasurableSet {A : Matrix ι ι ℝ | A.PosDef}

The positive-definite real matrices form a measurable set.