Commit 2021-11-05 23:39 8174bd07

feat(analysis/inner_product_space/rayleigh): Rayleigh quotient produces eigenvectors (#9840) Define self_adjoint for an operator T to mean ∀ x y, ⟪T x, y⟫ = ⟪x, T y⟫. (This doesn't require a definition of adjoint, although that will come soon.). Prove that a local extremum of the Rayleigh quotient of a self-adjoint operator on the unit sphere is an eigenvector, and use this to prove that in finite dimension a self-adjoint operator has an eigenvector.