[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
⊢ lowerInv hS = (Basis.toMatrix (Pi.basisFun 𝕜 n) ↑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))ᵀ
[PROOFSTEP]
letI := NormedAddCommGroup.ofMatrix hS.transpose
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
this : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix (_ : PosDef Sᵀ)
⊢ lowerInv hS = (Basis.toMatrix (Pi.basisFun 𝕜 n) ↑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))ᵀ
[PROOFSTEP]
letI := InnerProductSpace.ofMatrix hS.transpose
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
this✝ : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix (_ : PosDef Sᵀ)
this : InnerProductSpace 𝕜 (n → 𝕜) := InnerProductSpace.ofMatrix (_ : PosDef Sᵀ)
⊢ lowerInv hS = (Basis.toMatrix (Pi.basisFun 𝕜 n) ↑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))ᵀ
[PROOFSTEP]
ext i j
[GOAL]
case a.h
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
this✝ : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix (_ : PosDef Sᵀ)
this : InnerProductSpace 𝕜 (n → 𝕜) := InnerProductSpace.ofMatrix (_ : PosDef Sᵀ)
i j : n
⊢ lowerInv hS i j = (Basis.toMatrix (Pi.basisFun 𝕜 n) ↑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))ᵀ i j
[PROOFSTEP]
rw [LDL.lowerInv, Basis.coePiBasisFun.toMatrix_eq_transpose, coe_gramSchmidtBasis]
[GOAL]
case a.h
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
this✝ : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix (_ : PosDef Sᵀ)
this : InnerProductSpace 𝕜 (n → 𝕜) := InnerProductSpace.ofMatrix (_ : PosDef Sᵀ)
i j : n
⊢ gramSchmidt 𝕜 (↑(Pi.basisFun 𝕜 n)) i j = (gramSchmidt 𝕜 ↑(Pi.basisFun 𝕜 n))ᵀᵀ i j
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
⊢ Invertible (lowerInv hS)
[PROOFSTEP]
rw [LDL.lowerInv_eq_gramSchmidtBasis]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
⊢ Invertible (Basis.toMatrix (Pi.basisFun 𝕜 n) ↑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))ᵀ
[PROOFSTEP]
haveI :=
  Basis.invertibleToMatrix (Pi.basisFun 𝕜 n)
    (@gramSchmidtBasis 𝕜 (n → 𝕜) _ (_ : _) (InnerProductSpace.ofMatrix hS.transpose) n _ _ _ (Pi.basisFun 𝕜 n))
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
this : Invertible (Basis.toMatrix (Pi.basisFun 𝕜 n) ↑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))
⊢ Invertible (Basis.toMatrix (Pi.basisFun 𝕜 n) ↑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))ᵀ
[PROOFSTEP]
infer_instance
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
i j : n
hij : i < j
⊢ lowerInv hS i j = 0
[PROOFSTEP]
rw [←
  @gramSchmidt_triangular 𝕜 (n → 𝕜) _ (_ : _) (InnerProductSpace.ofMatrix hS.transpose) n _ _ _ i j hij
    (Pi.basisFun 𝕜 n),
  Pi.basisFun_repr, LDL.lowerInv]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
⊢ diag hS = lowerInv hS * S * (lowerInv hS)ᴴ
[PROOFSTEP]
ext i j
[GOAL]
case a.h
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
i j : n
⊢ diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
[PROOFSTEP]
by_cases hij : i = j
[GOAL]
case pos
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
i j : n
hij : i = j
⊢ diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
[PROOFSTEP]
simp only [diag, diagEntries, EuclideanSpace.inner_piLp_equiv_symm, star_star, hij, diagonal_apply_eq, Matrix.mul_assoc]
[GOAL]
case pos
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
i j : n
hij : i = j
⊢ lowerInv hS j ⬝ᵥ mulVec S (star (lowerInv hS j)) = (lowerInv hS * (S * (lowerInv hS)ᴴ)) j j
[PROOFSTEP]
rfl
[GOAL]
case neg
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
i j : n
hij : ¬i = j
⊢ diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
[PROOFSTEP]
simp only [LDL.diag, hij, diagonal_apply_ne, Ne.def, not_false_iff, mul_mul_apply]
[GOAL]
case neg
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
i j : n
hij : ¬i = j
⊢ 0 = lowerInv hS i ⬝ᵥ mulVec S ((lowerInv hS)ᴴᵀ j)
[PROOFSTEP]
rw [conjTranspose, transpose_map, transpose_transpose, dotProduct_mulVec,
  (LDL.lowerInv_orthogonal hS fun h : j = i => hij h.symm).symm, ← inner_conj_symm, mulVec_transpose,
  EuclideanSpace.inner_piLp_equiv_symm, ← IsROrC.star_def, ← star_dotProduct_star, dotProduct_comm, star_star]
[GOAL]
case neg
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
i j : n
hij : ¬i = j
⊢ vecMul (lowerInv hS i) S ⬝ᵥ star (lowerInv hS j) = vecMul (lowerInv hS i) S ⬝ᵥ map (lowerInv hS) star j
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
⊢ lower hS * diag hS * (lower hS)ᴴ = S
[PROOFSTEP]
rw [LDL.lower, conjTranspose_nonsing_inv, Matrix.mul_assoc,
  Matrix.inv_mul_eq_iff_eq_mul_of_invertible (LDL.lowerInv hS), Matrix.mul_inv_eq_iff_eq_mul_of_invertible]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
⊢ diag hS = lowerInv hS * S * (lowerInv hS)ᴴ
[PROOFSTEP]
exact LDL.diag_eq_lowerInv_conj hS
