the correspondence between matrix.pos_semidef and linear_map.is_positive

In this file, we show that x ∈ Mₙ being positive semi-definite is equivalent to x.to_euclidean_lin.is_positive

theorem Matrix.conjTranspose_eq_adjoint {𝕜 : Type u_3} {m : Type u_1} {n : Type u_2} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] [RCLike 𝕜] (A : Matrix m n 𝕜) : toLin' A.conjTranspose = LinearMap.adjoint (toLin' A)

The adjoint of the linear map associated to a matrix is the linear map associated to the conjugate transpose of that matrix.

theorem Matrix.posSemidef_star_mul_self {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) : (A.conjTranspose * A).PosSemidef

Alias of Matrix.posSemidef_conjTranspose_mul_self.

---

The conjugate transpose of a matrix multiplied by the matrix is positive semidefinite

theorem Matrix.posSemidef_mul_star_self {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) : (A * A.conjTranspose).PosSemidef

Alias of Matrix.posSemidef_self_mul_conjTranspose.

---

A matrix multiplied by its conjugate transpose is positive semidefinite

theorem Matrix.toEuclideanLin_eq_piLp_linearEquiv {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (x : Matrix n n 𝕜) : toEuclideanLin x = toLin' x

theorem Matrix.of_isHermitian' {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} (hx : x.IsHermitian) (x_1 : n → 𝕜) : ↑(RCLike.re (∑ i : n, star x_1 i * ∑ x_2 : n, x i x_2 * x_1 x_2)) = ∑ x_2 : n, star x_1 x_2 * ∑ x_3 : n, x x_2 x_3 * x_1 x_3

theorem Matrix.posSemidef_eq_linearMap_positive {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (x : Matrix n n 𝕜) : x.PosSemidef ↔ (toEuclideanLin x).IsPositive

theorem Matrix.posSemidef_iff {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (x : Matrix n n 𝕜) : x.PosSemidef ↔ ∃ (y : Matrix n n 𝕜), x = y.conjTranspose * y

theorem Matrix.dotProduct_eq_inner {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} [Fintype n] (x y : n → 𝕜) : star x ⬝ᵥ y = ∑ i : n, inner (x i) (y i)

theorem Matrix.PosSemidef.invertible_iff_posDef {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} (hx : x.PosSemidef) : Function.Bijective ⇑(toLin' x) ↔ x.PosDef

theorem Matrix.isHermitian_self_hMul_conjTranspose {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_1} {n : Type u_2} [Fintype m] (A : Matrix m n 𝕜) : (A.conjTranspose * A).IsHermitian

theorem Matrix.trace_star {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] {A : Matrix n n 𝕜} : star A.trace = A.conjTranspose.trace

theorem Matrix.nonneg_eigenvalues_of_posSemidef {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {μ : ℝ} {A : Matrix n n 𝕜} (hμ : Module.End.HasEigenvalue (toEuclideanLin A) ↑μ) (H : A.PosSemidef) : 0 ≤ μ

theorem Matrix.IsHermitian.nonneg_eigenvalues_of_posSemidef {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) (i : n) : 0 ≤ ⋯.eigenvalues i

noncomputable def Matrix.invertible_of_bij_toLin' {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (h : Function.Bijective ⇑(toLin' Q)) : Invertible Q

Equations

• Matrix.invertible_of_bij_toLin' h = ⋯.invertible

theorem Matrix.bij_toLin'_of_invertible {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (h : Invertible Q) : Function.Bijective ⇑(toLin' Q)

noncomputable instance Matrix.PosDef.invertible {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) : Invertible Q

Equations

• hQ.invertible = Matrix.invertible_of_bij_toLin' ⋯

theorem Matrix.mulVec_sum {n : Type u_1} {m : Type u_2} {k : Type u_3} {R : Type u_4} [NonUnitalNonAssocSemiring R] [Fintype n] [Fintype m] [Fintype k] (x : Matrix m n R) (y : k → n → R) : x.mulVec (∑ i : k, y i) = ∑ i : k, x.mulVec (y i)

theorem Matrix.vecMul_sum {n : Type u_1} {m : Type u_2} {k : Type u_3} {R : Type u_4} [NonUnitalNonAssocSemiring R] [Fintype m] [Fintype n] [Fintype k] (x : Matrix n m R) (y : k → n → R) : vecMul (∑ i : k, y i) x = ∑ i : k, vecMul (y i) x

theorem Matrix.toLin_piLp_eq_toLin' {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} [Fintype n] [DecidableEq n] : toLin (PiLp.basisFun 2 𝕜 n) (PiLp.basisFun 2 𝕜 n) = toLin'

theorem Matrix.posSemidef_iff_eq_rankOne {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} : x.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → EuclideanSpace 𝕜 n), x = ∑ i : Fin m, LinearMap.toMatrix' ↑(((rankOne 𝕜) (v i)) (v i))

theorem Matrix.posSemidef_iff_eq_rankOne' {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} : x.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), x = ∑ i : Fin m, LinearMap.toMatrix' ↑(((rankOne 𝕜) ((EuclideanSpace.equiv n 𝕜).symm (v i))) ((EuclideanSpace.equiv n 𝕜).symm (v i)))

theorem Matrix.posSemidef_iff_eq_rankOne'' {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} : x.PosSemidef ↔ ∃ (m : Type) (_hm : Fintype m) (v : m → n → 𝕜), x = ∑ i : m, LinearMap.toMatrix' ↑(((rankOne 𝕜) ((EuclideanSpace.equiv n 𝕜).symm (v i))) ((EuclideanSpace.equiv n 𝕜).symm (v i)))

theorem rankOne.EuclideanSpace.toEuclideanLin_symm {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {m : Type u_3} [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (x : EuclideanSpace 𝕜 n) (y : EuclideanSpace 𝕜 m) : Matrix.toEuclideanLin.symm ↑(((rankOne 𝕜) x) y) = Matrix.col (Fin 1) x * (Matrix.col (Fin 1) y).conjTranspose

theorem rankOne.EuclideanSpace.toMatrix' {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {m : Type u_3} [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (x : EuclideanSpace 𝕜 n) (y : EuclideanSpace 𝕜 m) : LinearMap.toMatrix' ↑(((rankOne 𝕜) x) y) = Matrix.col (Fin 1) x * (Matrix.col (Fin 1) y).conjTranspose

theorem rankOne.Pi.toMatrix'' {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (x y : n → 𝕜) : LinearMap.toMatrix' ↑(((rankOne 𝕜) ((EuclideanSpace.equiv n 𝕜).symm x)) ((EuclideanSpace.equiv n 𝕜).symm y)) = Matrix.col (Fin 1) x * (Matrix.col (Fin 1) y).conjTranspose

theorem Matrix.posSemidef_iff_col_mul_conjTranspose_col {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} : x.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → EuclideanSpace 𝕜 n), x = ∑ i : Fin m, col (Fin 1) (v i) * (col (Fin 1) (v i)).conjTranspose

a matrix $x$ is positive semi-definite if and only if there exists vectors $(v_i)$ such that $\sum_i v_iv_i^*=x$

theorem Matrix.posSemidef_iff_col_mul_conjTranspose_col' {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} : x.PosSemidef ↔ ∃ (m : Type) (_hm : Fintype m) (v : m → EuclideanSpace 𝕜 n), x = ∑ i : m, col (Fin 1) (v i) * (col (Fin 1) (v i)).conjTranspose

theorem Matrix.posSemidef_iff_vecMulVec {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} : x.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → EuclideanSpace 𝕜 n), x = ∑ i : Fin m, vecMulVec (v i) (star (v i))

theorem Matrix.posSemidef_iff_vecMulVec' {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} : x.PosSemidef ↔ ∃ (m : Type) (_hm : Fintype m) (v : m → EuclideanSpace 𝕜 n), x = ∑ i : m, vecMulVec (v i) (star (v i))

theorem vecMulVec_posSemidef {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (x : n → 𝕜) : (Matrix.vecMulVec x (star x)).PosSemidef

theorem Matrix.posDefOne {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] : PosDef 1

the identity is a positive definite matrix

theorem Matrix.PosDef.pos_eigenvalues {n : Type u_2} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosDef) (i : n) : 0 < ⋯.eigenvalues i

Alias of Matrix.PosDef.eigenvalues_pos.

---

The eigenvalues of a positive definite matrix are positive

theorem Matrix.PosDef.pos_trace {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] [Nonempty n] {x : Matrix n n 𝕜} (hx : x.PosDef) : 0 < RCLike.re x.trace

theorem Matrix.PosDef.trace_ne_zero {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] [Nonempty n] {x : Matrix n n 𝕜} (hx : x.PosDef) : x.trace ≠ 0

the trace of a positive definite matrix is non-zero

theorem Matrix.toEuclideanLin_apply' {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} [Fintype n] [DecidableEq n] (x : Matrix n n 𝕜) (v : EuclideanSpace 𝕜 n) : (toEuclideanLin x) v = x.mulVec v

theorem PosSemidef.complex {n : Type u_1} [Fintype n] [DecidableEq n] (x : Matrix n n ℂ) : x.PosSemidef ↔ ∀ (y : n → ℂ), 0 ≤ star y ⬝ᵥ x.mulVec y

theorem StdBasisMatrix.sum_eq_one {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (a : 𝕜) : ∑ k : n, Matrix.stdBasisMatrix k k a = a • 1

theorem stdBasisMatrix_hMul {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (i j k l : n) (a b : 𝕜) : Matrix.stdBasisMatrix i j a * Matrix.stdBasisMatrix k l b = (if j = k then 1 else 0) • Matrix.stdBasisMatrix i l (a * b)

theorem Matrix.smul_stdBasisMatrix' {n : Type u_1} {R : Type u_2} [CommSemiring R] [DecidableEq n] (i j : n) (c : R) : stdBasisMatrix i j c = c • stdBasisMatrix i j 1

theorem Matrix.trace_iff' {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] (x : Matrix n n 𝕜) : x.trace = ∑ i : n, x i i

theorem existsUnique_trace {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] [Nontrivial n] : ∃! φ : Matrix n n 𝕜 →ₗ[𝕜] 𝕜, (∀ (a b : Matrix n n 𝕜), φ (a * b) = φ (b * a)) ∧ φ 1 = 1

theorem Matrix.stdBasisMatrix.trace {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (i j : n) (a : 𝕜) : (stdBasisMatrix i j a).trace = if i = j then a else 0

theorem Matrix.stdBasisMatrix_eq {R : Type u_1} {n : Type u_2} {m : Type u_3} [Semiring R] [DecidableEq n] [DecidableEq m] (i : n) (j : m) (a : R) : stdBasisMatrix i j a = fun (i' : n) (j' : m) => if i = i' ∧ j = j' then a else 0

theorem vecMulVec_eq_zero_iff {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] (x : n → 𝕜) : Matrix.vecMulVec x (star x) = 0 ↔ x = 0

theorem Matrix.PosDef.diagonal_iff {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (x : n → 𝕜) : (diagonal x).PosDef ↔ ∀ (i : n), 0 < x i

theorem norm_ite {α : Type u_1} [Norm α] (P : Prop) [Decidable P] (a b : α) : ‖if P then a else b‖ = if P then ‖a‖ else ‖b‖

theorem Matrix.PosSemidef.diagonal_iff {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (x : n → 𝕜) : (diagonal x).PosSemidef ↔ ∀ (i : n), 0 ≤ x i

theorem Matrix.trace_conjTranspose_hMul_self_nonneg {n : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_1} [Fintype m] [Fintype n] (x : Matrix m n 𝕜) : 0 ≤ (x.conjTranspose * x).trace

theorem Matrix.PosSemidef.trace_conjTranspose_hMul_self_nonneg {n : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_1} [Fintype m] [Fintype n] [DecidableEq m] {Q : Matrix m m 𝕜} (hQ : Q.PosSemidef) (x : Matrix n m 𝕜) : 0 ≤ (Q * x.conjTranspose * x).trace

given a positive definite matrix $Q$, we have $0\leq\operatorname{Tr}(Qx^*x)$ for any matrix $x$

@[simp]

theorem Matrix.Finset.sum_abs_eq_zero_iff' {𝕜 : Type u_2} [RCLike 𝕜] {s : Type u_1} [Fintype s] {x : s → 𝕜} : ∑ i : s, ‖x i‖ ^ 2 = 0 ↔ ∀ (i : s), ‖x i‖ ^ 2 = 0

theorem Matrix.trace_conjTranspose_hMul_self_eq_zero {n : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_1} [Fintype n] [Fintype m] (x : Matrix n m 𝕜) : (x.conjTranspose * x).trace = 0 ↔ x = 0

theorem Matrix.PosDef.trace_conjTranspose_hMul_self_eq_zero {n : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_1} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] {Q : Matrix m m 𝕜} (hQ : Q.PosDef) {x : Matrix n m 𝕜} : (Q * x.conjTranspose * x).trace = 0 ↔ x = 0

given a positive definite matrix $Q$, we get $\textnormal{Tr}(Qx^*x)=0$ if and only if $x=0$ for any matrix $x$

theorem Matrix.Nontracial.trace_conjTranspose_hMul_self_eq_zero {n : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_1} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] {Q : Matrix m m 𝕜} (hQ : Q.PosDef) {x : Matrix n m 𝕜} : (Q * x.conjTranspose * x).trace = 0 ↔ x = 0

Alias of Matrix.PosDef.trace_conjTranspose_hMul_self_eq_zero.

---

given a positive definite matrix $Q$, we get $\textnormal{Tr}(Qx^*x)=0$ if and only if $x=0$ for any matrix $x$

theorem Matrix.IsHermitian.trace_conj_symm_star_hMul {n : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_1} [Fintype m] [Fintype n] {Q : Matrix m m 𝕜} (hQ : Q.IsHermitian) (x y : Matrix n m 𝕜) : (starRingEnd 𝕜) (Q * y.conjTranspose * x).trace = (Q * x.conjTranspose * y).trace

theorem Matrix.conjTranspose_hMul_self_eq_zero {n : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_1} [Fintype m] [Fintype n] (x : Matrix n m 𝕜) : x.conjTranspose * x = 0 ↔ x = 0

theorem Matrix.PosSemidef.smul {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] {x : Matrix n n 𝕜} (hx : x.PosSemidef) (α : NNReal) : (↑↑α • x).PosSemidef

theorem Matrix.PosSemidef.colMulConjTransposeCol {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (x : n → 𝕜) : (col (Fin 1) x * (col (Fin 1) x).conjTranspose).PosSemidef

theorem Matrix.PosSemidef.mulConjTransposeSelf {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) : (A * A.conjTranspose).PosSemidef

Alias of Matrix.posSemidef_self_mul_conjTranspose.

---

A matrix multiplied by its conjugate transpose is positive semidefinite