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.conj_transpose_eq_adjoint
{𝕜 : Type u_1}
{m : Type u_2}
{n : Type u_3}
[fintype m]
[decidable_eq m]
[fintype n]
[decidable_eq n]
[is_R_or_C 𝕜]
(A : matrix m n 𝕜) :
The adjoint of the linear map associated to a matrix is the linear map associated to the conjugate transpose of that matrix.
theorem
matrix.pos_semidef.star_mul_self
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{n : Type u_1}
[fintype n]
(x : matrix n n 𝕜) :
(x.conj_transpose.mul x).pos_semidef
theorem
matrix.pos_semidef.mul_star_self
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
(x : matrix n n 𝕜) :
(x.mul x.conj_transpose).pos_semidef
theorem
matrix.to_euclidean_lin_eq_pi_Lp_linear_equiv
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
(x : matrix n n 𝕜) :
⇑matrix.to_euclidean_lin x = ⇑((pi_Lp.linear_equiv 2 𝕜 (λ (_x : n), 𝕜)).symm.conj) (⇑matrix.to_lin' x)
theorem
matrix.pos_semidef_eq_linear_map_positive
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
(x : matrix n n 𝕜) :
theorem
matrix.pos_semidef_iff
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
(x : matrix n n 𝕜) :
x.pos_semidef ↔ ∃ (y : matrix n n 𝕜), x = y.conj_transpose.mul y
theorem
matrix.dot_product_eq_inner
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{n : Type u_1}
[fintype n]
(x y : n → 𝕜) :
matrix.dot_product (has_star.star x) y = finset.univ.sum (λ (i : n), has_inner.inner (x i) (y i))
theorem
matrix.pos_semidef.invertible_iff_pos_def
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{n : Type u_1}
[fintype n]
[decidable_eq n]
{x : matrix n n 𝕜}
(hx : x.pos_semidef) :
theorem
matrix.is_hermitian_self_mul_conj_transpose
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
(A : matrix n n 𝕜) :
(A.conj_transpose.mul A).is_hermitian
theorem
matrix.nonneg_eigenvalues_of_pos_semidef
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
{μ : ℝ}
{A : matrix n n 𝕜}
(hμ : module.End.has_eigenvalue (⇑matrix.to_euclidean_lin A) ↑μ)
(H : A.pos_semidef) :
0 ≤ μ
theorem
matrix.is_hermitian.nonneg_eigenvalues_of_pos_semidef
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
{A : matrix n n 𝕜}
(hA : A.pos_semidef)
(i : n) :
0 ≤ _.eigenvalues i
@[instance]
noncomputable
def
matrix.pos_def.invertible
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
{Q : matrix n n 𝕜}
(hQ : Q.pos_def) :
Equations
- hQ.invertible = _.invertible
theorem
matrix.to_lin_pi_Lp_eq_to_lin'
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{n : Type u_1}
[fintype n]
[decidable_eq n] :
matrix.to_lin (pi_Lp.basis_fun 2 𝕜 n) (pi_Lp.basis_fun 2 𝕜 n) = matrix.to_lin'
theorem
matrix.pos_semidef_iff_eq_rank_one
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{n : ℕ}
[decidable_eq 𝕜]
{x : matrix (fin n) (fin n) 𝕜} :
x.pos_semidef ↔ ∃ (m : ℕ) (v : fin m → euclidean_space 𝕜 (fin n)), x = finset.univ.sum (λ (i : fin m), ⇑linear_map.to_matrix' ↑(rank_one (v i) (v i)))
theorem
matrix.pos_semidef_iff_col_mul_conj_transpose_col
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
(x : matrix n n 𝕜) :
x.pos_semidef ↔ ∃ (v : n → n → 𝕜), finset.univ.sum (λ (i : n), (matrix.col (v i)).mul (matrix.col (v i)).conj_transpose) = x
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
vec_mul_vec.pos_semidef
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
(x : n → 𝕜) :
def
linear_map.positive_map
{M₁ : Type u_4}
{M₂ : Type u_5}
[normed_add_comm_group M₁]
[normed_add_comm_group M₂]
[inner_product_space ℂ M₁]
[inner_product_space ℂ M₂]
(T : (M₁ →ₗ[ℂ] M₁) →ₗ[ℂ] M₂ →ₗ[ℂ] M₂) :
Prop
we say a linear map $T \colon L(M_1) \to L(M_2)$ is a positive map if for all positive $x \in L(M_1)$, we also get $T(x)$ is positive
Equations
- T.positive_map = ∀ (x : M₁ →ₗ[ℂ] M₁), x.is_positive → (⇑T x).is_positive
theorem
linear_map.positive_map.star_hom
{M₁ : Type u_4}
{M₂ : Type u_5}
[normed_add_comm_group M₁]
[normed_add_comm_group M₂]
[inner_product_space ℂ M₁]
[inner_product_space ℂ M₂]
{n₁ : ℕ}
[finite_dimensional ℂ M₁]
[finite_dimensional ℂ M₂]
(hn₁ : finite_dimensional.finrank ℂ M₁ = n₁)
(φ : (M₁ →ₗ[ℂ] M₁) →⋆ₐ[ℂ] M₂ →ₗ[ℂ] M₂) :
a $^*$-homomorphism from $L(M_1)$ to $L(M_2)$ is a positive map
theorem
matrix.pos_def_one
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n] :
1.pos_def
the identity is a positive definite matrix
theorem
matrix.pos_def.pos_eigenvalues
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq 𝕜]
[decidable_eq n]
{A : matrix n n 𝕜}
(hA : A.pos_def)
(i : n) :
0 < _.eigenvalues i
each eigenvalue of a positive definite matrix is positive
theorem
matrix.pos_def.pos_trace
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
[nonempty n]
{x : matrix n n 𝕜}
(hx : x.pos_def) :
0 < ⇑is_R_or_C.re x.trace
theorem
matrix.pos_def.trace_ne_zero
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[nonempty n]
[decidable_eq 𝕜]
{x : matrix n n 𝕜}
(hx : x.pos_def) :
the trace of a positive definite matrix is non-zero
theorem
pos_semidef.complex
{n : Type u_1}
[fintype n]
[decidable_eq n]
(x : matrix n n ℂ) :
x.pos_semidef ↔ ∀ (y : n → ℂ), 0 ≤ matrix.dot_product (has_star.star y) (x.mul_vec y)
theorem
std_basis_matrix.sum_eq_one
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
(a : 𝕜) :
finset.univ.sum (λ (k : n), matrix.std_basis_matrix k k a) = a • 1
theorem
std_basis_matrix_mul
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
(i j k l : n)
(a b : 𝕜) :
(matrix.std_basis_matrix i j a).mul (matrix.std_basis_matrix k l b) = ite (j = k) 1 0 • matrix.std_basis_matrix i l (a * b)
theorem
matrix.smul_std_basis_matrix'
{n : Type u_1}
{R : Type u_2}
[comm_semiring R]
[decidable_eq n]
(i j : n)
(c : R) :
matrix.std_basis_matrix i j c = c • matrix.std_basis_matrix i j 1
theorem
matrix.std_basis_matrix.trace
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
(i j : n)
(a : 𝕜) :
(matrix.std_basis_matrix i j a).trace = ite (i = j) a 0
theorem
matrix.std_basis_matrix_eq
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{n : Type u_1}
[decidable_eq n]
(i j : n)
(a : 𝕜) :
theorem
vec_mul_vec_eq_zero_iff
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
(x : n → 𝕜) :
matrix.vec_mul_vec x (has_star.star x) = 0 ↔ x = 0
theorem
matrix.pos_def.diagonal
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
(x : n → 𝕜) :
(matrix.diagonal x).pos_def ↔ ∀ (i : n), 0 < ⇑is_R_or_C.re (x i) ∧ ↑(⇑is_R_or_C.re (x i)) = x i
theorem
matrix.pos_semidef.diagonal
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
(x : n → 𝕜) :
(matrix.diagonal x).pos_semidef ↔ ∀ (i : n), 0 ≤ ⇑is_R_or_C.re (x i) ∧ ↑(⇑is_R_or_C.re (x i)) = x i
theorem
matrix.trace_conj_transpose_mul_self_re_nonneg
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
(x : matrix n n 𝕜) :
0 ≤ ⇑is_R_or_C.re (x.conj_transpose.mul x).trace
theorem
matrix.pos_semidef.trace_conj_transpose_mul_self_nonneg
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
{Q : matrix n n 𝕜}
(x : matrix n n 𝕜)
(hQ : Q.pos_semidef) :
↑(⇑is_R_or_C.re ((Q.mul x.conj_transpose).mul x).trace) = ((Q.mul x.conj_transpose).mul x).trace ∧ 0 ≤ ⇑is_R_or_C.re ((Q.mul x.conj_transpose).mul x).trace
theorem
matrix.nontracial.trace_conj_transpose_mul_self_re_nonneg
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
{Q : matrix n n 𝕜}
(x : matrix n n 𝕜)
(hQ : Q.pos_def) :
0 ≤ ⇑is_R_or_C.re ((Q.mul x.conj_transpose).mul x).trace
given a positive definite matrix $Q$, we have $0\leq\Re(\textnormal{Tr}(Qx^*x))$ for any matrix $x$
theorem
matrix.nontracial.trace_conj_transpose_mul_self_eq_zero
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
{x Q : matrix n n 𝕜}
(hQ : Q.pos_def) :
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.is_hermitian.trace_conj_symm_star_mul
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
{Q : matrix n n 𝕜}
(hQ : Q.is_hermitian)
(x y : matrix n n 𝕜) :
⇑(star_ring_end 𝕜) ((Q.mul y.conj_transpose).mul x).trace = ((Q.mul x.conj_transpose).mul y).trace
theorem
matrix.pos_semidef_smul_iff
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
{x : matrix n n 𝕜}
(hx : x.pos_semidef)
(α : nnreal) :
(↑↑α • x).pos_semidef
theorem
rank_one.euclidean_space.to_matrix'
{𝕜 : Type u_1}
[is_R_or_C 𝕜]
{n : Type u_2}
[fintype n]
[decidable_eq n]
(x y : euclidean_space 𝕜 n) :
⇑linear_map.to_matrix' ↑(rank_one x y) = (matrix.col x).mul (matrix.col y).conj_transpose
theorem
matrix.pos_semidef.col_mul_conj_transpose_col
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
(x : n → 𝕜) :
((matrix.col x).mul (matrix.col x).conj_transpose).pos_semidef
theorem
matrix.pos_semidef.mul_conj_transpose_self
{𝕜 : Type u_1}
{n₁ : Type u_2}
{n₂ : Type u_3}
[is_R_or_C 𝕜]
[fintype n₁]
[fintype n₂]
(x : matrix n₁ n₂ 𝕜) :
(x.mul x.conj_transpose).pos_semidef