Theorem: Matrix.LogDetAtom.cond_elim (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
t : n → ℝ
Y Z D : Matrix n n ℝ
ht : ∀ (i : n), (t i).exp ≤ Y.diag i
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hPSD : (D.fromBlocks Z Z.transpose A).PosSemidef
⊢ A.PosDef
Tactic:
have h_D_pd : D.PosDef := LogDetAtom.optimality_D_posdef ht hD hZ hPSD
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
t : n → ℝ
Y Z D : Matrix n n ℝ
ht : ∀ (i : n), (t i).exp ≤ Y.diag i
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hPSD : (D.fromBlocks Z Z.transpose A).PosSemidef
h_D_pd : D.PosDef
⊢ A.PosDef

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
t : n → ℝ
Y Z D : Matrix n n ℝ
ht : ∀ (i : n), (t i).exp ≤ Y.diag i
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hPSD : (D.fromBlocks Z Z.transpose A).PosSemidef
h_D_pd : D.PosDef
⊢ A.PosDef
Tactic:
have h_A_psd : A.PosSemidef := PosSemidef₂₂_of_PosSemidef_toBlock hPSD
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
t : n → ℝ
Y Z D : Matrix n n ℝ
ht : ∀ (i : n), (t i).exp ≤ Y.diag i
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hPSD : (D.fromBlocks Z Z.transpose A).PosSemidef
h_D_pd : D.PosDef
h_A_psd : A.PosSemidef
⊢ A.PosDef

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
t : n → ℝ
Y Z D : Matrix n n ℝ
ht : ∀ (i : n), (t i).exp ≤ Y.diag i
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hPSD : (D.fromBlocks Z Z.transpose A).PosSemidef
h_D_pd : D.PosDef
h_A_psd : A.PosSemidef
⊢ A.PosDef
Tactic:
have h_Ddet_le_Adet : D.det ≤ A.det := LogDetAtom.optimality_Ddet_le_Adet ht hD hZ hPSD
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
t : n → ℝ
Y Z D : Matrix n n ℝ
ht : ∀ (i : n), (t i).exp ≤ Y.diag i
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hPSD : (D.fromBlocks Z Z.transpose A).PosSemidef
h_D_pd : D.PosDef
h_A_psd : A.PosSemidef
h_Ddet_le_Adet : D.det ≤ A.det
⊢ A.PosDef

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
t : n → ℝ
Y Z D : Matrix n n ℝ
ht : ∀ (i : n), (t i).exp ≤ Y.diag i
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hPSD : (D.fromBlocks Z Z.transpose A).PosSemidef
h_D_pd : D.PosDef
h_A_psd : A.PosSemidef
h_Ddet_le_Adet : D.det ≤ A.det
⊢ A.PosDef
Tactic:
have h_Adet_pos : 0 < A.det := lt_of_lt_of_le h_D_pd.det_pos h_Ddet_le_Adet
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
t : n → ℝ
Y Z D : Matrix n n ℝ
ht : ∀ (i : n), (t i).exp ≤ Y.diag i
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hPSD : (D.fromBlocks Z Z.transpose A).PosSemidef
h_D_pd : D.PosDef
h_A_psd : A.PosSemidef
h_Ddet_le_Adet : D.det ≤ A.det
h_Adet_pos : 0 < A.det
⊢ A.PosDef

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
t : n → ℝ
Y Z D : Matrix n n ℝ
ht : ∀ (i : n), (t i).exp ≤ Y.diag i
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hPSD : (D.fromBlocks Z Z.transpose A).PosSemidef
h_D_pd : D.PosDef
h_A_psd : A.PosSemidef
h_Ddet_le_Adet : D.det ≤ A.det
h_Adet_pos : 0 < A.det
⊢ A.PosDef
Tactic:
rw [h_A_psd.PosDef_iff_det_ne_zero]
State after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
t : n → ℝ
Y Z D : Matrix n n ℝ
ht : ∀ (i : n), (t i).exp ≤ Y.diag i
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hPSD : (D.fromBlocks Z Z.transpose A).PosSemidef
h_D_pd : D.PosDef
h_A_psd : A.PosSemidef
h_Ddet_le_Adet : D.det ≤ A.det
h_Adet_pos : 0 < A.det
⊢ A.det ≠ 0

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
t : n → ℝ
Y Z D : Matrix n n ℝ
ht : ∀ (i : n), (t i).exp ≤ Y.diag i
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hPSD : (D.fromBlocks Z Z.transpose A).PosSemidef
h_D_pd : D.PosDef
h_A_psd : A.PosSemidef
h_Ddet_le_Adet : D.det ≤ A.det
h_Adet_pos : 0 < A.det
⊢ A.det ≠ 0
Tactic:
apply ne_of_gt h_Adet_pos
State after:
no goals