[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
⊢ ↑T v ∈ (eigenspace T μ)ᗮ
[PROOFSTEP]
intro w hw
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
⊢ inner w (↑T v) = 0
[PROOFSTEP]
have : T w = (μ : 𝕜) • w := by rwa [mem_eigenspace_iff] at hw 
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
⊢ ↑T w = μ • w
[PROOFSTEP]
rwa [mem_eigenspace_iff] at hw 
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
this : ↑T w = μ • w
⊢ inner w (↑T v) = 0
[PROOFSTEP]
simp [← hT w, this, inner_smul_left, hv w hw]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
hμ : HasEigenvalue T μ
⊢ ↑(starRingEnd 𝕜) μ = μ
[PROOFSTEP]
obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
hμ : HasEigenvalue T μ
v : E
hv₁ : v ∈ eigenspace T μ
hv₂ : v ≠ 0
⊢ ↑(starRingEnd 𝕜) μ = μ
[PROOFSTEP]
rw [mem_eigenspace_iff] at hv₁ 
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
hμ : HasEigenvalue T μ
v : E
hv₁ : ↑T v = μ • v
hv₂ : v ≠ 0
⊢ ↑(starRingEnd 𝕜) μ = μ
[PROOFSTEP]
simpa [hv₂, inner_smul_left, inner_smul_right, hv₁] using hT v v
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
⊢ OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T μ }) fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)
[PROOFSTEP]
rintro μ ν hμν ⟨v, hv⟩ ⟨w, hw⟩
[GOAL]
case mk.mk
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
⊢ inner (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) μ) { val := v, property := hv })
      (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) ν) { val := w, property := hw }) =
    0
[PROOFSTEP]
by_cases hv' : v = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : v = 0
⊢ inner (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) μ) { val := v, property := hv })
      (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) ν) { val := w, property := hw }) =
    0
[PROOFSTEP]
simp [hv']
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : ¬v = 0
⊢ inner (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) μ) { val := v, property := hv })
      (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) ν) { val := w, property := hw }) =
    0
[PROOFSTEP]
have H := hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector ⟨hv, hv'⟩)
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : ¬v = 0
H : ↑(starRingEnd 𝕜) μ = μ
⊢ inner (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) μ) { val := v, property := hv })
      (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) ν) { val := w, property := hw }) =
    0
[PROOFSTEP]
rw [mem_eigenspace_iff] at hv hw 
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv✝ : v ∈ eigenspace T μ
hv : ↑T v = μ • v
w : E
hw✝ : w ∈ eigenspace T ν
hw : ↑T w = ν • w
hv' : ¬v = 0
H : ↑(starRingEnd 𝕜) μ = μ
⊢ inner (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) μ) { val := v, property := hv✝ })
      (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) ν) { val := w, property := hw✝ }) =
    0
[PROOFSTEP]
refine' Or.resolve_left _ hμν.symm
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv✝ : v ∈ eigenspace T μ
hv : ↑T v = μ • v
w : E
hw✝ : w ∈ eigenspace T ν
hw : ↑T w = ν • w
hv' : ¬v = 0
H : ↑(starRingEnd 𝕜) μ = μ
⊢ ν = μ ∨
    inner (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) μ) { val := v, property := hv✝ })
        (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) ν) { val := w, property := hw✝ }) =
      0
