mathlib3

8174bd07 - feat(analysis/inner_product_space/rayleigh): Rayleigh quotient produces eigenvectors (#9840)

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. Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca> Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca>