Positivity of matrices and linear maps

Compatibility wrappers for the part of Monlib's matrix-positive API now covered by Mathlib.

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

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

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

Alias of Matrix.posSemidef_conjTranspose_mul_self.

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

Alias of Matrix.posSemidef_self_mul_conjTranspose.

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

theorem Matrix.of_isHermitian' {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype 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] (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_3} [Fintype n] (x y : n → 𝕜) : star x ⬝ᵥ y = ∑ i : n, inner 𝕜 (x i) (y i)

theorem Matrix.isHermitian_self_hMul_conjTranspose {𝕜 : Type u_2} [RCLike 𝕜] {m : Type u_3} {n : Type u_4} [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

@[reducible]

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

A matrix is invertible when its associated linear map is bijective.

Equations

• Matrix.invertibleOfBijToLin' 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)

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

@[reducible]

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

A positive definite matrix is invertible.

Equations

• hQ.invertible = ⋯.invertible

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

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

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

The identity is a positive definite matrix.

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

Alias of Matrix.PosDef.eigenvalues_pos.

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

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

A positive definite matrix has trace with positive real part.

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

The Euclidean linear map associated to a matrix acts by matrix-vector multiplication.

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

theorem rankOne.EuclideanSpace.toMatrix' {𝕜 : Type u_3} [RCLike 𝕜] {n : Type u_4} {m : Type u_5} [Fintype n] [Fintype m] [DecidableEq m] (x : EuclideanSpace 𝕜 n) (y : EuclideanSpace 𝕜 m) : Matrix.toEuclideanLin.symm ↑(((rankOne 𝕜) x) y) = Matrix.replicateCol (Fin 1) x.ofLp * (Matrix.replicateCol (Fin 1) y.ofLp).conjTranspose

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

theorem Matrix.vecMulVec_eq_replicateCol_conjTranspose {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] (v : n → 𝕜) : vecMulVec v (star v) = replicateCol (Fin 1) v * (replicateCol (Fin 1) v).conjTranspose

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

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

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

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, toEuclideanLin.symm ↑(((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, toEuclideanLin.symm ↑(((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, toEuclideanLin.symm ↑(((rankOne 𝕜) ((EuclideanSpace.equiv n 𝕜).symm (v i))) ((EuclideanSpace.equiv n 𝕜).symm (v i)))

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

For complex matrices, positive semidefiniteness is equivalent to nonnegative quadratic forms.

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

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

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

theorem Matrix.smul_single' {n : Type u_3} {R : Type u_4} [CommSemiring R] [DecidableEq n] (i j : n) (c : R) : single i j c = c • single 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.single.trace {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (i j : n) (a : 𝕜) : (single i j a).trace = if i = j then a else 0

theorem Matrix.single_eq {R : Type u_3} {n : Type u_4} {m : Type u_5} [Semiring R] [DecidableEq n] [DecidableEq m] (i : n) (j : m) (a : R) : single 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 norm_ite {α : Type u_3} [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 𝕜] [DecidableEq n] (x : n → 𝕜) : (diagonal x).PosSemidef ↔ ∀ (i : n), 0 ≤ x i

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

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

theorem Matrix.commute_iff {α : Type u_1} {n : Type u_4} [NonUnitalSemiring α] [StarRing α] [Fintype n] {A B : Matrix n n α} (hA : A.IsHermitian) (hB : B.IsHermitian) : Commute A B ↔ (A * B).IsHermitian

Alias of Matrix.IsHermitian.commute_iff.

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

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

The trace of xᴴ * x is nonnegative.

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

A positive semidefinite matrix gives a nonnegative weighted xᴴ * x trace.

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

The trace of xᴴ * x vanishes exactly when x is zero.

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

A positive definite matrix gives a faithful weighted xᴴ * x trace.

theorem Matrix.Nontracial.trace_conjTranspose_hMul_self_eq_zero {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {m : Type u_3} [Fintype m] [Fintype 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.

---

A positive definite matrix gives a faithful weighted xᴴ * x trace.

theorem Matrix.IsHermitian.trace_conj_symm_star_hMul {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {m : Type u_3} [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

Hermitian weighted traces are conjugate symmetric.

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

xᴴ * x vanishes exactly when x is zero.

theorem Matrix.PosSemidef.replicateColMulConjTransposereplicateCol {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Finite n] (x : n → 𝕜) : (replicateCol (Fin 1) x * (replicateCol (Fin 1) x).conjTranspose).PosSemidef