Theorem: Matrix.LogDetAtom.feasibility_PosDef' (CvxLean/Lib/Math/LogDet.lean)

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef
Tactic:
have hY_tri : upperTriangular Y := by
{ rw [hY]
  apply upperTriangular.mul
  apply BlockTriangular_diagonal
  apply lowerTriangular.transpose
  apply LDL.lowerTriangular_lower }
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef
Tactic:
haveI := hA.Invertible
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
this : Invertible A
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
this : Invertible A
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef
Tactic:
rw [hZ, hY_tri.toUpperTri_eq]
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
this : Invertible A
⊢ (D.fromBlocks Y Y.transpose A).PosSemidef

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
this : Invertible A
⊢ (D.fromBlocks Y Y.transpose A).PosSemidef
Tactic:
apply LogDetAtom.feasibility_PosDef _ _ hY
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
this : Invertible A
⊢ D = LDL.diag hA

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
this : Invertible A
⊢ D = LDL.diag hA
Tactic:
simp [hD, hY, LDL.diag]
State after:
no goals

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ Y.upperTriangular
Tactic:
rw [hY]
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.diag hA * (LDL.lower hA).transpose).upperTriangular

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.diag hA * (LDL.lower hA).transpose).upperTriangular
Tactic:
apply upperTriangular.mul
State after:
case hM
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.diag hA).upperTriangular

case hN
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.lower hA).transpose.upperTriangular

State before:
case hM
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.diag hA).upperTriangular

case hN
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.lower hA).transpose.upperTriangular
Tactic:
apply BlockTriangular_diagonal
State after:
case hN
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.lower hA).transpose.upperTriangular

State before:
case hN
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.lower hA).transpose.upperTriangular
Tactic:
apply lowerTriangular.transpose
State after:
case hN.hM
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.lower hA).lowerTriangular

State before:
case hN.hM
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.lower hA).lowerTriangular
Tactic:
apply LDL.lowerTriangular_lower
State after:
no goals