mathlib refactor(analysis/inner_product_space): rename `is_self_adjoint` to `is_symmetric` and add `is_self

refactor(analysis/inner_product_space): rename `is_self_adjoint` to `is_symmetric` and add `is_self_adjoint`

Open mcdoll opened this issue 3 years ago • 4 comments

We rename the current inner_product_space.is_self_adjoint to linear_map.is_symmetric (which states that inner (A x) y = inner x (A y) for all x,y : E) and add a new definition is_self_adjoint for has_star R. This definition is used to state theorems that were previously stated for linear_map.is_symmetric, but are actually about self-adjointness for continuous_linear_map. The Hellinger-Toeplitz theorem then becomes the construction of a self-adjoint operator from a symmetric operator, which is consistent with the functional analysis literature. Moreover, since the definitions are now in the correct namespaces, we can use dot-notation. Consequently, most parts of inner_product_space/rayleigh and inner_product_space/spectrum now use is_self_adjoint and are also now in the continuous_linear_map.is_self_adjoint namespace. For the finite-dimensional case we use is_symmetric, since continuity is not used anywhere. Finally, there are some minor cleanups in the matrix diagonalization file.

Jul 13 '22 22:07 mcdoll

Am I correct in saying an operator is self-adjoint iff it's symmetric, unconditionally? If so, there's definitely no need for two separate predicates.

Jul 13 '22 22:07 vihdzp

The assertion is true modulo distinguishing between continuous_linear_map and linear_map and when your linear_maps are not a special kind of linear_pmaps (which is an implementation detail). The point why mathematicians distinguish between symmetrical and self-adjoint is that the two definitions are not equal for linear_pmaps - we don't have the definition of an adjoint there (yet. I am working on it) - and you cannot call the symmetry condition is_self_adjoint and similarly you cannot say that there is a spectral theorem of symmetric operators, but for self-adjoint operators. So while from a formal point of view you can remove one definition you really can't from a mathematical point of view.

Jul 14 '22 02:07 mcdoll

bors d=j-loreaux

Jul 27 '22 12:07 ocfnash

:v: j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.