internlm/Lean-Github huggingface dataset:
Theorem: Matrix.LogDetAtom.feasibility_PosDef
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ D * (LDL.lower hA).transpose * A⁻¹ * (D * (LDL.lower hA).transpose).transpose = Z * A⁻¹ * Z.conjTranspose
Tactic:
rw [hZ, hD]
Proof state after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ LDL.diag hA * (LDL.lower hA).transpose * A⁻¹ * (LDL.diag hA * (LDL.lower hA).transpose).transpose =
    LDL.diag hA * (LDL.lower hA).transpose * A⁻¹ * (LDL.diag hA * (LDL.lower hA).transpose).conjTranspose
Theorem: Matrix.LogDetAtom.feasibility_PosDef
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ LDL.diag hA * (LDL.lower hA).transpose * A⁻¹ * (LDL.diag hA * (LDL.lower hA).transpose).transpose =
    LDL.diag hA * (LDL.lower hA).transpose * A⁻¹ * (LDL.diag hA * (LDL.lower hA).transpose).conjTranspose
Tactic:
rfl
Proof state after:
no goals
Theorem: Matrix.LogDetAtom.feasibility_PosDef'
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef
Tactic:
have hY_tri : upperTriangular Y := by
{ rw [hY]
  apply upperTriangular.mul
  apply BlockTriangular_diagonal
  apply lowerTriangular.transpose
  apply LDL.lowerTriangular_lower }
Proof state after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef
Theorem: Matrix.LogDetAtom.feasibility_PosDef'
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef
Tactic:
haveI := hA.Invertible
Proof state after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
this : Invertible A
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef
Theorem: Matrix.LogDetAtom.feasibility_PosDef'
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
this : Invertible A
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef
Tactic:
rw [hZ, hY_tri.toUpperTri_eq]
Proof state after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
this : Invertible A
⊢ (D.fromBlocks Y Y.transpose A).PosSemidef
Theorem: Matrix.LogDetAtom.feasibility_PosDef'
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
this : Invertible A
⊢ (D.fromBlocks Y Y.transpose A).PosSemidef
Tactic:
apply LogDetAtom.feasibility_PosDef _ _ hY
Proof state after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
this : Invertible A
⊢ D = LDL.diag hA
Theorem: Matrix.LogDetAtom.feasibility_PosDef'
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
hY_tri : Y.upperTriangular
this : Invertible A
⊢ D = LDL.diag hA
Tactic:
simp [hD, hY, LDL.diag]
Proof state after:
no goals
Theorem: Matrix.LogDetAtom.feasibility_PosDef'
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ Y.upperTriangular
Tactic:
rw [hY]
Proof state after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.diag hA * (LDL.lower hA).transpose).upperTriangular
Theorem: Matrix.LogDetAtom.feasibility_PosDef'
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.diag hA * (LDL.lower hA).transpose).upperTriangular
Tactic:
apply upperTriangular.mul
Proof state after:
case hM
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.diag hA).upperTriangular

case hN
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.lower hA).transpose.upperTriangular
Theorem: Matrix.LogDetAtom.feasibility_PosDef'
Proof state before:
case hM
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.diag hA).upperTriangular

case hN
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.lower hA).transpose.upperTriangular
Tactic:
apply BlockTriangular_diagonal
Proof state after:
case hN
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.lower hA).transpose.upperTriangular
Theorem: Matrix.LogDetAtom.feasibility_PosDef'
Proof state before:
case hN
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.lower hA).transpose.upperTriangular
Tactic:
apply lowerTriangular.transpose
Proof state after:
case hN.hM
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.lower hA).lowerTriangular
Theorem: Matrix.LogDetAtom.feasibility_PosDef'
Proof state before:
case hN.hM
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z Y : Matrix n n ℝ
hY : Y = LDL.diag hA * (LDL.lower hA).transpose
hD : D = diagonal Y.diag
hZ : Z = Y.toUpperTri
⊢ (LDL.lower hA).lowerTriangular
Tactic:
apply LDL.lowerTriangular_lower
Proof state after:
no goals
Theorem: Matrix.LDL.diagEntries_pos
Proof 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
⊢ 0 < LDL.diagEntries hA i
Tactic:
have : (LDL.lowerInv hA).det ≠ 0 := by simp [LDL.det_lowerInv hA]
Proof 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
this : (LDL.lowerInv hA).det ≠ 0
⊢ 0 < LDL.diagEntries hA i
Theorem: Matrix.LDL.diagEntries_pos
Proof 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
this : (LDL.lowerInv hA).det ≠ 0
⊢ 0 < LDL.diagEntries hA i
Tactic:
have : LDL.lowerInv hA i ≠ 0 := fun h =>
  this (Matrix.det_eq_zero_of_row_eq_zero i (λ j => congr_fun h j))
Proof 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
this✝ : (LDL.lowerInv hA).det ≠ 0
this : LDL.lowerInv hA i ≠ 0
⊢ 0 < LDL.diagEntries hA i
Theorem: Matrix.LDL.diagEntries_pos
Proof 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
this✝ : (LDL.lowerInv hA).det ≠ 0
this : LDL.lowerInv hA i ≠ 0
⊢ 0 < LDL.diagEntries hA i
Tactic:
exact hA.2 (LDL.lowerInv hA i) this
Proof state after:
no goals
Theorem: Matrix.LDL.diagEntries_pos
Proof 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.lowerInv hA).det ≠ 0
Tactic:
simp [LDL.det_lowerInv hA]
Proof state after:
no goals
Theorem: Matrix.LogDetAtom.solution_eq_atom
Proof 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]
Proof 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
Theorem: Matrix.LogDetAtom.solution_eq_atom
Proof 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))
Proof 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
Theorem: Matrix.LogDetAtom.solution_eq_atom
Proof 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]
Proof state after:
no goals
Theorem: Matrix.LogDetAtom.feasibility_exp
Proof 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 ≤ (LDL.diag hA * (LDL.lower hA).transpose).diag i
Tactic:
simp [LDL.diag]
Proof state after:
no goals
Theorem: Matrix.IsHermitian₁₁_of_IsHermitian_toBlock
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA : A✝.PosDef
A B C D : Matrix n n ℝ
h : (A.fromBlocks B C D).IsHermitian
⊢ A.IsHermitian
Tactic:
ext i j
Proof state after:
case a
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA : A✝.PosDef
A B C D : Matrix n n ℝ
h : (A.fromBlocks B C D).IsHermitian
i j : n
⊢ A.conjTranspose i j = A i j
Theorem: Matrix.IsHermitian₁₁_of_IsHermitian_toBlock
Proof state before:
case a
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA : A✝.PosDef
A B C D : Matrix n n ℝ
h : (A.fromBlocks B C D).IsHermitian
i j : n
⊢ A.conjTranspose i j = A i j
Tactic:
simpa using congr_fun (congr_fun h (Sum.inl i)) (Sum.inl j)
Proof state after:
no goals
Theorem: Matrix.IsHermitian₂₂_of_IsHermitian_toBlock
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA : A✝.PosDef
A B C D : Matrix n n ℝ
h : (A.fromBlocks B C D).IsHermitian
⊢ D.IsHermitian
Tactic:
ext i j
Proof state after:
case a
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA : A✝.PosDef
A B C D : Matrix n n ℝ
h : (A.fromBlocks B C D).IsHermitian
i j : n
⊢ D.conjTranspose i j = D i j
Theorem: Matrix.IsHermitian₂₂_of_IsHermitian_toBlock
Proof state before:
case a
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA : A✝.PosDef
A B C D : Matrix n n ℝ
h : (A.fromBlocks B C D).IsHermitian
i j : n
⊢ D.conjTranspose i j = D i j
Tactic:
simpa using congr_fun (congr_fun h (Sum.inr i)) (Sum.inr j)
Proof state after:
no goals
Theorem: Matrix.PosSemidef₁₁_of_PosSemidef_toBlock
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA : A✝.PosDef
A B C D : Matrix n n ℝ
h : (A.fromBlocks B C D).PosSemidef
x : n → ℝ
⊢ 0 ≤ star x ⬝ᵥ A.mulVec x
Tactic:
simpa [Matrix.fromBlocks_mulVec, star] using h.2 (Sum.elim x 0)
Proof state after:
no goals
Theorem: Matrix.PosSemidef₂₂_of_PosSemidef_toBlock
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A✝ : Matrix n n ℝ
hA : A✝.PosDef
A B C D : Matrix n n ℝ
h : (A.fromBlocks B C D).PosSemidef
x : n → ℝ
⊢ 0 ≤ star x ⬝ᵥ D.mulVec x
Tactic:
simpa [Matrix.fromBlocks_mulVec, star] using h.2 (Sum.elim 0 x)
Proof state after:
no goals
Theorem: Matrix.LogDetAtom.optimality_D_posdef
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
⊢ D.PosDef
Tactic:
have h_D_psd : D.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_psd : D.PosSemidef
⊢ D.PosDef
Theorem: Matrix.LogDetAtom.optimality_D_posdef
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_psd : D.PosSemidef
⊢ D.PosDef
Tactic:
{ rw [h_D_psd.PosDef_iff_det_ne_zero, hD, det_diagonal, Finset.prod_ne_zero_iff]
  exact λ i _ => ne_of_gt (lt_of_lt_of_le ((t i).exp_pos) (ht i)) }
Proof state after:
no goals
Theorem: Matrix.LogDetAtom.optimality_D_posdef
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_psd : D.PosSemidef
⊢ D.PosDef
Tactic:
rw [h_D_psd.PosDef_iff_det_ne_zero, hD, det_diagonal, Finset.prod_ne_zero_iff]
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_psd : D.PosSemidef
⊢ ∀ a ∈ Finset.univ, Y.diag a ≠ 0
Theorem: Matrix.LogDetAtom.optimality_D_posdef
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_psd : D.PosSemidef
⊢ ∀ a ∈ Finset.univ, Y.diag a ≠ 0
Tactic:
exact λ i _ => ne_of_gt (lt_of_lt_of_le ((t i).exp_pos) (ht i))
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
⊢ D.det ≤ A.det
Tactic:
by_cases h_nonempty : Nonempty n
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
⊢ 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
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
⊢ 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 } }
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
⊢ 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
⊢ D.det ≤ A.det
Tactic:
{ haveI h_empty := not_nonempty_iff.1 h_nonempty
  simp [Matrix.det_isEmpty] }
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
⊢ D.det ≤ A.det
Tactic:
have h_D_pd : D.PosDef := LogDetAtom.optimality_D_posdef ht hD hZ 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
⊢ D.det ≤ A.det