chore(LinearAlgebra/Matrix/PosDef): rename Matrix.InnerProductSpace.ofMatrix (#30928)

- Renames `Matrix.NormedAddCommGroup.ofMatrix` to `Matrix.toNormedAddCommGroup`
- Removes `Matrix.InnerProductSpace.ofMatrix` and adds `Matrix.toInnerProductSpace` instead.
- Removes `Matrix.PosDef.matrixInnerProductSpace` and adds `Matrix.toMatrixInnerProductSpace` instead.
- Defines `Matrix.toSeminormedAddCommGroup` and `Matrix.toMatrixSeminormedAddCommGroup`.

Author: themathqueen

Mathlib/Analysis/Matrix/LDL.lean

@@ -47,16 +47,16 @@ variable {S : Matrix n n 𝕜} [Fintype n] (hS : S.PosDef)
 applying Gram-Schmidt-Orthogonalization w.r.t. the inner product induced by `Sᵀ` on the standard
 basis vectors `Pi.basisFun`. -/
 noncomputable def LDL.lowerInv : Matrix n n 𝕜 :=
-  @gramSchmidt 𝕜 (n → 𝕜) _ (_ :) (InnerProductSpace.ofMatrix hS.transpose) n _ _ _
-    (Pi.basisFun 𝕜 n)
+  @gramSchmidt 𝕜 (n → 𝕜) _ (Sᵀ.toNormedAddCommGroup hS.transpose)
+    (Sᵀ.toInnerProductSpace hS.transpose.posSemidef) n _ _ _ (Pi.basisFun 𝕜 n)
 
 theorem LDL.lowerInv_eq_gramSchmidtBasis :
     LDL.lowerInv hS =
       ((Pi.basisFun 𝕜 n).toMatrix
-          (@gramSchmidtBasis 𝕜 (n → 𝕜) _ (_ :) (InnerProductSpace.ofMatrix hS.transpose) n _ _ _
-            (Pi.basisFun 𝕜 n)))ᵀ := by
-  letI := NormedAddCommGroup.ofMatrix hS.transpose
-  letI := InnerProductSpace.ofMatrix hS.transpose
+          (@gramSchmidtBasis 𝕜 (n → 𝕜) _ (Sᵀ.toNormedAddCommGroup hS.transpose)
+            (Sᵀ.toInnerProductSpace hS.transpose.posSemidef) n _ _ _ (Pi.basisFun 𝕜 n)))ᵀ := by
+  letI := (Sᵀ.toNormedAddCommGroup hS.transpose)
+  letI := (Sᵀ.toInnerProductSpace hS.transpose.posSemidef)
   ext i j
   rw [LDL.lowerInv, Basis.coePiBasisFun.toMatrix_eq_transpose, coe_gramSchmidtBasis]
   rfl
@@ -65,13 +65,14 @@ noncomputable instance LDL.invertibleLowerInv : Invertible (LDL.lowerInv hS) :=
   rw [LDL.lowerInv_eq_gramSchmidtBasis]
   haveI :=
     Basis.invertibleToMatrix (Pi.basisFun 𝕜 n)
-      (@gramSchmidtBasis 𝕜 (n → 𝕜) _ (_ :) (InnerProductSpace.ofMatrix hS.transpose) n _ _ _
-        (Pi.basisFun 𝕜 n))
+      (@gramSchmidtBasis 𝕜 (n → 𝕜) _ (Sᵀ.toNormedAddCommGroup hS.transpose)
+        (Sᵀ.toInnerProductSpace hS.transpose.posSemidef) n _ _ _ (Pi.basisFun 𝕜 n))
   infer_instance
 
 theorem LDL.lowerInv_orthogonal {i j : n} (h₀ : i ≠ j) :
     ⟪LDL.lowerInv hS i, Sᵀ *ᵥ LDL.lowerInv hS j⟫ₑ = 0 :=
-  @gramSchmidt_orthogonal 𝕜 _ _ (_ :) (InnerProductSpace.ofMatrix hS.transpose) _ _ _ _ _ _ _ h₀
+  @gramSchmidt_orthogonal 𝕜 _ _ (Sᵀ.toNormedAddCommGroup hS.transpose)
+    (Sᵀ.toInnerProductSpace hS.transpose.posSemidef) _ _ _ _ _ _ _ h₀
 
 /-- The entries of the diagonal matrix `D` of the LDL decomposition. -/
 noncomputable def LDL.diagEntries : n → 𝕜 := fun i =>