[PROOFSTEP]
simpa [inner_smul_left, inner_smul_right, hv, hw, H] using (hT v w).symm
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
v : E
hv : v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
⊢ ↑T v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
[PROOFSTEP]
rw [← Submodule.iInf_orthogonal] at hv ⊢
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
v : E
hv : v ∈ ⨅ (i : 𝕜), (eigenspace T i)ᗮ
⊢ ↑T v ∈ ⨅ (i : 𝕜), (eigenspace T i)ᗮ
[PROOFSTEP]
exact T.iInf_invariant hT.invariant_orthogonalComplement_eigenspace v hv
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
⊢ eigenspace (restrict T (_ : ∀ ⦃v : E⦄, v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ → ↑T v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ)) μ = ⊥
[PROOFSTEP]
set p : Submodule 𝕜 E := (⨆ μ, eigenspace T μ)ᗮ
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
p : Submodule 𝕜 E := (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
⊢ eigenspace (restrict T (_ : ∀ ⦃v : E⦄, v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ → ↑T v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ)) μ = ⊥
[PROOFSTEP]
refine' eigenspace_restrict_eq_bot hT.orthogonalComplement_iSup_eigenspaces_invariant _
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
p : Submodule 𝕜 E := (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
⊢ Disjoint (eigenspace T μ) (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
[PROOFSTEP]
have H₂ : eigenspace T μ ⟂ p := (Submodule.isOrtho_orthogonal_right _).mono_left (le_iSup _ _)
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
p : Submodule 𝕜 E := (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
H₂ : eigenspace T μ ⟂ p
⊢ Disjoint (eigenspace T μ) (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
[PROOFSTEP]
exact H₂.disjoint
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
⊢ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ = ⊥
[PROOFSTEP]
have hT' : IsSymmetric _ := hT.restrict_invariant hT.orthogonalComplement_iSup_eigenspaces_invariant
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
hT' : IsSymmetric (restrict T (_ : ∀ ⦃v : E⦄, v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ → ↑T v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ))
⊢ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ = ⊥
[PROOFSTEP]
haveI := hT'.subsingleton_of_no_eigenvalue_finiteDimensional hT.orthogonalComplement_iSup_eigenspaces
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
hT' : IsSymmetric (restrict T (_ : ∀ ⦃v : E⦄, v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ → ↑T v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ))
this : Subsingleton { x // x ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ }
⊢ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ = ⊥
[PROOFSTEP]
exact Submodule.eq_bot_of_subsingleton _
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
⊢ (⨆ (μ : { μ // eigenspace T μ ≠ ⊥ }), eigenspace T ↑μ)ᗮ = ⊥
[PROOFSTEP]
rw [iSup_ne_bot_subtype, hT.orthogonalComplement_iSup_eigenspaces_eq_bot]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT✝ : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
hT : Fact (IsSymmetric T)
μ : Eigenvalues T
⊢ CompleteSpace { x // x ∈ eigenspace T (↑T μ) }
[PROOFSTEP]
infer_instance
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
v : E
μ : Eigenvalues T
⊢ ↑(diagonalization hT) (↑T v) μ = ↑T μ • ↑(diagonalization hT) v μ
[PROOFSTEP]
suffices
  ∀ w : PiLp 2 fun μ : Eigenvalues T => eigenspace T μ,
    T (hT.diagonalization.symm w) = hT.diagonalization.symm fun μ => (μ : 𝕜) • w μ
  by
  simpa only [LinearIsometryEquiv.symm_apply_apply, LinearIsometryEquiv.apply_symm_apply] using
    congr_arg (fun w => hT.diagonalization w μ) (this (hT.diagonalization v))
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
v : E
μ : Eigenvalues T
this :
  ∀ (w : PiLp 2 fun μ => { x // x ∈ eigenspace T (↑T μ) }),
    ↑T (↑(LinearIsometryEquiv.symm (diagonalization hT)) w) =
      ↑(LinearIsometryEquiv.symm (diagonalization hT)) fun μ => ↑T μ • w μ
⊢ ↑(diagonalization hT) (↑T v) μ = ↑T μ • ↑(diagonalization hT) v μ
[PROOFSTEP]
simpa only [LinearIsometryEquiv.symm_apply_apply, LinearIsometryEquiv.apply_symm_apply] using
  congr_arg (fun w => hT.diagonalization w μ) (this (hT.diagonalization v))
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
v : E
μ : Eigenvalues T
⊢ ∀ (w : PiLp 2 fun μ => { x // x ∈ eigenspace T (↑T μ) }),
    ↑T (↑(LinearIsometryEquiv.symm (diagonalization hT)) w) =
      ↑(LinearIsometryEquiv.symm (diagonalization hT)) fun μ => ↑T μ • w μ
[PROOFSTEP]
intro w
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
v : E
μ : Eigenvalues T
w : PiLp 2 fun μ => { x // x ∈ eigenspace T (↑T μ) }
⊢ ↑T (↑(LinearIsometryEquiv.symm (diagonalization hT)) w) =
    ↑(LinearIsometryEquiv.symm (diagonalization hT)) fun μ => ↑T μ • w μ
[PROOFSTEP]
have hwT : ∀ μ, T (w μ) = (μ : 𝕜) • w μ := fun μ => mem_eigenspace_iff.1 (w μ).2
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
v : E
μ : Eigenvalues T
w : PiLp 2 fun μ => { x // x ∈ eigenspace T (↑T μ) }
hwT : ∀ (μ : Eigenvalues T), ↑T ↑(w μ) = ↑(↑T μ • w μ)
⊢ ↑T (↑(LinearIsometryEquiv.symm (diagonalization hT)) w) =
    ↑(LinearIsometryEquiv.symm (diagonalization hT)) fun μ => ↑T μ • w μ
[PROOFSTEP]
simp only [hwT, diagonalization_symm_apply, map_sum, Submodule.coe_smul_of_tower]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
⊢ HasEigenvector T (↑(eigenvalues hT hn i)) (↑(eigenvectorBasis hT hn) i)
[PROOFSTEP]
let v : E := hT.eigenvectorBasis hn i
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
⊢ HasEigenvector T (↑(eigenvalues hT hn i)) (↑(eigenvectorBasis hT hn) i)
[PROOFSTEP]
let μ : 𝕜 := (hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i hT.orthogonalFamily_eigenspaces').val
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
⊢ HasEigenvector T (↑(eigenvalues hT hn i)) (↑(eigenvectorBasis hT hn) i)
[PROOFSTEP]
simp_rw [eigenvalues]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
⊢ HasEigenvector T
    (↑(↑IsROrC.re
        (↑T
          (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn
            (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
            (_ :
              OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
                Submodule.subtypeₗᵢ (eigenspace T (↑T μ)))))))
    (↑(eigenvectorBasis hT hn) i)
[PROOFSTEP]
change HasEigenvector T (IsROrC.re μ) v
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
⊢ HasEigenvector T (↑(↑IsROrC.re μ)) v
[PROOFSTEP]
have key : HasEigenvector T μ v :=
  by
  have H₁ : v ∈ eigenspace T μ := by
    simp_rw [eigenvectorBasis]
    exact hT.direct_sum_isInternal.subordinateOrthonormalBasis_subordinate hn i hT.orthogonalFamily_eigenspaces'
  have H₂ : v ≠ 0 := by simpa using (hT.eigenvectorBasis hn).toBasis.ne_zero i
  exact ⟨H₁, H₂⟩
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
⊢ HasEigenvector T μ v
[PROOFSTEP]
have H₁ : v ∈ eigenspace T μ := by
  simp_rw [eigenvectorBasis]
  exact hT.direct_sum_isInternal.subordinateOrthonormalBasis_subordinate hn i hT.orthogonalFamily_eigenspaces'
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
⊢ v ∈ eigenspace T μ
[PROOFSTEP]
simp_rw [eigenvectorBasis]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
⊢ ↑(DirectSum.IsInternal.subordinateOrthonormalBasis hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ))
          (_ :
            OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
              Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
      i ∈
    eigenspace T
      (↑T
        (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn
          (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
          (_ :
            OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
              Submodule.subtypeₗᵢ (eigenspace T (↑T μ)))))
[PROOFSTEP]
exact hT.direct_sum_isInternal.subordinateOrthonormalBasis_subordinate hn i hT.orthogonalFamily_eigenspaces'
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
H₁ : v ∈ eigenspace T μ
⊢ HasEigenvector T μ v
[PROOFSTEP]
have H₂ : v ≠ 0 := by simpa using (hT.eigenvectorBasis hn).toBasis.ne_zero i
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
H₁ : v ∈ eigenspace T μ
⊢ v ≠ 0
[PROOFSTEP]
simpa using (hT.eigenvectorBasis hn).toBasis.ne_zero i
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
H₁ : v ∈ eigenspace T μ
H₂ : v ≠ 0
⊢ HasEigenvector T μ v
[PROOFSTEP]
exact ⟨H₁, H₂⟩
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
key : HasEigenvector T μ v
⊢ HasEigenvector T (↑(↑IsROrC.re μ)) v
[PROOFSTEP]
have re_μ : ↑(IsROrC.re μ) = μ := by
  rw [← IsROrC.conj_eq_iff_re]
  exact hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector key)
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
key : HasEigenvector T μ v
⊢ ↑(↑IsROrC.re μ) = μ
[PROOFSTEP]
rw [← IsROrC.conj_eq_iff_re]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
key : HasEigenvector T μ v
⊢ ↑(starRingEnd 𝕜) μ = μ
[PROOFSTEP]
exact hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector key)
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
key : HasEigenvector T μ v
re_μ : ↑(↑IsROrC.re μ) = μ
⊢ HasEigenvector T (↑(↑IsROrC.re μ)) v
[PROOFSTEP]
simpa [re_μ] using key
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
v : E
i : Fin n
⊢ ↑(eigenvectorBasis hT hn).repr (↑T v) i = ↑(eigenvalues hT hn i) * ↑(eigenvectorBasis hT hn).repr v i
[PROOFSTEP]
suffices
  ∀ w : EuclideanSpace 𝕜 (Fin n),
    T ((hT.eigenvectorBasis hn).repr.symm w) = (hT.eigenvectorBasis hn).repr.symm fun i => hT.eigenvalues hn i * w i
  by
  simpa [OrthonormalBasis.sum_repr_symm] using
    congr_arg (fun v => (hT.eigenvectorBasis hn).repr v i) (this ((hT.eigenvectorBasis hn).repr v))
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
v : E
i : Fin n
this :
  ∀ (w : EuclideanSpace 𝕜 (Fin n)),
    ↑T (↑(LinearIsometryEquiv.symm (eigenvectorBasis hT hn).repr) w) =
      ↑(LinearIsometryEquiv.symm (eigenvectorBasis hT hn).repr) fun i => ↑(eigenvalues hT hn i) * w i
⊢ ↑(eigenvectorBasis hT hn).repr (↑T v) i = ↑(eigenvalues hT hn i) * ↑(eigenvectorBasis hT hn).repr v i
[PROOFSTEP]
simpa [OrthonormalBasis.sum_repr_symm] using
  congr_arg (fun v => (hT.eigenvectorBasis hn).repr v i) (this ((hT.eigenvectorBasis hn).repr v))
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
v : E
i : Fin n
⊢ ∀ (w : EuclideanSpace 𝕜 (Fin n)),
    ↑T (↑(LinearIsometryEquiv.symm (eigenvectorBasis hT hn).repr) w) =
      ↑(LinearIsometryEquiv.symm (eigenvectorBasis hT hn).repr) fun i => ↑(eigenvalues hT hn i) * w i
[PROOFSTEP]
intro w
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
⊢ ↑T (↑(LinearIsometryEquiv.symm (eigenvectorBasis hT hn).repr) w) =
    ↑(LinearIsometryEquiv.symm (eigenvectorBasis hT hn).repr) fun i => ↑(eigenvalues hT hn i) * w i
[PROOFSTEP]
simp_rw [← OrthonormalBasis.sum_repr_symm, LinearMap.map_sum, LinearMap.map_smul, apply_eigenvectorBasis]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
⊢ ∑ x : Fin n, w x • ↑(eigenvalues hT hn x) • ↑(eigenvectorBasis hT hn) x =
    ∑ x : Fin n, (↑(eigenvalues hT hn x) * w x) • ↑(eigenvectorBasis hT hn) x
[PROOFSTEP]
apply Fintype.sum_congr
[GOAL]
case h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
⊢ ∀ (a : Fin n),
    w a • ↑(eigenvalues hT hn a) • ↑(eigenvectorBasis hT hn) a =
      (↑(eigenvalues hT hn a) * w a) • ↑(eigenvectorBasis hT hn) a
[PROOFSTEP]
intro a
[GOAL]
case h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
a : Fin n
⊢ w a • ↑(eigenvalues hT hn a) • ↑(eigenvectorBasis hT hn) a =
    (↑(eigenvalues hT hn a) * w a) • ↑(eigenvectorBasis hT hn) a
[PROOFSTEP]
rw [smul_smul, mul_comm]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : 𝕜
v : E
T : E →ₗ[𝕜] E
h : v ∈ eigenspace T μ
⊢ inner v (↑T v) = μ * ↑‖v‖ ^ 2
[PROOFSTEP]
simp only [mem_eigenspace_iff.mp h, inner_smul_right, inner_self_eq_norm_sq_to_K]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
⊢ 0 ≤ μ
[PROOFSTEP]
obtain ⟨v, hv⟩ := hμ.exists_hasEigenvector
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
⊢ 0 ≤ μ
[PROOFSTEP]
have hpos : (0 : ℝ) < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using hv.2
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
⊢ 0 < ‖v‖ ^ 2
[PROOFSTEP]
simpa only [sq_pos_iff, norm_ne_zero_iff] using hv.2
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
⊢ 0 ≤ μ
[PROOFSTEP]
have : IsROrC.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2 :=
  by
  have :=
    congr_arg IsROrC.re
      (inner_product_apply_eigenvector hv.1)
        -- porting note: why can't `exact_mod_cast` do this? These lemmas are marked `norm_cast`
  rw [← IsROrC.ofReal_pow, ← IsROrC.ofReal_mul] at this 
  exact_mod_cast this
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
⊢ ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
[PROOFSTEP]
have :=
  congr_arg IsROrC.re
    (inner_product_apply_eigenvector hv.1)
      -- porting note: why can't `exact_mod_cast` do this? These lemmas are marked `norm_cast`
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : ↑IsROrC.re (inner v (↑T v)) = ↑IsROrC.re (↑μ * ↑‖v‖ ^ 2)
⊢ ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
[PROOFSTEP]
rw [← IsROrC.ofReal_pow, ← IsROrC.ofReal_mul] at this 
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : ↑IsROrC.re (inner v (↑T v)) = ↑IsROrC.re ↑(μ * ‖v‖ ^ 2)
⊢ ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
[PROOFSTEP]
exact_mod_cast this
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
⊢ 0 ≤ μ
[PROOFSTEP]
exact (zero_le_mul_right hpos).mp (this ▸ hnn v)
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
⊢ 0 < μ
[PROOFSTEP]
obtain ⟨v, hv⟩ := hμ.exists_hasEigenvector
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
⊢ 0 < μ
[PROOFSTEP]
have hpos : (0 : ℝ) < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using hv.2
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
⊢ 0 < ‖v‖ ^ 2
[PROOFSTEP]
simpa only [sq_pos_iff, norm_ne_zero_iff] using hv.2
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
⊢ 0 < μ
[PROOFSTEP]
have : IsROrC.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2 :=
  by
  have :=
    congr_arg IsROrC.re
      (inner_product_apply_eigenvector hv.1)
        -- porting note: why can't `exact_mod_cast` do this? These lemmas are marked `norm_cast`
  rw [← IsROrC.ofReal_pow, ← IsROrC.ofReal_mul] at this 
  exact_mod_cast this
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
⊢ ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
[PROOFSTEP]
have :=
  congr_arg IsROrC.re
    (inner_product_apply_eigenvector hv.1)
      -- porting note: why can't `exact_mod_cast` do this? These lemmas are marked `norm_cast`
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : ↑IsROrC.re (inner v (↑T v)) = ↑IsROrC.re (↑μ * ↑‖v‖ ^ 2)
⊢ ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
[PROOFSTEP]
rw [← IsROrC.ofReal_pow, ← IsROrC.ofReal_mul] at this 
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : ↑IsROrC.re (inner v (↑T v)) = ↑IsROrC.re ↑(μ * ‖v‖ ^ 2)
⊢ ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
[PROOFSTEP]
exact_mod_cast this
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
⊢ 0 < μ
[PROOFSTEP]
exact (zero_lt_mul_right hpos).mp (this ▸ hnn v)
