Theorem: Matrix.LogDetAtom.solution_eq_atom (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
A : Matrix n n ℝ
hA : A.PosDef
⊢ ∑ i : n, (LDL.diagEntries hA i).log = A.det.log
Tactic:
conv => rhs; rw [(LDL.lower_conj_diag hA).symm]
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA✝ : A✝.PosDef
A : Matrix n n ℝ
hA : A.PosDef
⊢ ∑ i : n, (LDL.diagEntries hA i).log = (LDL.lower hA * LDL.diag hA * (LDL.lower hA).conjTranspose).det.log

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA✝ : A✝.PosDef
A : Matrix n n ℝ
hA : A.PosDef
⊢ ∑ i : n, (LDL.diagEntries hA i).log = (LDL.lower hA * LDL.diag hA * (LDL.lower hA).conjTranspose).det.log
Tactic:
have heqsum := Real.log_prod Finset.univ (LDL.diagEntries hA)
  (fun i _ => ne_of_gt (LDL.diagEntries_pos hA i))
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA✝ : A✝.PosDef
A : Matrix n n ℝ
hA : A.PosDef
heqsum : (∏ i : n, LDL.diagEntries hA i).log = ∑ i : n, (LDL.diagEntries hA i).log
⊢ ∑ i : n, (LDL.diagEntries hA i).log = (LDL.lower hA * LDL.diag hA * (LDL.lower hA).conjTranspose).det.log

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA✝ : A✝.PosDef
A : Matrix n n ℝ
hA : A.PosDef
heqsum : (∏ i : n, LDL.diagEntries hA i).log = ∑ i : n, (LDL.diagEntries hA i).log
⊢ ∑ i : n, (LDL.diagEntries hA i).log = (LDL.lower hA * LDL.diag hA * (LDL.lower hA).conjTranspose).det.log
Tactic:
simp [LDL.diag, heqsum.symm]
State after:
no goals