Positive definiteness over the rationals

For an integer matrix, positive definiteness over ℤ is equivalent to positive definiteness after casting its entries to ℚ. This lets results about rational quadratic forms certify positive definiteness of integer matrices, and conversely.

The file also records the standard way of certifying a rational matrix as positive definite: write it as Bᴴ * B for an explicit B, and check that it is invertible. One general fact about Matrix.PosDef over any ring is recorded alongside, since Mathlib does not state it: a matrix on an empty index type is positive definite, which is what the rank-zero members of the classical Cartan families need.

Main results

• Matrix.PosDef.of_isEmpty: a matrix on an empty index type is positive definite.
• Ado.Matrix.posDef_map_intCast: an integer matrix that is positive definite over ℤ is positive definite over ℚ.
• Ado.Matrix.posDef_map_intCast_iff: positive definiteness over ℤ and over ℚ agree.
• Ado.Matrix.posDef_conjTranspose_mul_self_of_isUnit: an invertible rational matrix of the form Bᴴ * B is positive definite.

theorem Matrix.PosDef.of_isEmpty {n : Type u_1} {R : Type u_2} [Ring R] [PartialOrder R] [StarRing R] [IsEmpty n] (A : Matrix n n R) : A.PosDef

A matrix on an empty index type is vacuously positive definite. This is what the rank-zero members of the classical Cartan families A 0, B 0, C 0 and D 0 need.

theorem Ado.Matrix.posDef_map_intCast {n : Type u_1} {A : Matrix n n ℤ} (hA : A.PosDef) : (A.map Int.cast).PosDef

An integer matrix positive definite over ℤ is positive definite over ℚ.

theorem Ado.Matrix.posDef_map_intCast_iff {n : Type u_1} {A : Matrix n n ℤ} : (A.map Int.cast).PosDef ↔ A.PosDef

An integer matrix is positive definite over ℤ exactly when its cast to ℚ is positive definite. This transfers positive definiteness results between integer and rational matrices.

theorem Ado.Matrix.posDef_conjTranspose_mul_self_of_isUnit {n : Type u_1} {m : Type u_2} [Fintype m] [Fintype n] [DecidableEq n] (B : Matrix m n ℚ) (hunit : IsUnit (B.conjTranspose * B)) : (B.conjTranspose * B).PosDef

An invertible rational matrix of the form Bᴴ * B is positive definite. Being of that form gives positive semidefiniteness for free; invertibility upgrades it, by way of the injectivity hypothesis of Matrix.PosDef.conjTranspose_mul_self.

Mathlib's Matrix.PosSemidef.posDef_iff_isUnit says the same thing in one step, but only over an RCLike field, which ℚ is not; Matrix.PosDef.conjTranspose_mul_self is the criterion that does apply here, needing only StarOrderedRing and NoZeroDivisors.