internlm/Lean-Github huggingface dataset:
Theorem: LinearMap.spectral_theorem'
Proof state before:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : DecidableEq 𝕜
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
v : E
i : Fin n
xs : OrthonormalBasis (Fin n) 𝕜 E
as : Fin n → ℝ
hxs : ∀ (j : Fin n), Module.End.HasEigenvector T (↑(as j)) (xs j)
⊢ xs.repr (T v) i = ↑(as i) * xs.repr v i
Tactic:
suffices hsuff : ∀ (w : EuclideanSpace 𝕜 (Fin n)),
  T (xs.repr.symm w) = xs.repr.symm (fun i => as i * w i) by
    simpa only [LinearIsometryEquiv.symm_apply_apply,
      LinearIsometryEquiv.apply_symm_apply]
      using congr_arg (fun (v : E) => (xs.repr) v i) (hsuff ((xs.repr) v))
Proof state after:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : DecidableEq 𝕜
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
v : E
i : Fin n
xs : OrthonormalBasis (Fin n) 𝕜 E
as : Fin n → ℝ
hxs : ∀ (j : Fin n), Module.End.HasEigenvector T (↑(as j)) (xs j)
⊢ ∀ (w : EuclideanSpace 𝕜 (Fin n)), T (xs.repr.symm w) = xs.repr.symm fun i => ↑(as i) * w i
Theorem: LinearMap.spectral_theorem'
Proof state before:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : DecidableEq 𝕜
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
v : E
i : Fin n
xs : OrthonormalBasis (Fin n) 𝕜 E
as : Fin n → ℝ
hxs : ∀ (j : Fin n), Module.End.HasEigenvector T (↑(as j)) (xs j)
⊢ ∀ (w : EuclideanSpace 𝕜 (Fin n)), T (xs.repr.symm w) = xs.repr.symm fun i => ↑(as i) * w i
Tactic:
intros w
Proof state after:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : DecidableEq 𝕜
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
v : E
i : Fin n
xs : OrthonormalBasis (Fin n) 𝕜 E
as : Fin n → ℝ
hxs : ∀ (j : Fin n), Module.End.HasEigenvector T (↑(as j)) (xs j)
w : EuclideanSpace 𝕜 (Fin n)
⊢ T (xs.repr.symm w) = xs.repr.symm fun i => ↑(as i) * w i
Theorem: LinearMap.spectral_theorem'
Proof state before:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : DecidableEq 𝕜
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
v : E
i : Fin n
xs : OrthonormalBasis (Fin n) 𝕜 E
as : Fin n → ℝ
hxs : ∀ (j : Fin n), Module.End.HasEigenvector T (↑(as j)) (xs j)
w : EuclideanSpace 𝕜 (Fin n)
⊢ T (xs.repr.symm w) = xs.repr.symm fun i => ↑(as i) * w i
Tactic:
simp_rw [← OrthonormalBasis.sum_repr_symm, map_sum, LinearMap.map_smul,
  fun j => Module.End.mem_eigenspace_iff.mp (hxs j).1, smul_smul, mul_comm]
Proof state after:
no goals
Theorem: LinearMap.spectral_theorem'
Proof state before:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : DecidableEq 𝕜
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
v : E
i : Fin n
xs : OrthonormalBasis (Fin n) 𝕜 E
as : Fin n → ℝ
hxs : ∀ (j : Fin n), Module.End.HasEigenvector T (↑(as j)) (xs j)
hsuff : ∀ (w : EuclideanSpace 𝕜 (Fin n)), T (xs.repr.symm w) = xs.repr.symm fun i => ↑(as i) * w i
⊢ xs.repr (T v) i = ↑(as i) * xs.repr v i
Tactic:
simpa only [LinearIsometryEquiv.symm_apply_apply,
  LinearIsometryEquiv.apply_symm_apply]
  using congr_arg (fun (v : E) => (xs.repr) v i) (hsuff ((xs.repr) v))
Proof state after:
no goals
Theorem: Matrix.IsHermitian.hasEigenvector_eigenvectorBasis
Proof state before:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
i : n
⊢ Module.End.HasEigenvector (toLin' A) (↑(hA.eigenvalues i)) (hA.eigenvectorBasis i)
Tactic:
simp only [IsHermitian.eigenvectorBasis, OrthonormalBasis.coe_reindex]
Proof state after:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
i : n
⊢ Module.End.HasEigenvector (toLin' A) (↑(hA.eigenvalues i))
    ((⇑(⋯.eigenvectorBasis ⋯) ∘ ⇑(Fintype.equivOfCardEq ⋯).symm) i)
Theorem: Matrix.IsHermitian.hasEigenvector_eigenvectorBasis
Proof state before:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
i : n
⊢ Module.End.HasEigenvector (toLin' A) (↑(hA.eigenvalues i))
    ((⇑(⋯.eigenvectorBasis ⋯) ∘ ⇑(Fintype.equivOfCardEq ⋯).symm) i)
Tactic:
apply LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis
Proof state after:
no goals
Theorem: Matrix.spectral_theorem
Proof state before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n) * A = diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)
Tactic:
rw [basis_toMatrix_basisFun_mul]
Proof state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ (of fun i j => (xs.toBasis.repr (A.transpose j)) i) =
    diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)
Theorem: Matrix.spectral_theorem
Proof state before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ (of fun i j => (xs.toBasis.repr (A.transpose j)) i) =
    diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)
Tactic:
ext i j
Proof state after:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j
Theorem: Matrix.spectral_theorem
Proof state before:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j
Tactic:
let xs' := xs.reindex (Fintype.equivOfCardEq (Fintype.card_fin _)).symm
Proof state after:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j
Theorem: Matrix.spectral_theorem
Proof state before:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j
Tactic:
let as' : Fin (Fintype.card n) → ℝ :=
  fun i => as <| (Fintype.equivOfCardEq (Fintype.card_fin _)) i
