feat(LinearAlgebra/Matrix/PosDef): kronecker of positive (semi-)definite matrices is positive (semi-)definite (#28097)

This first shows that `U * x * star U` is positive (semi-)definite if and only if `x` is, for an invertible matrix `U` in a not necessarily commutative star-ring. Then using the spectral theorem, it follows that the kronecker of positive (semi-)definite matrices is positive (semi-)definite.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: themathqueen

Mathlib/Algebra/Algebra/StrictPositivity.lean

@@ -66,6 +66,21 @@ lemma _root_.isStrictlyPositive_one [LE A] [Monoid A] [Zero A] [ZeroLEOneClass A
 
 end basic
 
+section StarOrderedRing
+variable [Semiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A]
+
+lemma _root_.IsUnit.isStrictlyPositive_conjugate_iff {u a : A} (hu : IsUnit u) :
+    IsStrictlyPositive (u * a * star u) ↔ IsStrictlyPositive a := by
+  simp_rw [IsStrictlyPositive.iff_of_unital, hu.conjugate_nonneg_iff]
+  lift u to Aˣ using hu
+  rw [← Units.coe_star, Units.isUnit_mul_units, Units.isUnit_units_mul]
+
+lemma _root_.IsUnit.isStrictlyPositive_conjugate_iff' {u a : A} (hu : IsUnit u) :
+    IsStrictlyPositive (star u * a * u) ↔ IsStrictlyPositive a := by
+  simpa using hu.star.isStrictlyPositive_conjugate_iff
+
+end StarOrderedRing
+
 section Algebra
 
 variable {𝕜 : Type*} [Ring A] [PartialOrder A]

Mathlib/Algebra/Order/Star/Basic.lean

@@ -336,6 +336,17 @@ lemma star_lt_one_iff {x : R} : star x < 1 ↔ x < 1 := by
 protected theorem IsSelfAdjoint.sq_nonneg {a : R} (ha : IsSelfAdjoint a) : 0 ≤ a ^ 2 := by
   simp [sq, ha.mul_self_nonneg]
 
+lemma IsUnit.conjugate_nonneg_iff {u x : R} (hu : IsUnit u) :
+    0 ≤ u * x * star u ↔ 0 ≤ x := by
+  refine ⟨fun h ↦ ?_, fun h ↦ conjugate_nonneg' h _⟩
+  obtain ⟨v, hv⟩ := hu.exists_left_inv
+  have := by simpa [← mul_assoc] using conjugate_nonneg' h v
+  rwa [hv, one_mul, mul_assoc, ← star_mul, hv, star_one, mul_one] at this
+
+lemma IsUnit.conjugate_nonneg_iff' {u x : R} (hu : IsUnit u) :
+    0 ≤ star u * x * u ↔ 0 ≤ x := by
+  simpa using hu.star.conjugate_nonneg_iff
+
 end Semiring
 
 namespace MulOpposite

Mathlib/Algebra/Star/SelfAdjoint.lean

@@ -183,14 +183,19 @@ theorem pow {x : R} (hx : IsSelfAdjoint x) (n : ℕ) : IsSelfAdjoint (x ^ n) :=
   simp only [isSelfAdjoint_iff, star_pow, hx.star_eq]
 
 @[grind =]
-lemma _root_.isSelfAdjoint_conjugate_iff_of_isUnit {a u : R} (hu : IsUnit u) :
+lemma _root_.IsUnit.isSelfAdjoint_conjugate_iff {a u : R} (hu : IsUnit u) :
     IsSelfAdjoint (u * a * star u) ↔ IsSelfAdjoint a := by
   simp [IsSelfAdjoint, mul_assoc, hu.mul_right_inj, hu.star.mul_left_inj]
 
 @[grind =]
-lemma _root_.isSelfAdjoint_conjugate_iff_of_isUnit' {a u : R} (hu : IsUnit u) :
+lemma _root_.IsUnit.isSelfAdjoint_conjugate_iff' {a u : R} (hu : IsUnit u) :
     IsSelfAdjoint (star u * a * u) ↔ IsSelfAdjoint a := by
-  simpa using isSelfAdjoint_conjugate_iff_of_isUnit hu.star
+  simpa using hu.star.isSelfAdjoint_conjugate_iff
+
+@[deprecated (since := "2025-09-28")] alias _root_.isSelfAdjoint_conjugate_iff_of_isUnit :=
+  IsUnit.isSelfAdjoint_conjugate_iff
+@[deprecated (since := "2025-09-28")] alias _root_.isSelfAdjoint_conjugate_iff_of_isUnit' :=
+  IsUnit.isSelfAdjoint_conjugate_iff'
 
 end Monoid
 

Mathlib/Analysis/Matrix/Order.lean

@@ -228,6 +228,30 @@ theorem PosDef.commute_iff {A B : Matrix n n 𝕜} (hA : A.PosDef) (hB : B.PosDe
 lemma PosDef.posDef_sqrt [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) :
     PosDef (CFC.sqrt M) := hM.isStrictlyPositive.sqrt.posDef
 
+section kronecker
+variable {m : Type*} [Fintype m]
+
+open scoped Kronecker
+
+/-- The kronecker product of two positive semi-definite matrices is positive semi-definite. -/
+theorem PosSemidef.kronecker {x : Matrix n n 𝕜} {y : Matrix m m 𝕜}
+    (hx : x.PosSemidef) (hy : y.PosSemidef) : (x ⊗ₖ y).PosSemidef := by
+  classical
+  obtain ⟨a, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx.nonneg
+  obtain ⟨b, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hy.nonneg
+  simpa [mul_kronecker_mul, ← conjTranspose_kronecker, star_eq_conjTranspose] using
+    posSemidef_conjTranspose_mul_self _
+
+open Matrix in
+/-- The kronecker of two positive definite matrices is positive definite. -/
+theorem PosDef.kronecker {x : Matrix n n 𝕜} {y : Matrix m m 𝕜}
+    (hx : x.PosDef) (hy : y.PosDef) : (x ⊗ₖ y).PosDef := by
+  classical
+  exact hx.posSemidef.kronecker hy.posSemidef |>.posDef_iff_isUnit.mpr <|
+    hx.isUnit.kronecker hy.isUnit
+
+end kronecker
+
 /--
 A matrix is positive definite if and only if it has the form `Bᴴ * B` for some invertible `B`.
 -/

Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean

@@ -181,6 +181,24 @@ lemma coe_map_inv_mul_map (g : GL n R) : g.val⁻¹.map f * g.val.map f = 1 := b
   rw [← Matrix.map_mul]
   simp only [isUnits_det_units, nonsing_inv_mul, map_zero, map_one, Matrix.map_one]
 
+section kronecker
+variable {R m : Type*} [CommSemiring R] [Fintype m] [DecidableEq m]
+
+open scoped Kronecker
+
+/-- The invertible kronecker matrix of invertible matrices. -/
+protected def kronecker (x : GL n R) (y : GL m R) : GL (n × m) R where
+  val := x ⊗ₖ y
+  inv := ↑x⁻¹ ⊗ₖ ↑y⁻¹
+  val_inv := by simp only [← mul_kronecker_mul, Units.mul_inv, one_kronecker_one]
+  inv_val := by simp only [← mul_kronecker_mul, Units.inv_mul, one_kronecker_one]
+
+theorem _root_.Matrix.IsUnit.kronecker {x : Matrix n n R} {y : Matrix m m R}
+    (hx : IsUnit x) (hy : IsUnit y) : IsUnit (x ⊗ₖ y) :=
+  GeneralLinearGroup.kronecker hx.unit hy.unit |>.isUnit
+
+end kronecker
+
 end GeneralLinearGroup
 
 namespace SpecialLinearGroup

Mathlib/LinearAlgebra/Matrix/Hermitian.lean

@@ -45,8 +45,11 @@ instance (A : Matrix n n α) [Decidable (Aᴴ = A)] : Decidable (IsHermitian A)
 
 theorem IsHermitian.eq {A : Matrix n n α} (h : A.IsHermitian) : Aᴴ = A := h
 
-protected theorem IsHermitian.isSelfAdjoint {A : Matrix n n α} (h : A.IsHermitian) :
-    IsSelfAdjoint A := h
+theorem isHermitian_iff_isSelfAdjoint {A : Matrix n n α} :
+    A.IsHermitian ↔ IsSelfAdjoint A := Iff.rfl
+
+protected alias ⟨IsHermitian.isSelfAdjoint, _root_.IsSelfAdjoint.isHermitian⟩ :=
+  isHermitian_iff_isSelfAdjoint
 
 theorem IsHermitian.ext {A : Matrix n n α} : (∀ i j, star (A j i) = A i j) → A.IsHermitian := by
   intro h; ext i j; exact h i j

Mathlib/LinearAlgebra/Matrix/PosDef.lean

@@ -249,6 +249,31 @@ theorem PosSemidef.trace_eq_zero_iff {A : Matrix n n 𝕜} (hA : A.PosSemidef) :
       (by simpa using hA.eigenvalues_nonneg), Finset.mem_univ, true_imp_iff] at h
   exact funext_iff.eq ▸ hA.isHermitian.eigenvalues_eq_zero_iff.mp <| h
 
+section conjugate
+variable [DecidableEq n] {U x : Matrix n n R}
+
+/-- For an invertible matrix `U`, `star U * x * U` is positive semi-definite iff `x` is.
+This works on any ⋆-ring with a partial order.
+
+See `IsUnit.conjugate_nonneg_iff'` for  a similar statement for star-ordered rings. -/
+theorem IsUnit.posSemidef_conjugate_iff' (hU : IsUnit U) :
+    PosSemidef (star U * x * U) ↔ x.PosSemidef := by
+  simp_rw [PosSemidef, isHermitian_iff_isSelfAdjoint, hU.isSelfAdjoint_conjugate_iff',
+    and_congr_right_iff, ← mulVec_mulVec, dotProduct_mulVec, star_eq_conjTranspose, ← star_mulVec,
+    ← dotProduct_mulVec]
+  obtain ⟨V, hV⟩ := hU.exists_right_inv
+  exact fun _ => ⟨fun H y => by simpa [hV] using H (V *ᵥ y), fun H _ => H _⟩
+
+open Matrix in
+/-- For an invertible matrix `U`, `U * x * star U` is positive semi-definite iff `x` is.
+This works on any ⋆-ring with a partial order.
+
+See `IsUnit.conjugate_nonneg_iff` for  a similar statement for star-ordered rings. -/
+theorem IsUnit.posSemidef_conjugate_iff (hU : IsUnit U) :
+    PosSemidef (U * x * star U) ↔ x.PosSemidef := by simpa using hU.star.posSemidef_conjugate_iff'
+
+end conjugate
+
 /-- The matrix `vecMulVec a (star a)` is always positive semi-definite. -/
 theorem posSemidef_vecMulVec_self_star [StarOrderedRing R] (a : n → R) :
     (vecMulVec a (star a)).PosSemidef := by
@@ -470,6 +495,38 @@ theorem _root_.Matrix.posDef_inv_iff [DecidableEq n] {M : Matrix n n K} :
 
 end Field
 
+section conjugate
+variable [DecidableEq n] {x U : Matrix n n R}
+
+/-- For an invertible matrix `U`, `star U * x * U` is positive definite iff `x` is.
+This works on any ⋆-ring with a partial order.
+
+See `IsUnit.isStrictlyPositive_conjugate_iff'` for  a similar statement for star-ordered rings.
+For matrices, positive definiteness is equivalent to strict positivity when the underlying field is
+`ℝ` or `ℂ` (see `Matrix.isStrictlyPositive_iff_posDef`). -/
+theorem _root_.Matrix.IsUnit.posDef_conjugate_iff' (hU : IsUnit U) :
+    PosDef (star U * x * U) ↔ x.PosDef := by
+  simp_rw [PosDef, isHermitian_iff_isSelfAdjoint, hU.isSelfAdjoint_conjugate_iff',
+    and_congr_right_iff, ← mulVec_mulVec, dotProduct_mulVec, star_eq_conjTranspose, ← star_mulVec,
+    ← dotProduct_mulVec]
+  obtain ⟨V, hV, hV2⟩ := isUnit_iff_exists.mp hU
+  have hV3 (y : n → R) (hy : y ≠ 0) : U *ᵥ y ≠ 0 := fun h => by simpa [hy, hV2] using congr(V *ᵥ $h)
+  have hV4 (y : n → R) (hy : y ≠ 0) : V *ᵥ y ≠ 0 := fun h => by simpa [hy, hV] using congr(U *ᵥ $h)
+  exact fun _ => ⟨fun h x hx => by simpa [hV] using h _ (hV4 _ hx), fun h x hx => h _ (hV3 _ hx)⟩
+
+open Matrix in
+/-- For an invertible matrix `U`, `U * x * star U` is positive definite iff `x` is.
+This works on any ⋆-ring with a partial order.
+
+See `IsUnit.isStrictlyPositive_conjugate_iff` for  a similar statement for star-ordered rings.
+For matrices, positive definiteness is equivalent to strict positivity when the underlying field is
+`ℝ` or `ℂ` (see `Matrix.isStrictlyPositive_iff_posDef`). -/
+theorem _root_.Matrix.IsUnit.posDef_conjugate_iff (hU : IsUnit U) :
+    PosDef (U * x * star U) ↔ x.PosDef := by
+  simpa using hU.star.posDef_conjugate_iff'
+
+end conjugate
+
 section SchurComplement
 
 variable [StarOrderedRing R']