internlm/Lean-Github huggingface dataset:
Theorem: Matrix.LogDetAtom.optimality_Ddet_le_Adet
Proof 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
Proof 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
Theorem: Matrix.LogDetAtom.optimality_Ddet_le_Adet
Proof 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] }
Proof 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
Theorem: Matrix.LogDetAtom.optimality_Ddet_le_Adet
Proof 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
Proof 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
Theorem: Matrix.LogDetAtom.optimality_Ddet_le_Adet
Proof 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
Proof 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
Theorem: Matrix.LogDetAtom.optimality_Ddet_le_Adet
Proof 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 }
Proof state after:
no goals
Theorem: Matrix.LogDetAtom.optimality_Ddet_le_Adet
Proof 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]
Proof 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
Theorem: Matrix.LogDetAtom.optimality_Ddet_le_Adet
Proof 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]
Proof state after:
no goals
Theorem: Matrix.LogDetAtom.optimality_Ddet_le_Adet
Proof 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
Proof 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
Theorem: Matrix.LogDetAtom.optimality_Ddet_le_Adet
Proof 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
Proof state after:
no goals
Theorem: Matrix.LogDetAtom.optimality_Ddet_le_Adet
Proof 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
Proof 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
Theorem: Matrix.LogDetAtom.optimality_Ddet_le_Adet
Proof 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]
Proof state after:
no goals
Theorem: Matrix.LogDetAtom.cond_elim
Proof 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
Proof 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
Theorem: Matrix.LogDetAtom.cond_elim
Proof 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
Proof 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
Theorem: Matrix.LogDetAtom.cond_elim
Proof 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
Proof 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
Theorem: Matrix.LogDetAtom.cond_elim
Proof 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
Proof 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
Theorem: Matrix.LogDetAtom.cond_elim
Proof 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]
Proof 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
Theorem: Matrix.LogDetAtom.cond_elim
Proof 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
Proof state after:
no goals
Theorem: Matrix.LogDetAtom.optimality
Proof 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
Proof 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
Theorem: Matrix.LogDetAtom.optimality
Proof 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
Proof 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
Theorem: Matrix.LogDetAtom.optimality
Proof 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
Proof 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
Theorem: Matrix.LogDetAtom.optimality
Proof 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]
Proof 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
Theorem: Matrix.LogDetAtom.optimality
Proof 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))
Proof 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
Theorem: Matrix.LogDetAtom.optimality
Proof 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
Proof 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
Theorem: Matrix.LogDetAtom.optimality
Proof 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]
Proof state after:
no goals
Theorem: Module.End.eigenspace_add
Proof state before:
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f g : End R M
a b : R
⊢ f.eigenspace a ⊓ g.eigenspace b ≤ (f + g).eigenspace (a + b)
Tactic:
rintro x ⟨hf, hg⟩
Proof state after:
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f g : End R M
a b : R
x : M
hf : x ∈ ↑(f.eigenspace a)
hg : x ∈ ↑(g.eigenspace b)
⊢ x ∈ (f + g).eigenspace (a + b)
Theorem: Module.End.eigenspace_add
Proof state before:
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f g : End R M
a b : R
x : M
hf : x ∈ ↑(f.eigenspace a)
hg : x ∈ ↑(g.eigenspace b)
⊢ x ∈ (f + g).eigenspace (a + b)
Tactic:
simp only [eigenspace, SetLike.mem_coe, LinearMap.mem_ker,
  LinearMap.sub_apply, algebraMap_end_apply] at hf hg
Proof state after:
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f g : End R M
a b : R
x : M
hf : f x - a • x = 0
hg : g x - b • x = 0
⊢ x ∈ (f + g).eigenspace (a + b)
Theorem: Module.End.eigenspace_add
Proof state before:
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f g : End R M
a b : R
x : M
hf : f x - a • x = 0
hg : g x - b • x = 0
⊢ x ∈ (f + g).eigenspace (a + b)
Tactic:
simp only [eigenspace, map_add, LinearMap.mem_ker, LinearMap.sub_apply,
  LinearMap.add_apply, algebraMap_end_apply]
Proof state after:
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f g : End R M
a b : R
x : M
hf : f x - a • x = 0
hg : g x - b • x = 0
⊢ f x + g x - (a • x + b • x) = 0
Theorem: Module.End.eigenspace_add
Proof state before:
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f g : End R M
a b : R
x : M
hf : f x - a • x = 0
hg : g x - b • x = 0
⊢ f x + g x - (a • x + b • x) = 0
Tactic:
rw [← add_sub, add_comm (a • x), ← sub_sub, hg, add_sub, add_zero, hf]
Proof state after:
no goals
Theorem: Module.End.eigenspace_one
Proof state before:
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ eigenspace 1 1 = ⊤
Tactic:
apply eq_top_iff.2
Proof state after:
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ⊤ ≤ eigenspace 1 1