Commit 2023-06-15 05:48 990b386a

View on Github →

feat: port Analysis.InnerProductSpace.Rayleigh (#4920)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/InnerProductSpace/Rayleigh.lean

added theorem ContinuousLinearMap.iInf_rayleigh_eq_iInf_rayleigh_sphere

added theorem ContinuousLinearMap.iSup_rayleigh_eq_iSup_rayleigh_sphere

added theorem ContinuousLinearMap.image_rayleigh_eq_image_rayleigh_sphere

added theorem ContinuousLinearMap.rayleigh_smul

added theorem IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn

added theorem IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn_real

added theorem IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn

added theorem IsSelfAdjoint.hasEigenvector_of_isMaxOn

added theorem IsSelfAdjoint.hasEigenvector_of_isMinOn

added theorem IsSelfAdjoint.linearly_dependent_of_isLocalExtrOn

added theorem LinearMap.IsSymmetric.hasEigenvalue_iInf_of_finiteDimensional

added theorem LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional

added theorem LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf

added theorem LinearMap.IsSymmetric.subsingleton_of_no_eigenvalue_finiteDimensional