Proof state after:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j
Theorem: Matrix.spectral_theorem
Proof state before:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j
Tactic:
have hxs' : ∀ j, Module.End.HasEigenvector (Matrix.toLin' A) (as' j) (xs' j) := by
  simp only [xs', OrthonormalBasis.coe_reindex, Equiv.symm_symm]
  intros j
  exact (hxs ((Fintype.equivOfCardEq (Fintype.card_fin _)) j))
Proof state after:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j
Theorem: Matrix.spectral_theorem
Proof state before:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j
Tactic:
convert @LinearMap.spectral_theorem' 𝕜 _
  (PiLp 2 (fun (_ : n) => 𝕜)) _ _ (Fintype.card n) (Matrix.toLin' A)
  (EuclideanSpace.single j 1)
  ((Fintype.equivOfCardEq (Fintype.card_fin _)).symm i)
  xs' as' hxs'
Proof state after:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    xs'.repr ((toLin' A) (EuclideanSpace.single j 1)) ((Fintype.equivOfCardEq ⋯).symm i)

case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) * xs'.repr (EuclideanSpace.single j 1) ((Fintype.equivOfCardEq ⋯).symm i)
Theorem: Matrix.spectral_theorem
Proof state before:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    xs'.repr ((toLin' A) (EuclideanSpace.single j 1)) ((Fintype.equivOfCardEq ⋯).symm i)

case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) * xs'.repr (EuclideanSpace.single j 1) ((Fintype.equivOfCardEq ⋯).symm i)
Tactic:
{ erw [toLin'_apply]
  simp only [xs', OrthonormalBasis.coe_toBasis_repr_apply, of_apply,
    OrthonormalBasis.repr_reindex]
  erw [Equiv.symm_apply_apply, EuclideanSpace.single, WithLp.equiv_symm_pi_apply 2, mulVec_single]
  simp_rw [mul_one]
  rfl }
Proof state after:
case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) * xs'.repr (EuclideanSpace.single j 1) ((Fintype.equivOfCardEq ⋯).symm i)
Theorem: Matrix.spectral_theorem
Proof state before:
case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) * xs'.repr (EuclideanSpace.single j 1) ((Fintype.equivOfCardEq ⋯).symm i)
Tactic:
{ simp only [diagonal_mul, Function.comp]
  erw [Basis.toMatrix_apply, OrthonormalBasis.coe_toBasis_repr_apply,
    OrthonormalBasis.repr_reindex, Pi.basisFun_apply, LinearMap.coe_stdBasis,
    EuclideanSpace.single, WithLp.equiv_symm_pi_apply 2,
    Equiv.symm_apply_apply, Equiv.apply_symm_apply]
  congr; simp }
Proof state after:
no goals
Theorem: Matrix.spectral_theorem
Proof state before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
⊢ ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
Tactic:
simp only [xs', OrthonormalBasis.coe_reindex, Equiv.symm_symm]
Proof state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
⊢ ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) ((⇑xs ∘ ⇑(Fintype.equivOfCardEq ⋯)) j)
Theorem: Matrix.spectral_theorem
Proof state before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
⊢ ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) ((⇑xs ∘ ⇑(Fintype.equivOfCardEq ⋯)) j)
Tactic:
intros j
Proof state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j✝ : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
j : Fin (Fintype.card n)
⊢ Module.End.HasEigenvector (toLin' A) (↑(as' j)) ((⇑xs ∘ ⇑(Fintype.equivOfCardEq ⋯)) j)
Theorem: Matrix.spectral_theorem
Proof state before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j✝ : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
j : Fin (Fintype.card n)
⊢ Module.End.HasEigenvector (toLin' A) (↑(as' j)) ((⇑xs ∘ ⇑(Fintype.equivOfCardEq ⋯)) j)
Tactic:
exact (hxs ((Fintype.equivOfCardEq (Fintype.card_fin _)) j))
Proof state after:
no goals
Theorem: Matrix.spectral_theorem
Proof state before:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    xs'.repr ((toLin' A) (EuclideanSpace.single j 1)) ((Fintype.equivOfCardEq ⋯).symm i)
Tactic:
erw [toLin'_apply]
Proof state after:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    xs'.repr (A.mulVec (EuclideanSpace.single j 1)) ((Fintype.equivOfCardEq ⋯).symm i)
Theorem: Matrix.spectral_theorem
Proof state before:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    xs'.repr (A.mulVec (EuclideanSpace.single j 1)) ((Fintype.equivOfCardEq ⋯).symm i)
Tactic:
simp only [xs', OrthonormalBasis.coe_toBasis_repr_apply, of_apply,
  OrthonormalBasis.repr_reindex]
Proof state after:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ xs.repr (A.transpose j) i =
    xs.repr (A.mulVec (EuclideanSpace.single j 1))
      ((Fintype.equivOfCardEq ⋯).symm.symm ((Fintype.equivOfCardEq ⋯).symm i))
Theorem: Matrix.spectral_theorem
Proof state before:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ xs.repr (A.transpose j) i =
    xs.repr (A.mulVec (EuclideanSpace.single j 1))
      ((Fintype.equivOfCardEq ⋯).symm.symm ((Fintype.equivOfCardEq ⋯).symm i))
Tactic:
erw [Equiv.symm_apply_apply, EuclideanSpace.single, WithLp.equiv_symm_pi_apply 2, mulVec_single]
Proof state after:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ EquivLike.coe xs.repr (A.transpose j) i = xs.repr (fun i => A i j * 1) i