[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ eigenvectorMatrix hA * eigenvectorMatrixInv hA = 1
[PROOFSTEP]
apply Basis.toMatrix_mul_toMatrix_flip
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
⊢ eigenvectorMatrix hA i j = ↑(eigenvectorBasis hA) j i
[PROOFSTEP]
simp_rw [eigenvectorMatrix, Basis.toMatrix_apply, OrthonormalBasis.coe_toBasis, PiLp.basisFun_repr]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
⊢ eigenvectorMatrixInv hA i j = star (↑(eigenvectorBasis hA) i j)
[PROOFSTEP]
rw [eigenvectorMatrixInv, Basis.toMatrix_apply, OrthonormalBasis.coe_toBasis_repr_apply,
  OrthonormalBasis.repr_apply_apply, PiLp.basisFun_apply, PiLp.equiv_symm_single, EuclideanSpace.inner_single_right,
  one_mul, IsROrC.star_def]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ (eigenvectorMatrixInv hA)ᴴ = eigenvectorMatrix hA
[PROOFSTEP]
ext i j
[GOAL]
case a.h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
⊢ (eigenvectorMatrixInv hA)ᴴ i j = eigenvectorMatrix hA i j
[PROOFSTEP]
rw [conjTranspose_apply, eigenvectorMatrixInv_apply, eigenvectorMatrix_apply, star_star]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ (eigenvectorMatrix hA)ᴴ = eigenvectorMatrixInv hA
[PROOFSTEP]
rw [← conjTranspose_eigenvectorMatrixInv, conjTranspose_conjTranspose]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ eigenvectorMatrixInv hA * A = diagonal (IsROrC.ofReal ∘ eigenvalues hA) * eigenvectorMatrixInv hA
[PROOFSTEP]
rw [eigenvectorMatrixInv, PiLp.basis_toMatrix_basisFun_mul]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ (↑of fun i j =>
      ↑(↑(OrthonormalBasis.toBasis (eigenvectorBasis hA)).repr (↑(PiLp.equiv 2 fun i => 𝕜).symm (Aᵀ j))) i) =
    diagonal (IsROrC.ofReal ∘ eigenvalues hA) *
      Basis.toMatrix (OrthonormalBasis.toBasis (eigenvectorBasis hA)) ↑(PiLp.basisFun 2 𝕜 n)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
⊢ ↑of (fun i j => ↑(↑(OrthonormalBasis.toBasis (eigenvectorBasis hA)).repr (↑(PiLp.equiv 2 fun i => 𝕜).symm (Aᵀ j))) i)
      i j =
    (diagonal (IsROrC.ofReal ∘ eigenvalues hA) *
        Basis.toMatrix (OrthonormalBasis.toBasis (eigenvectorBasis hA)) ↑(PiLp.basisFun 2 𝕜 n))
      i j
[PROOFSTEP]
have := isHermitian_iff_isSymmetric.1 hA
[GOAL]
case a.h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
this : LinearMap.IsSymmetric (↑toEuclideanLin A)
⊢ ↑of (fun i j => ↑(↑(OrthonormalBasis.toBasis (eigenvectorBasis hA)).repr (↑(PiLp.equiv 2 fun i => 𝕜).symm (Aᵀ j))) i)
      i j =
    (diagonal (IsROrC.ofReal ∘ eigenvalues hA) *
        Basis.toMatrix (OrthonormalBasis.toBasis (eigenvectorBasis hA)) ↑(PiLp.basisFun 2 𝕜 n))
      i j
[PROOFSTEP]
convert
  this.eigenvectorBasis_apply_self_apply finrank_euclideanSpace (EuclideanSpace.single j 1)
    ((Fintype.equivOfCardEq (Fintype.card_fin _)).symm i) using
  1
[GOAL]
case h.e'_2
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
this : LinearMap.IsSymmetric (↑toEuclideanLin A)
⊢ ↑of (fun i j => ↑(↑(OrthonormalBasis.toBasis (eigenvectorBasis hA)).repr (↑(PiLp.equiv 2 fun i => 𝕜).symm (Aᵀ j))) i)
      i j =
    ↑(LinearMap.IsSymmetric.eigenvectorBasis this
            (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)).repr
      (↑(↑toEuclideanLin A) (EuclideanSpace.single j 1))
      (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)
[PROOFSTEP]
dsimp only [EuclideanSpace.single, toEuclideanLin_piLp_equiv_symm, toLin'_apply, Matrix.of_apply,
  IsHermitian.eigenvectorBasis]
[GOAL]
case h.e'_2
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
this : LinearMap.IsSymmetric (↑toEuclideanLin A)
⊢ ↑(↑(OrthonormalBasis.toBasis
                (OrthonormalBasis.reindex
                  (LinearMap.IsSymmetric.eigenvectorBasis (_ : LinearMap.IsSymmetric (↑toEuclideanLin A))
                    (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n))
                  (Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)))).repr
          (↑(PiLp.equiv 2 fun i => 𝕜).symm (Aᵀ j)))
      i =
    ↑(LinearMap.IsSymmetric.eigenvectorBasis this
            (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)).repr
      (↑(PiLp.equiv 2 fun i => 𝕜).symm (mulVec A (Pi.single j 1)))
      (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)
