Theorem: Matrix.LogDetAtom.optimality (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
⊢ ∑ i : n, t i ≤ A.det.log
Tactic:
have h_A_pd : A.PosDef := LogDetAtom.cond_elim 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_A_pd : A.PosDef
⊢ ∑ i : n, t i ≤ A.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
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_A_pd : A.PosDef
⊢ ∑ i : n, t i ≤ A.det.log
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_A_pd : A.PosDef
h_Ddet_le_Adet : D.det ≤ A.det
⊢ ∑ i : n, t i ≤ A.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
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_A_pd : A.PosDef
h_Ddet_le_Adet : D.det ≤ A.det
⊢ ∑ i : n, t i ≤ A.det.log
Tactic:
have h_Adet_pos: 0 < A.det := h_A_pd.det_pos
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_A_pd : A.PosDef
h_Ddet_le_Adet : D.det ≤ A.det
h_Adet_pos : 0 < A.det
⊢ ∑ i : n, t i ≤ A.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
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_A_pd : A.PosDef
h_Ddet_le_Adet : D.det ≤ A.det
h_Adet_pos : 0 < A.det
⊢ ∑ i : n, t i ≤ A.det.log
Tactic:
rw [← Real.exp_le_exp, Real.exp_sum, Real.exp_log h_Adet_pos]
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_A_pd : A.PosDef
h_Ddet_le_Adet : D.det ≤ A.det
h_Adet_pos : 0 < A.det
⊢ ∏ x : n, (t x).exp ≤ A.det

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_A_pd : A.PosDef
h_Ddet_le_Adet : D.det ≤ A.det
h_Adet_pos : 0 < A.det
⊢ ∏ x : n, (t x).exp ≤ A.det
Tactic:
apply le_trans (Finset.prod_le_prod (fun i _ => le_of_lt ((t i).exp_pos)) (fun i _ => ht i))
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_A_pd : A.PosDef
h_Ddet_le_Adet : D.det ≤ A.det
h_Adet_pos : 0 < A.det
⊢ ∏ i : n, Y.diag i ≤ A.det

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_A_pd : A.PosDef
h_Ddet_le_Adet : D.det ≤ A.det
h_Adet_pos : 0 < A.det
⊢ ∏ i : n, Y.diag i ≤ A.det
Tactic:
convert h_Ddet_le_Adet
State after:
case h.e'_3
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_A_pd : A.PosDef
h_Ddet_le_Adet : D.det ≤ A.det
h_Adet_pos : 0 < A.det
⊢ ∏ i : n, Y.diag i = D.det

State before:
case h.e'_3
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_A_pd : A.PosDef
h_Ddet_le_Adet : D.det ≤ A.det
h_Adet_pos : 0 < A.det
⊢ ∏ i : n, Y.diag i = D.det
Tactic:
simp [hD]
State after:
no goals