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 𝕜) :

Matrix.toLin' A.conjTranspose = LinearMap.adjoint (Matrix.toLin' A)

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

source

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

source

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

source

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

Matrix.toEuclideanLin x = Matrix.toLin' x

source

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

source

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

x.PosSemidef ↔ (Matrix.toEuclideanLin x).IsPositive

source

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

source

theorem Matrix.dotProduct_eq_inner {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} [Fintype n] (x : n → 𝕜) (y : n → 𝕜) :

Matrix.dotProduct (star x) y = ∑ i : n, inner (x i) (y i)

source

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 ⇑(Matrix.toLin' x) ↔ x.PosDef

source

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

source

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

star A.trace = A.conjTranspose.trace

source

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 (Matrix.toEuclideanLin A) ↑μ) (H : A.PosSemidef) :

0 ≤ μ

source

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

source

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 ⇑(Matrix.toLin' Q)) :

Invertible Q

Equations

Matrix.invertible_of_bij_toLin' h = ⋯.invertible

Instances For

source

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 ⇑(Matrix.toLin' Q)

source

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' ⋯

source

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)

source

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) :

Matrix.vecMul (∑ i : k, y i) x = ∑ i : k, Matrix.vecMul (y i) x

source

theorem Matrix.toLin_piLp_eq_toLin' {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} [Fintype n] [DecidableEq n] :

Matrix.toLin (PiLp.basisFun 2 𝕜 n) (PiLp.basisFun 2 𝕜 n) = Matrix.toLin'

source

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))

source

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)))

source

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)))

source

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

source

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

source

theorem rankOne.Pi.toMatrix'' {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (x : n → 𝕜) (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

source

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, Matrix.col (Fin 1) (v i) * (Matrix.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$

source

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, Matrix.col (Fin 1) (v i) * (Matrix.col (Fin 1) (v i)).conjTranspose

source

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, Matrix.vecMulVec (v i) (star (v i))

source

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, Matrix.vecMulVec (v i) (star (v i))

source

theorem vecMulVec_posSemidef {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (x : n → 𝕜) :

(Matrix.vecMulVec x (star x)).PosSemidef

source

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

Matrix.PosDef 1

the identity is a positive definite matrix

source

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

source

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

source

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

source

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

(Matrix.toEuclideanLin x) v = x.mulVec v

source

theorem PosSemidef.complex {n : Type u_1} [Fintype n] [DecidableEq n] (x : Matrix n n ℂ) :

x.PosSemidef ↔ ∀ (y : n → ℂ), 0 ≤ Matrix.dotProduct (star y) (x.mulVec y)

source

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

source

theorem stdBasisMatrix_hMul {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (i : n) (j : n) (k : n) (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)

source

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

Matrix.stdBasisMatrix i j c = c • Matrix.stdBasisMatrix i j 1

source

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

source

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

source

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

(Matrix.stdBasisMatrix i j a).trace = if i = j then a else 0

source

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) :

Matrix.stdBasisMatrix i j a = fun (i' : n) (j' : m) => if i = i' ∧ j = j' then a else 0

source

theorem vecMulVec_eq_zero_iff {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] (x : n → 𝕜) :

Matrix.vecMulVec x (star x) = 0 ↔ x = 0

source

theorem Matrix.PosDef.diagonal_iff {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (x : n → 𝕜) :

(Matrix.diagonal x).PosDef ↔ ∀ (i : n), 0 < x i

source

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‖

source

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

(Matrix.diagonal x).PosSemidef ↔ ∀ (i : n), 0 ≤ x i

source

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

source

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$

source

@[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

source

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

source

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$

source

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$

source

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 : Matrix n m 𝕜) (y : Matrix n m 𝕜) :

(starRingEnd 𝕜) (Q * y.conjTranspose * x).trace = (Q * x.conjTranspose * y).trace

source

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

source

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

(↑↑α • x).PosSemidef

source

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

(Matrix.col (Fin 1) x * (Matrix.col (Fin 1) x).conjTranspose).PosSemidef

source

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

Documentation

Monlib.LinearAlgebra.Matrix.PosEqLinearMapIsPositive

the correspondence between matrix.pos_semidef and linear_map.is_positive #