@@ -82,9 +83,8 @@ noncomputable def LDL.diag : Matrix n n 𝕜 :=
   Matrix.diagonal (LDL.diagEntries hS)
 
 theorem LDL.lowerInv_triangular {i j : n} (hij : i < j) : LDL.lowerInv hS i j = 0 := by
-  rw [←
-    @gramSchmidt_triangular 𝕜 (n → 𝕜) _ (_ :) (InnerProductSpace.ofMatrix hS.transpose) n _ _ _
-      i j hij (Pi.basisFun 𝕜 n),
+  rw [← @gramSchmidt_triangular 𝕜 (n → 𝕜) _ (Sᵀ.toNormedAddCommGroup hS.transpose)
+      (Sᵀ.toInnerProductSpace hS.transpose.posSemidef) n _ _ _ i j hij (Pi.basisFun 𝕜 n),
     Pi.basisFun_repr, LDL.lowerInv]
 
 /-- Inverse statement of **LDL decomposition**: we can conjugate a positive definite matrix

Mathlib/Analysis/Matrix/Order.lean

@@ -19,8 +19,8 @@ This allows us to use more general results from C⋆-algebras, like `CFC.sqrt`.
 * `Matrix.instPartialOrder`: the partial order on matrices given by `x ≤ y := (y - x).PosSemidef`.
 * `Matrix.PosSemidef.dotProduct_mulVec_zero_iff`: for a positive semi-definite matrix `A`,
 we have `x⋆ A x = 0` iff `A x = 0`.
-* `Matrix.PosDef.matrixInnerProductSpace`: the inner product on matrices induced by a
-positive definite matrix `M`: `⟪x, y⟫ = (y * M * xᴴ).trace`.
+* `Matrix.toMatrixInnerProductSpace`: the inner product on matrices induced by a
+positive semi-definite matrix `M`: `⟪x, y⟫ = (y * M * xᴴ).trace`.
 
 ## Implementation notes
 
@@ -263,34 +263,52 @@ lemma posDef_iff_eq_conjTranspose_mul_self [DecidableEq n] {A : Matrix n n 𝕜}
 @[deprecated (since := "2025-08-07")] alias PosDef.posDef_iff_eq_conjTranspose_mul_self :=
   CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self
 
+/-- The pre-inner product space structure implementation. Only an auxiliary for
+`Matrix.toMatrixSeminormedAddCommGroup`, `Matrix.toMatrixNormedAddCommGroup`,
+and `Matrix.toMatrixInnerProductSpace`. -/
+private abbrev PosSemidef.matrixPreInnerProductSpace {M : Matrix n n 𝕜} (hM : M.PosSemidef) :
+    PreInnerProductSpace.Core 𝕜 (Matrix n n 𝕜) where
+  inner x y := (y * M * xᴴ).trace
+  conj_inner_symm _ _ := by
+    simp only [mul_assoc, starRingEnd_apply, ← trace_conjTranspose, conjTranspose_mul,
+      conjTranspose_conjTranspose, hM.isHermitian.eq]
+  re_inner_nonneg x := RCLike.nonneg_iff.mp (hM.mul_mul_conjTranspose_same x).trace_nonneg |>.1
+  add_left := by simp [mul_add]
+  smul_left := by simp
+
+/-- A positive definite matrix `M` induces a norm on `Matrix n n 𝕜`
+`‖x‖ = sqrt (x * M * xᴴ).trace`. -/
+noncomputable def toMatrixSeminormedAddCommGroup (M : Matrix n n 𝕜) (hM : M.PosSemidef) :
+    SeminormedAddCommGroup (Matrix n n 𝕜) :=
+  @InnerProductSpace.Core.toSeminormedAddCommGroup _ _ _ _ _ hM.matrixPreInnerProductSpace
+
 /-- A positive definite matrix `M` induces a norm on `Matrix n n 𝕜`:
 `‖x‖ = sqrt (x * M * xᴴ).trace`. -/
-noncomputable def PosDef.matrixNormedAddCommGroup {M : Matrix n n 𝕜} (hM : M.PosDef) :
+noncomputable def toMatrixNormedAddCommGroup (M : Matrix n n 𝕜) (hM : M.PosDef) :
     NormedAddCommGroup (Matrix n n 𝕜) :=
   letI : InnerProductSpace.Core 𝕜 (Matrix n n 𝕜) :=
-  { inner x y := (y * M * xᴴ).trace
-    conj_inner_symm _ _ := by
-      simp only [mul_assoc, starRingEnd_apply, ← trace_conjTranspose, conjTranspose_mul,
-        conjTranspose_conjTranspose, hM.isHermitian.eq]
-    re_inner_nonneg x := RCLike.nonneg_iff.mp
-      (hM.posSemidef.mul_mul_conjTranspose_same x).trace_nonneg |>.1
-    add_left := by simp [mul_add]
-    smul_left := by simp
+  { __ := hM.posSemidef.matrixPreInnerProductSpace
     definite x hx := by
       classical
       obtain ⟨y, hy, rfl⟩ := CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self.mp
         hM.isStrictlyPositive
+      simp only at hx
       rw [← mul_assoc, ← conjTranspose_conjTranspose x, star_eq_conjTranspose, ← conjTranspose_mul,
         conjTranspose_conjTranspose, mul_assoc, trace_conjTranspose_mul_self_eq_zero_iff] at hx
       lift y to (Matrix n n 𝕜)ˣ using hy
       simpa [← mul_assoc] using congr(y⁻¹ * $hx) }
   this.toNormedAddCommGroup
 
-/-- A positive definite matrix `M` induces an inner product on `Matrix n n 𝕜`:
+/-- A positive semi-definite matrix `M` induces an inner product on `Matrix n n 𝕜`:
 `⟪x, y⟫ = (y * M * xᴴ).trace`. -/
-def PosDef.matrixInnerProductSpace {M : Matrix n n 𝕜} (hM : M.PosDef) :
-    letI : NormedAddCommGroup (Matrix n n 𝕜) := hM.matrixNormedAddCommGroup
+def toMatrixInnerProductSpace (M : Matrix n n 𝕜) (hM : M.PosSemidef) :
+    letI : SeminormedAddCommGroup (Matrix n n 𝕜) := M.toMatrixSeminormedAddCommGroup hM
     InnerProductSpace 𝕜 (Matrix n n 𝕜) :=
   InnerProductSpace.ofCore _
 
+@[deprecated (since := "2025-11-18")] alias PosDef.matrixNormedAddCommGroup :=
+  toMatrixNormedAddCommGroup
+@[deprecated (since := "2025-11-12")] alias PosDef.matrixInnerProductSpace :=
+  toMatrixInnerProductSpace
+
 end Matrix

Mathlib/Analysis/Matrix/PosDef.lean

@@ -13,8 +13,8 @@ This file proves that eigenvalues of positive (semi)definite matrices are (nonne
 
 ## Main definitions
 
-* `InnerProductSpace.ofMatrix`: the inner product on `n → 𝕜` induced by a positive definite
-  matrix `A`, and is given by `⟪x, y⟫ = xᴴMy`.
+* `Matrix.toInnerProductSpace`: the pre-inner product space on `n → 𝕜` induced by a
+  positive semi-definite matrix `M`, and is given by `⟪x, y⟫ = xᴴMy`.
 
 -/
 
@@ -89,23 +89,39 @@ lemma det_pos [DecidableEq n] (hA : A.PosDef) : 0 < det A := by
 
 end PosDef
 
-/-- A positive definite matrix `A` induces a norm `‖x‖ = sqrt (re xᴴMx)`. -/
-noncomputable abbrev NormedAddCommGroup.ofMatrix (hA : A.PosDef) : NormedAddCommGroup (n → 𝕜) :=
+/-- The pre-inner product space structure implementation. Only an auxiliary for
+`Matrix.toSeminormedAddCommGroup`, `Matrix.toNormedAddCommGroup`,
+and `Matrix.toInnerProductSpace`. -/
+private def PosSemidef.preInnerProductSpace {M : Matrix n n 𝕜} (hM : M.PosSemidef) :
+    PreInnerProductSpace.Core 𝕜 (n → 𝕜) where
+  inner x y := (M *ᵥ y) ⬝ᵥ star x
+  conj_inner_symm x y := by
+    rw [dotProduct_comm, star_dotProduct, starRingEnd_apply, star_star,
+      star_mulVec, dotProduct_comm (M *ᵥ y), dotProduct_mulVec, hM.isHermitian.eq]
+  re_inner_nonneg x := dotProduct_comm _ (star x) ▸ hM.re_dotProduct_nonneg x
+  add_left := by simp only [star_add, dotProduct_add, forall_const]
+  smul_left _ _ _ := by rw [← smul_eq_mul, ← dotProduct_smul, starRingEnd_apply, ← star_smul]
+
+/-- A positive semi-definite matrix `M` induces a norm `‖x‖ = sqrt (re xᴴMx)`. -/
+noncomputable abbrev toSeminormedAddCommGroup (M : Matrix n n 𝕜) (hM : M.PosSemidef) :
+    SeminormedAddCommGroup (n → 𝕜) :=
+  @InnerProductSpace.Core.toSeminormedAddCommGroup _ _ _ _ _ hM.preInnerProductSpace
+
+/-- A positive definite matrix `M` induces a norm `‖x‖ = sqrt (re xᴴMx)`. -/
+noncomputable abbrev toNormedAddCommGroup (M : Matrix n n 𝕜) (hM : M.PosDef) :
+    NormedAddCommGroup (n → 𝕜) :=
   @InnerProductSpace.Core.toNormedAddCommGroup _ _ _ _ _
-    { inner x y := (A *ᵥ y) ⬝ᵥ star x
-      conj_inner_symm x y := by
-        rw [dotProduct_comm, star_dotProduct, starRingEnd_apply, star_star,
-          star_mulVec, dotProduct_comm (A *ᵥ y), dotProduct_mulVec, hA.isHermitian.eq]
-      re_inner_nonneg x := dotProduct_comm _ (star x) ▸ hA.posSemidef.re_dotProduct_nonneg x
-      definite x (hx : _ ⬝ᵥ _ = 0) := by
-        by_contra! h
-        simpa [hx, lt_irrefl, dotProduct_comm] using hA.re_dotProduct_pos h
-      add_left := by simp only [star_add, dotProduct_add, forall_const]
-      smul_left _ _ _ := by rw [← smul_eq_mul, ← dotProduct_smul, starRingEnd_apply, ← star_smul] }
-
-/-- A positive definite matrix `A` induces an inner product `⟪x, y⟫ = xᴴMy`. -/
-def InnerProductSpace.ofMatrix (hA : A.PosDef) :
-    @InnerProductSpace 𝕜 (n → 𝕜) _ (NormedAddCommGroup.ofMatrix hA).toSeminormedAddCommGroup :=
+  { __ := hM.posSemidef.preInnerProductSpace
+    definite x (hx : _ ⬝ᵥ _ = 0) := by
+      by_contra! h
+      simpa [hx, lt_irrefl, dotProduct_comm] using hM.re_dotProduct_pos h }
+
+/-- A positive semi-definite matrix `M` induces an inner product `⟪x, y⟫ = xᴴMy`. -/
+def toInnerProductSpace (M : Matrix n n 𝕜) (hM : M.PosSemidef) :
+    @InnerProductSpace 𝕜 (n → 𝕜) _ (M.toSeminormedAddCommGroup hM) :=
   InnerProductSpace.ofCore _
 
+@[deprecated (since := "2025-10-26")] alias NormedAddCommGroup.ofMatrix := toNormedAddCommGroup
+@[deprecated (since := "2025-10-26")] alias InnerProductSpace.ofMatrix := toInnerProductSpace
+
 end Matrix

Mathlib/LinearAlgebra/Matrix/PosDef.lean

@@ -24,8 +24,6 @@ order on matrices on `ℝ` or `ℂ`.
   and `xᴴMx` is nonnegative for all `x`.
 * `Matrix.PosDef` : a matrix `M : Matrix n n R` is positive definite if it is Hermitian and `xᴴMx`
   is greater than zero for all nonzero `x`.
-* `Matrix.InnerProductSpace.ofMatrix`: the inner product on `n → 𝕜` induced by a positive definite
-  matrix `M`, and is given by `⟪x, y⟫ = xᴴMy`.
 
 ## Main results