Commit 2025-05-11 03:00 5170427c

View on Github →

feat: sort eigenvalues in Analysis.InnerProductSpace.Spectrum (#24178) Spectrum.eigenvalues and Spectrum.eigenvectorBasis now give the eigenvalues and eigenvectors in increasing order of eigenvalues, which clears a prior TODO. The new theorem eigenvalues_monotone allows the monotonicity to be used downstream.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Spectrum.lean

modified theorem LinearMap.IsSymmetric.apply_eigenvectorBasis

modified theorem LinearMap.IsSymmetric.diagonalization_apply_self_apply

modified theorem LinearMap.IsSymmetric.diagonalization_symm_apply

added theorem LinearMap.IsSymmetric.eigenvalues_antitone

modified theorem LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply

modified theorem LinearMap.IsSymmetric.hasEigenvalue_eigenvalues

modified theorem LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis