noncomputable def HermitianMat.sqrt {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) : HermitianMat d 𝕜

The square root of a Hermitian matrix. Negative eigenvalues are mapped to zero.

Equations

• A.sqrt = A.cfc Real.sqrt

theorem HermitianMat.sqrt_sq_eq_proj {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) : ↑A.sqrt * ↑A.sqrt = ↑A⁺

theorem HermitianMat.sqrt_sq {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (hA : 0 ≤ A) : ↑A.sqrt * ↑A.sqrt = ↑A

theorem HermitianMat.commute_sqrt_left {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} (hAB : Commute ↑A ↑B) : Commute ↑A.sqrt ↑B

theorem HermitianMat.commute_sqrt_right {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} (hAB : Commute ↑A ↑B) : Commute ↑A ↑B.sqrt

theorem HermitianMat.sqrt_inv_mul_self_mul_sqrt_inv_eq_one {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (hA : (↑A).PosDef) : ↑A⁻¹.sqrt * ↑A * ↑A⁻¹.sqrt = 1

For a positive definite matrix A, A^{-1/2} * A * A^{-1/2} = I.

theorem HermitianMat.sqrt_nonneg {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) : 0 ≤ A.sqrt

theorem HermitianMat.sqrt_pos {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (h : 0 < A) : 0 < A.sqrt

theorem HermitianMat.sqrt_posDef {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (hA : (↑A).PosDef) : (↑A.sqrt).PosDef

def HermitianMat.evalHermitianMatSqrt : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for HermitianMat.sqrt

Equations

• One or more equations did not get rendered due to their size.