Theorem: Matrix.LogDetAtom.optimality_Ddet_le_Adet (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
⊢ D.det ≤ A.det
Tactic:
by_cases h_nonempty : Nonempty n
State after:
case pos
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_nonempty : Nonempty n
⊢ D.det ≤ A.det

case neg
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_nonempty : ¬Nonempty n
⊢ D.det ≤ A.det

State before:
case pos
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_nonempty : Nonempty n
⊢ D.det ≤ A.det

case neg
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_nonempty : ¬Nonempty n
⊢ D.det ≤ A.det
Tactic:
{ have h_D_pd : D.PosDef := LogDetAtom.optimality_D_posdef ht hD hZ hPSD
  haveI h_D_invertible : Invertible D := h_D_pd.Invertible
  have h_Zdet : Z.det = D.det := by
  { rw [hZ, det_of_upperTriangular (upperTriangular_toUpperTri Y), hD, det_diagonal]
    simp [toUpperTri] }
  have h_ZDZ_semidef : (Zᴴ * D⁻¹ * Z).PosSemidef :=
    PosSemidef.conjTranspose_mul_mul D⁻¹ Z h_D_pd.nonsingular_inv.posSemidef
  have h_AZDZ_semidef : (A - Zᴴ * D⁻¹ * Z).PosSemidef :=
    (PosSemidef.fromBlocks₁₁ Z A h_D_pd).1 hPSD
  show D.det ≤ A.det
  { apply le_of_add_le_of_nonneg_left _ h_AZDZ_semidef.det_nonneg
    simpa [h_Zdet] using det_add_det_le_det_add _ _ h_ZDZ_semidef h_AZDZ_semidef } }
State after:
case neg
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_nonempty : ¬Nonempty n
⊢ D.det ≤ A.det

State before:
case neg
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_nonempty : ¬Nonempty n
⊢ D.det ≤ A.det
Tactic:
{ haveI h_empty := not_nonempty_iff.1 h_nonempty
  simp [Matrix.det_isEmpty] }
State after:
no goals

State before:
case pos
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_nonempty : Nonempty n
⊢ D.det ≤ A.det
Tactic:
have h_D_pd : D.PosDef := LogDetAtom.optimality_D_posdef ht hD hZ hPSD
State after:
case pos
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_nonempty : Nonempty n
h_D_pd : D.PosDef
⊢ D.det ≤ A.det

State before:
case pos
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_nonempty : Nonempty n
h_D_pd : D.PosDef
⊢ D.det ≤ A.det
Tactic:
haveI h_D_invertible : Invertible D := h_D_pd.Invertible
State after:
case pos
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_nonempty : Nonempty n
h_D_pd : D.PosDef
h_D_invertible : Invertible D
⊢ D.det ≤ A.det

State before:
case pos
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_nonempty : Nonempty n
h_D_pd : D.PosDef
h_D_invertible : Invertible D
⊢ D.det ≤ A.det
Tactic:
have h_Zdet : Z.det = D.det := by
{ rw [hZ, det_of_upperTriangular (upperTriangular_toUpperTri Y), hD, det_diagonal]
  simp [toUpperTri] }
State after:
case pos
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_nonempty : Nonempty n
h_D_pd : D.PosDef
h_D_invertible : Invertible D
h_Zdet : Z.det = D.det
⊢ D.det ≤ A.det

State before:
case pos
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_nonempty : Nonempty n
h_D_pd : D.PosDef
h_D_invertible : Invertible D
h_Zdet : Z.det = D.det
⊢ D.det ≤ A.det
Tactic:
have h_ZDZ_semidef : (Zᴴ * D⁻¹ * Z).PosSemidef :=
  PosSemidef.conjTranspose_mul_mul D⁻¹ Z h_D_pd.nonsingular_inv.posSemidef
State after:
case pos
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_nonempty : Nonempty n
h_D_pd : D.PosDef
h_D_invertible : Invertible D
h_Zdet : Z.det = D.det
h_ZDZ_semidef : (Z.conjTranspose * D⁻¹ * Z).PosSemidef
⊢ D.det ≤ A.det

State before:
case pos
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_nonempty : Nonempty n
h_D_pd : D.PosDef
h_D_invertible : Invertible D
h_Zdet : Z.det = D.det
h_ZDZ_semidef : (Z.conjTranspose * D⁻¹ * Z).PosSemidef
⊢ D.det ≤ A.det
Tactic:
have h_AZDZ_semidef : (A - Zᴴ * D⁻¹ * Z).PosSemidef :=
  (PosSemidef.fromBlocks₁₁ Z A h_D_pd).1 hPSD
State after:
case pos
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_nonempty : Nonempty n
h_D_pd : D.PosDef
h_D_invertible : Invertible D
h_Zdet : Z.det = D.det
h_ZDZ_semidef : (Z.conjTranspose * D⁻¹ * Z).PosSemidef
h_AZDZ_semidef : (A - Z.conjTranspose * D⁻¹ * Z).PosSemidef
⊢ D.det ≤ A.det

State before:
case pos
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_nonempty : Nonempty n
h_D_pd : D.PosDef
h_D_invertible : Invertible D
h_Zdet : Z.det = D.det
h_ZDZ_semidef : (Z.conjTranspose * D⁻¹ * Z).PosSemidef
h_AZDZ_semidef : (A - Z.conjTranspose * D⁻¹ * Z).PosSemidef
⊢ D.det ≤ A.det
Tactic:
{ apply le_of_add_le_of_nonneg_left _ h_AZDZ_semidef.det_nonneg
  simpa [h_Zdet] using det_add_det_le_det_add _ _ h_ZDZ_semidef h_AZDZ_semidef }
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
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_nonempty : Nonempty n
h_D_pd : D.PosDef
h_D_invertible : Invertible D
⊢ Z.det = D.det
Tactic:
rw [hZ, det_of_upperTriangular (upperTriangular_toUpperTri Y), hD, det_diagonal]
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_nonempty : Nonempty n
h_D_pd : D.PosDef
h_D_invertible : Invertible D
⊢ ∏ i : n, Y.toUpperTri i i = ∏ i : n, Y.diag i

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_nonempty : Nonempty n
h_D_pd : D.PosDef
h_D_invertible : Invertible D
⊢ ∏ i : n, Y.toUpperTri i i = ∏ i : n, Y.diag i
Tactic:
simp [toUpperTri]
State after:
no goals

State before:
case pos
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_nonempty : Nonempty n
h_D_pd : D.PosDef
h_D_invertible : Invertible D
h_Zdet : Z.det = D.det
h_ZDZ_semidef : (Z.conjTranspose * D⁻¹ * Z).PosSemidef
h_AZDZ_semidef : (A - Z.conjTranspose * D⁻¹ * Z).PosSemidef
⊢ D.det ≤ A.det
Tactic:
apply le_of_add_le_of_nonneg_left _ h_AZDZ_semidef.det_nonneg
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_nonempty : Nonempty n
h_D_pd : D.PosDef
h_D_invertible : Invertible D
h_Zdet : Z.det = D.det
h_ZDZ_semidef : (Z.conjTranspose * D⁻¹ * Z).PosSemidef
h_AZDZ_semidef : (A - Z.conjTranspose * D⁻¹ * Z).PosSemidef
⊢ D.det + (A - Z.conjTranspose * D⁻¹ * Z).det ≤ 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_nonempty : Nonempty n
h_D_pd : D.PosDef
h_D_invertible : Invertible D
h_Zdet : Z.det = D.det
h_ZDZ_semidef : (Z.conjTranspose * D⁻¹ * Z).PosSemidef
h_AZDZ_semidef : (A - Z.conjTranspose * D⁻¹ * Z).PosSemidef
⊢ D.det + (A - Z.conjTranspose * D⁻¹ * Z).det ≤ A.det
Tactic:
simpa [h_Zdet] using det_add_det_le_det_add _ _ h_ZDZ_semidef h_AZDZ_semidef
State after:
no goals

State before:
case neg
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_nonempty : ¬Nonempty n
⊢ D.det ≤ A.det
Tactic:
haveI h_empty := not_nonempty_iff.1 h_nonempty
State after:
case neg
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_nonempty : ¬Nonempty n
h_empty : IsEmpty n
⊢ D.det ≤ A.det

State before:
case neg
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_nonempty : ¬Nonempty n
h_empty : IsEmpty n
⊢ D.det ≤ A.det
Tactic:
simp [Matrix.det_isEmpty]
State after:
no goals