Commit 2023-06-15 06:12 15656ac1

View on Github →

feat: port Analysis.InnerProductSpace.Spectrum (#5058)

depends on: #4920

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/InnerProductSpace/Spectrum.lean

added theorem LinearMap.IsSymmetric.apply_eigenvectorBasis

added theorem LinearMap.IsSymmetric.conj_eigenvalue_eq_self

added theorem LinearMap.IsSymmetric.diagonalization_apply_self_apply

added theorem LinearMap.IsSymmetric.diagonalization_symm_apply

added theorem LinearMap.IsSymmetric.directSum_decompose_apply

added theorem LinearMap.IsSymmetric.direct_sum_isInternal

added theorem LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply

added theorem LinearMap.IsSymmetric.hasEigenvalue_eigenvalues

added theorem LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis

added theorem LinearMap.IsSymmetric.invariant_orthogonalComplement_eigenspace

added theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces

added theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot'

added theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot

added theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant

added theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspaces'

added theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspaces

added theorem eigenvalue_nonneg_of_nonneg

added theorem eigenvalue_pos_of_pos

added theorem inner_product_apply_eigenvector

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

added def Module.End.Eigenvalues.val