[PROOFSTEP]
simp_rw [mulVec_single, mul_one, OrthonormalBasis.coe_toBasis_repr_apply, OrthonormalBasis.repr_reindex]
[GOAL]
case h.e'_2
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
this : LinearMap.IsSymmetric (↑toEuclideanLin A)
⊢ ↑(LinearMap.IsSymmetric.eigenvectorBasis (_ : LinearMap.IsSymmetric (↑toEuclideanLin A))
            (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)).repr
      (↑(PiLp.equiv 2 fun i => 𝕜).symm (Aᵀ j))
      (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i) =
    ↑(LinearMap.IsSymmetric.eigenvectorBasis this
            (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)).repr
      (↑(PiLp.equiv 2 fun i => 𝕜).symm fun i => A i j)
      (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
this : LinearMap.IsSymmetric (↑toEuclideanLin A)
⊢ (diagonal (IsROrC.ofReal ∘ eigenvalues hA) *
        Basis.toMatrix (OrthonormalBasis.toBasis (eigenvectorBasis hA)) ↑(PiLp.basisFun 2 𝕜 n))
      i j =
    ↑(LinearMap.IsSymmetric.eigenvalues this (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)
          (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)) *
      ↑(LinearMap.IsSymmetric.eigenvectorBasis this
              (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)).repr
        (EuclideanSpace.single j 1)
        (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)
[PROOFSTEP]
simp only [diagonal_mul, (· ∘ ·), eigenvalues]
[GOAL]
case h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i j : n
this : LinearMap.IsSymmetric (↑toEuclideanLin A)
⊢ ↑(eigenvalues₀ hA (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)) *
      Basis.toMatrix (OrthonormalBasis.toBasis (eigenvectorBasis hA)) (↑(PiLp.basisFun 2 𝕜 n)) i j =
    ↑(LinearMap.IsSymmetric.eigenvalues this (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)
          (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)) *
      ↑(LinearMap.IsSymmetric.eigenvectorBasis this
              (_ : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n)).repr
        (EuclideanSpace.single j 1)
        (↑(Fintype.equivOfCardEq (_ : Fintype.card (Fin (Fintype.card n)) = Fintype.card n)).symm i)
[PROOFSTEP]
rw [eigenvectorBasis, Basis.toMatrix_apply, OrthonormalBasis.coe_toBasis_repr_apply, OrthonormalBasis.repr_reindex,
  eigenvalues₀, PiLp.basisFun_apply, PiLp.equiv_symm_single]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i : n
⊢ eigenvalues hA i = ↑IsROrC.re (star ((eigenvectorMatrix hA)ᵀ i) ⬝ᵥ mulVec A ((eigenvectorMatrix hA)ᵀ i))
[PROOFSTEP]
have := hA.spectral_theorem
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i : n
this : eigenvectorMatrixInv hA * A = diagonal (IsROrC.ofReal ∘ eigenvalues hA) * eigenvectorMatrixInv hA
⊢ eigenvalues hA i = ↑IsROrC.re (star ((eigenvectorMatrix hA)ᵀ i) ⬝ᵥ mulVec A ((eigenvectorMatrix hA)ᵀ i))
[PROOFSTEP]
rw [← @Matrix.mul_inv_eq_iff_eq_mul_of_invertible (A := hA.eigenvectorMatrixInv)] at this 
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i : n
this : eigenvectorMatrixInv hA * A * (eigenvectorMatrixInv hA)⁻¹ = diagonal (IsROrC.ofReal ∘ eigenvalues hA)
⊢ eigenvalues hA i = ↑IsROrC.re (star ((eigenvectorMatrix hA)ᵀ i) ⬝ᵥ mulVec A ((eigenvectorMatrix hA)ᵀ i))
[PROOFSTEP]
have := congr_arg IsROrC.re (congr_fun (congr_fun this i) i)
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i : n
this✝ : eigenvectorMatrixInv hA * A * (eigenvectorMatrixInv hA)⁻¹ = diagonal (IsROrC.ofReal ∘ eigenvalues hA)
this :
  ↑IsROrC.re ((eigenvectorMatrixInv hA * A * (eigenvectorMatrixInv hA)⁻¹) i i) =
    ↑IsROrC.re (diagonal (IsROrC.ofReal ∘ eigenvalues hA) i i)
⊢ eigenvalues hA i = ↑IsROrC.re (star ((eigenvectorMatrix hA)ᵀ i) ⬝ᵥ mulVec A ((eigenvectorMatrix hA)ᵀ i))
[PROOFSTEP]
rw [diagonal_apply_eq, Function.comp_apply, IsROrC.ofReal_re, inv_eq_left_inv hA.eigenvectorMatrix_mul_inv, ←
  conjTranspose_eigenvectorMatrix, mul_mul_apply] at this 
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
i : n
this✝ : eigenvectorMatrixInv hA * A * (eigenvectorMatrixInv hA)⁻¹ = diagonal (IsROrC.ofReal ∘ eigenvalues hA)
this : ↑IsROrC.re ((eigenvectorMatrix hA)ᴴ i ⬝ᵥ mulVec A ((eigenvectorMatrix hA)ᵀ i)) = eigenvalues hA i
⊢ eigenvalues hA i = ↑IsROrC.re (star ((eigenvectorMatrix hA)ᵀ i) ⬝ᵥ mulVec A ((eigenvectorMatrix hA)ᵀ i))
[PROOFSTEP]
exact this.symm
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ det A = ∏ i : n, ↑(eigenvalues hA i)
[PROOFSTEP]
apply mul_left_cancel₀ (det_ne_zero_of_left_inverse (eigenvectorMatrix_mul_inv hA))
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ det (eigenvectorMatrixInv hA) * det A = det (eigenvectorMatrixInv hA) * ∏ i : n, ↑(eigenvalues hA i)
[PROOFSTEP]
rw [← det_mul, spectral_theorem, det_mul, mul_comm, det_diagonal]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ det (eigenvectorMatrixInv hA) * ∏ i : n, (IsROrC.ofReal ∘ eigenvalues hA) i =
    det (eigenvectorMatrixInv hA) * ∏ i : n, ↑(eigenvalues hA i)
[PROOFSTEP]
simp_rw [Function.comp_apply]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ A = eigenvectorMatrix hA * diagonal (IsROrC.ofReal ∘ eigenvalues hA) * eigenvectorMatrixInv hA
[PROOFSTEP]
simpa [← Matrix.mul_assoc, hA.eigenvectorMatrix_mul_inv, Matrix.one_mul] using
  congr_arg (hA.eigenvectorMatrix * ·) hA.spectral_theorem
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ rank A = rank (diagonal (eigenvalues hA))
[PROOFSTEP]
conv_lhs => rw [hA.spectral_theorem']
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
| rank A
[PROOFSTEP]
rw [hA.spectral_theorem']
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
| rank A
[PROOFSTEP]
rw [hA.spectral_theorem']
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
| rank A
[PROOFSTEP]
rw [hA.spectral_theorem']
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ rank (eigenvectorMatrix hA * diagonal (IsROrC.ofReal ∘ eigenvalues hA) * eigenvectorMatrixInv hA) =
    rank (diagonal (eigenvalues hA))
[PROOFSTEP]
have hE := isUnit_det_of_invertible (hA.eigenvectorMatrix)
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
hE : IsUnit (det (eigenvectorMatrix hA))
⊢ rank (eigenvectorMatrix hA * diagonal (IsROrC.ofReal ∘ eigenvalues hA) * eigenvectorMatrixInv hA) =
    rank (diagonal (eigenvalues hA))
[PROOFSTEP]
have hiE := isUnit_det_of_invertible (hA.eigenvectorMatrixInv)
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
hE : IsUnit (det (eigenvectorMatrix hA))
hiE : IsUnit (det (eigenvectorMatrixInv hA))
⊢ rank (eigenvectorMatrix hA * diagonal (IsROrC.ofReal ∘ eigenvalues hA) * eigenvectorMatrixInv hA) =
    rank (diagonal (eigenvalues hA))
[PROOFSTEP]
simp only [rank_mul_eq_right_of_isUnit_det hA.eigenvectorMatrix _ hE,
  rank_mul_eq_left_of_isUnit_det hA.eigenvectorMatrixInv _ hiE, rank_diagonal, Function.comp_apply, ne_eq,
  algebraMap.lift_map_eq_zero_iff]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsHermitian A
⊢ rank A = Fintype.card { i // eigenvalues hA i ≠ 0 }
[PROOFSTEP]
rw [rank_eq_rank_diagonal hA, Matrix.rank_diagonal]
