Theorem: Matrix.PosDef.PosDef_sqrt (CvxLean/Lib/Math/Subadditivity.lean)

State before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosDef
⊢ ⋯.sqrt.PosDef
Tactic:
unfold IsHermitian.sqrt
State after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosDef
⊢ ((⋯.eigenvectorMatrix * diagonal fun i => (⋯.eigenvalues i).sqrt) * ⋯.eigenvectorMatrix.transpose).PosDef

State before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosDef
⊢ ((⋯.eigenvectorMatrix * diagonal fun i => (⋯.eigenvalues i).sqrt) * ⋯.eigenvectorMatrix.transpose).PosDef
Tactic:
refine'
  PosDef.conjTranspose_mul_mul _ (hA.1.eigenvectorMatrixᵀ)
    (PosDef_diagonal (fun i => Real.sqrt_pos.2 (hA.eigenvalues_pos i))) _
State after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosDef
⊢ ⋯.eigenvectorMatrix.transpose.det ≠ 0

State before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosDef
⊢ ⋯.eigenvectorMatrix.transpose.det ≠ 0
Tactic:
rw [det_transpose]
State after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosDef
⊢ ⋯.eigenvectorMatrix.det ≠ 0

State before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosDef
⊢ ⋯.eigenvectorMatrix.det ≠ 0
Tactic:
apply det_ne_zero_of_right_inverse hA.1.eigenvectorMatrix_mul_inv
State after:
no goals