[Merged by Bors] - refactor(analysis/inner_product_space): rename is_self_adjoint to is_symmetric and add is_self_adjoint

[mcdoll]

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.

---

[vihdzp]

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.

[mcdoll]

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.

[j-loreaux]

Other than some small golfs I think this looks good.

[j-loreaux]

There are a few more minor things to do, but it's getting close. Moreover, I think this diff makes it clear that this (the is_self_adjoint predicate) is a good change.

[hrmacbeth]

Is this a regression? This seems to me like a situation where it would be convenient to keep using is_symmetric rather than switch to the new is_self_adjoint. The current definition requires E →L[𝕜] E but the early lemmas will work for E →ₗ[𝕜] E and it seems like we should eventually switch to that setting. Unnecessary dependence on the adjoint here will make that impossible.

(If I missed an earlier discussion of this point, feel free to point me to it.)

[mcdoll]

Of course the lemmas work for both cases, they are equivalent. My point was if the operator is a-priori defined as a continuous linear operator, then one should use is_self_adjoint and if it is defined as a linear operator, then is_symmetric is the correct definition (as there is in general (i.e., infinite dimension) no adjoint).

[j-loreaux]

I think I agree with Heather here. This is the concrete definition of positivity, so the included selfadjoint condition should really be is_symmetric defined in terms of the inner product. Regressions aside, at the very least, if you're proving an operator is positive this way, it will likely be easy to show that it is symmetric (because you apparently have control over the values of the quadratic form), and then you don't need to invoke Hellinger-Toeplitz to get the selfadjoint condition.

[mcdoll]

Note that in the definition we assume that the operator is continuous. We could add a definition that constructs positive operator from linear_map that is symmetric and satisfies ∀ x, 0 ≤ T.re_apply_inner_self x. That would be the easiest way to construct a positive operator. I guess there is literature that proves the boundedness and the symmetry, but this is obviously redundant.

[j-loreaux]

I think maybe we are talking past each other, but I can't quite tell. Why not just have linear_map.is_positive defined as is_symmetric and ∀ x, 0 ≤ T.re_apply_inner_self x? Then it would apply in both situations (admittedly, dot notation wouldn't work so well anymore in the continuous case).

However, if your point is that is_positive should really be defined as is_self_adjoint and ∀ x, 0 ≤ T.re_apply_inner_self x for linear_pmaps in the unbounded case (as opposed to using is_symmetric), then I would prefer any definition which would unify the three settings, although I have some doubts whether this is really possible.

[mcdoll]

I agree that we might be not talking about the same thing. The current is_positive is defined for continuous_linear_map, so my point is that there is no reason to prefer is_symmetric over is_self_adjoint.
If it was defined for linear_map, then I would agree that is_symmetric is the correct choice. I don't think that changing the definition of is_positive from continuous_linear_map to linear_map is in the scope of this PR (I think the definition as it is now is good). Also, I don't really see the value in adding a definition linear_map.is_positive, but maybe you have a good reason for that. There might be an argument that it is necessary for the finite dimensional case, because we don't want to talk about continuous_linear_maps in finite dimensions.
As for the linear_pmap I cannot guarantee anything, but I am rather optimistic that we will need only two definitions (we could get away with one, but this would cause lots of annoying things with coercing to linear_pmap).

I am sorry if I come across as too stubborn on this, I only think that reverting to is_symmetric for continuous_linear_map would make this whole PR completely useless.

[hrmacbeth]

This also seems like a regression to me? This file currently does not "really" depend on the adjoint; it just has a spurious dependence introduced by #15281. But at this line you are proving a fact about a symmetric operator (in finite dimension) by invoking that it's self-adjoint (in the new, adjoint-dependent sense), then at line 245 calling a result is_self_adjoint.has_eigenvector_of_is_max_on which is proved for self-adjoint operators by at some point invoking hT.is_symmetric, the fact that they are symmetric.

After the renaming PR goes through I hope immediately to separate out is_symmetric, and make the Rayleigh file import only that. If that's to be possible, then this file needs to stay more or less as it was.

[mcdoll]

I guess you could argue that the finite dimension part should use is_self_adjoint (E →ₗ[𝕜] E) with finite dimensional adjoint, but it felt to me that that was really splitting hairs.

[mcdoll]

In this case here I was just using the totally overblown Hellinger-Toeplitz theorem to upgrade a linear map to a continuous linear map, so that on can use the things that are defined for is_self_adjoint (E →L[𝕜] E)

[hrmacbeth]

I guess you could argue that the finite dimension part should use is_self_adjoint (E →ₗ[𝕜] E) with finite dimensional adjoint, but it felt to me that that was really splitting hairs.

I was actually arguing the opposite, that the infinite dimension part should use is_symmetric ...

[mcdoll]

I know, but the whole point why I made this refactor is that I find that this goes too much against the mathematical standards. Technically you could say that the spectral theorem holds for bounded symmetric operators, but nobody does that. Moreover, the Rayleigh quotient is very useful for unbounded operators, so I would argue that the correct definition would be for is_self_adjoint (linear_pmap R E F), but unfortunately the adjoint is not yet defined for linear_pmap

[j-loreaux]

Per the discussion on Zulip, it seems that this PR is okay as-is.
bors r+

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed (retrying...):

• Build mathlib
• Lint mathlib
• Run tests

[j-loreaux]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests