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 : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef
Tactic:
have h_D_eq : D = Z * A⁻¹ * Zᴴ :=
  calc D
    = D * D⁻¹ * D := by
        rw [hD, Matrix.mul_inv_of_invertible, Matrix.one_mul]
  _ = D * (LDL.lowerInv hA * A * (LDL.lowerInv hA)ᵀ)⁻¹ * Dᵀ := by
        erw [hD, LDL.diag, diagonal_transpose, ← LDL.diag, LDL.diag_eq_lowerInv_conj]
        rfl
  _ = D * (LDL.lower hA)ᵀ * A⁻¹ * (D * (LDL.lower hA)ᵀ)ᵀ := by
        simp only [hD, LDL.lower, transpose_mul, transpose_transpose, transpose_nonsing_inv,
          Matrix.mul_assoc, Matrix.mul_inv_rev]
  _ = Z * A⁻¹ * Zᴴ := by
        rw [hZ, hD]; rfl
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 : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
h_D_eq : D = Z * A⁻¹ * Z.conjTranspose
⊢ (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 : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
h_D_eq : D = Z * A⁻¹ * Z.conjTranspose
⊢ (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 : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
h_D_eq : D = Z * A⁻¹ * Z.conjTranspose
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 : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
h_D_eq : D = Z * A⁻¹ * Z.conjTranspose
this : Invertible A
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef
Tactic:
erw [PosSemidef.fromBlocks₂₂ _ _ hA]
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 : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
h_D_eq : D = Z * A⁻¹ * Z.conjTranspose
this : Invertible A
⊢ (D - Z * A⁻¹ * Z.conjTranspose).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 : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
h_D_eq : D = Z * A⁻¹ * Z.conjTranspose
this : Invertible A
⊢ (D - Z * A⁻¹ * Z.conjTranspose).PosSemidef
Tactic:
simp [h_D_eq]
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 : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ D = D * D⁻¹ * D
Tactic:
rw [hD, Matrix.mul_inv_of_invertible, Matrix.one_mul]
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 : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ D * D⁻¹ * D = D * (LDL.lowerInv hA * A * (LDL.lowerInv hA).transpose)⁻¹ * D.transpose
Tactic:
erw [hD, LDL.diag, diagonal_transpose, ← LDL.diag, LDL.diag_eq_lowerInv_conj]
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 : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose * (LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose)⁻¹ *
      (LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose) =
    LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose * (LDL.lowerInv hA * A * (LDL.lowerInv hA).transpose)⁻¹ *
      (LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose)

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 : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose * (LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose)⁻¹ *
      (LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose) =
    LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose * (LDL.lowerInv hA * A * (LDL.lowerInv hA).transpose)⁻¹ *
      (LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose)
Tactic:
rfl
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 : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ D * (LDL.lowerInv hA * A * (LDL.lowerInv hA).transpose)⁻¹ * D.transpose =
    D * (LDL.lower hA).transpose * A⁻¹ * (D * (LDL.lower hA).transpose).transpose
Tactic:
simp only [hD, LDL.lower, transpose_mul, transpose_transpose, transpose_nonsing_inv,
  Matrix.mul_assoc, Matrix.mul_inv_rev]
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 : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ D * (LDL.lower hA).transpose * A⁻¹ * (D * (LDL.lower hA).transpose).transpose = Z * A⁻¹ * Z.conjTranspose
Tactic:
rw [hZ, hD]
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 : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ LDL.diag hA * (LDL.lower hA).transpose * A⁻¹ * (LDL.diag hA * (LDL.lower hA).transpose).transpose =
    LDL.diag hA * (LDL.lower hA).transpose * A⁻¹ * (LDL.diag hA * (LDL.lower hA).transpose).conjTranspose

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 : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ LDL.diag hA * (LDL.lower hA).transpose * A⁻¹ * (LDL.diag hA * (LDL.lower hA).transpose).transpose =
    LDL.diag hA * (LDL.lower hA).transpose * A⁻¹ * (LDL.diag hA * (LDL.lower hA).transpose).conjTranspose
Tactic:
rfl
State after:
no goals